better show for let expressions; fix a bug in type class desugaring

5 files changed, 13 insertions, 8 deletions

diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index 8efa8e76..ecc2c1b8 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -430,8 +430,8 @@ showLam x (DFreshName u d) = DFreshName u $ showLam (DUp 0 x) d
 showLam x (DLam xs y) = DLam (DSep (InfixR 11) x xs) y
 showLam x y = DLam x y
 
-shLet i a b = showLam (DLet ":=" (blue $ shVar i) $ DUp i a) (DUp i b)
-shLet_ a b = DFreshName True $ showLam (DLet ":=" (shVar 0) $ DUp 0 a) b
+shLet i a b = DLet' (DLet "=" (blue $ shVar i) $ DUp i a) (DUp i b)
+shLet_ a b = DFreshName True $ DLet' (DLet "=" (shVar 0) $ DUp 0 a) b
 
 -------------------------------------------------------------------------------- statement
 
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 9350f9fd..10801810 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -419,8 +419,8 @@ parseDef =
             constraints <- option [] $ try "constraint" $ getTTuple <$> setR parseTermOp <* reservedOp "=>"
             x <- upperCase
             (nps, args) <- telescopePat
-            cs <- expNS $ option [] $ reserved "where" *> identation False (deBruijnify nps <$> funAltDef (Just lhsOperator) varId)
-            pure . Instance x ({-todo-}map snd args) (deBruijnify (nps <> [x]) <$> constraints) <$> runCheck (compileStmt' cs)
+            cs <- expNS $ option [] $ reserved "where" *> identation False ({-deBruijnify nps <$> -} funAltDef (Just lhsOperator) varId)
+            pure . Instance x ({-todo-}map snd args) (deBruijnify nps <$> constraints) <$> runCheck (compileStmt' cs)
  <|> do reserved "type" *> do
             typeNS $ do
                 reserved "family" *> do
diff --git a/src/LambdaCube/Compiler/Patterns.hs b/src/LambdaCube/Compiler/Patterns.hs
index 1483450a..5fcdbc9e 100644
--- a/src/LambdaCube/Compiler/Patterns.hs
+++ b/src/LambdaCube/Compiler/Patterns.hs
@@ -305,7 +305,7 @@ compileGuardTree ulend lend si vt = fmap (\e -> foldr (uncurry SLam) e vt) . run
                     `SAppV` f
             Right n -> do
                 g1 <- guardTreeToCases (Nothing: path){-TODO-} $ filterGuardTree (up n f) s 0 n $ rUp n 0 ts
-                g2 <- guardTreeToCases (Nothing: path){-TODO-} (filterGuardTree' f s ts)
+                g2 <- guardTreeToCases (Nothing: path){-TODO-} $ filterGuardTree' f s ts
                 return $ SGlobal (SIName mempty $ MatchName $ sName s)
                  `SAppV` SLamV (Wildcard SType)
                  `SAppV` iterateN n SLamV g1
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 034df19d..ca39325f 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -210,7 +210,6 @@ renderDoc
             DPreOp _ op y -> renderA op <++> render' y
             DSep (InfixR 11) a b -> gr $ render' a <+++> render' b
             x@DApp{} -> case getApps x of
---                (DText "List", [x]) -> gr $ rtext "[" <+++> render' x <++> rtext "]"
                 (n, reverse -> xs) -> ((\xs -> (fst $ head xs, snd $ last xs)) *** P.nest 2 . P.sep) (unzip $ render' n: (render' <$> xs))
             DInfix _ x op y -> gr $ render' x <+++> renderA op <++> render' y
 
@@ -329,6 +328,7 @@ pattern DForall s vs e = DArr_ s (DPreOp 10 (SimpleAtom "forall") vs) e
 pattern DContext vs e = DArr_ "=>" vs e
 pattern DParContext vs e = DContext (DParen vs) e
 pattern DLam vs e = DPreOp (-10) (ComplexAtom "\\" 11 vs (SimpleAtom "->")) e
+pattern DLet' vs e = DPreOp (-10) (ComplexAtom "let" (-20) vs (SimpleAtom "in")) e
 
 --------------------------------------------------------------------------------
 
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs
index 2f1b5859..7d6b3970 100644
--- a/src/LambdaCube/Compiler/Statements.hs
+++ b/src/LambdaCube/Compiler/Statements.hs
@@ -59,6 +59,9 @@ 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' x = x
+
 type DefinedSet = Set.Set SName
 
 addForalls :: DefinedSet -> SExp -> SExp
@@ -99,7 +102,7 @@ compileStmt compilegt ds = \case
         --              , let ic = patVars i
                       ]
             ]
-        return $ cd ++ concat cds
+        return $ map addFix' cd ++ concat cds
     [TypeAnn n t] -> return [Primitive n t | n `notElem` [n' | FunAlt n' _ _ <- ds]]
     tf@[TypeFamily n t] -> case [d | d@(FunAlt n' _ _) <- ds, n' == n] of
         [] -> return [Primitive n t]
@@ -134,9 +137,11 @@ desugarValueDef p e = sequence
 getLet (Let x Nothing (SRHS dx)) = Just (x, dx)
 getLet _ = Nothing
 
+fst' (x, _) = x -- TODO
+
 desugarMutual :: {-MonadWriter [ParseCheck] m => -} [Stmt] -> [Stmt]
 desugarMutual [x] = [x]
-desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst{-TODO-} $ runWriter $ do
+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