refactoring

3 files changed, 58 insertions, 51 deletions

diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 0d1557c3..6fe8992f 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -910,9 +910,10 @@ instance Up ExpTV where
     up_ n i (ExpTV x xt vs) = error "up @ExpTV" --ExpTV (up_ n i x) (up_ n i xt) (up_ n i <$> vs)
     used i (ExpTV x xt vs) = used i x || used i xt -- -|| any (used i) vs{-?-}
     fold = error "fold @ExpTV"
-    maxDB_ (ExpTV a b cs) = maxDB_ a <> maxDB_ b -- <> foldMap maxDB_ cs{-?-}
     closedExp (ExpTV a b cs) = ExpTV (closedExp a) (closedExp b) cs
 
+--    maxDB_ (ExpTV a b cs) = maxDB_ a <> maxDB_ b -- <> foldMap maxDB_ cs{-?-}
+
 instance PShow ExpTV where
     pShowPrec p (ExpTV x t _) = pShowPrec p (x, t)
 
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index aba0f74a..9cac1299 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -15,13 +15,13 @@
 {-# OPTIONS_GHC -fno-warn-unused-binds #-}  -- TODO: remove
 -- {-# OPTIONS_GHC -O0 #-}
 module LambdaCube.Compiler.Infer
-    ( Binder (..), SName, Lit(..), Visibility(..)
+    ( SName, Lit(..), Visibility(..)
     , Exp (..), Neutral (..), ExpType, GlobalEnv
     , pattern Var, pattern CaseFun, pattern TyCaseFun, pattern App_, app_
     , pattern Con, pattern TyCon, pattern Pi, pattern Lam, pattern Fun, pattern ELit, pattern Func, pattern LabelEnd, pattern FL, pattern UFL, unFunc_
     , outputType, boolType, trueExp
     , down, Subst (..), free, subst
-    , initEnv, Env(..), pattern EBind2
+    , initEnv, Env(..)
     , SI(..), Range(..) -- todo: remove
     , Info(..), Infos, listAllInfos, listTypeInfos, listTraceInfos
     , inference, IM
@@ -113,13 +113,6 @@ data FName
     | FVecS
     | FEmpty
     | FHList
-    | FEq
-    | FOrd
-    | FNum
-    | FSigned
-    | FComponent
-    | FIntegral
-    | FFloating
     | FOutput
     | FType
     | FHCons
@@ -135,6 +128,14 @@ data FName
     | FNil
     | FCons
     | FSplit
+    -- todo: elim
+    | FEq
+    | FOrd
+    | FNum
+    | FSigned
+    | FComponent
+    | FIntegral
+    | FFloating
     deriving (Eq, Ord)
 
 cFName (RangeSI (Range fn p _), s) = fromMaybe (CFName (hashPos fn p) $ SData s) $ lookup s fntable
@@ -413,6 +414,16 @@ instance Up Exp where
         ELit{} -> mempty
         Neut x -> fold f i x
 
+    closedExp = \case
+        Lam_ _ c -> Lam_ mempty c
+        Pi_ _ a b c -> Pi_ mempty a (closedExp b) c
+        Con_ _ a b c -> Con_ mempty a b (closedExp <$> c)
+        TyCon_ _ a b -> TyCon_ mempty a (closedExp <$> b)
+        e@TType{} -> e
+        e@ELit{} -> e
+        Neut a -> Neut $ closedExp a
+
+instance HasMaxDB Exp where
     maxDB_ = \case
         Lam_ c _ -> c
         Pi_ c _ _ _ -> c
@@ -423,15 +434,6 @@ instance Up Exp where
         ELit{} -> mempty
         Neut x -> maxDB_ x
 
-    closedExp = \case
-        Lam_ _ c -> Lam_ mempty c
-        Pi_ _ a b c -> Pi_ mempty a (closedExp b) c
-        Con_ _ a b c -> Con_ mempty a b (closedExp <$> c)
-        TyCon_ _ a b -> TyCon_ mempty a (closedExp <$> b)
-        e@TType{} -> e
-        e@ELit{} -> e
-        Neut a -> Neut $ closedExp a
-
 instance Subst Exp Exp where
     subst_ i0 dx x = f i0
       where
@@ -480,15 +482,6 @@ instance Up Neutral where
         LabelEnd_ x -> fold f i x
         Delta{} -> mempty
 
-    maxDB_ = \case
-        Var_ k -> varDB k
-        CaseFun__ c _ _ _ -> c
-        TyCaseFun__ c _ _ _ -> c
-        App__ c a b -> c
-        Fun_ c _ _ _ _ _ -> c
-        LabelEnd_ x -> maxDB_ x
-        Delta{} -> mempty
-
     closedExp = \case
         x@Var_{} -> error "impossible"
         CaseFun__ _ a as n -> CaseFun__ mempty a (closedExp <$> as) (closedExp n)
@@ -498,6 +491,16 @@ instance Up Neutral where
         LabelEnd_ a -> LabelEnd_ (closedExp a)
         d@Delta{} -> d
 
+instance HasMaxDB Neutral where
+    maxDB_ = \case
+        Var_ k -> varDB k
+        CaseFun__ c _ _ _ -> c
+        TyCaseFun__ c _ _ _ -> c
+        App__ c a b -> c
+        Fun_ c _ _ _ _ _ -> c
+        LabelEnd_ x -> maxDB_ x
+        Delta{} -> mempty
+
 instance (Subst x a, Subst x b) => Subst x (a, b) where
     subst_ i dx x (a, b) = (subst_ i dx x a, subst_ i dx x b)
 
@@ -702,7 +705,7 @@ instance (Subst Exp a, Up a) => Up (CEnv a) where
 
     fold _ _ _ = error "fold @(CEnv _)"
 
-    maxDB_ _ = error "maxDB_ @(CEnv _)"
+--    maxDB_ _ = error "maxDB_ @(CEnv _)"
 
 instance (Subst Exp a, Up a) => Subst Exp (CEnv a) where
     subst_ i dx x = \case
@@ -868,8 +871,8 @@ inferN_ tellTrace = infer  where
         SLit si l       -> focus_' te exp (ELit l, litType l)
         STyped si et    -> focus_' te exp et
         SGlobal (si, s) -> focus_' te exp =<< getDef te si s
-        SApp si h a b   -> infer (EApp1 (si `validate` [sourceInfo a, sourceInfo b]) h te b) a
         SLet le a b     -> infer (ELet1 le te b{-in-}) a{-let-} -- infer te SLamV b `SAppV` a)
+        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'
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 43d92f22..1c2569f7 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -14,11 +14,11 @@ module LambdaCube.Compiler.Parser
     , Module(..), Visibility(..), Binder(..), SExp'(..), Extension(..), Extensions
     , pattern SVar, pattern SType, pattern Wildcard, pattern SAppV, pattern SLamV, pattern SAnn
     , pattern SBuiltin, pattern SPi, pattern Primitive, pattern SLabelEnd, pattern SLam, pattern Parens
-    , pattern TyType, pattern Wildcard_
+    , pattern TyType, pattern Wildcard_, pattern SLet
     , debug, isPi, varDB, lowerDB, upDB, cmpDB, MaxDB(..), iterateN, traceD
     , parseLC, runDefParser
     , getParamsS, addParamsS, getApps, apps', downToS, addForalls
-    , Up (..), up1, up
+    , Up (..), up1, up, HasMaxDB (..)
     , Doc, shLam, shApp, shLet, shLet_, shAtom, shAnn, shVar, epar, showDoc, showDoc_, sExpDoc, shCstr, shTuple
     , mtrace, sortDefs
     , trSExp', usedS, substSG0, substS
@@ -91,12 +91,12 @@ instance Show Void where show _ = error "show @Void"
 instance Eq Void where _ == _ = error "(==) @Void"
 
 data SExp' a
-    = SGlobal SIName
-    | SBind SI Binder (SData SIName{-parameter's name-}) (SExp' a) (SExp' a)
-    | SApp SI Visibility (SExp' a) (SExp' a)
-    | SLet SIName (SExp' a) (SExp' a)    -- let x = e in f   -->  SLet e f{-x is Var 0-}
-    | SVar_ (SData SIName) !Int
-    | SLit SI Lit
+    = SLit   SI Lit
+    | SGlobal SIName
+    | SApp   SI Visibility (SExp' a) (SExp' a)
+    | SBind  SI Binder (SData SIName){-parameter name-} (SExp' a) (SExp' a)
+    | SVar_  (SData SIName) !Int
+    | SLet_  SI (SData SIName) (SExp' a) (SExp' a)    -- let x = e in f   -->  SLet e f{-x is Var 0-}
     | STyped SI a
   deriving (Eq, Show)
 
@@ -117,6 +117,7 @@ pattern SLam h a b <- SBind _ (BLam h) _ a b where SLam h a b = sBind (BLam h) (
 pattern Wildcard t <- SBind _ BMeta _ t (SVar _ 0) where Wildcard t = sBind BMeta (SData (debugSI "pattern Wildcard2", "pattern_wildcard_name")) t (SVar (debugSI "pattern Wildcard2", ".wc") 0)
 pattern Wildcard_ si t  <- SBind _ BMeta _ t (SVar (si, _) 0)
 pattern SLamV a         = SLam Visible (Wildcard SType) a
+pattern SLet n a b <- SLet_ _ (SData n) a b where SLet n a b = SLet_ (sourceInfo a <> sourceInfo b) (SData n) a b
 
 pattern SApp' h a b <- SApp _ h a b where SApp' h a b = sApp h a b
 pattern SAppH a b       = SApp' Hidden a b
@@ -124,15 +125,14 @@ pattern SAppV a b       = SApp' Visible a b
 pattern SAppV2 f a b    = f `SAppV` a `SAppV` b
 
 pattern SType       = SBuiltin "'Type"
+pattern SLabelEnd a = SBuiltin "labelend" `SAppV` a
+pattern Section e   = SBuiltin "^section" `SAppV` e
+pattern Parens e    = SBuiltin "parens"  `SAppV` e
 pattern SAnn a t    = SBuiltin "typeAnn" `SAppH` t `SAppV` a
 pattern TyType a    = SAnn a SType
-pattern SLabelEnd a = SBuiltin "labelend" `SAppV` a
 
 pattern SBuiltin s <- SGlobal (_, s) where SBuiltin s = SGlobal (debugSI $ "builtin " ++ s, s)
 
-pattern Section e = SBuiltin "^section"  `SAppV` e
-pattern Parens e = SBuiltin "parens"  `SAppV` e
-
 sApp v a b = SApp (sourceInfo a <> sourceInfo b) v a b
 sBind v x a b = SBind (sourceInfo a <> sourceInfo b) v x a b
 
@@ -160,7 +160,7 @@ instance SourceInfo (SExp' a) where
         SGlobal (si, _)        -> si
         SBind si _ _ e1 e2     -> si
         SApp si _ e1 e2        -> si
-        SLet _ e1 e2           -> sourceInfo e1 <> sourceInfo e2
+        SLet_ si _ e1 e2       -> si
         SVar (si, _) _         -> si
         STyped si _            -> si
         SLit si _              -> si
@@ -169,7 +169,7 @@ instance SetSourceInfo (SExp' a) where
     setSI si = \case
         SBind _ a b c d -> SBind si a b c d
         SApp _ a b c    -> SApp si a b c
-        SLet le a b     -> SLet le a b
+        SLet_ _ le a b  -> SLet_ si le a b
         SVar (_, n) i   -> SVar (si, n) i
         STyped _ t      -> STyped si t
         SGlobal (_, n)  -> SGlobal (si, n)
@@ -229,6 +229,12 @@ upDB x (MaxDB i) = MaxDB $ ad x i where
 -}
 -------------------------------------------------------------------------------- low-level toolbox
 
+class HasMaxDB a where
+    maxDB_ :: a -> MaxDB
+
+instance (HasMaxDB a, HasMaxDB b) => HasMaxDB (a, b) where
+    maxDB_ (a, b) = maxDB_ a <> maxDB_ b
+
 class Up a where
     up_ :: Int -> Int -> a -> a
     up_ n i = iterateN n $ up1_ i
@@ -240,8 +246,6 @@ class Up a where
     used :: Int -> a -> Bool
     used = (getAny .) . fold ((Any .) . (==))
 
-    maxDB_ :: a -> MaxDB
-
     closedExp :: a -> a
     closedExp a = a
 
@@ -249,7 +253,6 @@ instance (Up a, Up b) => Up (a, b) where
     up_ n i (a, b) = (up_ n i a, up_ n i b)
     used i (a, b) = used i a || used i b
     fold f i (a, b) = fold f i a <> fold f i b
-    maxDB_ (a, b) = maxDB_ a <> maxDB_ b
     closedExp (a, b) = (closedExp a, closedExp b)
 
 up n = up_ n 0
@@ -281,7 +284,7 @@ mapS' = mapS__ (\_ _ _ -> error "mapS'") (const . SGlobal)
 mapS__ hh gg f2 h = g where
     g i = \case
         SApp si v a b -> SApp si v (g i a) (g i b)
-        SLet x a b -> SLet x (g i a) (g (h i) b)
+        SLet_ si x a b -> SLet_ si x (g i a) (g (h i) b)
         SBind si k si' a b -> SBind si k si' (g i a) (g (h i) b)
         SVar sn j -> f2 sn j i
         SGlobal sn -> gg sn i
@@ -305,7 +308,7 @@ substSG0 n = substSG n 0 . up1
 instance Up Void where
     up_ n i = error "up_ @Void"
     fold _ = error "fold_ @Void"
-    maxDB_ _ = error "maxDB @Void"
+--    maxDB_ _ = error "maxDB @Void"
 
 instance Up a => Up (SExp' a) where
     up_ n = mapS' (\sn j i -> SVar sn $ if j < i then j else j+n) (+1)
@@ -313,7 +316,7 @@ instance Up a => Up (SExp' a) where
             mapS' = mapS__ (\i si x -> STyped si $ up_ n i x) (const . SGlobal)
 
     fold f = foldS (\i si x -> fold f i x) mempty $ \sn j i -> f j i
-    maxDB_ _ = error "maxDB @SExp"
+--    maxDB_ _ = error "maxDB @SExp"
 
 dbf' = dbf_ 0
 dbf_ j xs e = foldl (\e (i, sn) -> substSG sn i e) e $ zip [j..] xs
@@ -330,7 +333,7 @@ trSExp :: (a -> b) -> SExp' a -> SExp' b
 trSExp f = g where
     g = \case
         SApp si v a b -> SApp si v (g a) (g b)
-        SLet x a b -> SLet x (g a) (g b)
+        SLet_ si x a b -> SLet_ si x (g a) (g b)
         SBind si k si' a b -> SBind si k si' (g a) (g b)
         SVar sn j -> SVar sn j
         SGlobal sn -> SGlobal sn