diff --git a/primer/gen/Primer/Gen/Core/Raw.hs b/primer/gen/Primer/Gen/Core/Raw.hs index 5967dd4ba..e01930e00 100644 --- a/primer/gen/Primer/Gen/Core/Raw.hs +++ b/primer/gen/Primer/Gen/Core/Raw.hs @@ -102,7 +102,13 @@ genValConName :: MonadGen m => m ValConName genValConName = qualifyName <$> genModuleName <*> genName genCon :: ExprGen Expr -genCon = Con <$> genMeta <*> genValConName +genCon = + Gen.recursive + Gen.choice + [genCon' (pure [])] + [genCon' (Gen.list (Range.linear 0 5) genExpr)] + where + genCon' tms = Con <$> genMeta <*> genValConName <*> tms genLam :: ExprGen Expr genLam = Lam <$> genMeta <*> genLVarName <*> genExpr diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs index 3bcdcd922..ea26c7103 100644 --- a/primer/gen/Primer/Gen/Core/Typed.hs +++ b/primer/gen/Primer/Gen/Core/Typed.hs @@ -66,7 +66,7 @@ import Primer.Gen.Core.Raw (genLVarName, genModuleName, genName, genTyVarName) import Primer.Module (Module (..)) import Primer.Name (Name, NameCounter, freshName, unName, unsafeMkName) import Primer.Refine (Inst (InstAPP, InstApp, InstUnconstrainedAPP), refine) -import Primer.Subst (substTy, substTys) +import Primer.Subst (substTy, substTySimul) import Primer.Test.TestM ( TestM, evalTestM, @@ -78,7 +78,6 @@ import Primer.TypeDef ( ValCon (..), typeDefKind, typeDefParameters, - valConType, ) import Primer.Typecheck ( Cxt (), @@ -86,6 +85,7 @@ import Primer.Typecheck ( TypeDefError (TDIHoleType), buildTypingContextFromModules, consistentKinds, + consistentTypes, extendLocalCxt, extendLocalCxtTy, extendLocalCxtTys, @@ -210,10 +210,11 @@ freshen fvs i n = else m -- genSyns T with cxt Γ should generate (e,S) st Γ |- e ∈ S and S ~ T (i.e. same up to holes and alpha) -genSyns :: TypeG -> GenT WT (ExprG, TypeG) +genSyns :: HasCallStack => TypeG -> GenT WT (ExprG, TypeG) genSyns ty = do + genPrimCon'' <- lift genPrimCon' genSpine' <- lift genSpine - Gen.recursive Gen.choice [genEmptyHole, genAnn] $ [genHole, genApp, genAPP, genLet] ++ catMaybes [genSpine'] + Gen.recursive Gen.choice [genEmptyHole, genAnn] $ [genHole, genApp, genAPP, genLet] ++ catMaybes [genPrimCon'', genSpine'] where genEmptyHole = pure (EmptyHole (), TEmptyHole ()) genAnn = do @@ -231,16 +232,12 @@ genSyns ty = do let locals' = map (first (Var () . LocalVarRef)) $ M.toList localTms globals <- asks globalCxt let globals' = map (first (Var () . GlobalVarRef)) $ M.toList globals - cons <- asks allCons - let cons' = map (first (Con ())) $ M.toList cons - let hsPure = locals' ++ globals' ++ cons' - primCons <- fmap (bimap (PrimCon ()) (TCon ())) <<$>> genPrimCon - let hs = map pure hsPure ++ primCons + let hs = locals' ++ globals' pure $ if null hs then Nothing else Just $ do - (he, hT) <- Gen.choice hs + (he, hT) <- Gen.element hs cxt <- ask runExceptT (refine cxt ty hT) >>= \case -- This error case indicates a bug. Crash and fail loudly! @@ -249,7 +246,7 @@ genSyns ty = do Right (Just (inst, instTy)) -> do (sb, is) <- genInstApp inst let f e = \case Right tm -> App () e tm; Left ty' -> APP () e ty' - Just . (foldl' f he is,) <$> substTys sb instTy + Just . (foldl' f he is,) <$> substTySimul sb instTy genApp = do s <- genWTType KType (f, fTy) <- genSyns (TFun () s ty) @@ -268,6 +265,10 @@ genSyns ty = do aTy <- genWTType ak Just . (APP () s aTy,) <$> substTy a aTy instTy _ -> pure Nothing + genPrimCon' = do + genPrimCon <&> map (bimap (fmap $ PrimCon ()) (TCon ())) <&> filter (consistentTypes ty . snd) <&> \case + [] -> Nothing + gens -> Just $ Gen.choice $ (\(g, t) -> (,t) <$> g) <$> gens genLet = Gen.choice [ -- let @@ -322,42 +323,94 @@ justT g = Gen.sized $ \s -> Gen.justT $ Gen.resize s g -- If @genInstApp insts = (sub, apps)@, then: -- - @apps@ is the same length as @insts@, and the entries correspond in the way -- documented by 'refine'. --- - the length of @sub@ is the number of 'InstUnconstrainedApp' in @inst@, and --- these entries correspond. --- - thus if @insts !! n = InstUnconstrainedAPP a k@ and this is the @m@th --- @InstUnconstrainedAPP@, then (for some type @t@ of kind @k@) --- @sub !! m = (a, t)@ and @apps !! n = Left t@. +-- - the size of @sub@ is the number of 'InstUnconstrainedApp' in @inst@, and +-- these entries correspond (by name). +-- - thus if @insts !! n = InstUnconstrainedAPP a k@, then (for some type @t@ of kind @k@) +-- @sub ! a = t@ and @apps !! n = Left t@. -- - @sub@ is idempotent, and @apps@ do not refer to these names. I.e. the names -- in @InstUnconstrainedAPP@ do not appear free in @apps@ or the rhs of @sub@. -genInstApp :: [Inst] -> GenT WT ([(TyVarName, Type' ())], [Either TypeG ExprG]) -genInstApp = reify [] +genInstApp :: [Inst] -> GenT WT (Map TyVarName (Type' ()), [Either TypeG ExprG]) +genInstApp = reify mempty where reify sb = \case - [] -> pure (reverse sb, []) - InstApp t : is -> (\a -> second (Right a :)) <$> (substTys sb t >>= genChk) <*> reify sb is - InstAPP t : is -> (\t' -> second (Left t' :)) <$> substTys sb t <*> reify sb is - InstUnconstrainedAPP v k : is -> genWTType k >>= \t' -> second (Left t' :) <$> reify ((v, t') : sb) is + [] -> pure (sb, []) + InstApp t : is -> (\a -> second (Right a :)) <$> (substTySimul sb t >>= genChk) <*> reify sb is + InstAPP t : is -> (\t' -> second (Left t' :)) <$> substTySimul sb t <*> reify sb is + InstUnconstrainedAPP v k : is -> genWTType k >>= \t' -> second (Left t' :) <$> reify (M.insert v t' sb) is genSyn :: GenT WT (ExprG, TypeG) -- Note that genSyns will generate things consistent with the given type, i.e. -- of any type genSyn = genSyns (TEmptyHole ()) -allCons :: Cxt -> M.Map ValConName (Type' ()) +-- TODO (saturated constructors) note that this allCons function only works for +-- synthesisable constructors which store their indices + +-- | Returns each ADT constructor's name along with its "telescope" of arguments: +-- - the parameters of the datatype (which are type arguments to the constructor) +-- - the types of its fields (and the names of the parameters scope over this) +-- - the ADT it belongs to (if @(c,([(p1,k1),(p2,k2)],_,T))@ is returned, then @c [A,B] _ ∈ T A B@) +allCons :: Cxt -> M.Map ValConName ([(TyVarName, Kind)], [Type' ()], TyConName) allCons cxt = M.fromList $ concatMap (uncurry consForTyDef) $ M.assocs $ typeDefs cxt where consForTyDef tc = \case - TypeDefAST td -> map (\vc -> (valConName vc, valConType tc td vc)) (astTypeDefConstructors td) + TypeDefAST td -> + map + ( \vc -> + ( valConName vc + , + ( astTypeDefParameters td + , valConArgs vc + , tc + ) + ) + ) + (astTypeDefConstructors td) TypeDefPrim _ -> [] genChk :: TypeG -> GenT WT ExprG genChk ty = do cse <- lift case_ abst' <- lift abst - let rec = genLet : catMaybes [lambda, abst', cse] + genCon' <- lift genCon + let rec = genLet : catMaybes [genCon', lambda, abst', cse] Gen.recursive Gen.choice [emb] rec where emb = fst <$> genSyns ty + genCon = + instantiateValCons ty >>= \case + Left TDIHoleType -> + asks allCons <&> \case + -- We have no constraints, generate any ctor + m | null m -> Nothing + cons -> Just $ do + let cons' = + M.toList cons <&> \(c, (params, fldsTys0, _)) -> do + indicesMap <- for params $ \(p, k) -> (p,) <$> genWTType k + -- NB: it is vital to use simultaneous substitution here. + -- Consider the case where we have a local type variable @a@ + -- in scope, say because we have already generated a + -- @Λa. ...@, and we are considering the case of the @MkPair@ + -- constructor for the type @data Pair a b = MkPair a b@. + -- The two "a"s (locally Λ-bound and from the typedef) refer + -- to completely different things. We may well generate the + -- substitution [a :-> Bool, b :-> a]. We must then say that + -- the fields of the @MkPair@ constructor are @Bool@ and (the + -- locally-bound) @a@. We must do a simultaneous substitution + -- to avoid substituting @b@ into @a@ and then further into + -- @Bool@. + fldsTys <- traverse (substTySimul $ M.fromList indicesMap) fldsTys0 + flds <- traverse (Gen.small . genChk) fldsTys + pure $ Con () c flds + Gen.choice cons' + 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 lambda = matchArrowType ty <&> \(sTy, tTy) -> do n <- genLVarNameAvoiding [tTy, sTy] @@ -572,7 +625,7 @@ genCxtExtendingLocal = do -- We have to be careful to only generate primitive constructors which are -- in scope (i.e. their type is in scope) -genPrimCon :: forall mc mg. (MonadReader Cxt mc, MonadGen mg) => mc [mg (PrimCon, TyConName)] +genPrimCon :: forall mc mg. (MonadReader Cxt mc, MonadGen mg) => mc [(mg PrimCon, TyConName)] genPrimCon = catMaybes <$> sequence [genChar, genInt] where genChar = whenInScope PrimChar 'a' Gen.unicode @@ -580,12 +633,12 @@ genPrimCon = catMaybes <$> sequence [genChar, genInt] genInt = whenInScope PrimInt 0 $ Gen.integral $ Range.linear (-intBound) intBound -- The 'tst' is arbitrary, only used for checking if the primcon is in scope -- and does not affect the generator. - whenInScope :: (a -> PrimCon) -> a -> mg a -> mc (Maybe (mg (PrimCon, TyConName))) + whenInScope :: (a -> PrimCon) -> a -> mg a -> mc (Maybe (mg PrimCon, TyConName)) whenInScope f tst g = do s <- asks $ primConInScope (f tst) pure $ case s of (False, _) -> Nothing - (True, tc) -> Just $ (\x -> (f x, tc)) <$> g + (True, tc) -> Just $ (,tc) $ f <$> g -- This ensures that when we modify the constructors of `PrimCon` (i.e. we add/remove primitive types), -- we are alerted that we need to update this generator. _ = \case diff --git a/primer/primer.cabal b/primer/primer.cabal index a73eb91d1..b80582a9e 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -108,6 +108,7 @@ library build-depends: , aeson >=2.0 && <2.2 + , assoc ^>=1.0.2 , base >=4.12 && <4.17.0 , bytestring >=0.10.8.2 && <0.12.0 , containers >=0.6.0.1 && <0.7.0 diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index be3faec0d..9ae57aff8 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -708,11 +708,11 @@ viewTreeExpr e0 = case e0 of , childTrees = [viewTreeExpr e, viewTreeType t] , rightChild = Nothing } - Con _ s -> + Con _ c tmApps -> Tree { nodeId - , body = TextBody $ RecordPair Flavor.Con $ globalName s - , childTrees = [] + , body = TextBody $ RecordPair Flavor.Con $ globalName c + , childTrees = map viewTreeExpr tmApps , rightChild = Nothing } Lam _ s e -> @@ -784,38 +784,28 @@ viewTreeExpr e0 = case e0 of -- and don't contain non-numerical characters boxId = nodeId <> "P" <> show i patternRootId = boxId <> "B" - patternBindAppID id = show id <> "A" in Tree { nodeId = boxId , body = BoxBody . RecordPair Flavor.Pattern $ - foldl' - ( \t (Bind m v) -> - let id = m ^. _id - in Tree - { nodeId = patternBindAppID id - , body = NoBody Flavor.PatternApp - , childTrees = - [ t - , Tree - { nodeId = show id - , body = TextBody $ RecordPair Flavor.PatternBind $ localName v - , childTrees = [] - , rightChild = Nothing - } - ] - , rightChild = Nothing - } - ) - ( Tree - { nodeId = patternRootId - , body = TextBody $ RecordPair Flavor.PatternCon $ globalName con - , childTrees = [] - , rightChild = Nothing - } - ) - binds + ( Tree + { nodeId = patternRootId + , body = TextBody $ RecordPair Flavor.PatternCon $ globalName con + , childTrees = + map + ( \(Bind m v) -> + Tree + { nodeId = show $ getID m + , body = TextBody $ RecordPair Flavor.PatternBind $ localName v + , childTrees = [] + , rightChild = Nothing + } + ) + binds + , rightChild = Nothing + } + ) , childTrees = [viewTreeExpr rhs] , rightChild = Nothing } diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 5f25d90d6..48d6cd2cf 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -19,13 +19,14 @@ import Foreword hiding (mod) import Control.Monad.Fresh (MonadFresh) import Data.Aeson (Value) +import Data.Bifunctor.Swap qualified as Swap import Data.Generics.Product (typed) import Data.List (findIndex) import Data.List.NonEmpty qualified as NE import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Text qualified as T -import Optics (set, (%), (?~), (^.), (^?), _Just) +import Optics (set, to, (%), (?~), (^.), (^?), _Just) import Primer.Action.Actions (Action (..), Movement (..), QualifiedText) import Primer.Action.Available qualified as Available import Primer.Action.Errors (ActionError (..)) @@ -67,6 +68,7 @@ import Primer.Core.DSL ( branch, case_, con, + conSat, emptyHole, hole, lAM, @@ -346,7 +348,6 @@ applyAction' a = case a of RemoveAnn -> termAction removeAnn "there are no annotations in types" ConstructLam x -> termAction (constructLam x) "cannot construct function in type" ConstructLAM x -> termAction (constructLAM x) "cannot construct function in type" - ConstructCon c -> termAction (constructCon c) "cannot construct con in type" ConstructPrim p -> termAction (constructPrim p) "cannot construct primitive literal in type" ConstructSaturatedCon c -> termAction (constructSatCon c) "cannot construct con in type" ConstructRefinedCon c -> termAction (constructRefinedCon c) "cannot construct con in type" @@ -397,6 +398,12 @@ moveExpr m@(Branch c) z | Case _ _ brs <- target z = Just z' -> pure z' Nothing -> throwError $ CustomFailure (Move m) "internal error: movement failed, even though branch exists" moveExpr m@(Branch _) _ = throwError $ CustomFailure (Move m) "Move-to-branch failed: this is not a case expression" +moveExpr m@(ConChild n) z | Con{} <- target z = + -- 'down' moves into the first argument, 'right' steps through the various arguments + case foldr (\_ z' -> right =<< z') (down z) [1 .. n] of + Just z' -> pure z' + Nothing -> throwError $ CustomFailure (Move m) "Move-to-constructor-argument failed: no such argument" +moveExpr m@(ConChild _) _ = throwError $ CustomFailure (Move m) "Move-to-constructor-argument failed: this is not a constructor" moveExpr Child2 z | Case{} <- target z = throwError $ CustomFailure (Move Child2) "cannot move to 'Child2' of a case: use Branch instead" @@ -405,10 +412,11 @@ moveExpr m z = move m z -- | Apply a movement to a zipper moveType :: ActionM m => Movement -> TypeZ -> m TypeZ moveType m@(Branch _) _ = throwError $ CustomFailure (Move m) "Move-to-branch unsupported in types (there are no cases in types!)" +moveType m@(ConChild _) _ = throwError $ CustomFailure (Move m) "Move-to-constructor-argument unsupported in types (type constructors do not directly store their arguments)" moveType m z = move m z -- | Apply a movement to a generic zipper - does not support movement to a case --- branch +-- branch, or into an argument of a constructor move :: forall m za a. (ActionM m, IsZipper za a, HasID za) => Movement -> za -> m za move m z = do mz' <- move' m z @@ -421,6 +429,7 @@ move m z = do move' Child1 = pure . down move' Child2 = pure . (down >=> right) move' (Branch _) = const $ throwError $ InternalFailure "move does not support Branch moves" + move' (ConChild _) = const $ throwError $ InternalFailure "move does not support Constructor argument moves" setMetadata :: (IsZipper za a, HasMetadata a) => Value -> za -> za setMetadata d z = z & _target % _metadata ?~ d @@ -500,14 +509,19 @@ insertRefinedVar x ast = do getVarType ast x >>= \case Left err -> throwError $ RefineError $ Right err Right t -> pure (var x, t) - let tgtTyCache = maybeTypeOf $ target ast -- our Cxt in the monad does not care about the local context, we have to extract it from the zipper. -- See https://github.com/hackworthltd/primer/issues/11 -- We only care about the type context for refine let (tycxt, _) = localVariablesInScopeExpr (Left ast) cxt <- asks $ TC.extendLocalCxtTys tycxt + tgtTy <- getTypeCache $ target ast case target ast of - EmptyHole{} -> flip replace ast <$> mkRefinedApplication cxt v vTy tgtTyCache + EmptyHole{} -> + getRefinedApplications cxt vTy tgtTy >>= \case + -- See Note [No valid refinement] + Nothing -> flip replace ast <$> hole v + Just as -> flip replace ast <$> apps' v (Swap.swap . bimap pure pure <$> as) + -- flip replace ast <$> mkRefinedApplication cxt v vTy tgtTyCache e -> throwError $ NeedEmptyHole (InsertRefinedVar x) e {- @@ -521,6 +535,41 @@ put the requested function inside a hole when we cannot find a suitable application spine. -} +getRefinedApplications :: + ( MonadError ActionError m + , MonadFresh NameCounter m + , MonadFresh ID m + ) => + TC.Cxt -> + TC.Type -> + TypeCache -> + m (Maybe [Either Type Expr]) +getRefinedApplications cxt eTy tgtTy' = do + tgtTy <- case tgtTy' of + TCChkedAt t -> pure t + TCEmb b -> pure $ tcChkedAt b + TCSynthed{} -> throwError $ RefineError $ Left "Don't have a type we were checked at" + mInst <- + runExceptT (refine cxt tgtTy eTy) >>= \case + -- Errors are only internal failures. Refinement failing is signaled with + -- a Maybe + Left err -> throwError $ InternalFailure $ show err + Right x -> pure $ fst <$> x + traverse (mapM f) mInst + where + -- Note that whilst the names in 'InstUnconstrainedAPP' scope over the + -- following 'Insts', and should be substituted with whatever the + -- 'InstUnconstrainedAPP' is instatiated to (here, 'tEmptyHole'), they + -- actually only ever appear in 'InstApp', rather than 'InstAPP' (see + -- 'Tests.Refine.tasty_scoping'). Since we ignore the type of an 'InstApp' + -- and unconditionally put a hole, we do not have to worry about doing this + -- substitution. + f = \case + InstApp _ -> Right <$> emptyHole + InstAPP a -> Left <$> generateTypeIDs a + InstUnconstrainedAPP _ _ -> Left <$> tEmptyHole + +{- mkRefinedApplication :: ActionM m => TC.Cxt -> m Expr -> TC.Type -> Maybe TypeCache -> m Expr mkRefinedApplication cxt e eTy tgtTy' = do tgtTy <- case tgtTy' of @@ -549,6 +598,7 @@ mkRefinedApplication cxt e eTy tgtTy' = do InstApp _ -> x `app` emptyHole InstAPP a -> x `aPP` generateTypeIDs a InstUnconstrainedAPP _ _ -> x `aPP` tEmptyHole +-} constructApp :: ActionM m => ExprZ -> m ExprZ constructApp ze = flip replace ze <$> app (pure (target ze)) emptyHole @@ -587,11 +637,6 @@ constructLAM mx ze = do result <- flip replace ze <$> lAM x (pure (target ze)) moveExpr Child1 result -constructCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ -constructCon c ze = case target ze of - EmptyHole{} -> flip replace ze <$> con (unsafeMkGlobalName c) - e -> throwError $ NeedEmptyHole (ConstructCon c) e - constructPrim :: ActionM m => PrimCon -> ExprZ -> m ExprZ constructPrim p ze = case target ze of EmptyHole{} -> flip replace ze <$> prim p @@ -601,41 +646,89 @@ constructSatCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ constructSatCon c ze = case target ze of -- Similar comments re smartholes apply as to insertSatVar EmptyHole{} -> do - ctorType <- - getConstructorType n >>= \case + nTmArgs <- + conInfo n >>= \case Left err -> throwError $ SaturatedApplicationError $ Left err Right t -> pure t - flip replace ze <$> mkSaturatedApplication (con n) ctorType + flip replace ze <$> conSat n (replicate nTmArgs emptyHole) e -> throwError $ NeedEmptyHole (ConstructSaturatedCon c) e where n = unsafeMkGlobalName c -getConstructorType :: +-- TODO: rename, dry (cf allCons'). Probably want to return more info so can use for refine also +conInfo :: + MonadReader TC.Cxt m => + ValConName -> + m (Either Text Int) +conInfo c = snd <<$>> getConstructorTypeAndArity c + +-- TODO: rename, improve docs +-- returns "type" of ctor, and its arity +getConstructorTypeAndArity :: MonadReader TC.Cxt m => ValConName -> - m (Either Text TC.Type) -getConstructorType c = + m (Either Text (TC.Type, Int)) +getConstructorTypeAndArity c = asks (flip lookupConstructor c . TC.typeDefs) <&> \case - Just (vc, tc, td) -> Right $ valConType tc td vc + Just (vc, tc, td) -> Right (valConType tc td vc, length $ vc.valConArgs) Nothing -> Left $ "Could not find constructor " <> show c constructRefinedCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ constructRefinedCon c ze = do let n = unsafeMkGlobalName c - cTy <- - getConstructorType n >>= \case + (cTy, numTmArgs) <- + getConstructorTypeAndArity n >>= \case Left err -> throwError $ RefineError $ Left err Right t -> pure t - let tgtTyCache = maybeTypeOf $ target ze -- our Cxt in the monad does not care about the local context, we have to extract it from the zipper. -- See https://github.com/hackworthltd/primer/issues/11 -- We only care about the type context for refine let (tycxt, _) = localVariablesInScopeExpr (Left ze) cxt <- asks $ TC.extendLocalCxtTys tycxt + tgtTy <- getTypeCache $ target ze case target ze of - EmptyHole{} -> flip replace ze <$> mkRefinedApplication cxt (con n) cTy tgtTyCache + -- TODO (saturated constructors) this use of application nodes will be rejected once full-saturation is enforced + EmptyHole{} -> do + -- TODO (saturated constructors) rather a code smell to grab the chkedAt type both here and in getRefinedApplications + let isTAppCon = tgtTy ^? _chkedAt % to TC.decomposeTAppCon % _Just + refined <- breakLR <<$>> getRefinedApplications cxt cTy tgtTy + -- If the type is not of the form 'type constructor applied to types' + -- then we give back a plain saturated constuctor. This avoids constucting + -- an unsaturated constructor in the case of inserting a @Cons@ into a hole + -- of type @List A -> List A@ + -- TODO (saturated constructors) perhaps we should eta-expand here? Should be discussed in FR + case isTAppCon *> refined of + -- TODO in the Nothing case, the inside of the hole is not synthesisable (but maybe we don't care, and rely on smartholes to fix it?), + -- (todo?: add reference to innards-of-hole-must-be-syn note from todo list "Note [Holes and bidirectionality]") + -- See Note [No valid refinement] + Nothing -> flip replace ze <$> hole (con n (replicate numTmArgs emptyHole)) + Just Nothing -> throwError $ InternalFailure "Types of constructors always have type abstractions before term abstractions" + Just (Just (_tys, tms)) -> flip replace ze <$> con n (pure <$> tms) e -> throwError $ NeedEmptyHole (ConstructRefinedCon c) e +getTypeCache :: MonadError ActionError m => Expr -> m TypeCache +getTypeCache = + maybeTypeOf <&> \case + Nothing -> throwError $ RefineError $ Left "Don't have a cached type" + Just ty -> pure ty + +-- | A view for lists where all 'Left' come before all 'Right' +breakLR :: [Either a b] -> Maybe ([a], [b]) +breakLR = + spanMaybe leftToMaybe <&> \case + (ls, rest) -> (ls,) <$> traverse rightToMaybe rest + +-- TODO/REVIEW: DRY this with primer-service/exe-replay/Main.hs + +-- | Similar to 'Data.List.span', but takes a 'Maybe' predicate. +spanMaybe :: (a -> Maybe b) -> [a] -> ([b], [a]) +spanMaybe f = go + where + go [] = ([], []) + go xxs@(x : xs) = case f x of + Just b -> first (b :) $ go xs + Nothing -> ([], xxs) + constructLet :: ActionM m => Maybe Text -> ExprZ -> m ExprZ constructLet mx ze = case target ze of EmptyHole{} -> do @@ -918,9 +1011,6 @@ toProgActionInput :: Available.InputAction -> Either ActionError [ProgAction] toProgActionInput def defName mNodeSel opt0 = \case - Available.MakeCon -> do - opt <- optGlobal - toProg [ConstructCon opt] Available.MakeConSat -> do ref <- offerRefined opt <- optGlobal diff --git a/primer/src/Primer/Action/Actions.hs b/primer/src/Primer/Action/Actions.hs index e1fa5a43c..859694298 100644 --- a/primer/src/Primer/Action/Actions.hs +++ b/primer/src/Primer/Action/Actions.hs @@ -58,8 +58,6 @@ data Action ConstructLam (Maybe Text) | -- | Construct a type abstraction "big-lambda" ConstructLAM (Maybe Text) - | -- | Put a constructor in an empty hole - ConstructCon QualifiedText | -- | Put a literal in an empty hole ConstructPrim PrimCon | -- | Put a constructor applied to a saturated spine in an empty hole diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index 05f48bcb4..ac5c031fa 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -72,7 +72,6 @@ import Primer.TypeDef ( ASTTypeDef (..), TypeDef (TypeDefAST), TypeDefMap, - ValCon (valConArgs), typeDefAST, valConName, ) @@ -122,8 +121,7 @@ data NoInputAction -- | An action which requires extra data (often a name) before it can be applied. data InputAction - = MakeCon - | MakeConSat + = MakeConSat | MakeInt | MakeChar | MakeVar @@ -199,17 +197,22 @@ forSig l Editable ty id = sortByPriority l $ case findType id ty of forExpr :: TypeDefMap -> Level -> Expr -> [Action] forExpr tydefs l expr = universalActions <> synOnly <> case expr of + -- TODO (saturated constructors)/REVIEW: in line with our permissive stance, + -- we allow putting a constructor in a hole of non-adt type, eg '? -> ?', + -- but that constructor will always be itself placed in a hole. For example, + -- in a hole of type 'Nat -> Nat', trying to insert the constructor 'Succ' + -- will leave 'Nat -> Nat ∋ {? Succ ? :: Nat ?}'. This could perhaps be + -- improved in the future to offer an "insert a eta-expanded ctor" action EmptyHole{} -> annotate <> [ Input MakeVar - , Input MakeCon + , Input MakeConSat ] <> mwhen (Map.member tInt tydefs) [Input MakeInt] <> mwhen (Map.member tChar tydefs) [Input MakeChar] <> mwhen (l /= Beginner) [ Input MakeVarSat - , Input MakeConSat , Input MakeLet , Input MakeLetRec , NoInput EnterHole @@ -328,20 +331,11 @@ options :: -- or found but didn't correspond to the expected sort of entity (type/expr/pattern). Maybe Options options typeDefs defs cxt level def mNodeSel = \case - MakeCon -> - pure - . noFree - . map (globalOpt . valConName . snd) - . filter (not . (&& level == Beginner) . uncurry hasArgsCon) - . concatMap (\td -> (td,) <$> astTypeDefConstructors td) - . mapMaybe (typeDefAST . snd) - $ Map.toList typeDefs MakeConSat -> pure . noFree - . map (globalOpt . valConName . snd) - . filter (uncurry hasArgsCon) - . concatMap (\td -> (td,) <$> astTypeDefConstructors td) + . map (globalOpt . valConName) + . concatMap astTypeDefConstructors . mapMaybe (typeDefAST . snd) $ Map.toList typeDefs MakeInt -> pure Options{opts = [], free = FreeInt} @@ -426,9 +420,6 @@ options typeDefs defs cxt level def mNodeSel = \case lAMVarKind = \case TForall _ _ k _ -> Just k _ -> Nothing - -- Constructor has either type or value arguments - hasArgsCon td vc = - not (null (astTypeDefParameters td)) || not (null (valConArgs vc)) -- Variable can be applied to something i.e. is a function or a polymorphic value hasArgsVar = \case TFun{} -> True @@ -461,7 +452,6 @@ sortByPriority l = DuplicateDef -> P.duplicate DeleteDef -> P.delete Input a -> case a of - MakeCon -> P.useValueCon MakeConSat -> P.useSaturatedValueCon MakeInt -> P.makeInt MakeChar -> P.makeChar diff --git a/primer/src/Primer/Action/Movement.hs b/primer/src/Primer/Action/Movement.hs index 9cabe84f0..d6b0d74d6 100644 --- a/primer/src/Primer/Action/Movement.hs +++ b/primer/src/Primer/Action/Movement.hs @@ -6,7 +6,19 @@ import Primer.Core.Meta (ValConName) import Primer.JSON (CustomJSON (..), FromJSON, PrimerJSON, ToJSON) -- | Core movements -data Movement = Child1 | Child2 | Parent | Branch ValConName +data Movement + = Child1 + | Child2 + | Parent + | Branch ValConName + | -- | zero-indexed + -- TODO (saturated constructors) the current, temporary, situation is that + -- constructors have both type arguments (indices) and term arguments. To move + -- into a term argument, one uses this @Movement@ type. To move into a *type* + -- argument, use the special 'EnterConTypeArgument' action (it cannot be a + -- movement because it changes from focusing on an expression to focusing on a + -- type). + ConChild Int deriving stock (Eq, Show, Read, Generic) deriving (FromJSON, ToJSON) via PrimerJSON Movement deriving anyclass (NFData) diff --git a/primer/src/Primer/Action/Priorities.hs b/primer/src/Primer/Action/Priorities.hs index 3398eca85..12d09c847 100644 --- a/primer/src/Primer/Action/Priorities.hs +++ b/primer/src/Primer/Action/Priorities.hs @@ -31,7 +31,6 @@ module Primer.Action.Priorities ( makeLambda, useVar, - useValueCon, makeInt, makeChar, makeCase, @@ -73,9 +72,6 @@ makeLambda _ = 5 useVar :: Level -> Int useVar _ = 10 -useValueCon :: Level -> Int -useValueCon _ = 11 - makeCase :: Level -> Int makeCase _ = 12 diff --git a/primer/src/Primer/Action/ProgError.hs b/primer/src/Primer/Action/ProgError.hs index ab736db96..a2fa35c27 100644 --- a/primer/src/Primer/Action/ProgError.hs +++ b/primer/src/Primer/Action/ProgError.hs @@ -19,6 +19,9 @@ data ProgError | TypeDefAlreadyExists TyConName | ConNotFound ValConName | ConAlreadyExists ValConName + | -- | We expected to see more arguments to a constructor than actually existed + -- (this should never happen in a well-typed program) + ConNotSaturated ValConName | ParamNotFound TyVarName | ParamAlreadyExists TyVarName | TyConParamClash Name diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index e0e3a10b1..05938637f 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -735,9 +735,16 @@ applyProgAction prog mdefName = \case ) type_ updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateDecons <=< updateCons) - updateCons e = case unfoldApp e of - (h, args) -> case unfoldAPP h of - (Con _ con', _tyArgs) | con' == con -> do + updateCons e = case (e, unfoldApp e) of + (Con m con' tms, _) | con' == con -> do + m' <- DSL.meta + case adjustAt index (Hole m') tms of + Just args' -> Con m con' <$> traverse (descendM updateCons) args' + Nothing -> throwError $ ConNotSaturated con + -- TODO (saturated constructors) this deconstruction of application nodes can be removed once full-saturation is enforced + -- (it currently assumes that constructors will either be fully saturated or have no syntactic arguments) + (_, (h, args)) -> case unfoldAPP h of + (Con _ con' [], _tyArgs) | con' == con -> do m' <- DSL.meta case adjustAt index (Hole m') args of Just args' -> foldApp h =<< traverse (descendM updateCons) args' @@ -788,9 +795,16 @@ applyProgAction prog mdefName = \case -- synthesis of the scrutinee's type, using the old typedef. Thus we must -- not update the scrutinee before this happens. updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons) - updateCons e = case unfoldApp e of - (h, args) -> case unfoldAPP h of - (Con _ con', _tyArgs) | con' == con -> do + updateCons e = case (e, unfoldApp e) of + (Con m con' tms, _) | con' == con -> do + m' <- DSL.meta + case insertAt index (EmptyHole m') tms of + Just args' -> Con m con' <$> traverse (descendM updateCons) args' + Nothing -> throwError $ ConNotSaturated con + -- TODO (saturated constructors) this deconstruction of application nodes can be removed once full-saturation is enforced + -- (it currently assumes that constructors will either be fully saturated or have no syntactic arguments) + (_, (h, args)) -> case unfoldAPP h of + (Con _ con' [], _tyArgs) | con' == con -> do m' <- DSL.meta case insertAt index (EmptyHole m') args of Just args' -> foldApp h =<< traverse (descendM updateCons) args' diff --git a/primer/src/Primer/Builtins/DSL.hs b/primer/src/Primer/Builtins/DSL.hs index b5492703d..70fb6a249 100644 --- a/primer/src/Primer/Builtins/DSL.hs +++ b/primer/src/Primer/Builtins/DSL.hs @@ -1,8 +1,10 @@ -- | Helpers for building expressions involving built-in types. module Primer.Builtins.DSL ( bool_, + boolAnn, nat, maybe_, + maybeAnn, list_, listOf, ) where @@ -20,46 +22,50 @@ import Primer.Builtins ( cSucc, cTrue, cZero, + tBool, tList, + tMaybe, ) import Primer.Core ( Expr, ID, - TyConName, Type, ) import Primer.Core.DSL ( - aPP, - app, - con, + ann, + con0, + conSat, tapp, tcon, ) -- These functions rely on particular types being in scope. bool_ :: MonadFresh ID m => Bool -> m Expr -bool_ b = con $ if b then cTrue else cFalse +bool_ b = con0 $ if b then cTrue else cFalse + +boolAnn :: MonadFresh ID m => Bool -> m Expr +boolAnn b = bool_ b `ann` tcon tBool nat :: MonadFresh ID m => Natural -> m Expr nat = \case - 0 -> con cZero - n -> app (con cSucc) $ nat (n - 1) + 0 -> conSat cZero [] + n -> conSat cSucc [nat (n - 1)] + +maybe_ :: MonadFresh ID m => (a -> m Expr) -> Maybe a -> m Expr +maybe_ f = \case + Nothing -> conSat cNothing [] + Just x -> conSat cJust [f x] -maybe_ :: MonadFresh ID m => m Type -> (a -> m Expr) -> Maybe a -> m Expr -maybe_ t f = \case - Nothing -> con cNothing `aPP` t - Just x -> con cJust `aPP` t `app` f x +maybeAnn :: MonadFresh ID m => m Type -> (a -> m Expr) -> Maybe a -> m Expr +maybeAnn t f x = maybe_ f x `ann` (tcon tMaybe `tapp` t) -list_ :: MonadFresh ID m => TyConName -> [m Expr] -> m Expr -list_ t = +list_ :: MonadFresh ID m => [m Expr] -> m Expr +list_ = foldr ( \a b -> - con cCons - `aPP` tcon t - `app` a - `app` b + conSat cCons [a, b] ) - (con cNil `aPP` tcon t) + (conSat cNil []) listOf :: MonadFresh ID m => m Type -> m Type listOf = tapp (tcon tList) diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index 6986713a0..9ea8901a3 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -145,7 +145,8 @@ data Expr' a b | Ann a (Expr' a b) (Type' b) | App a (Expr' a b) (Expr' a b) | APP a (Expr' a b) (Type' b) - | Con a ValConName -- See Note [Synthesisable constructors] + | Con a ValConName [Expr' a b] -- See Note [Synthesisable constructors] + -- TODO (saturated constructors) the docs need updating here. constructors are now checkable only | Lam a LVarName (Expr' a b) | LAM a TyVarName (Expr' a b) | Var a TmVarRef @@ -185,19 +186,27 @@ data Expr' a b deriving anyclass (NFData) -- Note [Synthesisable constructors] +-- TODO: this note needs updating for enforced-full-saturation! +-- TODO (saturated constructors): the name of this note needs to change for check-ctors: make sure to update all references! +-- -- Whilst our calculus is heavily inspired by bidirectional type systems -- (especially McBride's principled rendition), we do not treat constructors --- in this fashion. We view constructors as synthesisable terms +-- in this fashion. However, we are in the middle of changing the treatment +-- here. Currently we view constructors as synthesisable terms -- ("eliminations"), rather than checkable terms ("constructions"). -- This is for user-experience purposes: we are attempting a pedagogic -- system where the user-facing code is close to the core language, and -- we believe that the bidirectional style would be confusing and/or --- annoyingly restrictive in this particular instance. +-- annoyingly restrictive in this particular instance. (Our view here has +-- changed, due to asymmetries between construction and matching.) -- --- We follow the traditional non-bidirectional view of constructors here: --- a constructor is a term in-and-of itself (and one can infer its type). +-- We represent a constructor-applied-to-a-spine as a thing (and one can infer +-- its type), but do not insist that it is fully saturated. -- Thus one has `Cons` is a term, and we can derive the synthesis --- judgement `Cons ∈ ∀a. a -> List a -> List a`. +-- judgement `Cons ∈ ∀a. a -> List a -> List a`, but also that `Cons @a`, +-- `Cons @a x` and `Cons @a x y` are terms (for type `a` and terms `x, y`), with +-- the obvious synthesised types. This is a temporary situation, and we aim to +-- enforce full saturation (and no type applications) in due course. -- -- For comparison, the bidirectional view would be that constructors must -- always be fully applied, and one can only subject them to a typechecking @@ -214,8 +223,8 @@ data Expr' a b -- Clearly one could eta-expand, (and if necessary add an annotation) to -- use as constructor non-saturatedly: e.g. write `map (λn . Succ n) [2,3]`. -- --- In effect, we just bake this translation into the core. To do this, we --- require constructor names to be unique across different types. +-- In effect, we just bake (various stages of) this translation into the core. +-- To do this, we require constructor names to be unique across different types. -- Note [Case] -- We use a list for compatibility and ease of JSON @@ -278,6 +287,8 @@ _bindMeta = position @1 -- | Note that this does not recurse in to sub-expressions or sub-types. typesInExpr :: AffineTraversal' (Expr' a b) (Type' b) +-- TODO (saturated constructors): if constructors did not store their indices, +-- then this could be an affine traversal typesInExpr = atraversalVL $ \point f -> \case Ann m e ty -> Ann m e <$> f ty APP m e ty -> APP m e <$> f ty diff --git a/primer/src/Primer/Core/DSL.hs b/primer/src/Primer/Core/DSL.hs index 0b7ea582e..e200d250b 100644 --- a/primer/src/Primer/Core/DSL.hs +++ b/primer/src/Primer/Core/DSL.hs @@ -6,7 +6,10 @@ module Primer.Core.DSL ( ann, app, aPP, + conSat, con, + con0, + con1, lvar, gvar, var, @@ -35,7 +38,9 @@ module Primer.Core.DSL ( setMeta, S, tcon', + conSat', con', + con0', gvar', branch', apps, @@ -109,8 +114,28 @@ emptyHole = EmptyHole <$> meta ann :: MonadFresh ID m => m Expr -> m Type -> m Expr ann e t = Ann <$> meta <*> e <*> t -con :: MonadFresh ID m => ValConName -> m Expr -con c = Con <$> meta <*> pure c +con :: MonadFresh ID m => ValConName -> [m Expr] -> m Expr +con = conSat + +-- TODO (saturated constructors) once saturation is enforced, this will be +-- renamed to con, and the current con will be removed (since it creates +-- unsaturated constructors) +conSat :: MonadFresh ID m => ValConName -> [m Expr] -> m Expr +conSat c tms = Con <$> meta <*> pure c <*> sequence tms + +-- | Create a constructor of arity zero. +-- (This condition is not checked here. +-- If used with a constructor which has fields, +-- then the typechecker will complain, when run.) +con0 :: MonadFresh ID m => ValConName -> m Expr +con0 c = conSat c [] + +-- | Create a constructor of arity one. +-- (This condition is not checked here. +-- If used with a constructor which has fields, +-- then the typechecker will complain, when run.) +con1 :: MonadFresh ID m => ValConName -> m Expr -> m Expr +con1 c t = conSat c [t] lvar :: MonadFresh ID m => LVarName -> m Expr lvar v = Var <$> meta <*> pure (LocalVarRef v) @@ -153,8 +178,19 @@ char = prim . PrimChar int :: MonadFresh ID m => Integer -> m Expr int = prim . PrimInt -con' :: MonadFresh ID m => NonEmpty Name -> Name -> m Expr -con' m n = con $ qualifyName (ModuleName m) n +-- con' :: MonadFresh ID m => NonEmpty Name -> Name -> m Expr +-- con' m n = con $ qualifyName (ModuleName m) n +con' :: MonadFresh ID m => NonEmpty Name -> Name -> [m Expr] -> m Expr +con' = conSat' + +con0' :: MonadFresh ID m => NonEmpty Name -> Name -> m Expr +con0' m n = con0 $ qualifyName (ModuleName m) n + +-- TODO (saturated constructors) once saturation is enforced, this will be +-- renamed to con', and the current con' will be removed (since it creates +-- unsaturated constructors) +conSat' :: MonadFresh ID m => NonEmpty Name -> Name -> [m Expr] -> m Expr +conSat' m n = conSat $ qualifyName (ModuleName m) n gvar' :: MonadFresh ID m => NonEmpty Name -> Name -> m Expr gvar' m n = gvar $ qualifyName (ModuleName m) n diff --git a/primer/src/Primer/Core/Transform.hs b/primer/src/Primer/Core/Transform.hs index c8ae1d2ed..4b151297c 100644 --- a/primer/src/Primer/Core/Transform.hs +++ b/primer/src/Primer/Core/Transform.hs @@ -7,6 +7,8 @@ module Primer.Core.Transform ( foldApp, unfoldAPP, unfoldTApp, + decomposeTAppCon, + mkTAppCon, unfoldFun, ) where @@ -31,6 +33,7 @@ import Primer.Core ( typesInExpr, ) import Primer.Core.DSL (meta) +import Primer.Core.Meta (TyConName) import Primer.Core.Utils (_freeVars, _freeVarsTy) -- AST transformations. @@ -210,7 +213,7 @@ unfoldApp = second reverse . go go (App _ f x) = let (g, args) = go f in (g, x : args) go e = (e, []) --- | Fold an application head and a list of arguments in to a single expression. +-- | Fold an application head and a list of arguments into a single expression. foldApp :: (Foldable t, MonadFresh ID m) => Expr -> t Expr -> m Expr foldApp = foldlM $ \a b -> do m <- meta @@ -230,6 +233,21 @@ unfoldTApp = second reverse . go go (TApp _ f x) = let (g, args) = go f in (g, x : args) go e = (e, []) +-- | Fold an type-level application head and a list of arguments into a single expression. +foldTApp' :: (Monad m, Foldable t) => m a -> Type' a -> t (Type' a) -> m (Type' a) +foldTApp' m = foldlM $ \a b -> (\m' -> TApp m' a b) <$> m + +-- | @mkTAppCon C [X,Y,Z] = C X Y Z@ +mkTAppCon :: TyConName -> [Type' ()] -> Type' () +mkTAppCon c = runIdentity . foldTApp' (pure ()) (TCon () c) + +-- | Decompose @C X Y Z@ to @(C,[X,Y,Z])@ +decomposeTAppCon :: Type' a -> Maybe (TyConName, [Type' a]) +decomposeTAppCon = + unfoldTApp <&> \case + (TCon _ con, args) -> Just (con, args) + _ -> Nothing + -- | Split a function type into an array of argument types and the result type. -- Takes two arguments: the lhs and rhs of the topmost function node. unfoldFun :: Type' a -> Type' a -> (NonEmpty (Type' a), Type' a) diff --git a/primer/src/Primer/Core/Utils.hs b/primer/src/Primer/Core/Utils.hs index d916cda27..514d37a30 100644 --- a/primer/src/Primer/Core/Utils.hs +++ b/primer/src/Primer/Core/Utils.hs @@ -119,7 +119,7 @@ _freeTmVars = traversalVL $ go mempty Ann m e ty -> Ann m <$> go bound f e <*> pure ty App m e s -> App m <$> go bound f e <*> go bound f s APP m e ty -> APP m <$> go bound f e <*> pure ty - t@Con{} -> pure t + Con m c tms -> Con m c <$> traverse (go bound f) tms Lam m v e -> Lam m v <$> go (S.insert v bound) f e LAM m tv e -> -- A well scoped term will not refer to tv as a term @@ -151,7 +151,7 @@ _freeTyVars = traversalVL $ go mempty Ann m e ty -> Ann m <$> go bound f e <*> traverseFreeVarsTy bound f ty App m e s -> App m <$> go bound f e <*> go bound f s APP m e ty -> APP m <$> go bound f e <*> traverseFreeVarsTy bound f ty - t@Con{} -> pure t + Con m c tms -> Con m c <$> traverse (go bound f) tms Lam m v e -> -- A well scoped term will not refer to v as a type -- variable, so we do not need to add it to the bound set diff --git a/primer/src/Primer/Eval/Case.hs b/primer/src/Primer/Eval/Case.hs index 255643a3c..f156ef005 100644 --- a/primer/src/Primer/Eval/Case.hs +++ b/primer/src/Primer/Eval/Case.hs @@ -20,6 +20,7 @@ data CaseReductionDetail = CaseReductionDetail -- ^ the ID of the target (scrutinee) , targetCtorID :: ID -- ^ the ID of the constructor node in the target + -- TODO (saturated constructors) these may or may not be the same, depending on annotations. This needs clarity and documenting , ctorName :: ValConName -- ^ the name of the matching constructor , targetArgIDs :: [ID] diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs index e7deee73c..3b4a0675b 100644 --- a/primer/src/Primer/Eval/Redex.hs +++ b/primer/src/Primer/Eval/Redex.hs @@ -24,7 +24,7 @@ import Control.Monad.Fresh (MonadFresh) import Control.Monad.Log (MonadLog, WithSeverity) import Control.Monad.Trans.Maybe (MaybeT (runMaybeT)) import Data.Data (Data) -import Data.List.Extra (zip4) +import Data.List.Extra (zip3) import Data.Map qualified as M import Data.Set qualified as S import Data.Set.Optics (setOf) @@ -89,9 +89,7 @@ import Primer.Core ( getID, ) import Primer.Core.DSL (ann, letType, let_, letrec, lvar, tlet, tvar) -import Primer.Core.Transform (unfoldAPP, unfoldApp) import Primer.Core.Utils ( - alphaEqTy, concreteTy, forgetTypeMetadata, freeVars, @@ -138,7 +136,7 @@ import Primer.Eval.Detail ( import Primer.Eval.Detail qualified import Primer.Eval.Prim (tryPrimFun) import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON) -import Primer.Log (ConvertLogMessage (convert), logInfo, logWarning) +import Primer.Log (ConvertLogMessage (convert), logWarning) import Primer.Name (Name, NameCounter) import Primer.TypeDef ( TypeDefMap, @@ -146,8 +144,6 @@ import Primer.TypeDef ( import Primer.Typecheck.Utils ( TypeDefError (TDIHoleType, TDINotADT, TDINotSaturated, TDIUnknown), instantiateValCons', - lookupConstructor, - mkTAppCon, ) import Primer.Zipper ( LetBinding, @@ -187,12 +183,7 @@ data EvalLog -- but the number of arguments in the scrutinee differs from the number of bindings in the corresponding branch. -- (Or the number of arguments expected from the scrutinee's type differs from either of these.) -- This should not happen if the expression is type correct. - CaseRedexWrongArgNum ValConName [Expr] [Type' ()] (Maybe [Type' ()]) [LVarName] - | -- | A case redex required a double annotation on (some of) its resultant let binding(s) - -- This is expected to happen for e.g. @case Just \@? True : Maybe Int of ...@, and - -- does not represent any problem. We log it to obtain insight about how common this - -- is in practice. - CaseRedexDoubleAnn ValConName [Expr] [Type' ()] (Maybe [Type' ()]) [LVarName] + CaseRedexWrongArgNum ValConName [Expr] [Type' ()] [LVarName] | InvariantFailure Text deriving stock (Show, Eq, Data, Generic) deriving anyclass (NFData) @@ -298,14 +289,15 @@ data Redex -- reduction steps. E.g. -- cons == (Λa λx λxs. Cons @a x xs) : ∀a. a -> List a -> List a -- ) + -- TODO (saturated constructors) update the above comment! NB: only annotated scrutinees are welltyped CaseRedex { con :: ValConName -- ^ The head of the scrutinee , args :: [Expr] -- ^ The arguments of the scrutinee - , argTys :: forall m. MonadFresh NameCounter m => ([m (Type' ())], Maybe [m (Type' ())]) + , argTys :: forall m. MonadFresh NameCounter m => [m (Type' ())] -- ^ The type of each scrutinee's argument - -- (from inspecting the constructor's type applications and (maybe) the type annotation on the scrutinee) + -- (from inspecting the type annotation on the scrutinee) , binders :: [Bind] -- ^ The binders of the matching branch , rhs :: Expr @@ -502,27 +494,17 @@ viewCaseRedex :: Expr -> MaybeT m Redex viewCaseRedex tydefs = \case + -- Note that constructors are checkable, but scrutinees are synthesisable, + -- thus we only have terms such as @case (C x y : T a) of ...@. Thus we + -- know the type of the scrutinee syntactically. + -- -- The patterns in the case branch have a Maybe TypeCache attached, but we -- should not assume that this has been filled in correctly, so we record -- the type of the scrutinee, and reconstruct the types of the pattern -- variables. This is especially important, as we do not (yet?) take care of -- metadata correctly in this evaluator (for instance, substituting when we -- do a BETA reduction)! - orig@(Case m expr brs) -> do - let expr' = case expr of - Ann _ e _ -> e - _ -> expr - (c, cID, tyargs, args) <- extractCon expr' - tyFromCon <- case lookupConstructor tydefs c of - Nothing -> do - logWarning $ CaseRedexUnknownCtor c - mzero - Just (_, tc, _) -> do - pure $ mkTAppCon tc (forgetTypeMetadata <$> tyargs) - -- If the constructor had an annotation we must preserve it in the output - let tyFromAnn = case expr of - Ann _ _ ty' -> Just $ forgetTypeMetadata ty' - _ -> Nothing + orig@(Case mCase scrut@(Ann _ (Con mCon c args) ty) brs) -> do -- Style note: unfortunately do notation does not work well with polytyped binds on ghc 9.2.4 -- Thus we write this with an explicit bind instead. -- See https://gitlab.haskell.org/ghc/ghc/-/issues/18324 @@ -530,25 +512,12 @@ viewCaseRedex tydefs = \case -- Implementation note: it is important to instantiate with the type-from-the-annotation first, -- since we could have 'case Cons : ? of {}' and we would like to silently say "not a redex, -- because hole type", rather than logging that the Cons is not saturated. - traverse (`instantiateCon` c) tyFromAnn <&> pushMaybe >>= \argTysFromAnn -> - instantiateCon tyFromCon c >>= \argTysFromCon -> do - (patterns, br) <- extractBranch c brs - renameBindings m expr brs (tyFromCon : toList tyFromAnn) args patterns orig - <|> pure (formCaseRedex c (argTysFromCon, argTysFromAnn) args patterns br (orig, expr, cID)) + instantiateCon (forgetTypeMetadata ty) c >>= \argTys -> do + (patterns, br) <- extractBranch c brs + renameBindings mCase scrut brs patterns orig + <|> pure (formCaseRedex c argTys args patterns br (orig, scrut, getID mCon)) _ -> mzero where - pushMaybe :: Maybe (forall m'. c m' => [m' a]) -> forall m'. c m' => Maybe [m' a] - pushMaybe Nothing = Nothing - pushMaybe (Just xs) = Just xs - - extractCon expr = - -- NB: constructors never have mixed App and APPs: they are always of the - -- form C @a @b ... x y ... - let (h, as) = unfoldApp expr - (h', params) = unfoldAPP h - in case h' of - Con m c -> pure (c, getID m, params, as) - _ -> mzero extractBranch c brs = case find (\(CaseBranch n _ _) -> n == c) brs of Nothing -> do @@ -570,31 +539,28 @@ viewCaseRedex tydefs = \case {- Note [Case reduction and variable capture] There is a subtlety here around variable capture. Consider - case C @A' @B' s t : T A B of C a b -> e + case C s t : T A B of C a b -> e We would like to reduce this to - let a = s : S' : S; let b = t : T' : T in e - where we have annotated `s` and `t` with their two types - (one from the arguments `A'` `B'` to the constructor, - one from the arguments `A` `B` to the annotation), which will be - built from `A` and `B` according to the definition of the type `T` - (for reasons of bidirectionality). + let a = s : S; let b = t : T in e + where we have annotated `s` and `t` with their types, which will be + built from `A` and `B` according to the definition of the type `T`. Note that the binding of `a` may capture a reference in `t` - or (assuming type and term variables can shadow) in `T'` or `T`. + or (assuming type and term variables can shadow) in `T`. We must catch this case and rename the case binders as a first step. - Note that the free vars in `t : T' : T` are a subset of the free vars in the - arguments of the scrutinee (s, t) plus the arguments to its type - annotations (A', B', A, B). (In the non-annotated case, we only have - `A', B'` and not `A, B`). + Note that the free vars in `t : T` are a subset of the free vars in the + arguments of the constructor (s, t) plus the arguments to its type + annotations (A, B). We shall be conservative and rename all binders in every branch apart - from these free vars. + from these free vars, i.e. from any free var in the scrutinee + `C s t : T A B`. (We could get away with only renaming within the matching branch, only avoiding those FVs that actually occur, and in a "telescope" fashion: the first binder needs to avoid the FVs of all except the first argument, the second needs to avoid all but the first two args, ..., the last doesn't need any renaming.) -} - renameBindings meta scrutinee branches tyargs args patterns orig = - let avoid = foldMap' (S.map unLocalName . freeVarsTy) tyargs <> foldMap' freeVars args + renameBindings meta scrutinee branches patterns orig = + let avoid = freeVars scrutinee binders = S.fromList $ map (unLocalName . bindName) patterns in hoistMaybe $ if S.disjoint avoid binders @@ -602,7 +568,7 @@ viewCaseRedex tydefs = \case else Just $ RenameBindingsCase{meta, scrutinee, branches, avoid, orig} formCaseRedex :: ValConName -> - (forall m'. MonadFresh NameCounter m' => ([m' (Type' ())], Maybe [m' (Type' ())])) -> + (forall m'. MonadFresh NameCounter m' => [m' (Type' ())]) -> [Expr] -> [Bind] -> Expr -> @@ -884,13 +850,12 @@ runRedex = \case } pure (expr', BETAReduction details) -- case C as : T of ... ; C xs -> e ; ... ~> let xs=as:As in e for constructor C of type T, where args have types As - -- (and also the non-annotated-constructor case) -- Note that when forming the CaseRedex we checked that the variables @xs@ were fresh for @as@ and @As@, -- so this will not capture any variables. CaseRedex { con , args - , argTys = (argTysFromCon, argTysFromAnn) + , argTys , binders , rhs , orig @@ -898,29 +863,22 @@ runRedex = \case , conID } -> do let binderNames = map bindName binders - aTysC <- sequence argTysFromCon - aTysA <- traverse sequence argTysFromAnn - unless (length args == length aTysC && maybe True ((length args ==) . length) aTysA && length args == length binders) $ + argTys' <- sequence argTys + unless (length args == length argTys' && length args == length binders) $ logWarning $ - CaseRedexWrongArgNum con args aTysC aTysA binderNames + CaseRedexWrongArgNum con args argTys' binderNames -- TODO: we are putting trivial metadata in here... -- See https://github.com/hackworthltd/primer/issues/6 let ann' x t = x `ann` generateTypeIDs t - let mkAnn (tyC, tyA') = case tyA' of - Nothing -> (False, (`ann'` tyC)) - Just tyA - | alphaEqTy tyC tyA -> (False, (`ann'` tyC)) - | otherwise -> (True, \x -> x `ann'` tyC `ann'` tyA) - (diffAnn, letIDs, expr') <- + (letIDs, expr') <- foldrM - ( \(x, a, tyC, tyA) (diffAnn, is, t) -> do - let (d, putAnn) = mkAnn (tyC, tyA) - t' <- let_ x (putAnn $ pure a) (pure t) - pure (diffAnn || d, getID t' : is, t') + ( \(x, a, ty) (is, t) -> do + t' <- let_ x (pure a `ann'` ty) (pure t) + pure (getID t' : is, t') ) - (False, [], rhs) - (zip4 binderNames args aTysC $ maybe (repeat Nothing) (fmap Just) aTysA) - when diffAnn $ logInfo $ CaseRedexDoubleAnn con args aTysC aTysA binderNames + ([], rhs) + -- TODO (saturated constructors)/REVIEW should we use a lettype, rather than doing the substitution in the type/annotation? This is not really related to satcon, but I happened to notice it! + (zip3 binderNames args argTys') let details = CaseReductionDetail { before = orig diff --git a/primer/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs index b2da73b5e..7af8311e7 100644 --- a/primer/src/Primer/Examples.hs +++ b/primer/src/Primer/Examples.hs @@ -76,7 +76,8 @@ import Primer.Core.DSL ( app, branch, case_, - con, + con0, + conSat, create, emptyHole, gvar, @@ -95,7 +96,6 @@ import Primer.Core.DSL ( tforall, tfun, thole, - tlet, tvar, ) import Primer.Def ( @@ -124,8 +124,8 @@ not modName = "x" ( case_ (lvar "x") - [ branch B.cTrue [] (con B.cFalse) - , branch B.cFalse [] (con B.cTrue) + [ branch B.cTrue [] (conSat B.cFalse []) + , branch B.cFalse [] (conSat B.cTrue []) ] ) pure (this, DefAST $ ASTDef term type_) @@ -145,9 +145,9 @@ map modName = case_ (lvar "xs") [ branch B.cNil [] $ - con B.cNil `aPP` tvar "b" + conSat B.cNil [] , branch B.cCons [("y", Nothing), ("ys", Nothing)] $ - con B.cCons `aPP` tvar "b" `app` (lvar "f" `app` lvar "y") `app` (gvar this `aPP` tvar "a" `aPP` tvar "b" `app` lvar "f" `app` lvar "ys") + conSat 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_) @@ -160,9 +160,9 @@ map' modName = do lam "xs" $ case_ (lvar "xs") - [ branch B.cNil [] $ con B.cNil `aPP` tvar "b" + [ branch B.cNil [] $ conSat B.cNil [] , branch B.cCons [("y", Nothing), ("ys", Nothing)] $ - con B.cCons `aPP` tvar "b" `app` (lvar "f" `app` lvar "y") `app` (lvar "go" `app` lvar "ys") + conSat B.cCons [lvar "f" `app` lvar "y", lvar "go" `app` lvar "ys"] ] term <- lAM "a" $ @@ -183,7 +183,7 @@ odd modName = do lam "x" $ case_ (lvar "x") - [ branch B.cZero [] $ con B.cFalse + [ branch B.cZero [] $ conSat B.cFalse [] , branch B.cSucc [("n", Nothing)] $ gvar (qualifyName modName "even") `app` lvar "n" ] pure (qualifyName modName "odd", DefAST $ ASTDef term type_) @@ -199,7 +199,7 @@ even modName = do lam "x" $ case_ (lvar "x") - [ branch B.cZero [] $ con B.cTrue + [ branch B.cZero [] $ conSat B.cTrue [] , branch B.cSucc [("n", Nothing)] $ gvar (qualifyName modName "odd") `app` lvar "n" ] pure (qualifyName modName "even", DefAST $ ASTDef term type_) @@ -247,12 +247,12 @@ comprehensive' typeable modName = do term <- let_ "x" - (con B.cTrue) + (conSat B.cTrue [] `ann` tcon B.tBool) ( letrec "y" ( app ( hole - (con B.cJust) + (conSat B.cJust [emptyHole] `ann` (tcon B.tMaybe `tapp` tEmptyHole)) ) ( if typeable then emptyHole else hole $ gvar' (unModuleName modName) "unboundName" ) @@ -269,17 +269,18 @@ comprehensive' typeable modName = do ( aPP ( if typeable then - aPP - (con B.cLeft) - (tcon B.tBool) + lAM "b" (lam "x" $ conSat B.cLeft [lvar "x"]) + `ann` tforall + "b" + KType + ( tcon B.tBool + `tfun` (tcon B.tEither `tapp` tcon B.tBool `tapp` tvar "b") + ) else letType "b" (tcon B.tBool) - ( aPP - (con B.cLeft) - (tlet "c" (tvar "b") $ tvar "c") - ) + (conSat B.cLeft []) ) (tvar "β") ) @@ -288,7 +289,7 @@ comprehensive' typeable modName = do [ branch B.cZero [] - (con B.cFalse) + (conSat B.cFalse []) , branch B.cSucc [ @@ -361,7 +362,7 @@ even3Prog = (_, oddDef) <- odd modName even3Def <- do type_ <- tcon B.tBool - term <- gvar (qualifyName modName "even") `app` (con B.cSucc `app` (con B.cSucc `app` (con B.cSucc `app` con B.cZero))) + term <- gvar (qualifyName modName "even") `app` conSat B.cSucc [conSat B.cSucc [conSat B.cSucc [con0 B.cZero]]] pure $ DefAST $ ASTDef term type_ let globs = [("even", evenDef), ("odd", oddDef), ("even 3?", even3Def)] pure globs @@ -389,7 +390,7 @@ mapOddProg len = (mapName, mapDef) <- map modName mapOddDef <- do type_ <- tcon B.tList `tapp` tcon B.tBool - let lst = list_ B.tNat $ take len $ nat <$> [0 ..] + let lst = list_ $ take len $ nat <$> [0 ..] term <- gvar mapName `aPP` tcon B.tNat `aPP` tcon B.tBool `app` gvar oddName `app` lst pure $ DefAST $ ASTDef term type_ let globs = [("even", evenDef), ("odd", oddDef), ("map", mapDef), ("mapOdd", mapOddDef)] @@ -422,14 +423,14 @@ mapOddPrimProg len = lam "x" $ case_ (pfun P.IntRemainder `app` lvar "x" `app` int 2) - [ branch B.cNothing [] $ con B.cTrue -- this should be impossible (since denominator is obviously non-zero) + [ 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 ] pure $ DefAST $ ASTDef term type_ (mapName, mapDef) <- map modName mapOddDef <- do type_ <- tcon B.tList `tapp` tcon B.tBool - let lst = list_ P.tInt $ take len $ int <$> [0 ..] + 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)] @@ -458,7 +459,7 @@ badEven3Prog = (_, oddDef) <- odd modName even3Def <- do type_ <- tcon B.tNat - term <- gvar (qualifyName modName "even") `app` (con B.cSucc `app` (con B.cSucc `app` (con B.cSucc `app` con B.cZero))) + term <- gvar (qualifyName modName "even") `app` conSat B.cSucc [conSat B.cSucc [conSat B.cSucc [con0 B.cZero]]] pure $ DefAST $ ASTDef term type_ let globs = [("even", evenDef), ("odd", oddDef), ("even 3?", even3Def)] pure globs diff --git a/primer/src/Primer/Prelude/Logic.hs b/primer/src/Primer/Prelude/Logic.hs index 2bd447ad0..b6368989a 100644 --- a/primer/src/Primer/Prelude/Logic.hs +++ b/primer/src/Primer/Prelude/Logic.hs @@ -14,7 +14,7 @@ import Primer.Core.DSL ( apps, branch, case_, - con, + con0, gvar, lam, lvar, @@ -39,8 +39,8 @@ notDef = do "x" ( case_ (lvar "x") - [ branch B.cTrue [] (con B.cFalse) - , branch B.cFalse [] (con B.cTrue) + [ branch B.cTrue [] (con0 B.cFalse) + , branch B.cFalse [] (con0 B.cTrue) ] ) pure $ DefAST $ ASTDef term type_ @@ -63,12 +63,12 @@ andDef = do "y" ( case_ (lvar "y") - [ branch B.cTrue [] (con B.cTrue) - , branch B.cFalse [] (con B.cFalse) + [ branch B.cTrue [] (con0 B.cTrue) + , branch B.cFalse [] (con0 B.cFalse) ] ) ) - , branch B.cFalse [] (lam "y" $ con B.cFalse) + , branch B.cFalse [] (lam "y" $ con0 B.cFalse) ] ) pure $ DefAST $ ASTDef term type_ @@ -84,7 +84,7 @@ orDef = do "x" ( case_ (lvar "x") - [ branch B.cTrue [] (lam "y" $ con B.cTrue) + [ branch B.cTrue [] (lam "y" $ con0 B.cTrue) , branch B.cFalse [] @@ -92,8 +92,8 @@ orDef = do "y" ( case_ (lvar "y") - [ branch B.cTrue [] $ con B.cTrue - , branch B.cFalse [] $ con B.cFalse + [ branch B.cTrue [] $ con0 B.cTrue + , branch B.cFalse [] $ con0 B.cFalse ] ) ) @@ -139,8 +139,8 @@ impliesDef = do "y" ( case_ (lvar "x") - [ branch B.cTrue [] (case_ (lvar "y") [branch B.cTrue [] $ con B.cTrue, branch B.cFalse [] $ con B.cFalse]) - , branch B.cFalse [] (case_ (lvar "y") [branch B.cTrue [] $ con B.cTrue, branch B.cFalse [] $ con B.cTrue]) + [ branch B.cTrue [] (case_ (lvar "y") [branch B.cTrue [] $ con0 B.cTrue, branch B.cFalse [] $ con0 B.cFalse]) + , branch B.cFalse [] (case_ (lvar "y") [branch B.cTrue [] $ con0 B.cTrue, branch B.cFalse [] $ con0 B.cTrue]) ] ) ) diff --git a/primer/src/Primer/Prelude/Polymorphism.hs b/primer/src/Primer/Prelude/Polymorphism.hs index cce4348b2..d4bea8927 100644 --- a/primer/src/Primer/Prelude/Polymorphism.hs +++ b/primer/src/Primer/Prelude/Polymorphism.hs @@ -22,13 +22,12 @@ import Primer.Builtins.DSL ( ) import Primer.Core (GVarName, ID, Kind (KType), qualifyName) import Primer.Core.DSL ( - aPP, app, apps, apps', branch, case_, - con, + conSat, gvar, lAM, lam, @@ -75,11 +74,11 @@ mapDef = do lam "xs" $ case_ (lvar "xs") - [ branch cNil [] (con cNil `aPP` tvar "b") + [ branch cNil [] (conSat 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 apps (con cCons `aPP` tvar "b") [fy, fys] + in conSat cCons [fy, fys] ] pure $ DefAST $ ASTDef term type_ diff --git a/primer/src/Primer/Pretty.hs b/primer/src/Primer/Pretty.hs index 3ab0018a0..62b8473f0 100644 --- a/primer/src/Primer/Pretty.hs +++ b/primer/src/Primer/Pretty.hs @@ -23,6 +23,7 @@ import Prettyprinter ( line, line', space, + vsep, (<+>), ) import Prettyprinter.Render.Terminal ( @@ -86,7 +87,9 @@ prettyExpr :: PrettyOptions -> Expr' a b -> Doc AnsiStyle prettyExpr opts = \case Hole _ e -> (if inlineHoles opts then group else identity) (brac Curly Red (pE e)) EmptyHole _ -> col Red "?" - Con _ n -> col Green (gname opts n) + Con _ n tms -> + let prettyTms = brac Round White . pE <$> tms + in vsep $ col Green (gname opts n) : prettyTms Var _ v -> case v of GlobalVarRef n -> col Blue (gname opts n) LocalVarRef n -> lname n diff --git a/primer/src/Primer/Primitives.hs b/primer/src/Primer/Primitives.hs index a210a2704..413c0e1bc 100644 --- a/primer/src/Primer/Primitives.hs +++ b/primer/src/Primer/Primitives.hs @@ -24,15 +24,13 @@ import Data.Data (Data) import Data.Map qualified as M import Numeric.Natural (Natural) import Primer.Builtins ( - cJust, - cNothing, cSucc, cZero, tBool, tMaybe, tNat, ) -import Primer.Builtins.DSL (bool_, maybe_, nat) +import Primer.Builtins.DSL (boolAnn, maybeAnn, nat) import Primer.Core ( Expr, Expr' (App, Con, PrimCon), @@ -47,10 +45,7 @@ import Primer.Core ( qualifyName, ) import Primer.Core.DSL ( - aPP, - app, char, - con, int, tcon, ) @@ -178,24 +173,24 @@ primFunDef def args = case def of _ -> err IsSpace -> case args of [PrimCon _ (PrimChar c)] -> - Right $ bool_ $ isSpace c + Right $ boolAnn (isSpace c) _ -> err HexToNat -> case args of - [PrimCon _ (PrimChar c)] -> Right $ maybe_ (tcon tNat) nat $ digitToIntSafe c + [PrimCon _ (PrimChar c)] -> Right $ maybeAnn (tcon tNat) nat (digitToIntSafe c) where digitToIntSafe :: Char -> Maybe Natural digitToIntSafe c' = fromIntegral <$> (guard (isHexDigit c') $> digitToInt c') _ -> err NatToHex -> case args of [exprToNat -> Just n] -> - Right $ maybe_ (tcon tChar) char $ intToDigitSafe n + Right $ maybeAnn (tcon tChar) char $ intToDigitSafe n where intToDigitSafe :: Natural -> Maybe Char intToDigitSafe n' = guard (0 <= n && n <= 15) $> intToDigit (fromIntegral n') _ -> err EqChar -> case args of [PrimCon _ (PrimChar c1), PrimCon _ (PrimChar c2)] -> - Right $ bool_ $ c1 == c2 + Right $ boolAnn $ c1 == c2 _ -> err IntAdd -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> @@ -212,22 +207,18 @@ primFunDef def args = case def of IntQuotient -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> Right $ - if y == 0 - then con cNothing `aPP` tcon tInt - else - con cJust - `aPP` tcon tInt - `app` int (x `div` y) + 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 $ - if y == 0 - then con cNothing `aPP` tcon tInt - else - con cJust - `aPP` tcon tInt - `app` int (x `mod` y) + 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)] -> @@ -245,37 +236,35 @@ primFunDef def args = case def of _ -> err IntLT -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right $ bool_ $ x < y + Right $ boolAnn $ x < y _ -> err IntLTE -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right $ bool_ $ x <= y + Right $ boolAnn $ x <= y _ -> err IntGT -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right $ bool_ $ x > y + Right $ boolAnn $ x > y _ -> err IntGTE -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right $ bool_ $ x >= y + Right $ boolAnn $ x >= y _ -> err IntEq -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right $ bool_ $ x == y + Right $ boolAnn $ x == y _ -> err IntNeq -> case args of [PrimCon _ (PrimInt x), PrimCon _ (PrimInt y)] -> - Right $ bool_ $ x /= y + Right $ boolAnn $ x /= y _ -> err IntToNat -> case args of [PrimCon _ (PrimInt x)] -> Right $ - if x < 0 - then con cNothing `aPP` tcon tNat - else - con cJust - `aPP` tcon tNat - `app` nat (fromInteger x) + maybeAnn (tcon tNat) nat $ + if x < 0 + then Nothing + else Just $ fromInteger x _ -> err IntFromNat -> case args of [exprToNat -> Just n] -> @@ -283,7 +272,9 @@ primFunDef def args = case def of _ -> err where exprToNat = \case - Con _ c | c == cZero -> Just 0 - App _ (Con _ c) x | c == cSucc -> succ <$> exprToNat x + Con _ c [] | c == cZero -> Just 0 + Con _ c [x] | c == cSucc -> succ <$> exprToNat x + -- TODO (saturated constructors) this line will be unneeded when saturation is enforced + App _ (Con _ c []) x | c == cSucc -> succ <$> exprToNat x _ -> Nothing err = Left $ PrimFunError def args diff --git a/primer/src/Primer/Questions.hs b/primer/src/Primer/Questions.hs index d26792346..8ee6f064b 100644 --- a/primer/src/Primer/Questions.hs +++ b/primer/src/Primer/Questions.hs @@ -25,6 +25,7 @@ import Primer.Core ( TyVarName, Type' (..), ) +import Primer.Core.Transform (decomposeTAppCon) import Primer.Def ( DefMap, defType, @@ -33,7 +34,6 @@ import Primer.Name (Name, unName, unsafeMkName) import Primer.Name.Fresh (mkAvoidForFreshName, mkAvoidForFreshNameTy, mkAvoidForFreshNameTypeZ) import Primer.TypeDef (typeDefNameHints) import Primer.Typecheck.Cxt (Cxt, typeDefs) -import Primer.Typecheck.Utils (decomposeTAppCon) import Primer.Zipper ( ExprZ, TypeZ, diff --git a/primer/src/Primer/Refine.hs b/primer/src/Primer/Refine.hs index 42d67bd61..12759567e 100644 --- a/primer/src/Primer/Refine.hs +++ b/primer/src/Primer/Refine.hs @@ -9,7 +9,7 @@ import Primer.Core.Fresh (freshLocalName) import Primer.Core.Meta (ID, TyVarName) import Primer.Core.Type (Kind, Type' (TForall, TFun, TVar)) import Primer.Name (NameCounter) -import Primer.Subst (substTy, substTys) +import Primer.Subst (substTy, substTySimul) import Primer.Typecheck.Cxt (Cxt) import Primer.Typecheck.Kindcheck qualified as TC import Primer.Unification (InternalUnifyError, unify) @@ -29,7 +29,8 @@ data Inst -- * @e (InstAPP ty)@ represents "apply to the type @ty@: @e \@ty@" -- * @e (InstUnconstrainedAPP _ k)@ represents "apply to some type of kind @k@, but we don't care what" -- --- The names in @InstUnconstrainedAPP@s scope over all the @Inst@s to the right, as well as the returned @Type@. +-- The names in @InstUnconstrainedAPP@s are all unique, and they scope over all +-- the @Inst@s to the right, as well as the returned @Type@. refine :: forall m. (MonadFresh ID m, MonadFresh NameCounter m, MonadError InternalUnifyError m) => @@ -49,14 +50,14 @@ refine cxt tgtTy srcTy = go [] srcTy in unify cxt' uvs tgtTy tmTy >>= \case Just sub -> let f = \case - Left t -> InstApp <$> substTys (Map.toList sub) t -- need to instantiate unif vars + Left t -> InstApp <$> substTySimul sub t -- need to instantiate unif vars Right (v, k) -> pure $ case Map.lookup v sub of Nothing -> InstUnconstrainedAPP v k Just t -> InstAPP t in -- 'instantiation' is built up so the head corresponds to the -- outermost application. Reverse it so the head of the result -- corresponds to the innermost (first) application. - curry Just <$> traverse f (reverse instantiation) <*> substTys (Map.toList sub) tmTy + curry Just <$> traverse f (reverse instantiation) <*> substTySimul sub tmTy Nothing -> case tmTy of TFun _ s t -> go (Left s : instantiation) t TForall _ a k t -> do diff --git a/primer/src/Primer/Subst.hs b/primer/src/Primer/Subst.hs index 01ff5856a..11c09c5f4 100644 --- a/primer/src/Primer/Subst.hs +++ b/primer/src/Primer/Subst.hs @@ -1,50 +1,65 @@ module Primer.Subst ( substTy, - substTys, + substTySimul, ) where import Foreword import Control.Monad.Fresh (MonadFresh) -import Data.Set qualified as Set +import Data.Map qualified as M import Primer.Core.Fresh (freshLocalName) import Primer.Core.Meta (TyVarName) import Primer.Core.Type (Type' (..)) import Primer.Core.Type.Utils (freeVarsTy) import Primer.Name (NameCounter) --- | Simple and inefficient capture-avoiding substitution. --- @substTy n a t@ is @t[a/n]@ +-- | Simple and inefficient capture-avoiding simultaneous substitution. +-- @substTySimul [(a,A),(b,B)] t@ is @t[A,B/a,b]@, where any references to @a,b@ +-- in their replacements @A,B@ are not substituted. -- We restrict to '()', i.e. no metadata as we don't want to duplicate IDs etc -substTy :: MonadFresh NameCounter m => TyVarName -> Type' () -> Type' () -> m (Type' ()) -substTy n a = go +substTySimul :: MonadFresh NameCounter m => Map TyVarName (Type' ()) -> Type' () -> m (Type' ()) +substTySimul sub + | M.null sub = pure + | otherwise = go where - avoid = Set.singleton n <> freeVarsTy a + -- When going under a binder, we must rename it if it may capture a variable + -- from @sub@'s rhs + avoid = foldMap' freeVarsTy sub + -- We must avoid this binder @m@ capturing a free variable in (some rhs of) @sub@ + -- (e.g. @substTy [a :-> T b] (∀b.b a)@ should give @∀c.c (T b)@, and not @∀b.b (T b)@) + -- The generated names will not enter the user's program, so we don't need to worry about shadowing, only variable capture + subUnderBinder m t = do + let sub' = M.delete m sub + (m', sub'') <- + if m `elem` avoid + then do + -- If we are renaming, we + -- - must also avoid capturing any existing free variable + -- - choose to also avoid the names of any variables we are + -- substituting away (for clarity and ease of implementation) + m' <- freshLocalName (avoid <> freeVarsTy t <> M.keysSet sub) + pure (m', M.insert m (TVar () m') sub') + else pure (m, sub') + (m',) <$> substTySimul sub'' t go = \case t@TEmptyHole{} -> pure t THole m t -> THole m <$> go t t@TCon{} -> pure t TFun _ s t -> TFun () <$> go s <*> go t t@(TVar _ m) - | n == m -> pure a + | Just a <- M.lookup m sub -> pure a | otherwise -> pure t TApp _ s t -> TApp () <$> go s <*> go t - t@(TForall _ m k s) - | m == n -> pure t - -- We must avoid this @∀m@ capturing a free variable in @a@ - -- (e.g. @substTy a (T b) (∀b.b a)@ should give @∀c.c (T b)@, and not @∀b.b (T b)@) - -- these names will not enter the user's program, so we don't need to worry about shadowing, only variable capture - | m `elem` avoid -> freshLocalName (avoid <> freeVarsTy s) >>= \m' -> substTy m (TVar () m') s >>= fmap (TForall () m' k) . go - | otherwise -> TForall () m k <$> go s - TLet _ m s b - | m == n -> TLet () m <$> go s <*> pure b - -- We must avoid this let-bound @m@ capturing a free variable in @a@, - -- similarly to the TForall case - | m `elem` avoid -> freshLocalName (avoid <> freeVarsTy b) >>= \m' -> substTy m (TVar () m') b >>= ap (TLet () m' <$> go s) . go - | otherwise -> TLet () m <$> go s <*> go b + TForall _ m k s -> do + (m', s') <- subUnderBinder m s + pure $ TForall () m' k s' + TLet _ m s b -> do + s' <- go s + (m', b') <- subUnderBinder m b + pure $ TLet () m' s' b' --- | Iterated substitution: @substTys [(a,A),(b,B)] ty@ gives @(ty[B/b])[A/a]@. --- Thus if @B@ refers to a variable @a@, this reference will also be --- substituted. -substTys :: MonadFresh NameCounter m => [(TyVarName, Type' ())] -> Type' () -> m (Type' ()) -substTys sb t = foldrM (uncurry substTy) t sb +-- | Simple and inefficient capture-avoiding substitution. +-- @substTy n a t@ is @t[a/n]@ +-- We restrict to '()', i.e. no metadata as we don't want to duplicate IDs etc +substTy :: MonadFresh NameCounter m => TyVarName -> Type' () -> Type' () -> m (Type' ()) +substTy n a = substTySimul $ M.singleton n a diff --git a/primer/src/Primer/TypeDef.hs b/primer/src/Primer/TypeDef.hs index 66c92694c..91877aeee 100644 --- a/primer/src/Primer/TypeDef.hs +++ b/primer/src/Primer/TypeDef.hs @@ -19,9 +19,10 @@ import Primer.Core.Meta ( TyVarName, ValConName, ) +import Primer.Core.Transform (mkTAppCon) import Primer.Core.Type ( Kind (KFun, KType), - Type' (TApp, TCon, TForall, TFun, TVar), + Type' (TForall, TFun, TVar), ) import Primer.JSON ( CustomJSON (CustomJSON), @@ -74,7 +75,7 @@ data ValCon = ValCon valConType :: TyConName -> ASTTypeDef -> ValCon -> Type' () valConType tc td vc = - let ret = foldl' (\t (n, _) -> TApp () t (TVar () n)) (TCon () tc) (astTypeDefParameters td) + let ret = mkTAppCon tc (TVar () . fst <$> astTypeDefParameters td) args = foldr (TFun ()) ret (valConArgs vc) foralls = foldr (\(n, k) t -> TForall () n k t) args (astTypeDefParameters td) in foralls diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index bddf76496..c0f6bf05e 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -63,6 +63,7 @@ import Foreword import Control.Monad.Fresh (MonadFresh (..)) import Control.Monad.NestedError (MonadNestedError (..), modifyError') +import Data.List (lookup) import Data.Map qualified as M import Data.Map.Strict qualified as Map import Data.Set qualified as S @@ -118,6 +119,7 @@ import Primer.Core ( _typeMeta, ) import Primer.Core.DSL (branch, emptyHole, meta, meta') +import Primer.Core.Transform (decomposeTAppCon, mkTAppCon, unfoldTApp) import Primer.Core.Utils ( alphaEqTy, forgetTypeMetadata, @@ -149,7 +151,6 @@ import Primer.TypeDef ( TypeDefMap, ValCon (valConArgs, valConName), typeDefAST, - valConType, ) import Primer.Typecheck.Cxt (Cxt (Cxt, globalCxt, localCxt, smartHoles, typeDefs)) import Primer.Typecheck.Kindcheck ( @@ -170,7 +171,6 @@ import Primer.Typecheck.TypeError (TypeError (..)) import Primer.Typecheck.Utils ( TypeDefError (TDIHoleType, TDINotADT, TDINotSaturated, TDIUnknown), TypeDefInfo (TypeDefInfo), - decomposeTAppCon, getGlobalBaseNames, getGlobalNames, getTypeDefInfo, @@ -179,7 +179,6 @@ import Primer.Typecheck.Utils ( instantiateValCons', lookupConstructor, maybeTypeOf, - mkTAppCon, substituteTypeVars, typeOf, _typecache, @@ -494,12 +493,9 @@ synth = \case -- Annotate the Ann with the same type as e pure $ annSynth2 t'' i Ann e' t' EmptyHole i -> pure $ annSynth0 (TEmptyHole ()) i EmptyHole + -- TODO (saturated constructors): I think this comment has become detached from its code... -- We assume that constructor names are unique -- See Note [Synthesisable constructors] in Core.hs - Con i c -> do - asks (flip lookupConstructor c . typeDefs) >>= \case - Just (vc, tc, td) -> let t = valConType tc td vc in pure $ annSynth1 t i Con c - Nothing -> throwError' $ UnknownConstructor c -- When synthesising a hole, we first check that the expression inside it -- synthesises a type successfully. -- TODO: we would like to remove this hole (leaving e) if possible, but I @@ -514,6 +510,7 @@ synth = \case -- See https://github.com/hackworthltd/primer/issues/7 Hole i e -> do (_, e') <- synth e + -- TODO: document that innards of holes are synth, not chk positions! (Add "Note [Holes and bidirectionality]"?) Also clarify that holes themselves can be in chk or syn position, and thus replaceable with different terms depending on where they are. pure $ annSynth1 (TEmptyHole ()) i Hole e' Let i x a b -> do -- Synthesise a type for the bound expression @@ -554,6 +551,16 @@ synth = \case annSynth3 t i c = annSynth2 t i . flip c annSynth4 t i c = annSynth3 t i . flip c +zipWithExactM :: Applicative f => (a -> b -> f c) -> [a] -> [b] -> Maybe (f [c]) +zipWithExactM _ [] [] = Just $ pure [] +zipWithExactM _ [] _ = Nothing +zipWithExactM _ _ [] = Nothing +zipWithExactM f (x : xs) (y : ys) = ((:) <$> f x y <*>) <$> zipWithExactM f xs ys + +ensureJust :: MonadNestedError e e' m => e -> Maybe (m a) -> m a +ensureJust e Nothing = throwError' e +ensureJust _ (Just x) = x + -- There is a hard-wired map 'primConName' which associates each PrimCon to -- its PrimTypeDef (by name -- PrimTypeDefs have hardwired names). -- However, these PrimTypeDefs may or may not be in the Cxt. @@ -580,6 +587,52 @@ primConInScope pc cxt = -- | Similar to synth, but for checking rather than synthesis. check :: TypeM e m => Type -> Expr -> m ExprT check t = \case + con@(Con i c tms) -> do + -- If the input type @t@ is a hole-applied-to-some-arguments, + -- then refine it to the parent type of @c@ applied to some holes plus those original arguments + (cParent, parentParams) <- + asks (flip lookupConstructor c . typeDefs) >>= \case + Just (_, tn, td) -> pure (tn, length $ astTypeDefParameters td) + Nothing -> throwError' $ UnknownConstructor c -- unrecoverable error, smartholes can do nothing here + let t' = case unfoldTApp t of + (TEmptyHole{}, args) + | missing <- parentParams - length args + , missing >= 0 -> + mkTAppCon cParent $ replicate missing (TEmptyHole ()) <> args + (THole{}, args) + | missing <- parentParams - length args + , missing >= 0 -> + mkTAppCon cParent $ replicate missing (TEmptyHole ()) <> args + _ -> t + -- If typechecking fails because the type @t'@ is not an ADT with a + -- constructor @c@, and smartholes is on, we attempt to change the term to + -- '{? c : ? ?}' to recover. + let recoverSH err = + asks smartHoles >>= \case + NoSmartHoles -> throwError' err + SmartHoles -> do + -- 'synth' will take care of adding an annotation - no need to do it + -- explicitly here + (_, con') <- synth con + Hole <$> meta' (TCEmb TCBoth{tcChkedAt = t', tcSynthed = TEmptyHole ()}) <*> pure con' + instantiateValCons t' >>= \case + Left TDIHoleType -> throwError' $ InternalError "t' is not a hole, as we refined to parent type of c" + Left TDIUnknown{} -> throwError' $ InternalError "input type to check is not in scope" + Left TDINotADT -> recoverSH $ ConstructorNotFullAppADT t' c + Left TDINotSaturated -> recoverSH $ ConstructorNotFullAppADT t' c + -- If the input type @t@ is a fully-applied ADT constructor 'T As' + -- And 'C' is a constructor of 'T' (writing 'T's parameters as 'ps' with kinds 'ks') + -- with arguments 'Rs[ps]', + -- then this particular instantiation should have arguments 'Rs[As]' + Right (tc, _, instVCs) -> case lookup c instVCs of + Nothing -> recoverSH $ ConstructorWrongADT tc c + Just argTys -> do + -- Check that the arguments have the correct type + -- Note that being unsaturated is a fatal error and SmartHoles will not try to recover + -- (this is a design decision -- we put the burden onto code that builds ASTs, + -- e.g. the action code is responsible for only creating saturated constructors) + tms' <- ensureJust (UnsaturatedConstructor c) $ zipWithExactM check argTys tms + pure $ Con (annotate (TCChkedAt t') i) c tms' lam@(Lam i x e) -> do case matchArrowType t of Just (t1, t2) -> do diff --git a/primer/src/Primer/Typecheck/TypeError.hs b/primer/src/Primer/Typecheck/TypeError.hs index bba989e62..ba6214775 100644 --- a/primer/src/Primer/Typecheck/TypeError.hs +++ b/primer/src/Primer/Typecheck/TypeError.hs @@ -13,8 +13,20 @@ data TypeError = InternalError Text | UnknownVariable TmVarRef | TmVarWrongSort Name -- type var instead of term var + | -- | Constructors (term-level) only inhabit fully-applied ADTs + -- i.e. @Maybe a@, but not @Maybe@, @Maybe a b@, @Nat -> Bool@ or holes + ConstructorNotFullAppADT (Type' ()) ValConName + | -- | This ADT does not have a constructor of that name + ConstructorWrongADT TyConName ValConName | UnknownConstructor ValConName - | -- | Cannot use a PrimCon when either no type of the appropriate name is + | -- | Constructors (term-level) must be saturated. + -- This error catches both under- and over-saturation. + UnsaturatedConstructor ValConName + | -- TODO (saturated constructors) currently this catches both "wrong number + -- of type/term arguments", but when constructors become checkable, then + -- they will only have term arguments + + -- | Cannot use a PrimCon when either no type of the appropriate name is -- in scope, or it is a user-defined type PrimitiveTypeNotInScope TyConName | CannotSynthesiseType Expr diff --git a/primer/src/Primer/Typecheck/Utils.hs b/primer/src/Primer/Typecheck/Utils.hs index d2be9b8d2..6865f2d67 100644 --- a/primer/src/Primer/Typecheck/Utils.hs +++ b/primer/src/Primer/Typecheck/Utils.hs @@ -8,8 +8,6 @@ module Primer.Typecheck.Utils ( instantiateValCons, instantiateValCons', lookupConstructor, - mkTAppCon, - decomposeTAppCon, substituteTypeVars, maybeTypeOf, typeOf, @@ -30,7 +28,8 @@ import Data.Tuple.Extra (fst3) import Optics (Lens', view, (%)) import Primer.Core (Expr, Expr', GlobalName (baseName, qualifiedModule), ModuleName, TypeCache, _exprMetaLens) import Primer.Core.Meta (Meta, TyConName, TyVarName, ValConName, _type) -import Primer.Core.Type (Kind, Type' (TApp, TCon, TEmptyHole, THole)) +import Primer.Core.Transform (decomposeTAppCon) +import Primer.Core.Type (Kind, Type' (TEmptyHole, THole)) import Primer.Name (Name, NameCounter) import Primer.Subst (substTy) import Primer.TypeDef ( @@ -52,10 +51,6 @@ lookupConstructor tyDefs c = pure (vc, tc, td) in find ((== c) . valConName . fst3) allCons --- | @mkTAppCon C [X,Y,Z] = C X Y Z@ -mkTAppCon :: TyConName -> [Type' ()] -> Type' () -mkTAppCon c = foldl' (TApp ()) (TCon () c) - data TypeDefError = TDIHoleType -- a type hole | TDINotADT -- e.g. a function type etc @@ -129,18 +124,6 @@ instantiateValCons' tyDefs t = substituteTypeVars :: MonadFresh NameCounter m => [(TyVarName, Type' ())] -> Type' () -> m (Type' ()) substituteTypeVars = flip $ foldrM (uncurry substTy) --- | Decompose @C X Y Z@ to @(C,[X,Y,Z])@ -decomposeTAppCon :: Type' a -> Maybe (TyConName, [Type' a]) -decomposeTAppCon ty = do - (con, args) <- go ty - pure (con, reverse args) - where - go (TCon _ con) = Just (con, []) - go (TApp _ t s) = do - (con, args) <- go t - pure (con, s : args) - go _ = Nothing - -- | Get the (potentially absent) type of an 'Expr' maybeTypeOf :: Expr -> Maybe TypeCache maybeTypeOf = view _typecache diff --git a/primer/src/Primer/Zipper.hs b/primer/src/Primer/Zipper.hs index 5e911d901..69f132dd1 100644 --- a/primer/src/Primer/Zipper.hs +++ b/primer/src/Primer/Zipper.hs @@ -66,7 +66,6 @@ import Foreword import Data.Data (Data) import Data.Generics.Product (position) -import Data.Generics.Uniplate.Data () import Data.Generics.Uniplate.Zipper ( Zipper, fromZipper, @@ -85,6 +84,7 @@ import Optics ( only, preview, set, + singular, view, (%), (.~), @@ -98,7 +98,7 @@ import Primer.Core ( Bind' (..), CaseBranch' (CaseBranch), Expr, - Expr' (Case, LAM, Lam, Let, LetType, Letrec), + Expr' (Case, Con, LAM, Lam, Let, LetType, Letrec), ExprMeta, HasID (..), ID, @@ -249,9 +249,20 @@ instance HasID a => HasID (BindLoc' a b) where -- @Letrec@ or @LetType@ node (as those are the only ones that contain a -- @Type@). focusType :: (Data a, Data b) => ExprZ' a b -> Maybe (TypeZ' a b) -focusType z = do - t <- z ^? l - pure $ TypeZ (zipper t) $ \t' -> z & l .~ t' +-- TODO (saturated constructors): This is incomplete, since currently Con +-- have type arguments. However, this is only a temporary situation, and +-- handling them is difficult, since they have multiple type children we +-- cannot focus on just one! We will put up with this (will need a small +-- workaround in Eval and in focusOn: we can focus on these by ID, just +-- not via focusType!) until constructors no longer store their indices. +-- Whilst we could use 'singular' to focus on the first index of a constructor, +-- we prefer to focus on *no* type children of constructors, rather than +-- arbitrarily choosing the first one. +focusType z = case target z of + Con{} -> Nothing + _ -> do + t <- z ^? singular l + pure $ TypeZ (zipper t) $ \t' -> z & l .~ t' where l = _target % typesInExpr diff --git a/primer/test/Tests/API.hs b/primer/test/Tests/API.hs index 34ad3f53d..cdf3e4b2e 100644 --- a/primer/test/Tests/API.hs +++ b/primer/test/Tests/API.hs @@ -87,7 +87,7 @@ test_golden = unit_viewTreeExpr_injective_con :: Assertion unit_viewTreeExpr_injective_con = - distinctTreeExpr (con' ["M"] "C") (con' ["M"] "D") + distinctTreeExpr (con0' ["M"] "C") (con0' ["M"] "D") unit_viewTreeExpr_injective_lam :: Assertion unit_viewTreeExpr_injective_lam = diff --git a/primer/test/Tests/Action.hs b/primer/test/Tests/Action.hs index f50418a73..536d54dbe 100644 --- a/primer/test/Tests/Action.hs +++ b/primer/test/Tests/Action.hs @@ -27,7 +27,10 @@ import Primer.Core ( Kind (KType), PrimCon (PrimChar), TmVarRef (LocalVarRef), + TyConName, + ValConName, getID, + unsafeMkLocalName, ) import Primer.Core.DSL import Primer.Gen.Core.Raw ( @@ -37,7 +40,7 @@ import Primer.Gen.Core.Raw ( import Primer.Module (builtinModule, primitiveModule) import Primer.Primitives (tChar, tInt) import Primer.Test.TestM (evalTestM) -import Primer.Test.Util (clearMeta, constructCon, constructRefinedCon, constructTCon) +import Primer.Test.Util (clearMeta, constructRefinedCon, constructSaturatedCon, constructTCon) import Primer.Typecheck (SmartHoles (NoSmartHoles, SmartHoles)) import Primer.Zipper ( down, @@ -236,9 +239,9 @@ unit_8 = , Move Parent , ConstructApp , Move Child2 - , constructCon cTrue + , constructSaturatedCon cTrue ] - (app (ann (lam "x" (lvar "x")) (tfun (tcon tBool) (tcon tBool))) (con cTrue)) + (app (ann (lam "x" (lvar "x")) (tfun (tcon tBool) (tcon tBool))) (con0 cTrue)) unit_9 :: Assertion unit_9 = @@ -247,12 +250,18 @@ unit_9 = emptyHole [ ConstructLet (Just "x") , Move Child1 - , constructCon cTrue + , ConstructAnn + , Move Child1 + , constructSaturatedCon cTrue + , Move Parent + , EnterType + , constructTCon tBool + , ExitType , Move Parent , Move Child2 , ConstructVar $ LocalVarRef "x" ] - (let_ "x" (con cTrue) (lvar "x")) + (let_ "x" (con0 cTrue `ann` tcon tBool) (lvar "x")) unit_construct_arrow_left :: Assertion unit_construct_arrow_left = @@ -291,9 +300,9 @@ unit_rename_let :: Assertion unit_rename_let = actionTest NoSmartHoles - (let_ "x" (con cTrue) (lvar "x")) + (let_ "x" (con0 cTrue `ann` tEmptyHole) (lvar "x")) [RenameLet "y"] - (let_ "y" (con cTrue) (lvar "y")) + (let_ "y" (con0 cTrue `ann` tEmptyHole) (lvar "y")) unit_rename_letrec :: Assertion unit_rename_letrec = @@ -325,9 +334,9 @@ unit_rename_lam :: Assertion unit_rename_lam = actionTest NoSmartHoles - (ann (lam "x" (app (lvar "x") (con cFalse))) tEmptyHole) + (ann (lam "x" (app (lvar "x") (con0 cFalse))) tEmptyHole) [Move Child1, RenameLam "y"] - (ann (lam "y" (app (lvar "y") (con cFalse))) tEmptyHole) + (ann (lam "y" (app (lvar "y") (con0 cFalse))) tEmptyHole) unit_rename_lam_2 :: Assertion unit_rename_lam_2 = @@ -341,25 +350,25 @@ unit_rename_LAM :: Assertion unit_rename_LAM = actionTest NoSmartHoles - (ann (lAM "a" (aPP (con cNil) (tvar "a"))) (tforall "b" KType $ listOf (tvar "b"))) + (ann (lAM "a" (emptyHole `aPP` tvar "a")) (tforall "b" KType $ listOf (tvar "b"))) [Move Child1, RenameLAM "b"] - (ann (lAM "b" (aPP (con cNil) (tvar "b"))) (tforall "b" KType $ listOf (tvar "b"))) + (ann (lAM "b" (emptyHole `aPP` tvar "b")) (tforall "b" KType $ listOf (tvar "b"))) unit_rename_LAM_2 :: Assertion unit_rename_LAM_2 = actionTestExpectFail (const True) NoSmartHoles - (ann (lAM "b" (lAM "a" (aPP (con cNil) (tvar "b")))) tEmptyHole) + (ann (lAM "b" (lAM "a" (emptyHole `aPP` tvar "b"))) tEmptyHole) [Move Child1, Move Child1, RenameLAM "b"] unit_convert_let_to_letrec :: Assertion unit_convert_let_to_letrec = actionTest NoSmartHoles - (let_ "x" (con cTrue) (lvar "x")) + (let_ "x" (con0 cTrue) (lvar "x")) [ConvertLetToLetrec] - (letrec "x" (con cTrue) tEmptyHole (lvar "x")) + (letrec "x" (con0 cTrue) tEmptyHole (lvar "x")) unit_delete_type :: Assertion unit_delete_type = @@ -384,7 +393,7 @@ unit_bad_constructor = (const True) NoSmartHoles emptyHole - [ConstructCon (["M"], "NotARealConstructor")] + [ConstructSaturatedCon (["M"], "NotARealConstructor")] unit_bad_type_constructor :: Assertion unit_bad_type_constructor = @@ -399,7 +408,7 @@ unit_bad_app = actionTestExpectFail (const True) NoSmartHoles - (con cTrue) + (con0 cTrue) [ConstructApp] unit_insert_expr_in_type :: Assertion @@ -408,7 +417,7 @@ unit_insert_expr_in_type = (const True) NoSmartHoles (ann emptyHole tEmptyHole) - [EnterType, constructCon cTrue] + [EnterType, constructSaturatedCon cTrue] unit_bad_lambda :: Assertion unit_bad_lambda = @@ -423,16 +432,16 @@ unit_enter_emptyHole = actionTest NoSmartHoles emptyHole - [EnterHole, constructCon cTrue] - (hole $ con cTrue) + [EnterHole, ConstructAnn, Move Child1, constructSaturatedCon cTrue] + (hole $ con0 cTrue `ann` tEmptyHole) unit_enter_nonEmptyHole :: Assertion unit_enter_nonEmptyHole = actionTest NoSmartHoles (hole emptyHole) - [Move Child1, constructCon cTrue] - (hole $ con cTrue) + [Move Child1, ConstructAnn, Move Child1, constructSaturatedCon cTrue] + (hole $ con0 cTrue `ann` tEmptyHole) unit_bad_enter_hole :: Assertion unit_bad_enter_hole = @@ -459,7 +468,7 @@ unit_case_create = , Move Child1 , ConstructCase , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam "x" $ @@ -467,7 +476,7 @@ unit_case_create = ann ( case_ (lvar "x") - [branch cTrue [] (con cZero), branch cFalse [] emptyHole] + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) tEmptyHole ) @@ -485,7 +494,7 @@ unit_case_tidy = ann ( case_ (lvar "x") - [branch cTrue [] (con cZero), branch cFalse [] emptyHole] + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) tEmptyHole ) @@ -496,7 +505,7 @@ unit_case_tidy = ( lam "x" $ case_ (lvar "x") - [branch cTrue [] (con cZero), branch cFalse [] emptyHole] + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) (tfun (tcon tBool) (tcon tNat)) ) @@ -523,7 +532,7 @@ unit_case_move_branch_1 = , Move Child1 , Move Child1 , Move (Branch cZero) - , constructCon cZero + , constructSaturatedCon cZero , Move Parent , Move (Branch cSucc) , ConstructVar $ LocalVarRef "n" @@ -534,7 +543,7 @@ unit_case_move_branch_1 = ann ( case_ (lvar "x") - [branch cZero [] (con cZero), branch cSucc [("n", Nothing)] (lvar "n")] + [branch cZero [] (con0 cZero), branch cSucc [("n", Nothing)] (lvar "n")] ) tEmptyHole ) @@ -557,7 +566,7 @@ unit_case_move_branch_2 = [ Move Child1 , Move Child1 , Move (Branch cZero) - , constructCon cZero + , constructSaturatedCon cZero , Move Parent , Move (Branch cSucc) , ConstructVar $ LocalVarRef "n" @@ -566,7 +575,7 @@ unit_case_move_branch_2 = ( lam "x" $ case_ (lvar "x") - [branch cZero [] (con cZero), branch cSucc [("n", Nothing)] (lvar "n")] + [branch cZero [] (con0 cZero), branch cSucc [("n", Nothing)] (lvar "n")] ) (tfun (tcon tNat) (tcon tNat)) ) @@ -742,14 +751,14 @@ unit_case_create_smart_on_term = , ConstructVar $ LocalVarRef "x" , ConstructCase , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam "x" ( case_ (lvar "x") - [branch cTrue [] (con cZero), branch cFalse [] emptyHole] + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) ) (tfun (tcon tBool) (tcon tNat)) @@ -770,14 +779,14 @@ unit_case_create_smart_on_hole = , ConstructVar $ LocalVarRef "x" , Move Parent , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam "x" ( case_ (lvar "x") - [branch cTrue [] (con cZero), branch cFalse [] emptyHole] + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) ) (tfun (tcon tBool) (tcon tNat)) @@ -789,20 +798,22 @@ unit_case_change_smart_scrutinee_type = SmartHoles ( ann ( case_ - (con cTrue) - [branch cTrue [] (con cZero), branch cFalse [] emptyHole] + (con0 cTrue `ann` tcon tBool) + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) (tcon tNat) ) [ Move Child1 , Move Child1 , Delete - , constructCon cZero + , ConstructAnn + , EnterType + , constructTCon tNat ] ( ann ( case_ - (con cZero) - [branch cZero [] emptyHole, branch cSucc [("a11", Nothing)] emptyHole] -- fragile names here + (emptyHole `ann` tcon tNat) + [branch cZero [] emptyHole, branch cSucc [("a15", Nothing)] emptyHole] -- fragile names here ) (tcon tNat) ) @@ -865,17 +876,17 @@ unit_constructAPP :: Assertion unit_constructAPP = actionTest NoSmartHoles - (con cNil) + emptyHole [ConstructAPP, EnterType, constructTCon tBool] - (con cNil `aPP` tcon tBool) + (emptyHole `aPP` tcon tBool) unit_constructLAM :: Assertion unit_constructLAM = actionTest NoSmartHoles (emptyHole `ann` tEmptyHole) - [Move Child1, ConstructLAM (Just "a"), constructCon cTrue] - (lAM "a" (con cTrue) `ann` tEmptyHole) + [Move Child1, ConstructLAM (Just "a"), constructSaturatedCon cTrue] + (lAM "a" (con0 cTrue) `ann` tEmptyHole) unit_construct_TForall :: Assertion unit_construct_TForall = @@ -972,17 +983,17 @@ unit_construct_lam :: Assertion unit_construct_lam = actionTest SmartHoles - (con cTrue) + (con0 cTrue) [ConstructLam (Just "x")] - (ann (lam "x" (con cTrue)) tEmptyHole) + (ann (lam "x" (con0 cTrue)) tEmptyHole) unit_construct_LAM :: Assertion unit_construct_LAM = actionTest SmartHoles - (con cTrue) + (con0 cTrue) [ConstructLAM (Just "a")] - (ann (lAM "a" (con cTrue)) tEmptyHole) + (ann (lAM "a" (con0 cTrue)) tEmptyHole) unit_smart_type_1 :: Assertion unit_smart_type_1 = @@ -1014,7 +1025,7 @@ unit_refine_2 = NoSmartHoles (emptyHole `ann` (tcon tList `tapp` tcon tNat)) [Move Child1, constructRefinedCon cNil] - ((con cNil `aPP` tcon tNat) `ann` (tcon tList `tapp` tcon tNat)) + (con cNil [] `ann` (tcon tList `tapp` tcon tNat)) unit_refine_3 :: Assertion unit_refine_3 = @@ -1022,23 +1033,64 @@ unit_refine_3 = NoSmartHoles (emptyHole `ann` (tcon tList `tapp` tEmptyHole)) [Move Child1, constructRefinedCon cNil] - ((con cNil `aPP` tEmptyHole) `ann` (tcon tList `tapp` tEmptyHole)) + (con cNil [] `ann` (tcon tList `tapp` tEmptyHole)) unit_refine_4 :: Assertion unit_refine_4 = actionTest NoSmartHoles - (let_ "nil" (con cNil) $ emptyHole `ann` (tcon tList `tapp` tcon tNat)) + -- REVIEW (saturated constructors): for enforced-saturation, eta expansion is necessary here + -- Even though constructors are (may be changed later) synthesisable, their eta expansions are not + -- Thus an annotation is required! + (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tcon tNat)) [Move Child2, Move Child1, InsertRefinedVar $ LocalVarRef "nil"] - (let_ "nil" (con cNil) $ (lvar "nil" `aPP` tcon tNat) `ann` (tcon tList `tapp` tcon tNat)) + (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tcon tNat) `ann` (tcon tList `tapp` tcon tNat)) unit_refine_5 :: Assertion unit_refine_5 = actionTest NoSmartHoles - (let_ "nil" (con cNil) $ emptyHole `ann` (tcon tList `tapp` tEmptyHole)) + -- REVIEW (saturated constructors): see comments on unit_refine_4 r.e. eta only checkable + (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tEmptyHole)) [Move Child2, Move Child1, InsertRefinedVar $ LocalVarRef "nil"] - (let_ "nil" (con cNil) $ (lvar "nil" `aPP` tEmptyHole) `ann` (tcon tList `tapp` tEmptyHole)) + (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tEmptyHole) `ann` (tcon tList `tapp` tEmptyHole)) + +unit_refine_mismatch :: Assertion +unit_refine_mismatch = + actionTest + SmartHoles + (emptyHole `ann` tcon tNat) + [Move Child1, constructRefinedCon cCons] + (hole (con cCons [emptyHole, emptyHole] `ann` tEmptyHole) `ann` tcon tNat) + +-- REVIEW: perhaps we should be clever and eta expand? As a different action? +-- +-- Constructors are saturated, so if the hole has an arrow type, when we insert +-- a constructor it cannot match the arrow, so it is inserted into a hole +unit_refine_arr_1 :: Assertion +unit_refine_arr_1 = + actionTest + -- REVIEW: do we care about NoSmartHoles? Currently we rely on SH to insert the inner annotation here + SmartHoles + (emptyHole `ann` (tEmptyHole `tfun` tEmptyHole)) + [Move Child1, constructRefinedCon cCons] + (hole (con cCons [emptyHole, emptyHole] `ann` tEmptyHole) `ann` (tEmptyHole `tfun` tEmptyHole)) + +-- TODO (saturated constructors) update this comment for ctors-dont-store-indices ('Cons Nat') +-- +-- Constructors are checkable and fully saturated, so even if the hole has type +-- @List Nat -> List Nat@, when we insert a @Cons@ constructor, we end up with +-- @{? Cons ? ? ? :: ? ?}@ +-- (the inside of a hole is synthesisable position: see Note [Holes and bidirectionality]) +unit_refine_arr_2 :: Assertion +unit_refine_arr_2 = + actionTest + SmartHoles + -- TODO (saturated constructors) REVIEW: if want to eta-expand, then maybe want to get + -- @{? Cons Nat ? ? :: List Nat ?}@ in the hole? + (emptyHole `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) + [Move Child1, constructRefinedCon cCons] + (hole (con cCons [emptyHole, emptyHole] `ann` tEmptyHole) `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) unit_primitive_1 :: Assertion unit_primitive_1 = @@ -1059,11 +1111,45 @@ unit_primitive_1 = ] (lam "x" (char 'c') `ann` (tcon tInt `tfun` tcon tChar)) +-- This tests both that +-- - actions to move into/out of constructor arguments work correctly +-- - and constructEtaAnnCon is implemented correctly +unit_constructEtaAnnCon :: Assertion +unit_constructEtaAnnCon = + actionTest + NoSmartHoles + emptyHole + (constructEtaAnnCon cMakePair [tNat, tBool] [("n", tNat), ("m", tBool)] tPair) + ( lam "n" (lam "m" $ con cMakePair [lvar "n", lvar "m"]) + `ann` (tcon tNat `tfun` (tcon tBool `tfun` (tcon tPair `tapp` tcon tNat `tapp` tcon tBool))) + ) + -- * Helpers +-- Firstly, a helper for Tests.Action.Prog.unit_cross_module_actions +-- @constructEtaAnnCon@ c Ts [(a,A),...,(z,Z)] R makes +-- @Lam a. ... Lam z. Con c [a...z] :: A -> ... -> Z -> R Ts@ +-- but (for ease of implementation) only works for type constructors Ts, A...Z, R +-- (we assume that the correct number of args are given for the constructor's definition) +-- It leaves the cursor on the Ann node (i.e. the root of the thing it constructed) +constructEtaAnnCon :: ValConName -> [TyConName] -> [(Text, TyConName)] -> TyConName -> [Action] +constructEtaAnnCon c tyargs tmargs resultTy = + [ConstructAnn, EnterType] -- ? :: ? + <> concatMap (\(_, t) -> [ConstructArrowL, Move Child1, constructTCon t, Move Parent, Move Child2]) tmargs -- ? :: A -> ... -> Z -> ? + <> concatMap (\a -> [ConstructTApp, Move Child2, constructTCon a, Move Parent, Move Child1]) (reverse tyargs) -- ? :: A -> ... -> Z -> ? Ts + <> [constructTCon resultTy] -- ? :: A -> ... -> Z -> R Ts + <> replicate (length tyargs) (Move Parent) + <> replicate (length tmargs) (Move Parent) + <> [ExitType, Move Child1] -- ? :: A -> ... -> Z -> R Ts + <> map (\(n, _) -> ConstructLam $ Just n) tmargs -- \a....\z.? :: A -> ... -> Z -> R Ts + <> [constructSaturatedCon c] -- \a....\z. Con c [?,...,?] :: A -> ... -> Z -> R Ts + <> concatMap (\(i, (n, _)) -> [Move (ConChild i), ConstructVar $ LocalVarRef $ unsafeMkLocalName n, Move Parent]) (zip [0 ..] tmargs) -- \a....\z. Con c Ts [a,...,z] :: A -> ... -> Z -> R Ts + <> replicate (length tmargs) (Move Parent) + <> [Move Parent] + -- | Apply the actions to the input expression and test that the result matches -- the expected output, up to renaming of IDs and changing cached types. -actionTest :: SmartHoles -> S Expr -> [Action] -> S Expr -> Assertion +actionTest :: HasCallStack => SmartHoles -> S Expr -> [Action] -> S Expr -> Assertion actionTest sh inputExpr actions expectedOutput = do let (expr, i) = create inputExpr result <- either (assertFailure . show) pure $ runTestActions sh i expr actions @@ -1075,7 +1161,7 @@ actionTest sh inputExpr actions expectedOutput = do -- | Attempt to apply the actions to the input expression and test that they -- in fact cause an error to be raised. -actionTestExpectFail :: (ActionError -> Bool) -> SmartHoles -> S Expr -> [Action] -> Assertion +actionTestExpectFail :: HasCallStack => (ActionError -> Bool) -> SmartHoles -> S Expr -> [Action] -> Assertion actionTestExpectFail f sh expr actions = case runTestActions sh i e actions of Right _ -> assertFailure "action succeeded" diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 9096cd39a..8703b9beb 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -1,3 +1,6 @@ +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedRecordDot #-} + module Tests.Action.Available where import Foreword @@ -23,14 +26,17 @@ import Hedgehog ( import Hedgehog.Gen qualified as Gen import Hedgehog.Internal.Property (forAllWithT) import Hedgehog.Range qualified as Range -import Optics (toListOf, (%), (^..)) -import Primer.Action (ActionError (CaseBindsClash, NameCapture), toProgActionInput, toProgActionNoInput) +import Optics (ix, toListOf, (%), (.~), (^..), _head) +import Primer.Action (ActionError (CaseBindsClash, NameCapture), Movement (Child1, Child2), moveExpr, toProgActionInput, toProgActionNoInput) +import Primer.Action.Available (InputAction (MakeConSat), NoInputAction (Raise), Option (Option)) import Primer.Action.Available qualified as Available import Primer.App ( App, EditAppM, Editable (..), + Level (Beginner), NodeType (..), + Prog (..), ProgError (ActionError, DefAlreadyExists), appProg, checkAppWellFormed, @@ -40,22 +46,37 @@ import Primer.App ( progCxt, runEditAppM, ) +import Primer.Builtins (builtinModuleName, cCons, cTrue, tList, tNat) import Primer.Core ( + Expr, GVarName, GlobalName (baseName, qualifiedModule), HasID (_id), ID, - ModuleName (ModuleName), + ModuleName (ModuleName, unModuleName), + getID, mkSimpleModuleName, moduleNamePretty, qualifyName, _typeMeta, ) import Primer.Core.DSL ( + S, + ann, + app, + con, + con0, + create, create', emptyHole, gvar, + hole, + lam, + lvar, tEmptyHole, + tapp, + tcon, + tfun, ) import Primer.Core.Utils ( exprIDs, @@ -74,22 +95,27 @@ import Primer.Log (PureLog, runPureLog) import Primer.Module ( Module (Module, moduleDefs), builtinModule, + moduleDefsQualified, moduleTypesQualified, primitiveModule, ) import Primer.Name (Name (unName)) -import Primer.Test.Util (testNoSevereLogs) +import Primer.Test.TestM (evalTestM) +import Primer.Test.Util (clearMeta, testNoSevereLogs) import Primer.Typecheck ( CheckEverythingRequest (CheckEverything, toCheck, trusted), SmartHoles (NoSmartHoles, SmartHoles), buildTypingContextFromModules, checkEverything, + typeDefs, ) +import Primer.Zipper (focus) import System.FilePath (()) import Tasty (Property, withDiscards, withTests) import Test.Tasty (TestTree, testGroup) import Test.Tasty.Golden (goldenVsString) -import Test.Tasty.HUnit (Assertion, (@?=)) +import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=)) +import Tests.Action.Prog (defaultEmptyProg, expectSuccess, findGlobalByName, gvn, progActionTest) import Tests.Typecheck (TypeCacheAlpha (TypeCacheAlpha), runTypecheckTestMIn) import Text.Pretty.Simple (pShowNoColor) @@ -218,14 +244,14 @@ tasty_available_actions_accepted = withTests 500 $ let ty = astDefType d' ids = ty ^.. typeIDs i <- Gen.element ids - let ann = "actionsForDefSig id " <> show i - pure (ann, (Just (SigNode, i), Available.forSig l defMut ty i)) + let ann' = "actionsForDefSig id " <> show i + pure (ann', (Just (SigNode, i), Available.forSig l defMut ty i)) , defAST def <&> \d' -> (7,) $ do let expr = astDefExpr d' ids = expr ^.. exprIDs i <- Gen.element ids - let ann = "actionsForDefBody id " <> show i - pure (ann, (Just (BodyNode, i), Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i)) + let ann' = "actionsForDefBody id " <> show i + pure (ann', (Just (BodyNode, i), Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i)) ] case acts of [] -> label "no offered actions" >> success @@ -296,3 +322,112 @@ tasty_available_actions_accepted = withTests 500 $ ensureSHNormal a = case checkAppWellFormed a of Left err -> annotateShow err >> failure Right a' -> TypeCacheAlpha a === TypeCacheAlpha a' + +-- 'Raise' works when moving checkable terms into synthesisable position +unit_raise_sh :: Assertion +unit_raise_sh = + let test :: HasCallStack => S Expr -> S Expr -> Assertion + test t1 t2 = + offeredActionTest + SmartHoles + Beginner + (emptyHole `app` t1 `app` emptyHole) + [Child1, Child2] + (Left Raise) + (t2 `app` emptyHole) + testSyn :: HasCallStack => S Expr -> Assertion + testSyn e = test e e + testChk :: HasCallStack => S Expr -> Assertion + testChk t = test t (t `ann` tEmptyHole) + in do + testSyn emptyHole + testChk $ lam "x" (lvar "x") + testChk $ con0 cTrue + +unit_sat_con_1 :: Assertion +unit_sat_con_1 = + offeredActionTest + SmartHoles + Beginner + (emptyHole `ann` (tEmptyHole `tfun` tEmptyHole)) + [Child1] + (Right (MakeConSat, Option "Cons" $ Just $ unName <$> unModuleName builtinModuleName)) + (hole (con cCons [emptyHole, emptyHole] `ann` tEmptyHole) `ann` (tEmptyHole `tfun` tEmptyHole)) + +unit_sat_con_2 :: Assertion +unit_sat_con_2 = + offeredActionTest + SmartHoles + Beginner + (emptyHole `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) + [Child1] + (Right (MakeConSat, Option "Cons" $ Just $ unName <$> unModuleName builtinModuleName)) + (hole (con cCons [emptyHole, emptyHole] `ann` tEmptyHole) `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) + +-- | Apply the action to the node in the input expression pointed to by the +-- 'Movement' (starting from the root), checking that it would actually be offered +-- there, and then checking the result matches the expected output, up to renaming +-- of IDs and changing cached types. +offeredActionTest :: + HasCallStack => + SmartHoles -> + Level -> + S Expr -> + [Movement] -> + Either NoInputAction (InputAction, Option) -> + S Expr -> + Assertion +offeredActionTest sh l inputExpr position action expectedOutput = do + let modules = [builtinModule] + let ((expr, exprDef, exprDefName, prog), i) = create $ do + prog0 <- defaultEmptyProg + e <- inputExpr + d <- ASTDef e <$> tEmptyHole + let p = + prog0 + & (#progModules % _head % #moduleDefs % ix "main" .~ DefAST d) + & (#progImports .~ modules) + pure (e, d, gvn "main", p) + let id' = evalTestM (i + 1) $ + runExceptT $ + flip runReaderT (buildTypingContextFromModules modules sh) $ + do + ez <- foldlM (flip moveExpr) (focus expr) position + pure $ getID ez + id <- case id' of + Left err -> assertFailure $ show err + Right i' -> pure i' + let cxt = buildTypingContextFromModules modules sh + let defs = foldMap' moduleDefsQualified modules + let offered = Available.forBody cxt.typeDefs l Editable expr id + let options = Available.options cxt.typeDefs defs cxt l exprDef (Just (BodyNode, id)) + let assertElem msg x xs = + assertBool + ( msg + <> show x + <> " is not an element of " + <> show xs + ) + (x `elem` xs) + let assertOffered a = assertElem "Requested action not offered: " a offered + action' <- case action of + Left a -> do + assertOffered $ Available.NoInput a + pure $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) exprDef exprDefName (Just (BodyNode, id)) a + Right (a, o) -> do + assertOffered $ Available.Input a + case options a of + Nothing -> assertFailure "Available.options returned Nothing" + Just os -> do + assertElem "Requested option not offered: " o os.opts + pure $ toProgActionInput exprDef exprDefName (Just (BodyNode, id)) o a + action'' <- case action' of + Left err -> assertFailure $ show err + Right a -> pure a + let expected = create' expectedOutput + progActionTest (pure prog) action'' $ expectSuccess $ \_ prog' -> + let result = pure . astDefExpr <=< defAST <=< findGlobalByName prog' $ exprDefName + in -- Compare result to input, ignoring any difference in metadata + -- NB: we don't compare up-to-alpha, as names should be determined by the + -- actions on-the-nose + fmap clearMeta result @?= Just (clearMeta expected) diff --git a/primer/test/Tests/Action/Capture.hs b/primer/test/Tests/Action/Capture.hs index ec1067f61..3d6398a19 100644 --- a/primer/test/Tests/Action/Capture.hs +++ b/primer/test/Tests/Action/Capture.hs @@ -8,7 +8,6 @@ import Primer.Action ( ActionError (NameCapture, NeedEmptyHole), Movement (..), ) -import Primer.Builtins import Primer.Core ( Kind (KType), ) @@ -160,7 +159,7 @@ unit_ty_tm_same_namespace = actionTestExpectFail isNameCapture NoSmartHoles - (ann (lAM "a" $ con cNil `aPP` tvar "a") tEmptyHole) + (ann (lAM "a" $ emptyHole `ann` tvar "a") tEmptyHole) [Move Child1, Move Child1, ConstructLam (Just "a")] -- * Helpers diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 9cab4e1a0..4520f54f6 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -88,12 +88,12 @@ import Primer.Core ( ) import Primer.Core.DSL ( S, - aPP, ann, app, branch, case_, con, + con0, create, create', emptyHole, @@ -116,7 +116,7 @@ import Primer.Module (Module (Module, moduleDefs, moduleName, moduleTypes), buil import Primer.Name import Primer.Primitives (PrimDef (IntAdd, ToUpper), primitiveGVar, tChar) import Primer.Test.TestM (TestM, evalTestM) -import Primer.Test.Util (LogMsg, assertNoSevereLogs, constructCon, constructTCon, zeroIDs, zeroTypeIDs) +import Primer.Test.Util (LogMsg, assertNoSevereLogs, constructSaturatedCon, constructTCon, zeroIDs, zeroTypeIDs) import Primer.Test.Util qualified as Util import Primer.TypeDef (ASTTypeDef (..), TypeDef (..), ValCon (..), typeDefAST) import Primer.Typecheck ( @@ -125,6 +125,7 @@ import Primer.Typecheck ( TypeError (KindError), ) import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@=?), (@?=)) +import Tests.Action (constructEtaAnnCon) import Tests.Typecheck (checkProgWellFormed) import Prelude (error) @@ -530,7 +531,7 @@ unit_copy_paste_duplicate = do toDef = gvn "blank" ((p, fromType, fromExpr, _toType, _toExpr), maxID) = create $ do mainType <- tforall "a" KType (tvar "a" `tfun` (tcon tMaybe `tapp` tEmptyHole)) - mainExpr <- lAM "b" $ lam "x" $ con cJust `aPP` tvar "b" `app` lvar "x" + mainExpr <- lAM "b" $ lam "x" $ con cJust [lvar "x"] let mainDef = ASTDef mainExpr mainType blankDef <- ASTDef <$> emptyHole <*> tEmptyHole pure @@ -628,16 +629,16 @@ unit_raise = do clearDefMapIDs (foldMap' moduleDefsQualified $ progModules r) @?= clearDefMapIDs (foldMap' moduleDefsQualified $ progModules tcpExpected) -- ∀a. List a -> ∀b. b -> Pair a b --- /\a . λ x . case x of Nil -> ? ; Cons y ys -> /\@b z -> Pair @a @b y z --- copy the Just @a y into the hole to get --- /\a . λ x . case x of Nil -> lettype b = ? in let y = ? : a in Pair @a @b y z ; Cons y ys -> /\@b z -> Pair @a @b y z +-- /\a . λ x . case x of Nil -> ? ; Cons y ys -> /\b . λz . MakePair (y : a) (z : b) +-- copy the MakePair @a @b y z into the hole to get +-- /\a . λ x . case x of Nil -> MakePair (? : a) (? : ?) ; Cons y ys -> /\b . λz . MakePair (y : a) (z : b) unit_copy_paste_expr_1 :: Assertion unit_copy_paste_expr_1 = do let mainName' = "main" mainName = gvn mainName' ((pInitial, srcID, pExpected), maxID) = create $ do ty <- tforall "a" KType $ (tcon tList `tapp` tvar "a") `tfun` tforall "b" KType (tvar "b" `tfun` (tcon tPair `tapp` tvar "a" `tapp` tvar "b")) - let toCopy' = con cMakePair `aPP` tvar "a" `aPP` tvar "b" `app` lvar "y" `app` lvar "z" -- want different IDs for the two occurences in expected + 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" $ @@ -647,7 +648,7 @@ unit_copy_paste_expr_1 = do [ branch cNil [] r , branch cCons [("y", Nothing), ("ys", Nothing)] $ lAM "b" $ lam "z" $ pure toCopy ] - expectPasted <- con cMakePair `aPP` tvar "a" `aPP` tEmptyHole `app` emptyHole `app` emptyHole + 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 -- expectPasted <- letType "b" tEmptyHole $ let_ "y" (emptyHole `ann` tvar "a") $ let_ "z" (emptyHole `ann` tvar "b") toCopy' @@ -886,12 +887,12 @@ unit_RenameCon = hole ( hole $ case_ - ( con cA - `aPP` tEmptyHole - `aPP` tEmptyHole - `app` con (vcn "True") - `app` con (vcn "True") - `app` con (vcn "True") + ( con + cA + [ con0 (vcn "True") + , con0 (vcn "True") + , con0 (vcn "True") + ] ) [ branch cA [("p", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole , branch cB [("r", Nothing), ("x", Nothing)] emptyHole @@ -915,12 +916,12 @@ unit_RenameCon = hole ( hole $ case_ - ( con (vcn "A'") - `aPP` tEmptyHole - `aPP` tEmptyHole - `app` con (vcn "True") - `app` con (vcn "True") - `app` con (vcn "True") + ( con + (vcn "A'") + [ con0 (vcn "True") + , con0 (vcn "True") + , con0 (vcn "True") + ] ) [ branch (vcn "A'") [("p", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole , branch cB [("r", Nothing), ("x", Nothing)] emptyHole @@ -937,7 +938,7 @@ unit_RenameCon_clash = x <- hole ( hole - (con cA) + (con0 cA) ) astDef "def" x <$> tEmptyHole ] @@ -1007,12 +1008,12 @@ unit_SetConFieldType = progActionTest ( defaultProgEditableTypeDefs . sequence . pure $ do x <- - con cA - `aPP` tEmptyHole - `aPP` tEmptyHole - `app` con (vcn "True") - `app` con (vcn "True") - `app` con (vcn "True") + con + cA + [ con0 (vcn "True") + , con0 (vcn "True") + , con0 (vcn "True") + ] astDef "def" x <$> tEmptyHole ) [SetConFieldType tT cA 1 $ TCon () (tcn "Int")] @@ -1027,33 +1028,25 @@ unit_SetConFieldType = forgetMetadata (astDefExpr def) @?= forgetMetadata ( create' $ - con cA - `aPP` tEmptyHole - `aPP` tEmptyHole - `app` con (vcn "True") - `app` hole (con (vcn "True")) - `app` con (vcn "True") + con + cA + [ con0 (vcn "True") + , hole (con0 (vcn "True")) + , con0 (vcn "True") + ] ) unit_SetConFieldType_partial_app :: Assertion unit_SetConFieldType_partial_app = progActionTest ( defaultProgEditableTypeDefs $ do - x <- con cA `app` lvar "x" + x <- con cA [lvar "x"] sequence [ astDef "def" x <$> tcon tT ] ) [SetConFieldType tT cA 1 $ TCon () (tcn "Int")] - $ expectSuccess - $ \_ prog' -> do - def <- findDef (gvn "def") prog' - forgetMetadata (astDefExpr def) - @?= forgetMetadata - ( create' $ - hole $ - con cA `app` lvar "x" - ) + $ expectError (@?= ConNotSaturated cA) unit_SetConFieldType_case :: Assertion unit_SetConFieldType_case = @@ -1130,12 +1123,13 @@ unit_AddConField = ( defaultProgEditableTypeDefs $ do x <- case_ - ( con cA - `aPP` tEmptyHole - `aPP` tEmptyHole - `app` con (vcn "True") - `app` con (vcn "True") - `app` con (vcn "True") + ( con + cA + [ con0 (vcn "True") + , con0 (vcn "True") + , con0 (vcn "True") + ] + `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole) ) [ branch cA [("p", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole , branch cB [("r", Nothing), ("x", Nothing)] emptyHole @@ -1157,15 +1151,16 @@ unit_AddConField = @?= forgetMetadata ( create' $ case_ - ( con cA - `aPP` tEmptyHole - `aPP` tEmptyHole - `app` con (vcn "True") - `app` emptyHole - `app` con (vcn "True") - `app` con (vcn "True") + ( con + cA + [ con0 (vcn "True") + , emptyHole + , con0 (vcn "True") + , con0 (vcn "True") + ] + `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole) ) - [ branch cA [("p", Nothing), ("a25", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole + [ branch cA [("p", Nothing), ("a24", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole , branch cB [("r", Nothing), ("x", Nothing)] emptyHole ] ) @@ -1174,27 +1169,24 @@ unit_AddConField_partial_app :: Assertion unit_AddConField_partial_app = progActionTest ( defaultProgEditableTypeDefs $ do - x <- con cA `app` con (vcn "True") + x <- con cA [con0 (vcn "True")] sequence [ astDef "def" x <$> tEmptyHole ] ) [AddConField tT cA 2 $ TCon () (tcn "Int")] - $ expectSuccess - $ \_ prog' -> do - def <- findDef (gvn "def") prog' - forgetMetadata (astDefExpr def) - @?= forgetMetadata - ( create' $ - hole $ - con cA `app` con (vcn "True") - ) + $ expectError (@?= ConNotSaturated cA) +-- TODO (saturated constructors) when saturation is enforced, this test is a bit odd! +-- one may think that it should outright fail, since the program is not well-typed +-- why does it not???? +-- +-- TODO (saturated constructors) When developing ctors not store indices, I have simply removed indices in this test, but I suspect that there is something odd with the test since saturation was enforced unit_AddConField_partial_app_end :: Assertion unit_AddConField_partial_app_end = progActionTest ( defaultProgEditableTypeDefs $ do - x <- con cA `app` con (vcn "True") + x <- con cA [con0 (vcn "True")] sequence [ astDef "def" x <$> tEmptyHole ] @@ -1211,7 +1203,7 @@ unit_AddConField_partial_app_end = forgetMetadata (astDefExpr def) @?= forgetMetadata ( create' $ - con cA `app` con (vcn "True") `app` emptyHole + con cA [con0 (vcn "True"), emptyHole] ) unit_AddConField_case_ann :: Assertion @@ -1333,7 +1325,7 @@ unit_cross_module_actions = handleAndTC [ MoveToDef $ gvn "main" , SigAction [constructTCon (qualifyM "T")] - , BodyAction + , BodyAction $ [ ConstructApp , Move Child1 , ConstructVar (GlobalVarRef $ qualifyM "foo") @@ -1341,26 +1333,29 @@ unit_cross_module_actions = , Move Child2 , ConstructApp , Move Child1 - , constructCon (qualifyM "C") - , Move Parent - , Move Child2 - , constructCon cZero - , Move Parent - , Move Parent - , ConstructCase - , Move (Branch (qualifyM "C")) - , ConstructApp - , Move Child1 - , constructCon (qualifyM "C") - , Move Parent - , Move Child2 - , ConstructApp - , Move Child1 - , constructCon cSucc - , Move Parent - , Move Child2 - , ConstructVar (LocalVarRef "a27") ] + <> constructEtaAnnCon (qualifyM "C") [] [("n", tNat)] (qualifyM "T") + <> [ Move Parent + , Move Child2 + , constructSaturatedCon cZero + , Move Parent + , Move Parent + , ConstructCase + , Move (Branch (qualifyM "C")) + , ConstructApp + , Move Child1 + ] + <> constructEtaAnnCon (qualifyM "C") [] [("n", tNat)] (qualifyM "T") + <> [ Move Parent + , Move Child2 + , ConstructApp + , Move Child1 + ] + <> constructEtaAnnCon cSucc [] [("n", tNat)] tNat + <> [ Move Parent + , Move Child2 + , ConstructVar (LocalVarRef "a36") + ] ] handleAndTC [RenameDef (qualifyM "foo") "bar"] handleAndTC [RenameType (qualifyM "T") "R"] @@ -1395,7 +1390,7 @@ unit_cross_module_actions = , ConstructVar $ GlobalVarRef $ qualifyName (ModuleName ["AnotherModule"]) "bar" , Move Parent , Move Child2 - , constructCon cTrue + , constructSaturatedCon cTrue ] ] -- Copy-paste within the sig of bar to make bar :: Bool -> Bool diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs index b0d3de771..cd182eb1d 100644 --- a/primer/test/Tests/Eval.hs +++ b/primer/test/Tests/Eval.hs @@ -36,7 +36,7 @@ import Primer.Core ( Kind (KFun, KType), LocalName, Type, - Type' (TCon, TEmptyHole), + Type' (TCon, TEmptyHole, TVar), getID, unLocalName, unsafeMkGlobalName, @@ -115,7 +115,7 @@ runTryReduceType globals locals (ty, i) = do unit_tryReduce_no_redex :: Assertion unit_tryReduce_no_redex = do - r <- runTryReduce mempty mempty mempty (create (con cZero)) + r <- runTryReduce mempty mempty mempty (create (con0 cZero)) r @?= Left NotRedex unit_tryReduce_beta :: Assertion @@ -124,7 +124,7 @@ unit_tryReduce_beta = do create $ do x <- lvar "x" l <- lam "x" (pure x) - a <- con cZero + a <- con0 cZero app (pure l) (pure a) result <- runTryReduce mempty mempty mempty (input, maxid) case result of @@ -139,7 +139,7 @@ unit_tryReduce_beta_annotation = do t2 <- tcon' ["M"] "B" x <- lvar "x" l <- lam "x" (pure x) - a <- con' ["M"] "C" + a <- con0' ["M"] "C" i <- app (ann (pure l) (tfun (pure t1) (pure t2))) (pure a) r <- ann (let_ "x" (ann (pure a) (pure t1)) (pure x)) (pure t2) pure (l, x, a, i, r, t1, t2) @@ -165,7 +165,7 @@ unit_tryReduce_beta_annotation_hole = do create $ do x <- lvar "x" l <- lam "x" (pure x) - a <- con' ["M"] "C" + a <- con0' ["M"] "C" app (ann (pure l) tEmptyHole) (pure a) result <- runTryReduce tydefs mempty mempty (input, maxid) case result of @@ -176,7 +176,7 @@ unit_tryReduce_BETA :: Assertion unit_tryReduce_BETA = do let ((body, lambda, arg, input, expectedResult, k, ty), maxid) = create $ do - b <- aPP (con cNil) (tvar "x") + b <- con cNil [] l <- lAM "x" (pure b) a <- tcon tBool let k_ = KFun KType KType @@ -201,7 +201,7 @@ unit_tryReduce_BETA = do unit_tryReduce_local_term_var :: Assertion unit_tryReduce_local_term_var = do -- We assume we're inside a larger expression (e.g. a let) where the node that binds x has ID 5. - let ((expr, val), i) = create $ (,) <$> lvar "x" <*> con' ["M"] "C" + let ((expr, val), i) = create $ (,) <$> lvar "x" <*> con0' ["M"] "C" locals = singletonCxt @ID 5 $ LetBind "x" val result <- runTryReduce tydefs mempty locals (expr, i) case result of @@ -256,8 +256,8 @@ unit_tryReduce_global_var = do unit_tryReduce_let :: Assertion unit_tryReduce_let = do - let (expr, i) = create $ let_ "x" (con' ["M"] "C") (con' ["M"] "D") - expectedResult = create' $ con' ["M"] "D" + let (expr, i) = create $ let_ "x" (con0' ["M"] "C") (con0' ["M"] "D") + expectedResult = create' $ con0' ["M"] "D" result <- runTryReduce tydefs mempty mempty (expr, i) case result of Right (expr', LetRemoval detail) -> do @@ -293,8 +293,8 @@ unit_tryReduce_let_self_capture = do unit_tryReduce_lettype :: Assertion unit_tryReduce_lettype = do - let (expr, i) = create $ letType "x" (tcon' ["M"] "C") (con' ["M"] "D") - expectedResult = create' $ con' ["M"] "D" + let (expr, i) = create $ letType "x" (tcon' ["M"] "C") (con0' ["M"] "D") + expectedResult = create' $ con0' ["M"] "D" result <- runTryReduce tydefs mempty mempty (expr, i) case result of Right (expr', LetRemoval detail) -> do @@ -369,8 +369,8 @@ unit_tryReduce_tlet_self_capture = do unit_tryReduce_letrec :: Assertion unit_tryReduce_letrec = do - let (expr, i) = create $ letrec "x" (con' ["M"] "C") (tcon' ["M"] "T") (con' ["M"] "D") - expectedResult = create' $ con' ["M"] "D" + let (expr, i) = create $ letrec "x" (con0' ["M"] "C") (tcon' ["M"] "T") (con0' ["M"] "D") + expectedResult = create' $ con0' ["M"] "D" result <- runTryReduce tydefs mempty mempty (expr, i) case result of Right (expr', LetRemoval detail) -> do @@ -385,22 +385,10 @@ unit_tryReduce_letrec = do unit_tryReduce_case_1 :: Assertion unit_tryReduce_case_1 = do - let (expr, i) = create $ case_ (con' ["M"] "C") [branch' (["M"], "B") [("b", Nothing)] (con' ["M"] "D"), branch' (["M"], "C") [] (con' ["M"] "E")] - expectedResult = create' $ con' ["M"] "E" + let (expr, i) = create $ case_ (con0' ["M"] "C") [branch' (["M"], "B") [("b", Nothing)] (con0' ["M"] "D"), branch' (["M"], "C") [] (con0' ["M"] "E")] result <- runTryReduce tydefs mempty mempty (expr, i) case result of - Right (expr', CaseReduction detail) -> do - expr' ~= expectedResult - - detail.before ~= expr - detail.after ~= expectedResult - detail.targetID @?= 1 - detail.targetCtorID @?= 1 - detail.ctorName @?= vcn ["M"] "C" - detail.targetArgIDs @?= [] - detail.branchBindingIDs @?= [] - detail.branchRhsID @?= 4 - detail.letIDs @?= [] + Left NotRedex -> pure () _ -> assertFailure $ show result unit_tryReduce_case_2 :: Assertion @@ -408,9 +396,9 @@ unit_tryReduce_case_2 = do let (expr, i) = create $ case_ - (app (app (app (con' ["M"] "C") (lam "x" (lvar "x"))) (lvar "y")) (lvar "z")) - [ branch' (["M"], "B") [("b", Nothing)] (con' ["M"] "D") - , branch' (["M"], "C") [("c", Nothing), ("d", Nothing), ("e", Nothing)] (con' ["M"] "E") + (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") ] x = unsafeMkGlobalName (["M"], "X") y = unsafeMkGlobalName (["M"], "Y") @@ -437,7 +425,7 @@ unit_tryReduce_case_2 = do ( let_ "e" (lvar "z" `ann` tcon z) - (con' ["M"] "E") + (con0' ["M"] "E") ) ) result <- runTryReduce tydef mempty mempty (expr, i) @@ -448,12 +436,12 @@ unit_tryReduce_case_2 = do detail.before ~= expr detail.after ~= expectedResult detail.targetID @?= 1 - detail.targetCtorID @?= 4 + detail.targetCtorID @?= 2 detail.ctorName @?= vcn ["M"] "C" - detail.targetArgIDs @?= [5, 7, 8] - detail.branchBindingIDs @?= [11, 12, 13] - detail.branchRhsID @?= 14 - detail.letIDs @?= [21, 18, 15] + detail.targetArgIDs @?= [3, 5, 6] + detail.branchBindingIDs @?= [10, 11, 12] + detail.branchRhsID @?= 13 + detail.letIDs @?= [20, 17, 14] _ -> assertFailure $ show result unit_tryReduce_case_3 :: Assertion @@ -461,9 +449,9 @@ unit_tryReduce_case_3 = do let (expr, i) = create $ case_ - (app (aPP (con' ["M"] "C") (tcon' ["M"] "D")) (con' ["M"] "E")) - [ branch' (["M"], "B") [("b", Nothing)] (con' ["M"] "D") - , branch' (["M"], "C") [("c", Nothing)] (con' ["M"] "F") + (con' ["M"] "C" [con0' ["M"] "E"] `ann` (tcon' ["M"] "T" `tapp` tcon' ["M"] "D")) + [ branch' (["M"], "B") [("b", Nothing)] (con0' ["M"] "D") + , branch' (["M"], "C") [("c", Nothing)] (con0' ["M"] "F") ] tydef = Map.singleton (unsafeMkGlobalName (["M"], "T")) $ @@ -472,11 +460,11 @@ unit_tryReduce_case_3 = do { astTypeDefParameters = [("a", KType)] , astTypeDefConstructors = [ ValCon (unsafeMkGlobalName (["M"], "B")) [TEmptyHole ()] - , ValCon (unsafeMkGlobalName (["M"], "C")) [TEmptyHole ()] + , ValCon (unsafeMkGlobalName (["M"], "C")) [TVar () "a"] ] , astTypeDefNameHints = [] } - expectedResult = create' $ let_ "c" (con' ["M"] "E" `ann` tEmptyHole) (con' ["M"] "F") + expectedResult = create' $ let_ "c" (con0' ["M"] "E" `ann` tcon' ["M"] "D") (con0' ["M"] "F") result <- runTryReduce tydef mempty mempty (expr, i) case result of Right (expr', CaseReduction detail) -> do @@ -485,12 +473,12 @@ unit_tryReduce_case_3 = do detail.before ~= expr detail.after ~= expectedResult detail.targetID @?= 1 - detail.targetCtorID @?= 3 + detail.targetCtorID @?= 2 detail.ctorName @?= vcn ["M"] "C" - detail.targetArgIDs @?= [5] - detail.branchBindingIDs @?= [8] - detail.branchRhsID @?= 9 - detail.letIDs @?= [10] + detail.targetArgIDs @?= [3] + detail.branchBindingIDs @?= [9] + detail.branchRhsID @?= 10 + detail.letIDs @?= [11] _ -> assertFailure $ show result unit_tryReduce_case_name_clash :: Assertion @@ -498,7 +486,7 @@ unit_tryReduce_case_name_clash = do let (expr, i) = create $ case_ - (con' ["M"] "C" `app` emptyHole `app` lvar "x") + (con' ["M"] "C" [emptyHole, lvar "x"] `ann` tcon' ["M"] "T") [branch' (["M"], "C") [("x", Nothing), ("y", Nothing)] emptyHole] tydef = Map.singleton (unsafeMkGlobalName (["M"], "T")) $ @@ -511,7 +499,7 @@ unit_tryReduce_case_name_clash = do expectedResult = create' $ case_ - (con' ["M"] "C" `app` emptyHole `app` lvar "x") + (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) case result of @@ -531,7 +519,7 @@ unit_tryReduce_case_name_clash = do unit_tryReduce_case_scrutinee_not_redex :: Assertion unit_tryReduce_case_scrutinee_not_redex = do - let (expr, i) = create $ case_ (lvar "x") [branch' (["M"], "B") [] (con' ["M"] "D")] + let (expr, i) = create $ case_ (lvar "x") [branch' (["M"], "B") [] (con0' ["M"] "D")] result <- runTryReduce tydefs mempty mempty (expr, i) result @?= Left NotRedex @@ -543,7 +531,8 @@ unit_tryReduce_prim = do <$> pfun EqChar `app` char 'a' `app` char 'a' - <*> con cTrue + <*> con0 cTrue + `ann` tcon tBool result <- runTryReduce tydefs primDefs mempty (expr, i) case result of Right (expr', ApplyPrimFun detail) -> do @@ -590,8 +579,8 @@ unit_step_non_redex :: Assertion unit_step_non_redex = let ((idX, e1, e2), maxID) = create $ do x <- lvar "x" - e1' <- let_ "x" (con' ["M"] "C") $ lam "x" $ pure x - e2' <- let_ "x" (con' ["M"] "C" `app` lvar "x") $ pure x + e1' <- let_ "x" (lam "eta" $ con' ["M"] "C" [lvar "eta"]) $ lam "x" $ pure x + e2' <- let_ "x" (con' ["M"] "C" [lvar "x"]) $ pure x pure (getID x, e1', e2') in do assertBool "Should not be in 'redexes', as shadowed by a lambda" @@ -657,7 +646,7 @@ unit_findNodeByID_1 = do -- id 0 x_ <- lvar "x" -- id 1 - c_ <- con' ["M"] "C" + c_ <- con0' ["M"] "C" -- id 2 e <- let_ "x" (pure c_) (pure x_) pure (x_, c_, e) @@ -728,7 +717,7 @@ unit_findNodeByID_tlet = do unit_findNodeByID_scoping_1 :: Assertion unit_findNodeByID_scoping_1 = do - let expr = create' $ let_ "x" (con' ["M"] "C") $ lam "x" $ lvar "x" + let expr = create' $ let_ "x" (con0' ["M"] "C") $ lam "x" $ lvar "x" case findNodeByID 3 Syn expr of Just (Cxt locals, Left _) | Just (Nothing, _, _) <- Map.lookup "x" locals -> @@ -739,8 +728,8 @@ unit_findNodeByID_scoping_1 = do unit_findNodeByID_scoping_2 :: Assertion unit_findNodeByID_scoping_2 = do let (bind, expr) = create' $ do - b <- con' ["M"] "D" - e <- let_ "x" (con' ["M"] "C") $ let_ "x" (pure b) $ lvar "x" + b <- con0' ["M"] "D" + e <- let_ "x" (con0' ["M"] "C") $ let_ "x" (pure b) $ lvar "x" pure (b, e) case findNodeByID 4 Syn expr of Just (locals@(Cxt locals'), Left _) @@ -839,7 +828,7 @@ tydefs = c <> d } unit_redexes_con :: Assertion -unit_redexes_con = redexesOf (con' ["M"] "C") <@?=> mempty +unit_redexes_con = redexesOf (con0' ["M"] "C") <@?=> mempty (<@?=>) :: (HasCallStack, Eq a, Show a) => IO a -> a -> Assertion m <@?=> x = m >>= (@?= x) @@ -866,7 +855,7 @@ unit_redexes_lam_1 = ( lam "x" (lvar "x") `mkAnn` (tvar "a" `tfun` tvar "a") ) - (con' ["M"] "C") + (con0' ["M"] "C") in do redexesOf (e noAnn) <@?=> mempty redexesOf (e withAnn) <@?=> Set.singleton 0 @@ -880,7 +869,7 @@ unit_redexes_lam_2 = ( lam "x" (lvar "x") `mkAnn` (tvar "a" `tfun` tvar "a") ) - (con' ["M"] "C") + (con0' ["M"] "C") ) in do redexesOf (e noAnn) <@?=> mempty @@ -893,7 +882,7 @@ unit_redexes_lam_3 = "y" ( app (lam "x" (lvar "x") `mkAnn` (tvar "a" `tfun` tvar "a")) - (app (lam "z" (lvar "z") `mkAnn` (tvar "a" `tfun` tvar "a")) (con' ["M"] "C")) + (app (lam "z" (lvar "z") `mkAnn` (tvar "a" `tfun` tvar "a")) (con0' ["M"] "C")) ) in do redexesOf (e noAnn) <@?=> mempty @@ -906,7 +895,7 @@ unit_redexes_lam_4 = "y" ( app (lam "x" (lvar "x") `mkAnn` (tvar "a" `tfun` tvar "a")) - (app (lam "z" (lvar "z") `mkAnn` (tvar "a" `tfun` tvar "a")) (con' ["M"] "C")) + (app (lam "z" (lvar "z") `mkAnn` (tvar "a" `tfun` tvar "a")) (con0' ["M"] "C")) ) in do redexesOf (e noAnn) <@?=> mempty @@ -914,13 +903,13 @@ unit_redexes_lam_4 = unit_redexes_LAM_1 :: Assertion unit_redexes_LAM_1 = - redexesOf (lAM "a" (con' ["M"] "C")) <@?=> mempty + redexesOf (lAM "a" (con0' ["M"] "C")) <@?=> mempty unit_redexes_LAM_2 :: Assertion unit_redexes_LAM_2 = let e mkAnn = aPP - (lAM "a" (con' ["M"] "C") `mkAnn` tforall "a" KType (tcon' ["M"] "C")) + (lAM "a" (con0' ["M"] "C") `mkAnn` tforall "a" KType (tcon' ["M"] "C")) (tcon' ["M"] "A") in do redexesOf (e noAnn) <@?=> mempty @@ -932,7 +921,7 @@ unit_redexes_LAM_3 = lAM "a" ( aPP - (lAM "b" (con' ["M"] "X") `mkAnn` tforall "a" KType (tcon' ["M"] "C")) + (lAM "b" (con0' ["M"] "X") `mkAnn` tforall "a" KType (tcon' ["M"] "C")) (tcon' ["M"] "T") ) in do @@ -944,7 +933,7 @@ unit_redexes_LAM_4 = let e mkAnn = let_ "x" - (con' ["M"] "C") + (con0' ["M"] "C") ( lAM "a" ( aPP @@ -960,12 +949,12 @@ unit_redexes_LAM_4 = unit_redexes_let_1 :: Assertion unit_redexes_let_1 = - redexesOf (let_ "x" (con' ["M"] "C") (app (lvar "x") (lvar "y"))) + redexesOf (let_ "x" (con0' ["M"] "C") (app (lvar "x") (lvar "y"))) <@?=> Set.singleton 3 unit_redexes_let_2 :: Assertion unit_redexes_let_2 = - redexesOf (let_ "x" (con' ["M"] "C") (lam "x" (app (lvar "x") (lvar "y")))) + redexesOf (let_ "x" (con0' ["M"] "C") (lam "x" (app (lvar "x") (lvar "y")))) <@?=> Set.singleton 0 -- We cannot substitute one occurrence of a let-bound variable if it @@ -991,13 +980,13 @@ unit_redexes_lettype_capture = unit_redexes_letrec_1 :: Assertion unit_redexes_letrec_1 = - redexesOf (letrec "x" (app (con' ["M"] "C") (lvar "x")) (tcon' ["M"] "T") (app (lvar "x") (lvar "y"))) - <@?=> Set.fromList [3, 6] + redexesOf (letrec "x" (con' ["M"] "C" [lvar "x"]) (tcon' ["M"] "T") (app (lvar "x") (lvar "y"))) + <@?=> Set.fromList [2, 5] unit_redexes_letrec_2 :: Assertion unit_redexes_letrec_2 = - redexesOf (letrec "x" (app (con' ["M"] "C") (lvar "x")) (tcon' ["M"] "T") (lvar "y")) - <@?=> Set.fromList [0, 3] + redexesOf (letrec "x" (con' ["M"] "C" [lvar "x"]) (tcon' ["M"] "T") (lvar "y")) + <@?=> Set.fromList [0, 2] -- Test that our self-capture logic does not apply to letrec. unit_redexes_letrec_3 :: Assertion @@ -1014,11 +1003,11 @@ unit_redexes_letrec_app_1 = app ( letrec "e" - (con' ["M"] "C") + (con0' ["M"] "C") (tcon' ["M"] "T") (mkAnn (lam "x" (lvar "e")) (tcon' ["M"] "D" `tfun` tcon' ["M"] "T")) ) - (con' ["M"] "D") + (con0' ["M"] "D") in do redexesOf (e noAnn) <@?=> Set.fromList [5] redexesOf (e withAnn) <@?=> Set.fromList [6] @@ -1032,7 +1021,7 @@ unit_redexes_letrec_APP_1 = aPP ( letrec "e" - (con' ["M"] "C") + (con0' ["M"] "C") (tcon' ["M"] "T") (lAM "x" (lvar "e") `mkAnn` tforall "a" KType (tcon' ["M"] "T")) ) @@ -1043,15 +1032,15 @@ unit_redexes_letrec_APP_1 = unit_redexes_lettype_1 :: Assertion unit_redexes_lettype_1 = - redexesOf (letType "x" (tcon' ["M"] "T") (con' ["M"] "C")) <@?=> Set.fromList [0] + redexesOf (letType "x" (tcon' ["M"] "T") (con0' ["M"] "C")) <@?=> Set.fromList [0] unit_redexes_lettype_2 :: Assertion unit_redexes_lettype_2 = - redexesOf (letType "x" (tcon' ["M"] "T") (aPP (con' ["M"] "C") (tvar "x"))) <@?=> Set.fromList [4] + redexesOf (letType "x" (tcon' ["M"] "T") (con0' ["M"] "C" `ann` tvar "x")) <@?=> Set.fromList [4] unit_redexes_lettype_3 :: Assertion unit_redexes_lettype_3 = - redexesOf (letType "x" (tcon' ["M"] "T") (letrec "y" (con' ["M"] "C") (tvar "x") (lvar "y"))) <@?=> Set.fromList [4, 5] + redexesOf (letType "x" (tcon' ["M"] "T") (letrec "y" (con0' ["M"] "C") (tvar "x") (lvar "y"))) <@?=> Set.fromList [4, 5] -- We cannot substitute one occurrence of a let-bound variable if it -- would result in capture of a free variable in the bound term by the @@ -1081,39 +1070,40 @@ unit_redexes_tlet_4 = do -- NB we must not say node 5 (the occurrence of the variable) is a redex redexesOf (lAM "x" $ emptyHole `ann` tlet "x" (tvar "x") (tvar "x")) <@?=> Set.fromList [3] +-- Cannot reduce a case if there is no annotation (thus ill-typed) unit_redexes_case_1 :: Assertion unit_redexes_case_1 = - redexesOf (case_ (con' ["M"] "C") [branch' (["M"], "C") [] (con' ["M"] "D")]) - <@?=> Set.singleton 0 + redexesOf (case_ (con0' ["M"] "C") [branch' (["M"], "C") [] (con0' ["M"] "D")]) + <@?=> mempty -- Same as above, but the scrutinee has an annotation unit_redexes_case_1_annotated :: Assertion unit_redexes_case_1_annotated = - redexesOf (case_ (ann (con' ["M"] "C") (tcon' ["M"] "C")) [branch' (["M"], "C") [] (con' ["M"] "D")]) + redexesOf (case_ (ann (con0' ["M"] "C") (tcon' ["M"] "C")) [branch' (["M"], "C") [] (con0' ["M"] "D")]) <@?=> Set.singleton 0 unit_redexes_case_2 :: Assertion unit_redexes_case_2 = - redexesOf (case_ (lam "x" (lvar "x")) [branch' (["M"], "C") [] (con' ["M"] "D")]) + redexesOf (case_ (lam "x" (lvar "x") `ann` (tEmptyHole `tfun` tEmptyHole)) [branch' (["M"], "C") [] (con0' ["M"] "D")]) <@?=> mempty -- The case expression can be reduced, as can the variable x in the branch rhs. unit_redexes_case_3 :: Assertion unit_redexes_case_3 = - redexesOf (let_ "x" (con' ["M"] "C") (case_ (con' ["M"] "C") [branch' (["M"], "C") [] (lvar "x")])) - <@?=> Set.fromList [2, 4] + redexesOf (let_ "x" (con0' ["M"] "C") (case_ (con0' ["M"] "C" `ann` tcon' ["M"] "C") [branch' (["M"], "C") [] (lvar "x")])) + <@?=> Set.fromList [2, 6] -- The variable x in the rhs is bound to the branch pattern, so is no longer reducible. -- However this means the let is redundant, and can be reduced. unit_redexes_case_4 :: Assertion unit_redexes_case_4 = - redexesOf (let_ "x" (con' ["M"] "C") (case_ (con' ["M"] "C") [branch' (["M"], "C") [("x", Nothing)] (lvar "x")])) + redexesOf (let_ "x" (con0' ["M"] "C") (case_ (con0' ["M"] "C" `ann` tcon' ["M"] "C") [branch' (["M"], "C") [("x", Nothing)] (lvar "x")])) <@?=> Set.fromList [0, 2] -- If scrutinee of a case is a redex itself, we recognise that unit_redexes_case_5 :: Assertion unit_redexes_case_5 = - redexesOf (let_ "x" (con' ["M"] "C") (case_ (lvar "x") [])) <@?=> Set.fromList [3] + redexesOf (let_ "x" (con0' ["M"] "C") (case_ (lvar "x") [])) <@?=> Set.fromList [3] -- The body of a let has the same directionality as the let itself unit_redexes_let_upsilon :: Assertion @@ -1168,11 +1158,11 @@ unit_eval_modules_scrutinize_imported_type :: Assertion unit_eval_modules_scrutinize_imported_type = let test = do importModules [m] - foo <- case_ (con cTrue) [branch cTrue [] $ con cFalse, branch cFalse [] $ con cTrue] + foo <- case_ (con0 cTrue `ann` tcon tBool) [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] EvalResp{evalRespExpr = e} <- handleEvalRequest EvalReq{evalReqExpr = foo, evalReqRedex = getID foo} - expect <- con cFalse + expect <- con0 cFalse pure $ e ~= expect a = newEmptyApp in runAppTestM (appIdCounter a) a test <&> fst >>= \case diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index 174d1bf87..07547f563 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -37,7 +37,7 @@ import Primer.Builtins ( tNat, tPair, ) -import Primer.Builtins.DSL (bool_, list_, nat) +import Primer.Builtins.DSL (boolAnn, list_, nat) import Primer.Core import Primer.Core.DSL import Primer.Core.Utils ( @@ -58,7 +58,6 @@ import Primer.Module ( builtinModule, builtinTypes, moduleDefsQualified, - moduleTypesQualified, primitiveModule, ) import Primer.Primitives ( @@ -120,7 +119,7 @@ import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=)) import Tests.Action.Prog (runAppTestM) import Tests.Eval.Utils (genDirTm, testModules, (~=)) import Tests.Gen.Core.Typed (checkTest) -import Tests.Typecheck (expectTypedWithPrims, runTypecheckTestM, runTypecheckTestMWithPrims) +import Tests.Typecheck (runTypecheckTestM, runTypecheckTestMWithPrims) unit_1 :: Assertion unit_1 = @@ -152,9 +151,9 @@ unit_3 = unit_4 :: Assertion unit_4 = let ((expr, expected), maxID) = create $ do - e <- let_ "a" (lvar "b") $ con' ["M"] "C" `app` lvar "a" `app` lam "a" (lvar "a") `app` lam "b" (con' ["M"] "D" `app` lvar "a" `app` lvar "b") - let b' = "a29" -- NB: fragile name a29 - expect <- con' ["M"] "C" `app` lvar "b" `app` lam "a" (lvar "a") `app` lam b' (con' ["M"] "D" `app` lvar "b" `app` lvar b') + e <- let_ "a" (lvar "b") $ con' ["M"] "C" [lvar "a", lam "a" (lvar "a"), lam "b" (con' ["M"] "D" [lvar "a", lvar "b"])] + let b' = "a19" -- NB: fragile name + expect <- con' ["M"] "C" [lvar "b", lam "a" (lvar "a"), lam b' (con' ["M"] "D" [lvar "b", lvar b'])] pure (e, expect) in do s <- evalFullTest maxID mempty mempty 7 Syn expr @@ -179,7 +178,7 @@ unit_5 = unit_6 :: Assertion unit_6 = let ((e, expt), maxID) = create $ do - tr <- con cTrue + tr <- con0 cTrue an <- ann (pure tr) (tcon tBool) pure (an, tr) in do @@ -225,10 +224,10 @@ unit_9 = (mapName, mapDef) <- Examples.map' modName (evenName, evenDef) <- Examples.even modName (oddName, oddDef) <- Examples.odd modName - let lst = list_ tNat $ take n $ iterate (con cSucc `app`) (con cZero) + let lst = list_ $ take n $ iterate (con1 cSucc) (con0 cZero) expr <- gvar mapName `aPP` tcon tNat `aPP` tcon tBool `app` gvar evenName `app` lst let globs = [(mapName, mapDef), (evenName, evenDef), (oddName, oddDef)] - expect <- list_ tBool (take n $ cycle [con cTrue, con cFalse]) `ann` (tcon tList `tapp` tcon tBool) + expect <- list_ (take n $ cycle [con0 cTrue, con0 cFalse]) `ann` (tcon tList `tapp` tcon tBool) pure (globs, expr, expect) in do evalFullTest maxID builtinTypes (M.fromList globals) 500 Syn e >>= \case @@ -237,32 +236,31 @@ unit_9 = s <- evalFullTest maxID builtinTypes (M.fromList globals) 1000 Syn e s <~==> Right expected --- Check that we handle constructors-are-synthesisable well --- NB: annotated scrutinees are common, e.g. (λx.case x of ... : S -> T) s --- but plain constructors should be supported also, as we let users write --- construtors in synthesisable position +-- A case redex must have an scrutinee which is an annotated constructor. +-- Plain constructors are not well-typed here, for bidirectionality reasons, +-- although they just fail to reduce rather than the evaluator throwing a type error. unit_10 :: Assertion unit_10 = let ((s, t, expected), maxID) = create $ do annCase <- case_ - (con cZero `ann` tcon tNat) - [ branch cZero [] $ con cTrue - , branch cSucc [("n", Nothing)] $ con cFalse + (con0 cZero `ann` tcon tNat) + [ branch cZero [] $ con0 cTrue + , branch cSucc [("n", Nothing)] $ con0 cFalse ] noannCase <- case_ - (con cZero) - [ branch cZero [] $ con cTrue - , branch cSucc [("n", Nothing)] $ con cFalse + (con0 cZero) + [ branch cZero [] $ con0 cTrue + , branch cSucc [("n", Nothing)] $ con0 cFalse ] - expect <- con cTrue + expect <- con0 cTrue pure (annCase, noannCase, expect) in do s' <- evalFullTest maxID builtinTypes mempty 2 Syn s s' <~==> Right expected - t' <- evalFullTest maxID builtinTypes mempty 2 Syn t - t' <~==> Right expected + t' <- evalFullTest maxID builtinTypes mempty 1 Syn t + t' <~==> Right t -- This example shows that when we are under even a 'let' all we can do is -- substitute, otherwise we may go down a rabbit hole! @@ -274,13 +272,13 @@ unit_11 = (oddName, oddDef) <- Examples.odd modName let ty = tcon tNat `tfun` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat) let expr1 = - let_ "x" (con cZero) $ - lam "n" (con cMakePair `aPP` tcon tBool `aPP` tcon tNat `app` (gvar evenName `app` lvar "n") `app` lvar "x") + let_ "x" (con0 cZero) $ + lam "n" (con cMakePair [gvar evenName `app` lvar "n", lvar "x"]) `ann` ty - expr <- expr1 `app` con cZero + expr <- expr1 `app` con0 cZero let globs = [(evenName, evenDef), (oddName, oddDef)] expect <- - (con cMakePair `aPP` tcon tBool `aPP` tcon tNat `app` con cTrue `app` con cZero) + con cMakePair [con0 cTrue, con0 cZero] `ann` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat) pure (globs, expr, expect) in do @@ -301,11 +299,11 @@ unit_12 = lam "x" $ case_ (lvar "x") - [ branch cZero [] $ con cTrue + [ branch cZero [] $ con0 cTrue , branch cSucc [("i", Nothing)] $ lvar "f" `app` lvar "i" ] - expr <- let_ "n" (con cZero) $ letrec "f" f (tcon tNat `tfun` tcon tBool) $ lvar "f" `app` lvar "n" - expect <- con cTrue `ann` tcon tBool + expr <- let_ "n" (con0 cZero) $ letrec "f" f (tcon tNat `tfun` tcon tBool) $ lvar "f" `app` lvar "n" + expect <- con0 cTrue `ann` tcon tBool pure (expr, expect) in do s <- evalFullTest maxID builtinTypes mempty 15 Syn e @@ -314,8 +312,8 @@ unit_12 = unit_13 :: Assertion unit_13 = let ((e, expected), maxID) = create $ do - expr <- (lam "x" (con' ["M"] "C" `app` lvar "x" `app` let_ "x" (con cTrue) (lvar "x") `app` lvar "x") `ann` (tcon tNat `tfun` tcon tBool)) `app` con cZero - expect <- (con' ["M"] "C" `app` con cZero `app` con cTrue `app` con cZero) `ann` tcon tBool + expr <- (lam "x" (con' ["M"] "C" [lvar "x", let_ "x" (con0 cTrue) (lvar "x"), lvar "x"]) `ann` (tcon tNat `tfun` tcon tBool)) `app` con0 cZero + expect <- con' ["M"] "C" [con0 cZero, con0 cTrue, con0 cZero] `ann` tcon tBool pure (expr, expect) in do s <- evalFullTest maxID builtinTypes mempty 15 Syn e @@ -324,8 +322,8 @@ unit_13 = unit_14 :: Assertion unit_14 = let ((e, expected), maxID) = create $ do - expr <- (lam "x" (lam "x" $ lvar "x") `ann` (tcon tBool `tfun` (tcon tNat `tfun` tcon tNat))) `app` con cTrue `app` con cZero - expect <- con cZero `ann` tcon tNat + expr <- (lam "x" (lam "x" $ lvar "x") `ann` (tcon tBool `tfun` (tcon tNat `tfun` tcon tNat))) `app` con0 cTrue `app` con0 cZero + expect <- con0 cZero `ann` tcon tNat pure (expr, expect) in do s <- evalFullTest maxID builtinTypes mempty 15 Syn e @@ -344,9 +342,9 @@ unit_15 :: Assertion unit_15 = let ((expr, steps, expected), maxID) = create $ do let l = let_ "x" (lvar "y") - let c a b = con' ["M"] "C" `app` lvar a `app` lvar b + let c a b = con' ["M"] "C" [lvar a, lvar b] e0 <- l $ lam "y" $ c "x" "y" - let y' = "a50" -- NB: fragile name "a50" + let y' = "a38" e1 <- l $ lam y' $ let_ "y" (lvar y') $ c "x" "y" e2 <- l $ lam y' $ let_ "y" (lvar y') $ c "x" y' e3 <- l $ lam y' $ c "x" y' @@ -502,19 +500,19 @@ unit_type_preservation_case_regression_tm = e <- lam "x" $ case_ - (con cMakePair `aPP` tcon tNat `aPP` tcon tBool `app` emptyHole `app` lvar "x") + (con cMakePair [emptyHole, lvar "x"] `ann` ((tcon tPair `tapp` tcon tNat) `tapp` tcon tBool)) [branch cMakePair [("x", Nothing), ("y", Nothing)] emptyHole] + let x' = "a42" -- NB: fragile name expect1 <- lam "x" $ case_ - (con cMakePair `aPP` tcon tNat `aPP` tcon tBool `app` emptyHole `app` lvar "x") - -- NB: fragile name a42 - [branch cMakePair [("a42", Nothing), ("y", Nothing)] $ let_ "x" (lvar "a42") emptyHole] + (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_ "a42" (emptyHole `ann` tcon tNat) $ + let_ x' (emptyHole `ann` tcon tNat) $ let_ "y" (lvar "x" `ann` tcon tBool) $ - let_ "x" (lvar "a42") emptyHole + let_ "x" (lvar x') emptyHole pure (e, expect1, expect2) in do s1 <- evalFullTest maxID builtinTypes mempty 1 Chk expr @@ -536,23 +534,23 @@ unit_type_preservation_case_regression_ty = e <- lAM "x" $ case_ - ( (con cMakePair `aPP` tEmptyHole `aPP` tvar "x" `app` emptyHole `app` emptyHole) + ( con cMakePair [emptyHole, emptyHole] `ann` (tcon tPair `tapp` tEmptyHole `tapp` tvar "x") ) [branch cMakePair [("x", Nothing), ("y", Nothing)] emptyHole] + let x' = "a42" -- NB fragile name expect1 <- lAM "x" $ case_ - ( (con cMakePair `aPP` tEmptyHole `aPP` tvar "x" `app` emptyHole `app` emptyHole) + ( con cMakePair [emptyHole, emptyHole] `ann` (tcon tPair `tapp` tEmptyHole `tapp` tvar "x") ) - -- NB fragile name a54 - [branch cMakePair [("a54", Nothing), ("y", Nothing)] $ let_ "x" (lvar "a54") emptyHole] + [branch cMakePair [(x', Nothing), ("y", Nothing)] $ let_ "x" (lvar x') emptyHole] expect2 <- lAM "x" $ - let_ "a54" (emptyHole `ann` tEmptyHole) $ + let_ x' (emptyHole `ann` tEmptyHole) $ let_ "y" (emptyHole `ann` tvar "x") $ - let_ "x" (lvar "a54") emptyHole + let_ "x" (lvar x') emptyHole pure (e, expect1, expect2) in do s1 <- evalFullTest maxID builtinTypes mempty 1 Chk expr @@ -560,33 +558,6 @@ unit_type_preservation_case_regression_ty = s2 <- evalFullTest maxID builtinTypes mempty 2 Chk expr s2 <~==> Left (TimedOut expected2) --- Consider --- case Just @? False : Maybe Nat of Just x -> Succ x ; Nothing -> ? --- In the past we would reduce this to --- let x = False : Nat in Succ x --- which is ill-typed (we ignored the hole in the type-application, --- which acts as a type-changing cast). --- We simply test that the one-step reduction of this expression is well-typed, --- without mandating what the result should be. -unit_type_preservation_case_hole_regression :: Assertion -unit_type_preservation_case_hole_regression = evalTestM 0 $ do - t <- - case_ - ((con cJust `aPP` tEmptyHole `app` con cFalse) `ann` (tcon tMaybe `tapp` tcon tNat)) - [ branch cNothing [] emptyHole - , branch cJust [("x", Nothing)] $ con cSucc `app` lvar "x" - ] - let tds = foldMap' moduleTypesQualified testModules - let globs = foldMap' moduleDefsQualified testModules - ((_steps, s), logs) <- runPureLogT $ evalFullStepCount tds globs 1 Syn t - let s' = case s of - Left (TimedOut e) -> e - Right e -> e - pure $ do - expectTypedWithPrims $ pure t `ann` tEmptyHole - assertNoSevereLogs @EvalLog logs - expectTypedWithPrims $ pure s' `ann` tEmptyHole - -- Previously EvalFull reducing a BETA expression could result in variable -- capture. We would reduce (Λa.t : ∀b.T) S to -- let b = S in (let a = S in t) : T @@ -874,14 +845,14 @@ unit_prim_isSpace_1 = unaryPrimTest IsSpace (char '\n') - (bool_ True) + (boolAnn True) unit_prim_isSpace_2 :: Assertion unit_prim_isSpace_2 = unaryPrimTest IsSpace (char 'a') - (bool_ False) + (boolAnn False) tasty_prim_hex_nat :: Property tasty_prim_hex_nat = withTests 20 . property $ do @@ -899,7 +870,7 @@ tasty_prim_hex_nat = withTests 20 . property $ do [ branch cNothing [] - (con cNothing) + (con0 cNothing) , branch cJust [("x", Nothing)] @@ -907,14 +878,14 @@ tasty_prim_hex_nat = withTests 20 . property $ do `app` lvar "x" ) ] - <*> (con cJust `aPP` tcon tNat) - `app` ne + <*> con1 cJust ne + `ann` (tcon tMaybe `tapp` tcon tNat) else (,) <$> pfun NatToHex `app` ne - <*> con cNothing - `aPP` tcon tChar + <*> con0 cNothing + `ann` (tcon tMaybe `tapp` tcon tChar) s <- evalFullTasty maxID builtinTypes primDefs 7 Syn e over evalResultExpr zeroIDs s === Right (zeroIDs r) @@ -924,7 +895,7 @@ unit_prim_char_eq_1 = EqChar (char 'a') (char 'a') - (con cTrue) + (con0 cTrue `ann` tcon tBool) unit_prim_char_eq_2 :: Assertion unit_prim_char_eq_2 = @@ -932,7 +903,7 @@ unit_prim_char_eq_2 = EqChar (char 'a') (char 'A') - (con cFalse) + (con0 cFalse `ann` tcon tBool) unit_prim_char_partial :: Assertion unit_prim_char_partial = @@ -992,7 +963,7 @@ unit_prim_int_quotient = IntQuotient (int 7) (int 3) - (con cJust `aPP` tcon tInt `app` int 2) + (conSat cJust [int 2] `ann` (tcon tMaybe `tapp` tcon tInt)) unit_prim_int_quotient_negative :: Assertion unit_prim_int_quotient_negative = @@ -1000,7 +971,7 @@ unit_prim_int_quotient_negative = IntQuotient (int (-7)) (int 3) - (con cJust `aPP` tcon tInt `app` int (-3)) + (conSat cJust [int (-3)] `ann` (tcon tMaybe `tapp` tcon tInt)) unit_prim_int_quotient_zero :: Assertion unit_prim_int_quotient_zero = @@ -1008,7 +979,7 @@ unit_prim_int_quotient_zero = IntQuotient (int (-7)) (int 0) - (con cNothing `aPP` tcon tInt) + (conSat cNothing [] `ann` (tcon tMaybe `tapp` tcon tInt)) unit_prim_int_remainder :: Assertion unit_prim_int_remainder = @@ -1016,7 +987,7 @@ unit_prim_int_remainder = IntRemainder (int 7) (int 3) - (con cJust `aPP` tcon tInt `app` int 1) + (conSat cJust [int 1] `ann` (tcon tMaybe `tapp` tcon tInt)) unit_prim_int_remainder_negative_1 :: Assertion unit_prim_int_remainder_negative_1 = @@ -1024,7 +995,7 @@ unit_prim_int_remainder_negative_1 = IntRemainder (int (-7)) (int (-3)) - (con cJust `aPP` tcon tInt `app` int (-1)) + (conSat cJust [int (-1)] `ann` (tcon tMaybe `tapp` tcon tInt)) unit_prim_int_remainder_negative_2 :: Assertion unit_prim_int_remainder_negative_2 = @@ -1032,7 +1003,7 @@ unit_prim_int_remainder_negative_2 = IntRemainder (int (-7)) (int 3) - (con cJust `aPP` tcon tInt `app` int 2) + (conSat cJust [int 2] `ann` (tcon tMaybe `tapp` tcon tInt)) unit_prim_int_remainder_negative_3 :: Assertion unit_prim_int_remainder_negative_3 = @@ -1040,7 +1011,7 @@ unit_prim_int_remainder_negative_3 = IntRemainder (int 7) (int (-3)) - (con cJust `aPP` tcon tInt `app` int (-2)) + (conSat cJust [int (-2)] `ann` (tcon tMaybe `tapp` tcon tInt)) unit_prim_int_remainder_zero :: Assertion unit_prim_int_remainder_zero = @@ -1048,7 +1019,7 @@ unit_prim_int_remainder_zero = IntRemainder (int 7) (int 0) - (con cNothing `aPP` tcon tInt) + (conSat cNothing [] `ann` (tcon tMaybe `tapp` tcon tInt)) unit_prim_int_quot :: Assertion unit_prim_int_quot = @@ -1120,7 +1091,7 @@ unit_prim_int_eq_1 = IntEq (int 2) (int 2) - (bool_ True) + (boolAnn True) unit_prim_int_eq_2 :: Assertion unit_prim_int_eq_2 = @@ -1128,7 +1099,7 @@ unit_prim_int_eq_2 = IntEq (int 2) (int 1) - (bool_ False) + (boolAnn False) unit_prim_int_neq_1 :: Assertion unit_prim_int_neq_1 = @@ -1136,7 +1107,7 @@ unit_prim_int_neq_1 = IntNeq (int 2) (int 2) - (bool_ False) + (boolAnn False) unit_prim_int_neq_2 :: Assertion unit_prim_int_neq_2 = @@ -1144,7 +1115,7 @@ unit_prim_int_neq_2 = IntNeq (int 2) (int 1) - (bool_ True) + (boolAnn True) unit_prim_int_less_than_1 :: Assertion unit_prim_int_less_than_1 = @@ -1152,7 +1123,7 @@ unit_prim_int_less_than_1 = IntLT (int 1) (int 2) - (bool_ True) + (boolAnn True) unit_prim_int_less_than_2 :: Assertion unit_prim_int_less_than_2 = @@ -1160,7 +1131,7 @@ unit_prim_int_less_than_2 = IntLT (int 1) (int 1) - (bool_ False) + (boolAnn False) unit_prim_int_less_than_or_equal_1 :: Assertion unit_prim_int_less_than_or_equal_1 = @@ -1168,7 +1139,7 @@ unit_prim_int_less_than_or_equal_1 = IntLTE (int 1) (int 2) - (bool_ True) + (boolAnn True) unit_prim_int_less_than_or_equal_2 :: Assertion unit_prim_int_less_than_or_equal_2 = @@ -1176,7 +1147,7 @@ unit_prim_int_less_than_or_equal_2 = IntLTE (int 1) (int 1) - (bool_ True) + (boolAnn True) unit_prim_int_less_than_or_equal_3 :: Assertion unit_prim_int_less_than_or_equal_3 = @@ -1184,7 +1155,7 @@ unit_prim_int_less_than_or_equal_3 = IntLTE (int 2) (int 1) - (bool_ False) + (boolAnn False) unit_prim_int_greater_than_1 :: Assertion unit_prim_int_greater_than_1 = @@ -1192,7 +1163,7 @@ unit_prim_int_greater_than_1 = IntGT (int 2) (int 1) - (bool_ True) + (boolAnn True) unit_prim_int_greater_than_2 :: Assertion unit_prim_int_greater_than_2 = @@ -1200,7 +1171,7 @@ unit_prim_int_greater_than_2 = IntGT (int 1) (int 1) - (bool_ False) + (boolAnn False) unit_prim_int_greater_than_or_equal_1 :: Assertion unit_prim_int_greater_than_or_equal_1 = @@ -1208,7 +1179,7 @@ unit_prim_int_greater_than_or_equal_1 = IntGTE (int 1) (int 2) - (bool_ False) + (boolAnn False) unit_prim_int_greater_than_or_equal_2 :: Assertion unit_prim_int_greater_than_or_equal_2 = @@ -1216,7 +1187,7 @@ unit_prim_int_greater_than_or_equal_2 = IntGTE (int 1) (int 1) - (bool_ True) + (boolAnn True) unit_prim_int_greater_than_or_equal_3 :: Assertion unit_prim_int_greater_than_or_equal_3 = @@ -1224,21 +1195,21 @@ unit_prim_int_greater_than_or_equal_3 = IntGTE (int 2) (int 1) - (bool_ True) + (boolAnn True) unit_prim_int_toNat :: Assertion unit_prim_int_toNat = unaryPrimTest IntToNat (int 0) - (con cJust `aPP` tcon tNat `app` nat 0) + (conSat cJust [nat 0] `ann` (tcon tMaybe `tapp` tcon tNat)) unit_prim_int_toNat_negative :: Assertion unit_prim_int_toNat_negative = unaryPrimTest IntToNat (int (-1)) - (con cNothing `aPP` tcon tNat) + (conSat cNothing [] `ann` (tcon tMaybe `tapp` tcon tNat)) unit_prim_int_fromNat :: Assertion unit_prim_int_fromNat = @@ -1273,13 +1244,11 @@ unit_prim_partial_map = `aPP` tcon tChar `app` pfun ToUpper `app` list_ - tChar [ char 'a' , char 'b' , char 'c' ] <*> list_ - tChar [ char 'A' , char 'B' , char 'C' @@ -1317,11 +1286,11 @@ unit_eval_full_modules_scrutinize_imported_type :: Assertion unit_eval_full_modules_scrutinize_imported_type = let test = do importModules [m] - foo <- case_ (con cTrue) [branch cTrue [] $ con cFalse, branch cFalse [] $ con cTrue] + foo <- case_ (con0 cTrue `ann` tcon tBool) [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] resp <- handleEvalFullRequest EvalFullReq{evalFullReqExpr = foo, evalFullCxtDir = Chk, evalFullMaxSteps = 2} - expect <- con cFalse + expect <- con0 cFalse pure $ case resp of EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" EvalFullRespNormal e -> e ~= expect diff --git a/primer/test/Tests/FreeVars.hs b/primer/test/Tests/FreeVars.hs index 1e6601dec..291768876 100644 --- a/primer/test/Tests/FreeVars.hs +++ b/primer/test/Tests/FreeVars.hs @@ -23,7 +23,7 @@ unit_2 = ( lam "x" $ case_ (lvar "x") - [ branch cZero [] $ con cTrue + [ branch cZero [] $ con0 cTrue , branch cSucc [("n", Nothing)] (app (lvar "f") (lvar "n")) ] ) diff --git a/primer/test/Tests/Prelude/Integer.hs b/primer/test/Tests/Prelude/Integer.hs index 6a5808319..bdffa9c0d 100644 --- a/primer/test/Tests/Prelude/Integer.hs +++ b/primer/test/Tests/Prelude/Integer.hs @@ -14,9 +14,6 @@ import Primer.Core.DSL ( int, ) import Primer.Prelude.Integer qualified as P -import Primer.Primitives ( - tInt, - ) import Tasty (Property, property, withTests) import Tests.Prelude.Utils (functionOutput, (<===>)) @@ -69,9 +66,9 @@ tasty_odd_prop = property $ do tasty_sum_prop :: Property tasty_sum_prop = property $ do ns <- forAll $ G.list (Range.linear 0 10) (G.integral_ (Range.constant (-10) 10)) - functionOutput P.sum [list_ tInt $ map int ns] 2000 <===> Right (create' $ int $ sum ns) + functionOutput P.sum [list_ $ map int ns] 2000 <===> Right (create' $ int $ sum ns) tasty_product_prop :: Property tasty_product_prop = property $ do ns <- forAll $ G.list (Range.linear 0 10) (G.integral_ (Range.constant 1 10)) - functionOutput P.product [list_ tInt $ map int ns] 2000 <===> Right (create' $ int $ product ns) + functionOutput P.product [list_ $ map int ns] 2000 <===> Right (create' $ int $ product ns) diff --git a/primer/test/Tests/Prelude/Polymorphism.hs b/primer/test/Tests/Prelude/Polymorphism.hs index 4e62ade18..063a48581 100644 --- a/primer/test/Tests/Prelude/Polymorphism.hs +++ b/primer/test/Tests/Prelude/Polymorphism.hs @@ -16,10 +16,9 @@ import Primer.Builtins.DSL ( list_, ) import Primer.Core.DSL ( - aPP, apps, char, - con, + conSat, create', gvar, int, @@ -50,7 +49,7 @@ tasty_id_prop = property $ do ns <- forAll $ G.list (Range.constant 0 10) (G.integral_ (Range.constant (-10) 10)) functionOutput' P.id [Right $ tcon tInt, Left $ int n] 20 <===> Right (create' $ int n) -- Integer Test functionOutput' P.id [Right $ tcon tBool, Left $ bool_ b] 20 <===> Right (create' $ bool_ b) -- Bool Test - functionOutput' P.id [Right $ tcon tList `tapp` tcon tInt, Left $ list_ tInt $ map int ns] 20 <===> Right (create' $ list_ tInt $ map int ns) -- List of Int Test + functionOutput' P.id [Right $ tcon tList `tapp` tcon tInt, Left $ list_ $ map int ns] 20 <===> Right (create' $ list_ $ map int ns) -- List of Int Test tasty_const_prop :: Property tasty_const_prop = property $ do @@ -78,12 +77,12 @@ tasty_const_prop = property $ do functionOutput' -- List of Int Test P.const [ Right $ tcon tList `tapp` tcon tInt - , Left $ list_ tInt $ map int ns + , Left $ list_ $ map int ns , Right $ tcon tInt , Left $ int n ] 20 - <===> Right (create' $ list_ tInt $ map int ns) + <===> Right (create' $ list_ $ map int ns) tasty_map_prop :: Property tasty_map_prop = property $ do @@ -92,26 +91,26 @@ tasty_map_prop = property $ do let addOne = lam "x" $ apps (pfun IntAdd) [lvar "x", int 1] in functionOutput' -- Mapping over integers (+1) P.map - [Right $ tcon tInt, Right $ tcon tInt, Left addOne, Left $ list_ tInt $ map int ns] + [Right $ tcon tInt, Right $ tcon tInt, Left addOne, Left $ list_ $ map int ns] 1000 - <===> Right (create' $ list_ tInt $ map (int . (+ 1)) ns) + <===> Right (create' $ list_ $ map (int . (+ 1)) ns) functionOutput' -- Mapping over bools (not) P.map - [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.not), Left $ list_ tBool $ map bool_ bs] + [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.not), Left $ list_ $ map bool_ bs] 1000 - <===> Right (create' $ list_ tBool $ map (bool_ . not) bs) + <===> Right (create' $ list_ $ map (bool_ . not) bs) -- Right fold over a list of characters with @cons@. tasty_foldr_list_char :: Property tasty_foldr_list_char = property $ do as <- forAll $ G.list (Range.linear 0 10) G.unicode as' <- forAll $ G.list (Range.linear 0 10) G.unicode - let cons = lam "x" $ lam "xs" $ apps (con cCons `aPP` tcon tChar) [lvar "x", lvar "xs"] + let cons = lam "x" $ lam "xs" $ conSat cCons [lvar "x", lvar "xs"] in functionOutput' P.foldr - [Right $ listOf (tcon tChar), Right $ listOf (tcon tChar), Left cons, Left $ list_ tChar $ map char as, Left $ list_ tChar $ map char as'] + [Right $ listOf (tcon tChar), Right $ listOf (tcon tChar), Left cons, Left $ list_ $ map char as, Left $ list_ $ map char as'] 1000 - <===> Right (create' $ list_ tChar $ map char (foldr (:) as as')) + <===> Right (create' $ list_ $ map char (foldr (:) as as')) {- HLINT ignore tasty_foldr_bool "Use and" -} -- Right fold over a list of bools with logical @and@. @@ -120,7 +119,7 @@ tasty_foldr_bool = property $ do bs <- forAll $ G.list (Range.linear 0 10) G.bool_ functionOutput' P.foldr - [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.and), Left $ bool_ True, Left $ list_ tBool $ map bool_ bs] + [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.and), Left $ bool_ True, Left $ list_ $ map bool_ bs] 1000 <===> Right (create' $ bool_ (foldr (&&) True bs)) @@ -131,7 +130,7 @@ tasty_foldr_right_assoc = property $ do let subtract' = lam "x" $ lam "y" $ apps (pfun IntMinus) [lvar "x", lvar "y"] functionOutput' P.foldr - [Right $ tcon tInt, Right $ tcon tInt, Left subtract', Left $ int 0, Left $ list_ tInt $ map int ns] + [Right $ tcon tInt, Right $ tcon tInt, Left subtract', Left $ int 0, Left $ list_ $ map int ns] 1000 <===> Right (create' $ int (foldr (-) 0 ns)) @@ -143,6 +142,6 @@ unit_foldr_short_circuit = in do functionOutput' P.foldr - [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.and), Left $ bool_ True, Left $ list_ tBool $ map bool_ bs] + [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.and), Left $ bool_ True, Left $ list_ $ map bool_ bs] 100 <~==> Right (create' $ bool_ False) diff --git a/primer/test/Tests/Questions.hs b/primer/test/Tests/Questions.hs index 709850762..8f71f7643 100644 --- a/primer/test/Tests/Questions.hs +++ b/primer/test/Tests/Questions.hs @@ -179,8 +179,8 @@ unit_variablesInScope_lambda = do -- Given a let, its bound variable is in scope in the body but not the bound expression unit_variablesInScope_let :: Assertion unit_variablesInScope_let = do - let oneLet = let_ "x" (con cTrue) emptyHole - twoLet = let_ "x" (con cTrue) (let_ "y" (con cZero) emptyHole) + let oneLet = let_ "x" (con0 cTrue `ann` tcon tBool) emptyHole + twoLet = let_ "x" (con0 cTrue `ann` tcon tBool) (let_ "y" (con0 cZero `ann` tcon tNat) emptyHole) hasVariables oneLet pure mempty hasVariables oneLet down mempty hasVariables oneLet (down >=> right) [("x", TCon () tBool)] @@ -196,7 +196,7 @@ unit_variablesInScope_let = do -- Given a letrec, its bound variable is in scope in both the body and the bound expression unit_variablesInScope_letrec :: Assertion unit_variablesInScope_letrec = do - let expr = letrec "x" (con cTrue) (tcon tBool) emptyHole + let expr = letrec "x" (con0 cTrue) (tcon tBool) emptyHole hasVariables expr pure [] hasVariables expr down [("x", TCon () tBool)] hasVariables expr (down >=> right) [("x", TCon () tBool)] @@ -209,7 +209,7 @@ unit_variablesInScope_letrec = do -- LHS. unit_variablesInScope_case :: Assertion unit_variablesInScope_case = do - let expr = ann (case_ (con cZero) [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole]) (tcon tNat) + let expr = ann (case_ (con0 cZero `ann` tcon tNat) [branch cZero [] emptyHole, branch cSucc [("n", Nothing)] emptyHole]) (tcon tNat) hasVariables expr pure [] hasVariables expr down [] hasVariables expr (down >=> down) [] @@ -228,7 +228,7 @@ unit_variablesInScope_type = do unit_variablesInScope_shadowed :: Assertion unit_variablesInScope_shadowed = do let ty = tforall "a" (KFun KType KType) $ tforall "b" KType $ tcon tNat `tfun` tforall "a" KType (tcon tBool `tfun` (tcon tList `tapp` tvar "b")) - expr' = lAM "c" $ lAM "d" $ lam "c" $ lAM "c" $ lam "c" $ con cNil `aPP` tvar "d" + expr' = lAM "c" $ lAM "d" $ lam "c" $ lAM "c" $ lam "c" $ con0 cNil expr = ann expr' ty hasVariablesType ty pure [] hasVariablesType ty down [("a", KFun KType KType)] diff --git a/primer/test/Tests/Refine.hs b/primer/test/Tests/Refine.hs index 06acc4624..78113133a 100644 --- a/primer/test/Tests/Refine.hs +++ b/primer/test/Tests/Refine.hs @@ -33,7 +33,7 @@ import Primer.Gen.Core.Typed ( import Primer.Module (builtinModule, primitiveModule) import Primer.Name (NameCounter) import Primer.Refine (Inst (InstAPP, InstApp, InstUnconstrainedAPP), refine) -import Primer.Subst (substTy, substTys) +import Primer.Subst (substTy, substTySimul) import Primer.Test.TestM (evalTestM) import Primer.TypeDef (astTypeDefConstructors, astTypeDefParameters, typeDefAST, valConType) import Primer.Typecheck ( @@ -290,17 +290,18 @@ tasty_refinement_synths = propertyWTInExtendedLocalGlobalCxt [builtinModule, pri annotateShow e (ty, e') <- synthTest =<< generateIDs e e === forgetMetadata e' -- check no smart holes stuff happened - let g i a = case (i, a) of (InstUnconstrainedAPP n _, Left t) -> Just (n, t); _ -> Nothing - sb' = catMaybes $ zipWith g is apps + let g i a = case (i, a) of (InstUnconstrainedAPP n _, Left t) -> Just $ M.singleton n t; _ -> Nothing + sb' = mconcat $ catMaybes $ zipWith g is apps -- Check some invariants from @genInstApp@ sb === sb' - instTy' <- substTys sb instTy + instTy' <- substTySimul sb instTy ty === instTy' diff ty consistentTypes tgt _ -> discard -- | (Because unif vars are only in one side) the names from -- 'InstUnconstrainedAPP' do not appear in 'InstAPP's (but can in 'InstApp's) +-- Also, these names are distinct tasty_scoping :: Property tasty_scoping = propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ do tgt <- forAllT $ genWTType KType @@ -310,9 +311,13 @@ tasty_scoping = propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModu annotateShow r case r of Just (is, _) -> do - let ns = S.fromList $ mapMaybe unconstrName is + let ns' = mapMaybe unconstrName is + ns = S.fromList ns' ts = mapMaybe aPPTy is fvs = mconcat $ map freeVarsTy ts + -- names are distinct + length ns' === S.size ns + -- names do not occur in 'InstAPP's ns `S.intersection` fvs === mempty _ -> discard where diff --git a/primer/test/Tests/Transform.hs b/primer/test/Tests/Transform.hs index 85616034d..523d82031 100644 --- a/primer/test/Tests/Transform.hs +++ b/primer/test/Tests/Transform.hs @@ -178,7 +178,7 @@ unit_app :: Assertion unit_app = afterRename "x" "y" (app (lvar "x") (lvar "x")) (Just (app (lvar "y") (lvar "y"))) unit_con :: Assertion -unit_con = afterRename "x" "y" (con cTrue) (Just (con cTrue)) +unit_con = afterRename "x" "y" (conSat cJust [lvar "x"]) (Just (conSat cJust [lvar "y"])) unit_case :: Assertion unit_case = @@ -294,12 +294,13 @@ afterRename' rename normalise fromVar toVar input output = do unit_unfoldApp_1 :: Assertion unit_unfoldApp_1 = let expr :: Expr' () () - expr = App () (App () (App () (Con () $ vcn ["M"] "C") (Lam () "x" (v "x"))) (App () (v "w") (v "y"))) (v "z") + expr = App () (App () (App () (EmptyHole ()) (Lam () "x" (v "x"))) (App () (v "w") (v "y"))) (v "z") v = Var () . LocalVarRef - in unfoldApp expr @?= (Con () $ vcn ["M"] "C", [Lam () "x" (v "x"), App () (v "w") (v "y"), v "z"]) + in unfoldApp expr @?= (EmptyHole (), [Lam () "x" (v "x"), App () (v "w") (v "y"), v "z"]) unit_unfoldApp_2 :: Assertion unit_unfoldApp_2 = let expr :: Expr' () () - expr = Con () $ vcn ["M"] "C" + expr = Con () (vcn ["M"] "C") [v "x", v "y"] + v = Var () . LocalVarRef in unfoldApp expr @?= (expr, []) diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index 023621eca..eb7160456 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -27,6 +27,7 @@ import Primer.Builtins ( boolDef, cCons, cFalse, + cMakePair, cNil, cSucc, cTrue, @@ -140,12 +141,63 @@ unit_const = (lam "x" (lam "y" (lvar "x"))) (tfun (tcon tBool) (tfun (tcon tBool) (tcon tBool))) -unit_true :: Assertion -unit_true = expectTyped $ con cTrue +unit_true_bool :: Assertion +unit_true_bool = expectTyped $ con0 cTrue `ann` tcon tBool + +-- An empty hole accepts saturated constructors +unit_true_hole :: Assertion +unit_true_hole = expectTyped $ con0 cTrue `ann` tEmptyHole + +-- An empty hole rejects under-saturated constructors +unit_unsat_con_hole_1 :: Assertion +unit_unsat_con_hole_1 = + (con0 cSucc `ann` tEmptyHole) + `expectFailsWith` \_ -> UnsaturatedConstructor cSucc + +-- An empty hole rejects over-saturated constructors +unit_unsat_con_hole_2 :: Assertion +unit_unsat_con_hole_2 = + con cSucc [emptyHole, emptyHole] + `ann` tEmptyHole + `expectFailsWith` \_ -> UnsaturatedConstructor cSucc + +-- 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) + +-- 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) + +-- 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) + +-- A hole-headed TApp rejects saturated constructors, if application spine is too long for the constructor +unit_con_hole_app_type_4 :: Assertion +unit_con_hole_app_type_4 = + ( con cMakePair [emptyHole, emptyHole] + `ann` (tEmptyHole `tapp` tcon tBool `tapp` tcon tNat `tapp` tEmptyHole) + ) + `expectFailsWith` \_ -> + ConstructorNotFullAppADT + (TApp () (TApp () (TApp () (TEmptyHole ()) (TCon () tBool)) (TCon () tNat)) (TEmptyHole ())) + cMakePair unit_constructor_doesn't_exist :: Assertion unit_constructor_doesn't_exist = - con nope `expectFailsWith` const (UnknownConstructor nope) + (con nope [] `ann` tEmptyHole) `expectFailsWith` const (UnknownConstructor nope) where nope = vcn ["M"] "Nope" @@ -153,9 +205,27 @@ unit_inc :: Assertion unit_inc = expectTyped $ ann - (lam "n" (app (con cSucc) (lvar "n"))) + (lam "n" (con1 cSucc $ lvar "n")) (tfun (tcon tNat) (tcon tNat)) +-- NB: @Succ :: Nat@ is wrong: unsaturated! +-- cf unit_inc_unsat2 +unit_inc_unsat1 :: Assertion +unit_inc_unsat1 = + ann + (lam "n" (app (con0 cSucc `ann` tEmptyHole) (lvar "n"))) + (tfun (tcon tNat) (tcon tNat)) + `expectFailsWith` const (UnsaturatedConstructor cSucc) + +-- NB: @Succ :: Nat -> Nat@ is wrong: constructors don't inhabit function types! +-- cf unit_inc_unsat1 +unit_inc_unsat2 :: Assertion +unit_inc_unsat2 = + ann + (lam "n" (app (con0 cSucc `ann` (tcon tNat `tfun` tcon tNat)) (lvar "n"))) + (tfun (tcon tNat) (tcon tNat)) + `expectFailsWith` const (ConstructorNotFullAppADT (TFun () (TCon () tNat) (TCon () tNat)) cSucc) + unit_compose_nat :: Assertion unit_compose_nat = expectTyped $ @@ -169,10 +239,10 @@ unit_compose_nat = ) ) --- let x = True in x +-- let x = True :: Bool in x unit_let :: Assertion unit_let = - expectTyped $ let_ "x" (con cTrue) (lvar "x") + expectTyped $ let_ "x" (con0 cTrue `ann` tcon tBool) (lvar "x") -- Normal lets do not permit recursion unit_recursive_let :: Assertion @@ -200,39 +270,36 @@ unit_letrec_2 = "x" ( case_ (lvar "x") - [ branch cZero [] (con cZero) + [ branch cZero [] (con0 cZero) , branch cSucc [("n", Nothing)] - ( app - (con cSucc) - (app (con cSucc) (app (lvar "double") (lvar "n"))) - ) + (con1 cSucc $ con1 cSucc $ app (lvar "double") (lvar "n")) ] ) ) (tfun (tcon tNat) (tcon tNat)) - (app (lvar "double") (app (con cSucc) (con cZero))) + (app (lvar "double") (con cSucc [con0 cZero])) --- let x = True --- in let y = False +-- let x = True :: Bool +-- in let y = False :: Bool -- in x unit_nested_let :: Assertion unit_nested_let = - expectTyped $ let_ "x" (con cTrue) (let_ "y" (con cFalse) (lvar "x")) + expectTyped $ let_ "x" (con0 cTrue `ann` tcon tBool) (let_ "y" (con0 cFalse `ann` tcon tBool) (lvar "x")) -- let yes = \x -> True : Bool -> Bool --- in let y = False +-- in let y = False :: Bool -- in yes y unit_let_function :: Assertion unit_let_function = expectTyped $ let_ "yes" - (ann (lam "x" (con cTrue)) (tfun (tcon tBool) (tcon tBool))) - (let_ "y" (con cFalse) (app (lvar "yes") (lvar "y"))) + (ann (lam "x" (con0 cTrue)) (tfun (tcon tBool) (tcon tBool))) + (let_ "y" (con0 cFalse `ann` tcon tBool) (app (lvar "yes") (lvar "y"))) --- (\f -> f : (Bool -> Bool) -> (Bool -> Bool)) (let y = True in \x -> y) +-- (\f -> f : (Bool -> Bool) -> (Bool -> Bool)) (let y = True :: Bool in \x -> y) unit_let_in_arg :: Assertion unit_let_in_arg = expectTyped $ @@ -241,7 +308,7 @@ unit_let_in_arg = (lam "f" (lvar "f")) (tfun (tfun (tcon tBool) (tcon tBool)) (tfun (tcon tBool) (tcon tBool))) ) - (let_ "y" (con cTrue) (lam "x" (lvar "y"))) + (let_ "y" (con0 cTrue `ann` tcon tBool) (lam "x" (lvar "y"))) unit_mkTAppCon :: Assertion unit_mkTAppCon = do @@ -310,7 +377,7 @@ unit_valConType = do unit_case_isZero :: Assertion unit_case_isZero = expectTyped $ - ann (lam "x" $ case_ (lvar "x") [branch cZero [] (con cTrue), branch cSucc [("n", Nothing)] (con cFalse)]) (tfun (tcon tNat) (tcon tBool)) + 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 @@ -333,13 +400,13 @@ unit_ann_bad = unit_ann_insert :: Assertion unit_ann_insert = - app (lam "x" $ lvar "x") (con cZero) - `smartSynthGives` app (ann (lam "x" $ lvar "x") tEmptyHole) (con cZero) + app (lam "x" $ lvar "x") (con0 cZero) + `smartSynthGives` app (ann (lam "x" $ lvar "x") tEmptyHole) (con0 cZero) unit_app_not_arrow :: Assertion unit_app_not_arrow = - app (con cZero) (con cZero) - `smartSynthGives` app (hole (con cZero)) (con cZero) + app (con0 cZero `ann` tcon tNat) (con0 cZero) + `smartSynthGives` app (hole (con0 cZero `ann` tcon tNat)) (con0 cZero) -- Note: there is something odd with this test, related to -- annotations-changing-types/chk-annotations I think the correct thing to give @@ -348,23 +415,45 @@ unit_app_not_arrow = -- The smartTC currently gives an annotation inside a hole. unit_chk_lam_not_arrow :: Assertion unit_chk_lam_not_arrow = - app (con cSucc) (lam "x" $ lvar "x") - `smartSynthGives` app (con cSucc) (hole $ ann (lam "x" $ lvar "x") tEmptyHole) + (con1 cSucc (lam "x" $ lvar "x") `ann` tcon tNat) + `smartSynthGives` (con1 cSucc (hole $ ann (lam "x" $ lvar "x") tEmptyHole) `ann` tcon tNat) unit_check_emb :: Assertion unit_check_emb = - app (con cSucc) (con cTrue) - `smartSynthGives` app (con cSucc) (hole $ con cTrue) + (con1 cSucc (con0 cTrue) `ann` tcon tNat) -- TODO: this test does not pass..., and is bug in TC code + `smartSynthGives` (con1 cSucc (hole $ con0 cTrue `ann` tEmptyHole) `ann` tcon tNat) + +unit_bad_con_sh :: Assertion +unit_bad_con_sh = + (con0 cTrue `ann` tcon tNat) + `smartSynthGives` (hole (con0 cTrue `ann` tEmptyHole) `ann` tcon tNat) + +unit_con_syn_sh :: Assertion +unit_con_syn_sh = + con0 cTrue + `smartSynthGives` (con0 cTrue `ann` tEmptyHole) + +unit_con_not_adt_sh :: Assertion +unit_con_not_adt_sh = + con0 cTrue + `ann` (tcon tNat `tfun` tcon tBool) + `smartSynthGives` (hole (con0 cTrue `ann` tEmptyHole) `ann` (tcon tNat `tfun` tcon tBool)) + +unit_con_wrong_adt_sh :: Assertion +unit_con_wrong_adt_sh = + con0 cTrue + `ann` tcon tNat + `smartSynthGives` (hole (con0 cTrue `ann` tEmptyHole) `ann` tcon tNat) unit_case_scrutinee :: Assertion unit_case_scrutinee = - ann (case_ (con cSucc) [branch' (["M"], "C") [] $ lvar "x"]) (tcon tBool) - `smartSynthGives` ann (case_ (hole $ con cSucc) []) (tcon tBool) + ann (case_ (lam "n" (con1 cSucc $ lvar "n") `ann` (tcon tNat `tfun` tcon tNat)) [branch' (["M"], "C") [] $ lvar "x"]) (tcon tBool) + `smartSynthGives` ann (case_ (hole $ lam "n" (con1 cSucc $ lvar "n") `ann` (tcon tNat `tfun` tcon tNat)) []) (tcon tBool) unit_case_branches :: Assertion unit_case_branches = - ann (case_ (con cZero) [branch' (["M"], "C") [] $ lvar "x"]) (tcon tBool) - `smartSynthGives` ann (case_ (con cZero) [branch cZero [] emptyHole, branch cSucc [("a7", Nothing)] emptyHole]) (tcon tBool) -- Fragile name here "a7" + ann (case_ (con0 cZero `ann` tcon tNat) [branch' (["M"], "C") [] $ lvar "x"]) (tcon tBool) + `smartSynthGives` ann (case_ (con0 cZero `ann` tcon tNat) [branch cZero [] emptyHole, branch cSucc [("a9", Nothing)] emptyHole]) (tcon tBool) -- Fragile name here "a9" unit_remove_hole :: Assertion unit_remove_hole = @@ -379,9 +468,9 @@ unit_remove_hole = -- This is tracked as https://github.com/hackworthltd/primer/issues/7 unit_remove_hole_not_perfect :: Assertion unit_remove_hole_not_perfect = - app (hole (con cSucc)) (con cZero) - `smartSynthGives` app (hole (con cSucc)) (con cZero) -- We currently give this as output - -- app (con cSucc) (con cZero) -- We would prefer to see the hole removed + app (hole $ lam "n" (con1 cSucc $ lvar "n") `ann` (tcon tNat `tfun` tcon tNat)) (con0 cZero) + `smartSynthGives` app (hole $ lam "n" (con1 cSucc $ lvar "n") `ann` (tcon tNat `tfun` tcon tNat)) (con0 cZero) -- We currently give this as output + -- app (lam "n" ( con1 cSucc $ lvar "n") `ann` (tcon tNat `tfun` tcon tNat)) (con0 cZero) -- We would prefer to see the hole removed -- When not using "smart" TC which automatically inserts holes etc, -- one would have to do a bit of dance to build a case expression, and @@ -395,7 +484,7 @@ unit_smart_remove_clean_case = ann ( case_ (lvar "x") - [branch cTrue [] (con cZero), branch cFalse [] emptyHole] + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) tEmptyHole ) @@ -404,7 +493,7 @@ unit_smart_remove_clean_case = ( lam "x" $ case_ (lvar "x") - [branch cTrue [] (con cZero), branch cFalse [] emptyHole] + [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] ) (tfun (tcon tBool) (tcon tNat)) @@ -422,8 +511,8 @@ unit_poly_head_Nat = ( lam "x" $ case_ (lvar "x") - [ branch cNil [] (con cZero) - , branch cCons [("y", Nothing), ("ys", Nothing)] $ con cSucc `app` lvar "y" + [ branch cNil [] (con0 cZero) + , branch cCons [("y", Nothing), ("ys", Nothing)] $ con1 cSucc $ lvar "y" ] ) ((tcon tList `tapp` tcon tNat) `tfun` tcon tNat) @@ -824,7 +913,7 @@ expectFailsWith m err = do Left constructionErr -> assertFailure $ show constructionErr Right expr' -> pure expr' case runTypecheckTestM NoSmartHoles (m >>= synth) of - Left e -> err expr @?= e + Left e -> e @?= err expr Right _ -> assertFailure "Expected failure but succeeded" smartSynthGives :: HasCallStack => TypecheckTestM Expr -> TypecheckTestM Expr -> Assertion diff --git a/primer/test/Tests/Unification.hs b/primer/test/Tests/Unification.hs index 2747c9f3e..de2205e19 100644 --- a/primer/test/Tests/Unification.hs +++ b/primer/test/Tests/Unification.hs @@ -38,7 +38,7 @@ import Primer.Gen.Core.Typed ( import Primer.Module (Module, builtinModule, primitiveModule) import Primer.Name (NameCounter) import Primer.Primitives (tInt) -import Primer.Subst (substTys) +import Primer.Subst (substTySimul) import Primer.Test.TestM (evalTestM) import Primer.Test.Util (tcn) import Primer.TypeDef (ASTTypeDef (ASTTypeDef, astTypeDefConstructors, astTypeDefNameHints, astTypeDefParameters), TypeDef (TypeDefAST)) @@ -486,8 +486,8 @@ tasty_sub_unifies = propertyWTInExtendedUVCxt [builtinModule, primitiveModule] $ case u of Nothing -> discard Just sub -> do - s' <- substTys (M.toList sub) s - t' <- substTys (M.toList sub) t + s' <- substTySimul sub s + t' <- substTySimul sub t diff s' consistentTypes t' -- unify ga uvs S T = Maybe sub => for t/a in sub, have checkKind uvs(a) t @@ -516,8 +516,8 @@ tasty_unified_checks = propertyWTInExtendedUVCxt [builtinModule, primitiveModule case u of Nothing -> discard Just sub -> do - s' <- substTys (M.toList sub) s - t' <- substTys (M.toList sub) t + s' <- substTySimul sub s + t' <- substTySimul sub t s'' <- checkKindTest k =<< generateTypeIDs s' s' === forgetTypeMetadata s'' -- check no smartholes happened t'' <- checkKindTest k =<< generateTypeIDs t' diff --git a/primer/test/Tests/Utils.hs b/primer/test/Tests/Utils.hs index 7d26e7631..38298d4c0 100644 --- a/primer/test/Tests/Utils.hs +++ b/primer/test/Tests/Utils.hs @@ -29,7 +29,7 @@ genAST example = fst $ create $ example <&> snd -- particular next 'ID', only that 'nextID' returns whatever -- 'Examples.map''s next 'ID' happens to be. unit_nextID_exampleMap :: Assertion -unit_nextID_exampleMap = nextID (genAST $ Examples.map modName) @?= ID 41 +unit_nextID_exampleMap = nextID (genAST $ Examples.map modName) @?= ID 35 -- See note for 'unit_nextID_exampleMap'. unit_nextID_exampleEven :: Assertion @@ -41,4 +41,4 @@ unit_nextID_exampleOdd = nextID (genAST $ Examples.odd modName) @?= ID 11 -- See note for 'unit_nextID_exampleMap'. unit_nextID_exampleComprehensive :: Assertion -unit_nextID_exampleComprehensive = nextID (genAST $ Examples.comprehensive modName) @?= ID 49 +unit_nextID_exampleComprehensive = nextID (genAST $ Examples.comprehensive modName) @?= ID 52 diff --git a/primer/test/outputs/APITree/Expr b/primer/test/outputs/APITree/Expr index efecffa2c..761eb46b9 100644 --- a/primer/test/outputs/APITree/Expr +++ b/primer/test/outputs/APITree/Expr @@ -12,23 +12,47 @@ Tree , childTrees = [ Tree { nodeId = "10" - , body = TextBody - ( RecordPair - { fst = Con - , snd = Name - { qualifiedModule = Just - ( ModuleName - { unModuleName = "Builtins" :| [] } - ) - , baseName = "True" - } + , body = NoBody Ann + , childTrees = + [ Tree + { nodeId = "11" + , body = TextBody + ( RecordPair + { fst = Con + , snd = Name + { qualifiedModule = Just + ( ModuleName + { unModuleName = "Builtins" :| [] } + ) + , baseName = "True" + } + } + ) + , childTrees = [] + , rightChild = Nothing } - ) - , childTrees = [] + , Tree + { nodeId = "12" + , body = TextBody + ( RecordPair + { fst = TCon + , snd = Name + { qualifiedModule = Just + ( ModuleName + { unModuleName = "Builtins" :| [] } + ) + , baseName = "Bool" + } + } + ) + , childTrees = [] + , rightChild = Nothing + } + ] , rightChild = Nothing } , Tree - { nodeId = "11" + { nodeId = "13" , body = TextBody ( RecordPair { fst = Letrec @@ -40,39 +64,83 @@ Tree ) , childTrees = [ Tree - { nodeId = "12" + { nodeId = "14" , body = NoBody App , childTrees = [ Tree - { nodeId = "13" + { nodeId = "15" , body = NoBody Hole , childTrees = [ Tree - { nodeId = "14" - , body = TextBody - ( RecordPair - { fst = Con - , snd = Name - { qualifiedModule = Just - ( ModuleName - { unModuleName = "Builtins" :| [] } - ) - , baseName = "Just" - } + { nodeId = "16" + , body = NoBody Ann + , childTrees = + [ Tree + { nodeId = "17" + , body = TextBody + ( RecordPair + { fst = Con + , snd = Name + { qualifiedModule = Just + ( ModuleName + { unModuleName = "Builtins" :| [] } + ) + , baseName = "Just" + } + } + ) + , childTrees = + [ Tree + { nodeId = "18" + , body = NoBody EmptyHole + , childTrees = [] + , rightChild = Nothing + } + ] + , rightChild = Nothing } - ) - , childTrees = [] + , Tree + { nodeId = "19" + , body = NoBody TApp + , childTrees = + [ Tree + { nodeId = "20" + , body = TextBody + ( RecordPair + { fst = TCon + , snd = Name + { qualifiedModule = Just + ( ModuleName + { unModuleName = "Builtins" :| [] } + ) + , baseName = "Maybe" + } + } + ) + , childTrees = [] + , rightChild = Nothing + } + , Tree + { nodeId = "21" + , body = NoBody TEmptyHole + , childTrees = [] + , rightChild = Nothing + } + ] + , rightChild = Nothing + } + ] , rightChild = Nothing } ] , rightChild = Nothing } , Tree - { nodeId = "15" + { nodeId = "22" , body = NoBody Hole , childTrees = [ Tree - { nodeId = "16" + { nodeId = "23" , body = TextBody ( RecordPair { fst = GlobalVar @@ -95,11 +163,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "17" + { nodeId = "24" , body = NoBody THole , childTrees = [ Tree - { nodeId = "18" + { nodeId = "25" , body = TextBody ( RecordPair { fst = TCon @@ -119,11 +187,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "19" + { nodeId = "26" , body = NoBody Ann , childTrees = [ Tree - { nodeId = "20" + { nodeId = "27" , body = TextBody ( RecordPair { fst = Lam @@ -135,7 +203,7 @@ Tree ) , childTrees = [ Tree - { nodeId = "21" + { nodeId = "28" , body = TextBody ( RecordPair { fst = LAM @@ -147,15 +215,15 @@ Tree ) , childTrees = [ Tree - { nodeId = "22" + { nodeId = "29" , body = NoBody App , childTrees = [ Tree - { nodeId = "23" + { nodeId = "30" , body = NoBody APP , childTrees = [ Tree - { nodeId = "24" + { nodeId = "31" , body = TextBody ( RecordPair { fst = LetType @@ -167,74 +235,24 @@ Tree ) , childTrees = [ Tree - { nodeId = "26" - , body = NoBody APP - , childTrees = - [ Tree - { nodeId = "27" - , body = TextBody - ( RecordPair - { fst = Con - , snd = Name - { qualifiedModule = Just - ( ModuleName - { unModuleName = "Builtins" :| [] } - ) - , baseName = "Left" - } - } - ) - , childTrees = [] - , rightChild = Nothing - } - , Tree - { nodeId = "28" - , body = TextBody - ( RecordPair - { fst = TLet - , snd = Name - { qualifiedModule = Nothing - , baseName = "c" - } - } - ) - , childTrees = - [ Tree - { nodeId = "29" - , body = TextBody - ( RecordPair - { fst = TVar - , snd = Name - { qualifiedModule = Nothing - , baseName = "b" - } - } - ) - , childTrees = [] - , rightChild = Nothing - } - , Tree - { nodeId = "30" - , body = TextBody - ( RecordPair - { fst = TVar - , snd = Name - { qualifiedModule = Nothing - , baseName = "c" - } - } - ) - , childTrees = [] - , rightChild = Nothing - } - ] - , rightChild = Nothing + { nodeId = "33" + , body = TextBody + ( RecordPair + { fst = Con + , snd = Name + { qualifiedModule = Just + ( ModuleName + { unModuleName = "Builtins" :| [] } + ) + , baseName = "Left" + } } - ] + ) + , childTrees = [] , rightChild = Nothing } , Tree - { nodeId = "25" + { nodeId = "32" , body = TextBody ( RecordPair { fst = TCon @@ -254,7 +272,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "31" + { nodeId = "34" , body = TextBody ( RecordPair { fst = TVar @@ -271,11 +289,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "32" + { nodeId = "35" , body = NoBody Case , childTrees = [ Tree - { nodeId = "33" + { nodeId = "36" , body = TextBody ( RecordPair { fst = LocalVar @@ -291,12 +309,12 @@ Tree ] , rightChild = Just ( Tree - { nodeId = "32P0" + { nodeId = "35P0" , body = BoxBody ( RecordPair { fst = Pattern , snd = Tree - { nodeId = "32P0B" + { nodeId = "35P0B" , body = TextBody ( RecordPair { fst = PatternCon @@ -316,7 +334,7 @@ Tree ) , childTrees = [ Tree - { nodeId = "34" + { nodeId = "37" , body = TextBody ( RecordPair { fst = Con @@ -335,16 +353,16 @@ Tree ] , rightChild = Just ( Tree - { nodeId = "32P1" + { nodeId = "35P1" , body = BoxBody ( RecordPair { fst = Pattern , snd = Tree - { nodeId = "35A" + { nodeId = "38A" , body = NoBody PatternApp , childTrees = [ Tree - { nodeId = "32P1B" + { nodeId = "35P1B" , body = TextBody ( RecordPair { fst = PatternCon @@ -361,7 +379,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "35" + { nodeId = "38" , body = TextBody ( RecordPair { fst = PatternBind @@ -381,21 +399,21 @@ Tree ) , childTrees = [ Tree - { nodeId = "36" + { nodeId = "39" , body = NoBody App , childTrees = [ Tree - { nodeId = "37" + { nodeId = "40" , body = NoBody App , childTrees = [ Tree - { nodeId = "38" + { nodeId = "41" , body = NoBody EmptyHole , childTrees = [] , rightChild = Nothing } , Tree - { nodeId = "39" + { nodeId = "42" , body = TextBody ( RecordPair { fst = LocalVar @@ -412,7 +430,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "40" + { nodeId = "43" , body = TextBody ( RecordPair { fst = LocalVar @@ -445,11 +463,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "41" + { nodeId = "44" , body = NoBody TFun , childTrees = [ Tree - { nodeId = "42" + { nodeId = "45" , body = TextBody ( RecordPair { fst = TCon @@ -466,7 +484,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "43" + { nodeId = "46" , body = TextBody ( RecordPair { fst = TForall @@ -478,15 +496,15 @@ Tree ) , childTrees = [ Tree - { nodeId = "44" + { nodeId = "47" , body = NoBody TApp , childTrees = [ Tree - { nodeId = "45" + { nodeId = "48" , body = NoBody TApp , childTrees = [ Tree - { nodeId = "46" + { nodeId = "49" , body = TextBody ( RecordPair { fst = TCon @@ -503,7 +521,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "47" + { nodeId = "50" , body = TextBody ( RecordPair { fst = TCon @@ -523,7 +541,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "48" + { nodeId = "51" , body = TextBody ( RecordPair { fst = TVar diff --git a/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi b/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi index b3a9fe6df..fef8c912a 100644 --- a/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi +++ b/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi @@ -1,15 +1,24 @@ -let x = True in - let rec y = (({?Just?}) ({?unboundName?})) :: ({?Maybe?}) in +let x = (True) :: (Bool) in + let rec y = + ( + ( + {?(Just (?)) :: ((Maybe) (?))?} + ) + ( + {?unboundName?} + ) + ) :: + ( + {?Maybe?} + ) + in ( λi. Λβ. ( ( let type b = Bool in - ( - Left - ) @let c = b in - c + Left ) @β ) ( diff --git a/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi b/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi index cda6dcaad..23b6fa5ab 100644 --- a/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi +++ b/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi @@ -1,11 +1,29 @@ let x = - True + ( + True + ) :: + ( + Bool + ) in let rec y = ( ( {? - Just + ( + Just + ( + ? + ) + ) :: + ( + ( + Maybe + ) + ( + ? + ) + ) ?} ) ( @@ -28,12 +46,7 @@ let type b = Bool in - ( - Left - ) @let c = - b - in - c + Left ) @β ) ( diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment index 2e239fad9..cafa9843e 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment @@ -88,6 +88,32 @@ Output ) , ( 11 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "x" + , context = Nothing + } + , Option + { option = "y" + , context = Nothing + } + , Option + { option = "z" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 13 , [ Input MakeLam ( Options @@ -136,7 +162,7 @@ Output ] ) , - ( 12 + ( 14 , [ Input MakeLam ( Options @@ -163,7 +189,7 @@ Output ] ) , - ( 13 + ( 15 , [ Input MakeLam ( Options @@ -191,7 +217,7 @@ Output ] ) , - ( 14 + ( 16 , [ Input MakeLam ( Options @@ -212,11 +238,38 @@ Output , free = FreeVarName } ) + , NoInput MakeCase , NoInput DeleteExpr ] ) , - ( 15 + ( 17 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 18 , [ Input MakeLam ( Options @@ -252,7 +305,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -265,16 +319,170 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Left" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Right" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nil" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Cons" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nothing" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Just" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Zero" , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Succ" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "MakePair" + , context = Just + ( "Builtins" :| [] ) + } + ] + , free = FreeNone + } + ) + , Input MakeInt + ( Options + { opts = [] + , free = FreeInt + } + ) + , Input MakeChar + ( Options + { opts = [] + , free = FreeChar + } + ) + , NoInput Raise + ] + ) + , + ( 22 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input MakeVar + ( Options + { opts = + [ Option + { option = "x" + , context = Nothing + } + , Option + { option = "y" + , context = Nothing + } ] , free = FreeNone } ) , NoInput MakeCase + , Input MakeConSat + ( Options + { opts = + [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Left" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Right" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nil" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Cons" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nothing" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Just" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Succ" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "MakePair" + , context = Just + ( "Builtins" :| [] ) + } + ] + , free = FreeNone + } + ) , Input MakeInt ( Options { opts = [] @@ -291,7 +499,7 @@ Output ] ) , - ( 18 + ( 25 , [ Input MakeLam ( Options @@ -321,7 +529,7 @@ Output ] ) , - ( 19 + ( 26 , [ Input MakeLam ( Options @@ -374,7 +582,7 @@ Output ] ) , - ( 20 + ( 27 , [ Input MakeLam ( Options @@ -400,7 +608,7 @@ Output ] ) , - ( 21 + ( 28 , [ Input MakeLam ( Options @@ -427,7 +635,7 @@ Output ] ) , - ( 22 + ( 29 , [ Input MakeLam ( Options @@ -453,7 +661,7 @@ Output ] ) , - ( 23 + ( 30 , [ Input MakeLam ( Options @@ -479,7 +687,7 @@ Output ] ) , - ( 24 + ( 31 , [ Input MakeLam ( Options @@ -505,7 +713,44 @@ Output ] ) , - ( 27 + ( 32 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input RenameLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 33 , [ Input MakeLam ( Options @@ -531,7 +776,7 @@ Output ] ) , - ( 28 + ( 34 , [ Input MakeLam ( Options @@ -558,7 +803,33 @@ Output ] ) , - ( 29 + ( 44 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 45 , [ Input MakeLam ( Options @@ -585,7 +856,33 @@ Output ] ) , - ( 30 + ( 46 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 47 , [ Input RenamePattern ( Options @@ -613,7 +910,7 @@ Output ] ) , - ( 31 + ( 48 , [ Input MakeLam ( Options @@ -640,7 +937,7 @@ Output ] ) , - ( 32 + ( 49 , [ Input MakeLam ( Options @@ -667,7 +964,7 @@ Output ] ) , - ( 33 + ( 50 , [ Input MakeLam ( Options @@ -711,7 +1008,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -724,16 +1022,55 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Left" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Right" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nil" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Cons" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nothing" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Just" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Zero" , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Succ" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "MakePair" + , context = Just + ( "Builtins" :| [] ) + } ] , free = FreeNone } ) - , NoInput MakeCase , Input MakeInt ( Options { opts = [] @@ -750,7 +1087,7 @@ Output ] ) , - ( 34 + ( 51 , [ Input MakeLam ( Options @@ -777,7 +1114,7 @@ Output ] ) , - ( 35 + ( 52 , [ Input MakeLam ( Options @@ -804,14 +1141,21 @@ Output ] ) , - ( 16 + ( 12 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 17 + ( 19 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 20 , [ NoInput MakeFun , NoInput Raise @@ -819,14 +1163,76 @@ Output ] ) , - ( 25 + ( 21 + , + [ NoInput MakeFun + , Input MakeTCon + ( Options + { opts = + [ Option + { option = "Bool" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Either" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "List" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Maybe" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nat" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Pair" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Char" + , context = Just + ( "Primitives" :| [] ) + } + , Option + { option = "Int" + , context = Just + ( "Primitives" :| [] ) + } + ] + , free = FreeNone + } + ) + , NoInput Raise + ] + ) + , + ( 23 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 26 + ( 24 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 35 , [ NoInput MakeFun , NoInput DeleteType @@ -837,6 +1243,7 @@ Output , [ NoInput MakeFun , NoInput AddInput + , NoInput Raise , NoInput DeleteType ] ) @@ -890,6 +1297,69 @@ Output ) , ( 43 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 53 + , + [ NoInput MakeFun + , NoInput AddInput + , NoInput DeleteType + ] + ) + , + ( 54 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 55 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 56 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 57 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 58 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 59 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 60 , [ NoInput MakeFun , NoInput Raise diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment index 0f856d849..069a1acdb 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment @@ -13,10 +13,6 @@ Output ( 11 , [] ) - , - ( 12 - , [] - ) , ( 13 , [] @@ -30,19 +26,15 @@ Output , [] ) , - ( 18 - , [] - ) - , - ( 19 + ( 16 , [] ) , - ( 20 + ( 17 , [] ) , - ( 21 + ( 18 , [] ) , @@ -50,11 +42,11 @@ Output , [] ) , - ( 23 + ( 25 , [] ) , - ( 24 + ( 26 , [] ) , @@ -90,23 +82,67 @@ Output , [] ) , - ( 35 + ( 44 , [] ) , - ( 16 + ( 45 , [] ) , - ( 17 + ( 46 , [] ) , - ( 25 + ( 47 , [] ) , - ( 26 + ( 48 + , [] + ) + , + ( 49 + , [] + ) + , + ( 50 + , [] + ) + , + ( 51 + , [] + ) + , + ( 52 + , [] + ) + , + ( 12 + , [] + ) + , + ( 19 + , [] + ) + , + ( 20 + , [] + ) + , + ( 21 + , [] + ) + , + ( 23 + , [] + ) + , + ( 24 + , [] + ) + , + ( 35 , [] ) , @@ -141,6 +177,38 @@ Output ( 43 , [] ) + , + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 + , [] + ) + , + ( 58 + , [] + ) + , + ( 59 + , [] + ) + , + ( 60 + , [] + ) ] , sigActions = [ diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment index 6a9e882c3..13217d2ed 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment @@ -125,13 +125,61 @@ Output , free = FreeVarName } ) - , NoInput MakeAnn + , NoInput RemoveAnn , NoInput Raise , NoInput DeleteExpr ] ) , ( 11 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "x" + , context = Nothing + } + , Option + { option = "y" + , context = Nothing + } + , Option + { option = "z" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "β" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 13 , [ Input MakeLam ( Options @@ -202,7 +250,7 @@ Output ] ) , - ( 12 + ( 14 , [ Input MakeLam ( Options @@ -251,7 +299,7 @@ Output ] ) , - ( 13 + ( 15 , [ Input MakeLam ( Options @@ -301,7 +349,55 @@ Output ] ) , - ( 14 + ( 16 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeCase + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "β" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput RemoveAnn + , NoInput DeleteExpr + ] + ) + , + ( 17 , [ Input MakeLam ( Options @@ -344,11 +440,12 @@ Output } ) , NoInput MakeAnn + , NoInput Raise , NoInput DeleteExpr ] ) , - ( 15 + ( 18 , [ Input MakeLam ( Options @@ -389,7 +486,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -451,11 +549,151 @@ Output , free = FreeNone } ) + , Input MakeVarSat + ( Options + { opts = + [ Option + { option = "comprehensive" + , context = Just + ( "M" :| [] ) + } + ] + , free = FreeNone + } + ) + , Input MakeInt + ( Options + { opts = [] + , free = FreeInt + } + ) + , Input MakeChar + ( Options + { opts = [] + , free = FreeChar + } + ) + , Input MakeLet + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input MakeLetRec + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "β" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , NoInput Raise + , NoInput EnterHole + ] + ) + , + ( 22 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input MakeVar + ( Options + { opts = + [ Option + { option = "x" + , context = Nothing + } + , Option + { option = "y" + , context = Nothing + } + , Option + { option = "comprehensive" + , context = Just + ( "M" :| [] ) + } + ] + , free = FreeNone + } + ) , NoInput MakeCase , Input MakeConSat ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -485,6 +723,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just @@ -588,7 +831,7 @@ Output ] ) , - ( 18 + ( 25 , [ Input MakeLam ( Options @@ -640,7 +883,7 @@ Output ] ) , - ( 19 + ( 26 , [ Input MakeLam ( Options @@ -715,7 +958,7 @@ Output ] ) , - ( 20 + ( 27 , [ Input MakeLam ( Options @@ -782,7 +1025,7 @@ Output ] ) , - ( 21 + ( 28 , [ Input MakeLam ( Options @@ -831,7 +1074,7 @@ Output ] ) , - ( 22 + ( 29 , [ Input MakeLam ( Options @@ -879,7 +1122,7 @@ Output ] ) , - ( 23 + ( 30 , [ Input MakeLam ( Options @@ -921,13 +1164,13 @@ Output , free = FreeVarName } ) - , NoInput MakeAnn + , NoInput RemoveAnn , NoInput Raise , NoInput DeleteExpr ] ) , - ( 24 + ( 31 , [ Input MakeLam ( Options @@ -970,12 +1213,90 @@ Output } ) , NoInput MakeAnn + , Input RenameLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) , NoInput Raise , NoInput DeleteExpr ] ) , - ( 27 + ( 32 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , Input RenameLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 33 , [ Input MakeLam ( Options @@ -1023,7 +1344,7 @@ Output ] ) , - ( 28 + ( 34 , [ Input MakeLam ( Options @@ -1072,7 +1393,55 @@ Output ] ) , - ( 29 + ( 44 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 45 , [ Input MakeLam ( Options @@ -1121,7 +1490,55 @@ Output ] ) , - ( 30 + ( 46 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 47 , [ Input RenamePattern ( Options @@ -1149,7 +1566,7 @@ Output ] ) , - ( 31 + ( 48 , [ Input MakeLam ( Options @@ -1198,7 +1615,7 @@ Output ] ) , - ( 32 + ( 49 , [ Input MakeLam ( Options @@ -1247,7 +1664,7 @@ Output ] ) , - ( 33 + ( 50 , [ Input MakeLam ( Options @@ -1296,7 +1713,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -1358,54 +1776,6 @@ Output , free = FreeNone } ) - , NoInput MakeCase - , Input MakeConSat - ( Options - { opts = - [ Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "MakePair" - , context = Just - ( "Builtins" :| [] ) - } - ] - , free = FreeNone - } - ) , Input MakeVarSat ( Options { opts = @@ -1495,7 +1865,7 @@ Output ] ) , - ( 34 + ( 51 , [ Input MakeLam ( Options @@ -1544,7 +1914,7 @@ Output ] ) , - ( 35 + ( 52 , [ Input MakeLam ( Options @@ -1593,7 +1963,7 @@ Output ] ) , - ( 16 + ( 12 , [ NoInput MakeFun , NoInput MakeTApp @@ -1620,7 +1990,7 @@ Output ] ) , - ( 17 + ( 19 , [ NoInput MakeFun , NoInput MakeTApp @@ -1643,12 +2013,11 @@ Output , free = FreeVarName } ) - , NoInput Raise , NoInput DeleteType ] ) , - ( 25 + ( 20 , [ NoInput MakeFun , NoInput MakeTApp @@ -1660,26 +2029,181 @@ Output , context = Nothing } , Option - { option = "γ" + { option = "β" , context = Nothing } , Option - { option = "β1" + { option = "γ" , context = Nothing } ] , free = FreeVarName } ) + , NoInput Raise , NoInput DeleteType ] ) , - ( 26 + ( 21 , [ NoInput MakeFun + , Input MakeTVar + ( Options + { opts = [] + , free = FreeNone + } + ) + , Input MakeTCon + ( Options + { opts = + [ Option + { option = "Bool" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Either" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "List" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Maybe" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nat" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Pair" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Char" + , context = Just + ( "Primitives" :| [] ) + } + , Option + { option = "Int" + , context = Just + ( "Primitives" :| [] ) + } + ] + , free = FreeNone + } + ) , NoInput MakeTApp , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "β" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + ] + ) + , + ( 23 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "β" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput DeleteType + ] + ) + , + ( 24 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "β" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 35 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input RenameForall ( Options { opts = [ Option @@ -1703,6 +2227,230 @@ Output ) , ( 36 + , + [ NoInput MakeFun + , NoInput AddInput + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 37 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 38 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 39 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 40 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 41 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 42 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 43 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput DeleteType + ] + ) + , + ( 53 , [ NoInput MakeFun , NoInput AddInput @@ -1730,7 +2478,7 @@ Output ] ) , - ( 37 + ( 54 , [ NoInput MakeFun , NoInput MakeTApp @@ -1758,7 +2506,7 @@ Output ] ) , - ( 38 + ( 55 , [ NoInput MakeFun , NoInput MakeTApp @@ -1805,7 +2553,7 @@ Output ] ) , - ( 39 + ( 56 , [ NoInput MakeFun , NoInput MakeTApp @@ -1833,7 +2581,7 @@ Output ] ) , - ( 40 + ( 57 , [ NoInput MakeFun , NoInput MakeTApp @@ -1861,7 +2609,7 @@ Output ] ) , - ( 41 + ( 58 , [ NoInput MakeFun , NoInput MakeTApp @@ -1889,7 +2637,7 @@ Output ] ) , - ( 42 + ( 59 , [ NoInput MakeFun , NoInput MakeTApp @@ -1917,7 +2665,7 @@ Output ] ) , - ( 43 + ( 60 , [ NoInput MakeFun , NoInput MakeTApp diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment index 0f856d849..069a1acdb 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment @@ -13,10 +13,6 @@ Output ( 11 , [] ) - , - ( 12 - , [] - ) , ( 13 , [] @@ -30,19 +26,15 @@ Output , [] ) , - ( 18 - , [] - ) - , - ( 19 + ( 16 , [] ) , - ( 20 + ( 17 , [] ) , - ( 21 + ( 18 , [] ) , @@ -50,11 +42,11 @@ Output , [] ) , - ( 23 + ( 25 , [] ) , - ( 24 + ( 26 , [] ) , @@ -90,23 +82,67 @@ Output , [] ) , - ( 35 + ( 44 , [] ) , - ( 16 + ( 45 , [] ) , - ( 17 + ( 46 , [] ) , - ( 25 + ( 47 , [] ) , - ( 26 + ( 48 + , [] + ) + , + ( 49 + , [] + ) + , + ( 50 + , [] + ) + , + ( 51 + , [] + ) + , + ( 52 + , [] + ) + , + ( 12 + , [] + ) + , + ( 19 + , [] + ) + , + ( 20 + , [] + ) + , + ( 21 + , [] + ) + , + ( 23 + , [] + ) + , + ( 24 + , [] + ) + , + ( 35 , [] ) , @@ -141,6 +177,38 @@ Output ( 43 , [] ) + , + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 + , [] + ) + , + ( 58 + , [] + ) + , + ( 59 + , [] + ) + , + ( 60 + , [] + ) ] , sigActions = [ diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment index 768520e1d..7e3e6ddd1 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment @@ -90,6 +90,33 @@ Output ) , ( 11 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "x" + , context = Nothing + } + , Option + { option = "y" + , context = Nothing + } + , Option + { option = "z" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 13 , [ Input MakeLam ( Options @@ -139,7 +166,7 @@ Output ] ) , - ( 12 + ( 14 , [ Input MakeLam ( Options @@ -167,7 +194,7 @@ Output ] ) , - ( 13 + ( 15 , [ Input MakeLam ( Options @@ -196,7 +223,7 @@ Output ] ) , - ( 14 + ( 16 , [ Input MakeLam ( Options @@ -217,12 +244,40 @@ Output , free = FreeVarName } ) + , NoInput MakeCase , NoInput MakeApp , NoInput DeleteExpr ] ) , - ( 15 + ( 17 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 18 , [ Input MakeLam ( Options @@ -263,7 +318,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -325,11 +381,130 @@ Output , free = FreeNone } ) + , Input MakeVarSat + ( Options + { opts = + [ Option + { option = "comprehensive" + , context = Just + ( "M" :| [] ) + } + ] + , free = FreeNone + } + ) + , Input MakeInt + ( Options + { opts = [] + , free = FreeInt + } + ) + , Input MakeChar + ( Options + { opts = [] + , free = FreeChar + } + ) + , Input MakeLet + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input MakeLetRec + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput Raise + , NoInput EnterHole + ] + ) + , + ( 22 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input MakeVar + ( Options + { opts = + [ Option + { option = "x" + , context = Nothing + } + , Option + { option = "y" + , context = Nothing + } + , Option + { option = "comprehensive" + , context = Just + ( "M" :| [] ) + } + ] + , free = FreeNone + } + ) , NoInput MakeCase , Input MakeConSat ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -359,6 +534,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just @@ -441,7 +621,7 @@ Output ] ) , - ( 18 + ( 25 , [ Input MakeLam ( Options @@ -472,7 +652,7 @@ Output ] ) , - ( 19 + ( 26 , [ Input MakeLam ( Options @@ -526,7 +706,7 @@ Output ] ) , - ( 20 + ( 27 , [ Input MakeLam ( Options @@ -553,7 +733,7 @@ Output ] ) , - ( 21 + ( 28 , [ Input MakeLam ( Options @@ -581,7 +761,7 @@ Output ] ) , - ( 22 + ( 29 , [ Input MakeLam ( Options @@ -608,7 +788,7 @@ Output ] ) , - ( 23 + ( 30 , [ Input MakeLam ( Options @@ -635,7 +815,7 @@ Output ] ) , - ( 24 + ( 31 , [ Input MakeLam ( Options @@ -662,7 +842,45 @@ Output ] ) , - ( 27 + ( 32 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , Input RenameLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 33 , [ Input MakeLam ( Options @@ -689,7 +907,7 @@ Output ] ) , - ( 28 + ( 34 , [ Input MakeLam ( Options @@ -717,7 +935,34 @@ Output ] ) , - ( 29 + ( 44 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 45 , [ Input MakeLam ( Options @@ -745,7 +990,34 @@ Output ] ) , - ( 30 + ( 46 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 47 , [ Input RenamePattern ( Options @@ -773,7 +1045,7 @@ Output ] ) , - ( 31 + ( 48 , [ Input MakeLam ( Options @@ -801,7 +1073,7 @@ Output ] ) , - ( 32 + ( 49 , [ Input MakeLam ( Options @@ -829,7 +1101,7 @@ Output ] ) , - ( 33 + ( 50 , [ Input MakeLam ( Options @@ -878,7 +1150,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -940,54 +1213,6 @@ Output , free = FreeNone } ) - , NoInput MakeCase - , Input MakeConSat - ( Options - { opts = - [ Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "MakePair" - , context = Just - ( "Builtins" :| [] ) - } - ] - , free = FreeNone - } - ) , Input MakeVarSat ( Options { opts = @@ -1056,7 +1281,7 @@ Output ] ) , - ( 34 + ( 51 , [ Input MakeLam ( Options @@ -1084,7 +1309,7 @@ Output ] ) , - ( 35 + ( 52 , [ Input MakeLam ( Options @@ -1112,14 +1337,21 @@ Output ] ) , - ( 16 + ( 12 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 17 + ( 19 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 20 , [ NoInput MakeFun , NoInput Raise @@ -1127,14 +1359,76 @@ Output ] ) , - ( 25 + ( 21 + , + [ NoInput MakeFun + , Input MakeTCon + ( Options + { opts = + [ Option + { option = "Bool" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Either" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "List" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Maybe" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Nat" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Pair" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "Char" + , context = Just + ( "Primitives" :| [] ) + } + , Option + { option = "Int" + , context = Just + ( "Primitives" :| [] ) + } + ] + , free = FreeNone + } + ) + , NoInput Raise + ] + ) + , + ( 23 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 26 + ( 24 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 35 , [ NoInput MakeFun , NoInput DeleteType @@ -1145,6 +1439,7 @@ Output , [ NoInput MakeFun , NoInput AddInput + , NoInput Raise , NoInput DeleteType ] ) @@ -1198,6 +1493,69 @@ Output ) , ( 43 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 53 + , + [ NoInput MakeFun + , NoInput AddInput + , NoInput DeleteType + ] + ) + , + ( 54 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 55 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 56 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 57 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 58 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 59 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 60 , [ NoInput MakeFun , NoInput Raise diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment index 0f856d849..069a1acdb 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment @@ -13,10 +13,6 @@ Output ( 11 , [] ) - , - ( 12 - , [] - ) , ( 13 , [] @@ -30,19 +26,15 @@ Output , [] ) , - ( 18 - , [] - ) - , - ( 19 + ( 16 , [] ) , - ( 20 + ( 17 , [] ) , - ( 21 + ( 18 , [] ) , @@ -50,11 +42,11 @@ Output , [] ) , - ( 23 + ( 25 , [] ) , - ( 24 + ( 26 , [] ) , @@ -90,23 +82,67 @@ Output , [] ) , - ( 35 + ( 44 , [] ) , - ( 16 + ( 45 , [] ) , - ( 17 + ( 46 , [] ) , - ( 25 + ( 47 , [] ) , - ( 26 + ( 48 + , [] + ) + , + ( 49 + , [] + ) + , + ( 50 + , [] + ) + , + ( 51 + , [] + ) + , + ( 52 + , [] + ) + , + ( 12 + , [] + ) + , + ( 19 + , [] + ) + , + ( 20 + , [] + ) + , + ( 21 + , [] + ) + , + ( 23 + , [] + ) + , + ( 24 + , [] + ) + , + ( 35 , [] ) , @@ -141,6 +177,38 @@ Output ( 43 , [] ) + , + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 + , [] + ) + , + ( 58 + , [] + ) + , + ( 59 + , [] + ) + , + ( 60 + , [] + ) ] , sigActions = [ diff --git a/primer/testlib/Primer/Test/Expected.hs b/primer/testlib/Primer/Test/Expected.hs index 99f17e1d4..fbad69e36 100644 --- a/primer/testlib/Primer/Test/Expected.hs +++ b/primer/testlib/Primer/Test/Expected.hs @@ -28,7 +28,8 @@ import Primer.Core.DSL ( aPP, ann, app, - con, + con0, + conSat, create, gvar, tapp, @@ -58,9 +59,9 @@ mapEven n = (mapName, mapDef) <- Examples.map modName (evenName, evenDef) <- Examples.even modName (oddName, oddDef) <- Examples.odd modName - let lst = list_ tNat $ take n $ iterate (con cSucc `app`) (con cZero) + let lst = list_ $ take n $ iterate (conSat cSucc . (: [])) (con0 cZero) expr <- gvar mapName `aPP` tcon tNat `aPP` tcon tBool `app` gvar evenName `app` lst let globs = M.fromList [(mapName, mapDef), (evenName, evenDef), (oddName, oddDef)] - expect <- list_ tBool (take n $ cycle [con cTrue, con cFalse]) `ann` (tcon tList `tapp` tcon tBool) + expect <- list_ (take n $ cycle [con0 cTrue, con0 cFalse]) `ann` (tcon tList `tapp` tcon tBool) pure (globs, expr, expect) in Expected globals e id expected diff --git a/primer/testlib/Primer/Test/Util.hs b/primer/testlib/Primer/Test/Util.hs index 26bf4bb50..34d93377e 100644 --- a/primer/testlib/Primer/Test/Util.hs +++ b/primer/testlib/Primer/Test/Util.hs @@ -5,7 +5,7 @@ module Primer.Test.Util ( assertException, primDefs, constructTCon, - constructCon, + constructSaturatedCon, constructRefinedCon, tcn, vcn, @@ -40,7 +40,7 @@ import Primer.API ( runPrimerM, ) import Primer.Action ( - Action (ConstructCon, ConstructRefinedCon, ConstructTCon), + Action (ConstructRefinedCon, ConstructSaturatedCon, ConstructTCon), ) import Primer.Core ( Expr', @@ -87,8 +87,8 @@ primDefs = Map.mapKeys primitive $ moduleDefs primitiveModule constructTCon :: TyConName -> Action constructTCon = ConstructTCon . toQualText -constructCon :: ValConName -> Action -constructCon = ConstructCon . toQualText +constructSaturatedCon :: ValConName -> Action +constructSaturatedCon = ConstructSaturatedCon . toQualText constructRefinedCon :: ValConName -> Action constructRefinedCon = ConstructRefinedCon . toQualText