diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index a3283e528..4f52b5c14 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -159,12 +159,13 @@ import Primer.App ( newApp, newEmptyApp, progAllDefs, - progAllTypeDefs, progAllTypeDefsMeta, progCxt, + progDefMap, progImports, progModules, progSelection, + progTypeDefMap, redoLogEmpty, runEditAppM, runQueryAppM, @@ -1494,7 +1495,7 @@ availableActions = curry3 $ logAPI (noError AvailableActions) $ \(sid, level, se prog <- getProgram sid let allDefs = progAllDefs prog allTypeDefs = progAllTypeDefsMeta prog - allDefs' = snd <$> allDefs + allDefs' = progDefMap prog allTypeDefs' = forgetTypeDefMetadata . snd <$> allTypeDefs case selection of SelectionDef sel -> do @@ -1526,11 +1527,11 @@ actionOptions :: actionOptions = curry4 $ logAPI (noError ActionOptions) $ \(sid, level, selection, action) -> do app <- getApp sid let prog = appProg app - allDefs = progAllDefs prog - allTypeDefs = progAllTypeDefs prog + allDefs = progDefMap prog + allTypeDefs = progTypeDefMap prog def <- snd <$> findASTTypeOrTermDef prog selection maybe (throwM $ ActionOptionsNoID selection) pure - $ Available.options (snd <$> allTypeDefs) (snd <$> allDefs) (progCxt prog) level def selection action + $ 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,7 +1563,7 @@ applyActionNoInput = curry3 $ logAPI (noError ApplyActionNoInput) $ \(sid, selec def <- snd <$> findASTTypeOrTermDef prog selection actions <- either (throwM . ToProgActionError (Available.NoInput action)) pure - $ toProgActionNoInput (snd <$> progAllDefs prog) def selection action + $ toProgActionNoInput (progDefMap prog) def selection action applyActions sid actions applyActionInput :: diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs index 212495c95..0e9e26b17 100644 --- a/primer-api/test/Tests/API.hs +++ b/primer-api/test/Tests/API.hs @@ -70,9 +70,6 @@ import Primer.App ( ) import Primer.App qualified as App import Primer.Builtins ( - cCons, - cFalse, - cNil, cTrue, cZero, tBool, @@ -101,8 +98,14 @@ import Primer.EvalFullInterp ( import Primer.Examples ( comprehensive, even3App, + even3MainExpected, + even3MainName, mapOddApp, + mapOddMainExpected, + mapOddMainName, mapOddPrimApp, + mapOddPrimMainExpected, + mapOddPrimMainName, ) import Primer.Gen.Core.Raw (evalExprGen, genExpr, genType) import Primer.Module (moduleDefsQualified) @@ -114,7 +117,6 @@ import Primer.Test.Util ( assertException, constructSaturatedCon, constructTCon, - gvn, (@?=), ) import Primer.UUIDv4 (nextRandom) @@ -517,10 +519,10 @@ test_evalFull_even3 = let step = liftIO . step' step "Add the even3App to the session" sid <- addSession "even3App" even3App - step "Eval even3" - let expr = create' $ gvar $ gvn ["Even3"] "even 3?" + step "Eval main" + let expr = create' $ gvar even3MainName resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders) - let expected = create' $ con0 cFalse + let expected = even3MainExpected case resp of Left e -> liftIO $ assertFailure $ "ProgError: " <> show e Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e @@ -534,9 +536,9 @@ test_evalFull_mapOdd = step "Add the mapOddApp to the session" sid <- addSession "mapOddApp" mapOddApp step "Eval mapOdd" - let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + let expr = create' $ gvar mapOddMainName resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders) - let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + let expected = mapOddMainExpected case resp of Left e -> liftIO $ assertFailure $ "ProgError: " <> show e Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e @@ -550,9 +552,9 @@ test_evalFull_mapOddPrim = step "Add the mapOddPrimApp to the session" sid <- addSession "mapOddPrimApp" mapOddPrimApp step "Eval mapOdd" - let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + let expr = create' $ gvar mapOddPrimMainName resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders) - let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + let expected = mapOddPrimMainExpected case resp of Left e -> liftIO $ assertFailure $ "ProgError: " <> show e Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e @@ -565,9 +567,9 @@ test_evalFull'_even3 = let step = liftIO . step' step "Add the even3App to the session" sid <- addSession "even3App" even3App - step "Eval even3" - resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["Even3"] "even 3?" - let expected = viewTreeExpr $ create' $ con0 cFalse + step "Eval main" + resp <- evalFull' sid (Just 1000) (Just UnderBinders) even3MainName + let expected = viewTreeExpr even3MainExpected case resp of EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e EvalFullRespNormal e -> zTIds e @?= zTIds expected @@ -580,8 +582,8 @@ test_evalFull'_mapOdd = step "Add the mapOddApp to the session" sid <- addSession "mapOddApp" mapOddApp step "Eval mapOdd" - resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["MapOdd"] "mapOdd" - let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + resp <- evalFull' sid (Just 1000) (Just UnderBinders) mapOddMainName + let expected = viewTreeExpr mapOddMainExpected case resp of EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e EvalFullRespNormal e -> zTIds e @?= zTIds expected @@ -594,8 +596,8 @@ test_evalFull'_mapOddPrim = step "Add the mapOddPrimApp to the session" sid <- addSession "mapOddPrimApp" mapOddPrimApp step "Eval mapOdd" - resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["MapOdd"] "mapOdd" - let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + resp <- evalFull' sid (Just 1000) (Just UnderBinders) mapOddPrimMainName + let expected = viewTreeExpr mapOddPrimMainExpected case resp of EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e EvalFullRespNormal e -> zTIds e @?= zTIds expected @@ -608,10 +610,10 @@ test_evalInterp_even3 = expectFailBecause "interpreter can't reduce top-level de let step = liftIO . step' step "Add the even3App to the session" sid <- addSession "even3App" even3App - step "Eval even3" - let expr = create' $ gvar $ gvn ["Even3"] "even 3?" + step "Eval main" + let expr = create' $ gvar even3MainName resp <- evalInterp sid $ App.EvalInterpReq expr Chk - let expected = create' $ con0 cFalse + let expected = even3MainExpected case resp of Left e -> liftIO $ assertFailure $ "ProgError: " <> show e Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected @@ -625,9 +627,9 @@ test_evalInterp_mapOdd = expectFailBecause "interpreter can't reduce top-level d step "Add the mapOddApp to the session" sid <- addSession "mapOddApp" mapOddApp step "Eval mapOdd" - let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + let expr = create' $ gvar mapOddMainName resp <- evalInterp sid $ App.EvalInterpReq expr Chk - let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + let expected = mapOddMainExpected case resp of Left e -> liftIO $ assertFailure $ "ProgError: " <> show e Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected @@ -641,9 +643,9 @@ test_evalInterp_mapOddPrim = expectFailBecause "interpreter can't reduce top-lev step "Add the mapOddPrimApp to the session" sid <- addSession "mapOddPrimApp" mapOddPrimApp step "Eval mapOdd" - let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + let expr = create' $ gvar mapOddPrimMainName resp <- evalInterp sid $ App.EvalInterpReq expr Chk - let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + let expected = mapOddPrimMainExpected case resp of Left e -> liftIO $ assertFailure $ "ProgError: " <> show e Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected @@ -656,9 +658,9 @@ test_evalInterp'_even3 = expectFailBecause "interpreter can't reduce top-level d let step = liftIO . step' step "Add the even3App to the session" sid <- addSession "even3App" even3App - step "Eval even3" - (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["Even3"] "even 3?" - let expected = viewTreeExpr $ create' $ con0 cFalse + step "Eval main" + (EvalInterpRespNormal e) <- evalInterp' sid even3MainName + let expected = viewTreeExpr even3MainExpected zTIds e @?= zTIds expected -- https://github.com/hackworthltd/primer/issues/1247 @@ -670,8 +672,8 @@ test_evalInterp'_mapOdd = expectFailBecause "interpreter can't reduce top-level step "Add the mapOddApp to the session" sid <- addSession "mapOddApp" mapOddApp step "Eval mapOdd" - (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["MapOdd"] "mapOdd" - let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + (EvalInterpRespNormal e) <- evalInterp' sid mapOddMainName + let expected = viewTreeExpr mapOddMainExpected zTIds e @?= zTIds expected -- https://github.com/hackworthltd/primer/issues/1247 @@ -683,8 +685,8 @@ test_evalInterp'_mapOddPrim = expectFailBecause "interpreter can't reduce top-le step "Add the mapOddPrimApp to the session" sid <- addSession "mapOddPrimApp" mapOddPrimApp step "Eval mapOdd" - (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["MapOdd"] "mapOdd" - let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + (EvalInterpRespNormal e) <- evalInterp' sid mapOddPrimMainName + let expected = viewTreeExpr mapOddPrimMainExpected zTIds e @?= zTIds expected -- https://github.com/hackworthltd/primer/issues/1247 @@ -695,10 +697,10 @@ test_evalBoundedInterp_even3 = expectFailBecause "interpreter can't reduce top-l let step = liftIO . step' step "Add the even3App to the session" sid <- addSession "even3App" even3App - step "Eval even3" - let expr = create' $ gvar $ gvn ["Even3"] "even 3?" + step "Eval main" + let expr = create' $ gvar even3MainName resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000) - let expected = create' $ con0 cFalse + let expected = even3MainExpected case resp of Left err -> liftIO $ assertFailure $ "ProgError: " <> show err Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err @@ -713,9 +715,9 @@ test_evalBoundedInterp_mapOdd = expectFailBecause "interpreter can't reduce top- step "Add the mapOddApp to the session" sid <- addSession "mapOddApp" mapOddApp step "Eval mapOdd" - let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + let expr = create' $ gvar mapOddMainName resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000) - let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + let expected = mapOddMainExpected case resp of Left err -> liftIO $ assertFailure $ "ProgError: " <> show err Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err @@ -730,9 +732,9 @@ test_evalBoundedInterp_mapOddPrim = expectFailBecause "interpreter can't reduce step "Add the mapOddPrimApp to the session" sid <- addSession "mapOddPrimApp" mapOddPrimApp step "Eval mapOdd" - let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd" + let expr = create' $ gvar mapOddPrimMainName resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000) - let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + let expected = mapOddPrimMainExpected case resp of Left err -> liftIO $ assertFailure $ "ProgError: " <> show err Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err @@ -746,9 +748,9 @@ test_evalBoundedInterp'_even3 = expectFailBecause "interpreter can't reduce top- let step = liftIO . step' step "Add the even3App to the session" sid <- addSession "even3App" even3App - step "Eval even3" - resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["Even3"] "even 3?" - let expected = viewTreeExpr $ create' $ con0 cFalse + step "Eval main" + resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) even3MainName + let expected = viewTreeExpr even3MainExpected case resp of EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected e -> liftIO $ assertFailure $ show e @@ -762,8 +764,8 @@ test_evalBoundedInterp'_mapOdd = expectFailBecause "interpreter can't reduce top step "Add the mapOddApp to the session" sid <- addSession "mapOddApp" mapOddApp step "Eval mapOdd" - resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["MapOdd"] "mapOdd" - let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) mapOddMainName + let expected = viewTreeExpr mapOddMainExpected case resp of EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected e -> liftIO $ assertFailure $ show e @@ -777,8 +779,8 @@ test_evalBoundedInterp'_mapOddPrim = expectFailBecause "interpreter can't reduce step "Add the mapOddPrimApp to the session" sid <- addSession "mapOddPrimApp" mapOddPrimApp step "Eval mapOdd" - resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["MapOdd"] "mapOdd" - let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] + resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) mapOddPrimMainName + let expected = viewTreeExpr mapOddPrimMainExpected case resp of EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected e -> liftIO $ assertFailure $ show e diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 6d1df4411..6c148576e 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -35,8 +35,8 @@ module Primer.App ( newEmptyProg', newProg, newProg', - allDefs, - allTypes, + progDefMap, + progTypeDefMap, progAllModules, progAllDefs, progAllTypeDefs, @@ -476,16 +476,18 @@ importModules ms = do let p' = p & #progImports %~ (<> checkedImports) modify (\a -> a & #currentState % #prog .~ p') --- | Get all type definitions from all modules (including imports) -allTypes :: Prog -> TypeDefMap -allTypes = fmap snd . progAllTypeDefs +-- | Given a 'Prog', return its 'TypeDefMap' (i.e., all type +-- definitions from all modules, including imports). +progTypeDefMap :: Prog -> TypeDefMap +progTypeDefMap = fmap snd . progAllTypeDefs allTypesMeta :: Prog -> Map TyConName (TypeDef TypeMeta KindMeta) allTypesMeta = fmap snd . progAllTypeDefsMeta --- | Get all definitions from all modules (including imports) -allDefs :: Prog -> DefMap -allDefs = fmap snd . progAllDefs +-- | Given a 'Prog', return its 'DefMap' (i.e., all term definitions +-- from all modules, including imports). +progDefMap :: Prog -> DefMap +progDefMap = fmap snd . progAllDefs -- | The action log -- This is the canonical store of the program - we can recreate any current or @@ -599,7 +601,7 @@ handleQuestion :: MonadQueryApp m ProgError => Question a -> m a handleQuestion = \case VariablesInScope defid exprid -> do node <- focusNode' defid exprid - defs <- asks $ allDefs . appProg + defs <- asks $ progDefMap . appProg let (tyvars, termvars, globals) = case node of Left zE -> variablesInScopeExpr defs zE Right zT -> (variablesInScopeTy zT, [], []) @@ -622,7 +624,7 @@ focusNode prog = focusNodeDefs $ foldMap' moduleDefsQualified $ progModules prog -- This looks in the editable modules and also in any imports focusNodeImports :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either Loc (Either TypeZip KindTZ)) -focusNodeImports prog = focusNodeDefs $ allDefs prog +focusNodeImports prog = focusNodeDefs $ progDefMap prog focusNodeDefs :: MonadError ProgError m => DefMap -> GVarName -> ID -> m (Either Loc (Either TypeZip KindTZ)) focusNodeDefs defs defname nodeid = @@ -670,11 +672,11 @@ handleEvalRequest req = do app <- ask let prog = appProg app let as = AvoidShadowing - result <- runFreshM app $ Eval.step as (allTypes prog) (allDefs prog) (evalReqExpr req) Syn (evalReqRedex req) + result <- runFreshM app $ Eval.step as (progTypeDefMap prog) (progDefMap prog) (evalReqExpr req) Syn (evalReqRedex req) case result of Left err -> throwError' err Right (expr, detail) -> do - redexes <- Eval.redexes as (allTypes prog) (allDefs prog) Syn expr + redexes <- Eval.redexes as (progTypeDefMap prog) (progDefMap prog) Syn expr pure EvalResp { evalRespExpr = expr @@ -692,7 +694,7 @@ handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxS let prog = appProg app let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False} let optsR = RunRedexOptions{pushAndElide = True} - result <- runFreshM app $ evalFull evalFullOptions optsV optsR (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr + result <- runFreshM app $ evalFull evalFullOptions optsV optsR (progTypeDefMap prog) (progDefMap prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr pure $ case result of Left (TimedOut e) -> EvalFullRespTimedOut e Right nf -> EvalFullRespNormal nf @@ -718,8 +720,8 @@ handleEvalInterpRequest :: handleEvalInterpRequest (EvalInterpReq{expr, dir}) = do app <- ask let prog = appProg app - let env = mkGlobalEnv (allDefs prog) - result <- runFreshM app $ generateIDs $ interp' (allTypes prog) env dir (forgetMetadata expr) + let env = mkGlobalEnv (progDefMap prog) + result <- runFreshM app $ generateIDs $ interp' (progTypeDefMap prog) env dir (forgetMetadata expr) pure $ EvalInterpRespNormal result -- | Handle an 'EvalBoundedInterpReq'. @@ -742,8 +744,8 @@ handleEvalBoundedInterpRequest :: handleEvalBoundedInterpRequest (EvalBoundedInterpReq{expr, dir, timeout}) = do app <- ask let prog = appProg app - let env = mkGlobalEnv (allDefs prog) - result <- liftIO $ interp timeout (allTypes prog) env dir (forgetMetadata expr) + let env = mkGlobalEnv (progDefMap prog) + result <- liftIO $ interp timeout (progTypeDefMap prog) env dir (forgetMetadata expr) case result of Left x -> pure $ EvalBoundedInterpRespFailed x Right e' -> runFreshM app $ generateIDs e' <&> EvalBoundedInterpRespNormal @@ -2145,7 +2147,7 @@ liftError :: MonadError ProgError m => (e -> ProgError) -> ExceptT e m b -> m b liftError = modifyError allConNames :: Prog -> [(TyConName, [ValConName])] -allConNames p = ifoldMap (\tn td -> pure (tn, valConName <$> typeDefConstructors td)) $ allTypes p +allConNames p = ifoldMap (\tn td -> pure (tn, valConName <$> typeDefConstructors td)) $ progTypeDefMap p where typeDefConstructors td = maybe [] astTypeDefConstructors $ typeDefAST td diff --git a/primer/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs index be4ff1878..fb13dd2cd 100644 --- a/primer/src/Primer/Examples.hs +++ b/primer/src/Primer/Examples.hs @@ -41,6 +41,14 @@ module Primer.Examples ( even3App, mapOddApp, mapOddPrimApp, + + -- * Metadata about the examples. + even3MainName, + even3MainExpected, + mapOddMainName, + mapOddMainExpected, + mapOddPrimMainName, + mapOddPrimMainExpected, ) where import Foreword hiding ( @@ -64,6 +72,7 @@ import Primer.Builtins.DSL ( nat, ) import Primer.Core ( + Expr, GVarName, ID, ModuleName (unModuleName), @@ -81,6 +90,7 @@ import Primer.Core.DSL ( con0, con1, create, + create', emptyHole, gvar, gvar', @@ -360,10 +370,10 @@ evenOddModule modName = , nextID ) --- | A program whose @main@ asks whether 3 is even. -even3Prog :: (Prog, ID, NameCounter) -even3Prog = +even3 :: (Prog, ID, NameCounter, GVarName, Expr) +even3 = let modName = mkSimpleModuleName "Even3" + mainName = "even 3?" ((builtinMod, defs), nextID) = create $ do builtinModule' <- builtinModule (_, evenDef) <- even modName @@ -372,7 +382,7 @@ even3Prog = type_ <- tcon B.tBool term <- gvar (qualifyName modName "even") `app` con1 B.cSucc (con1 B.cSucc $ con1 B.cSucc $ con0 B.cZero) pure $ DefAST $ ASTDef term type_ - let globs = [("even", evenDef), ("odd", oddDef), ("even 3?", even3Def)] + let globs = [("even", evenDef), ("odd", oddDef), (mainName, even3Def)] pure (builtinModule', globs) in ( defaultProg { progImports = [builtinMod] @@ -386,12 +396,18 @@ even3Prog = } , nextID , toEnum 0 + , qualifyName modName mainName + , create' $ con0 B.cFalse ) --- | A program whose @main@ 'map's 'odd' over a list of 'B.tNat'. -mapOddProg :: Int -> (Prog, ID, NameCounter) -mapOddProg len = +-- | A program whose @main@ asks whether 3 is even. +even3Prog :: (Prog, ID, NameCounter) +even3Prog = prog even3 + +mapOdd :: Int -> (Prog, ID, NameCounter, GVarName, Expr) +mapOdd len = let modName = mkSimpleModuleName "MapOdd" + mainName = "mapOdd" ((builtinMod, defs), nextID) = create $ do builtinModule' <- builtinModule (_, evenDef) <- even modName @@ -402,7 +418,7 @@ mapOddProg len = term <- gvar mapName `aPP` tcon B.tNat `aPP` tcon B.tBool `app` gvar oddName `app` lst type_ <- tcon B.tList `tapp` tcon B.tBool pure $ DefAST $ ASTDef term type_ - let globs = [("even", evenDef), ("odd", oddDef), ("map", mapDef), ("mapOdd", mapOddDef)] + let globs = [("even", evenDef), ("odd", oddDef), ("map", mapDef), (mainName, mapOddDef)] pure (builtinModule', globs) in ( defaultProg { progImports = [builtinMod] @@ -416,14 +432,18 @@ mapOddProg len = } , nextID , toEnum 0 + , qualifyName modName mainName + , create' $ con B.cCons [con0 B.cFalse, con B.cCons [con0 B.cTrue, con B.cCons [con0 B.cFalse, con B.cCons [con0 B.cTrue, con B.cNil []]]]] ) --- | A program whose @main@ 'map's 'odd' over a list of 'P.tInt'. --- This is the same as 'mapOddProg', except it works over primitive --- integers, rather than inductively-defined naturals. -mapOddPrimProg :: Int -> (Prog, ID, NameCounter) -mapOddPrimProg len = +-- | A program whose @main@ 'map's 'odd' over a list of 'B.tNat'. +mapOddProg :: Int -> (Prog, ID, NameCounter) +mapOddProg = prog . mapOdd + +mapOddPrim :: Int -> (Prog, ID, NameCounter, GVarName, Expr) +mapOddPrim len = let modName = mkSimpleModuleName "MapOdd" + mainName = "mapOdd" ((builtinMod, primitiveMod, defs), nextID) = create $ do builtinModule' <- builtinModule primitiveModule' <- primitiveModule @@ -444,7 +464,7 @@ mapOddPrimProg len = let lst = list_ $ take len $ int <$> [0 ..] term <- gvar mapName `aPP` tcon P.tInt `aPP` tcon B.tBool `app` gvar oddName `app` lst pure $ DefAST $ ASTDef term type_ - let globs = [("odd", oddDef), ("map", mapDef), ("mapOdd", mapOddDef)] + let globs = [("odd", oddDef), ("map", mapDef), (mainName, mapOddDef)] pure (builtinModule', primitiveModule', globs) in ( defaultProg { progImports = [builtinMod, primitiveMod] @@ -458,8 +478,16 @@ mapOddPrimProg len = } , nextID , toEnum 0 + , qualifyName modName mainName + , create' $ con B.cCons [con0 B.cFalse, con B.cCons [con0 B.cTrue, con B.cCons [con0 B.cFalse, con B.cCons [con0 B.cTrue, con B.cNil []]]]] ) +-- | A program whose @main@ 'map's 'odd' over a list of 'P.tInt'. +-- This is the same as 'mapOddProg', except it works over primitive +-- integers, rather than inductively-defined naturals. +mapOddPrimProg :: Int -> (Prog, ID, NameCounter) +mapOddPrimProg = prog . mapOddPrim + -- | A "bad" version of 'even3Prog' where the type of @even 3?@ is -- specified as @Nat@. badEven3Prog :: (Prog, ID, NameCounter) @@ -551,3 +579,36 @@ mapOddPrimApp :: App mapOddPrimApp = let (p, id_, nc) = mapOddPrimProg 4 in mkApp id_ nc p + +prog :: (Prog, ID, NameCounter, GVarName, Expr) -> (Prog, ID, NameCounter) +prog f = + let (p, i, n, _, _) = f + in (p, i, n) + +main :: (Prog, ID, NameCounter, GVarName, Expr) -> GVarName +main f = + let (_, _, _, m, _) = f + in m + +expected :: (Prog, ID, NameCounter, GVarName, Expr) -> Expr +expected f = + let (_, _, _, _, expect) = f + in expect + +even3MainName :: GVarName +even3MainName = main even3 + +even3MainExpected :: Expr +even3MainExpected = expected even3 + +mapOddMainName :: GVarName +mapOddMainName = main $ mapOdd 4 + +mapOddMainExpected :: Expr +mapOddMainExpected = expected $ mapOdd 4 + +mapOddPrimMainName :: GVarName +mapOddPrimMainName = main $ mapOddPrim 4 + +mapOddPrimMainExpected :: Expr +mapOddPrimMainExpected = expected $ mapOddPrim 4 diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 462002b6a..d40876e58 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -87,12 +87,13 @@ import Primer.App ( handleQuestion, nextProgID, progAllDefs, - progAllTypeDefs, progAllTypeDefsMeta, progCxt, + progDefMap, progImports, progModules, progSmartHoles, + progTypeDefMap, redoLogEmpty, runEditAppM, undoLogEmpty, @@ -660,7 +661,7 @@ genAction :: ) genAction l a = do let allTypes = map (forgetTypeDefMetadata . snd) $ progAllTypeDefsMeta $ appProg a - allDefs = map snd $ progAllDefs $ appProg a + allDefs = progDefMap $ appProg a (loc, mut, s) <- genLoc a let acts = case (loc, s) of (Left (_, def), SelectionTypeDef (TypeDefSelection defName Nothing)) -> @@ -718,14 +719,14 @@ toProgAction l a (def, loc, action) = do Available.NoInput act' -> do progActs <- either (\e -> annotateShow e >> failure) pure - $ toProgActionNoInput (map snd $ progAllDefs $ appProg a) def' loc act' + $ 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 - (map snd $ progAllTypeDefs $ appProg a) - (map snd $ progAllDefs $ appProg a) + (progTypeDefMap $ appProg a) + (progDefMap $ appProg a) (progCxt $ appProg a) l def' diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 623a263a4..17599bb35 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -61,8 +61,8 @@ import Primer.App ( newEmptyProg', newProg', nextProgID, - progAllDefs, progAllModules, + progDefMap, ) import Primer.App qualified as App import Primer.Builtins ( @@ -1621,7 +1621,7 @@ unit_sh_lost_id = -- * Utilities findGlobalByName :: Prog -> GVarName -> Maybe Def -findGlobalByName p n = Map.lookup n . fmap snd $ progAllDefs p +findGlobalByName p n = Map.lookup n $ progDefMap p -- We use a program with two defs: "main" and "other" defaultEmptyProg :: MonadFresh ID m => m Prog diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs index e151a6a5f..ce087dfe9 100644 --- a/primer/test/Tests/EvalFullInterp.hs +++ b/primer/test/Tests/EvalFullInterp.hs @@ -900,10 +900,10 @@ unit_prim_partial_map = -- unit_interp_even3 :: Assertion -- unit_interp_even3 = -- let (prog, _, _) = even3Prog --- types = allTypes prog --- defs = allDefs prog --- expr = create1 $ gvar $ gvn ["Even3"] "even 3?" --- expect = create1 $ con0 cFalse +-- types = progTypeDefMap prog +-- defs = progDefMap prog +-- expr = create1 $ gvar even3MainName +-- expect = forgetMetadata even3MainExpected -- in do -- s <- evalFullTest types defs Chk expr -- s @?= Right expect @@ -911,9 +911,9 @@ unit_prim_partial_map = -- unit_interp_mapOdd2 :: Assertion -- unit_interp_mapOdd2 = -- let (prog, _, _) = mapOddProg 2 --- types = allTypes prog --- defs = allDefs prog --- expr = create1 $ gvar $ gvn ["MapOdd"] "mapOdd" +-- types = progTypeDefMap prog +-- defs = progDefMap prog +-- expr = create1 $ gvar mapOddMainName -- expect = create1 $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]] -- in do -- s <- evalFullTest types defs Chk expr @@ -922,9 +922,9 @@ unit_prim_partial_map = -- unit_interp_mapOddPrim2 :: Assertion -- unit_interp_mapOddPrim2 = -- let (prog, _, _) = mapOddPrimProg 2 --- types = allTypes prog --- defs = allDefs prog --- expr = create1 $ gvar $ gvn ["MapOdd"] "mapOdd" +-- types = progTypeDefMap prog +-- defs = progDefMap prog +-- expr = create1 $ gvar mapOddPrimMainName -- expect = create1 $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]] -- in do -- s <- evalFullTest types defs Chk expr @@ -982,7 +982,7 @@ unit_handleEvalBoundedInterpRequest_modules = -- unit_handleEvalInterpRequest_even3 :: Assertion -- unit_handleEvalInterpRequest_even3 = -- let test = do --- expr <- gvar $ gvn ["Even3"] "even 3?" +-- expr <- gvar even3MainName -- (EvalInterpRespNormal e) <- -- readerToState -- $ handleEvalInterpRequest @@ -990,8 +990,7 @@ unit_handleEvalBoundedInterpRequest_modules = -- { expr = expr -- , dir = Chk -- } --- expect <- con0 cFalse --- pure $ e ~= expect +-- pure $ e ~= even3MainExpected -- in runAppTestM even3App test <&> fst >>= \case -- Left err -> assertFailure $ show err -- Right assertion -> assertion @@ -999,7 +998,7 @@ unit_handleEvalBoundedInterpRequest_modules = -- unit_handleEvalInterpRequest_mapOdd :: Assertion -- unit_handleEvalInterpRequest_mapOdd = -- let test = do --- expr <- gvar $ gvn ["MapOdd"] "mapOdd" +-- expr <- gvar mapOddMainName -- (EvalInterpRespNormal e) <- -- readerToState -- $ handleEvalInterpRequest @@ -1007,9 +1006,7 @@ unit_handleEvalBoundedInterpRequest_modules = -- { expr = expr -- , dir = Chk -- } --- -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3] --- expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] --- pure $ e ~= expect +-- pure $ e ~= mapOddMainExpected -- in runAppTestM mapOddApp test <&> fst >>= \case -- Left err -> assertFailure $ show err -- Right assertion -> assertion @@ -1017,7 +1014,7 @@ unit_handleEvalBoundedInterpRequest_modules = -- unit_handleEvalInterpRequest_mapOddPrim :: Assertion -- unit_handleEvalInterpRequest_mapOddPrim = -- let test = do --- expr <- gvar $ gvn ["MapOdd"] "mapOdd" +-- expr <- gvar mapOddPrimMainName -- (EvalInterpRespNormal e) <- -- readerToState -- $ handleEvalInterpRequest @@ -1025,9 +1022,7 @@ unit_handleEvalBoundedInterpRequest_modules = -- { expr = expr -- , dir = Chk -- } --- -- Note that the 'mapOddPrimApp' includes a program runs @mapOdd@ over a list of [0..3] --- expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] --- pure $ e ~= expect +-- pure $ e ~= mapOddPrimMainExpected -- in runAppTestM mapOddPrimApp test <&> fst >>= \case -- Left err -> assertFailure $ show err -- Right assertion -> assertion @@ -1083,7 +1078,7 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = $ EvalBoundedInterpReq { expr = foo , dir = Chk - , timeout = MicroSec 200 + , timeout = MicroSec 10_000 } expect <- con0 cFalse pure $ case resp of @@ -1108,7 +1103,7 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = -- unit_handleEvalBoundedInterpRequest_even3 :: Assertion -- unit_handleEvalBoundedInterpRequest_even3 = -- let test = do --- expr <- gvar $ gvn ["Even3"] "even 3?" +-- expr <- gvar even3MainName -- resp <- -- readerToState -- $ handleEvalBoundedInterpRequest @@ -1117,10 +1112,9 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = -- , dir = Chk -- , timeout = MicroSec 10_000 -- } --- expect <- con0 cFalse -- pure $ case resp of -- EvalBoundedInterpRespFailed err -> assertFailure $ show err --- EvalBoundedInterpRespNormal e -> e ~= expect +-- EvalBoundedInterpRespNormal e -> e ~= even3MainExpected -- in runAppTestM even3App test <&> fst >>= \case -- Left err -> assertFailure $ show err -- Right assertion -> assertion @@ -1128,7 +1122,7 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = -- unit_handleEvalBoundedInterpRequest_mapOdd :: Assertion -- unit_handleEvalBoundedInterpRequest_mapOdd = -- let test = do --- expr <- gvar $ gvn ["MapOdd"] "mapOdd" +-- expr <- gvar mapOddMainName -- resp <- -- readerToState -- $ handleEvalBoundedInterpRequest @@ -1137,11 +1131,9 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = -- , dir = Chk -- , timeout = MicroSec 10_000 -- } --- -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3] --- expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] -- pure $ case resp of -- EvalBoundedInterpRespFailed err -> assertFailure $ show err --- EvalBoundedInterpRespNormal e -> e ~= expect +-- EvalBoundedInterpRespNormal e -> e ~= mapOddMainExpected -- in runAppTestM mapOddApp test <&> fst >>= \case -- Left err -> assertFailure $ show err -- Right assertion -> assertion @@ -1149,7 +1141,7 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = -- unit_handleEvalBoundedInterpRequest_mapOddPrim :: Assertion -- unit_handleEvalBoundedInterpRequest_mapOddPrim = -- let test = do --- expr <- gvar $ gvn ["MapOdd"] "mapOdd" +-- expr <- gvar mapOddPrimMainName -- resp <- -- readerToState -- $ handleEvalBoundedInterpRequest @@ -1158,11 +1150,9 @@ unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type = -- , dir = Chk -- , timeout = MicroSec 10_000 -- } --- -- Note that the 'mapOddPrimApp' includes a program runs @mapOdd@ over a list of [0..3] --- expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] -- pure $ case resp of -- EvalBoundedInterpRespFailed err -> assertFailure $ show err --- EvalBoundedInterpRespNormal e -> e ~= expect +-- EvalBoundedInterpRespNormal e -> e ~= mapOddPrimMainExpected -- in runAppTestM mapOddPrimApp test <&> fst >>= \case -- Left err -> assertFailure $ show err -- Right assertion -> assertion diff --git a/primer/test/Tests/EvalFullStep.hs b/primer/test/Tests/EvalFullStep.hs index 839883324..1a377956d 100644 --- a/primer/test/Tests/EvalFullStep.hs +++ b/primer/test/Tests/EvalFullStep.hs @@ -16,11 +16,11 @@ import Optics import Primer.App ( EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullOptions, evalFullReqExpr), EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut), - allDefs, - allTypes, handleEvalFullRequest, importModules, newEmptyApp, + progDefMap, + progTypeDefMap, ) import Primer.Builtins ( boolDef, @@ -51,9 +51,15 @@ import Primer.Eval import Primer.EvalFullStep import Primer.Examples ( even3App, + even3MainExpected, + even3MainName, even3Prog, mapOddApp, + mapOddMainExpected, + mapOddMainName, mapOddPrimApp, + mapOddPrimMainExpected, + mapOddPrimMainName, mapOddPrimProg, mapOddProg, ) @@ -107,7 +113,6 @@ import Primer.Test.TestM ( import Primer.Test.Util ( assertNoSevereLogs, failWhenSevereLogs, - gvn, primDefs, testNoSevereLogs, zeroIDs, @@ -1696,10 +1701,10 @@ unit_prim_partial_map = unit_evalFull_even3 :: Assertion unit_evalFull_even3 = let (prog, maxID, _) = even3Prog - types = allTypes prog - defs = allDefs prog - (expr, _) = create $ gvar $ gvn ["Even3"] "even 3?" - (expect, _) = create $ con0 cFalse + types = progTypeDefMap prog + defs = progDefMap prog + (expr, _) = create $ gvar even3MainName + expect = even3MainExpected in do s <- evalFullTest maxID types defs 100 Chk expr s <~==> Right expect @@ -1707,9 +1712,9 @@ unit_evalFull_even3 = unit_evalFull_mapOdd2 :: Assertion unit_evalFull_mapOdd2 = let (prog, maxID, _) = mapOddProg 2 - types = allTypes prog - defs = allDefs prog - (expr, _) = create $ gvar $ gvn ["MapOdd"] "mapOdd" + types = progTypeDefMap prog + defs = progDefMap prog + (expr, _) = create $ gvar mapOddMainName (expect, _) = create $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]] in do s <- evalFullTest maxID types defs 200 Chk expr @@ -1718,9 +1723,9 @@ unit_evalFull_mapOdd2 = unit_evalFull_mapOddPrim2 :: Assertion unit_evalFull_mapOddPrim2 = let (prog, maxID, _) = mapOddPrimProg 2 - types = allTypes prog - defs = allDefs prog - (expr, _) = create $ gvar $ gvn ["MapOdd"] "mapOdd" + types = progTypeDefMap prog + defs = progDefMap prog + (expr, _) = create $ gvar mapOddPrimMainName (expect, _) = create $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]] in do s <- evalFullTest maxID types defs 200 Chk expr @@ -1792,7 +1797,7 @@ unit_handleEvalFullRequest_modules_scrutinize_imported_type = unit_handleEvalFullRequest_even3 :: Assertion unit_handleEvalFullRequest_even3 = let test = do - expr <- gvar $ gvn ["Even3"] "even 3?" + expr <- gvar even3MainName resp <- readerToState $ handleEvalFullRequest @@ -1802,10 +1807,9 @@ unit_handleEvalFullRequest_even3 = , evalFullMaxSteps = 200 , evalFullOptions = UnderBinders } - expect <- con0 cFalse pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" - EvalFullRespNormal e -> e ~= expect + EvalFullRespNormal e -> e ~= even3MainExpected in runAppTestM even3App test <&> fst >>= \case Left err -> assertFailure $ show err Right assertion -> assertion @@ -1813,7 +1817,7 @@ unit_handleEvalFullRequest_even3 = unit_handleEvalFullRequest_mapOdd :: Assertion unit_handleEvalFullRequest_mapOdd = let test = do - expr <- gvar $ gvn ["MapOdd"] "mapOdd" + expr <- gvar mapOddMainName resp <- readerToState $ handleEvalFullRequest @@ -1823,11 +1827,9 @@ unit_handleEvalFullRequest_mapOdd = , evalFullMaxSteps = 400 , evalFullOptions = UnderBinders } - -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3] - expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" - EvalFullRespNormal e -> e ~= expect + EvalFullRespNormal e -> e ~= mapOddMainExpected in runAppTestM mapOddApp test <&> fst >>= \case Left err -> assertFailure $ show err Right assertion -> assertion @@ -1835,7 +1837,7 @@ unit_handleEvalFullRequest_mapOdd = unit_handleEvalFullRequest_mapOddPrim :: Assertion unit_handleEvalFullRequest_mapOddPrim = let test = do - expr <- gvar $ gvn ["MapOdd"] "mapOdd" + expr <- gvar mapOddPrimMainName resp <- readerToState $ handleEvalFullRequest @@ -1845,11 +1847,9 @@ unit_handleEvalFullRequest_mapOddPrim = , evalFullMaxSteps = 300 , evalFullOptions = UnderBinders } - -- Note that the 'mapOddPrimApp' includes a program runs @mapOddPrim@ over a list of [0..3] - expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]] pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" - EvalFullRespNormal e -> e ~= expect + EvalFullRespNormal e -> e ~= mapOddPrimMainExpected in runAppTestM mapOddPrimApp test <&> fst >>= \case Left err -> assertFailure $ show err Right assertion -> assertion diff --git a/primer/test/Tests/Shadowing.hs b/primer/test/Tests/Shadowing.hs index 14611129e..3fff9fd2d 100644 --- a/primer/test/Tests/Shadowing.hs +++ b/primer/test/Tests/Shadowing.hs @@ -12,7 +12,14 @@ import Hedgehog (annotateShow, discard, failure, forAll, label, success, (===)) import Hedgehog.Gen qualified as Gen import Hedgehog.Range qualified as Range import Primer.Action.Available (Action (NoInput), NoInputAction (LetToRec)) -import Primer.App (App, appProg, handleEditRequest, progAllDefs, progAllTypeDefs, runEditAppM) +import Primer.App ( + App, + appProg, + handleEditRequest, + progDefMap, + progTypeDefMap, + runEditAppM, + ) import Primer.Core ( Expr, Expr' (Case, Var), @@ -299,8 +306,8 @@ tasty_available_actions_shadow = withDiscards 2000 noShadowingApp :: App -> [(Either (TypeDef () ()) Def, Shadowing)] noShadowingApp a = let p = appProg a - tds = snd <$> toList (progAllTypeDefs p) - ds = snd <$> toList (progAllDefs p) + tds = toList (progTypeDefMap p) + ds = toList (progDefMap p) in map (\d -> (Left d, noShadowingTypeDef d)) tds <> map (\d -> (Right d, noShadowingDef d)) ds where combineShadow ShadowingNotExists s = s