diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json index 297e72d98..a3cb60972 100644 --- a/primer-service/test/outputs/OpenAPI/openapi.json +++ b/primer-service/test/outputs/OpenAPI/openapi.json @@ -170,7 +170,6 @@ }, "InputAction": { "enum": [ - "MakeCon", "MakeConSat", "MakeInt", "MakeChar", @@ -1063,7 +1062,6 @@ "required": true, "schema": { "enum": [ - "MakeCon", "MakeConSat", "MakeInt", "MakeChar", diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs index 7ca5bebe7..d53a1fcc9 100644 --- a/primer/gen/Primer/Gen/Core/Typed.hs +++ b/primer/gen/Primer/Gen/Core/Typed.hs @@ -79,7 +79,6 @@ import Primer.TypeDef ( ValCon (..), typeDefKind, typeDefParameters, - valConType, ) import Primer.Typecheck ( Cxt (), @@ -234,17 +233,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 - -- TODO (saturated constructors) when saturation is enforced, constructors should not appear on the left of an app node - cons <- asks allCons - let cons' = map (first (\c -> Con () c [] [])) $ 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! @@ -275,7 +269,7 @@ genSyns ty = do genCon = instantiateValCons ty >>= \case Left TDIHoleType -> - asks allCons' <&> \case + asks allCons <&> \case -- We have no constraints, generate any ctor m | null m -> Nothing cons -> Just $ do @@ -390,24 +384,14 @@ genSyn :: GenT WT (ExprG, TypeG) -- of any type genSyn = genSyns (TEmptyHole ()) -allCons :: Cxt -> M.Map ValConName (Type' ()) -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) - TypeDefPrim _ -> [] - --- TODO (saturated constructors) when saturation is enforced, allCons should be --- no longer needed, and we can rename allCons' - -- | 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@ maps to @([(p1,k1),(p2,k2)],_,T)@ in the -- returned map, then @c [A,B] _ ∈ T A B@ for any @A@ of kind @k1@ and @B@ -- of kind @k2@) -allCons' :: Cxt -> M.Map ValConName ([(TyVarName, Kind)], [Type' ()], TyConName) -allCons' cxt = M.fromList $ concatMap (uncurry consForTyDef) $ M.assocs $ typeDefs cxt +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 -> diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index f8f870362..5ac8af53b 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -69,7 +69,6 @@ import Primer.Core.DSL ( branch, case_, con, - con0, emptyHole, hole, lAM, @@ -350,7 +349,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" @@ -614,12 +612,6 @@ constructLAM mx ze = do result <- flip replace ze <$> lAM x (pure (target ze)) moveExpr Child1 result --- TODO (saturated constructors) this action will make no sense once full-saturation is enforced -constructCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ -constructCon c ze = case target ze of - EmptyHole{} -> flip replace ze <$> con0 (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 @@ -667,14 +659,19 @@ constructRefinedCon c ze = do case target ze of EmptyHole{} -> breakLR <<$>> getRefinedApplications cxt cTy tgtTy >>= \case + Just (Just (tys, tms)) + | length tys == numTyArgs && length tms == numTmArgs -> + flip replace ze <$> con n (pure <$> tys) (pure <$> tms) + -- If the refinement is not saturated, just give a saturated constructor + -- This could happen when refining @Cons@ to fit in a hole of type @List Nat -> List Nat@ + -- as we get the "type" of @Cons@ being @∀a. a -> List a -> List a@ + -- and thus a refinement of @Nat, _@. + | otherwise -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole)) -- See Note [No valid refinement] Nothing -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole)) -- TODO (saturated constructors): when constructors are checkable the above will not be valid -- since the inside of a hole must be synthesisable (see Note [Holes and bidirectionality]) - -- TODO (saturated constructors): when saturation is enforced, the Just Just case may not be valid - -- if the target type is not an applied-ADT Just Nothing -> throwError $ InternalFailure "Types of constructors always have type abstractions before term abstractions" - Just (Just (tys, tms)) -> flip replace ze <$> con n (pure <$> tys) (pure <$> tms) e -> throwError $ NeedEmptyHole (ConstructRefinedCon c) e getTypeCache :: MonadError ActionError m => Expr -> m TypeCache @@ -971,9 +968,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 cf4124e5b..902de34fc 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..e3ec29151 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -122,8 +122,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 @@ -202,14 +201,13 @@ forExpr tydefs l expr = 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,19 +326,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) + . filter (not . (&& level == Beginner) . uncurry hasArgsCon) . concatMap (\td -> (td,) <$> astTypeDefConstructors td) . mapMaybe (typeDefAST . snd) $ Map.toList typeDefs @@ -461,7 +451,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/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/App.hs b/primer/src/Primer/App.hs index dcb3cc647..3454e99da 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -64,7 +64,7 @@ import Control.Monad.Fresh (MonadFresh (..)) import Control.Monad.Log (MonadLog, WithSeverity) import Control.Monad.NestedError (MonadNestedError, throwError') import Data.Data (Data) -import Data.Generics.Uniplate.Operations (descendM, transform, transformM) +import Data.Generics.Uniplate.Operations (transform, transformM) import Data.Generics.Uniplate.Zipper ( fromZipper, ) @@ -144,7 +144,7 @@ import Primer.Core ( ) import Primer.Core.DSL (S, ann, create, emptyHole, hole, tEmptyHole, tvar) import Primer.Core.DSL qualified as DSL -import Primer.Core.Transform (foldApp, renameVar, unfoldAPP, unfoldApp, unfoldTApp) +import Primer.Core.Transform (renameVar, unfoldTApp) import Primer.Core.Utils (freeVars, generateTypeIDs, regenerateExprIDs, regenerateTypeIDs, _freeTmVars, _freeTyVars, _freeVarsTy) import Primer.Def ( ASTDef (..), @@ -772,7 +772,7 @@ applyProgAction prog mdefName = \case ) type_ updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateDecons <=< updateCons) - updateCons e = + updateCons = let typecache = _typecache % _Just -- Previously the @index@th argument @t@ to this -- constructor would have been typechecked against the old @@ -798,25 +798,12 @@ applyProgAction prog mdefName = \case (_, Nothing, Just c) -> hole $ pure x `ann` generateTypeIDs c -- This last case means that the input program had no (useful) metadata (_, Nothing, Nothing) -> hole $ pure x `ann` tEmptyHole - in case (e, unfoldApp e) of - (Con m con' tys tms, _) | con' == con -> do + in transformM $ \case + Con m con' tys tms | con' == con -> do adjustAtA index enhole tms >>= \case - Just args' -> Con m con' tys <$> traverse (descendM updateCons) args' + Just args' -> pure $ Con m con' tys 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 - adjustAtA index enhole args >>= \case - Just args' -> foldApp h =<< traverse (descendM updateCons) args' - Nothing -> do - -- The constructor is not applied as far as the changed field, - -- so the full application still typechecks, but its type has changed. - -- Thus, we put the whole thing in to a hole. - Hole <$> DSL.meta <*> (foldApp h =<< traverse (descendM updateCons) args) - _ -> - -- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones - descendM updateCons e + e -> pure e updateDecons = transformCaseBranches prog type_ $ traverse $ \cb@(CaseBranch vc binds e) -> if vc == con @@ -858,27 +845,13 @@ 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 (e, unfoldApp e) of - (Con m con' tys tms, _) | con' == con -> do + updateCons = transformM $ \case + Con m con' tys tms | con' == con -> do m' <- DSL.meta case insertAt index (EmptyHole m') tms of - Just args' -> Con m con' tys <$> traverse (descendM updateCons) args' + Just args' -> pure $ Con m con' tys 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' - Nothing -> - -- The constructor is not applied as far as the field immediately prior to the new one, - -- so the full application still typechecks, but its type has changed. - -- Thus, we put the whole thing in to a hole. - Hole <$> DSL.meta <*> (foldApp h =<< traverse (descendM updateCons) args) - _ -> - -- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones - descendM updateCons e + e -> pure e updateDecons = transformCaseBranches prog type_ $ traverse $ \cb@(CaseBranch vc binds e) -> if vc == con diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index 9e05ec887..bca61e2b7 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -224,6 +224,7 @@ data Expr' a b -- become synthesisable. -- Note [Synthesisable constructors] +-- -- Whilst our calculus is heavily inspired by bidirectional type systems -- (especially McBride's principled rendition), we do not treat constructors -- in this fashion. However, we are in the middle of changing the treatment @@ -236,30 +237,36 @@ data Expr' a b -- changed, due to asymmetries between construction and matching.) -- -- 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`, 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. +-- its type), where we insist that it is fully saturated. +-- Thus whilst `Cons` is a term, it is ill-typed. The only well-formed +-- `Cons` usages are `Cons @A x xs`, which synthesises `List A` +-- when `A ∋ x` and `List A ∋ xs`. +-- +-- Whilst this may be a bit inconsistent with the treatment of +-- functions, it has the advantage of symmetry with construction and +-- matching. (I.e. every time one sees a particular constructor, it +-- has the same form: a head of that constructor, and the same number +-- of (term) fields.) +-- TODO (saturated constructors): technically, a construction will +-- have type arguments/indices and a match will not, but this is +-- temporary, as we will soon remove indices (which will require +-- constructors to be only checkable, rather than synthesisable). -- --- For comparison, the bidirectional view would be that constructors must --- always be fully applied, and one can only subject them to a typechecking --- judgement where the type is an input. --- Thus `List Int ∋ Cons 2 Nil`, but `Cons` and `Cons 2` are ill-typed. --- Under this view, one needs to be aware of the difference between, say, +-- Thus one needs to be aware of the difference between, say, -- a globally-defined function, and a constructor "of the same type". -- For example, one can partially apply an addition function and map it -- across a list: `map (1 +) [2,3]` is well-typed, but one cannot map -- the `Succ` constructor in the same way. --- (Notice, however, that since one will always know what type one is --- considering, the constructor does not need any type applications --- corresponding to the parameters of its datatype.) -- 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 (various stages of) this translation into the core. --- To do this, we require constructor names to be unique across different types. +-- For comparison, the bidirectional view would be that constructors +-- must always be fully applied (which is the same as our treatment), +-- and one can only subject them to a typechecking judgement where the +-- type is an input (which is different to our treatment), and they do +-- not need to store their indices/type applications (different to our +-- treatment). +-- Thus `List Int ∋ Cons 2 Nil`, but `Cons 2 Nil` does not synthesise a type. -- Note [Case] -- We use a list for compatibility and ease of JSON diff --git a/primer/src/Primer/Core/Transform.hs b/primer/src/Primer/Core/Transform.hs index 7e052a9f8..ebb5542c4 100644 --- a/primer/src/Primer/Core/Transform.hs +++ b/primer/src/Primer/Core/Transform.hs @@ -4,9 +4,6 @@ module Primer.Core.Transform ( renameTyVar, renameTyVarExpr, unfoldApp, - foldApp, - unfoldAPP, - decomposeAppCon, unfoldTApp, decomposeTAppCon, foldTApp, @@ -16,26 +13,21 @@ module Primer.Core.Transform ( import Foreword -import Control.Monad.Fresh (MonadFresh) import Data.Data (Data) import Data.Generics.Uniplate.Data (descendM) import Data.List.NonEmpty qualified as NE import Optics (Field2 (_2), getting, noneOf, notElemOf, to, traverseOf, (%)) import Primer.Core ( CaseBranch' (..), - Expr, Expr' (..), - ID, LVarName, LocalName (unLocalName), TmVarRef (..), TyVarName, Type' (..), - ValConName, bindName, typesInExpr, ) -import Primer.Core.DSL (meta) import Primer.Core.Meta (TyConName) import Primer.Core.Utils (_freeVars, _freeVarsTy) @@ -221,30 +213,6 @@ 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 into a single expression. -foldApp :: (Foldable t, MonadFresh ID m) => Expr -> t Expr -> m Expr -foldApp = foldlM $ \a b -> do - m <- meta - pure $ App m a b - --- | Unfold a nested term-level type application into the application head and a list of arguments. -unfoldAPP :: Expr' a b -> (Expr' a b, [Type' b]) -unfoldAPP = second reverse . go - where - go (APP _ f x) = let (g, args) = go f in (g, x : args) - go e = (e, []) - --- | Decompose @C @A @B x y z@ to @(C,[A,B],[x,y,z])@ -decomposeAppCon :: Expr' a b -> Maybe (ValConName, a, [Type' b], [Expr' a b]) -decomposeAppCon = - unfoldApp <&> first unfoldAPP <&> \case - -- TODO (saturated constructors): This is suspicious (we reorder types and terms), but - -- (a) for well-typed terms, either tms0 or tys will be empty (since constructors only have top-level foralls) - -- (b) the situation that constructors can be on the left of an app or aPP node is temporary - -- and shortly decomposeAppCon will become a trivial match on the 'Con' constructor. - ((Con m c tys0 tms0, tys), tms) -> Just (c, m, tys0 ++ tys, tms0 ++ tms) - _ -> Nothing - -- | Unfold a nested type-level application into the application head and a list of arguments. unfoldTApp :: Type' a -> (Type' a, [Type' a]) unfoldTApp = second reverse . go diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs index 538fdfd19..8def0bb4f 100644 --- a/primer/src/Primer/Eval/Redex.hs +++ b/primer/src/Primer/Eval/Redex.hs @@ -60,6 +60,7 @@ import Primer.Core ( Ann, App, Case, + Con, LAM, Lam, Let, @@ -89,7 +90,7 @@ import Primer.Core ( getID, ) import Primer.Core.DSL (ann, letType, let_, letrec, lvar, tlet, tvar) -import Primer.Core.Transform (decomposeAppCon, decomposeTAppCon) +import Primer.Core.Transform (decomposeTAppCon) import Primer.Core.Utils ( alphaEqTy, concreteTy, @@ -549,8 +550,8 @@ viewCaseRedex tydefs = \case <|> pure (formCaseRedex c abstractArgTys tyargs args patterns br (orig, expr, cID)) _ -> mzero where - extractCon expr = case decomposeAppCon expr of - Just (c, m, params, as) -> pure (c, getID m, params, as) + extractCon = \case + Con m c params as -> pure (c, getID m, params, as) _ -> mzero extractBranch c brs = case find (\(CaseBranch n _ _) -> n == c) brs of diff --git a/primer/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs index 607f910b5..d3aa1dd86 100644 --- a/primer/src/Primer/Examples.hs +++ b/primer/src/Primer/Examples.hs @@ -270,12 +270,14 @@ comprehensive' typeable modName = do ( app ( aPP ( if typeable - then -- TODO (saturated constructors) this line is - -- only acceptible (i.e. makes a well typed - -- example) because constructors currently - -- need not be fully-saturated, and are - -- synthesisable. - con B.cLeft [tcon B.tBool] [] + then + lAM "b" (lam "x" $ con B.cLeft [tcon B.tBool, tvar "b"] [lvar "x"]) + `ann` tforall + "b" + KType + ( tcon B.tBool + `tfun` (tcon B.tEither `tapp` tcon B.tBool `tapp` tvar "b") + ) else letType "b" diff --git a/primer/src/Primer/Primitives.hs b/primer/src/Primer/Primitives.hs index 27312b7ba..7b4fc1337 100644 --- a/primer/src/Primer/Primitives.hs +++ b/primer/src/Primer/Primitives.hs @@ -35,7 +35,7 @@ import Primer.Builtins ( import Primer.Builtins.DSL (bool_, maybe_, nat) import Primer.Core ( Expr, - Expr' (App, Con, PrimCon), + Expr' (Con, PrimCon), GVarName, GlobalName, ID, @@ -274,7 +274,5 @@ primFunDef def args = case def of exprToNat = \case 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/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 2edea202d..fb651e7d4 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -117,8 +117,8 @@ import Primer.Core ( _exprTypeMeta, _typeMeta, ) -import Primer.Core.DSL (S, apps', branch, create', emptyHole, meta, meta') -import Primer.Core.Transform (decomposeAppCon, decomposeTAppCon, mkTAppCon) +import Primer.Core.DSL (S, branch, create', emptyHole, meta, meta') +import Primer.Core.Transform (decomposeTAppCon, mkTAppCon) import Primer.Core.Utils ( alphaEqTy, forgetTypeMetadata, @@ -143,14 +143,13 @@ import Primer.Module ( ) import Primer.Name (Name, NameCounter) import Primer.Primitives (primConName) -import Primer.Subst (substTy) +import Primer.Subst (substTy, substTySimul) import Primer.TypeDef ( ASTTypeDef (astTypeDefConstructors, astTypeDefParameters), TypeDef (..), TypeDefMap, ValCon (valConArgs, valConName), typeDefAST, - valConType, ) import Primer.Typecheck.Cxt (Cxt (Cxt, globalCxt, localCxt, smartHoles, typeDefs)) import Primer.Typecheck.Kindcheck ( @@ -499,20 +498,27 @@ synth = \case EmptyHole i -> pure $ annSynth0 (TEmptyHole ()) i EmptyHole -- 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 $ annSynth3 t i Con c [] [] - Nothing -> throwError' $ UnknownConstructor c Con i c tys tms -> do - -- TODO (saturated constructors) for now we synth exactly the same as the application tree, - -- but take care not to actually change the shape of the program. - -- This will change when full-saturation is enforced - elab <- apps' (pure $ Con i c [] []) $ (Right . pure <$> tys) ++ (Left . pure <$> tms) - (ty, e) <- synth elab - (tys', tms') <- case decomposeAppCon e of - Just (_, _, tys', tms') -> pure (tys', tms') - Nothing -> throwError' $ InternalError "saturated constructor: elaborated term is not ctor-headed" - pure $ annSynth3 ty i Con c tys' tms' + -- When C is a constructor of some ADT T with parameters ps with kinds ks, where C has args of types Rs[ps] + (adtName, params, argTys0) <- + asks (flip lookupConstructor c . typeDefs) >>= \case + Just (vc, tc, td) -> pure (tc, astTypeDefParameters td, valConArgs vc) + Nothing -> throwError' $ UnknownConstructor c + -- And |ps| = |As| and k ∋ A for each matching element + tys'Sub <- ensureJust (UnsaturatedConstructor c) $ zipWithExactM (\(p, k) ty -> (p,) <$> checkKind' k ty) params tys + -- 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) + let tys' = snd <$> tys'Sub + let tys'SubNoMeta = second forgetTypeMetadata <$> tys'Sub + let tys'NoMeta = snd <$> tys'SubNoMeta + -- And |rs| = |Rs| and R[As] ∋ r for each matching element + argTys <- traverse (substTySimul (M.fromList tys'SubNoMeta)) argTys0 + -- Fatal error, see comments on UnsaturatedConstructor error above + tms' <- ensureJust (UnsaturatedConstructor c) $ zipWithExactM check argTys tms + -- Then C @As rs ∈ T As + let synthedType = foldl' (TApp ()) (TCon () adtName) tys'NoMeta + pure $ annSynth3 synthedType i Con c tys' tms' -- When synthesising a hole, we first check that the expression inside it -- synthesises a type successfully (see Note [Holes and bidirectionality]). -- TODO: we would like to remove this hole (leaving e) if possible, but I @@ -567,6 +573,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. diff --git a/primer/src/Primer/Typecheck/TypeError.hs b/primer/src/Primer/Typecheck/TypeError.hs index bba989e62..3b5ae2624 100644 --- a/primer/src/Primer/Typecheck/TypeError.hs +++ b/primer/src/Primer/Typecheck/TypeError.hs @@ -14,6 +14,11 @@ data TypeError | UnknownVariable TmVarRef | TmVarWrongSort Name -- type var instead of term var | UnknownConstructor ValConName + | -- TODO (saturated constructors) eventually constructors will not store type arguments + + -- | Constructors (term-level) must be saturated. + -- This error catches both under- and over-saturation (of both type and term arguments). + UnsaturatedConstructor ValConName | -- | Cannot use a PrimCon when either no type of the appropriate name is -- in scope, or it is a user-defined type PrimitiveTypeNotInScope TyConName diff --git a/primer/test/Tests/Action.hs b/primer/test/Tests/Action.hs index 3baa34fb8..2f45b1196 100644 --- a/primer/test/Tests/Action.hs +++ b/primer/test/Tests/Action.hs @@ -39,7 +39,6 @@ import Primer.Primitives (tChar, tInt) import Primer.Test.TestM (evalTestM) import Primer.Test.Util ( clearMeta, - constructCon, constructRefinedCon, constructSaturatedCon, constructTCon, @@ -242,7 +241,7 @@ unit_8 = , Move Parent , ConstructApp , Move Child2 - , constructCon cTrue + , constructSaturatedCon cTrue ] (app (ann (lam "x" (lvar "x")) (tfun (tcon tBool) (tcon tBool))) (con0 cTrue)) @@ -253,7 +252,7 @@ unit_9 = emptyHole [ ConstructLet (Just "x") , Move Child1 - , constructCon cTrue + , constructSaturatedCon cTrue , Move Parent , Move Child2 , ConstructVar $ LocalVarRef "x" @@ -401,7 +400,7 @@ unit_bad_constructor = (const True) NoSmartHoles emptyHole - [ConstructCon (["M"], "NotARealConstructor")] + [ConstructSaturatedCon (["M"], "NotARealConstructor")] unit_bad_type_constructor :: Assertion unit_bad_type_constructor = @@ -425,7 +424,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 = @@ -440,7 +439,7 @@ unit_enter_emptyHole = actionTest NoSmartHoles emptyHole - [EnterHole, constructCon cTrue] + [EnterHole, constructSaturatedCon cTrue] (hole $ con0 cTrue) unit_enter_nonEmptyHole :: Assertion @@ -448,7 +447,7 @@ unit_enter_nonEmptyHole = actionTest NoSmartHoles (hole emptyHole) - [Move Child1, constructCon cTrue] + [Move Child1, constructSaturatedCon cTrue] (hole $ con0 cTrue) unit_bad_enter_hole :: Assertion @@ -476,7 +475,7 @@ unit_case_create = , Move Child1 , ConstructCase , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam "x" $ @@ -540,7 +539,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" @@ -574,7 +573,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" @@ -759,7 +758,7 @@ unit_case_create_smart_on_term = , ConstructVar $ LocalVarRef "x" , ConstructCase , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam @@ -787,7 +786,7 @@ unit_case_create_smart_on_hole = , ConstructVar $ LocalVarRef "x" , Move Parent , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam @@ -814,7 +813,7 @@ unit_case_change_smart_scrutinee_type = [ Move Child1 , Move Child1 , Delete - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( case_ @@ -891,7 +890,7 @@ unit_constructLAM = actionTest NoSmartHoles (emptyHole `ann` tEmptyHole) - [Move Child1, ConstructLAM (Just "a"), constructCon cTrue] + [Move Child1, ConstructLAM (Just "a"), constructSaturatedCon cTrue] (lAM "a" (con0 cTrue) `ann` tEmptyHole) unit_construct_TForall :: Assertion @@ -1101,24 +1100,28 @@ unit_refine_mismatch_var = $ hole (lvar "cons" `aPP` tEmptyHole `app` emptyHole `app` emptyHole) `ann` tcon tBool ) --- Note @cons @? ∈ ? -> List ? -> List ? ~ ? -> ?@, --- thus inserting a refined @cons@ in a hole of type @? -> ?@ may not refine as --- much as you may expect! +-- 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 NoSmartHoles (emptyHole `ann` (tEmptyHole `tfun` tEmptyHole)) [Move Child1, constructRefinedCon cCons] - (con cCons [tEmptyHole] [] `ann` (tEmptyHole `tfun` tEmptyHole)) + (hole (con cCons [tEmptyHole] [emptyHole, emptyHole]) `ann` (tEmptyHole `tfun` tEmptyHole)) +-- TODO (saturated constructors) update this comment for ctors-dont-store-indices ('Cons Nat') and ctors-are-chk +-- +-- Constructors are fully saturated, so even if the hole has type +-- @List Nat -> List Nat@, when we insert a @Cons@ constructor, we end up with +-- @{? Cons @? ? ? ?}@ unit_refine_arr_2 :: Assertion unit_refine_arr_2 = actionTest NoSmartHoles (emptyHole `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) [Move Child1, constructRefinedCon cCons] - (con cCons [tcon tNat] [emptyHole] `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) + (hole (con cCons [tEmptyHole] [emptyHole, emptyHole]) `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) unit_primitive_1 :: Assertion unit_primitive_1 = diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 22f703439..06be5f5ec 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -29,6 +29,7 @@ import Primer.Action ( Branch, Child1, Child2, + ConChild, Parent ), ) @@ -121,7 +122,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 (..), forgetTypeDefMetadata, typeDefAST) import Primer.Typecheck ( @@ -956,7 +957,16 @@ unit_RenameCon_clash = x <- hole ( hole - (con0 cA) + ( con + cA + [ tEmptyHole + , tEmptyHole + ] + [ emptyHole + , emptyHole + , emptyHole + ] + ) ) astDef "def" x <$> tEmptyHole ] @@ -1145,19 +1155,6 @@ unit_SetConFieldType_nehole_2 = (tcon $ tcn "Bool") (hole $ con0 $ vcn "True") -unit_SetConFieldType_partial_app :: Assertion -unit_SetConFieldType_partial_app = - progActionTest - ( defaultProgEditableTypeDefs $ do - x <- lam "x" $ con cA [tEmptyHole, tEmptyHole] [lvar "x"] - sequence - [ astDef "def" x <$> tcon (tcn "Bool") `tfun` (tcon (tcn "Bool") `tfun` (tcon (tcn "Bool") `tfun` ((tcon tT `tapp` tEmptyHole) `tapp` tEmptyHole))) - ] - ) - [SetConFieldType tT cA 1 $ TCon () (tcn "Int")] - $ expectError - (@?= ConNotSaturated cA) - unit_SetConFieldType_case :: Assertion unit_SetConFieldType_case = progActionTest @@ -1274,50 +1271,11 @@ unit_AddConField = , con0 (vcn "True") ] ) - [ branch cA [("p", Nothing), ("a45", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole + [ branch cA [("p", Nothing), ("a40", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole , branch cB [("r", Nothing), ("x", Nothing)] emptyHole ] ) -unit_AddConField_partial_app :: Assertion -unit_AddConField_partial_app = - progActionTest - ( defaultProgEditableTypeDefs $ do - x <- - con cA [tEmptyHole, tEmptyHole] [con0 (vcn "True")] - sequence - [ astDef "def" x <$> tEmptyHole - ] - ) - [AddConField tT cA 2 $ TCon () (tcn "Int")] - $ expectError - (@?= ConNotSaturated cA) - -unit_AddConField_partial_app_end :: Assertion -unit_AddConField_partial_app_end = - progActionTest - ( defaultProgEditableTypeDefs $ do - x <- - con cA [tEmptyHole, tEmptyHole] [con0 (vcn "True")] - sequence - [ astDef "def" x <$> tEmptyHole - ] - ) - [AddConField tT cA 1 $ TCon () (tcn "Int")] - $ expectSuccess - $ \_ prog' -> do - td <- findTypeDef tT prog' - astTypeDefConstructors td - @?= [ ValCon cA [TCon () (tcn "Bool"), TCon () (tcn "Int"), TCon () (tcn "Bool"), TCon () (tcn "Bool")] - , ValCon cB [TApp () (TApp () (TCon () tT) (TVar () "b")) (TVar () "a"), TVar () "b"] - ] - def <- findDef (gvn "def") prog' - forgetMetadata (astDefExpr def) - @?= forgetMetadata - ( create' $ - con cA [tEmptyHole, tEmptyHole] [con0 (vcn "True"), emptyHole] - ) - unit_AddConField_case_ann :: Assertion unit_AddConField_case_ann = progActionTest @@ -1448,27 +1406,18 @@ unit_cross_module_actions = , ConstructVar (GlobalVarRef $ qualifyM "foo") , Move Parent , Move Child2 - , ConstructApp - , Move Child1 - , constructCon (qualifyM "C") - , Move Parent - , Move Child2 - , constructCon cZero + , constructSaturatedCon (qualifyM "C") + , Move $ ConChild 0 + , constructSaturatedCon 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 "a38") + , constructSaturatedCon (qualifyM "C") + , Move $ ConChild 0 + , constructSaturatedCon cSucc + , Move $ ConChild 0 + , ConstructVar (LocalVarRef "a37") ] ] handleAndTC [RenameDef (qualifyM "foo") "bar"] @@ -1504,7 +1453,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/Typecheck.hs b/primer/test/Tests/Typecheck.hs index ae9edbec6..169d81919 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -154,15 +154,17 @@ unit_const = unit_true :: Assertion unit_true = expectTyped $ con0 cTrue --- An empty hole accepts under-saturated constructors +-- An empty hole rejects under-saturated constructors unit_unsat_con_hole_1 :: Assertion -unit_unsat_con_hole_1 = expectTyped $ con cSucc [] [] `ann` tEmptyHole +unit_unsat_con_hole_1 = + (con 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` const (TypeDoesNotMatchArrow $ TCon () tNat) + `expectFailsWith` \_ -> UnsaturatedConstructor cSucc -- A hole-headed TApp accepts saturated constructors unit_con_hole_app_type_1 :: Assertion @@ -221,9 +223,16 @@ unit_inc :: Assertion unit_inc = expectTyped $ ann - (lam "n" (app (con0 cSucc) (lvar "n"))) + (lam "n" (con cSucc [] [lvar "n"])) (tfun (tcon tNat) (tcon tNat)) +unit_inc_unsat :: Assertion +unit_inc_unsat = + ann + (lam "n" (app (con0 cSucc) (lvar "n"))) + (tfun (tcon tNat) (tcon tNat)) + `expectFailsWith` const (UnsaturatedConstructor cSucc) + unit_compose_nat :: Assertion unit_compose_nat = expectTyped $ 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 82856f700..1489cd997 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment @@ -253,7 +253,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -275,7 +276,6 @@ Output , free = FreeNone } ) - , NoInput MakeCase , Input MakeInt ( Options { opts = [] @@ -328,7 +328,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -350,7 +351,6 @@ Output , free = FreeNone } ) - , NoInput MakeCase , Input MakeInt ( Options { opts = [] @@ -554,6 +554,69 @@ Output , NoInput DeleteExpr ] ) + , + ( 26 + , + [ 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 + ] + ) + , + ( 27 + , + [ 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 + ] + ) , ( 28 , @@ -576,12 +639,13 @@ Output , free = FreeVarName } ) + , NoInput MakeCase , NoInput Raise , NoInput DeleteExpr ] ) , - ( 29 + ( 31 , [ Input MakeLam ( Options @@ -608,7 +672,33 @@ Output ] ) , - ( 30 + ( 41 + , + [ 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 + ] + ) + , + ( 42 , [ Input MakeLam ( Options @@ -635,7 +725,34 @@ Output ] ) , - ( 31 + ( 43 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeCase + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 44 , [ Input RenamePattern ( Options @@ -663,7 +780,7 @@ Output ] ) , - ( 32 + ( 45 , [ Input MakeLam ( Options @@ -690,7 +807,7 @@ Output ] ) , - ( 33 + ( 46 , [ Input MakeLam ( Options @@ -717,7 +834,7 @@ Output ] ) , - ( 34 + ( 47 , [ Input MakeLam ( Options @@ -761,7 +878,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -783,7 +901,6 @@ Output , free = FreeNone } ) - , NoInput MakeCase , Input MakeInt ( Options { opts = [] @@ -800,7 +917,7 @@ Output ] ) , - ( 35 + ( 48 , [ Input MakeLam ( Options @@ -827,7 +944,7 @@ Output ] ) , - ( 36 + ( 49 , [ Input MakeLam ( Options @@ -922,24 +1039,64 @@ Output ] ) , - ( 26 + ( 29 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 27 + ( 30 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 37 + ( 32 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 33 , [ NoInput MakeFun , NoInput AddInput + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 34 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 35 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 36 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 37 + , + [ NoInput MakeFun + , NoInput Raise , NoInput DeleteType ] ) @@ -961,6 +1118,21 @@ Output ) , ( 40 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 50 + , + [ NoInput MakeFun + , NoInput AddInput + , NoInput DeleteType + ] + ) + , + ( 51 , [ NoInput MakeFun , NoInput Raise @@ -968,7 +1140,7 @@ Output ] ) , - ( 41 + ( 52 , [ NoInput MakeFun , NoInput Raise @@ -976,7 +1148,7 @@ Output ] ) , - ( 42 + ( 53 , [ NoInput MakeFun , NoInput Raise @@ -984,7 +1156,7 @@ Output ] ) , - ( 43 + ( 54 , [ NoInput MakeFun , NoInput Raise @@ -992,7 +1164,23 @@ Output ] ) , - ( 44 + ( 55 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 56 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 57 , [ 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 7e5455083..1a69e1d3f 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment @@ -58,15 +58,15 @@ Output , [] ) , - ( 28 + ( 26 , [] ) , - ( 29 + ( 27 , [] ) , - ( 30 + ( 28 , [] ) , @@ -74,23 +74,39 @@ Output , [] ) , - ( 32 + ( 41 , [] ) , - ( 33 + ( 42 , [] ) , - ( 34 + ( 43 , [] ) , - ( 35 + ( 44 , [] ) , - ( 36 + ( 45 + , [] + ) + , + ( 46 + , [] + ) + , + ( 47 + , [] + ) + , + ( 48 + , [] + ) + , + ( 49 , [] ) , @@ -106,11 +122,31 @@ Output , [] ) , - ( 26 + ( 29 , [] ) , - ( 27 + ( 30 + , [] + ) + , + ( 32 + , [] + ) + , + ( 33 + , [] + ) + , + ( 34 + , [] + ) + , + ( 35 + , [] + ) + , + ( 36 , [] ) , @@ -130,19 +166,35 @@ Output , [] ) , - ( 41 + ( 50 , [] ) , - ( 42 + ( 51 , [] ) , - ( 43 + ( 52 , [] ) , - ( 44 + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 , [] ) ] 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 4a9d23f02..4de57b843 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment @@ -390,7 +390,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -452,54 +453,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 = @@ -630,7 +583,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -692,54 +646,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 = @@ -1162,13 +1068,13 @@ Output , free = FreeVarName } ) - , NoInput MakeAnn + , NoInput RemoveAnn , NoInput Raise , NoInput DeleteExpr ] ) , - ( 28 + ( 26 , [ Input MakeLam ( Options @@ -1211,33 +1117,47 @@ 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 ] ) , - ( 29 + ( 27 , [ Input MakeLam ( Options { opts = [ Option - { option = "z" - , context = Nothing - } - , Option - { option = "x1" + { option = "p" , context = Nothing } , Option - { option = "y1" + { option = "q" , context = Nothing } ] , free = FreeVarName } ) - , NoInput MakeCase , NoInput MakeApp , NoInput MakeAPP , Input MakeLAM @@ -1260,12 +1180,27 @@ Output } ) , NoInput MakeAnn + , Input RenameLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) , NoInput Raise , NoInput DeleteExpr ] ) , - ( 30 + ( 28 , [ Input MakeLam ( Options @@ -1316,33 +1251,54 @@ Output , ( 31 , - [ Input RenamePattern + [ Input MakeLam ( Options { opts = [ Option - { option = "j" + { option = "z" , context = Nothing } , Option - { option = "m" + { option = "x1" , context = Nothing } , Option - { option = "i1" + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeCase + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" , context = Nothing } , Option - { option = "n1" + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" , context = Nothing } ] , free = FreeVarName } ) + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr ] ) , - ( 32 + ( 41 , [ Input MakeLam ( Options @@ -1363,7 +1319,6 @@ Output , free = FreeVarName } ) - , NoInput MakeCase , NoInput MakeApp , NoInput MakeAPP , Input MakeLAM @@ -1391,7 +1346,7 @@ Output ] ) , - ( 33 + ( 42 , [ Input MakeLam ( Options @@ -1440,7 +1395,7 @@ Output ] ) , - ( 34 + ( 43 , [ Input MakeLam ( Options @@ -1461,91 +1416,204 @@ Output , free = FreeVarName } ) - , Input MakeVar + , NoInput MakeCase + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM ( Options { opts = [ Option - { option = "x" - , context = Nothing - } - , Option - { option = "y" + { option = "α" , context = Nothing } , Option - { option = "i" + { option = "γ" , context = Nothing } , Option - { option = "n" + { option = "β1" , context = Nothing } - , Option - { option = "comprehensive" - , context = Just - ( "M" :| [] ) - } ] - , free = FreeNone + , free = FreeVarName } ) - , Input MakeCon + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 44 + , + [ Input RenamePattern ( Options { opts = [ Option - { option = "True" - , context = Just - ( "Builtins" :| [] ) + { option = "j" + , context = Nothing } , Option - { option = "False" - , context = Just - ( "Builtins" :| [] ) + { option = "m" + , context = Nothing } , Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) + { option = "i1" + , context = Nothing } , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) + { option = "n1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + ] + ) + , + ( 45 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing } , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) + { option = "x1" + , context = Nothing } , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeCase + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing } , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) + { option = "γ" + , context = Nothing } , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 46 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing } , Option - { option = "Zero" - , context = Just - ( "Builtins" :| [] ) + { option = "x1" + , context = Nothing } , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeCase + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing } , Option - { option = "MakePair" + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 47 + , + [ 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 = "i" + , context = Nothing + } + , Option + { option = "n" + , context = Nothing + } + , Option + { option = "comprehensive" , context = Just - ( "Builtins" :| [] ) + ( "M" :| [] ) } ] , free = FreeNone @@ -1556,6 +1624,16 @@ Output ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -1585,6 +1663,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just @@ -1688,7 +1771,7 @@ Output ] ) , - ( 35 + ( 48 , [ Input MakeLam ( Options @@ -1737,7 +1820,7 @@ Output ] ) , - ( 36 + ( 49 , [ Input MakeLam ( Options @@ -1920,7 +2003,7 @@ Output ] ) , - ( 26 + ( 29 , [ NoInput MakeFun , NoInput MakeTApp @@ -1947,7 +2030,7 @@ Output ] ) , - ( 27 + ( 30 , [ NoInput MakeFun , NoInput MakeTApp @@ -1973,8 +2056,278 @@ Output , NoInput DeleteType ] ) + , + ( 32 + , + [ 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 + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput DeleteType + ] + ) + , + ( 33 + , + [ 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 + ] + ) + , + ( 34 + , + [ 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 + ] + ) + , + ( 35 + , + [ 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 + ] + ) + , + ( 36 + , + [ 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 + ] + ) , ( 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 DeleteType + ] + ) + , + ( 50 , [ NoInput MakeFun , NoInput AddInput @@ -2002,7 +2355,7 @@ Output ] ) , - ( 38 + ( 51 , [ NoInput MakeFun , NoInput MakeTApp @@ -2030,7 +2383,7 @@ Output ] ) , - ( 39 + ( 52 , [ NoInput MakeFun , NoInput MakeTApp @@ -2077,7 +2430,7 @@ Output ] ) , - ( 40 + ( 53 , [ NoInput MakeFun , NoInput MakeTApp @@ -2105,7 +2458,7 @@ Output ] ) , - ( 41 + ( 54 , [ NoInput MakeFun , NoInput MakeTApp @@ -2133,7 +2486,7 @@ Output ] ) , - ( 42 + ( 55 , [ NoInput MakeFun , NoInput MakeTApp @@ -2161,7 +2514,7 @@ Output ] ) , - ( 43 + ( 56 , [ NoInput MakeFun , NoInput MakeTApp @@ -2189,7 +2542,7 @@ Output ] ) , - ( 44 + ( 57 , [ 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 7e5455083..1a69e1d3f 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment @@ -58,15 +58,15 @@ Output , [] ) , - ( 28 + ( 26 , [] ) , - ( 29 + ( 27 , [] ) , - ( 30 + ( 28 , [] ) , @@ -74,23 +74,39 @@ Output , [] ) , - ( 32 + ( 41 , [] ) , - ( 33 + ( 42 , [] ) , - ( 34 + ( 43 , [] ) , - ( 35 + ( 44 , [] ) , - ( 36 + ( 45 + , [] + ) + , + ( 46 + , [] + ) + , + ( 47 + , [] + ) + , + ( 48 + , [] + ) + , + ( 49 , [] ) , @@ -106,11 +122,31 @@ Output , [] ) , - ( 26 + ( 29 , [] ) , - ( 27 + ( 30 + , [] + ) + , + ( 32 + , [] + ) + , + ( 33 + , [] + ) + , + ( 34 + , [] + ) + , + ( 35 + , [] + ) + , + ( 36 , [] ) , @@ -130,19 +166,35 @@ Output , [] ) , - ( 41 + ( 50 , [] ) , - ( 42 + ( 51 , [] ) , - ( 43 + ( 52 , [] ) , - ( 44 + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 , [] ) ] 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 016dba77e..a97cc4bec 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment @@ -264,7 +264,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -326,54 +327,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 = @@ -483,7 +436,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -545,54 +499,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 = @@ -854,6 +760,71 @@ Output , NoInput DeleteExpr ] ) + , + ( 26 + , + [ 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 + ] + ) + , + ( 27 + , + [ 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 + ] + ) , ( 28 , @@ -876,13 +847,14 @@ Output , free = FreeVarName } ) + , NoInput MakeCase , NoInput MakeApp , NoInput Raise , NoInput DeleteExpr ] ) , - ( 29 + ( 31 , [ Input MakeLam ( Options @@ -910,7 +882,34 @@ Output ] ) , - ( 30 + ( 41 + , + [ 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 + ] + ) + , + ( 42 , [ Input MakeLam ( Options @@ -938,7 +937,35 @@ Output ] ) , - ( 31 + ( 43 + , + [ 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 Raise + , NoInput DeleteExpr + ] + ) + , + ( 44 , [ Input RenamePattern ( Options @@ -966,7 +993,7 @@ Output ] ) , - ( 32 + ( 45 , [ Input MakeLam ( Options @@ -994,7 +1021,7 @@ Output ] ) , - ( 33 + ( 46 , [ Input MakeLam ( Options @@ -1022,7 +1049,7 @@ Output ] ) , - ( 34 + ( 47 , [ Input MakeLam ( Options @@ -1071,7 +1098,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -1133,54 +1161,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 = @@ -1249,7 +1229,7 @@ Output ] ) , - ( 35 + ( 48 , [ Input MakeLam ( Options @@ -1277,7 +1257,7 @@ Output ] ) , - ( 36 + ( 49 , [ Input MakeLam ( Options @@ -1373,24 +1353,64 @@ Output ] ) , - ( 26 + ( 29 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 27 + ( 30 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 37 + ( 32 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 33 , [ NoInput MakeFun , NoInput AddInput + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 34 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 35 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 36 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 37 + , + [ NoInput MakeFun + , NoInput Raise , NoInput DeleteType ] ) @@ -1412,6 +1432,21 @@ Output ) , ( 40 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 50 + , + [ NoInput MakeFun + , NoInput AddInput + , NoInput DeleteType + ] + ) + , + ( 51 , [ NoInput MakeFun , NoInput Raise @@ -1419,7 +1454,7 @@ Output ] ) , - ( 41 + ( 52 , [ NoInput MakeFun , NoInput Raise @@ -1427,7 +1462,7 @@ Output ] ) , - ( 42 + ( 53 , [ NoInput MakeFun , NoInput Raise @@ -1435,7 +1470,7 @@ Output ] ) , - ( 43 + ( 54 , [ NoInput MakeFun , NoInput Raise @@ -1443,7 +1478,23 @@ Output ] ) , - ( 44 + ( 55 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 56 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 57 , [ 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 7e5455083..1a69e1d3f 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment @@ -58,15 +58,15 @@ Output , [] ) , - ( 28 + ( 26 , [] ) , - ( 29 + ( 27 , [] ) , - ( 30 + ( 28 , [] ) , @@ -74,23 +74,39 @@ Output , [] ) , - ( 32 + ( 41 , [] ) , - ( 33 + ( 42 , [] ) , - ( 34 + ( 43 , [] ) , - ( 35 + ( 44 , [] ) , - ( 36 + ( 45 + , [] + ) + , + ( 46 + , [] + ) + , + ( 47 + , [] + ) + , + ( 48 + , [] + ) + , + ( 49 , [] ) , @@ -106,11 +122,31 @@ Output , [] ) , - ( 26 + ( 29 , [] ) , - ( 27 + ( 30 + , [] + ) + , + ( 32 + , [] + ) + , + ( 33 + , [] + ) + , + ( 34 + , [] + ) + , + ( 35 + , [] + ) + , + ( 36 , [] ) , @@ -130,19 +166,35 @@ Output , [] ) , - ( 41 + ( 50 , [] ) , - ( 42 + ( 51 , [] ) , - ( 43 + ( 52 , [] ) , - ( 44 + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 , [] ) ] diff --git a/primer/testlib/Primer/Test/Util.hs b/primer/testlib/Primer/Test/Util.hs index 99ecb7ccf..003d90711 100644 --- a/primer/testlib/Primer/Test/Util.hs +++ b/primer/testlib/Primer/Test/Util.hs @@ -5,7 +5,6 @@ module Primer.Test.Util ( assertException, primDefs, constructTCon, - constructCon, constructRefinedCon, constructSaturatedCon, tcn, @@ -41,7 +40,7 @@ import Primer.API ( runPrimerM, ) import Primer.Action ( - Action (ConstructCon, ConstructRefinedCon, ConstructSaturatedCon, ConstructTCon), + Action (ConstructRefinedCon, ConstructSaturatedCon, ConstructTCon), ) import Primer.Core ( Expr', @@ -88,9 +87,6 @@ primDefs = Map.mapKeys primitive $ moduleDefs primitiveModule constructTCon :: TyConName -> Action constructTCon = ConstructTCon . toQualText -constructCon :: ValConName -> Action -constructCon = ConstructCon . toQualText - constructSaturatedCon :: ValConName -> Action constructSaturatedCon = ConstructSaturatedCon . toQualText