diff --git a/fourmolu.yaml b/fourmolu.yaml index 2125efd2d..c83b2a03f 100644 --- a/fourmolu.yaml +++ b/fourmolu.yaml @@ -8,3 +8,11 @@ haddock-style: single-line newlines-between-decls: 1 single-constraint-parens: auto +# Foreword might not actually re-export _all_ operators from these modules, +# but this is a lot nicer than explicitly listing all of the ones that it does. +# For some reason they're not picked up with `module Foreword exports Protolude`. +reexports: + - module Foreword exports Prelude + - module Foreword exports Control.Applicative + - module Foreword exports Data.Function + - module Foreword exports Data.Monoid diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index 4f52b5c14..1196e3286 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -588,9 +588,8 @@ deleteSession = logAPI (noError DeleteSession) $ \sid -> do listSessions :: (MonadIO m, MonadAPILog l m) => OffsetLimit -> PrimerM m (Page Session) listSessions = logAPI (noError ListSessions) $ \ol -> do q <- asks dbOpQueue - callback <- liftIO - $ atomically - $ do + callback <- liftIO $ + atomically $ do cb <- newEmptyTMVar writeTBQueue q $ Database.ListSessions ol cb pure cb @@ -603,9 +602,8 @@ findSessions :: (MonadIO m, MonadAPILog l m) => Text -> OffsetLimit -> PrimerM m findSessions = curry $ logAPI (noError FindSessions) $ \case (substr, ol) -> do q <- asks dbOpQueue - callback <- liftIO - $ atomically - $ do + callback <- liftIO $ + atomically $ do cb <- newEmptyTMVar writeTBQueue q $ Database.FindSessions substr ol cb pure cb @@ -793,9 +791,8 @@ viewProg p = , constructors = case d of TypeDef.TypeDefPrim _ -> Nothing TypeDef.TypeDefAST t -> - Just - $ astTypeDefConstructors t - <&> \(TypeDef.ValCon nameCon argsCon) -> + Just $ + astTypeDefConstructors t <&> \(TypeDef.ValCon nameCon argsCon) -> ValCon { name = nameCon , fields = viewTreeType' . over _typeKindMeta (show . view _id) . over _typeMeta (show . view _id) <$> argsCon @@ -875,8 +872,8 @@ viewTreeExpr e0 = case e0 of , body = NoBody Flavor.Lam , childTrees = [RecordPair EdgeFlavor.Lam $ viewTreeExpr e] , rightChild = - Just - $ RecordPair + Just $ + RecordPair EdgeFlavor.Bind Tree { nodeId = bindingNodeId @@ -891,8 +888,8 @@ viewTreeExpr e0 = case e0 of , body = NoBody Flavor.LAM , childTrees = [RecordPair EdgeFlavor.Lam $ viewTreeExpr e] , rightChild = - Just - $ RecordPair + Just $ + RecordPair EdgeFlavor.Bind Tree { nodeId = bindingNodeId @@ -916,8 +913,8 @@ viewTreeExpr e0 = case e0 of , body = NoBody Flavor.Let , childTrees = [RecordPair EdgeFlavor.LetEqual $ viewTreeExpr e1, RecordPair EdgeFlavor.LetIn $ viewTreeExpr e2] , rightChild = - Just - $ RecordPair + Just $ + RecordPair EdgeFlavor.Bind Tree { nodeId = bindingNodeId @@ -932,8 +929,8 @@ viewTreeExpr e0 = case e0 of , body = NoBody Flavor.LetType , childTrees = [RecordPair EdgeFlavor.LetEqual $ viewTreeExpr e, RecordPair EdgeFlavor.LetIn $ viewTreeType t] , rightChild = - Just - $ RecordPair + Just $ + RecordPair EdgeFlavor.Bind Tree { nodeId = bindingNodeId @@ -948,8 +945,8 @@ viewTreeExpr e0 = case e0 of , body = NoBody Flavor.Letrec , childTrees = [RecordPair EdgeFlavor.LetEqual $ viewTreeExpr e1, RecordPair EdgeFlavor.Ann $ viewTreeType t, RecordPair EdgeFlavor.LetIn $ viewTreeExpr e2] , rightChild = - Just - $ RecordPair + Just $ + RecordPair EdgeFlavor.Bind Tree { nodeId = bindingNodeId @@ -1111,8 +1108,8 @@ viewTreeType' t0 = case t0 of , body = NoBody Flavor.TForall , childTrees = [RecordPair EdgeFlavor.ForallKind $ viewTreeKind' k, RecordPair EdgeFlavor.Forall $ viewTreeType' t] , rightChild = - Just - $ RecordPair + Just $ + RecordPair EdgeFlavor.Bind Tree { nodeId = bindingNodeId @@ -1127,8 +1124,8 @@ viewTreeType' t0 = case t0 of , body = NoBody Flavor.TLet , childTrees = [RecordPair EdgeFlavor.LetEqual $ viewTreeType' t, RecordPair EdgeFlavor.LetIn $ viewTreeType' b] , rightChild = - Just - $ RecordPair + Just $ + RecordPair EdgeFlavor.Bind Tree { nodeId = bindingNodeId @@ -1257,8 +1254,8 @@ evalFull' = curry4 $ logAPI (noError EvalFull') $ \(sid, lim, closed, d) -> do -- evaluation step will be to inline this definition, removing the node. let e = create' $ DSL.gvar d x <- - handleEvalFullRequest - $ EvalFullReq + handleEvalFullRequest $ + EvalFullReq { evalFullReqExpr = e , evalFullCxtDir = Chk , evalFullMaxSteps = fromMaybe 10 lim @@ -1343,8 +1340,8 @@ evalInterp' = curry $ logAPI (noError EvalInterp') $ \(sid, d) -> do -- evaluation step will be to inline this definition, removing the node. let e = create' $ DSL.gvar d (App.EvalInterpRespNormal e') <- - handleEvalInterpRequest - $ EvalInterpReq + handleEvalInterpRequest $ + EvalInterpReq { expr = e , dir = Chk } @@ -1437,8 +1434,8 @@ evalBoundedInterp' = curry3 $ logAPI (noError EvalBoundedInterp') $ \(sid, timeo -- evaluation step will be to inline this definition, removing the node. let e = create' $ DSL.gvar d x <- - handleEvalBoundedInterpRequest - $ EvalBoundedInterpReq + handleEvalBoundedInterpRequest $ + EvalBoundedInterpReq { expr = e , dir = Chk , timeout = fromMaybe (MicroSec 10) timeout @@ -1467,8 +1464,8 @@ createDefinition :: Maybe Text -> PrimerM m Prog createDefinition = - curry3 - $ logAPI (noError CreateDef) \(sid, moduleName, mDefName) -> + curry3 $ + logAPI (noError CreateDef) \(sid, moduleName, mDefName) -> edit sid (App.Edit [App.CreateDef moduleName mDefName]) >>= either (throwM . AddDefError moduleName mDefName) (pure . viewProg) @@ -1480,8 +1477,8 @@ createTypeDef :: [ValConName] -> PrimerM m Prog createTypeDef = - curry3 - $ logAPI (noError CreateTypeDef) \(sid, tyconName, valcons) -> + curry3 $ + logAPI (noError CreateTypeDef) \(sid, tyconName, valcons) -> edit sid (App.Edit [App.AddTypeDef tyconName $ ASTTypeDef [] (map (`TypeDef.ValCon` []) valcons) []]) >>= either (throwM . AddTypeDefError tyconName valcons) (pure . viewProg) @@ -1530,8 +1527,8 @@ actionOptions = curry4 $ logAPI (noError ActionOptions) $ \(sid, level, selectio allDefs = progDefMap prog allTypeDefs = progTypeDefMap prog def <- snd <$> findASTTypeOrTermDef prog selection - maybe (throwM $ ActionOptionsNoID selection) pure - $ Available.options allTypeDefs allDefs (progCxt prog) level def selection action + maybe (throwM $ ActionOptionsNoID selection) pure $ + Available.options allTypeDefs allDefs (progCxt prog) level def selection action findASTDef :: MonadThrow m => Map GVarName (Editable, Def.Def) -> GVarName -> m (Editable, ASTDef) findASTDef allDefs def = case allDefs Map.!? def of @@ -1562,8 +1559,8 @@ applyActionNoInput = curry3 $ logAPI (noError ApplyActionNoInput) $ \(sid, selec prog <- getProgram sid def <- snd <$> findASTTypeOrTermDef prog selection actions <- - either (throwM . ToProgActionError (Available.NoInput action)) pure - $ toProgActionNoInput (progDefMap prog) def selection action + either (throwM . ToProgActionError (Available.NoInput action)) pure $ + toProgActionNoInput (progDefMap prog) def selection action applyActions sid actions applyActionInput :: @@ -1576,8 +1573,8 @@ applyActionInput = curry3 $ logAPI (noError ApplyActionInput) $ \(sid, body, act prog <- getProgram sid def <- snd <$> findASTTypeOrTermDef prog body.selection actions <- - either (throwM . ToProgActionError (Available.Input action)) pure - $ toProgActionInput def body.selection body.option action + either (throwM . ToProgActionError (Available.Input action)) pure $ + toProgActionInput def body.selection body.option action applyActions sid actions data ApplyActionBody = ApplyActionBody diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs index 0e9e26b17..f0f097acc 100644 --- a/primer-api/test/Tests/API.hs +++ b/primer-api/test/Tests/API.hs @@ -808,30 +808,30 @@ test_eval_undo = Just e@EmptyHole{} -> pure $ getID e _ -> liftIO $ assertFailure "unexpected form of main" _ <- - expectSuccess - $ edit sid - $ Edit - [ MoveToDef $ qualifyName scope "main" - , BodyAction - [ SetCursor i1 - , InsertSaturatedVar $ GlobalVarRef Integer.even - ] - ] + expectSuccess $ + edit sid $ + Edit + [ MoveToDef $ qualifyName scope "main" + , BodyAction + [ SetCursor i1 + , InsertSaturatedVar $ GlobalVarRef Integer.even + ] + ] step "insert 4" i2 <- getMain >>= \case Just (App _ _ e) -> pure $ getID e _ -> liftIO $ assertFailure "unexpected form of main" _ <- - expectSuccess - $ edit sid - $ Edit - [ MoveToDef $ qualifyName scope "main" - , BodyAction - [ SetCursor i2 - , ConstructPrim $ PrimInt 4 - ] - ] + expectSuccess $ + edit sid $ + Edit + [ MoveToDef $ qualifyName scope "main" + , BodyAction + [ SetCursor i2 + , ConstructPrim $ PrimInt 4 + ] + ] step "get edited App" app0 <- getApp sid step "undo" @@ -876,12 +876,12 @@ test_selectioninfo = Just e@EmptyHole{} -> pure $ getID e _ -> assertFailure' $ "unexpected form of " <> toS (unName d) _ <- - expectSuccess - $ edit sid - $ Edit - [ MoveToDef $ qualifyName scope d - , BodyAction $ SetCursor i : as - ] + expectSuccess $ + edit sid $ + Edit + [ MoveToDef $ qualifyName scope d + , BodyAction $ SetCursor i : as + ] pure () let mkType d as = do _ <- expectSuccess $ edit sid $ Edit [CreateDef scope $ Just $ unName d] @@ -890,12 +890,12 @@ test_selectioninfo = Just e@TEmptyHole{} -> pure $ getID e _ -> assertFailure' $ "unexpected form of " <> toS (unName d) _ <- - expectSuccess - $ edit sid - $ Edit - [ MoveToDef $ qualifyName scope d - , SigAction $ SetCursor i : as - ] + expectSuccess $ + edit sid $ + Edit + [ MoveToDef $ qualifyName scope d + , SigAction $ SetCursor i : as + ] pure () step "tm1 :: ? = not {? Zero ?}" @@ -917,15 +917,15 @@ test_selectioninfo = e -> assertFailure' $ "unexpected form of tm1: " <> show e step "tm1 mismatch info" tm1tk <- - getSelectionTypeOrKind sid - $ SelectionDef - $ DefSelection (qualifyName scope "tm1") - $ Just - $ NodeSelection BodyNode htm1 + getSelectionTypeOrKind sid $ + SelectionDef $ + DefSelection (qualifyName scope "tm1") $ + Just $ + NodeSelection BodyNode htm1 zeroTKIds tm1tk @?= zeroTKIds - ( Type - $ Mismatch + ( Type $ + Mismatch { got = viewTreeType $ create' $ tcon tNat , expected = viewTreeType $ create' $ tcon tBool } @@ -952,15 +952,15 @@ test_selectioninfo = e -> assertFailure' $ "unexpected form of tm2: " <> show e step "tm2 mismatch info" tm2tk <- - getSelectionTypeOrKind sid - $ SelectionDef - $ DefSelection (qualifyName scope "tm2") - $ Just - $ NodeSelection BodyNode htm2 + getSelectionTypeOrKind sid $ + SelectionDef $ + DefSelection (qualifyName scope "tm2") $ + Just $ + NodeSelection BodyNode htm2 zeroTKIds tm2tk @?= zeroTKIds - ( Type - $ Mismatch + ( Type $ + Mismatch { got = viewTreeType $ create' $ tcon tNat , -- We require @expected@ to be an empty hole, matching -- the behaviour of @? True@ @@ -990,15 +990,15 @@ test_selectioninfo = e -> assertFailure' $ "unexpected form of ty1: " <> show e step "ty1 mismatch info" ty1tk <- - getSelectionTypeOrKind sid - $ SelectionDef - $ DefSelection (qualifyName scope "ty1") - $ Just - $ NodeSelection SigNode hty1 + getSelectionTypeOrKind sid $ + SelectionDef $ + DefSelection (qualifyName scope "ty1") $ + Just $ + NodeSelection SigNode hty1 zeroTKIds ty1tk @?= zeroTKIds - ( Kind - $ Mismatch + ( Kind $ + Mismatch { got = viewTreeKind $ create' $ ktype `kfun` ktype , expected = viewTreeKind $ create' ktype } @@ -1024,15 +1024,15 @@ test_selectioninfo = e -> assertFailure' $ "unexpected form of ty2: " <> show e step "ty2 mismatch info" ty2tk <- - getSelectionTypeOrKind sid - $ SelectionDef - $ DefSelection (qualifyName scope "ty2") - $ Just - $ NodeSelection SigNode hty2 + getSelectionTypeOrKind sid $ + SelectionDef $ + DefSelection (qualifyName scope "ty2") $ + Just $ + NodeSelection SigNode hty2 zeroTKIds ty2tk @?= zeroTKIds - ( Kind - $ Mismatch + ( Kind $ + Mismatch { got = viewTreeKind $ create' ktype , -- We require @expected@ to be @?@, matching the behaviour of an empty hole. -- Arguably we should change both this and the empty hole case to diff --git a/primer-api/test/Tests/Database.hs b/primer-api/test/Tests/Database.hs index a3d4ca30d..7d4aaf114 100644 --- a/primer-api/test/Tests/Database.hs +++ b/primer-api/test/Tests/Database.hs @@ -156,9 +156,8 @@ testSessionName testName t expected = [ testCase "unsafe" $ case mkSessionName t of Nothing -> assertFailure "name is invalid" Just sn -> fromSessionName sn @?= expected - , testCase "safe" - $ fromSessionName (safeMkSessionName t) - @?= expected + , testCase "safe" $ + fromSessionName (safeMkSessionName t) @?= expected ] emptyQHarness :: Text -> PrimerM (PureLogT (WithSeverity LogMsg) IO) () -> TestTree emptyQHarness desc test = testCaseSteps (toS desc) $ \step' -> do diff --git a/primer-api/testlib/Primer/API/Test/Util.hs b/primer-api/testlib/Primer/API/Test/Util.hs index 2c923275e..55f91c3f7 100644 --- a/primer-api/testlib/Primer/API/Test/Util.hs +++ b/primer-api/testlib/Primer/API/Test/Util.hs @@ -45,10 +45,9 @@ runAPI action = do dbOpQueue <- newTBQueueIO 1 initialSessions <- StmMap.newIO (r, logs) <- - withAsync (runNullDb' $ serve (ServiceCfg dbOpQueue version)) - $ const - $ runPureLogT - . runPrimerM action - $ Env initialSessions dbOpQueue version + withAsync (runNullDb' $ serve (ServiceCfg dbOpQueue version)) $ + const $ + runPureLogT . runPrimerM action $ + Env initialSessions dbOpQueue version assertNoSevereLogs logs pure r diff --git a/primer-benchmark/src/Benchmarks.hs b/primer-benchmark/src/Benchmarks.hs index 4c5f941a8..17244f04c 100644 --- a/primer-benchmark/src/Benchmarks.hs +++ b/primer-benchmark/src/Benchmarks.hs @@ -114,13 +114,13 @@ benchmarks = evalOptionsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False} evalOptionsR = RunRedexOptions{pushAndElide = True} evalTestMPureLogsStep e maxEvals = - evalTestM (maxID e) - $ runPureLogT - $ EFStep.evalFull @EFStep.EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) + evalTestM (maxID e) $ + runPureLogT $ + EFStep.evalFull @EFStep.EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) evalTestMDiscardLogsStep e maxEvals = - evalTestM (maxID e) - $ runDiscardLogT - $ EFStep.evalFull @EFStep.EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) + evalTestM (maxID e) $ + runDiscardLogT $ + EFStep.evalFull @EFStep.EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) evalTestMInterp e d = EFInterp.interp' builtinTypes (EFInterp.mkGlobalEnv $ defMap e) d (forgetMetadata $ expr e) @@ -143,9 +143,8 @@ benchmarks = tcTest id = evalTestM id . runExceptT @TypeError . tcWholeProgWithImports - benchTC e n = EnvBench e n $ \(prog, maxId, _) -> NF (tcTest maxId) prog - $ pure - $ \case + benchTC e n = EnvBench e n $ \(prog, maxId, _) -> NF (tcTest maxId) prog $ + pure $ \case Left err -> assertFailure $ "Failed to typecheck: " <> show err Right p -> assertBool "Unexpected smarthole changes" $ forgetProgTypecache p == forgetProgTypecache prog @@ -165,10 +164,8 @@ runTests :: [Benchmark] -> TestTree runTests = testGroup "Benchmark result tests" . map go where go (EnvBench act n b) = withResource act (const $ pure ()) $ \e -> - testCase (toS n) - $ e - >>= testBenchmarkable - . b + testCase (toS n) $ + e >>= testBenchmarkable . b go (Group n bs) = testGroup (toS n) $ map go bs testBenchmarkable (NF f x test) = test >>= ($ f x) diff --git a/primer-selda/src/Primer/Database/Selda/SQLite.hs b/primer-selda/src/Primer/Database/Selda/SQLite.hs index b477c77a8..20c0caba1 100644 --- a/primer-selda/src/Primer/Database/Selda/SQLite.hs +++ b/primer-selda/src/Primer/Database/Selda/SQLite.hs @@ -114,9 +114,8 @@ runSeldaSQLiteDbT db m = -- that is handled by this 'handleSeldaDbException' call must have -- occurred in 'withSQLite' itself (e.g., SQLite file not found); -- hence, we use 'ConnectionFailed' here. - convertSeldaDbException ConnectionFailed - $ withSQLite db - $ do + convertSeldaDbException ConnectionFailed $ + withSQLite db $ do -- By default, SQLite has a case-insensitive @LIKE@ -- implementation. See: -- https://www.sqlite.org/pragma.html#pragma_case_sensitive_like @@ -210,8 +209,8 @@ type MonadSeldaSQLiteDb m l = (ConvertLogMessage SeldaDbLogMessage l, MonadCatch instance MonadSeldaSQLiteDb m l => MonadDb (SeldaSQLiteDbT m) where insertSession v s a n t = do nr <- - convertSeldaDbException (InsertError s) - $ insert sessions [SessionRow s v (Aeson.encode a) (fromSessionName n) (utcTime t)] + convertSeldaDbException (InsertError s) $ + insert sessions [SessionRow s v (Aeson.encode a) (fromSessionName n) (utcTime t)] -- This operation should affect exactly one row. case nr of 0 -> throwM $ InsertZeroRowsAffected s @@ -220,8 +219,8 @@ instance MonadSeldaSQLiteDb m l => MonadDb (SeldaSQLiteDbT m) where updateSessionApp v s a t = do nr <- - convertSeldaDbException (UpdateAppError s) - $ update + convertSeldaDbException (UpdateAppError s) $ + update sessions (\session -> session ! #uuid .== literal s) (\session -> session `with` [#gitversion := literal v, #app := literal (Aeson.encode a), #lastmodified := literal (utcTime t)]) @@ -233,8 +232,8 @@ instance MonadSeldaSQLiteDb m l => MonadDb (SeldaSQLiteDbT m) where updateSessionName v s n t = do nr <- - convertSeldaDbException (UpdateNameError s) - $ update + convertSeldaDbException (UpdateNameError s) $ + update sessions (\session -> session ! #uuid .== literal s) (\session -> session `with` [#gitversion := literal v, #name := literal (fromSessionName n), #lastmodified := literal (utcTime t)]) @@ -245,9 +244,8 @@ instance MonadSeldaSQLiteDb m l => MonadDb (SeldaSQLiteDbT m) where _ -> throwM $ UpdateNameConsistencyError s listSessions ol = convertSeldaDbException ListSessionsError $ do - n' <- query - $ Selda.aggregate - $ do + n' <- query $ + Selda.aggregate $ do session <- allSessions pure $ Selda.count $ session ! #uuid n <- case n' of @@ -263,9 +261,8 @@ instance MonadSeldaSQLiteDb m l => MonadDb (SeldaSQLiteDbT m) where -- require some refactoring. See: -- -- https://github.com/hackworthltd/primer/issues/1037 - n' <- query - $ Selda.aggregate - $ do + n' <- query $ + Selda.aggregate $ do session <- sessionByNameSubstr substr pure $ Selda.count $ session ! #uuid n <- case n' of @@ -292,9 +289,9 @@ instance MonadSeldaSQLiteDb m l => MonadDb (SeldaSQLiteDbT m) where -- 'safeMkSessionName' here. let sessionName = safeMkSessionName n lastModified = LastModified t - when (fromSessionName sessionName /= n) - $ logError - $ IllegalSessionName sid n + when (fromSessionName sessionName /= n) $ + logError $ + IllegalSessionName sid n pure $ Right (SessionData decodedApp sessionName lastModified) deleteSession sid = convertSeldaDbException (DeleteSessionError sid) $ do diff --git a/primer-selda/testlib/Primer/Database/Selda/Test/Util.hs b/primer-selda/testlib/Primer/Database/Selda/Test/Util.hs index 616179937..ed80f5268 100644 --- a/primer-selda/testlib/Primer/Database/Selda/Test/Util.hs +++ b/primer-selda/testlib/Primer/Database/Selda/Test/Util.hs @@ -90,8 +90,8 @@ mkSessionRow :: Int -> IO SessionRow mkSessionRow n = do u <- nextRandom now <- lowPrecisionCurrentTime - pure - $ SessionRow + pure $ + SessionRow { uuid = u , gitversion = "test-version" , app = Aeson.encode newApp @@ -104,8 +104,8 @@ mkSessionRow' :: (Int -> Text) -> Int -> IO SessionRow mkSessionRow' mkName n = do u <- nextRandom now <- lowPrecisionCurrentTime - pure - $ SessionRow + pure $ + SessionRow { uuid = u , gitversion = "test-version" , app = Aeson.encode newApp diff --git a/primer-service/src/Primer/Finite.hs b/primer-service/src/Primer/Finite.hs index 7bf269f98..0cca5eb65 100644 --- a/primer-service/src/Primer/Finite.hs +++ b/primer-service/src/Primer/Finite.hs @@ -26,14 +26,10 @@ packFinite = fmap Finite . eitherToMaybe . refine instance (KnownNat l, KnownNat u) => ToParamSchema (Finite l u) where toParamSchema _ = toParamSchema (Proxy @Natural) - & #minimum - ?~ fromIntegral (natVal $ Proxy @l) - & #exclusiveMinimum - ?~ False - & #maximum - ?~ fromIntegral (natVal $ Proxy @u) - & #exclusiveMaximum - ?~ False + & #minimum ?~ fromIntegral (natVal $ Proxy @l) + & #exclusiveMinimum ?~ False + & #maximum ?~ fromIntegral (natVal $ Proxy @u) + & #exclusiveMaximum ?~ False instance (KnownNat l, KnownNat u, l <= u) => FromHttpApiData (Finite l u) where parseUrlPiece x = do diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index 81abd8d1e..a603eb8f9 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -125,11 +125,10 @@ deriving via PrimerJSON Session instance ToSchema Session -- https://hackage.haskell.org/package/openapi3-3.2.2/docs/src/Data.OpenApi.Internal.Schema.html#line-662 instance ToSchema LastModified where declareNamedSchema _ = - pure - $ named "LastModified" - $ timeSchema "date-time" - & #example - ?~ toJSON (UTCTime (fromGregorian 2022 10 20) 0) + pure $ + named "LastModified" $ + timeSchema "date-time" + & #example ?~ toJSON (UTCTime (fromGregorian 2022 10 20) 0) instance ToParamSchema LastModified where toParamSchema _ = timeParamSchema "date-time" diff --git a/primer-service/src/Primer/Pagination.hs b/primer-service/src/Primer/Pagination.hs index 02d12ff49..071d52c72 100644 --- a/primer-service/src/Primer/Pagination.hs +++ b/primer-service/src/Primer/Pagination.hs @@ -82,10 +82,8 @@ instance ToHttpApiData Positive where instance ToParamSchema Positive where toParamSchema _ = toParamSchema (Proxy @Int) - & #minimum - ?~ 0 - & #exclusiveMinimum - ?~ True + & #minimum ?~ 0 + & #exclusiveMinimum ?~ True instance ToSchema Positive where declareNamedSchema = plain . toParamSchema diff --git a/primer-service/src/Primer/Server.hs b/primer-service/src/Primer/Server.hs index f4c2859ff..4f88c406a 100644 --- a/primer-service/src/Primer/Server.hs +++ b/primer-service/src/Primer/Server.hs @@ -127,15 +127,9 @@ type ConvertServerLogs l = openAPIInfo :: OpenApi openAPIInfo = toOpenApi (Proxy @OpenAPI.API) - & #info - % #title - .~ "Primer backend API" - & #info - % #description - ?~ "A backend service implementing a pedagogic functional programming language." - & #info - % #version - .~ "0.7" + & #info % #title .~ "Primer backend API" + & #info % #description ?~ "A backend service implementing a pedagogic functional programming language." + & #info % #version .~ "0.7" & refParamSchemas @Level [ ("/openapi/sessions/{sessionId}/action/available", "level") , ("/openapi/sessions/{sessionId}/action/options", "level") @@ -159,20 +153,13 @@ openAPIInfo = refParamSchemas :: forall a. ToSchema a => [(FilePath, Text)] -> OpenApi -> OpenApi refParamSchemas params api = api - & #components - % #schemas - %~ IOHM.insert name (toSchema $ Proxy @a) - & #paths - %~ composeList (map (uncurry $ flip adjustParam) params) + & #components % #schemas %~ IOHM.insert name (toSchema $ Proxy @a) + & #paths %~ composeList (map (uncurry $ flip adjustParam) params) where composeList = appEndo . foldMap' Endo adjustParam paramName = - IOHM.adjust - $ #post - % mapped - % #parameters - % mapped - %~ \case + IOHM.adjust $ + #post % mapped % #parameters % mapped %~ \case Inline x | x ^. #name == paramName -> Inline $ x & #schema ?~ Ref (Reference name) p -> p name = show $ typeRep @a @@ -386,15 +373,14 @@ serve :: Log.Handler IO (Log.WithSeverity l) -> IO () serve ss q v port origins logger = do - Warp.runSettings warpSettings - $ noCache - $ - -- It may make sense to allow access to some resources - -- regardless of origin, but for now, we use a blanket CORS - -- policy for every resource, hence the 'const' function here. - cors (const $ Just $ apiCors origins) - $ metrics - $ genericServeT nt server + Warp.runSettings warpSettings $ + noCache $ + -- It may make sense to allow access to some resources + -- regardless of origin, but for now, we use a blanket CORS + -- policy for every resource, hence the 'const' function here. + cors (const $ Just $ apiCors origins) $ + metrics $ + genericServeT nt server where -- By default Warp will try to bind on either IPv4 or IPv6, whichever is -- available. @@ -412,14 +398,13 @@ serve ss q v port origins logger = do nt :: Primer l a -> Handler a nt m = - Handler - $ ExceptT - $ flip runLoggingT logger - $ do - -- This is not guaranteed to be consecutive with the logs from the action in the case of concurrent actions - -- (unlikely in a dev environment, except perhaps a getProgram&getActions request) - logInfo RequestStart - catch (Right <$> runPrimerM m (Env ss q v)) handler + Handler $ + ExceptT $ + flip runLoggingT logger $ do + -- This is not guaranteed to be consecutive with the logs from the action in the case of concurrent actions + -- (unlikely in a dev environment, except perhaps a getProgram&getActions request) + logInfo RequestStart + catch (Right <$> runPrimerM m (Env ss q v)) handler -- Catch exceptions from the API and convert them to Servant -- errors via 'Either'. diff --git a/primer-service/src/Servant/OpenApi/OperationId.hs b/primer-service/src/Servant/OpenApi/OperationId.hs index c10cd1a63..acec1e6a8 100644 --- a/primer-service/src/Servant/OpenApi/OperationId.hs +++ b/primer-service/src/Servant/OpenApi/OperationId.hs @@ -53,6 +53,4 @@ instance where toOpenApi _ = toOpenApi (Proxy @api) - & traversalVL allOperations - % #operationId - %~ (Just (pack (symbolVal (Proxy @id))) <>) + & traversalVL allOperations % #operationId %~ (Just (pack (symbolVal (Proxy @id))) <>) diff --git a/primer-service/test/Tests/OpenAPI.hs b/primer-service/test/Tests/OpenAPI.hs index 71c0efa00..0522e5b4d 100644 --- a/primer-service/test/Tests/OpenAPI.hs +++ b/primer-service/test/Tests/OpenAPI.hs @@ -109,9 +109,9 @@ test_golden :: TestTree test_golden = testGroup "golden" - [ goldenVsString "openapi.json" "test/outputs/OpenAPI/openapi.json" - $ pure - $ encodePretty openAPIInfo + [ goldenVsString "openapi.json" "test/outputs/OpenAPI/openapi.json" $ + pure $ + encodePretty openAPIInfo ] testToJSON :: (ToJSON a, ToSchema a, Show a) => Gen a -> Property @@ -197,8 +197,8 @@ genKindTree = viewTreeKind <$> genKind tasty_NodeBody :: Property tasty_NodeBody = - testToJSON - $ G.choice + testToJSON $ + G.choice [ TextBody <$> (RecordPair <$> G.enumBounded <*> API.genName) , PrimBody <$> (RecordPair <$> G.enumBounded <*> genPrimCon) , BoxBody <$> (RecordPair <$> G.enumBounded <*> genTree) @@ -317,8 +317,8 @@ genPaginatedMeta = do tp <- genPositive np <- G.maybe genPositive lp <- genPositive - pure - $ PM + pure $ + PM { totalItems = ti , pageSize = ps , firstPage = fp diff --git a/primer/gen/Primer/Gen/App.hs b/primer/gen/Primer/Gen/App.hs index b8e457a37..2bcff776d 100644 --- a/primer/gen/Primer/Gen/App.hs +++ b/primer/gen/Primer/Gen/App.hs @@ -67,8 +67,8 @@ genProg :: SmartHoles -> [Module] -> GenT WT Prog genProg sh initialImports = local (extendCxtByModules initialImports) $ do imports <- telescope (Range.linear 0 2) (local . extendCxtByModule) (genModule "I") home <- local (extendCxtByModules imports) $ telescope (Range.linear 1 2) (local . extendCxtByModule) (genModule "M") - pure - $ Prog + pure $ + Prog { progImports = initialImports <> imports , progModules = home , progSelection = Nothing @@ -98,8 +98,8 @@ genProg sh initialImports = local (extendCxtByModules initialImports) $ do tds' <- genTypeDefGroup $ Just mn tds <- traverse (\(n, d) -> (n,) <$> generateTypeDefIDs d) tds' defs <- local (extendTypeDefCxt $ M.fromList tds') (genASTDefGroup mn) - pure - $ Module + pure $ + Module { moduleName = mn , moduleTypes = M.fromList $ first baseName <$> tds , moduleDefs = defs diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs index 76cb6ed97..d555d5a24 100644 --- a/primer/gen/Primer/Gen/Core/Typed.hs +++ b/primer/gen/Primer/Gen/Core/Typed.hs @@ -233,8 +233,8 @@ genSyns ty = do globals <- asks globalCxt let globals' = map (first (Var () . GlobalVarRef)) $ M.toList globals let hs = locals' ++ globals' - pure - $ if null hs + pure $ + if null hs then Nothing else Just $ do (he, hT) <- Gen.element hs @@ -267,8 +267,7 @@ genSyns ty = do _ -> pure Nothing genPrimCon' = do consistentCons <- - filter (consistentTypes ty . snd) - . map (bimap (fmap $ PrimCon ()) (TCon ())) + filter (consistentTypes ty . snd) . map (bimap (fmap $ PrimCon ()) (TCon ())) <$> genPrimCon pure $ case consistentCons of [] -> Nothing @@ -396,24 +395,24 @@ genChk ty = do Left _ -> pure Nothing -- not an ADT Right (_, _, []) -> pure Nothing -- is an empty ADT Right (_, _, vcs) -> - pure - $ Just - $ Gen.choice - $ vcs - <&> \(vc, tmArgTypes) -> - Con () vc <$> traverse genChk tmArgTypes + pure $ + Just $ + Gen.choice $ + vcs + <&> \(vc, tmArgTypes) -> + Con () vc <$> traverse genChk tmArgTypes lambda = matchArrowType ty <&> \(sTy, tTy) -> do n <- genLVarNameAvoiding [tTy, sTy] Lam () n <$> local (extendLocalCxt (n, sTy)) (genChk tTy) abst = do mfa <- matchForallType ty - pure - $ mfa - <&> \(n, k, t) -> do - m <- genTyVarNameAvoiding ty - ty' <- substTy n (TVar () m) t - LAM () m <$> local (extendLocalCxtTy (m, k)) (genChk ty') + pure $ + mfa + <&> \(n, k, t) -> do + m <- genTyVarNameAvoiding ty + ty' <- substTy n (TVar () m) t + LAM () m <$> local (extendLocalCxtTy (m, k)) (genChk ty') genLet = Gen.choice [ -- let @@ -472,8 +471,8 @@ genChk ty = do casePrim :: WT (Maybe (GenT WT ExprG)) casePrim = do primGens <- genPrimCon - pure - $ if null primGens + pure $ + if null primGens then Nothing else Just $ do (pg, scrutTy0) <- Gen.element primGens @@ -490,8 +489,8 @@ genChk ty = do genStrictSubsequence :: MonadGen m => NonEmpty a -> m [a] genStrictSubsequence xs = Gen.justT $ do s <- Gen.subsequence $ toList xs - pure - $ if length s == length xs + pure $ + if length s == length xs then Nothing else Just s @@ -514,16 +513,16 @@ genWTType k = do vari :: WT (Maybe (GenT WT TypeG)) vari = do goodVars <- filter (consistentKinds k . snd) . M.toList <$> asks localTyVars - pure - $ if null goodVars + pure $ + if null goodVars then Nothing else Just $ Gen.element $ map (TVar () . fst) goodVars constr :: WT (Maybe (GenT WT TypeG)) constr = do tds <- asks $ M.assocs . typeDefs let goodTCons = filter (consistentKinds k . typeDefKind . snd) tds - pure - $ if null goodTCons + pure $ + if null goodTCons then Nothing else Just $ Gen.element $ map (TCon () . fst) goodTCons arrow :: Maybe (GenT WT TypeG) @@ -557,11 +556,11 @@ genWTKind = Gen.recursive Gen.choice [pure $ KType ()] [KFun () <$> genWTKind <* -- need definitions for the symbols! genGlobalCxtExtension :: GenT WT [(GVarName, TypeG)] genGlobalCxtExtension = - local forgetLocals - $ Gen.list (Range.linear 1 5) - $ (,) - <$> (qualifyName <$> genModuleName <*> genName) - <*> genWTType (KType ()) + local forgetLocals $ + Gen.list (Range.linear 1 5) $ + (,) + <$> (qualifyName <$> genModuleName <*> genName) + <*> genWTType (KType ()) -- We are careful to not let generated globals depend on whatever -- locals may be in the cxt diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 4d4875ef3..06e614a99 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -300,9 +300,8 @@ applyActionsToParam sh (paramName, def) actions = runExceptT $ do Nothing -> throwError $ ParamNotFound paramName Just (_, k) -> -- no action in kinds should care about the context - flip runReaderT (initialCxt sh) - $ withWrappedKind k - $ \zk' -> + flip runReaderT (initialCxt sh) $ + withWrappedKind k $ \zk' -> foldlM (flip applyActionAndSynth) (InKind zk') actions let def' = set @@ -343,22 +342,21 @@ applyActionsToField smartHoles imports (mod, mods) (tyName, conName', index, tyD (tz, cs) <- getCompose . flip (findAndAdjustA ((== conName') . valConName)) (astTypeDefConstructors tyDef) - $ Compose - . \(ValCon _ ts) -> do + $ Compose . \(ValCon _ ts) -> do (tz', cs') <- getCompose . flip (adjustAtA index) ts $ Compose - . fmap (First . Just &&& target . top) - . flip withWrappedType \tz'' -> - foldlM (\l a -> local addParamsToCxt $ applyActionAndSynth a l) (InType tz'') actions + . fmap (First . Just &&& target . top) + . flip withWrappedType \tz'' -> + foldlM (\l a -> local addParamsToCxt $ applyActionAndSynth a l) (InType tz'') actions maybe (throwError $ InternalFailure "applyActionsToField: con field index out of bounds") (pure . first (First . Just)) $ bisequence (getFirst tz', ValCon conName' <$> cs') (valCons, zt) <- - maybe (throwError $ InternalFailure "applyActionsToField: con name not found") pure - $ bisequence (cs, getFirst tz) + maybe (throwError $ InternalFailure "applyActionsToField: con name not found") pure $ + bisequence (cs, getFirst tz) let mod' = mod{moduleTypes = insert tyName (TypeDefAST tyDef{astTypeDefConstructors = valCons}) $ moduleTypes mod} (,zt) <$> checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods}) addParamsToCxt :: TC.Cxt -> TC.Cxt @@ -676,9 +674,9 @@ getVarType ast x = in \cxt -> cxt { TC.localCxt = - Map.fromList - $ map (bimap unLocalName TC.T) tmcxt - <> map (bimap unLocalName TC.K) tycxt + Map.fromList $ + map (bimap unLocalName TC.T) tmcxt + <> map (bimap unLocalName TC.K) tycxt } mkSaturatedApplicationArgs :: MonadFresh ID m => TC.Type -> [Either (m Expr) (m Type)] diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index 16440196f..919d4ab45 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -371,14 +371,14 @@ forTypeDef :: [Action] forTypeDef _ NonEditable _ _ _ _ = mempty forTypeDef l Editable tydefs defs tdName td = - sortByPriority l - $ [ Input RenameType - , Input AddCon - , NoInput DeleteTypeDef - ] - <> mwhen - (l == Expert && not (typeInUse tdName td tydefs defs)) - [Input AddTypeParam] + sortByPriority l $ + [ Input RenameType + , Input AddCon + , NoInput DeleteTypeDef + ] + <> mwhen + (l == Expert && not (typeInUse tdName td tydefs defs)) + [Input AddTypeParam] forTypeDefParamNode :: TyVarName -> @@ -391,21 +391,20 @@ forTypeDefParamNode :: [Action] forTypeDefParamNode _ _ NonEditable _ _ _ _ = mempty forTypeDefParamNode paramName l Editable tydefs defs tdName td = - sortByPriority l - $ [ Input RenameTypeParam - ] - <> mwhen - ( l - == Expert - && not - ( typeInUse tdName td tydefs defs - || elemOf - (to astTypeDefConstructors % folded % to valConArgs % folded % getting _freeVarsTy % _2) - paramName - td - ) - ) - [NoInput DeleteTypeParam] + sortByPriority l $ + [ Input RenameTypeParam + ] + <> mwhen + ( l == Expert + && not + ( typeInUse tdName td tydefs defs + || elemOf + (to astTypeDefConstructors % folded % to valConArgs % folded % getting _freeVarsTy % _2) + paramName + td + ) + ) + [NoInput DeleteTypeParam] forTypeDefParamKindNode :: TyVarName -> @@ -458,12 +457,12 @@ forTypeDefConsFieldNode :: [Action] forTypeDefConsFieldNode _ _ _ _ NonEditable _ _ _ _ = mempty forTypeDefConsFieldNode con index id l Editable _ _ _ td = - sortByPriority l - $ mwhen ((view _id <$> fieldType) == Just id) [NoInput DeleteConField] - <> case findTypeOrKind id =<< fieldType of - Nothing -> mempty - Just (Left t) -> forType l t - Just (Right k) -> forKind l k + sortByPriority l $ + mwhen ((view _id <$> fieldType) == Just id) [NoInput DeleteConField] + <> case findTypeOrKind id =<< fieldType of + Nothing -> mempty + Just (Left t) -> forType l t + Just (Right k) -> forKind l k where fieldType = getTypeDefConFieldType td con index @@ -626,22 +625,21 @@ options typeDefs defs cxt level def0 sel0 = \case findNode >>= \case ExprNode e | Just t <- exprType e -> do - pure - $ (locals <&> \(ln, t') -> (localOpt' (t `eqType` t') $ unLocalName ln, t')) - <> (globals <&> \(gn, t') -> (globalOpt' (t `eqType` t') gn, t')) + pure $ + (locals <&> \(ln, t') -> (localOpt' (t `eqType` t') $ unLocalName ln, t')) + <> (globals <&> \(gn, t') -> (globalOpt' (t `eqType` t') gn, t')) _ -> - pure - $ (first (localOpt . unLocalName) <$> locals) - <> (first globalOpt <$> globals) + pure $ + (first (localOpt . unLocalName) <$> locals) + <> (first globalOpt <$> globals) valConOpts = let vcs = allNonPrimValCons typeDefs in do findNode >>= \case ExprNode e | Just t <- exprType e -> do - pure - $ vcs - <&> \vc@(vc', tc, _) -> + pure $ + vcs <&> \vc@(vc', tc, _) -> -- Since all datatypes are regular ADTs (not GADTs), the only things needed for -- a value constructor to be a correct fit for a hole are -- - the hole's type is "a type constructor applied to a bunch of things" @@ -718,9 +716,8 @@ sortByPriority :: [Action] -> [Action] sortByPriority l = - sortOn - $ ($ l) - . \case + sortOn $ + ($ l) . \case NoInput a -> case a of MakeCase -> P.makeCase MakeApp -> P.applyFunction diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index c329d31c6..55fd5b12d 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -407,8 +407,8 @@ newEmptyProgImporting imported = ] , progImports = imported' , progSelection = - Just - $ SelectionDef + Just $ + SelectionDef DefSelection { def = qualifyName moduleName defName , node = Nothing @@ -462,17 +462,17 @@ importModules ms = do let currentModules = progAllModules p let currentNames = moduleName <$> currentModules let newNames = moduleName <$> ms - unless (disjoint currentNames newNames && not (anySame newNames)) - $ throwError - $ ActionError - $ ImportNameClash - $ (currentNames `intersect` newNames) - <> (newNames \\ ordNub newNames) + unless (disjoint currentNames newNames && not (anySame newNames)) $ + throwError $ + ActionError $ + ImportNameClash $ + (currentNames `intersect` newNames) + <> (newNames \\ ordNub newNames) -- Imports must be well-typed (and cannot depend on the editable modules) checkedImports <- - liftError (ActionError . ImportFailed ()) - $ checkEverything NoSmartHoles - $ CheckEverything{trusted = progImports p, toCheck = ms} + liftError (ActionError . ImportFailed ()) $ + checkEverything NoSmartHoles $ + CheckEverything{trusted = progImports p, toCheck = ms} let p' = p & #progImports %~ (<> checkedImports) modify (\a -> a & #currentState % #prog .~ p') @@ -782,8 +782,8 @@ applyProgAction prog = \case else do let m' = m{moduleDefs = Map.insert newNameBase (DefAST def) $ Map.delete defName defs} renamedModules <- - maybe (throwError $ ActionError NameCapture) pure - $ traverseOf + maybe (throwError $ ActionError NameCapture) pure $ + traverseOf (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr) (renameVar (GlobalVarRef d) (GlobalVarRef newName)) (m' : ms) @@ -921,10 +921,10 @@ applyProgAction prog = \case ) type_ updateDefs = - over (traversed % #_DefAST % #astDefExpr) - $ transform - $ over (#_Con % _2) updateName - . over (#_Case % _3 % traversed % #_CaseBranch % _1 % #_PatCon) updateName + over (traversed % #_DefAST % #astDefExpr) $ + transform $ + over (#_Con % _2) updateName + . over (#_Case % _3 % traversed % #_CaseBranch % _1 % #_PatCon) updateName updateName n = if n == old then new else n RenameTypeParam type_ old (unsafeMkLocalName -> new) -> editModule (qualifiedModule type_) prog $ \m -> do @@ -954,8 +954,7 @@ applyProgAction prog = \case % #valConArgs % traversed ) - $ maybe (throwError $ ActionError NameCapture) pure - . renameTyVar old new + $ maybe (throwError $ ActionError NameCapture) pure . renameTyVar old new AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) -> editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do when (con `elem` allValConNames prog) $ throwError $ ConAlreadyExists con @@ -966,8 +965,7 @@ applyProgAction prog = \case traverseOf (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr) (updateDefs allCons) - $ m' - : ms + $ m' : ms pure ( ms' , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing @@ -1042,17 +1040,17 @@ applyProgAction prog = \case (liftError (ActionError . TypeError) $ fmap TC.typeTtoType $ TC.checkKind (KType ()) =<< generateTypeIDs new) (progCxt prog) in alterTypeDef - ( traverseOf #astTypeDefConstructors - $ maybe (throwError $ ConNotFound con) pure - <=< findAndAdjustA - ((== con) . valConName) - ( traverseOf - #valConArgs - ( maybe (throwError $ IndexOutOfRange index) pure - <=< liftA2 (insertAt index) new' - . pure - ) - ) + ( traverseOf #astTypeDefConstructors $ + maybe (throwError $ ConNotFound con) pure + <=< findAndAdjustA + ((== con) . valConName) + ( traverseOf + #valConArgs + ( maybe (throwError $ IndexOutOfRange index) pure + <=< liftA2 (insertAt index) new' + . pure + ) + ) ) type_ -- NB: we must updateDecons first, as transformCaseBranches may do @@ -1206,13 +1204,13 @@ applyProgAction prog = \case Right (mod', zt) -> pure ( mod' - , Just - $ SelectionTypeDef + , Just $ + SelectionTypeDef TypeDefSelection { def = tyName , node = - Just - $ TypeDefConsNodeSelection + Just $ + TypeDefConsNodeSelection TypeDefConsSelection { con , field = @@ -1235,12 +1233,12 @@ applyProgAction prog = \case mods' <- runFullTCPass smartHoles imports (mod' : mods) pure ( mods' - , Just - $ SelectionTypeDef - $ TypeDefSelection tyName - $ Just - $ TypeDefParamNodeSelection - $ TypeDefParamSelection{param = paramName, kindMeta = Just $ Right $ Right $ kz ^. _target % _kindMetaLens} + , Just $ + SelectionTypeDef $ + TypeDefSelection tyName $ + Just $ + TypeDefParamNodeSelection $ + TypeDefParamSelection{param = paramName, kindMeta = Just $ Right $ Right $ kz ^. _target % _kindMetaLens} ) SetSmartHoles smartHoles -> pure $ prog & #progSmartHoles .~ smartHoles @@ -1263,21 +1261,17 @@ applyProgAction prog = \case Just renamedMods -> if imported curMods == imported renamedMods then - pure - $ prog - & #progModules - .~ editable renamedMods - & #progSelection - % _Just - %~ renameModule' oldName n + pure $ + prog + & #progModules .~ editable renamedMods + & #progSelection % _Just %~ renameModule' oldName n else - throwError - $ + throwError $ -- It should never happen that the action edits an -- imported module, since the oldName should be distinct -- from the name of any import - ActionError - $ InternalFailure "RenameModule: imported modules were edited by renaming" + ActionError $ + InternalFailure "RenameModule: imported modules were edited by renaming" where checkTypeNotInUse tdName td ms = when @@ -1323,8 +1317,8 @@ editModule :: editModule n p f = do m <- lookupEditableModule n p (m', s) <- f m - pure - $ p + pure $ + p { progModules = m' : filter ((/= n) . moduleName) (progModules p) , progSelection = s } @@ -1340,8 +1334,8 @@ editModuleCross n p f = do m <- lookupEditableModule n p let otherModules = filter ((/= n) . moduleName) (progModules p) (m', s) <- f (m, otherModules) - pure - $ p + pure $ + p { progModules = m' , progSelection = s } @@ -1737,9 +1731,9 @@ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do let sharedScope = if fromDefName == toDefName then -- We rely here on the fact that there are no binders in kinds - getSharedScopeTy (either identity (bimap unfocusKind unfocusKindT) c) - $ Right - $ either identity unfocusKindT tgt + getSharedScopeTy (either identity (bimap unfocusKind unfocusKindT) c) $ + Right $ + either identity unfocusKindT tgt else mempty -- Delete unbound vars (nb: no vars in kinds) let cTgt = bimap (either target target) (either target target) c @@ -1759,8 +1753,8 @@ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do let newSel = NodeSelection SigNode - ( Right - $ bimap + ( Right $ + bimap (view $ _target % _typeMetaLens) (view $ _target % _kindMetaLens) pasted @@ -1848,13 +1842,12 @@ tcWholeProg p = do (SigNode, Right (Right (Left x))) -> pure $ Just $ NodeSelection SigNode $ Right $ Left $ x ^. _target % _typeMetaLens (SigNode, Right (Right (Right zk))) -> pure $ Just $ NodeSelection SigNode $ Right $ Right $ zk ^. _target % _kindMetaLens _ -> pure Nothing -- something's gone wrong: expected a SigNode, but found it in the body, or vv, or just not found it - pure - $ Just - . SelectionDef - $ DefSelection - { def = defName_ - , node = updatedNode - } + pure $ + Just . SelectionDef $ + DefSelection + { def = defName_ + , node = updatedNode + } Just (SelectionTypeDef s) -> do let defName_ = s.def -- If something goes wrong in finding the metadata, we just don't set a field selection. @@ -1863,40 +1856,39 @@ tcWholeProg p = do Nothing -> Nothing Just (sn, tda) -> case sn of TypeDefParamNodeSelection paramSel -> - Just - $ TypeDefParamNodeSelection - $ paramSel - & #kindMeta - %~ \case - Just (Right (Right m)) -> do - k <- - tda - ^? #astTypeDefParameters - % afolding - (find ((== paramSel.param) . fst)) - % _2 - Right . Right . view _kindMetaLens . target <$> focusOnKind (getID m) k - _ -> Nothing + Just $ + TypeDefParamNodeSelection $ + paramSel + & #kindMeta %~ \case + Just (Right (Right m)) -> do + k <- + tda + ^? #astTypeDefParameters + % afolding + (find ((== paramSel.param) . fst)) + % _2 + Right . Right . view _kindMetaLens . target <$> focusOnKind (getID m) k + _ -> Nothing TypeDefConsNodeSelection conSel -> - Just - $ TypeDefConsNodeSelection - $ conSel - & over #field \case - Nothing -> Nothing - Just fieldSel -> - flip (set #meta) fieldSel . Right <$> do - ty <- getTypeDefConFieldType tda conSel.con fieldSel.index - id <- case fieldSel.meta of - Left _ -> Nothing -- Any selection in a typedef should have TypeMeta or KindMeta, not ExprMeta - Right m -> pure $ getID m - bimap (view $ _target % _typeMetaLens) (view $ _target % _kindMetaLens) <$> focusOnTy id ty - pure - $ Just - $ SelectionTypeDef - $ TypeDefSelection - { def = defName_ - , node = updatedNode - } + Just $ + TypeDefConsNodeSelection $ + conSel + & over #field \case + Nothing -> Nothing + Just fieldSel -> + flip (set #meta) fieldSel . Right <$> do + ty <- getTypeDefConFieldType tda conSel.con fieldSel.index + id <- case fieldSel.meta of + Left _ -> Nothing -- Any selection in a typedef should have TypeMeta or KindMeta, not ExprMeta + Right m -> pure $ getID m + bimap (view $ _target % _typeMetaLens) (view $ _target % _kindMetaLens) <$> focusOnTy id ty + pure $ + Just $ + SelectionTypeDef $ + TypeDefSelection + { def = defName_ + , node = updatedNode + } pure $ p'{progSelection = newSel} -- | Do a full check of a 'Prog', both the imports and the local modules @@ -2135,8 +2127,8 @@ transformNamedCaseBranch :: Expr -> m Expr transformNamedCaseBranch type_ con f = transformNamedCaseBranches type_ $ \m -> - traverse - $ \cb -> if caseBranchName cb == PatCon con then f m cb else pure cb + traverse $ + \cb -> if caseBranchName cb == PatCon con then f m cb else pure cb progCxt :: Prog -> Cxt progCxt p = buildTypingContextFromModules (progAllModules p) (progSmartHoles p) diff --git a/primer/src/Primer/Core/Utils.hs b/primer/src/Primer/Core/Utils.hs index c3387e310..d7b21e534 100644 --- a/primer/src/Primer/Core/Utils.hs +++ b/primer/src/Primer/Core/Utils.hs @@ -236,10 +236,8 @@ alphaEq = go (0, mempty, mempty) ( zipWith ( \(CaseBranch c1 (fmap bindName -> vs1) t1) (CaseBranch c2 (fmap bindName -> vs2) t2) -> - c1 - == c2 - && length vs1 - == length vs2 + c1 == c2 + && length vs1 == length vs2 && go (foldl' (uncurry . newTm) bs $ zip vs1 vs2) t1 t2 ) brs1 diff --git a/primer/src/Primer/Database.hs b/primer/src/Primer/Database.hs index bb1df96e5..8a94844d2 100644 --- a/primer/src/Primer/Database.hs +++ b/primer/src/Primer/Database.hs @@ -413,15 +413,15 @@ instance Exception NullDbException instance (MonadThrow m, MonadIO m) => MonadDb (NullDbT m) where insertSession _ id_ a n t = do ss <- ask - result <- liftIO - $ atomically - $ do - lookup <- StmMap.lookup id_ ss - case lookup of - Nothing -> do - StmMap.insert (SessionData a n t) id_ ss - pure $ Right () - Just _ -> pure $ Left $ NullDbException "insertSession failed because session already exists" + result <- liftIO $ + atomically $ + do + lookup <- StmMap.lookup id_ ss + case lookup of + Nothing -> do + StmMap.insert (SessionData a n t) id_ ss + pure $ Right () + Just _ -> pure $ Left $ NullDbException "insertSession failed because session already exists" case result of Left e -> throwM e Right _ -> pure () @@ -463,15 +463,15 @@ instance (MonadThrow m, MonadIO m) => MonadDb (NullDbT m) where updateOrFail :: (MonadThrow m, MonadIO m) => SessionId -> (SessionData -> SessionData) -> Sessions -> m () updateOrFail id_ f ss = do - result <- liftIO - $ atomically - $ do - lookup <- StmMap.lookup id_ ss - case lookup of - Nothing -> pure $ Left $ NullDbException "updateSessionName lookup failed" - Just s -> do - StmMap.insert (f s) id_ ss - pure $ Right () + result <- liftIO $ + atomically $ + do + lookup <- StmMap.lookup id_ ss + case lookup of + Nothing -> pure $ Left $ NullDbException "updateSessionName lookup failed" + Just s -> do + StmMap.insert (f s) id_ ss + pure $ Right () case result of Left e -> throwM e Right _ -> pure () diff --git a/primer/src/Primer/Eval.hs b/primer/src/Primer/Eval.hs index 4b0c3d686..e6d4ec89e 100644 --- a/primer/src/Primer/Eval.hs +++ b/primer/src/Primer/Eval.hs @@ -100,8 +100,8 @@ step :: Dir -> ID -> m (Either EvalError (Expr, EvalDetail)) -step as tydefs globals expr d i = runExceptT - $ case findNodeByID i d expr of +step as tydefs globals expr d i = runExceptT $ + case findNodeByID i d expr of Just (cxt, Left (d', z)) -> do (node', detail) <- tryReduceExpr as tydefs globals cxt d' (target z) let expr' = unfocusExpr $ replace node' z diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs index dd5c34839..7db17bbff 100644 --- a/primer/src/Primer/Eval/NormalOrder.hs +++ b/primer/src/Primer/Eval/NormalOrder.hs @@ -135,10 +135,10 @@ foldMapExpr opts extract topDir = go mempty . (topDir,) . focus -- Prefer to compute inside the body of a let, but otherwise compute in the binding -- NB: we never push lets into lets, so the Cxt is reset for non-body children Just (ViewLet{bindingVL, bodyVL, typeChildrenVL, termChildrenVL}) -> - msum - $ go (cxtAddLet bindingVL lets) bodyVL - : map (goType mempty) typeChildrenVL - <> map (go mempty) termChildrenVL + msum $ + go (cxtAddLet bindingVL lets) bodyVL + : map (goType mempty) typeChildrenVL + <> map (go mempty) termChildrenVL -- Since stuck things other than lets are stuck on the first child or -- its type annotation, we can handle them all uniformly -- Since this node is not a let, the context is reset @@ -146,9 +146,9 @@ foldMapExpr opts extract topDir = go mempty . (topDir,) . focus case (opts, lets) of (StopAtBinders, Cxt (_ : _)) -> mzero _ -> - msum - $ (goType mempty =<< focusType' ez) -- NB: no binders in term scope over a type child - : map (go mempty) (exprChildren opts dez) + msum $ + (goType mempty =<< focusType' ez) -- NB: no binders in term scope over a type child + : map (go mempty) (exprChildren opts dez) goType :: Cxt -> TypeZ -> f a goType lets tz = extract.ty tz lets diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs index feafc5173..cf6f86690 100644 --- a/primer/src/Primer/Eval/Redex.hs +++ b/primer/src/Primer/Eval/Redex.hs @@ -581,10 +581,10 @@ viewCaseRedex opts tydefs = \case Nothing -> mzero Just tyargsFromAnn -> do tyargs <- do - unless (length params == length tyargsFromAnn) - $ logWarning - $ CaseRedexNotSaturated - $ forgetTypeMetadata annotation + unless (length params == length tyargsFromAnn) $ + logWarning $ + CaseRedexNotSaturated $ + forgetTypeMetadata annotation pure $ zip params tyargsFromAnn (patterns, br) <- extractBranch (PatCon c) brs fb renameBindings mCase scrut brs fb patterns orig @@ -640,8 +640,8 @@ viewCaseRedex opts tydefs = \case renameBindings meta scrutinee branches fallbackBranch patterns orig = let avoid = freeVars scrutinee <> mwhen opts.avoidShadowing (bindersBelow $ focus scrutinee) binders = maybe mempty (S.fromList . map (unLocalName . bindName)) patterns - in hoistMaybe - $ if S.disjoint avoid binders + in hoistMaybe $ + if S.disjoint avoid binders then Nothing else Just $ RenameBindingsCase{meta, scrutinee, branches, fallbackBranch, avoid, orig} formCaseRedex :: @@ -683,12 +683,12 @@ viewRedex :: viewRedex opts tydefs globals dir = \case orig@(Var _ (GlobalVarRef gvar)) | Just (DefAST def) <- gvar `M.lookup` globals -> - pure - $ InlineGlobal{gvar, def, orig} + pure $ + InlineGlobal{gvar, def, orig} Let mLet var rhs (Var mVar (LocalVarRef var')) | var == var' -> - pure - $ InlineLet + pure $ + InlineLet { var , expr = rhs , letID = getID mLet @@ -696,8 +696,8 @@ viewRedex opts tydefs globals dir = \case } Letrec mLet var rhs ty (Var mVar (LocalVarRef var')) | var == var' -> - pure - $ InlineLetrec + pure $ + InlineLetrec { var , expr = rhs , ty @@ -712,8 +712,8 @@ viewRedex opts tydefs globals dir = \case , not opts.aggressiveElision || n `S.member` freeVars expr' , S.disjoint (getBoundHereDn expr') (setOf (_2 % (_freeVarsLetBinding `summing` to letBindingName)) letBinding1) , not opts.avoidShadowing || S.disjoint (getBoundHereDn expr') (boundVarsLetBinding . snd $ letBinding1) -> - pure - $ PushLet + pure $ + PushLet { bindings = pure $ first getID letBinding1 , expr = expr' , orig @@ -724,8 +724,8 @@ viewRedex opts tydefs globals dir = \case , not opts.aggressiveElision || null unused , S.disjoint (getBoundHereDn body) (setOf (folded % _2 % (_freeVarsLetBinding `summing` to letBindingName)) $ letBinding1 : letBindings) , not opts.avoidShadowing || S.disjoint (getBoundHereDn body) (foldMap' (boundVarsLetBinding . snd) $ letBinding1 : letBindings) -> - pure - $ PushLet + pure $ + PushLet { bindings = first getID <$> letBinding1 :| letBindings , expr = body , orig @@ -736,8 +736,8 @@ viewRedex opts tydefs globals dir = \case | not opts.groupedLets , letBindingName (snd letBinding1) `S.notMember` freeVars expr' , opts.aggressiveElision || isLeaf expr' -> - pure - $ ElideLet + pure $ + ElideLet { letBindingsDrop = pure $ first getID letBinding1 , letBindingsKeep = mempty , body = expr' @@ -746,8 +746,8 @@ viewRedex opts tydefs globals dir = \case | opts.groupedLets , (letBindingsKeep, nonEmpty -> Just letBindingsDrop) <- partitionLets (letBinding1 : letBindings) body , opts.aggressiveElision || isLeaf body -> - pure - $ ElideLet + pure $ + ElideLet { letBindingsDrop = first getID <$> letBindingsDrop , letBindingsKeep , body @@ -764,8 +764,8 @@ viewRedex opts tydefs globals dir = \case then pure $ RenameBindingsLAM{tyvar = v, meta, body, avoid, orig = l} else mzero orig@(App _ (Ann _ (Lam m var body) (TFun _ srcTy tgtTy)) app) -> - pure - $ Beta + pure $ + Beta { var , body , srcTy @@ -775,15 +775,14 @@ viewRedex opts tydefs globals dir = \case , lamID = getID m } e@App{} -> - lift - $ hoistMaybe - $ tryPrimFun (M.mapMaybe defPrim globals) e - >>= \(primFun, args, result) -> - pure ApplyPrimFun{result, primFun, args, orig = e} + lift $ + hoistMaybe $ + tryPrimFun (M.mapMaybe defPrim globals) e >>= \(primFun, args, result) -> + pure ApplyPrimFun{result, primFun, args, orig = e} -- (Λa.t : ∀b.T) S ~> (letType a = S in t) : (letType b = S in T) orig@(APP _ (Ann _ (LAM m a body) (TForall _ forallVar forallKind tgtTy)) argTy) -> - pure - $ BETA + pure $ + BETA { tyvar = a , body , forallVar @@ -871,8 +870,8 @@ viewRedexType :: ViewRedexOptions -> Type -> Reader Cxt (Maybe RedexType) viewRedexType opts = \case TLet mLet v s (TVar mVar var) | v == var -> - purer - $ InlineLetInType + purer $ + InlineLetInType { var , ty = s , letID = getID mLet @@ -885,8 +884,8 @@ viewRedexType opts = \case , not opts.aggressiveElision || letTypeBindingName' (snd letBinding1) `S.member` freeVarsTy ty' , S.disjoint (getBoundHereDnTy ty') (setOf (_2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) letBinding1) , not opts.avoidShadowing || S.disjoint (getBoundHereDnTy ty') (boundVarsLetBindingTy . snd $ letBinding1) -> - purer - $ PushLetType + purer $ + PushLetType { bindings = pure $ first getID letBinding1 , intoTy = ty' , origTy = orig @@ -897,8 +896,8 @@ viewRedexType opts = \case , not opts.aggressiveElision || null unused , S.disjoint (getBoundHereDnTy body) (setOf (folded % _2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) (letBinding1 : letBindings)) , not opts.avoidShadowing || S.disjoint (getBoundHereDnTy body) (foldMap' (boundVarsLetBindingTy . snd) $ letBinding1 : letBindings) -> - purer - $ PushLetType + purer $ + PushLetType { bindings = first getID <$> letBinding1 :| letBindings , intoTy = body , origTy = orig @@ -906,8 +905,8 @@ viewRedexType opts = \case | not opts.groupedLets , letTypeBindingName' (snd letBinding1) `S.notMember` freeVarsTy ty' , opts.aggressiveElision || isLeaf ty' -> - purer - $ ElideLetInType + purer $ + ElideLetInType { letBindingsDrop = pure $ first getID letBinding1 , letBindingsKeep = mempty , body = ty' @@ -916,8 +915,8 @@ viewRedexType opts = \case | opts.groupedLets , (letBindingsKeep, nonEmpty -> Just letBindingsDrop) <- partitionLetsTy (letBinding1 : letBindings) body , opts.aggressiveElision || isLeaf body -> - purer - $ ElideLetInType + purer $ + ElideLetInType { letBindingsDrop = first getID <$> letBindingsDrop , letBindingsKeep , body @@ -925,11 +924,10 @@ viewRedexType opts = \case } orig@(TForall meta origBinder kind body) -> do avoid <- liftA2 (<>) cxtToAvoidTy $ when' opts.avoidShadowing cxtToAvoidTyShadow - pure - $ if origBinder `S.member` avoid + pure $ + if origBinder `S.member` avoid then - pure - $ + pure $ -- If anything we may substitute would cause capture, we should rename this binder RenameForall { meta @@ -1088,9 +1086,9 @@ runRedex opts = \case , conID } -> do let binderNames = maybe mempty (map bindName) binders - unless (isNothing binders || (length args == length argTys && length args == length binderNames)) - $ logWarning - $ CaseRedexWrongArgNum con args argTys binderNames + unless (isNothing binders || (length args == length argTys && length args == length binderNames)) $ + logWarning $ + CaseRedexWrongArgNum con args argTys binderNames let freshLocalNameLike n avoid = if S.member n avoid then freshLocalName avoid @@ -1251,8 +1249,8 @@ filterLetsTy ls t = filterLets' (toList ls) (S.map unLocalName $ freeVarsTy t) filterLets' :: [LetBinding] -> Set Name -> [LetBinding] filterLets' ls fvs = - fst - $ foldr + fst $ + foldr ( \l (ls', fvs') -> let ln = letBindingName l in if ln `S.member` fvs' @@ -1266,8 +1264,8 @@ filterLets' ls fvs = -- note that some of the unused may be used in later unused, but not in later used or in the term partitionLets :: [(a, LetBinding)] -> Expr -> ([(a, LetBinding)], [(a, LetBinding)]) partitionLets ls e = - fst - $ foldr + fst $ + foldr ( \l ((used, unused), fvs') -> let ln = letBindingName $ snd l in if ln `S.member` fvs' @@ -1281,8 +1279,8 @@ partitionLets ls e = -- note that some of the unused may be used in later unused, but not in later used or in the term partitionLetsTy :: [(a, LetTypeBinding)] -> Type -> ([(a, LetTypeBinding)], [(a, LetTypeBinding)]) partitionLetsTy ls t = - fst - $ foldr + fst $ + foldr ( \l@(_, LetTypeBind n l') ((used, unused), fvs') -> if n `S.member` fvs' then ((l : used, unused), S.delete n fvs' `S.union` freeVarsTy l') diff --git a/primer/src/Primer/EvalFullInterp.hs b/primer/src/Primer/EvalFullInterp.hs index d88fcc97a..7cbc26d0b 100644 --- a/primer/src/Primer/EvalFullInterp.hs +++ b/primer/src/Primer/EvalFullInterp.hs @@ -267,9 +267,9 @@ interp' tydefs env@(envTm, envTy) dir = \case in interp' tydefs ( extendTmsEnv - ( zip (Right . bindName <$> xs) - $ zipWith (\a argTy -> Ann () a $ interpTy envTy' argTy) as - $ ctorArgTys tycon c + ( zip (Right . bindName <$> xs) $ + zipWith (\a argTy -> Ann () a $ interpTy envTy' argTy) as $ + ctorArgTys tycon c ) env ) diff --git a/primer/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs index b967f0917..1a29867be 100644 --- a/primer/src/Primer/Examples.hs +++ b/primer/src/Primer/Examples.hs @@ -151,17 +151,17 @@ map modName = in do type_ <- tforall "a" ktype $ tforall "b" ktype $ (tvar "a" `tfun` tvar "b") `tfun` ((tcon B.tList `tapp` tvar "a") `tfun` (tcon B.tList `tapp` tvar "b")) term <- - lAM "a" - $ lAM "b" - $ lam "f" - $ lam "xs" - $ case_ - (lvar "xs") - [ branch B.cNil [] - $ con B.cNil [] - , branch B.cCons [("y", Nothing), ("ys", Nothing)] - $ con B.cCons [lvar "f" `app` lvar "y", gvar this `aPP` tvar "a" `aPP` tvar "b" `app` lvar "f" `app` lvar "ys"] - ] + lAM "a" $ + lAM "b" $ + lam "f" $ + lam "xs" $ + case_ + (lvar "xs") + [ branch B.cNil [] $ + con B.cNil [] + , branch B.cCons [("y", Nothing), ("ys", Nothing)] $ + con B.cCons [lvar "f" `app` lvar "y", gvar this `aPP` tvar "a" `aPP` tvar "b" `app` lvar "f" `app` lvar "ys"] + ] pure (this, DefAST $ ASTDef term type_) -- | The polymorphic function @map@ (over @List a@ as defined by @@ -170,19 +170,19 @@ map' :: MonadFresh ID m => ModuleName -> m (GVarName, Def) map' modName = do type_ <- tforall "a" ktype $ tforall "b" ktype $ (tvar "a" `tfun` tvar "b") `tfun` ((tcon B.tList `tapp` tvar "a") `tfun` (tcon B.tList `tapp` tvar "b")) let worker = - lam "xs" - $ case_ + lam "xs" $ + case_ (lvar "xs") [ branch B.cNil [] $ con B.cNil [] - , branch B.cCons [("y", Nothing), ("ys", Nothing)] - $ con B.cCons [lvar "f" `app` lvar "y", lvar "go" `app` lvar "ys"] + , branch B.cCons [("y", Nothing), ("ys", Nothing)] $ + con B.cCons [lvar "f" `app` lvar "y", lvar "go" `app` lvar "ys"] ] term <- - lAM "a" - $ lAM "b" - $ lam "f" - $ letrec "go" worker ((tcon B.tList `tapp` tvar "a") `tfun` (tcon B.tList `tapp` tvar "b")) - $ lvar "go" + lAM "a" $ + lAM "b" $ + lam "f" $ + letrec "go" worker ((tcon B.tList `tapp` tvar "a") `tfun` (tcon B.tList `tapp` tvar "b")) $ + lvar "go" pure (qualifyName modName "map", DefAST $ ASTDef term type_) -- | The function @odd@, defined over the inductive natural number @@ -193,8 +193,8 @@ odd :: MonadFresh ID m => ModuleName -> m (GVarName, Def) odd modName = do type_ <- tcon B.tNat `tfun` tcon B.tBool term <- - lam "x" - $ case_ + lam "x" $ + case_ (lvar "x") [ branch B.cZero [] $ con0 B.cFalse , branch B.cSucc [("n", Nothing)] $ gvar (qualifyName modName "even") `app` lvar "n" @@ -209,8 +209,8 @@ even :: MonadFresh ID m => ModuleName -> m (GVarName, Def) even modName = do type_ <- tcon B.tNat `tfun` tcon B.tBool term <- - lam "x" - $ case_ + lam "x" $ + case_ (lvar "x") [ branch B.cZero [] $ con0 B.cTrue , branch B.cSucc [("n", Nothing)] $ gvar (qualifyName modName "odd") `app` lvar "n" @@ -311,8 +311,8 @@ comprehensive' typeable modName = do ] $ caseFB_ (lvar "n") - [ branch B.cZero [] - $ app + [ branch B.cZero [] $ + app ( app emptyHole (lvar "x") @@ -450,8 +450,8 @@ mapOddPrim len = oddDef <- do type_ <- tcon P.tInt `tfun` tcon B.tBool term <- - lam "x" - $ case_ + lam "x" $ + case_ (pfun P.IntRemainder `app` lvar "x" `app` int 2) [ branch B.cNothing [] $ con0 B.cTrue -- this should be impossible (since denominator is obviously non-zero) , branch B.cJust [("r", Nothing)] $ pfun P.IntEq `app` lvar "r" `app` int 1 diff --git a/primer/src/Primer/Module.hs b/primer/src/Primer/Module.hs index a8ff3cfcf..eb490f3fb 100644 --- a/primer/src/Primer/Module.hs +++ b/primer/src/Primer/Module.hs @@ -124,9 +124,9 @@ renameModule' fromName toName = transformBi (\n -> if n == fromName then toName -- change in the future. nextModuleID :: Module -> ID nextModuleID m = - getMax - $ foldMap' (Max . nextID) (moduleDefs m) - <> foldMap' (Max . nextIDTypeDef) (moduleTypes m) + getMax $ + foldMap' (Max . nextID) (moduleDefs m) + <> foldMap' (Max . nextIDTypeDef) (moduleTypes m) -- | This module depends on the builtin module, due to some terms referencing builtin types. -- It contains all primitive types and terms. @@ -149,8 +149,8 @@ builtinModule = do maybeDef' <- generateTypeDefIDs $ TypeDefAST maybeDef pairDef' <- generateTypeDefIDs $ TypeDefAST pairDef eitherDef' <- generateTypeDefIDs $ TypeDefAST eitherDef - pure - $ Module + pure $ + Module { moduleName = builtinModuleName , moduleTypes = M.fromList diff --git a/primer/src/Primer/Prelude/Integer.hs b/primer/src/Primer/Prelude/Integer.hs index 9929c717f..2b4aee9c7 100644 --- a/primer/src/Primer/Prelude/Integer.hs +++ b/primer/src/Primer/Prelude/Integer.hs @@ -195,8 +195,8 @@ lcmDef = do (apps (gvar gcd) [lvar "x", lvar "y"]) ( apps (pfun IntQuot) - [ app (gvar abs) - $ apps + [ app (gvar abs) $ + apps (pfun IntMul) [lvar "x", lvar "y"] , lvar "m" diff --git a/primer/src/Primer/Prelude/Polymorphism.hs b/primer/src/Primer/Prelude/Polymorphism.hs index a65909af6..164411a54 100644 --- a/primer/src/Primer/Prelude/Polymorphism.hs +++ b/primer/src/Primer/Prelude/Polymorphism.hs @@ -64,23 +64,23 @@ map = qualifyName modName "map" mapDef :: MonadFresh ID m => m Def mapDef = do type_ <- - tforall "a" ktype - $ tforall "b" ktype - $ (tvar "a" `tfun` tvar "b") - `tfun` (listOf (tvar "a") `tfun` listOf (tvar "b")) + tforall "a" ktype $ + tforall "b" ktype $ + (tvar "a" `tfun` tvar "b") + `tfun` (listOf (tvar "a") `tfun` listOf (tvar "b")) term <- - lAM "a" - $ lAM "b" - $ lam "f" - $ lam "xs" - $ case_ - (lvar "xs") - [ branch cNil [] (con cNil []) - , branch cCons [("y", Nothing), ("ys", Nothing)] - $ let fy = app (lvar "f") (lvar "y") - fys = apps' (gvar map) [Right $ tvar "a", Right $ tvar "b", Left $ lvar "f", Left $ lvar "ys"] - in con cCons [fy, fys] - ] + lAM "a" $ + lAM "b" $ + lam "f" $ + lam "xs" $ + case_ + (lvar "xs") + [ branch cNil [] (con cNil []) + , branch cCons [("y", Nothing), ("ys", Nothing)] $ + let fy = app (lvar "f") (lvar "y") + fys = apps' (gvar map) [Right $ tvar "a", Right $ tvar "b", Left $ lvar "f", Left $ lvar "ys"] + in con cCons [fy, fys] + ] pure $ DefAST $ ASTDef term type_ foldr :: GVarName @@ -89,24 +89,24 @@ foldr = qualifyName modName "foldr" foldrDef :: MonadFresh ID m => m Def foldrDef = do type_ <- - tforall "a" ktype - $ tforall "b" ktype - $ (tvar "a" `tfun` (tvar "b" `tfun` tvar "b")) - `tfun` (tvar "b" `tfun` (listOf (tvar "a") `tfun` tvar "b")) + tforall "a" ktype $ + tforall "b" ktype $ + (tvar "a" `tfun` (tvar "b" `tfun` tvar "b")) + `tfun` (tvar "b" `tfun` (listOf (tvar "a") `tfun` tvar "b")) term <- - lAM "a" - $ lAM "b" - $ lam "f" - $ lam "y" - $ lam "xs" - $ case_ - (lvar "xs") - [ branch cNil [] (lvar "y") - , branch - cCons - [("x'", Nothing), ("xs'", Nothing)] - ( let foldxs' = apps' (gvar foldr) [Right $ tvar "a", Right $ tvar "b", Left $ lvar "f", Left $ lvar "y", Left $ lvar "xs'"] - in apps (lvar "f") [lvar "x'", foldxs'] - ) - ] + lAM "a" $ + lAM "b" $ + lam "f" $ + lam "y" $ + lam "xs" $ + case_ + (lvar "xs") + [ branch cNil [] (lvar "y") + , branch + cCons + [("x'", Nothing), ("xs'", Nothing)] + ( let foldxs' = apps' (gvar foldr) [Right $ tvar "a", Right $ tvar "b", Left $ lvar "f", Left $ lvar "y", Left $ lvar "xs'"] + in apps (lvar "f") [lvar "x'", foldxs'] + ) + ] pure $ DefAST $ ASTDef term type_ diff --git a/primer/src/Primer/Pretty.hs b/primer/src/Primer/Pretty.hs index 82be3c693..6c8736706 100644 --- a/primer/src/Primer/Pretty.hs +++ b/primer/src/Primer/Pretty.hs @@ -158,26 +158,26 @@ prettyExpr opts = \case col Yellow "let" <+> lname v <+> col Yellow "=" - <> inlineblock opts (pE e) - <> col Yellow "in" - <> line - <> indent' 2 (pE e') + <> inlineblock opts (pE e) + <> col Yellow "in" + <> line + <> indent' 2 (pE e') LetType _ v t e -> col Yellow "let type" <+> lname v <+> col Yellow "=" - <> inlineblock opts (pT t) - <> col Yellow "in" - <> line - <> indent' 2 (pE e) + <> inlineblock opts (pT t) + <> col Yellow "in" + <> line + <> indent' 2 (pE e) Letrec _ v e t e' -> col Yellow "let rec" <+> lname v <+> col Yellow "=" - <> inlineblock opts (typeann e t) - <> col Yellow "in" - <> line - <> indent' 2 (pE e') + <> inlineblock opts (typeann e t) + <> col Yellow "in" + <> line + <> indent' 2 (pE e') PrimCon _ p -> prim p where pT = prettyType opts @@ -246,16 +246,19 @@ prettyType opts typ = case typ of TForall _ n _ t -> (if inlineLambda opts then group else identity) ( col Yellow "∀" - <+> lname n <> col Yellow "." <> line <> indent' 2 (pT t) + <+> lname n + <> col Yellow "." + <> line + <> indent' 2 (pT t) ) TLet _ v t b -> col Yellow "let" <+> lname v <+> col Yellow "=" - <> inlineblock opts (pT t) - <> col Yellow "in" - <> line - <> indent' 2 (pT b) + <> inlineblock opts (pT t) + <> col Yellow "in" + <> line + <> indent' 2 (pT b) where pT = prettyType opts diff --git a/primer/src/Primer/Primitives.hs b/primer/src/Primer/Primitives.hs index d3bc5670d..ee6643038 100644 --- a/primer/src/Primer/Primitives.hs +++ b/primer/src/Primer/Primitives.hs @@ -253,33 +253,33 @@ primFunDef def args = case def of _ -> err IntQuotient -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right - $ maybeAnn (tcon tInt) int - $ if y == 0 - then Nothing - else Just $ x `div` y + Right $ + maybeAnn (tcon tInt) int $ + if y == 0 + then Nothing + else Just $ x `div` y _ -> err IntRemainder -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right - $ maybeAnn (tcon tInt) int - $ if y == 0 - then Nothing - else Just $ x `mod` y + Right $ + maybeAnn (tcon tInt) int $ + if y == 0 + then Nothing + else Just $ x `mod` y _ -> err IntQuot -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right - $ int - $ if y == 0 then 0 else x `div` y + Right $ + int $ + if y == 0 then 0 else x `div` y _ -> err IntRem -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right - $ int - $ if y == 0 - then x - else x `mod` y + Right $ + int $ + if y == 0 + then x + else x `mod` y _ -> err IntLT -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> @@ -307,11 +307,11 @@ primFunDef def args = case def of _ -> err IntToNat -> case args of [PrimCon _ (PrimInt x)] -> - Right - $ maybeAnn (tcon tNat) nat - $ if x < 0 - then Nothing - else Just $ fromInteger x + Right $ + maybeAnn (tcon tNat) nat $ + if x < 0 + then Nothing + else Just $ fromInteger x _ -> err IntFromNat -> case args of [exprToNat -> Just n] -> diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 0b401328e..c9bafacdb 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -374,15 +374,14 @@ checkTypeDefs tds = do ( (1 ==) . S.size $ S.fromList - $ qualifiedModule tc - : fmap (qualifiedModule . valConName) cons + $ qualifiedModule tc : fmap (qualifiedModule . valConName) cons ) "Module name of type and all constructors must be the same" assert (distinct $ map (unLocalName . fst) params <> map (baseName . valConName) cons) "Duplicate names in one tydef: between parameter-names and constructor-names" - local (extendLocalCxtTys params) - $ traverseOf astTypeDefConArgs (checkKind' (KType ())) td + local (extendLocalCxtTys params) $ + traverseOf astTypeDefConArgs (checkKind' (KType ())) td astTypeDefConArgs :: Traversal (ASTTypeDef a c) (ASTTypeDef b c) (Type' a c) (Type' b c) astTypeDefConArgs = #astTypeDefConstructors % traversed % #valConArgs % traversed @@ -433,8 +432,7 @@ checkEverything sh CheckEverything{trusted, toCheck} = updatedSigs <- traverseOf (traverseDefs % #_DefAST % #astDefType) (fmap typeTtoType . checkKind' (KType ())) toCheck' -- Now extend the context with the new types let defsUpdatedSigs = itoListOf foldDefTypesWithName updatedSigs - local (extendGlobalCxt defsUpdatedSigs) - $ + local (extendGlobalCxt defsUpdatedSigs) $ -- Check the body (of AST definitions) against the new type traverseOf (traverseDefs % #_DefAST) @@ -459,10 +457,10 @@ checkEverything sh CheckEverything{trusted, toCheck} = traverseDefs = traverseDefs' equality foldDefTypesWithName :: IxFold GVarName [Module] Type foldDefTypesWithName = - icompose qualifyName - $ traverseDefs' (reindexed moduleName selfIndex) - % to defType - % to forgetTypeMetadata + icompose qualifyName $ + traverseDefs' (reindexed moduleName selfIndex) + % to defType + % to forgetTypeMetadata {- HLINT ignore synth "Avoid lambda using `infix`" -} -- Note [Let expressions] @@ -826,9 +824,8 @@ check t = \case -- We do want to remove (e.g.) {? λx.x : ? ?} to get λx.x, -- if that typechecks. (But only a simple hole annotation, as we do -- not wish to delete any interesting annotations.) - flip catchError (const default_) - $ check t e' - >>= \case + flip catchError (const default_) $ + check t e' >>= \case Hole{} -> default_ -- Don't let the recursive call mint a hole. e'' -> pure e'' (Hole _ (Ann _ _ ty), SmartHoles) @@ -841,9 +838,8 @@ check t = \case -- cannot typecheck, e.g. Bool ∋ λx.t returns {? λx.t : ? ?} default_ (Hole _ e', SmartHoles) -> - flip catchError (const default_) - $ check t e' - >>= \case + flip catchError (const default_) $ + check t e' >>= \case Hole{} -> default_ -- Don't let the recursive call mint a hole. e'' -> pure e'' _ -> default_ @@ -949,11 +945,11 @@ checkBranch t (vc, args) (CaseBranch nb patterns rhs) = bind <- Bind <$> meta' (TCChkedAt ty) <*> pure name pure (bind, ty) assertCorrectCon = - assert (PatCon vc == nb) - $ "checkBranch: expected a branch on " - <> show vc - <> " but found branch on " - <> show nb + assert (PatCon vc == nb) $ + "checkBranch: expected a branch on " + <> show vc + <> " but found branch on " + <> show nb -- | Checks if a type can be unified with a function (arrow) type. Returns the -- arrowised version - i.e. if it's a hole then it returns an arrow type with diff --git a/primer/src/Primer/Typecheck/Utils.hs b/primer/src/Primer/Typecheck/Utils.hs index d10cb082b..6508465e6 100644 --- a/primer/src/Primer/Typecheck/Utils.hs +++ b/primer/src/Primer/Typecheck/Utils.hs @@ -147,11 +147,11 @@ getGlobalNames = do let ctors = Map.foldMapWithKey ( \t def -> - S.fromList - $ (f t :) - $ map (f . valConName) - $ maybe [] astTypeDefConstructors - $ typeDefAST def + S.fromList $ + (f t :) $ + map (f . valConName) $ + maybe [] astTypeDefConstructors $ + typeDefAST def ) tyDefs pure $ S.union topLevel ctors diff --git a/primer/src/Primer/Unification.hs b/primer/src/Primer/Unification.hs index 8e86b4048..f3ab5856f 100644 --- a/primer/src/Primer/Unification.hs +++ b/primer/src/Primer/Unification.hs @@ -65,11 +65,11 @@ unify :: m (Maybe (M.Map TyVarName Type)) unify cxt unificationVars s t = do result <- - runExceptT - $ flip execStateT mempty - $ flip runReaderT initEnv - $ unU - $ unify' s t + runExceptT $ + flip execStateT mempty $ + flip runReaderT initEnv $ + unU $ + unify' s t case result of Left _err -> pure Nothing Right sb -> do diff --git a/primer/src/Primer/Zipper.hs b/primer/src/Primer/Zipper.hs index 2d685e614..250ef2501 100644 --- a/primer/src/Primer/Zipper.hs +++ b/primer/src/Primer/Zipper.hs @@ -293,8 +293,8 @@ focusType z = case target z of focusKind :: (Data b, Data c) => TypeZ' a b c -> Maybe (KindZ' a b c) focusKind (ZipNest z f) = case target z of TForall m n k t -> - pure - $ ZipNest + pure $ + ZipNest ( ZipNest (focus k) $ \k' -> replace (TForall m n k' t) z @@ -489,8 +489,8 @@ findNodeWithParent id x = do InExpr ez -> (ExprNode $ target ez, ExprNode . target <$> up ez) InType tz -> ( TypeNode $ target tz - , Just - $ maybe + , Just $ + maybe (ExprNode $ target $ unfocusType tz) (TypeNode . target) (up tz) diff --git a/primer/test/Tests/Action.hs b/primer/test/Tests/Action.hs index 521e1542b..622c0c2a2 100644 --- a/primer/test/Tests/Action.hs +++ b/primer/test/Tests/Action.hs @@ -82,8 +82,8 @@ tasty_ConstructVar_succeeds_on_hole_when_in_scope = property $ do let expr = create' $ ann (lam "x" emptyHole) (tfun tEmptyHole tEmptyHole) annotateShow expr expr' <- - either (\err -> footnoteShow err >> failure) pure - $ runTestActions + either (\err -> footnoteShow err >> failure) pure $ + runTestActions NoSmartHoles (maxID expr) expr @@ -497,11 +497,11 @@ unit_case_create = , constructSaturatedCon cZero ] ( ann - ( lam "x" - $ hole - $ case_ - (lvar "x") - [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] + ( lam "x" $ + hole $ + case_ + (lvar "x") + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) (tfun (tcon tBool) (tcon tNat)) ) @@ -512,18 +512,18 @@ unit_case_tidy = actionTest NoSmartHoles ( ann - ( lam "x" - $ hole - $ case_ - (lvar "x") - [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] + ( lam "x" $ + hole $ + case_ + (lvar "x") + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) (tfun (tcon tBool) (tcon tNat)) ) [Move Child1, Move Child1, FinishHole] ( ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (lvar "x") [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) @@ -536,14 +536,14 @@ unit_case_move_branch_1 = actionTest NoSmartHoles ( ann - ( lam "x" - $ hole - $ ann - ( case_ - (lvar "x") - [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] - ) - tEmptyHole + ( lam "x" $ + hole $ + ann + ( case_ + (lvar "x") + [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] + ) + tEmptyHole ) (tfun (tcon tNat) (tcon tNat)) ) @@ -558,14 +558,14 @@ unit_case_move_branch_1 = , ConstructVar $ LocalVarRef "n" ] ( ann - ( lam "x" - $ hole - $ ann - ( case_ - (lvar "x") - [branch cZero [] (con0 cZero), branch cSucc [("n", Nothing)] (lvar "n")] - ) - tEmptyHole + ( lam "x" $ + hole $ + ann + ( case_ + (lvar "x") + [branch cZero [] (con0 cZero), branch cSucc [("n", Nothing)] (lvar "n")] + ) + tEmptyHole ) (tfun (tcon tNat) (tcon tNat)) ) @@ -576,8 +576,8 @@ unit_case_move_branch_2 = actionTest NoSmartHoles ( ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (lvar "x") [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] ) @@ -592,8 +592,8 @@ unit_case_move_branch_2 = , ConstructVar $ LocalVarRef "n" ] ( ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (lvar "x") [branch cZero [] (con0 cZero), branch cSucc [("n", Nothing)] (lvar "n")] ) @@ -606,14 +606,14 @@ unit_case_move_scrutinee_1 = actionTest NoSmartHoles ( ann - ( lam "x" - $ hole - $ ann - ( case_ - (lvar "x") - [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] - ) - tEmptyHole + ( lam "x" $ + hole $ + ann + ( case_ + (lvar "x") + [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] + ) + tEmptyHole ) (tfun (tcon tNat) (tcon tNat)) ) @@ -625,14 +625,14 @@ unit_case_move_scrutinee_1 = , SetMetadata "meta" ] ( ann - ( lam "x" - $ hole - $ ann - ( case_ - (setMeta "meta" $ lvar "x") - [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] - ) - tEmptyHole + ( lam "x" $ + hole $ + ann + ( case_ + (setMeta "meta" $ lvar "x") + [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] + ) + tEmptyHole ) (tfun (tcon tNat) (tcon tNat)) ) @@ -643,8 +643,8 @@ unit_case_move_scrutinee_2 = actionTest NoSmartHoles ( ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (lvar "x") [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] ) @@ -652,8 +652,8 @@ unit_case_move_scrutinee_2 = ) [Move Child1, Move Child1, Move Child1, SetMetadata "meta"] ( ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (setMeta "meta" $ lvar "x") [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] ) @@ -685,14 +685,14 @@ unit_bad_case_3 = (const True) NoSmartHoles ( ann - ( lam "x" - $ hole - $ ann - ( case_ - (lvar "x") - [branch cTrue [] emptyHole, branch cFalse [] emptyHole] - ) - tEmptyHole + ( lam "x" $ + hole $ + ann + ( case_ + (lvar "x") + [branch cTrue [] emptyHole, branch cFalse [] emptyHole] + ) + tEmptyHole ) (tfun (tcon tBool) (tcon tNat)) ) @@ -719,8 +719,8 @@ unit_case_on_hole = , ConstructCase ] ( ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (ann emptyHole $ tcon tNat) [branch cZero [] emptyHole, branch cSucc [("a44", Nothing)] emptyHole] -- NB: fragile names here ) @@ -733,8 +733,8 @@ unit_case_fill_hole_scrut = actionTest NoSmartHoles ( ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (ann emptyHole $ tcon tNat) [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] ) @@ -749,8 +749,8 @@ unit_case_fill_hole_scrut = , RemoveAnn ] ( ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (lvar "x") [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole] ) @@ -900,53 +900,53 @@ unit_case_branches = let e cse = ann cse (tcon tBool) n = "a39" e0 = - e - $ caseFB_ + e $ + caseFB_ (emptyHole `ann` tcon tNat) [] (con0 cTrue) e1 = - e - $ caseFB_ + e $ + caseFB_ (emptyHole `ann` tcon tNat) [branch cSucc [(n, Nothing)] $ con0 cTrue] (con0 cTrue) e2 = - e - $ case_ + e $ + case_ (emptyHole `ann` tcon tNat) [ branch cZero [] $ con0 cFalse , branch cSucc [(n, Nothing)] $ con0 cTrue ] e3 = - e - $ caseFB_ + e $ + caseFB_ (emptyHole `ann` tcon tNat) [branch cSucc [(n, Nothing)] $ con0 cTrue] (con0 cFalse) e4 = - e - $ caseFB_ + e $ + caseFB_ (emptyHole `ann` tcon tNat) [] (con0 cFalse) e' cse = ann cse (tcon tMaybe `tapp` tcon tNat) e5 = - e' - $ case_ + e' $ + case_ (emptyHole `ann` tcon tNat) [ branch cZero [] $ con0 cNothing , branch cSucc [("n", Nothing)] $ con1 cJust $ lvar "n" ] e6 = - e' - $ caseFB_ + e' $ + caseFB_ (emptyHole `ann` tcon tNat) [branch cZero [] $ con0 cNothing] (con1 cJust emptyHole) e7 = - e' - $ caseFB_ + e' $ + caseFB_ (emptyHole `ann` tcon tNat) [branch cZero [] $ con0 cNothing] (con1 cJust $ con0 cZero) @@ -1003,26 +1003,26 @@ unit_case_prim :: Assertion unit_case_prim = let e cse = ann cse (tcon tBool) e0 = - e - $ caseFB_ + e $ + caseFB_ (emptyHole `ann` tcon tChar) [] (con0 cTrue) e1 = - e - $ caseFB_ + e $ + caseFB_ (emptyHole `ann` tcon tChar) [branchPrim (PrimChar 'x') $ con0 cTrue] (con0 cTrue) e2 = - e - $ caseFB_ + e $ + caseFB_ (emptyHole `ann` tcon tChar) [branchPrim (PrimChar 'x') $ con0 cFalse] (con0 cTrue) e3 = - e - $ caseFB_ + e $ + caseFB_ (emptyHole `ann` tcon tChar) [] (con0 cTrue) @@ -1146,8 +1146,8 @@ unit_poly_1 = , Move Child2 , ConstructVar $ LocalVarRef "id" ] - ( let_ "id" (ann (lAM "a" $ lam "x" $ lvar "x") (tforall "a" ktype $ tfun (tvar "a") (tvar "a"))) - $ app (aPP (lvar "id") (tforall "b" ktype $ tfun (tvar "b") (tvar "b"))) (lvar "id") + ( let_ "id" (ann (lAM "a" $ lam "x" $ lvar "x") (tforall "a" ktype $ tfun (tvar "a") (tvar "a"))) $ + app (aPP (lvar "id") (tforall "b" ktype $ tfun (tvar "b") (tvar "b"))) (lvar "id") ) unit_constructTApp :: Assertion @@ -1223,8 +1223,7 @@ unit_refine_mismatch_var = ) ) ) - $ emptyHole - `ann` tcon tBool + $ emptyHole `ann` tcon tBool ) [Move Child2, Move Child1, InsertRefinedVar $ LocalVarRef "cons"] ( let_ @@ -1239,8 +1238,7 @@ unit_refine_mismatch_var = ) ) ) - $ hole (lvar "cons" `aPP` tEmptyHole `app` emptyHole `app` emptyHole) - `ann` tcon tBool + $ hole (lvar "cons" `aPP` tEmptyHole `app` emptyHole `app` emptyHole) `ann` tcon tBool ) unit_primitive_1 :: Assertion @@ -1331,8 +1329,7 @@ actionTestExpectFail f sh expr actions = -- given value. Fails if the actions fail. runTestActions :: SmartHoles -> ID -> Expr -> [Action] -> Either ActionError Expr runTestActions sh i expr actions = - unfocusExpr - . unfocusLoc + unfocusExpr . unfocusLoc <$> evalTestM (i + 1) ( do diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 27eb79b57..5bd8cd7cb 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -262,16 +262,15 @@ mkTests deps (defName, DefAST def') = Input a . fromMaybe (error "id not found") $ Available.options typeDefs defs cxt level (Right def) id a - in testGroup testName - $ enumeratePairs - <&> \(level, mut) -> + in testGroup testName $ + enumeratePairs <&> \(level, mut) -> let defActions = map (offered level $ SelectionDef $ DefSelection defName Nothing) $ Available.forDef defs level mut d bodyActions = map ( \id -> ( id - , map (offered level $ SelectionDef $ DefSelection defName $ Just $ NodeSelection BodyNode id) - $ Available.forBody + , map (offered level $ SelectionDef $ DefSelection defName $ Just $ NodeSelection BodyNode id) $ + Available.forBody typeDefs level mut @@ -290,42 +289,37 @@ mkTests deps (defName, DefAST def') = ) . toListOf (_typeMeta % _id) $ astDefType def - in goldenVsString (show level <> ":" <> show mut) ("test/outputs/available-actions" testName show level <> "-" <> show mut <> ".fragment") - $ pure - . BS.fromStrict - . encodeUtf8 - . TL.toStrict - . pShowNoColor - $ Output - { defActions - , bodyActions - , sigActions - } + in goldenVsString (show level <> ":" <> show mut) ("test/outputs/available-actions" testName show level <> "-" <> show mut <> ".fragment") $ + pure . BS.fromStrict . encodeUtf8 . TL.toStrict . pShowNoColor $ + Output + { defActions + , bodyActions + , sigActions + } -- Any offered action will complete successfully, -- other than one with a student-specified name that introduces capture. tasty_available_actions_accepted :: Property -tasty_available_actions_accepted = withTests 500 - $ withDiscards 2000 - $ propertyWT [] - $ do - l <- forAllT $ Gen.element enumerate - cxt <- forAllT $ Gen.choice $ map sequence [[], [builtinModule], [builtinModule, primitiveModule]] - -- We only test SmartHoles mode (which is the only supported student-facing - -- mode - NoSmartHoles is only used for internal sanity testing etc) - a <- forAllT $ genApp SmartHoles cxt - (def'', loc, action) <- forAllT $ genAction l a - annotateShow def'' - annotateShow loc - annotateShow action - let (_defName, def) = (bimap fst fst def'', bimap snd snd def'') - collect action - pa <- toProgAction l a (def, loc, action) - case pa of - NoOpt progActs -> void $ actionSucceeds (handleEditRequest progActs) a - OptOffered _ progActs -> void $ actionSucceeds (handleEditRequest progActs) a - OptGen _ progActs -> void $ actionSucceedsOrCapture (handleEditRequest progActs) a - NoOfferedOpts -> annotate "no options" >> success +tasty_available_actions_accepted = withTests 500 $ + withDiscards 2000 $ + propertyWT [] $ do + l <- forAllT $ Gen.element enumerate + cxt <- forAllT $ Gen.choice $ map sequence [[], [builtinModule], [builtinModule, primitiveModule]] + -- We only test SmartHoles mode (which is the only supported student-facing + -- mode - NoSmartHoles is only used for internal sanity testing etc) + a <- forAllT $ genApp SmartHoles cxt + (def'', loc, action) <- forAllT $ genAction l a + annotateShow def'' + annotateShow loc + annotateShow action + let (_defName, def) = (bimap fst fst def'', bimap snd snd def'') + collect action + pa <- toProgAction l a (def, loc, action) + case pa of + NoOpt progActs -> void $ actionSucceeds (handleEditRequest progActs) a + OptOffered _ progActs -> void $ actionSucceeds (handleEditRequest progActs) a + OptGen _ progActs -> void $ actionSucceedsOrCapture (handleEditRequest progActs) a + NoOfferedOpts -> annotate "no options" >> success -- Running multiple "things" one after the other will succeed -- (other than student-specified names causing capture), where a "thing" is one of: @@ -335,112 +329,111 @@ tasty_available_actions_accepted = withTests 500 -- - running some full evaluation -- - asking a @Question@ tasty_multiple_requests_accepted :: Property -tasty_multiple_requests_accepted = withTests 500 - $ withDiscards 2000 - $ propertyWT [] - $ do - l <- forAllT $ Gen.element enumerate - cxt <- forAllT $ Gen.choice $ map sequence [[], [builtinModule], [builtinModule, primitiveModule]] - -- We only test SmartHoles mode (which is the only supported student-facing - -- mode - NoSmartHoles is only used for internal sanity testing etc) - app0 <- forAllT $ genApp SmartHoles cxt - numActions <- forAllT $ Gen.int $ Range.linear 1 20 - let appDefs = foldMap' (M.keys . moduleDefsQualified) . progModules . appProg - genAction' a' = - Gen.frequency - $ second pure - <$> catMaybes - [ Just (3, AddTm) - , Just (2, AddTy) - , Just (1, Eval1) - , if null $ appDefs a' then Nothing else Just (1, EvalFull) - , Just (1, Question) - , if null $ appDefs a' then Nothing else Just (1, EvalBoundedInterp) - , if undoLogEmpty $ appProg a' then Nothing else Just (2, Undo) - , if redoLogEmpty $ appProg a' then Nothing else Just (2, Redo) - , Just (1, RenameModule) - , Just (10, AvailAct) - ] - void $ iterateNM numActions app0 $ \appN -> - forAllT (genAction' appN) >>= \a -> do - collect a - case a of - AddTm -> do - m <- forAllT $ Gen.element $ fmap moduleName $ progModules $ appProg appN - n <- forAllT $ Gen.choice [Just . unName <$> genName, pure Nothing] - actionSucceedsOrCapture (handleMutationRequest $ Edit [CreateDef m n]) appN - >>= ignoreCaptureClash appN - AddTy -> do - m <- forAllT $ Gen.element $ fmap moduleName $ progModules $ appProg appN - n <- qualifyName m <$> forAllT genName - actionSucceedsOrCapture (handleMutationRequest $ Edit [AddTypeDef n $ ASTTypeDef [] [] []]) appN - >>= ignoreCaptureClash appN - Eval1 -> do - (e', _) <- forAllT genSyn - e <- generateIDs e' - i <- forAllT $ Gen.element $ e ^.. exprIDs - actionSucceedsOrNotRedex (readerToState $ handleEvalRequest $ EvalReq e i) appN - EvalFull -> do - g <- forAllT $ Gen.element $ appDefs appN - tld <- gvar g - steps <- forAllT $ Gen.integral $ Range.linear 0 100 - optsN <- forAllT $ Gen.element @[] [StopAtBinders, UnderBinders] - actionSucceeds (readerToState $ handleEvalFullRequest $ EvalFullReq tld Chk steps optsN) appN - EvalBoundedInterp -> do - g <- forAllT $ Gen.element $ appDefs appN - tld <- gvar g - usec <- forAllT $ Gen.integral $ Range.linear 0 1000 - actionSucceeds (readerToState $ handleEvalBoundedInterpRequest $ EvalBoundedInterpReq tld Chk (MicroSec usec)) appN - Question -> do - -- Obtain a non-exhaustive case warning if we add a new question - let _w :: Question q -> () - _w = \case - VariablesInScope{} -> () - GenerateName{} -> () - (_, e, w) <- forAllT $ genLoc appN - -- We only support questions in editable modules - case e of - Editable -> pure () - NonEditable -> discard - (def, node) <- case w of - SelectionDef (DefSelection{def, node = Just node}) -> pure (def, node.meta) - SelectionDef (DefSelection{node = Nothing}) -> discard - -- We don't currently support questions on typedefs - SelectionTypeDef _ -> discard - (_, q) <- - forAllWithT fst - $ Gen.choice - [ pure ("VariablesInScope", void $ handleQuestion (VariablesInScope def node)) - , ("GenerateName",) . void . handleQuestion . GenerateName def node <$> do - k <- genWTKind - Gen.choice - [ Left <$> Gen.maybe (genWTType k) - , pure $ Right $ Just k - , pure $ Right Nothing - ] +tasty_multiple_requests_accepted = withTests 500 $ + withDiscards 2000 $ + propertyWT [] $ do + l <- forAllT $ Gen.element enumerate + cxt <- forAllT $ Gen.choice $ map sequence [[], [builtinModule], [builtinModule, primitiveModule]] + -- We only test SmartHoles mode (which is the only supported student-facing + -- mode - NoSmartHoles is only used for internal sanity testing etc) + app0 <- forAllT $ genApp SmartHoles cxt + numActions <- forAllT $ Gen.int $ Range.linear 1 20 + let appDefs = foldMap' (M.keys . moduleDefsQualified) . progModules . appProg + genAction' a' = + Gen.frequency $ + second pure + <$> catMaybes + [ Just (3, AddTm) + , Just (2, AddTy) + , Just (1, Eval1) + , if null $ appDefs a' then Nothing else Just (1, EvalFull) + , Just (1, Question) + , if null $ appDefs a' then Nothing else Just (1, EvalBoundedInterp) + , if undoLogEmpty $ appProg a' then Nothing else Just (2, Undo) + , if redoLogEmpty $ appProg a' then Nothing else Just (2, Redo) + , Just (1, RenameModule) + , Just (10, AvailAct) ] - actionSucceeds (readerToState q) appN - Undo -> actionSucceeds (handleMutationRequest App.Undo) appN - Redo -> actionSucceeds (handleMutationRequest App.Redo) appN - AvailAct -> do - (def'', loc, action) <- forAllT $ genAction l appN - annotateShow def'' - annotateShow loc - annotateShow action - let def = bimap snd snd def'' - collect action - pa <- toProgAction l appN (def, loc, action) - case pa of - NoOpt progActs -> actionSucceeds (handleEditRequest progActs) appN - OptOffered _ progActs -> actionSucceeds (handleEditRequest progActs) appN - OptGen _ progActs -> - actionSucceedsOrCapture (handleEditRequest progActs) appN - >>= ignoreCaptureClash appN - NoOfferedOpts -> annotate "ignoring - no options" >> pure appN - RenameModule -> do - m <- forAllT $ moduleName <$> Gen.element (progModules $ appProg appN) - n <- forAllT (Gen.nonEmpty (Range.linear 1 5) genName) - actionSucceedsOrCapture (handleMutationRequest $ Edit [App.RenameModule m $ unName <$> n]) appN >>= ignoreCaptureClash appN + void $ iterateNM numActions app0 $ \appN -> + forAllT (genAction' appN) >>= \a -> do + collect a + case a of + AddTm -> do + m <- forAllT $ Gen.element $ fmap moduleName $ progModules $ appProg appN + n <- forAllT $ Gen.choice [Just . unName <$> genName, pure Nothing] + actionSucceedsOrCapture (handleMutationRequest $ Edit [CreateDef m n]) appN + >>= ignoreCaptureClash appN + AddTy -> do + m <- forAllT $ Gen.element $ fmap moduleName $ progModules $ appProg appN + n <- qualifyName m <$> forAllT genName + actionSucceedsOrCapture (handleMutationRequest $ Edit [AddTypeDef n $ ASTTypeDef [] [] []]) appN + >>= ignoreCaptureClash appN + Eval1 -> do + (e', _) <- forAllT genSyn + e <- generateIDs e' + i <- forAllT $ Gen.element $ e ^.. exprIDs + actionSucceedsOrNotRedex (readerToState $ handleEvalRequest $ EvalReq e i) appN + EvalFull -> do + g <- forAllT $ Gen.element $ appDefs appN + tld <- gvar g + steps <- forAllT $ Gen.integral $ Range.linear 0 100 + optsN <- forAllT $ Gen.element @[] [StopAtBinders, UnderBinders] + actionSucceeds (readerToState $ handleEvalFullRequest $ EvalFullReq tld Chk steps optsN) appN + EvalBoundedInterp -> do + g <- forAllT $ Gen.element $ appDefs appN + tld <- gvar g + usec <- forAllT $ Gen.integral $ Range.linear 0 1000 + actionSucceeds (readerToState $ handleEvalBoundedInterpRequest $ EvalBoundedInterpReq tld Chk (MicroSec usec)) appN + Question -> do + -- Obtain a non-exhaustive case warning if we add a new question + let _w :: Question q -> () + _w = \case + VariablesInScope{} -> () + GenerateName{} -> () + (_, e, w) <- forAllT $ genLoc appN + -- We only support questions in editable modules + case e of + Editable -> pure () + NonEditable -> discard + (def, node) <- case w of + SelectionDef (DefSelection{def, node = Just node}) -> pure (def, node.meta) + SelectionDef (DefSelection{node = Nothing}) -> discard + -- We don't currently support questions on typedefs + SelectionTypeDef _ -> discard + (_, q) <- + forAllWithT fst $ + Gen.choice + [ pure ("VariablesInScope", void $ handleQuestion (VariablesInScope def node)) + , ("GenerateName",) . void . handleQuestion . GenerateName def node <$> do + k <- genWTKind + Gen.choice + [ Left <$> Gen.maybe (genWTType k) + , pure $ Right $ Just k + , pure $ Right Nothing + ] + ] + actionSucceeds (readerToState q) appN + Undo -> actionSucceeds (handleMutationRequest App.Undo) appN + Redo -> actionSucceeds (handleMutationRequest App.Redo) appN + AvailAct -> do + (def'', loc, action) <- forAllT $ genAction l appN + annotateShow def'' + annotateShow loc + annotateShow action + let def = bimap snd snd def'' + collect action + pa <- toProgAction l appN (def, loc, action) + case pa of + NoOpt progActs -> actionSucceeds (handleEditRequest progActs) appN + OptOffered _ progActs -> actionSucceeds (handleEditRequest progActs) appN + OptGen _ progActs -> + actionSucceedsOrCapture (handleEditRequest progActs) appN + >>= ignoreCaptureClash appN + NoOfferedOpts -> annotate "ignoring - no options" >> pure appN + RenameModule -> do + m <- forAllT $ moduleName <$> Gen.element (progModules $ appProg appN) + n <- forAllT (Gen.nonEmpty (Range.linear 1 5) genName) + actionSucceedsOrCapture (handleMutationRequest $ Edit [App.RenameModule m $ unName <$> n]) appN >>= ignoreCaptureClash appN where ignoreCaptureClash a = \case Succeed b -> pure b @@ -715,13 +708,13 @@ toProgAction l a (def, loc, action) = do Just action' -> case action' of Available.NoInput act' -> do progActs <- - either (\e -> annotateShow e >> failure) pure - $ toProgActionNoInput (progDefMap $ appProg a) def' loc act' + either (\e -> annotateShow e >> failure) pure $ + toProgActionNoInput (progDefMap $ appProg a) def' loc act' pure $ NoOpt progActs Available.Input act' -> do Available.Options{Available.opts, Available.free} <- - maybe (annotate "id not found" >> failure) pure - $ Available.options + maybe (annotate "id not found" >> failure) pure $ + Available.options (progTypeDefMap $ appProg a) (progDefMap $ appProg a) (progCxt $ appProg a) @@ -948,12 +941,12 @@ offeredActionTest' sh l inputDef position action = do ms <- sequence [builtinModule, primitiveModule] prog0 <- defaultEmptyProg d <- inputDef - pure - $ prog0 - & (#progModules % _head % #moduleDefs % ix "main" .~ DefAST d) - & (#progImports .~ ms) - -- Temporarily disable smart holes, so what is written in unit tests is what is in the prog - & (#progSmartHoles .~ NoSmartHoles) + pure $ + prog0 + & (#progModules % _head % #moduleDefs % ix "main" .~ DefAST d) + & (#progImports .~ ms) + -- Temporarily disable smart holes, so what is written in unit tests is what is in the prog + & (#progSmartHoles .~ NoSmartHoles) -- Typecheck everything to fill in typecaches. -- This lets us test offered names for renaming variable binders. let progChecked = runTypecheckTestM NoSmartHoles $ checkProgWellFormed progRaw @@ -964,19 +957,19 @@ offeredActionTest' sh l inputDef position action = do Just (DefAST def@(ASTDef e t)) -> (progImports p, e, t, def, qualifyName (moduleName m) "main", p & #progSmartHoles .~ sh) _ -> error "offeredActionTest: didn't find 'main'" _ -> error "offeredActionTest: expected exactly one progModule" - let id' = evalTestM (nextProgID prog) - $ runExceptT - $ flip runReaderT (buildTypingContextFromModules modules sh) - $ case position of - InBody pos' -> do - ez <- foldlM (flip moveExpr) (focus expr) $ exprMoves pos' - case typeMoves pos' of - Nothing -> pure $ getID ez - Just ms -> do - tz' <- enterType ez - tz <- foldlM (flip moveType) tz' ms - pure $ getID tz - InSig moves -> getID <$> foldlM (flip move) (focus sig) moves + let id' = evalTestM (nextProgID prog) $ + runExceptT $ + flip runReaderT (buildTypingContextFromModules modules sh) $ + case position of + InBody pos' -> do + ez <- foldlM (flip moveExpr) (focus expr) $ exprMoves pos' + case typeMoves pos' of + Nothing -> pure $ getID ez + Just ms -> do + tz' <- enterType ez + tz <- foldlM (flip moveType) tz' ms + pure $ getID tz + InSig moves -> getID <$> foldlM (flip move) (focus sig) moves id <- case id' of Left err -> assertFailure $ show err Right i' -> pure i' @@ -988,8 +981,8 @@ offeredActionTest' sh l inputDef position action = do let options = Available.options cxt.typeDefs defs cxt l (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) action' <- case action of Left a -> - pure - $ if Available.NoInput a `elem` offered + pure $ + if Available.NoInput a `elem` offered then Right $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a else Left $ ActionNotOffered (Available.NoInput a) offered Right (a, o) -> do @@ -997,8 +990,8 @@ offeredActionTest' sh l inputDef position action = do then case options a of Nothing -> assertFailure "Available.options returned Nothing" Just os -> - pure - $ if o `elem` os.opts + pure $ + if o `elem` os.opts then Right $ toProgActionInput (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) o a else Left $ OptionNotOffered o os.opts else pure $ Left $ ActionNotOffered (Available.Input a) offered diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index baedf7e73..aa803912d 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -158,17 +158,15 @@ mkEmptyTestApp p = in mkApp (nextProgID p) (appNameCounter a) p unit_empty_actions_only_change_the_log :: Assertion -unit_empty_actions_only_change_the_log = progActionTest defaultEmptyProg [] - $ expectSuccess - $ \prog prog' -> +unit_empty_actions_only_change_the_log = progActionTest defaultEmptyProg [] $ + expectSuccess $ \prog prog' -> prog' @?= prog{progLog = Log [[]]} -- We can move to the default def in a program -- (this may only exist at the start of a session) unit_move_to_def_main :: Assertion -unit_move_to_def_main = progActionTest defaultEmptyProg [moveToDef "main"] - $ expectSuccess - $ \prog prog' -> +unit_move_to_def_main = progActionTest defaultEmptyProg [moveToDef "main"] $ + expectSuccess $ \prog prog' -> prog' @?= prog { progLog = Log [[moveToDef "main"]] @@ -179,9 +177,8 @@ unit_move_to_def_main = progActionTest defaultEmptyProg [moveToDef "main"] -- def. unit_move_to_def_and_construct_let :: Assertion unit_move_to_def_and_construct_let = - progActionTest defaultEmptyProg [moveToDef "other", BodyAction [ConstructLet (Just "x")]] - $ expectSuccess - $ \prog prog' -> + progActionTest defaultEmptyProg [moveToDef "other", BodyAction [ConstructLet (Just "x")]] $ + expectSuccess $ \prog prog' -> case astDefExpr <$> lookupASTDef' "other" prog' of Just Let{} -> -- Check that main is unchanged @@ -190,9 +187,8 @@ unit_move_to_def_and_construct_let = unit_rename_def :: Assertion unit_rename_def = - progActionTest defaultEmptyProg [renameDef "other" "foo"] - $ expectSuccess - $ \_ prog' -> do + progActionTest defaultEmptyProg [renameDef "other" "foo"] $ + expectSuccess $ \_ prog' -> do assertNothing (lookupDef' "other" prog') assertJust (lookupDef' "foo" prog') assertJust (lookupDef' "main" prog') @@ -205,13 +201,13 @@ assertJust = assertBool "Expected Nothing" . isJust unit_rename_def_to_same_name_as_existing_def :: Assertion unit_rename_def_to_same_name_as_existing_def = - progActionTest defaultEmptyProg [renameDef "main" "main"] - $ expectError (@?= DefAlreadyExists (gvn "main")) + progActionTest defaultEmptyProg [renameDef "main" "main"] $ + expectError (@?= DefAlreadyExists (gvn "main")) unit_rename_def_to_same_name_as_existing_def_prim :: Assertion unit_rename_def_to_same_name_as_existing_def_prim = - progActionTest defaultFullProg [renameDef "other" "toUpper"] - $ expectError (@?= DefAlreadyExists (gvn "toUpper")) + progActionTest defaultFullProg [renameDef "other" "toUpper"] $ + expectError (@?= DefAlreadyExists (gvn "toUpper")) unit_rename_def_referenced :: Assertion unit_rename_def_referenced = @@ -244,9 +240,8 @@ unit_rename_def_recursive = unit_delete_def :: Assertion unit_delete_def = - progActionTest defaultEmptyProg [deleteDef "other"] - $ expectSuccess - $ \_ prog' -> do + progActionTest defaultEmptyProg [deleteDef "other"] $ + expectSuccess $ \_ prog' -> do assertNothing (lookupDef' "other" prog') assertJust (lookupDef' "main" prog') @@ -265,15 +260,14 @@ unit_delete_def_referenced = unit_delete_def_unknown_id :: Assertion unit_delete_def_unknown_id = - progActionTest defaultEmptyProg [deleteDef "unknown"] - $ expectError (@?= DefNotFound (gvn "unknown")) + progActionTest defaultEmptyProg [deleteDef "unknown"] $ + expectError (@?= DefNotFound (gvn "unknown")) -- 'foo = foo' shouldn't count as "in use" and block deleting itself unit_delete_def_recursive :: Assertion unit_delete_def_recursive = - progActionTest defaultEmptyProg [moveToDef "main", BodyAction [ConstructVar $ globalVarRef "main"], deleteDef "main"] - $ expectSuccess - $ \prog prog' -> + progActionTest defaultEmptyProg [moveToDef "main", BodyAction [ConstructVar $ globalVarRef "main"], deleteDef "main"] $ + expectSuccess $ \prog prog' -> Map.delete (qualifyName mainModuleName "main") (foldMap' moduleDefsQualified $ progModules prog) @@ -295,9 +289,8 @@ unit_construct_let_without_moving_to_def_first = $ expectError (@?= NoDefSelected) unit_create_def :: Assertion -unit_create_def = progActionTest defaultEmptyProg [CreateDef mainModuleName $ Just "newDef"] - $ expectSuccess - $ \_ prog' -> do +unit_create_def = progActionTest defaultEmptyProg [CreateDef mainModuleName $ Just "newDef"] $ + expectSuccess $ \_ prog' -> do case lookupASTDef' "newDef" prog' of Nothing -> assertFailure $ show $ moduleDefs <$> progModules prog' Just def -> do @@ -305,14 +298,14 @@ unit_create_def = progActionTest defaultEmptyProg [CreateDef mainModuleName $ Ju unit_create_def_clash_prim :: Assertion unit_create_def_clash_prim = - progActionTest defaultFullProg [CreateDef mainModuleName $ Just "toUpper"] - $ expectError (@?= DefAlreadyExists (gvn "toUpper")) + progActionTest defaultFullProg [CreateDef mainModuleName $ Just "toUpper"] $ + expectError (@?= DefAlreadyExists (gvn "toUpper")) unit_create_def_nonexistant_module :: Assertion unit_create_def_nonexistant_module = let nonExistantModule = ModuleName ["NonExistantModule"] - in progActionTest defaultEmptyProg [CreateDef nonExistantModule $ Just "newDef"] - $ expectError (@?= ModuleNotFound nonExistantModule) + in progActionTest defaultEmptyProg [CreateDef nonExistantModule $ Just "newDef"] $ + expectError (@?= ModuleNotFound nonExistantModule) unit_create_def_imported_module :: Assertion unit_create_def_imported_module = @@ -344,14 +337,14 @@ unit_create_typedef = , astTypeDefConstructors = [ValCon (vcn "Node") [TVar () "a", TApp () (TCon () (tcn "List")) (TApp () (TCon () (tcn "Tree")) (TVar () "a"))]] , astTypeDefNameHints = ["xs", "ys", "zs"] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "List") lst, AddTypeDef (tcn "Tree") tree] - $ expectSuccess - $ \_ prog' -> do - case Map.elems $ foldMap' (fmap forgetTypeDefMetadata . moduleTypes) $ progModules prog' of - [lst', tree'] -> do - TypeDefAST lst @=? lst' - TypeDefAST tree @=? tree' - _ -> assertFailure $ show $ moduleTypes <$> progModules prog' + in progActionTest defaultEmptyProg [AddTypeDef (tcn "List") lst, AddTypeDef (tcn "Tree") tree] $ + expectSuccess $ + \_ prog' -> do + case Map.elems $ foldMap' (fmap forgetTypeDefMetadata . moduleTypes) $ progModules prog' of + [lst', tree'] -> do + TypeDefAST lst @=? lst' + TypeDefAST tree @=? tree' + _ -> assertFailure $ show $ moduleTypes <$> progModules prog' -- "List" is unknown here unit_create_typedef_bad_1 :: Assertion @@ -362,8 +355,8 @@ unit_create_typedef_bad_1 = , astTypeDefConstructors = [ValCon (vcn "Node") [TVar () "a", TApp () (TCon () $ tcn "List") (TApp () (TCon () $ tcn "Tree") (TVar () "a"))]] , astTypeDefNameHints = ["xs", "ys", "zs"] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "Tree") td] - $ expectError (@?= (TypeDefError $ show $ KindError $ UnknownTypeConstructor (tcn "List"))) + in progActionTest defaultEmptyProg [AddTypeDef (tcn "Tree") td] $ + expectError (@?= (TypeDefError $ show $ KindError $ UnknownTypeConstructor (tcn "List"))) -- duplicate type(names) added unit_create_typedef_bad_2 :: Assertion @@ -380,8 +373,8 @@ unit_create_typedef_bad_2 = , astTypeDefConstructors = [] , astTypeDefNameHints = [] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td1, AddTypeDef (tcn "T") td2] - $ expectError (@?= TypeDefAlreadyExists (tcn "T")) + in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td1, AddTypeDef (tcn "T") td2] $ + expectError (@?= TypeDefAlreadyExists (tcn "T")) -- Forbid duplicate constructor names within one type unit_create_typedef_bad_3 :: Assertion @@ -395,8 +388,8 @@ unit_create_typedef_bad_3 = ] , astTypeDefNameHints = [] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] - $ expectError (@?= TypeDefError "InternalError \"Duplicate-ly-named constructor (perhaps in different typedefs)\"") + in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $ + expectError (@?= TypeDefError "InternalError \"Duplicate-ly-named constructor (perhaps in different typedefs)\"") -- Forbid duplicate constructor names across types unit_create_typedef_bad_4 :: Assertion @@ -413,8 +406,8 @@ unit_create_typedef_bad_4 = , astTypeDefConstructors = [ValCon (vcn "C") []] , astTypeDefNameHints = [] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T1") td1, AddTypeDef (tcn "T2") td2] - $ expectError (@?= TypeDefError "InternalError \"Duplicate-ly-named constructor (perhaps in different typedefs)\"") + in progActionTest defaultEmptyProg [AddTypeDef (tcn "T1") td1, AddTypeDef (tcn "T2") td2] $ + expectError (@?= TypeDefError "InternalError \"Duplicate-ly-named constructor (perhaps in different typedefs)\"") -- Forbid duplicate parameter names unit_create_typedef_bad_5 :: Assertion @@ -425,8 +418,8 @@ unit_create_typedef_bad_5 = , astTypeDefConstructors = [] , astTypeDefNameHints = [] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] - $ expectError (@?= TypeDefError "InternalError \"Duplicate parameter names in one tydef\"") + in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $ + expectError (@?= TypeDefError "InternalError \"Duplicate parameter names in one tydef\"") -- Forbid clash between type name and parameter name unit_create_typedef_bad_6 :: Assertion @@ -437,8 +430,8 @@ unit_create_typedef_bad_6 = , astTypeDefConstructors = [] , astTypeDefNameHints = [] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] - $ expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between type-def-name and parameter-names\"") + in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $ + expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between type-def-name and parameter-names\"") -- Forbid clash between parameter name and constructor name unit_create_typedef_bad_7 :: Assertion @@ -449,8 +442,8 @@ unit_create_typedef_bad_7 = , astTypeDefConstructors = [ValCon (vcn "a") []] , astTypeDefNameHints = [] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] - $ expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between parameter-names and constructor-names\"") + in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $ + expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between parameter-names and constructor-names\"") -- Forbid clash between type name and name of a primitive type unit_create_typedef_bad_prim :: Assertion @@ -461,8 +454,8 @@ unit_create_typedef_bad_prim = , astTypeDefConstructors = [] , astTypeDefNameHints = [] } - in progActionTest defaultFullProg [AddTypeDef (tcn "Char") td] - $ expectError (@?= TypeDefAlreadyExists (tcn "Char")) + in progActionTest defaultFullProg [AddTypeDef (tcn "Char") td] $ + expectError (@?= TypeDefAlreadyExists (tcn "Char")) -- Allow clash between type name and constructor name in one type unit_create_typedef_8 :: Assertion @@ -473,9 +466,9 @@ unit_create_typedef_8 = , astTypeDefConstructors = [ValCon (vcn "T") []] , astTypeDefNameHints = [] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] - $ expectSuccess - $ \_ prog' -> Map.elems (foldMap' moduleTypes (progModules prog')) @?= [TypeDefAST td] + in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $ + expectSuccess $ + \_ prog' -> Map.elems (foldMap' moduleTypes (progModules prog')) @?= [TypeDefAST td] -- Allow clash between type name and constructor name across types unit_create_typedef_9 :: Assertion @@ -492,15 +485,14 @@ unit_create_typedef_9 = , astTypeDefConstructors = [] , astTypeDefNameHints = [] } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td1, AddTypeDef (tcn "C") td2] - $ expectSuccess - $ \_ prog' -> Map.elems (foldMap' moduleTypes (progModules prog')) @?= [TypeDefAST td2, TypeDefAST td1] + in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td1, AddTypeDef (tcn "C") td2] $ + expectSuccess $ + \_ prog' -> Map.elems (foldMap' moduleTypes (progModules prog')) @?= [TypeDefAST td2, TypeDefAST td1] unit_construct_arrow_in_sig :: Assertion unit_construct_arrow_in_sig = - progActionTest defaultEmptyProg [moveToDef "other", SigAction [ConstructArrowL, Move Child1]] - $ expectSuccess - $ \_ prog' -> + progActionTest defaultEmptyProg [moveToDef "other", SigAction [ConstructArrowL, Move Child1]] $ + expectSuccess $ \_ prog' -> case lookupASTDef' "other" prog' of Just def -> -- Check that the signature is an arrow type @@ -530,9 +522,8 @@ unit_sigaction_creates_holes = moveToDef "main" , SigAction [Delete, ConstructTCon (mainModuleNameText, "Int")] ] - in progActionTest defaultFullProg acts - $ expectSuccess - $ \_ prog' -> + in progActionTest defaultFullProg acts $ + expectSuccess $ \_ prog' -> case lookupASTDef' "other" prog' of Just def -> -- Check that the definition is a non-empty hole @@ -552,10 +543,7 @@ unit_copy_paste_duplicate = do blankDef <- ASTDef <$> emptyHole <*> tEmptyHole pure ( newProg'{progSelection = Nothing} - & #progModules - % _head - % #moduleDefs - .~ Map.fromList [("main", DefAST mainDef), ("blank", DefAST blankDef)] + & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST mainDef), ("blank", DefAST blankDef)] , getID mainType , getID mainExpr , getID (astDefType blankDef) @@ -598,12 +586,12 @@ unit_copy_paste_type_scoping = do (pInitial, srcID, pExpected) = create' $ do toCopy <- tvar "a" `tfun` tvar "b" `tfun` tforall "e" ktype (tvar "c" `tfun` tvar "d" `tfun` tvar "e" `tfun` tvar "f") let skel r = - tforall "a" ktype - $ tforall "d" ktype - $ tforall "f" ktype - $ tfun (tforall "b" ktype $ tforall "c" ktype $ tforall "d" ktype $ pure toCopy) - $ tforall "c" ktype - $ tforall "f" ktype r + tforall "a" ktype $ + tforall "d" ktype $ + tforall "f" ktype $ + tfun (tforall "b" ktype $ tforall "c" ktype $ tforall "d" ktype $ pure toCopy) $ + tforall "c" ktype $ + tforall "f" ktype r defInitial <- ASTDef <$> emptyHole <*> skel tEmptyHole expected <- ASTDef <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "e" ktype (tEmptyHole `tfun` tEmptyHole `tfun` tvar "e" `tfun` tEmptyHole)) pure @@ -660,13 +648,13 @@ unit_copy_paste_expr_1 = do let toCopy' = con cMakePair [lvar "y" `ann` tvar "a", lvar "z" `ann` tvar "b"] -- want different IDs for the two occurences in expected toCopy <- toCopy' let skel r = - lAM "a" - $ lam "x" - $ case_ - (lvar "x") - [ branch cNil [] r - , branch cCons [("y", Nothing), ("ys", Nothing)] $ lAM "b" $ lam "z" $ pure toCopy - ] + lAM "a" $ + lam "x" $ + case_ + (lvar "x") + [ branch cNil [] r + , branch cCons [("y", Nothing), ("ys", Nothing)] $ lAM "b" $ lam "z" $ pure toCopy + ] expectPasted <- con cMakePair [emptyHole `ann` tvar "a", emptyHole `ann` tEmptyHole] -- TODO: in the future we may want to insert let bindings for variables -- which are out of scope in the target, and produce something like @@ -773,9 +761,9 @@ unit_import_vars = gets (fmap (Map.assocs . moduleDefsQualified) . progModules . appProg) >>= \case [[(i, DefAST d)]] -> do (_, vs) <- readerToState (handleQuestion (VariablesInScope i $ getID $ astDefExpr d)) - pure - $ assertBool "VariablesInScope did not report the imported Int.+" - $ any ((== primitiveGVar IntAdd) . fst) vs + pure $ + assertBool "VariablesInScope did not report the imported Int.+" $ + any ((== primitiveGVar IntAdd) . fst) vs _ -> pure $ assertFailure "Expected one def 'main' from newEmptyApp" a = newEmptyApp in runAppTestM a test <&> fst >>= \case @@ -865,8 +853,8 @@ unit_copy_paste_import = unit_DeleteTypeDef :: Assertion unit_DeleteTypeDef = progActionTest - ( defaultProgEditableTypeDefs - $ sequence + ( defaultProgEditableTypeDefs $ + sequence [ do x <- emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tEmptyHole) astDef "def1" x <$> tEmptyHole @@ -875,8 +863,8 @@ unit_DeleteTypeDef = progActionTest astDef "def2" x <$> tEmptyHole , do x <- - lam "a" - $ case_ + lam "a" $ + case_ (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int"))) [ branch cA [("x", Nothing), ("y", Nothing), ("z", Nothing)] emptyHole , branch cB [("s", Nothing), ("t", Nothing)] emptyHole @@ -891,9 +879,9 @@ unit_DeleteTypeDef = progActionTest def1 <- findDef (gvn "def1") prog' forgetMetadata (astDefExpr def1) @?= forgetMetadata - ( create' - $ emptyHole - `ann` (tEmptyHole `tapp` tcon (tcn "Bool") `tapp` tEmptyHole) + ( create' $ + emptyHole + `ann` (tEmptyHole `tapp` tcon (tcn "Bool") `tapp` tEmptyHole) ) def2 <- findDef (gvn "def2") prog' forgetMetadata (astDefExpr def2) @@ -904,21 +892,21 @@ unit_DeleteTypeDef = progActionTest def3 <- findDef (gvn "def3") prog' forgetMetadata (astDefExpr def3) @?= forgetMetadata - ( create' - $ lam "a" - $ case_ - ( hole - $ emptyHole - `ann` (tEmptyHole `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int")) - ) - [] + ( create' $ + lam "a" $ + case_ + ( hole $ + emptyHole + `ann` (tEmptyHole `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int")) + ) + [] ) unit_RenameType :: Assertion unit_RenameType = progActionTest - ( defaultProgEditableTypeDefs - $ sequence + ( defaultProgEditableTypeDefs $ + sequence [ do x <- emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tEmptyHole) astDef "def" x <$> tEmptyHole @@ -935,16 +923,15 @@ unit_RenameType = , ValCon cB [TApp () (TApp () (TCon () (tcn "T'")) (TVar () "b")) (TVar () "a"), TVar () "b"] ] -- The old name does not refer to anything - assertBool "Expected the old name to be out of scope" - $ not - $ Map.member (tcn "T") - $ foldMap' moduleTypesQualified (progAllModules prog') + assertBool "Expected the old name to be out of scope" $ + not $ + Map.member (tcn "T") $ + foldMap' moduleTypesQualified (progAllModules prog') def <- findDef (gvn "def") prog' forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ emptyHole - `ann` (tcon (tcn "T'") `tapp` tcon (tcn "Bool") `tapp` tEmptyHole) + ( create' $ + emptyHole `ann` (tcon (tcn "T'") `tapp` tcon (tcn "Bool") `tapp` tEmptyHole) ) unit_RenameType_clash :: Assertion @@ -957,12 +944,12 @@ unit_RenameType_clash = unit_RenameCon :: Assertion unit_RenameCon = progActionTest - ( defaultProgEditableTypeDefs - $ sequence + ( defaultProgEditableTypeDefs $ + sequence [ do x <- - hole - $ case_ + hole $ + case_ ( con cA [ con0 (vcn "True") @@ -988,27 +975,27 @@ unit_RenameCon = def <- findDef (gvn "def") prog' forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ hole - $ case_ - ( con - (vcn "A'") - [ con0 (vcn "True") - , con0 (vcn "True") - , con0 (vcn "True") - ] - `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole) - ) - [ branch (vcn "A'") [("p", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole - , branch cB [("r", Nothing), ("x", Nothing)] emptyHole - ] + ( create' $ + hole $ + case_ + ( con + (vcn "A'") + [ con0 (vcn "True") + , con0 (vcn "True") + , con0 (vcn "True") + ] + `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole) + ) + [ branch (vcn "A'") [("p", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole + , branch cB [("r", Nothing), ("x", Nothing)] emptyHole + ] ) unit_RenameCon_clash :: Assertion unit_RenameCon_clash = progActionTest - ( defaultProgEditableTypeDefs - $ sequence + ( defaultProgEditableTypeDefs $ + sequence [ do x <- hole @@ -1049,8 +1036,8 @@ unit_RenameTypeParam_clash = unit_AddCon :: Assertion unit_AddCon = progActionTest - ( defaultProgEditableTypeDefs - $ sequence + ( defaultProgEditableTypeDefs $ + sequence [ do x <- case_ @@ -1073,8 +1060,8 @@ unit_AddCon = def <- findDef (gvn "def") prog' forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ case_ + ( create' $ + case_ (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int"))) [ branch cA [("x", Nothing), ("y", Nothing), ("z", Nothing)] emptyHole , branch (vcn "C") [] emptyHole @@ -1085,8 +1072,8 @@ unit_AddCon = unit_AddCon_sparse :: Assertion unit_AddCon_sparse = progActionTest - ( defaultProgEditableTypeDefs - $ sequence + ( defaultProgEditableTypeDefs $ + sequence [ do x <- caseFB_ @@ -1108,8 +1095,8 @@ unit_AddCon_sparse = def <- findDef (gvn "def") prog' forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ caseFB_ + ( create' $ + caseFB_ (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int"))) [ branch cB [("s", Nothing), ("t", Nothing)] emptyHole , branch (vcn "C") [] emptyHole @@ -1119,8 +1106,8 @@ unit_AddCon_sparse = unit_DeleteCon :: Assertion unit_DeleteCon = progActionTest - ( defaultProgEditableTypeDefs - $ sequence + ( defaultProgEditableTypeDefs $ + sequence [ do x <- case_ @@ -1141,8 +1128,8 @@ unit_DeleteCon = progActionTest def <- findDef (gvn "def") prog' forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ case_ + ( create' $ + case_ (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int"))) [ branch cB [("s", Nothing), ("t", Nothing)] emptyHole ] @@ -1180,8 +1167,8 @@ unit_AddConField = def <- findDef (gvn "def") prog' forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ case_ + ( create' $ + case_ ( con cA [ con0 (vcn "True") @@ -1219,8 +1206,8 @@ unit_AddConField_case_ann = def <- findDef (gvn "def") prog' forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ case_ + ( create' $ + case_ (emptyHole `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole)) [ branch cA @@ -1262,8 +1249,8 @@ unit_DeleteConField = def <- findDef (gvn "def") prog' forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ case_ + ( create' $ + case_ ( con cA [ con0 (vcn "True") @@ -1300,8 +1287,8 @@ unit_ConFieldAction = ] forgetMetadata (astDefExpr def) @?= forgetMetadata - ( create' - $ do + ( create' $ + do con cA [ con0 $ vcn "True" @@ -1436,8 +1423,8 @@ unit_rename_module_clash = unit_rename_module_nonexistant :: Assertion unit_rename_module_nonexistant = let nonExistantModule = ModuleName ["NonExistantModule"] - in progActionTest defaultEmptyProg [RenameModule nonExistantModule ["Builtins"]] - $ expectError (@?= ModuleNotFound nonExistantModule) + in progActionTest defaultEmptyProg [RenameModule nonExistantModule ["Builtins"]] $ + expectError (@?= ModuleNotFound nonExistantModule) unit_rename_module_imported :: Assertion unit_rename_module_imported = @@ -1520,12 +1507,12 @@ unit_cross_module_actions = -- Copy-paste within the sig of bar to make bar :: Bool -> Bool -- NB: CopyPasteSig relies on SmartHoles to fix any introduced inconsistencies barTy <- - gets - $ fmap astDefType - . defAST - <=< ( flip findGlobalByName (qualifyName (ModuleName ["AnotherModule"]) "bar") - . appProg - ) + gets $ + fmap astDefType + . defAST + <=< ( flip findGlobalByName (qualifyName (ModuleName ["AnotherModule"]) "bar") + . appProg + ) let srcId = case barTy of Just (TFun _ src _) -> getID src _ -> error "Unexpected shape of 'barTy'" @@ -1593,8 +1580,8 @@ unit_sh_lost_id = case astDefExpr <$> defAST def of Just (Var m (GlobalVarRef f)) | f == foo -> case progSelection prog' of Just (SelectionDef DefSelection{def = selectedDef, node = Just sel}) -> - unless (selectedDef == foo && getID sel == getID m) - $ assertFailure "expected selection to point at the recursive reference" + unless (selectedDef == foo && getID sel == getID m) $ + assertFailure "expected selection to point at the recursive reference" _ -> assertFailure "expected the selection to point at some node" _ -> assertFailure "expected foo" _ -> assertFailure "definition not found" @@ -1607,10 +1594,10 @@ unit_sh_lost_id = e <- hole $ hole (gvar foo) `ann` (tEmptyHole `tfun` tEmptyHole) t <- tEmptyHole `tapp` tEmptyHole let m = - Module n mempty - $ Map.singleton "foo" - $ DefAST - $ ASTDef e t + Module n mempty $ + Map.singleton "foo" $ + DefAST $ + ASTDef e t pure $ p & #progModules %~ (m :) -- * Utilities @@ -1627,22 +1614,21 @@ defaultEmptyProg = do otherType <- tEmptyHole let mainDef = ASTDef mainExpr mainType otherDef = ASTDef otherExpr otherType - in pure - $ newEmptyProg' + in pure $ + newEmptyProg' { progSelection = - Just - . SelectionDef - $ DefSelection (gvn "main") - $ Just - NodeSelection - { nodeType = BodyNode - , meta = Left (Meta 1 Nothing Nothing) - } + Just . SelectionDef $ + DefSelection (gvn "main") $ + Just + NodeSelection + { nodeType = BodyNode + , meta = Left (Meta 1 Nothing Nothing) + } } - & #progModules - % _head - % #moduleDefs - .~ Map.fromList [("main", DefAST mainDef), ("other", DefAST otherDef)] + & #progModules + % _head + % #moduleDefs + .~ Map.fromList [("main", DefAST mainDef), ("other", DefAST otherDef)] unit_good_defaultEmptyProg :: Assertion unit_good_defaultEmptyProg = checkProgWellFormed defaultEmptyProg @@ -1665,16 +1651,10 @@ defaultFullProg = do renamed = transformBi (const m) [builtinModule', primitiveModule'] renamedTypes = foldOf (folded % #moduleTypes) renamed renamedDefs = foldOf (folded % #moduleDefs) renamed - pure - $ p - & #progModules - % _head - % #moduleTypes - %~ (renamedTypes <>) - & #progModules - % _head - % #moduleDefs - %~ (renamedDefs <>) + pure $ + p + & #progModules % _head % #moduleTypes %~ (renamedTypes <>) + & #progModules % _head % #moduleDefs %~ (renamedDefs <>) findTypeDef :: TyConName -> Prog -> IO (ASTTypeDef () ()) findTypeDef d p = maybe (assertFailure "couldn't find typedef") pure $ (typeDefAST <=< Map.lookup d) $ foldMap' moduleTypesQualified $ progModules p @@ -1695,19 +1675,17 @@ defaultProgEditableTypeDefs ds = do fieldsB <- sequence [(tcon tT `tapp` tvar "b") `tapp` tvar "a", tvar "b"] ka <- ktype kb <- ktype - pure - $ TypeDefAST + pure $ + TypeDefAST ASTTypeDef { astTypeDefParameters = [(pA, ka), (pB, kb)] , astTypeDefConstructors = [ValCon cA fieldsA, ValCon cB fieldsB] , astTypeDefNameHints = [] } - pure - $ p - & (#progModules % _head % #moduleTypes) - %~ (Map.singleton (baseName tT) td <>) - & (#progModules % _head % #moduleDefs) - %~ (Map.fromList (second DefAST <$> ds') <>) + pure $ + p + & (#progModules % _head % #moduleTypes) %~ (Map.singleton (baseName tT) td <>) + & (#progModules % _head % #moduleDefs) %~ (Map.fromList (second DefAST <$> ds') <>) tT :: TyConName tT = tcn "T" diff --git a/primer/test/Tests/Database.hs b/primer/test/Tests/Database.hs index 238c53a95..d253bc92f 100644 --- a/primer/test/Tests/Database.hs +++ b/primer/test/Tests/Database.hs @@ -100,9 +100,8 @@ test_invalid = [ testCase "unsafe" $ case mkSessionName t of Nothing -> pure () Just _ -> assertFailure "name is valid" - , testCase "safe" - $ safeMkSessionName t - @?= defaultSessionName + , testCase "safe" $ + safeMkSessionName t @?= defaultSessionName ] testSessionName :: TestName -> Text -> Text -> TestTree @@ -112,9 +111,8 @@ testSessionName testName t expected = [ testCase "unsafe" $ case mkSessionName t of Nothing -> assertFailure "name is invalid" Just sn -> fromSessionName sn @?= expected - , testCase "safe" - $ fromSessionName (safeMkSessionName t) - @?= expected + , testCase "safe" $ + fromSessionName (safeMkSessionName t) @?= expected ] -- | A "fail" database that fails on every operation. diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs index 9251883a8..434629a8c 100644 --- a/primer/test/Tests/Eval.hs +++ b/primer/test/Tests/Eval.hs @@ -108,10 +108,10 @@ import Tests.Gen.Core.Typed (checkTest) runTryReduce :: HasCallStack => TypeDefMap -> DefMap -> Cxt -> (Expr, ID) -> IO (Either EvalError (Expr, EvalDetail)) runTryReduce tys globals locals (expr, i) = do let (r, logs) = - evalTestM i - $ runPureLogT - $ runExceptT - $ tryReduceExpr @EvalLog NoAvoidShadowing tys globals locals Syn expr + evalTestM i $ + runPureLogT $ + runExceptT $ + tryReduceExpr @EvalLog NoAvoidShadowing tys globals locals Syn expr assertNoSevereLogs logs pure r @@ -119,10 +119,10 @@ runTryReduce tys globals locals (expr, i) = do runTryReduceType :: HasCallStack => DefMap -> Cxt -> (Type, ID) -> IO (Either EvalError (Type, EvalDetail)) runTryReduceType globals locals (ty, i) = do let (r, logs) = - evalTestM i - $ runPureLogT - $ runExceptT - $ tryReduceType @EvalLog NoAvoidShadowing globals locals ty + evalTestM i $ + runPureLogT $ + runExceptT $ + tryReduceType @EvalLog NoAvoidShadowing globals locals ty assertNoSevereLogs logs pure r @@ -379,8 +379,8 @@ unit_tryReduce_case_1 = do unit_tryReduce_case_2 :: Assertion unit_tryReduce_case_2 = do let (expr, i) = - create - $ case_ + create $ + case_ (con' ["M"] "C" [lam "x" (lvar "x"), lvar "y", lvar "z"] `ann` tcon' ["M"] "T") [ branch' (["M"], "B") [("b", Nothing)] (con0' ["M"] "D") , branch' (["M"], "C") [("c", Nothing), ("d", Nothing), ("e", Nothing)] (con0' ["M"] "E") @@ -389,19 +389,19 @@ unit_tryReduce_case_2 = do y = unsafeMkGlobalName (["M"], "Y") z = unsafeMkGlobalName (["M"], "Z") tydef = - Map.singleton (unsafeMkGlobalName (["M"], "T")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [] - , astTypeDefConstructors = - [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] - , ValCon (unsafeMkGlobalName (["M"], "C")) [TCon () x, TCon () y, TCon () z] - ] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "T")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [] + , astTypeDefConstructors = + [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] + , ValCon (unsafeMkGlobalName (["M"], "C")) [TCon () x, TCon () y, TCon () z] + ] + , astTypeDefNameHints = [] + } expectedResult = - create' - $ let_ + create' $ + let_ "c" (lam "x" (lvar "x") `ann` tcon x) ( let_ @@ -432,8 +432,8 @@ unit_tryReduce_case_2 = do unit_tryReduce_case_3 :: Assertion unit_tryReduce_case_3 = do let (expr, i) = - create - $ case_ + create $ + case_ ( con' ["M"] "C" [con0' ["M"] "E"] `ann` (tcon' ["M"] "T" `tapp` tcon' ["M"] "D") ) @@ -441,16 +441,16 @@ unit_tryReduce_case_3 = do , branch' (["M"], "C") [("c", Nothing)] (con0' ["M"] "F") ] tydef = - Map.singleton (unsafeMkGlobalName (["M"], "T")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [("a", KType ())] - , astTypeDefConstructors = - [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] - , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] - ] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "T")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [("a", KType ())] + , astTypeDefConstructors = + [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] + , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] + ] + , astTypeDefNameHints = [] + } expectedResult = create' $ let_ "c" (con0' ["M"] "E" `ann` tlet "a" (tcon' ["M"] "D") (tvar "a" `tfun` tvar "a")) (con0' ["M"] "F") result <- runTryReduce tydef mempty mempty (expr, i) case result of @@ -471,24 +471,24 @@ unit_tryReduce_case_3 = do unit_tryReduce_case_fallback_1 :: Assertion unit_tryReduce_case_fallback_1 = do let (expr, i) = - create - $ caseFB_ + create $ + caseFB_ ( con' ["M"] "C" [con0' ["M"] "E"] `ann` (tcon' ["M"] "T" `tapp` tcon' ["M"] "D") ) [branch' (["M"], "B") [("b", Nothing)] (con0' ["M"] "D")] (con0' ["M"] "F") tydef = - Map.singleton (unsafeMkGlobalName (["M"], "T")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [("a", KType ())] - , astTypeDefConstructors = - [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] - , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] - ] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "T")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [("a", KType ())] + , astTypeDefConstructors = + [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] + , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] + ] + , astTypeDefNameHints = [] + } expectedResult = create' (con0' ["M"] "F") result <- runTryReduce tydef mempty mempty (expr, i) case result of @@ -509,24 +509,24 @@ unit_tryReduce_case_fallback_1 = do unit_tryReduce_case_fallback_2 :: Assertion unit_tryReduce_case_fallback_2 = do let (expr, i) = - create - $ caseFB_ + create $ + caseFB_ ( con' ["M"] "C" [con0' ["M"] "E"] `ann` (tcon' ["M"] "T" `tapp` tcon' ["M"] "D") ) [branch' (["M"], "C") [("c", Nothing)] (con0' ["M"] "F")] (con0' ["M"] "D") tydef = - Map.singleton (unsafeMkGlobalName (["M"], "T")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [("a", KType ())] - , astTypeDefConstructors = - [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] - , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] - ] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "T")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [("a", KType ())] + , astTypeDefConstructors = + [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] + , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] + ] + , astTypeDefNameHints = [] + } expectedResult = create' $ let_ "c" (con0' ["M"] "E" `ann` tlet "a" (tcon' ["M"] "D") (tvar "a" `tfun` tvar "a")) (con0' ["M"] "F") result <- runTryReduce tydef mempty mempty (expr, i) case result of @@ -547,24 +547,24 @@ unit_tryReduce_case_fallback_2 = do unit_tryReduce_case_fallback_3 :: Assertion unit_tryReduce_case_fallback_3 = do let (expr, i) = - create - $ caseFB_ + create $ + caseFB_ ( con' ["M"] "C" [con0' ["M"] "E"] `ann` (tcon' ["M"] "T" `tapp` tcon' ["M"] "D") ) [] (con0' ["M"] "D") tydef = - Map.singleton (unsafeMkGlobalName (["M"], "T")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [("a", KType ())] - , astTypeDefConstructors = - [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] - , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] - ] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "T")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [("a", KType ())] + , astTypeDefConstructors = + [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] + , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] + ] + , astTypeDefNameHints = [] + } expectedResult = create' $ con0' ["M"] "D" result <- runTryReduce tydef mempty mempty (expr, i) case result of @@ -580,21 +580,21 @@ unit_tryReduce_case_fallback_3 = do unit_tryReduce_case_name_clash :: Assertion unit_tryReduce_case_name_clash = do let (expr, i) = - create - $ case_ + create $ + case_ (con' ["M"] "C" [emptyHole, lvar "x"] `ann` tcon' ["M"] "T") [branch' (["M"], "C") [("x", Nothing), ("y", Nothing)] emptyHole] tydef = - Map.singleton (unsafeMkGlobalName (["M"], "T")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [] - , astTypeDefConstructors = [ValCon (unsafeMkGlobalName (["M"], "C")) [TEmptyHole (), TEmptyHole ()]] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "T")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon (unsafeMkGlobalName (["M"], "C")) [TEmptyHole (), TEmptyHole ()]] + , astTypeDefNameHints = [] + } expectedResult = - create' - $ case_ + create' $ + case_ (con' ["M"] "C" [emptyHole, lvar "x"] `ann` tcon' ["M"] "T") [branch' (["M"], "C") [("a9", Nothing), ("y", Nothing)] $ let_ "x" (lvar "a9") emptyHole] result <- runTryReduce tydef mempty mempty (expr, i) @@ -622,22 +622,22 @@ unit_tryReduce_case_scrutinee_not_redex = do unit_tryReduce_case_prim_1 :: Assertion unit_tryReduce_case_prim_1 = do let (expr, i) = - create - $ caseFB_ + create $ + caseFB_ (char 'b') [branchPrim (PrimChar 'b') (con0' ["M"] "F")] (con0' ["M"] "D") tydef = - Map.singleton (unsafeMkGlobalName (["M"], "T")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [("a", KType ())] - , astTypeDefConstructors = - [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] - , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] - ] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "T")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [("a", KType ())] + , astTypeDefConstructors = + [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] + , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] + ] + , astTypeDefNameHints = [] + } expectedResult = create' $ con0' ["M"] "F" result <- runTryReduce tydef mempty mempty (expr, i) case result of @@ -658,22 +658,22 @@ unit_tryReduce_case_prim_1 = do unit_tryReduce_case_prim_2 :: Assertion unit_tryReduce_case_prim_2 = do let (expr, i) = - create - $ caseFB_ + create $ + caseFB_ (char 'b') [branchPrim (PrimChar 'c') (con0' ["M"] "F")] -- not b (con0' ["M"] "D") tydef = - Map.singleton (unsafeMkGlobalName (["M"], "T")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [("a", KType ())] - , astTypeDefConstructors = - [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] - , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] - ] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "T")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [("a", KType ())] + , astTypeDefConstructors = + [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] + , ValCon (unsafeMkGlobalName (["M"], "C")) [TFun () (TVar () "a") (TVar () "a")] + ] + , astTypeDefNameHints = [] + } expectedResult = create' $ con0' ["M"] "D" result <- runTryReduce tydef mempty mempty (expr, i) case result of @@ -694,14 +694,14 @@ unit_tryReduce_case_prim_2 = do unit_tryReduce_prim :: Assertion unit_tryReduce_prim = do let ((expr, expectedResult, prims), i) = - create - $ (,,) - <$> pfun EqChar - `app` char 'a' - `app` char 'a' - <*> con0 cTrue - `ann` tcon tBool - <*> primDefs + create $ + (,,) + <$> pfun EqChar + `app` char 'a' + `app` char 'a' + <*> con0 cTrue + `ann` tcon tBool + <*> primDefs result <- runTryReduce tydefs prims mempty (expr, i) case result of Right (expr', ApplyPrimFun detail) -> do @@ -716,32 +716,32 @@ unit_tryReduce_prim = do unit_tryReduce_prim_fail_unsaturated :: Assertion unit_tryReduce_prim_fail_unsaturated = do let ((expr, prims), i) = - create - $ (,) - <$> pfun EqChar - `app` char 'a' - <*> primDefs + create $ + (,) + <$> pfun EqChar + `app` char 'a' + <*> primDefs result <- runTryReduce tydefs prims mempty (expr, i) result @?= Left NotRedex unit_tryReduce_prim_fail_unreduced_args :: Assertion unit_tryReduce_prim_fail_unreduced_args = do let ((expr, prims), i) = - create - $ (,) - <$> pfun EqChar - `app` char 'a' - `app` (pfun ToUpper `app` char 'a') - <*> primDefs + create $ + (,) + <$> pfun EqChar + `app` char 'a' + `app` (pfun ToUpper `app` char 'a') + <*> primDefs result <- runTryReduce tydefs prims mempty (expr, i) result @?= Left NotRedex runStep :: ID -> TypeDefMap -> DefMap -> (Expr, ID) -> IO (Either EvalError (Expr, EvalDetail)) runStep i' tys globals (e, i) = do let (r, logs) = - evalTestM i' - $ runPureLogT - $ step @EvalLog NoAvoidShadowing tys globals e Syn i + evalTestM i' $ + runPureLogT $ + step @EvalLog NoAvoidShadowing tys globals e Syn i assertNoSevereLogs logs pure r @@ -972,21 +972,21 @@ tydefs :: TypeDefMap tydefs = c <> d where c = - Map.singleton (unsafeMkGlobalName (["M"], "C")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [] - , astTypeDefConstructors = [ValCon (unsafeMkGlobalName (["M"], "C")) []] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "C")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon (unsafeMkGlobalName (["M"], "C")) []] + , astTypeDefNameHints = [] + } d = - Map.singleton (unsafeMkGlobalName (["M"], "D")) - $ TypeDefAST - $ ASTTypeDef - { astTypeDefParameters = [] - , astTypeDefConstructors = [ValCon (unsafeMkGlobalName (["M"], "D")) []] - , astTypeDefNameHints = [] - } + Map.singleton (unsafeMkGlobalName (["M"], "D")) $ + TypeDefAST $ + ASTTypeDef + { astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon (unsafeMkGlobalName (["M"], "D")) []] + , astTypeDefNameHints = [] + } unit_redexes_con :: Assertion unit_redexes_con = redexesOf (con0' ["M"] "C") <@?=> mempty @@ -1361,8 +1361,8 @@ unit_eval_modules = importModules [primitiveModule', builtinModule'] foo <- pfun ToUpper `app` char 'a' EvalResp{evalRespExpr = e} <- - readerToState - $ handleEvalRequest + readerToState $ + handleEvalRequest EvalReq{evalReqExpr = foo, evalReqRedex = getID foo} expect <- char 'A' pure $ e ~= expect @@ -1382,8 +1382,8 @@ unit_eval_modules_scrutinize_imported_type = (con0 cTrue `ann` tcon tBool) [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] EvalResp{evalRespExpr = e} <- - readerToState - $ handleEvalRequest + readerToState $ + handleEvalRequest EvalReq{evalReqExpr = foo, evalReqRedex = getID foo} expect <- con0 cFalse pure $ e ~= expect @@ -1394,8 +1394,8 @@ unit_eval_modules_scrutinize_imported_type = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = Map.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1407,26 +1407,25 @@ unit_eval_modules_scrutinize_imported_type = tasty_type_preservation :: Property tasty_type_preservation = let testModules = [builtinModule, primitiveModule] - in withTests 200 - $ withDiscards 2000 - $ propertyWT testModules - $ do - let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules - as <- forAllT $ Gen.element enumerate - tds <- asks typeDefs - (dir, t, ty) <- genDirTm - rs <- failWhenSevereLogs $ redexes @EvalLog as tds globs dir t - when (null rs) discard - r <- forAllT $ Gen.element rs - s <- failWhenSevereLogs $ step @EvalLog as tds globs t dir r - case s of - Left err -> annotateShow err >> failure - Right (s', _) -> - if hasTypeLets s' - then label "skipped due to LetType" >> success - else do - s'' <- checkTest ty s' - forgetMetadata s' === forgetMetadata s'' -- check no smart holes happened + in withTests 200 $ + withDiscards 2000 $ + propertyWT testModules $ do + let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules + as <- forAllT $ Gen.element enumerate + tds <- asks typeDefs + (dir, t, ty) <- genDirTm + rs <- failWhenSevereLogs $ redexes @EvalLog as tds globs dir t + when (null rs) discard + r <- forAllT $ Gen.element rs + s <- failWhenSevereLogs $ step @EvalLog as tds globs t dir r + case s of + Left err -> annotateShow err >> failure + Right (s', _) -> + if hasTypeLets s' + then label "skipped due to LetType" >> success + else do + s'' <- checkTest ty s' + forgetMetadata s' === forgetMetadata s'' -- check no smart holes happened -- | Reductions do not interfere with each other -- if @i,j ∈ redexes e@ (and @i /= j@), and @e@ reduces to @e'@ via redex @i@ @@ -1442,36 +1441,35 @@ tasty_type_preservation = tasty_redex_independent :: Property tasty_redex_independent = let testModules = [builtinModule, primitiveModule] - in withTests 200 - $ withDiscards 2000 - $ propertyWT testModules - $ do - let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules - as <- forAllT $ Gen.element enumerate - tds <- asks typeDefs - (dir, t, _) <- genDirTm - annotateShow dir - annotateShow t - rs <- failWhenSevereLogs $ redexes @EvalLog as tds globs dir t - when (length rs <= 1) discard - i <- forAllT $ Gen.element rs - j <- forAllT $ Gen.element $ delete i rs - s <- failWhenSevereLogs $ step @EvalLog as tds globs t dir i - case s of - Left err -> annotateShow err >> failure - Right (s', siDetails) -> do - annotateShow s' - if elemOf exprIDs j s' - then do - sj <- failWhenSevereLogs $ step @EvalLog as tds globs t dir j - case (sj, siDetails) of - (Right (_, BindRename{}), _) -> success - (_, PushLetDown{}) -> success - (_, PushLetDownTy{}) -> success - (Right (_, PushLetDown{}), CaseReduction{}) -> success - (Right (_, PushLetDown{}), CaseReductionTrivial{}) -> success - (Right (_, PushLetDown{}), RemoveAnn{}) -> success - (Right (_, PushLetDown{}), LetRemoval{}) -> success - (Right (_, PushLetDownTy{}), TLetRemoval{}) -> success - _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog as tds globs dir s') - else success + in withTests 200 $ + withDiscards 2000 $ + propertyWT testModules $ do + let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules + as <- forAllT $ Gen.element enumerate + tds <- asks typeDefs + (dir, t, _) <- genDirTm + annotateShow dir + annotateShow t + rs <- failWhenSevereLogs $ redexes @EvalLog as tds globs dir t + when (length rs <= 1) discard + i <- forAllT $ Gen.element rs + j <- forAllT $ Gen.element $ delete i rs + s <- failWhenSevereLogs $ step @EvalLog as tds globs t dir i + case s of + Left err -> annotateShow err >> failure + Right (s', siDetails) -> do + annotateShow s' + if elemOf exprIDs j s' + then do + sj <- failWhenSevereLogs $ step @EvalLog as tds globs t dir j + case (sj, siDetails) of + (Right (_, BindRename{}), _) -> success + (_, PushLetDown{}) -> success + (_, PushLetDownTy{}) -> success + (Right (_, PushLetDown{}), CaseReduction{}) -> success + (Right (_, PushLetDown{}), CaseReductionTrivial{}) -> success + (Right (_, PushLetDown{}), RemoveAnn{}) -> success + (Right (_, PushLetDown{}), LetRemoval{}) -> success + (Right (_, PushLetDownTy{}), TLetRemoval{}) -> success + _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog as tds globs dir s') + else success diff --git a/primer/test/Tests/Eval/Utils.hs b/primer/test/Tests/Eval/Utils.hs index b667b26cb..25f268253 100644 --- a/primer/test/Tests/Eval/Utils.hs +++ b/primer/test/Tests/Eval/Utils.hs @@ -73,8 +73,8 @@ testModule = { moduleName = ModuleName ["M"] , moduleTypes = mempty , moduleDefs = - Map.singleton "idChar" - $ DefAST + Map.singleton "idChar" $ + DefAST ASTDef { astDefType = ty , astDefExpr = expr @@ -97,15 +97,15 @@ x ~~= y = forgetTypeMetadata x @?= forgetTypeMetadata y -- or a 'TLet' in an embedded type. hasTypeLets :: (Data a, Data b, Data c) => Expr' a b c -> Bool hasTypeLets e = - not - $ null [() | LetType{} <- universe e] - && null [() | TLet{} <- universeBi @_ @Type e] + not $ + null [() | LetType{} <- universe e] + && null [() | TLet{} <- universeBi @_ @Type e] -- | Does this expression have any holes? hasHoles :: Expr -> Bool hasHoles e = - not - $ null [() | Hole{} <- universe e] - && null [() | EmptyHole{} <- universe e] - && null [() | THole{} <- universeBi @_ @Type e] - && null [() | TEmptyHole{} <- universeBi @_ @Type e] + not $ + null [() | Hole{} <- universe e] + && null [() | EmptyHole{} <- universe e] + && null [() | THole{} <- universeBi @_ @Type e] + && null [() | TEmptyHole{} <- universeBi @_ @Type e] diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs index ce087dfe9..8c8e6057b 100644 --- a/primer/test/Tests/EvalFullInterp.hs +++ b/primer/test/Tests/EvalFullInterp.hs @@ -283,8 +283,8 @@ unit_case_let_capture = let (expr, expected) = create2 $ do let l = let_ "x" (lvar "y") e0 <- - l - $ case_ + l $ + case_ emptyHole [ branch' (["M"], "C") [("x", Nothing)] (lvar "x") , branch' (["M"], "D") [("y", Nothing)] (lvar "x") @@ -376,13 +376,13 @@ unit_closed_single_lets :: Assertion unit_closed_single_lets = let (expr, expected) = create2 $ do e0 <- - let_ "x" (con0 cFalse) - $ let_ "y" (con0 cTrue) - $ con - cMakePair - [ lvar "x" - , lvar "y" - ] + let_ "x" (con0 cFalse) $ + let_ "y" (con0 cTrue) $ + con + cMakePair + [ lvar "x" + , lvar "y" + ] e4 <- con cMakePair @@ -432,10 +432,8 @@ unit_let_self_capture = -- implementation is sufficiently different that it doesn't make sense -- to combine them. tasty_type_preservation :: Property -tasty_type_preservation = withTests 1000 - $ withDiscards 2000 - $ propertyWT testModules - $ do +tasty_type_preservation = withTests 1000 $ + withDiscards 2000 . propertyWT testModules $ do let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules tds <- asks typeDefs (dir, forgetMetadata -> t, ty) <- genDirTm @@ -452,10 +450,8 @@ tasty_type_preservation = withTests 1000 s' === forgetMetadata s'' -- check no smart holes happened tasty_two_interp_agree :: Property -tasty_two_interp_agree = withTests 1000 - $ withDiscards 2000 - $ propertyWT testModules - $ do +tasty_two_interp_agree = withTests 1000 $ + withDiscards 2000 . propertyWT testModules $ do let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules tds <- asks typeDefs (dir, t, _ty) <- genDirTm @@ -500,8 +496,8 @@ tasty_prim_hex_nat = withTests 20 . property $ do n <- forAllT $ Gen.integral $ Range.constant 0 50 let ne = nat n (dir, forgetMetadata -> e, forgetMetadata -> r, prims) = - create' - $ if n <= 15 + create' $ + if n <= 15 then (Chk,,,) <$> case_ @@ -524,9 +520,9 @@ tasty_prim_hex_nat = withTests 20 . property $ do else (Syn,,,) <$> pfun NatToHex - `app` ne + `app` ne <*> con cNothing [] - `ann` (tcon tMaybe `tapp` tcon tChar) + `ann` (tcon tMaybe `tapp` tcon tChar) <*> primDefs s <- evalIO $ evalFullTest builtinTypes prims dir e s === Right r @@ -550,11 +546,11 @@ unit_prim_char_eq_2 = unit_prim_char_partial :: Assertion unit_prim_char_partial = let (forgetMetadata -> e, prims) = - create' - $ (,) - <$> pfun EqChar - `app` char 'a' - <*> primDefs + create' $ + (,) + <$> pfun EqChar + `app` char 'a' + <*> primDefs in do s <- evalFullTest mempty prims Syn e s @?= Right e @@ -939,8 +935,8 @@ unit_handleEvalInterpRequest_modules = importModules [primitiveModule', builtinModule'] foo <- pfun ToUpper `app` char 'a' (EvalInterpRespNormal e) <- - readerToState - $ handleEvalInterpRequest + readerToState $ + handleEvalInterpRequest EvalInterpReq { expr = foo , dir = Chk @@ -961,8 +957,8 @@ unit_handleEvalBoundedInterpRequest_modules = importModules [primitiveModule', builtinModule'] foo <- pfun ToUpper `app` char 'a' resp <- - readerToState - $ handleEvalBoundedInterpRequest + readerToState $ + handleEvalBoundedInterpRequest EvalBoundedInterpReq { expr = foo , dir = Chk @@ -1039,12 +1035,12 @@ unit_handleEvalInterpRequest_modules_scrutinize_imported_type = (con0 cTrue `ann` tcon tBool) [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] (EvalInterpRespNormal e) <- - readerToState - $ handleEvalInterpRequest - $ EvalInterpReq - { expr = foo - , dir = Chk - } + readerToState $ + handleEvalInterpRequest $ + EvalInterpReq + { expr = foo + , dir = Chk + } expect <- con0 cFalse pure $ e ~= expect a = newEmptyApp @@ -1054,8 +1050,8 @@ unit_handleEvalInterpRequest_modules_scrutinize_imported_type = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = M.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1073,13 +1069,13 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = (con0 cTrue `ann` tcon tBool) [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] resp <- - readerToState - $ handleEvalBoundedInterpRequest - $ EvalBoundedInterpReq - { expr = foo - , dir = Chk - , timeout = MicroSec 10_000 - } + readerToState $ + handleEvalBoundedInterpRequest $ + EvalBoundedInterpReq + { expr = foo + , dir = Chk + , timeout = MicroSec 10_000 + } expect <- con0 cFalse pure $ case resp of EvalBoundedInterpRespFailed err -> assertFailure $ show err @@ -1091,8 +1087,8 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = M.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1165,13 +1161,13 @@ unit_handleEvalBoundedInterpRequest_timeout = importModules [m'] e <- letrec "x" (lvar "x") (tcon tBool) (lvar "x") resp <- - readerToState - $ handleEvalBoundedInterpRequest - $ EvalBoundedInterpReq - { expr = e - , dir = Chk - , timeout = MicroSec 10_000 - } + readerToState $ + handleEvalBoundedInterpRequest $ + EvalBoundedInterpReq + { expr = e + , dir = Chk + , timeout = MicroSec 10_000 + } pure $ case resp of EvalBoundedInterpRespFailed err -> err @?= Timeout EvalBoundedInterpRespNormal _ -> assertFailure "expected timeout" @@ -1182,8 +1178,8 @@ unit_handleEvalBoundedInterpRequest_timeout = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = M.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1198,13 +1194,13 @@ unit_handleEvalBoundedInterpRequest_missing_branch = importModules [m'] e <- case_ (con0 cTrue `ann` tcon tBool) [branch cFalse [] emptyHole] resp <- - readerToState - $ handleEvalBoundedInterpRequest - $ EvalBoundedInterpReq - { expr = e - , dir = Chk - , timeout = MicroSec 10_000 - } + readerToState $ + handleEvalBoundedInterpRequest $ + EvalBoundedInterpReq + { expr = e + , dir = Chk + , timeout = MicroSec 10_000 + } let expect = NoBranch (Left cTrue) [PatCon cFalse] pure $ case resp of EvalBoundedInterpRespFailed err -> err @?= expect @@ -1216,8 +1212,8 @@ unit_handleEvalBoundedInterpRequest_missing_branch = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = M.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1246,8 +1242,8 @@ unit_handleEvalInterpRequest_missing_branch = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = M.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1262,13 +1258,13 @@ unit_handleEvalBoundedInterpRequest_missing_branch_prim = importModules [m'] e <- case_ (char 'a' `ann` tcon tChar) [branchPrim (PrimChar 'b') emptyHole] resp <- - readerToState - $ handleEvalBoundedInterpRequest - $ EvalBoundedInterpReq - { expr = e - , dir = Chk - , timeout = MicroSec 10_000 - } + readerToState $ + handleEvalBoundedInterpRequest $ + EvalBoundedInterpReq + { expr = e + , dir = Chk + , timeout = MicroSec 10_000 + } let expect = NoBranch (Right (PrimChar 'a')) [PatPrim (PrimChar 'b')] pure $ case resp of EvalBoundedInterpRespFailed err -> err @?= expect @@ -1280,8 +1276,8 @@ unit_handleEvalBoundedInterpRequest_missing_branch_prim = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = M.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1310,8 +1306,8 @@ unit_handleEvalInterpRequest_missing_branch_prim = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = M.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1342,8 +1338,8 @@ unit_case_prim = e2 = create1 $ caseFB_ (char 'a') [branchPrim (PrimChar 'a') $ con0 cFalse] (con0 cTrue) expect2 = create1 $ con0 cFalse e3 = - create1 - $ caseFB_ + create1 $ + caseFB_ (char 'b') [ branchPrim (PrimChar 'a') $ con0 cTrue , branchPrim (PrimChar 'b') $ con0 cFalse @@ -1351,8 +1347,8 @@ unit_case_prim = (con0 cTrue) expect3 = create1 $ con0 cFalse e4 = - create1 - $ caseFB_ + create1 $ + caseFB_ ( (lam "x" (lvar "x") `ann` (tcon tChar `tfun` tcon tChar)) `app` char 'a' ) @@ -1393,12 +1389,12 @@ evalFullTest = evalFullTest' (MicroSec (-1)) -- negative time means wait forever unaryPrimTest :: (HasCallStack) => PrimDef -> S Expr -> S Expr -> Assertion unaryPrimTest f x y = let (forgetMetadata -> e, forgetMetadata -> r, prims) = - create' - $ (,,) - <$> pfun f - `app` x - <*> y - <*> primDefs + create' $ + (,,) + <$> pfun f + `app` x + <*> y + <*> primDefs in do s <- evalFullTest mempty prims Syn e s @?= Right r @@ -1406,13 +1402,13 @@ unaryPrimTest f x y = binaryPrimTest :: (HasCallStack) => PrimDef -> S Expr -> S Expr -> S Expr -> Assertion binaryPrimTest f x y z = let (forgetMetadata -> e, forgetMetadata -> r, prims) = - create' - $ (,,) - <$> pfun f - `app` x - `app` y - <*> z - <*> primDefs + create' $ + (,,) + <$> pfun f + `app` x + `app` y + <*> z + <*> primDefs in do s <- evalFullTest mempty prims Syn e s @?= Right r diff --git a/primer/test/Tests/EvalFullStep.hs b/primer/test/Tests/EvalFullStep.hs index 1a377956d..aa2d8942b 100644 --- a/primer/test/Tests/EvalFullStep.hs +++ b/primer/test/Tests/EvalFullStep.hs @@ -400,22 +400,22 @@ unit_case_let_capture = let rnx = let_ "x" (lvar w) let rny = let_ "y" (lvar z) e0 <- - l - $ case_ + l $ + case_ emptyHole [ branch' (["M"], "C") [("x", Nothing)] (lvar "x") , branch' (["M"], "D") [("y", Nothing)] (lvar "x") ] e1 <- - l - $ case_ + l $ + case_ emptyHole [ branch' (["M"], "C") [(w, Nothing)] (rnx $ lvar "x") , branch' (["M"], "D") [("y", Nothing)] (lvar "x") ] e2 <- - l - $ case_ + l $ + case_ emptyHole [ branch' (["M"], "C") [(w, Nothing)] (rnx $ lvar "x") , branch' (["M"], "D") [(z, Nothing)] (rny $ lvar "x") @@ -648,16 +648,16 @@ unit_closed_single_lets :: Assertion unit_closed_single_lets = let ((expr, expected), maxID) = create $ do e0 <- - let_ "x" (con0 cFalse) - $ let_ "y" (con0 cTrue) - $ con - cMakePair - [ lvar "x" - , lvar "y" - ] + let_ "x" (con0 cFalse) $ + let_ "y" (con0 cTrue) $ + con + cMakePair + [ lvar "x" + , lvar "y" + ] e1 <- - let_ "x" (con0 cFalse) - $ con + let_ "x" (con0 cFalse) $ + con cMakePair [ lvar "x" , let_ "y" (con0 cTrue) $ lvar "y" @@ -701,13 +701,13 @@ unit_closed_letrec_binder :: Assertion unit_closed_letrec_binder = let ((expr, expected), maxID) = create $ do e0 <- - letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) - $ lam "y" - $ lvar "x" + letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ + lam "y" $ + lvar "x" e1 <- - lam "y" - $ letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) - $ lvar "x" + lam "y" $ + letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ + lvar "x" pure (e0, map (Left . TimedOut) [e0, e1] ++ [Right e1]) test (n, expect) = do r <- evalFullTestClosed GroupedLets maxID mempty mempty n Syn expr @@ -767,9 +767,8 @@ unit_closed_subst = do -- because the interpreter doesn't avoid evaluating under binders -- (for now, at least). tasty_open_closed_agree_base_types :: Property -tasty_open_closed_agree_base_types = withDiscards 1000 - $ propertyWT testModules - $ do +tasty_open_closed_agree_base_types = withDiscards 1000 $ + propertyWT testModules $ do let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False} let optsR = RunRedexOptions{pushAndElide = True} ty <- forAllT $ Gen.element @[] [tBool, tNat, tInt] @@ -800,9 +799,8 @@ tasty_open_closed_agree_base_types = withDiscards 1000 -- | Resuming evaluation is the same as running it for longer in the first place tasty_resume :: Property -tasty_resume = withDiscards 2000 - $ propertyWT testModules - $ do +tasty_resume = withDiscards 2000 $ + propertyWT testModules $ do (dir, t, _) <- genDirTm testModules' <- sequence testModules resumeTest testModules' dir t @@ -876,25 +874,25 @@ unit_type_preservation_case_regression_tm :: Assertion unit_type_preservation_case_regression_tm = let ((expr, expected1, expected2), maxID) = create $ do e <- - lam "x" - $ case_ + lam "x" $ + case_ ( con cMakePair [emptyHole, lvar "x"] `ann` ((tcon tPair `tapp` tcon tNat) `tapp` tcon tBool) ) [branch cMakePair [("x", Nothing), ("y", Nothing)] emptyHole] let x' = "a46" -- NB fragile name expect1 <- - lam "x" - $ case_ + lam "x" $ + case_ ( con cMakePair [emptyHole, lvar "x"] `ann` ((tcon tPair `tapp` tcon tNat) `tapp` tcon tBool) ) [branch cMakePair [(x', Nothing), ("y", Nothing)] $ let_ "x" (lvar x') emptyHole] expect2 <- - lam "x" - $ let_ x' (emptyHole `ann` tlet "a" (tcon tNat) (tvar "a")) - $ let_ "y" (lvar "x" `ann` tlet "b" (tcon tBool) (tvar "b")) - $ let_ "x" (lvar x') emptyHole + lam "x" $ + let_ x' (emptyHole `ann` tlet "a" (tcon tNat) (tvar "a")) $ + let_ "y" (lvar "x" `ann` tlet "b" (tcon tBool) (tvar "b")) $ + let_ "x" (lvar x') emptyHole pure (e, expect1, expect2) in do s1 <- evalFullTest maxID builtinTypes mempty 1 Chk expr @@ -916,25 +914,25 @@ unit_type_preservation_case_regression_ty :: Assertion unit_type_preservation_case_regression_ty = let ((expr, expected1, expected2), maxID) = create $ do e <- - lAM "x" - $ case_ + lAM "x" $ + case_ ( con cMakePair [emptyHole, emptyHole] `ann` (tcon tPair `tapp` tEmptyHole `tapp` tvar "x") ) [branch cMakePair [("x", Nothing), ("y", Nothing)] emptyHole] let x' = "a46" -- NB fragile name expect1 <- - lAM "x" - $ case_ + lAM "x" $ + case_ ( con cMakePair [emptyHole, emptyHole] `ann` (tcon tPair `tapp` tEmptyHole `tapp` tvar "x") ) [branch cMakePair [(x', Nothing), ("y", Nothing)] $ let_ "x" (lvar x') emptyHole] expect2 <- - lAM "x" - $ let_ x' (emptyHole `ann` tlet "a" tEmptyHole (tvar "a")) - $ let_ "y" (emptyHole `ann` tlet "b" (tvar "x") (tvar "b")) - $ let_ "x" (lvar x') emptyHole + lAM "x" $ + let_ x' (emptyHole `ann` tlet "a" tEmptyHole (tvar "a")) $ + let_ "y" (emptyHole `ann` tlet "b" (tvar "x") (tvar "b")) $ + let_ "x" (lvar x') emptyHole pure (e, expect1, expect2) in do s1 <- evalFullTest maxID builtinTypes mempty 1 Chk expr @@ -954,95 +952,95 @@ unit_type_preservation_BETA_regression = -- The 'A' sequence previously captured in the type "S" above -- Λb x. (Λa λc (? : a) : ∀b.(Nat -> b)) @(b Bool) x eA <- - lAM "b" - $ lam "x" - $ ( lAM "a" (lam "c" $ emptyHole `ann` tvar "a") + lAM "b" $ + lam "x" $ + ( lAM "a" (lam "c" $ emptyHole `ann` tvar "a") `ann` tforall "b" ktype (tcon tNat `tfun` tvar "b") ) - `aPP` (tvar "b" `tapp` tcon tBool) - `app` lvar "x" + `aPP` (tvar "b" `tapp` tcon tBool) + `app` lvar "x" -- Do the BETA step -- Λb x. ((lettype a = b Bool in λc (? : a)) : (let b = b Bool in Nat -> b)) x expectA1 <- - lAM "b" - $ lam "x" - $ ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a") + lAM "b" $ + lam "x" $ + ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a") `ann` tlet "b" (tvar "b" `tapp` tcon tBool) (tcon tNat `tfun` tvar "b") ) - `app` lvar "x" + `app` lvar "x" -- NB: the point of the ... `app` lvar x is to make the annotated term be in SYN position -- so we reduce the type, rather than taking an upsilon step -- Push the let b -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (Nat -> (let b = b Bool in b))) x expectA2 <- - lAM "b" - $ lam "x" - $ ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a") + lAM "b" $ + lam "x" $ + ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a") `ann` (tcon tNat `tfun` tlet "b" (tvar "b" `tapp` tcon tBool) (tvar "b")) ) - `app` lvar "x" + `app` lvar "x" -- Inline the let -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (Nat -> b Bool)) x expectA3 <- - lAM "b" - $ lam "x" - $ ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a") + lAM "b" $ + lam "x" $ + ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a") `ann` (tcon tNat `tfun` (tvar "b" `tapp` tcon tBool)) ) - `app` lvar "x" + `app` lvar "x" -- Push the let -- Λb. λx. (λc (lettype a = b Bool in (? : a)) : (Nat -> b Bool)) x expectA4 <- - lAM "b" - $ lam "x" - $ ( lam "c" (letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a")) + lAM "b" $ + lam "x" $ + ( lam "c" (letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a")) `ann` (tcon tNat `tfun` (tvar "b" `tapp` tcon tBool)) ) - `app` lvar "x" + `app` lvar "x" -- Do the beta step -- Λb. λx. (let c = (x : Nat) in (lettype a = b Bool in (? : a)) : (b Bool)) expectA5 <- - lAM "b" - $ lam "x" - $ let_ "c" (lvar "x" `ann` tcon tNat) (letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a")) - `ann` (tvar "b" `tapp` tcon tBool) + lAM "b" $ + lam "x" $ + let_ "c" (lvar "x" `ann` tcon tNat) (letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a")) + `ann` (tvar "b" `tapp` tcon tBool) -- Elide a pointless let -- Λb. λx. ((lettype a = b Bool in (? : a)) : (b Bool)) expectA6 <- - lAM "b" - $ lam "x" - $ letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a") - `ann` (tvar "b" `tapp` tcon tBool) + lAM "b" $ + lam "x" $ + letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a") + `ann` (tvar "b" `tapp` tcon tBool) -- Push the lets, eliding those that are redundant -- Λb. λx. ((? : lettype a = b Bool in a) : (b Bool)) expectA7 <- - lAM "b" - $ lam "x" - $ emptyHole - `ann` tlet "a" (tvar "b" `tapp` tcon tBool) (tvar "a") - `ann` (tvar "b" `tapp` tcon tBool) + lAM "b" $ + lam "x" $ + emptyHole + `ann` tlet "a" (tvar "b" `tapp` tcon tBool) (tvar "a") + `ann` (tvar "b" `tapp` tcon tBool) -- Inline a let -- Λb. λx. ((? : b Bool) : (b Bool)) expectA8 <- - lAM "b" - $ lam "x" - $ emptyHole - `ann` (tvar "b" `tapp` tcon tBool) - `ann` (tvar "b" `tapp` tcon tBool) + lAM "b" $ + lam "x" $ + emptyHole + `ann` (tvar "b" `tapp` tcon tBool) + `ann` (tvar "b" `tapp` tcon tBool) -- The 'B' sequence previously captured in the term "t" above -- Λb. (Λa (foo @(b Bool) : ∀b.Nat) @Char eB <- - lAM "b" - $ ( lAM "a" (gvar foo `aPP` (tvar "b" `tapp` tcon tBool)) - `ann` tforall "b" ktype (tcon tNat) - ) - `aPP` tcon tChar + lAM "b" $ + ( lAM "a" (gvar foo `aPP` (tvar "b" `tapp` tcon tBool)) + `ann` tforall "b" ktype (tcon tNat) + ) + `aPP` tcon tChar -- BETA step -- Λb. (lettype a = Char in foo @(b Bool)) : (let b = Char in Nat) expectB1 <- - lAM "b" - $ letType "a" (tcon tChar) (gvar foo `aPP` (tvar "b" `tapp` tcon tBool)) - `ann` tlet "b" (tcon tChar) (tcon tNat) + lAM "b" $ + letType "a" (tcon tChar) (gvar foo `aPP` (tvar "b" `tapp` tcon tBool)) + `ann` tlet "b" (tcon tChar) (tcon tNat) -- Drop annotation, elide lettype -- Λb. foo @(b Bool) expectB3 <- lAM "b" $ gvar foo `aPP` (tvar "b" `tapp` tcon tBool) @@ -1072,9 +1070,9 @@ unit_type_preservation_BETA_regression = tyB = TForall () "c" (KFun () (KType ()) (KType ())) $ TCon () tNat foo = qualifyName (ModuleName ["M"]) "foo" fooTy = TForall () "d" (KType ()) $ TCon () tNat - tmp ty e = case runTypecheckTestMWithPrims NoSmartHoles - $ local (extendGlobalCxt [(foo, fooTy)]) - $ check ty e of + tmp ty e = case runTypecheckTestMWithPrims NoSmartHoles $ + local (extendGlobalCxt [(foo, fooTy)]) $ + check ty e of Left err -> assertFailure $ show err Right _ -> pure () in do @@ -1121,17 +1119,17 @@ unit_let_self_capture = -- We do not need to do anything special for letrec e4 <- lAM "a" $ lam "f" $ lam "x" $ letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "x") expect4a <- - lAM "a" - $ lam "f" - $ lam "x" - $ letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "f" `app` lvar "x") - `ann` tvar "a" + lAM "a" $ + lam "f" $ + lam "x" $ + letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "f" `app` lvar "x") + `ann` tvar "a" expect4b <- - lAM "a" - $ lam "f" - $ lam "x" - $ (lvar "f" `app` letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "x")) - `ann` tvar "a" + lAM "a" $ + lam "f" $ + lam "x" $ + (lvar "f" `app` letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "x")) + `ann` tvar "a" pure ( e1 , t1 @@ -1200,25 +1198,25 @@ spanM f (x : xs) = do unit_regression_self_capture_let_let :: Assertion unit_regression_self_capture_let_let = do let e = - lAM "y" - $ let_ "x" (emptyHole `ann` tvar "y") - $ let_ "y" (emptyHole `ann` tvar "y") - $ lvar "y" - `app` lvar "x" + lAM "y" $ + let_ "x" (emptyHole `ann` tvar "y") $ + let_ "y" (emptyHole `ann` tvar "y") $ + lvar "y" + `app` lvar "x" f = - lAM "y" - $ let_ + lAM "y" $ + let_ "y" (emptyHole `ann` tvar "y") (lvar "y") - `app` let_ - "x" - (emptyHole `ann` tvar "y") - (lvar "x") + `app` let_ + "x" + (emptyHole `ann` tvar "y") + (lvar "x") g = - lAM "y" - $ (emptyHole `ann` tvar "y") - `app` (emptyHole `ann` tvar "y") + lAM "y" $ + (emptyHole `ann` tvar "y") + `app` (emptyHole `ann` tvar "y") (e', i) = create e ev n = evalFullTest i mempty mempty n Chk e' x ~ y = x >>= (<~==> Left (TimedOut (create' y))) @@ -1234,10 +1232,8 @@ unit_regression_self_capture_let_let = do -- implementation is sufficiently different that it doesn't make sense -- to combine them. tasty_type_preservation :: Property -tasty_type_preservation = withTests 1000 - $ withDiscards 2000 - $ propertyWT testModules - $ do +tasty_type_preservation = withTests 1000 $ + withDiscards 2000 . propertyWT testModules $ do let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False} let optsR = RunRedexOptions{pushAndElide = True} let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules @@ -1303,8 +1299,8 @@ tasty_prim_hex_nat = withTests 20 . property $ do n <- forAllT $ Gen.integral $ Range.constant 0 50 let ne = nat n ((dir, e, r, prims), maxID) = - create - $ if n <= 15 + create $ + if n <= 15 then (Chk,,,) <$> case_ @@ -1327,9 +1323,9 @@ tasty_prim_hex_nat = withTests 20 . property $ do else (Syn,,,) <$> pfun NatToHex - `app` ne + `app` ne <*> con cNothing [] - `ann` (tcon tMaybe `tapp` tcon tChar) + `ann` (tcon tMaybe `tapp` tcon tChar) <*> primDefs s <- evalFullTasty maxID builtinTypes prims 7 dir e over evalResultExpr zeroIDs s === Right (zeroIDs r) @@ -1353,11 +1349,11 @@ unit_prim_char_eq_2 = unit_prim_char_partial :: Assertion unit_prim_char_partial = let ((e, prims), maxID) = - create - $ (,) - <$> pfun EqChar - `app` char 'a' - <*> primDefs + create $ + (,) + <$> pfun EqChar + `app` char 'a' + <*> primDefs in do s <- evalFullTest maxID mempty prims 1 Syn e s <~==> Right e @@ -1740,8 +1736,8 @@ unit_handleEvalFullRequest_modules = importModules [primitiveModule', builtinModule'] foo <- pfun ToUpper `app` char 'a' resp <- - readerToState - $ handleEvalFullRequest + readerToState $ + handleEvalFullRequest EvalFullReq { evalFullReqExpr = foo , evalFullCxtDir = Chk @@ -1768,14 +1764,14 @@ unit_handleEvalFullRequest_modules_scrutinize_imported_type = (con0 cTrue `ann` tcon tBool) [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] resp <- - readerToState - $ handleEvalFullRequest - $ EvalFullReq - { evalFullReqExpr = foo - , evalFullCxtDir = Chk - , evalFullMaxSteps = 2 - , evalFullOptions = UnderBinders - } + readerToState $ + handleEvalFullRequest $ + EvalFullReq + { evalFullReqExpr = foo + , evalFullCxtDir = Chk + , evalFullMaxSteps = 2 + , evalFullOptions = UnderBinders + } expect <- con0 cFalse pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" @@ -1787,8 +1783,8 @@ unit_handleEvalFullRequest_modules_scrutinize_imported_type = where m = do boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef - pure - $ Module + pure $ + Module { moduleName = qualifiedModule tBool , moduleTypes = Map.singleton (baseName tBool) boolDef' , moduleDefs = mempty @@ -1799,14 +1795,14 @@ unit_handleEvalFullRequest_even3 = let test = do expr <- gvar even3MainName resp <- - readerToState - $ handleEvalFullRequest - $ EvalFullReq - { evalFullReqExpr = expr - , evalFullCxtDir = Chk - , evalFullMaxSteps = 200 - , evalFullOptions = UnderBinders - } + readerToState $ + handleEvalFullRequest $ + EvalFullReq + { evalFullReqExpr = expr + , evalFullCxtDir = Chk + , evalFullMaxSteps = 200 + , evalFullOptions = UnderBinders + } pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" EvalFullRespNormal e -> e ~= even3MainExpected @@ -1819,14 +1815,14 @@ unit_handleEvalFullRequest_mapOdd = let test = do expr <- gvar mapOddMainName resp <- - readerToState - $ handleEvalFullRequest - $ EvalFullReq - { evalFullReqExpr = expr - , evalFullCxtDir = Chk - , evalFullMaxSteps = 400 - , evalFullOptions = UnderBinders - } + readerToState $ + handleEvalFullRequest $ + EvalFullReq + { evalFullReqExpr = expr + , evalFullCxtDir = Chk + , evalFullMaxSteps = 400 + , evalFullOptions = UnderBinders + } pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" EvalFullRespNormal e -> e ~= mapOddMainExpected @@ -1839,14 +1835,14 @@ unit_handleEvalFullRequest_mapOddPrim = let test = do expr <- gvar mapOddPrimMainName resp <- - readerToState - $ handleEvalFullRequest - $ EvalFullReq - { evalFullReqExpr = expr - , evalFullCxtDir = Chk - , evalFullMaxSteps = 300 - , evalFullOptions = UnderBinders - } + readerToState $ + handleEvalFullRequest $ + EvalFullReq + { evalFullReqExpr = expr + , evalFullCxtDir = Chk + , evalFullMaxSteps = 300 + , evalFullOptions = UnderBinders + } pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" EvalFullRespNormal e -> e ~= mapOddPrimMainExpected @@ -1856,10 +1852,8 @@ unit_handleEvalFullRequest_mapOddPrim = -- Test that evaluation does not duplicate node IDs tasty_unique_ids :: Property -tasty_unique_ids = withTests 1000 - $ withDiscards 2000 - $ propertyWT testModules - $ do +tasty_unique_ids = withTests 1000 $ + withDiscards 2000 . propertyWT testModules $ do let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False} let optsR = RunRedexOptions{pushAndElide = True} let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules @@ -1889,8 +1883,8 @@ unit_wildcard = expectTerm = create' $ con0 cTrue (eDiverge, maxIDDiverge) = create $ caseFB_ loop [branch cZero [] $ con0 cFalse] (con0 cTrue) expectDiverge = - create' - $ caseFB_ + create' $ + caseFB_ ( letrec "x" (lvar "x") (tcon tNat) (lvar "x") `ann` tcon tNat ) @@ -1912,8 +1906,8 @@ unit_case_prim = (e2, maxID2) = create $ caseFB_ (char 'a') [branchPrim (PrimChar 'a') $ con0 cFalse] (con0 cTrue) expect2 = create' $ con0 cFalse (e3, maxID3) = - create - $ caseFB_ + create $ + caseFB_ (char 'b') [ branchPrim (PrimChar 'a') $ con0 cTrue , branchPrim (PrimChar 'b') $ con0 cFalse @@ -1921,8 +1915,8 @@ unit_case_prim = (con0 cTrue) expect3 = create' $ con0 cFalse (e4, maxID4) = - create - $ caseFB_ + create $ + caseFB_ ( (lam "x" (lvar "x") `ann` (tcon tChar `tfun` tcon tChar)) `app` char 'a' ) @@ -2005,25 +1999,25 @@ evalFullTasty id_ tydefs globals n d e = do unaryPrimTest :: HasCallStack => PrimDef -> S Expr -> S Expr -> Assertion unaryPrimTest f x y = let ((e, r, prims), maxID) = - create - $ (,,) - <$> pfun f - `app` x - <*> y - <*> primDefs + create $ + (,,) + <$> pfun f + `app` x + <*> y + <*> primDefs in do s <- evalFullTest maxID mempty prims 2 Syn e s <~==> Right r binaryPrimTest :: HasCallStack => PrimDef -> S Expr -> S Expr -> S Expr -> Assertion binaryPrimTest f x y z = let ((e, r, prims), maxID) = - create - $ (,,) - <$> pfun f - `app` x - `app` y - <*> z - <*> primDefs + create $ + (,,) + <$> pfun f + `app` x + `app` y + <*> z + <*> primDefs in do s <- evalFullTest maxID mempty prims 2 Syn e s <~==> Right r diff --git a/primer/test/Tests/Examples.hs b/primer/test/Tests/Examples.hs index 3e5c0dd92..d0dfb2de1 100644 --- a/primer/test/Tests/Examples.hs +++ b/primer/test/Tests/Examples.hs @@ -35,8 +35,8 @@ checkExamplesRequest = where others = ModuleName $ pure "OtherExamples" otherExamples = - Module others mempty - $ Map.fromList + Module others mempty $ + Map.fromList [ first baseName $ create' $ not others , first baseName $ create' $ comprehensiveWellTyped others ] @@ -51,8 +51,8 @@ unit_check_examples = case runTypecheckTestM unit_comprehensive_ill_typed :: Assertion unit_comprehensive_ill_typed = case runTypecheckTestM NoSmartHoles - ( checkEverything NoSmartHoles - $ CheckEverything + ( checkEverything NoSmartHoles $ + CheckEverything { trusted = [create' builtinModule] , toCheck = [Module modName mempty $ Map.fromList [first baseName $ create' $ comprehensive modName]] } diff --git a/primer/test/Tests/FreeVars.hs b/primer/test/Tests/FreeVars.hs index c9e29e590..bf0a810d4 100644 --- a/primer/test/Tests/FreeVars.hs +++ b/primer/test/Tests/FreeVars.hs @@ -19,8 +19,8 @@ unit_2 = t = ann ( app - ( lam "x" - $ case_ + ( lam "x" $ + case_ (lvar "x") [ branch cZero [] $ con0 cTrue , branch cSucc [("n", Nothing)] (app (lvar "f") (lvar "n")) diff --git a/primer/test/Tests/Gen/App.hs b/primer/test/Tests/Gen/App.hs index bf641d13a..adae29d4c 100644 --- a/primer/test/Tests/Gen/App.hs +++ b/primer/test/Tests/Gen/App.hs @@ -19,14 +19,13 @@ import Primer.Typecheck (SmartHoles (NoSmartHoles), TypeError) import Tasty (Property, withDiscards, withTests) tasty_genProg_well_formed :: Property -tasty_genProg_well_formed = withTests 500 - $ withDiscards 2000 - $ propertyWT [] - $ do - builtinModule' <- builtinModule - primitiveModule' <- primitiveModule - p <- forAllT $ genProg NoSmartHoles [builtinModule', primitiveModule'] - c <- runExceptT @TypeError $ checkProgWellFormed p - case c of - Left err -> annotateShow err >> failure - Right _ -> pure () +tasty_genProg_well_formed = withTests 500 $ + withDiscards 2000 $ + propertyWT [] $ do + builtinModule' <- builtinModule + primitiveModule' <- primitiveModule + p <- forAllT $ genProg NoSmartHoles [builtinModule', primitiveModule'] + c <- runExceptT @TypeError $ checkProgWellFormed p + case c of + Left err -> annotateShow err >> failure + Right _ -> pure () diff --git a/primer/test/Tests/Gen/Core/Typed.hs b/primer/test/Tests/Gen/Core/Typed.hs index 38839e8e9..2b3574ff2 100644 --- a/primer/test/Tests/Gen/Core/Typed.hs +++ b/primer/test/Tests/Gen/Core/Typed.hs @@ -77,9 +77,8 @@ propertyWTInExtendedLocalGlobalCxt :: [S Module] -> PropertyT WT () -> Property propertyWTInExtendedLocalGlobalCxt mods = propertyWT mods . inExtendedGlobalCxt . inExtendedLocalCxt tasty_genTy :: Property -tasty_genTy = withTests 1000 - $ propertyWTInExtendedGlobalCxt [builtinModule, primitiveModule] - $ do +tasty_genTy = withTests 1000 $ + propertyWTInExtendedGlobalCxt [builtinModule, primitiveModule] $ do k <- forAllT genWTKind ty <- forAllT $ genWTType k ty' <- checkKindTest k =<< generateTypeIDs ty @@ -111,35 +110,33 @@ checkValidContextTest t = do -- This indirectly also tests genCxtExtendingLocal, genCxtExtendingGlobal and genTypeDefGroup tasty_genCxtExtending_typechecks :: Property -tasty_genCxtExtending_typechecks = withTests 1000 - $ propertyWT [builtinModule, primitiveModule] - $ do +tasty_genCxtExtending_typechecks = withTests 1000 $ + propertyWT [builtinModule, primitiveModule] $ do cxt <- forAllT genCxtExtendingGlobal checkValidContextTest cxt cxt' <- forAllT $ local (const cxt) genCxtExtendingLocal checkValidContextTest cxt' tasty_inExtendedLocalGlobalCxt_valid :: Property -tasty_inExtendedLocalGlobalCxt_valid = withTests 1000 - $ withDiscards 2000 - $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] - $ do - cxt <- ask - checkValidContextTest cxt +tasty_inExtendedLocalGlobalCxt_valid = withTests 1000 $ + withDiscards 2000 $ + propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ do + cxt <- ask + checkValidContextTest cxt tasty_genCxtExtending_is_extension :: Property tasty_genCxtExtending_is_extension = - withTests 1000 - $ let cxt0 = initialCxt NoSmartHoles - in propertyWT [] $ do - cxt1 <- forAllT genCxtExtendingGlobal - diff cxt0 extendsGlobal cxt1 - cxt2 <- forAllT $ local (const cxt1) genCxtExtendingGlobal - diff cxt1 extendsGlobal cxt2 - cxt3 <- forAllT $ local (const cxt2) genCxtExtendingLocal - diff cxt2 extendsLocal cxt3 - cxt4 <- forAllT $ local (const cxt3) genCxtExtendingLocal - diff cxt3 extendsLocal cxt4 + withTests 1000 $ + let cxt0 = initialCxt NoSmartHoles + in propertyWT [] $ do + cxt1 <- forAllT genCxtExtendingGlobal + diff cxt0 extendsGlobal cxt1 + cxt2 <- forAllT $ local (const cxt1) genCxtExtendingGlobal + diff cxt1 extendsGlobal cxt2 + cxt3 <- forAllT $ local (const cxt2) genCxtExtendingLocal + diff cxt2 extendsLocal cxt3 + cxt4 <- forAllT $ local (const cxt3) genCxtExtendingLocal + diff cxt3 extendsLocal cxt4 where extendsGlobal (Cxt{typeDefs = tds1, localCxt = lc1, globalCxt = gc1, smartHoles = sh1}) @@ -147,50 +144,48 @@ tasty_genCxtExtending_is_extension = tds1 `M.isSubmapOf` tds2 && lc1 - == lc2 -- we don't extend the locals + == lc2 -- we don't extend the locals && lc1 - == mempty -- and it doesn't make too much sense to do a global extension if already have locals in scope + == mempty -- and it doesn't make too much sense to do a global extension if already have locals in scope && gc1 - `M.isSubmapOf` gc2 + `M.isSubmapOf` gc2 && sh1 - == sh2 + == sh2 extendsLocal (Cxt{typeDefs = tds1, localCxt = lc1, globalCxt = gc1, smartHoles = sh1}) (Cxt{typeDefs = tds2, localCxt = lc2, globalCxt = gc2, smartHoles = sh2}) = tds1 == tds2 && lc1 - `M.isSubmapOf` lc2 -- we only extend the locals + `M.isSubmapOf` lc2 -- we only extend the locals && gc1 - == gc2 + == gc2 && sh1 - == sh2 + == sh2 tasty_genSyns :: Property -tasty_genSyns = withTests 1000 - $ withDiscards 2000 - $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] - $ do - tgtTy <- forAllT $ genWTType (KType ()) - _ :: Type' (Meta (Kind' ())) (Meta ()) <- checkKindTest (KType ()) =<< generateTypeIDs tgtTy - (e, ty) <- forAllT $ genSyns tgtTy - (ty', e') <- synthTest =<< generateIDs e - annotateShow e' - annotateShow ty' - diff ty consistentTypes $ forgetTypeMetadata tgtTy - ty === ty' - e === forgetMetadata e' -- check no smart holes stuff happened +tasty_genSyns = withTests 1000 $ + withDiscards 2000 $ + propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ do + tgtTy <- forAllT $ genWTType (KType ()) + _ :: Type' (Meta (Kind' ())) (Meta ()) <- checkKindTest (KType ()) =<< generateTypeIDs tgtTy + (e, ty) <- forAllT $ genSyns tgtTy + (ty', e') <- synthTest =<< generateIDs e + annotateShow e' + annotateShow ty' + diff ty consistentTypes $ forgetTypeMetadata tgtTy + ty === ty' + e === forgetMetadata e' -- check no smart holes stuff happened tasty_genChk :: Property -tasty_genChk = withTests 1000 - $ withDiscards 2000 - $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] - $ do - ty <- forAllT $ genWTType (KType ()) - _ :: Type' (Meta (Kind' ())) (Meta ()) <- checkKindTest (KType ()) =<< generateTypeIDs ty - t <- forAllT $ genChk ty - t' <- checkTest ty =<< generateIDs t - t === forgetMetadata t' -- check no smart holes stuff happened +tasty_genChk = withTests 1000 $ + withDiscards 2000 $ + propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ do + ty <- forAllT $ genWTType (KType ()) + _ :: Type' (Meta (Kind' ())) (Meta ()) <- checkKindTest (KType ()) =<< generateTypeIDs ty + t <- forAllT $ genChk ty + t' <- checkTest ty =<< generateIDs t + t === forgetMetadata t' -- check no smart holes stuff happened -- Lift 'synth' into a property synthTest :: HasCallStack => Expr -> PropertyT WT (Type' () (), ExprT) diff --git a/primer/test/Tests/Prelude/Utils.hs b/primer/test/Tests/Prelude/Utils.hs index c31e7867d..3147379ba 100644 --- a/primer/test/Tests/Prelude/Utils.hs +++ b/primer/test/Tests/Prelude/Utils.hs @@ -31,8 +31,8 @@ x <===> y = withFrozenCallStack $ on compareExpr (over evalResultExpr zeroIDs) x if ok then success else do - annotate - $ unlines + annotate $ + unlines [ "Pretty Printed Output:" , "LHS____________________________________________________" , prettyWrap a diff --git a/primer/test/Tests/Primitives.hs b/primer/test/Tests/Primitives.hs index 9dd71e579..68c25fc85 100644 --- a/primer/test/Tests/Primitives.hs +++ b/primer/test/Tests/Primitives.hs @@ -50,16 +50,15 @@ unit_prim_con_scope_ast = do -- Our type def is accepted test (checkValidContext =<< ask) @?= Right () -- Char is in scope (though the wrong kind to accept 'PrimChar's!) - assertBool "Char is not in scope?" - $ isRight - $ test - $ checkKind (KFun () (KType ()) (KType ())) - =<< tcon tChar + assertBool "Char is not in scope?" $ + isRight $ + test $ + checkKind (KFun () (KType ()) (KType ())) =<< tcon tChar test (synth =<< char 'a') @?= Left (PrimitiveTypeNotInScope tChar) where charASTDef = - TypeDefAST - $ ASTTypeDef + TypeDefAST $ + ASTTypeDef { astTypeDefParameters = [("a", KType ())] , astTypeDefConstructors = mempty , astTypeDefNameHints = mempty diff --git a/primer/test/Tests/Prog.hs b/primer/test/Tests/Prog.hs index 720ea0034..fa8a6cb9e 100644 --- a/primer/test/Tests/Prog.hs +++ b/primer/test/Tests/Prog.hs @@ -66,16 +66,16 @@ unit_nextProgID_types = kp1 <- kfun khole ktype tC <- tfun tEmptyHole tEmptyHole let t1 = - TypeDefAST - $ ASTTypeDef + TypeDefAST $ + ASTTypeDef { astTypeDefParameters = [("p1", kp1)] , astTypeDefConstructors = [ValCon (qualifyName n "C") [tC]] , astTypeDefNameHints = mempty } kp2 <- khole let t2 = - TypeDefPrim - $ PrimTypeDef + TypeDefPrim $ + PrimTypeDef { primTypeDefParameters = [("p2", kp2)] , primTypeDefNameHints = mempty } @@ -85,8 +85,8 @@ unit_nextProgID_types = , moduleTypes = M.fromList [("T1", t1), ("T2", t2)] , moduleDefs = mempty } - pure - $ Prog + pure $ + Prog { progImports = [] , progModules = [m] , progSelection = Nothing diff --git a/primer/test/Tests/Questions.hs b/primer/test/Tests/Questions.hs index fa9bd0097..7cc890d9a 100644 --- a/primer/test/Tests/Questions.hs +++ b/primer/test/Tests/Questions.hs @@ -71,8 +71,8 @@ test_laws = where -- ideally there'd be a library for this - see https://github.com/hedgehogqa/haskell-hedgehog-classes/issues/13 lawsToTestTree (Laws className props) = - testGroup className - $ map (\(n, p) -> testPropertyNamed n "" p) props + testGroup className $ + map (\(n, p) -> testPropertyNamed n "" p) props -- * Properties of monoids handling shadowing diff --git a/primer/test/Tests/Refine.hs b/primer/test/Tests/Refine.hs index 10e34aaa0..5c82eea91 100644 --- a/primer/test/Tests/Refine.hs +++ b/primer/test/Tests/Refine.hs @@ -251,9 +251,8 @@ tasty_arr_app = propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModu -- if refine _ T S = Just (I:IS,_) , then refine _ T (S $ I) = Just (IS,_); here "S $ I" means "inspect S, I assert they match and strip off a layer" tasty_matches :: Property -tasty_matches = withDiscards 2000 - $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] - $ do +tasty_matches = withDiscards 2000 $ + propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ do tgt <- forAllT $ genWTType (KType ()) src <- forAllT $ genWTType (KType ()) cxt <- ask diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs index 910366553..65926451e 100644 --- a/primer/test/Tests/Serialization.hs +++ b/primer/test/Tests/Serialization.hs @@ -78,9 +78,8 @@ import Test.Tasty.HUnit -- | Check that encoding the value produces the file. test_encode :: TestTree test_encode = - testGroup "encode" - $ fixtures - <&> \(Fixture x path) -> + testGroup "encode" $ + fixtures <&> \(Fixture x path) -> goldenVsString (takeBaseName path) path (pure $ encodePretty x) where -- TODO: put this in Foreword. See: @@ -91,9 +90,8 @@ test_encode = -- | Check that decoding the file produces the value. test_decode :: TestTree test_decode = - testGroup "decode" - $ fixtures - <&> \(Fixture x path) -> + testGroup "decode" $ + fixtures <&> \(Fixture x path) -> testCase (takeBaseName path) $ either assertFailure (x @=?) =<< eitherDecodeFileStrict path -- | A fixture holds some value which is JSON serializable and path to a @@ -129,8 +127,8 @@ fixtures = f2 <- tcon tNat k1 <- ktype kb <- ktype `kfun` ktype - pure - $ TypeDefAST + pure $ + TypeDefAST ASTTypeDef { astTypeDefParameters = [("a", k1), ("b", kb)] , astTypeDefConstructors = [ValCon (vcn ["M"] "C") [f1, f2]] @@ -158,17 +156,17 @@ fixtures = } selection :: Selection selection = - SelectionDef - $ DefSelection (qualifyName modName defName) - $ Just - NodeSelection - { nodeType = BodyNode - , meta = Left exprMeta - } + SelectionDef $ + DefSelection (qualifyName modName defName) $ + Just + NodeSelection + { nodeType = BodyNode + , meta = Left exprMeta + } reductionDetail :: EvalDetail reductionDetail = - BetaReduction - $ BetaReductionDetail + BetaReduction $ + BetaReductionDetail { before = expr , after = expr , bindingName = "x" diff --git a/primer/test/Tests/Shadowing.hs b/primer/test/Tests/Shadowing.hs index a334c0115..c419135bf 100644 --- a/primer/test/Tests/Shadowing.hs +++ b/primer/test/Tests/Shadowing.hs @@ -210,10 +210,8 @@ checkShadowing t = -- Check evaluation does not introduce shadowing, except in some known cases tasty_eval_full_shadow :: Property -tasty_eval_full_shadow = withTests 500 - $ withDiscards 2000 - $ propertyWTInExtendedGlobalCxt testModules - $ do +tasty_eval_full_shadow = withTests 500 $ + withDiscards 2000 . propertyWTInExtendedGlobalCxt testModules $ do let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = True} let optsR = RunRedexOptions{pushAndElide = True} let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules @@ -235,9 +233,8 @@ tasty_eval_full_shadow = withTests 500 tasty_eval_shadow :: Property tasty_eval_shadow = - withDiscards 2000 - $ propertyWTInExtendedGlobalCxt testModules - $ do + withDiscards 2000 $ + propertyWTInExtendedGlobalCxt testModules $ do let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules tds <- asks typeDefs (dir, t, _ty) <- genDirTm @@ -264,9 +261,8 @@ getEvalResultExpr = \case Right e -> e tasty_available_actions_shadow :: Property -tasty_available_actions_shadow = withDiscards 2000 - $ propertyWT [] - $ do +tasty_available_actions_shadow = withDiscards 2000 $ + propertyWT [] $ do l <- forAllT $ Gen.element enumerate cxt <- forAllT $ Gen.choice $ map sequence [[], [builtinModule], [builtinModule, primitiveModule]] a <- forAllT $ genApp SmartHoles cxt diff --git a/primer/test/Tests/Subst.hs b/primer/test/Tests/Subst.hs index 1c1a1b5f0..caf594834 100644 --- a/primer/test/Tests/Subst.hs +++ b/primer/test/Tests/Subst.hs @@ -54,8 +54,8 @@ tasty_subst_non_free_id = propertyWT [] $ do let free = freeVarsTy t let bound = boundVarsTy t a <- - forAllT - $ frequency + forAllT $ + frequency [ (1, Just genTyVarName) , (1, element bound) ] @@ -63,8 +63,8 @@ tasty_subst_non_free_id = propertyWT [] $ do -- We frequently try substituting @a@ with some variable occuring in @t@ -- as (terms containing) those are more likely to flush out bugs in substitution s <- - forAllT - $ frequency + forAllT $ + frequency [ (1, Just $ genWTType =<< genWTKind) , (1, TVar () <<$>> element free) , (1, TVar () <<$>> element bound) @@ -85,8 +85,8 @@ tasty_subst_remove_free = withDiscards 300 $ propertyWT [] $ inExtendedLocalCxt -- We frequently try substituting @a@ with some variable occuring in @t@ -- as (terms containing) those are more likely to flush out bugs in substitution s <- - forAllT - $ frequency + forAllT $ + frequency [ (1, Just $ genWTType =<< genWTKind) , (1, TVar () <<$>> element free') , (1, TVar () <<$>> element (boundVarsTy t)) @@ -104,8 +104,8 @@ tasty_subst_counter_indep = withDiscards 300 $ propertyWT [] $ inExtendedLocalCx -- We frequently try substituting @a@ with some variable occuring in @t@ -- as (terms containing) those are more likely to flush out bugs in substitution s <- - forAllT - $ frequency + forAllT $ + frequency [ (1, Just $ genWTType =<< genWTKind) , (1, TVar () <<$>> element free) , (1, TVar () <<$>> element (boundVarsTy t)) diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index dbf47c4f2..356ff8f2a 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -153,8 +153,8 @@ unit_undefined_variable = unit_const :: Assertion unit_const = - expectTyped - $ ann + expectTyped $ + ann (lam "x" (lam "y" (lvar "x"))) (tfun (tcon tBool) (tfun (tcon tBool) (tcon tBool))) @@ -179,25 +179,25 @@ unit_unsat_con_hole_2 = -- A hole-headed TApp accepts saturated constructors unit_con_hole_app_type_1 :: Assertion unit_con_hole_app_type_1 = - expectTyped - $ con cMakePair [emptyHole, emptyHole] - `ann` (tEmptyHole `tapp` tEmptyHole) + expectTyped $ + con cMakePair [emptyHole, emptyHole] + `ann` (tEmptyHole `tapp` tEmptyHole) -- A hole-headed TApp accepts saturated constructors -- The application spine can be shorter than that required for the constructor unit_con_hole_app_type_2 :: Assertion unit_con_hole_app_type_2 = - expectTyped - $ con cMakePair [emptyHole, emptyHole] - `ann` (tEmptyHole `tapp` tcon tNat) + expectTyped $ + con cMakePair [emptyHole, emptyHole] + `ann` (tEmptyHole `tapp` tcon tNat) -- A hole-headed TApp accepts saturated constructors -- The application spine can match than that required for the constructor unit_con_hole_app_type_3 :: Assertion unit_con_hole_app_type_3 = - expectTyped - $ con cMakePair [emptyHole, emptyHole] - `ann` (tEmptyHole `tapp` tcon tBool `tapp` tcon tNat) + expectTyped $ + con cMakePair [emptyHole, emptyHole] + `ann` (tEmptyHole `tapp` tcon tBool `tapp` tcon tNat) -- A hole-headed TApp rejects saturated constructors, if application spine is too long for the constructor unit_con_hole_app_type_4 :: Assertion @@ -219,8 +219,8 @@ unit_constructor_doesn't_exist = unit_inc :: Assertion unit_inc = - expectTyped - $ ann + expectTyped $ + ann (lam "n" (con cSucc [lvar "n"])) (tfun (tcon tNat) (tcon tNat)) @@ -244,8 +244,8 @@ unit_inc_unsat2 = unit_compose_nat :: Assertion unit_compose_nat = - expectTyped - $ ann + expectTyped $ + ann (lam "f" (lam "g" (app (lvar "f") (hole (lvar "g"))))) ( tfun (tfun (tcon tNat) (tcon tNat)) @@ -269,8 +269,8 @@ unit_recursive_let = -- letrec x : Bool = x in x unit_letrec_1 :: Assertion unit_letrec_1 = - expectTyped - $ letrec "x" (lvar "x") (tcon tBool) (lvar "x") + expectTyped $ + letrec "x" (lvar "x") (tcon tBool) (lvar "x") -- let double : Nat -> Nat -- double = \x -> case x of @@ -279,8 +279,8 @@ unit_letrec_1 = -- in double (Succ Zero) unit_letrec_2 :: Assertion unit_letrec_2 = - expectTyped - $ letrec + expectTyped $ + letrec "double" ( lam "x" @@ -309,8 +309,8 @@ unit_nested_let = -- in yes y unit_let_function :: Assertion unit_let_function = - expectTyped - $ let_ + expectTyped $ + let_ "yes" (ann (lam "x" (con0 cTrue)) (tfun (tcon tBool) (tcon tBool))) (let_ "y" (con0 cFalse `ann` tcon tBool) (app (lvar "yes") (lvar "y"))) @@ -318,8 +318,8 @@ unit_let_function = -- (\f -> f : (Bool -> Bool) -> (Bool -> Bool)) (let y = True :: Bool in \x -> y) unit_let_in_arg :: Assertion unit_let_in_arg = - expectTyped - $ app + expectTyped $ + app ( ann (lam "f" (lvar "f")) (tfun (tfun (tcon tBool) (tcon tBool)) (tfun (tcon tBool) (tcon tBool))) @@ -377,14 +377,14 @@ unit_valConType = do , TForall () "a" (KType ()) $ TFun () (TVar () "a") $ TFun () (TApp () (TCon () tList) (TVar () "a")) $ TApp () (TCon () tList) (TVar () "a") ] f tEither eitherDef - @?= [ TForall () "a" (KType ()) - $ TForall () "b" (KType ()) - $ TFun () (TVar () "a") - $ mkTAppCon tEither [TVar () "a", TVar () "b"] - , TForall () "a" (KType ()) - $ TForall () "b" (KType ()) - $ TFun () (TVar () "b") - $ mkTAppCon tEither [TVar () "a", TVar () "b"] + @?= [ TForall () "a" (KType ()) $ + TForall () "b" (KType ()) $ + TFun () (TVar () "a") $ + mkTAppCon tEither [TVar () "a", TVar () "b"] + , TForall () "a" (KType ()) $ + TForall () "b" (KType ()) $ + TFun () (TVar () "b") $ + mkTAppCon tEither [TVar () "a", TVar () "b"] ] where f tc td = map (valConType tc td) (astTypeDefConstructors td) @@ -392,8 +392,8 @@ unit_valConType = do -- Nat -> Bool accepts \x . case x of Z -> True ; S _ -> False unit_case_isZero :: Assertion unit_case_isZero = - expectTyped - $ ann (lam "x" $ case_ (lvar "x") [branch cZero [] (con0 cTrue), branch cSucc [("n", Nothing)] (con0 cFalse)]) (tfun (tcon tNat) (tcon tBool)) + expectTyped $ + ann (lam "x" $ case_ (lvar "x") [branch cZero [] (con0 cTrue), branch cSucc [("n", Nothing)] (con0 cFalse)]) (tfun (tcon tNat) (tcon tBool)) -- Nat -> Bool rejects \x . case x of {} unit_case_badEmpty :: Assertion @@ -420,12 +420,12 @@ unit_case_subst :: Assertion unit_case_subst = do let ty x = tforall "a" ktype $ tforall "b" ktype $ (tvar x `tfun` (tvar "b" `tfun` tcon tNat)) `tfun` tcon tNat let expr a b = - lAM a - $ lAM b - $ lam "f" - $ case_ - (emptyHole `ann` (tcon tSwap `tapp` tvar b `tapp` tvar a)) - [branch cMakeSwap [("x", Nothing), ("y", Nothing)] $ lvar "f" `app` lvar "x" `app` lvar "y"] + lAM a $ + lAM b $ + lam "f" $ + case_ + (emptyHole `ann` (tcon tSwap `tapp` tvar b `tapp` tvar a)) + [branch cMakeSwap [("x", Nothing), ("y", Nothing)] $ lvar "f" `app` lvar "x" `app` lvar "y"] -- Firstly, with distinct names between type definition and type usage -- (this version should always work) expectTyped $ expr "u" "v" `ann` ty "a" @@ -438,8 +438,8 @@ unit_case_subst = do -- Nat -> Bool accepts \x . case x of Z -> True ; _ -> False unit_case_fallback :: Assertion unit_case_fallback = - expectTyped - $ ann (lam "x" $ caseFB_ (lvar "x") [branch cZero [] (con0 cTrue)] (con0 cFalse)) (tfun (tcon tNat) (tcon tBool)) + expectTyped $ + ann (lam "x" $ caseFB_ (lvar "x") [branch cZero [] (con0 cTrue)] (con0 cFalse)) (tfun (tcon tNat) (tcon tBool)) -- Nat -> Bool rejects \x . case x of S _ -> False unit_case_fallback_inexhaustive :: Assertion @@ -456,8 +456,8 @@ unit_case_fallback_redundant = -- Char -> Bool accepts \x . case x of 'b' -> True ; _ -> False unit_case_primitive :: Assertion unit_case_primitive = - expectTypedWithPrims - $ ann (lam "x" $ caseFB_ (lvar "x") [branchPrim (PrimChar 'b') (con0 cTrue)] (con0 cFalse)) (tfun (tcon tChar) (tcon tBool)) + expectTypedWithPrims $ + ann (lam "x" $ caseFB_ (lvar "x") [branchPrim (PrimChar 'b') (con0 cTrue)] (con0 cFalse)) (tfun (tcon tChar) (tcon tBool)) -- Cannot annotate something with a non-existent type constructor unit_ann_bad :: Assertion @@ -551,19 +551,19 @@ unit_remove_hole_not_perfect = unit_smart_remove_clean_case :: Assertion unit_smart_remove_clean_case = ann - ( lam "x" - $ hole - $ ann - ( case_ - (lvar "x") - [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] - ) - tEmptyHole + ( lam "x" $ + hole $ + ann + ( case_ + (lvar "x") + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] + ) + tEmptyHole ) (tfun (tcon tBool) (tcon tNat)) `smartSynthGives` ann - ( lam "x" - $ case_ + ( lam "x" $ + case_ (lvar "x") [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) @@ -571,17 +571,17 @@ unit_smart_remove_clean_case = unit_poly :: Assertion unit_poly = - expectTyped - $ ann + expectTyped $ + ann (lam "id" $ lAM "a" $ aPP (lvar "id") (tvar "a")) (tforall "c" ktype (tvar "c" `tfun` tvar "c") `tfun` tforall "b" ktype (tvar "b" `tfun` tvar "b")) unit_poly_head_Nat :: Assertion unit_poly_head_Nat = - expectTyped - $ ann - ( lam "x" - $ case_ + expectTyped $ + ann + ( lam "x" $ + case_ (lvar "x") [ branch cNil [] (con0 cZero) , branch cCons [("y", Nothing), ("ys", Nothing)] $ con1 cSucc $ lvar "y" @@ -688,25 +688,23 @@ unit_prim_fun_applied = -- Whenever we synthesise a type, then it kind-checks against (KType()) tasty_synth_well_typed_extcxt :: Property -tasty_synth_well_typed_extcxt = withTests 1000 - $ withDiscards 2000 - $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] - $ do - (e, _ty) <- forAllT genSyn - ty' <- generateTypeIDs . fst =<< synthTest =<< generateIDs e - void $ checkKindTest (KType ()) ty' +tasty_synth_well_typed_extcxt = withTests 1000 $ + withDiscards 2000 $ + propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ do + (e, _ty) <- forAllT genSyn + ty' <- generateTypeIDs . fst =<< synthTest =<< generateIDs e + void $ checkKindTest (KType ()) ty' -- As tasty_synth_well_typed_extcxt, but in the empty context -- this is in case there are problems with primitive constructors -- (which cannot be used unless their corresponding type is in scope) tasty_synth_well_typed_defcxt :: Property -tasty_synth_well_typed_defcxt = withTests 1000 - $ withDiscards 2000 - $ propertyWT [] - $ do - (e, _ty) <- forAllT genSyn - ty' <- generateTypeIDs . fst =<< synthTest =<< generateIDs e - void $ checkKindTest (KType ()) ty' +tasty_synth_well_typed_defcxt = withTests 1000 $ + withDiscards 2000 $ + propertyWT [] $ do + (e, _ty) <- forAllT genSyn + ty' <- generateTypeIDs . fst =<< synthTest =<< generateIDs e + void $ checkKindTest (KType ()) ty' -- Regression test: when we created holes at change-of-direction when checking, -- (i.e. when we were checking T ∋ e for some synthesisable e ∈ S with S /= T) @@ -868,64 +866,52 @@ instance Eq (TypeCacheAlpha App.Selection) where _ == _ = False instance Eq (TypeCacheAlpha Prog) where TypeCacheAlpha (Prog i1 m1 s1 sh1 l1 r1) == TypeCacheAlpha (Prog i2 m2 s2 sh2 l2 r2) = - TypeCacheAlpha i1 - == TypeCacheAlpha i2 - && TypeCacheAlpha m1 - == TypeCacheAlpha m2 - && TypeCacheAlpha s1 - == TypeCacheAlpha s2 - && sh1 - == sh2 - && l1 - == l2 - && r1 - == r2 + TypeCacheAlpha i1 == TypeCacheAlpha i2 + && TypeCacheAlpha m1 == TypeCacheAlpha m2 + && TypeCacheAlpha s1 == TypeCacheAlpha s2 + && sh1 == sh2 + && l1 == l2 + && r1 == r2 instance Eq (TypeCacheAlpha App.App) where TypeCacheAlpha a1 == TypeCacheAlpha a2 = - appInit a1 - == appInit a2 - && appIdCounter a1 - == appIdCounter a2 - && appNameCounter a1 - == appNameCounter a2 - && TypeCacheAlpha (appProg a1) - == TypeCacheAlpha (appProg a2) + appInit a1 == appInit a2 + && appIdCounter a1 == appIdCounter a2 + && appNameCounter a1 == appNameCounter a2 + && TypeCacheAlpha (appProg a1) == TypeCacheAlpha (appProg a2) -- Test that smartholes is idempotent (for well-typed input) tasty_smartholes_idempotent_syn :: Property -tasty_smartholes_idempotent_syn = withTests 1000 - $ withDiscards 2000 - $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] - $ local (\c -> c{smartHoles = SmartHoles}) - $ do - (e, _ty) <- forAllT genSyn - (ty', e') <- synthTest =<< generateIDs e - (ty'', e'') <- synthTest $ exprTtoExpr e' - ty' === ty'' - TypeCacheAlpha e' === TypeCacheAlpha e'' +tasty_smartholes_idempotent_syn = withTests 1000 $ + withDiscards 2000 $ + propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ + local (\c -> c{smartHoles = SmartHoles}) $ do + (e, _ty) <- forAllT genSyn + (ty', e') <- synthTest =<< generateIDs e + (ty'', e'') <- synthTest $ exprTtoExpr e' + ty' === ty'' + TypeCacheAlpha e' === TypeCacheAlpha e'' -- Test that smartholes is idempotent (for well-typed input) -- This also shows that checkKind is idempotent-on-the-nose tasty_smartholes_idempotent_chk :: Property -tasty_smartholes_idempotent_chk = withTests 1000 - $ withDiscards 2000 - $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] - $ local (\c -> c{smartHoles = SmartHoles}) - $ do - ty <- forAllT $ genWTType (KType ()) - e <- forAllT $ genChk ty - tyI <- generateTypeIDs ty - ty' <- checkKindTest (KType ()) tyI - -- Note that ty /= ty' in general, as the generators can create a THole _ (TEmptyHole _) - annotateShow ty' - e' <- checkTest (forgetTypeMetadata ty') =<< generateIDs e - annotateShow e' - ty'' <- checkKindTest (KType ()) $ typeTtoType ty' - annotateShow ty'' - e'' <- checkTest (forgetTypeMetadata ty'') $ exprTtoExpr e' - annotateShow e'' - ty' === ty'' - TypeCacheAlpha e' === TypeCacheAlpha e'' +tasty_smartholes_idempotent_chk = withTests 1000 $ + withDiscards 2000 $ + propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ + local (\c -> c{smartHoles = SmartHoles}) $ do + ty <- forAllT $ genWTType (KType ()) + e <- forAllT $ genChk ty + tyI <- generateTypeIDs ty + ty' <- checkKindTest (KType ()) tyI + -- Note that ty /= ty' in general, as the generators can create a THole _ (TEmptyHole _) + annotateShow ty' + e' <- checkTest (forgetTypeMetadata ty') =<< generateIDs e + annotateShow e' + ty'' <- checkKindTest (KType ()) $ typeTtoType ty' + annotateShow ty'' + e'' <- checkTest (forgetTypeMetadata ty'') $ exprTtoExpr e' + annotateShow e'' + ty' === ty'' + TypeCacheAlpha e' === TypeCacheAlpha e'' -- We must ensure that when we check a program with smartholes that -- any updates to any types are taken into account when checking any @@ -950,8 +936,8 @@ unit_tcWholeProg_notice_type_updates = mkProg ds = do builtinModule' <- builtinModule ds' <- ds - pure - $ Prog + pure $ + Prog { progImports = [builtinModule'] , progModules = [Module (ModuleName ["M"]) mempty ds'] , progSmartHoles = SmartHoles @@ -969,18 +955,17 @@ unit_tcWholeProg_notice_type_updates = -- This is only up to alpha in the TypeCaches, for the same reasons as -- unit_smartholes_idempotent_alpha_typecache tasty_tcWholeProg_idempotent :: Property -tasty_tcWholeProg_idempotent = withTests 500 - $ withDiscards 2000 - $ propertyWT [] - $ do - base <- forAllT $ Gen.choice $ map sequence [[], [builtinModule], [builtinModule, primitiveModule]] - p <- forAllT $ genProg SmartHoles base - case runTypecheckTestM SmartHoles $ do - p' <- tcWholeProgWithImports p - p'' <- tcWholeProgWithImports p' - pure (p', p'') of - Left err -> annotateShow err >> failure - Right (p', p'') -> TypeCacheAlpha p' === TypeCacheAlpha p'' +tasty_tcWholeProg_idempotent = withTests 500 $ + withDiscards 2000 $ + propertyWT [] $ do + base <- forAllT $ Gen.choice $ map sequence [[], [builtinModule], [builtinModule, primitiveModule]] + p <- forAllT $ genProg SmartHoles base + case runTypecheckTestM SmartHoles $ do + p' <- tcWholeProgWithImports p + p'' <- tcWholeProgWithImports p' + pure (p', p'') of + Left err -> annotateShow err >> failure + Right (p', p'') -> TypeCacheAlpha p' === TypeCacheAlpha p'' -- Check that all our builtins are well formed -- (these are used to seed initial programs) @@ -998,8 +983,8 @@ unit_good_defaults = do -- Check that our higher-order test typedef is well formed unit_good_maybeT :: Assertion -unit_good_maybeT = case runTypecheckTestM NoSmartHoles - $ checkEverything +unit_good_maybeT = case runTypecheckTestM NoSmartHoles $ + checkEverything NoSmartHoles CheckEverything { trusted = [builtinMod] @@ -1096,8 +1081,8 @@ testModule :: MonadFresh ID m => m Module testModule = do maybeTDef' <- maybeTDef swapDef' <- swapDef - pure - $ Module + pure $ + Module { moduleName = ModuleName ["TestModule"] , moduleTypes = Map.fromList @@ -1115,8 +1100,8 @@ maybeTDef = do field <- tvar "m" `tapp` (tcon tMaybe `tapp` tvar "a") ka <- ktype km <- ktype `kfun` ktype - pure - $ ASTTypeDef + pure $ + ASTTypeDef { astTypeDefParameters = [("m", km), ("a", ka)] , astTypeDefConstructors = [ValCon (vcn ["TestModule"] "MakeMaybeT") [field]] , astTypeDefNameHints = [] @@ -1134,8 +1119,8 @@ swapDef = do f2 <- tvar "a" ka <- ktype kb <- ktype - pure - $ ASTTypeDef + pure $ + ASTTypeDef { astTypeDefParameters = [("a", ka), ("b", kb)] , astTypeDefConstructors = [ValCon cMakeSwap [f1, f2]] , astTypeDefNameHints = [] diff --git a/primer/test/Tests/Undo.hs b/primer/test/Tests/Undo.hs index 624535b78..4189515b3 100644 --- a/primer/test/Tests/Undo.hs +++ b/primer/test/Tests/Undo.hs @@ -74,8 +74,8 @@ unit_redo_eval = ] ] eval = - readerToState - $ handleEvalFullRequest + readerToState $ + handleEvalFullRequest App.EvalFullReq { App.evalFullReqExpr = Var (Meta 0 Nothing Nothing) (GlobalVarRef $ qualifyName scope "main") , App.evalFullCxtDir = Syn @@ -119,8 +119,8 @@ unit_redo_eval_interp = ] ] eval = - readerToState - $ handleEvalInterpRequest + readerToState $ + handleEvalInterpRequest App.EvalInterpReq { App.expr = Var (Meta 0 Nothing Nothing) (GlobalVarRef $ qualifyName scope "main") , App.dir = Syn @@ -162,8 +162,8 @@ unit_redo_eval_interp_bounded = ] ] eval = - readerToState - $ handleEvalBoundedInterpRequest + readerToState $ + handleEvalBoundedInterpRequest App.EvalBoundedInterpReq { App.expr = Var (Meta 0 Nothing Nothing) (GlobalVarRef $ qualifyName scope "main") , App.dir = Syn diff --git a/primer/test/Tests/Unification.hs b/primer/test/Tests/Unification.hs index 6fdbc59c9..c954503f8 100644 --- a/primer/test/Tests/Unification.hs +++ b/primer/test/Tests/Unification.hs @@ -105,8 +105,8 @@ unit_diff_module_not_refl = @?= Nothing where mint = - TypeDefAST - $ ASTTypeDef + TypeDefAST $ + ASTTypeDef { astTypeDefParameters = mempty , astTypeDefConstructors = mempty , astTypeDefNameHints = mempty @@ -237,8 +237,8 @@ unit_ill_kinded_0 = let res = evalTestM 0 - ( runExceptT - $ unify + ( runExceptT $ + unify defaultCxt (S.singleton "a") (TApp () (TEmptyHole ()) (TCon () tList)) @@ -528,9 +528,8 @@ tasty_unified_checks = propertyWTInExtendedUVCxt [builtinModule, primitiveModule -- S,T diff kinds => unify ga uvs S T fails -- This requires each to not be holey - i.e. don't synthesise KHole tasty_diff_kinds_never_unify :: Property -tasty_diff_kinds_never_unify = withDiscards 5000 - $ propertyWTInExtendedUVCxt [builtinModule, primitiveModule] - $ \uvs -> do +tasty_diff_kinds_never_unify = withDiscards 5000 $ + propertyWTInExtendedUVCxt [builtinModule, primitiveModule] $ \uvs -> do cxt <- ask k1 <- forAllT genWTKind k2 <- forAllT genWTKind diff --git a/primer/test/Tests/Zipper.hs b/primer/test/Tests/Zipper.hs index d763da520..ba7a32027 100644 --- a/primer/test/Tests/Zipper.hs +++ b/primer/test/Tests/Zipper.hs @@ -55,10 +55,10 @@ unit_binders_below_type = unit_binders_below :: Assertion unit_binders_below = let e = - create' - $ ann - ( lam "x" - $ case_ + create' $ + ann + ( lam "x" $ + case_ (lAM "y" emptyHole) [branch' (["M"], "C") [("z", Nothing), ("w", Nothing)] $ aPP (hole $ lam "v" emptyHole) (tapp tEmptyHole $ tforall "a" ktype $ tforall "b" ktype tEmptyHole)] ) diff --git a/primer/testlib/Primer/Test/Eval.hs b/primer/testlib/Primer/Test/Eval.hs index c1b944be0..3fc4c1a20 100644 --- a/primer/testlib/Primer/Test/Eval.hs +++ b/primer/testlib/Primer/Test/Eval.hs @@ -203,9 +203,9 @@ annotatedPair modName = do (oddName, oddDef) <- Examples.odd modName let ty = tcon tNat `tfun` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat) let expr1 = - let_ "x" (con0 cZero) - $ lam "n" (con cMakePair [gvar evenName `app` lvar "n", lvar "x"]) - `ann` ty + let_ "x" (con0 cZero) $ + lam "n" (con cMakePair [gvar evenName `app` lvar "n", lvar "x"]) + `ann` ty expr <- expr1 `app` con0 cZero let globs = [(evenName, evenDef), (oddName, oddDef)] expect <- @@ -218,8 +218,8 @@ letrecLambda :: S (Expr, Expr) letrecLambda = do -- 'f' is a bit silly here, but could just as well be a definition of 'even' let f = - lam "x" - $ case_ + lam "x" $ + case_ (lvar "x") [ branch cZero [] $ con0 cTrue , branch cSucc [("i", Nothing)] $ lvar "f" `app` lvar "i" @@ -267,7 +267,7 @@ primitiveAnnotation = <$> ( pfun ToUpper `ann` (tcon tChar `tfun` tcon tChar) ) - `app` (char 'a' `ann` tcon tChar) + `app` (char 'a' `ann` tcon tChar) <*> char 'A' <*> primDefs @@ -275,20 +275,20 @@ lazyPrimitive1 :: S (Expr, Expr, DefMap) lazyPrimitive1 = (,,) <$> pfun PrimConst - `app` bool_ True - `app` emptyHole + `app` bool_ True + `app` emptyHole <*> bool_ True - `ann` tcon tBool + `ann` tcon tBool <*> primDefs lazyPrimitive2 :: S (Expr, Expr, DefMap) lazyPrimitive2 = (,,) <$> pfun PrimConst - `app` bool_ True - `app` letrec "x" (lvar "x") (tcon tNat) (lvar "x") + `app` bool_ True + `app` letrec "x" (lvar "x") (tcon tNat) (lvar "x") <*> bool_ True - `ann` tcon tBool + `ann` tcon tBool <*> primDefs primitivePartialMap :: ModuleName -> S (Expr, Expr, DefMap, DefMap) @@ -296,19 +296,19 @@ primitivePartialMap modName = do (mapName, mapDef) <- Examples.map' modName (,,,) <$> gvar mapName - `aPP` tcon tChar - `aPP` tcon tChar - `app` pfun ToUpper - `app` list_ - [ char 'a' - , char 'b' - , char 'c' - ] + `aPP` tcon tChar + `aPP` tcon tChar + `app` pfun ToUpper + `app` list_ + [ char 'a' + , char 'b' + , char 'c' + ] <*> list_ [ char 'A' , char 'B' , char 'C' ] - `ann` (tcon tList `tapp` tcon tChar) + `ann` (tcon tList `tapp` tcon tChar) <*> pure (M.singleton mapName mapDef) <*> primDefs