introduce let in core (not used yet)

5 files changed, 51 insertions, 25 deletions

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index 273791a7..0a221d2c 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -148,6 +148,7 @@ data Exp
     | Pi_    !MaxDB Visibility Exp Exp
     | Neut   Neutral
     | RHS    Exp{-always in hnf-}
+    | Let_   !MaxDB ExpType Exp
 
 data Neutral
     = Var_        !Int{-De Bruijn index-}
@@ -155,7 +156,6 @@ data Neutral
     | CaseFun__   !MaxDB CaseFunName   [Exp] Neutral
     | TyCaseFun__ !MaxDB TyCaseFunName [Exp] Neutral
     | Fun_        !MaxDB FunName [Exp]{-given parameters, reversed-} Exp{-unfolded expression, in hnf-}
---    | Let_        !MaxDB
 
 -------------------------------------------------------------------------------- auxiliary functions and patterns
 
@@ -163,7 +163,10 @@ type Type = Exp
 
 data ExpType = ET {expr :: Exp, ty :: Type}
     deriving (Eq)
-
+{-
+pattern ET a b <- ET_ a b
+  where ET a b =  ET_ a (hnf b)
+-}
 instance Rearrange ExpType where
     rearrange l f (ET e t) = ET (rearrange l f e) (rearrange l f t)
 
@@ -201,6 +204,13 @@ pattern Lam y               <- Lam_ _ y
   where Lam y               =  Lam_ (lowerDB (maxDB_ y)) y
 pattern Pi v x y            <- Pi_ _ v x y
   where Pi v x y            =  Pi_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y
+pattern Let x y             <- Let_ _ x y
+  where Let x y             =  Let_ (maxDB_ x <> lowerDB (maxDB_ y)) x y
+
+pattern SubstLet x <- (substLet -> Just x)
+
+substLet (Let x y) = Just $ subst 0 (expr x) y
+substLet _ = Nothing
 
 pattern CaseFun a b c   = Neut (CaseFun_ a b c)
 pattern TyCaseFun a b c = Neut (TyCaseFun_ a b c)
@@ -306,9 +316,14 @@ mkFun :: FunName -> [Exp] -> Exp -> Exp
 mkFun f xs e = mkFun_ (foldMap maxDB_ xs) f xs e
 
 pattern ReducedN y <- Fun f _ (RHS y)
-pattern Reduced y <- Neut (ReducedN y)
+pattern Reduced y <- (reduce -> Just y)
+
+-- TODO: too much hnf call
+reduce (Neut (ReducedN y)) = Just $ hnf y
+reduce (SubstLet x) = Just $ hnf x
+reduce _ = Nothing
 
-hnf (Reduced y) = y
+hnf (reduce -> Just y) = y
 hnf a = a
 
 outputType = tTyCon0 FOutput $ error "cs 9"
@@ -385,6 +400,7 @@ instance Subst Exp Exp where
             Con_ md s n as  -> Con_ (md <> upDB i dx) s n $ f i <$> as
             Pi_ md h a b    -> Pi_ (md <> upDB i dx) h (f i a) (f (i+1) b)
             TyCon_ md s as  -> TyCon_ (md <> upDB i dx) s $ f i <$> as
+            Let_ md a b     -> Let_ (md <> upDB i dx) (subst_ i dx x a) (f (i+1) b)
             RHS a           -> RHS $ hnf $ f i a
 
 instance Rearrange Exp where
@@ -396,6 +412,7 @@ instance Rearrange Exp where
             Con_ md s pn as -> Con_ (upDB_ g i md) s pn $ map (f i) as
             TyCon_ md s as  -> TyCon_ (upDB_ g i md) s $ map (f i) as
             Neut x          -> Neut $ rearrange i g x
+            Let x y         -> Let (rearrange i g x) (rearrange (i+1) g y)
             RHS x           -> RHS $ rearrange i g x
 
 instance Rearrange Neutral where
@@ -421,6 +438,7 @@ instance Up Exp where
         TType_ _ -> mempty
         ELit{} -> mempty
         Neut x -> foldVar f i x
+        Let x y -> foldVar f i x <> foldVar f (i+1) y
         RHS x -> foldVar f i x
 
 instance Up Neutral where
@@ -445,6 +463,7 @@ instance HasMaxDB Exp where
         Pi_ c _ _ _ -> c
         Con_ c _ _ _ -> c
         TyCon_ c _ _ -> c
+        Let_ c _ _ -> c
 
         TType_ _ -> mempty
         ELit{} -> mempty
@@ -481,6 +500,7 @@ instance ClosedExp Exp where
         e@TType_{} -> e
         e@ELit{} -> e
         Neut a -> Neut $ closedExp a
+        Let a b -> Let_ mempty a b
         RHS a -> RHS (closedExp a)
 
 instance ClosedExp Neutral where
@@ -519,6 +539,7 @@ instance MkDoc Exp where
         TType           -> text "Type"
         ELit l          -> pShow l
         Neut x          -> mkDoc pr x
+        Let a b         -> shLet_ (pShow a) (pShow b)
         RHS x           -> text "_rhs" `DApp` mkDoc pr x
 
 showNth n = show n ++ f (n `div` 10 `mod` 10) (n `mod` 10)
@@ -719,6 +740,7 @@ app_ :: Exp -> Exp -> Exp
 app_ (Lam x) a = subst 0 a x
 app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a])
 app_ (TyCon s xs) a = TyCon s (xs ++ [a])
+app_ (SubstLet f) a = app_ f a
 app_ (Neut f) a = neutApp f a
   where
     neutApp (ReducedN x) a = app_ x a    -- ???
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index d47726d0..325338bf 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -533,22 +533,22 @@ shLet_ a b = DFreshName True $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b
 -------------------------------------------------------------------------------- statement
 
 data Stmt
-    = Let SIName (Maybe SExp) SExp
+    = StLet SIName (Maybe SExp) SExp
     | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} [(SIName, SExp)]{-constructor names and types-}
     | PrecDef SIName Fixity
 
-pattern Primitive n t = Let n (Just t) (SBuiltin "undefined")
+pattern Primitive n t = StLet n (Just t) (SBuiltin "undefined")
 
 instance PShow Stmt where
     pShow stmt = vcat . map DResetFreshNames $ case stmt of
         Primitive n t -> pure $ shAnn (pShow n) (pShow t)
-        Let n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)]
+        StLet n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)]
         Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl DApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) </> "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs])
         PrecDef n i -> pure $ pShow i <+> text (sName n) --DOp0 (sName n) i
 
 instance DeBruijnify SIName Stmt where
     deBruijnify_ k v = \case
-        Let sn mt e -> Let sn (deBruijnify_ k v <$> mt) (deBruijnify_ k v e)
+        StLet sn mt e -> StLet sn (deBruijnify_ k v <$> mt) (deBruijnify_ k v e)
         x -> error $ "deBruijnify @ " ++ ppShow x
 
 -------------------------------------------------------------------------------- statement with dependencies
@@ -570,7 +570,7 @@ sortDefs xs = map snValue <$> scc snId snChildren snRevChildren nodes
           where
             need = Set.toList $ case s of
                 PrecDef{} -> mempty
-                Let _ mt e -> foldMap names mt <> names e
+                StLet _ mt e -> foldMap names mt <> names e
                 Data _ ps t cs -> foldMap (names . snd) ps <> names t <> foldMap (names . snd) cs
 
             names = foldName Set.singleton
@@ -581,7 +581,7 @@ sortDefs xs = map snValue <$> scc snId snChildren snRevChildren nodes
       where
         def = \case
             PrecDef{} -> mempty
-            Let n _ _ -> [n]
+            StLet n _ _ -> [n]
             Data n _ _ cs -> n: map fst cs
 
 -------------------------------------------------------------------------------- module
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 3b8bdd5a..38269b0e 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -227,6 +227,9 @@ inferN e s = do
 
 substTo i x = subst i x . up1_ (i+1)
 
+mkLet x xt y = subst 0 x y
+--mkLet x xt (ET y yt) = ET (Let (ET x xt) y) yt
+
 inferN_ :: forall m . Monad m => (forall a . String -> String -> IM m a -> IM m a) -> Env -> SExp2 -> IM m ExpType'
 inferN_ tellTrace = infer  where
 
@@ -243,7 +246,7 @@ inferN_ tellTrace = infer  where
         SApp_ si h a b  -> infer (EApp1 (si `validate` [sourceInfo a, sourceInfo b]) h te b) a
         SBind_ si h _ a b -> infer ((if h /= BMeta then CheckType_ (sourceInfo exp) TType else id) $ EBind1 si h te $ (if isPi h then TyType else id) b) a
 
-    checkN :: Env -> SExp2 -> Type -> IM m ExpType'
+    checkN :: Env -> SExp2 -> Type{-hnf-} -> IM m ExpType'
     checkN te x t = tellTrace "check" (showEnvSExpType te x t) $ checkN_ te x t
 
     checkN_ te (Parens e) t = checkN_ te e t
@@ -269,10 +272,10 @@ inferN_ tellTrace = infer  where
         | SLam h a b <- e, Pi h' x y <- t, h == h'  = do
 --            tellType e t
             let same = checkSame te a x
-            if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ ppShow a ++ "\nwith\n" ++ showEnvExp te (ET x TType)
+            if same then checkN (EBind2 (BLam h) x te) b $ hnf y else error $ "checkSame:\n" ++ ppShow a ++ "\nwith\n" ++ showEnvExp te (ET x TType)
         | Pi Hidden a b <- t = do
             bb <- notHiddenLam e
-            if bb then checkN (EBind2 (BLam Hidden) a te) (up1 e) b
+            if bb then checkN (EBind2 (BLam Hidden) a te) (up1 e) $ hnf b
                  else infer (CheckType_ (sourceInfo e) t te) e
         | otherwise = infer (CheckType_ (sourceInfo e) t te) e
       where
@@ -313,15 +316,15 @@ inferN_ tellTrace = infer  where
                 _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr_ TType t y) $ EApp1 si h te b) $ up 1 eet
             | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet
         EApp1 si h te b
-            | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b x
+            | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b $ hnf x
             | Pi Hidden x y  <- et, h == Visible -> focus_ (EApp1 mempty Hidden env $ Wildcard $ Wildcard SType) eet  --  e b --> e _ b
 --            | CheckType (Pi Hidden _ _) te' <- te -> error "ok"
 --            | CheckAppType Hidden _ te' _ <- te -> error "ok"
             | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (up 3 b)
           where
             cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr_ TType x y)
-        ELet2 ln (ET x{-let-} xt) te -> focus_ te $ subst 0 (mkELet ln x xt te){-let-} eet{-in-}
-        CheckIType x te -> checkN te x e
+        ELet2 ln (ET x{-let-} xt) te -> focus_ te $ mkLet (mkELet ln x xt te){-let-} xt eet{-in-}
+        CheckIType x te -> checkN te x $ hnf e
         CheckType_ si t te
             | hArgs et > hArgs t
                             -> focus_ (EApp1 mempty Hidden (CheckType_ si t te) $ Wildcard $ Wildcard SType) eet
@@ -461,6 +464,7 @@ recheck' sn e (ET x xt) = ET (recheck_ "main" (checkEnv e) (ET x xt)) xt
         ET (CaseFun s@(CaseFunName _ t pars) as n) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
         ET (TyCaseFun s [m, t, f] n) zt  -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f]
         ET (Neut (Fun_ md f a x)) zt -> checkApps ("lab-" ++ show f ++ ppShow a ++ "\n" ++ ppShow (nType f)) [] zt (\xs -> Neut $ Fun_ md f (reverse xs) x) te (nType f) $ reverse a   -- TODO: recheck x
+        ET (Let (ET x xt) y) zt -> Let (recheck'' "let" te $ ET x xt) $ recheck_ "let_in" te $ ET y (Pi Visible xt $ up1 zt)  -- TODO
         ET (RHS x) zt -> RHS $ recheck_ msg te (ET x zt)
       where
         checkApps s acc zt f _ t []
@@ -485,7 +489,7 @@ handleStmt = \case
         t <- inferType n $ trSExp' t_
         tellType (sourceInfo n) t
         addToEnv n $ flip ET t $ lamify t $ DFun (mkFName n) t
-  Let n mt t_ -> do
+  StLet n mt t_ -> do
         let t__ = maybe id (flip SAnn) mt t_
         ET x t <- inferTerm n $ trSExp' $ addFix n t__
         tellType (sourceInfo n) t
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index f4ea8489..1d5139b8 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -131,7 +131,7 @@ mkDesugarInfo ss = DesugarInfo
     , consMap = Map.fromList $
         [(sName cn, Left ((CaseName $ sName t, pars ty), second pars <$> cs)) | Data t ps ty cs <- ss, (cn, ct) <- cs]
      ++ [(sName t, Right $ pars $ UncurryS ps ty) | Data t ps ty _ <- ss]
---     ++ [(t, Right $ length xs) | Let (_, t) _ (Just ty) xs _ <- ss]
+--     ++ [(t, Right $ length xs) | StLet (_, t) _ (Just ty) xs _ <- ss]
      ++ [("'Type", Right 0)]
     , definedSet = Set.singleton "'Type" <> foldMap defined ss
     }
@@ -139,7 +139,7 @@ mkDesugarInfo ss = DesugarInfo
     pars (UncurryS l _) = length $ filter ((== Visible) . fst) l -- todo
 
     defined = \case
-        Let sn _ _ -> Set.singleton $ sName sn
+        StLet sn _ _ -> Set.singleton $ sName sn
         Data sn _ _ cs -> Set.fromList $ sName sn: map (sName . fst) cs
         PrecDef{} -> mempty
 
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs
index 42f02b07..1ce2beb6 100644
--- a/src/LambdaCube/Compiler/Statements.hs
+++ b/src/LambdaCube/Compiler/Statements.hs
@@ -49,7 +49,7 @@ mkLets_ mkLet = mkLets' mkLet . concatMap desugarMutual . sortDefs
 
 mkLets' mkLet = f where
     f [] e = e
-    f (Let n mt x: ds) e = mkLet n (maybe id (flip SAnn) mt (addFix n x)) (deBruijnify [n] $ f ds e)
+    f (StLet n mt x: ds) e = mkLet n (maybe id (flip SAnn) mt (addFix n x)) (deBruijnify [n] $ f ds e)
     f (PrecDef{}: ds) e = f ds e
     f (x: ds) e = error $ "mkLets: " ++ ppShow x
 
@@ -57,7 +57,7 @@ addFix n x
     | usedS n x = SBuiltin "primFix" `SAppV` SLamV (deBruijnify [n] x)
     | otherwise = x
 
-addFix' (Let n nt nd) = Let n nt $ addFix n nd
+addFix' (StLet n nt nd) = StLet n nt $ addFix n nd
 addFix' x = x
 
 type DefinedSet = Set.Set SName
@@ -97,7 +97,7 @@ compileStmt compilegt ds = \case
 --            , let ts = fst $ getParamsS $ up1 t
             , let as = [ funAlt m p $ noGuards {- -$ SLam Hidden (Wildcard SType) $ up1 -} $ SLet m' e $ sVar "cst" 0
                       | Instance n' i cstrs alts <- ds, n' == n
-                      , Let m' ~Nothing e <- alts, m' == m
+                      , StLet m' ~Nothing e <- alts, m' == m
                       , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVarSimp $ dummyName "cst2")]
         --              , let ic = patVars i
                       ]
@@ -113,7 +113,7 @@ compileStmt compilegt ds = \case
           | n `elem` [n' | TypeFamily n' _ <- ds] -> return []
           | otherwise -> do
             cf <- compilegt (SIName_ (mconcat [sourceInfo n | FunAlt n _ _ <- fs]) (nameFixity n) $ sName n) vs [gt | FunAlt _ _ gt <- fs]
-            return [Let n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) cf]
+            return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) cf]
         fs -> fail $ "different number of arguments of " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd . head <$> fs)
     [Stmt x] -> return [x]
   where
@@ -134,7 +134,7 @@ desugarValueDef p e = sequence
     dns = reverse $ getPVars p
     n = mangleNames dns
 
-getLet (Let x Nothing (SRHS dx)) = Just (x, dx)
+getLet (StLet x Nothing (SRHS dx)) = Just (x, dx)
 getLet _ = Nothing
 
 fst' (x, _) = x -- TODO
@@ -144,7 +144,7 @@ desugarMutual [x] = [x]
 desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do
     ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy)
     return $
-        Let xy Nothing (addFix xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss
+        StLet xy Nothing (addFix xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss
   where
     xy = mangleNames ns
 desugarMutual xs = error "desugarMutual"