feat!: saturated constructors

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

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,14 +78,14 @@ import Primer.TypeDef (
   ValCon (..),
   typeDefKind,
   typeDefParameters,
-  valConType,
  )
 import Primer.Typecheck (
   Cxt (),
   SmartHoles (NoSmartHoles),
   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,20 +625,20 @@ 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
     intBound = fromIntegral (maxBound :: Word64) -- arbitrary
     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

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

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
             }