diff options
Diffstat (limited to 'src/LambdaCube')
-rw-r--r-- | src/LambdaCube/Compiler/DesugaredSource.hs | 7 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 2 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Statements.hs | 14 |
3 files changed, 16 insertions, 7 deletions
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs index fb14b4e3..e83eb0ea 100644 --- a/src/LambdaCube/Compiler/DesugaredSource.hs +++ b/src/LambdaCube/Compiler/DesugaredSource.hs | |||
@@ -265,6 +265,7 @@ data SExp' a | |||
265 | | SBind_ SI Binder (SData SIName){-parameter name-} (SExp' a) (SExp' a) | 265 | | SBind_ SI Binder (SData SIName){-parameter name-} (SExp' a) (SExp' a) |
266 | | SVar_ (SData SIName) !Int | 266 | | SVar_ (SData SIName) !Int |
267 | | SLet_ SI (SData SIName) (SExp' a) (SExp' a) -- let x = e in f --> SLet e f{-x is Var 0-} | 267 | | SLet_ SI (SData SIName) (SExp' a) (SExp' a) -- let x = e in f --> SLet e f{-x is Var 0-} |
268 | | SLHS SIName (SExp' a) | ||
268 | | STyped a | 269 | | STyped a |
269 | deriving (Eq) | 270 | deriving (Eq) |
270 | 271 | ||
@@ -378,6 +379,7 @@ instance SourceInfo (SExp' a) where | |||
378 | SLet_ si _ _ _ -> si | 379 | SLet_ si _ _ _ -> si |
379 | SVar sn _ -> sourceInfo sn | 380 | SVar sn _ -> sourceInfo sn |
380 | SLit si _ -> si | 381 | SLit si _ -> si |
382 | SLHS n x -> sourceInfo x | ||
381 | STyped _ -> mempty | 383 | STyped _ -> mempty |
382 | 384 | ||
383 | instance SetSourceInfo SExp where | 385 | instance SetSourceInfo SExp where |
@@ -388,6 +390,7 @@ instance SetSourceInfo SExp where | |||
388 | SVar sn i -> SVar (setSI si sn) i | 390 | SVar sn i -> SVar (setSI si sn) i |
389 | SGlobal sn -> SGlobal (setSI si sn) | 391 | SGlobal sn -> SGlobal (setSI si sn) |
390 | SLit _ l -> SLit si l | 392 | SLit _ l -> SLit si l |
393 | SLHS n x -> SLHS n $ setSI si x | ||
391 | STyped v -> elimVoid v | 394 | STyped v -> elimVoid v |
392 | 395 | ||
393 | foldS | 396 | foldS |
@@ -407,6 +410,7 @@ foldS h g f = fs | |||
407 | SVar sn j -> f sn j i | 410 | SVar sn j -> f sn j i |
408 | SGlobal sn -> g sn i | 411 | SGlobal sn -> g sn i |
409 | x@SLit{} -> mempty | 412 | x@SLit{} -> mempty |
413 | SLHS _ x -> fs i x | ||
410 | STyped x -> h i x | 414 | STyped x -> h i x |
411 | 415 | ||
412 | foldName f = foldS (\_ -> elimVoid) (\sn _ -> f sn) mempty 0 | 416 | foldName f = foldS (\_ -> elimVoid) (\sn _ -> f sn) mempty 0 |
@@ -428,6 +432,7 @@ mapS hh gg f2 = g where | |||
428 | SBind_ si k si' a b -> SBind_ si k si' (g i a) (g (i+1) b) | 432 | SBind_ si k si' a b -> SBind_ si k si' (g i a) (g (i+1) b) |
429 | SVar sn j -> f2 sn j i | 433 | SVar sn j -> f2 sn j i |
430 | SGlobal sn -> gg sn i | 434 | SGlobal sn -> gg sn i |
435 | SLHS n x -> SLHS n $ g i x | ||
431 | STyped x -> hh i x | 436 | STyped x -> hh i x |
432 | x@SLit{} -> x | 437 | x@SLit{} -> x |
433 | 438 | ||
@@ -453,6 +458,7 @@ trSExp f = g where | |||
453 | SVar sn j -> SVar sn j | 458 | SVar sn j -> SVar sn j |
454 | SGlobal sn -> SGlobal sn | 459 | SGlobal sn -> SGlobal sn |
455 | SLit si l -> SLit si l | 460 | SLit si l -> SLit si l |
461 | SLHS n x -> SLHS n (g x) | ||
456 | STyped a -> STyped $ f a | 462 | STyped a -> STyped $ f a |
457 | 463 | ||
458 | trSExp' :: SExp -> SExp' a | 464 | trSExp' :: SExp -> SExp' a |
@@ -471,6 +477,7 @@ instance (HasFreeVars a, PShow a) => PShow (SExp' a) where | |||
471 | SBind_ _ h _ SType b -> shLam_ (usedVar 0 b) h Nothing (pShow b) | 477 | SBind_ _ h _ SType b -> shLam_ (usedVar 0 b) h Nothing (pShow b) |
472 | SBind_ _ h _ a b -> shLam (usedVar 0 b) h (pShow a) (pShow b) | 478 | SBind_ _ h _ a b -> shLam (usedVar 0 b) h (pShow a) (pShow b) |
473 | SLet _ a b -> shLet_ (pShow a) (pShow b) | 479 | SLet _ a b -> shLet_ (pShow a) (pShow b) |
480 | SLHS n x -> "_lhs" `DApp` pShow n `DApp` pShow x | ||
474 | STyped a -> pShow a | 481 | STyped a -> pShow a |
475 | SVar _ i -> shVar i | 482 | SVar _ i -> shVar i |
476 | SLit _ l -> pShow l | 483 | SLit _ l -> pShow l |
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 3eaae43b..444dd1b9 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -238,6 +238,7 @@ inferN_ tellTrace = infer where | |||
238 | Parens x -> infer te x | 238 | Parens x -> infer te x |
239 | SAnn x t -> checkN (CheckIType x te) t TType | 239 | SAnn x t -> checkN (CheckIType x te) t TType |
240 | SRHS x -> infer (ERHS te) x | 240 | SRHS x -> infer (ERHS te) x |
241 | SLHS n x -> infer te x | ||
241 | SVar sn i -> focusTell te exp $ ET (Var i) $ snd $ varType "C2" i te | 242 | SVar sn i -> focusTell te exp $ ET (Var i) $ snd $ varType "C2" i te |
242 | SLit si l -> focusTell te exp $ ET (ELit l) (nType l) | 243 | SLit si l -> focusTell te exp $ ET (ELit l) (nType l) |
243 | STyped et -> focusTell' te exp et | 244 | STyped et -> focusTell' te exp et |
@@ -268,6 +269,7 @@ inferN_ tellTrace = infer where | |||
268 | = infer te $ x `SAppV` SLamV (SLamV (STyped (subst (n'+2) (Var 1) $ up1_ (n'+3) $ up 2 t, TType))) `SAppV` a `SAppV` b `SAppV` SVar siv v | 269 | = infer te $ x `SAppV` SLamV (SLamV (STyped (subst (n'+2) (Var 1) $ up1_ (n'+3) $ up 2 t, TType))) `SAppV` a `SAppV` b `SAppV` SVar siv v |
269 | -} | 270 | -} |
270 | | SRHS x <- e = checkN (ERHS te) x t | 271 | | SRHS x <- e = checkN (ERHS te) x t |
272 | | SLHS n x <- e = checkN te x t | ||
271 | | SApp_ si h a b <- e = infer (CheckAppType si h t te b) a | 273 | | SApp_ si h a b <- e = infer (CheckAppType si h t te b) a |
272 | | SLam h a b <- e, Pi h' x y <- t, h == h' = do | 274 | | SLam h a b <- e, Pi h' x y <- t, h == h' = do |
273 | -- tellType e t | 275 | -- tellType e t |
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs index 1ce2beb6..178e5505 100644 --- a/src/LambdaCube/Compiler/Statements.hs +++ b/src/LambdaCube/Compiler/Statements.hs | |||
@@ -96,11 +96,11 @@ compileStmt compilegt ds = \case | |||
96 | | (m, t) <- ms | 96 | | (m, t) <- ms |
97 | -- , let ts = fst $ getParamsS $ up1 t | 97 | -- , let ts = fst $ getParamsS $ up1 t |
98 | , let as = [ funAlt m p $ noGuards {- -$ SLam Hidden (Wildcard SType) $ up1 -} $ SLet m' e $ sVar "cst" 0 | 98 | , let as = [ funAlt m p $ noGuards {- -$ SLam Hidden (Wildcard SType) $ up1 -} $ SLet m' e $ sVar "cst" 0 |
99 | | Instance n' i cstrs alts <- ds, n' == n | 99 | | Instance n' i cstrs alts <- ds, n' == n |
100 | , StLet m' ~Nothing e <- alts, m' == m | 100 | , StLet m' ~Nothing e <- alts, m' == m |
101 | , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVarSimp $ dummyName "cst2")] | 101 | , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVarSimp $ dummyName "cst2")] |
102 | -- , let ic = patVars i | 102 | -- , let ic = patVars i |
103 | ] | 103 | ] |
104 | ] | 104 | ] |
105 | return $ cd ++ concat cds | 105 | return $ cd ++ concat cds |
106 | [TypeAnn n t] -> return [Primitive n t | n `notElem` [n' | FunAlt n' _ _ <- ds]] | 106 | [TypeAnn n t] -> return [Primitive n t | n `notElem` [n' | FunAlt n' _ _ <- ds]] |
@@ -113,7 +113,7 @@ compileStmt compilegt ds = \case | |||
113 | | n `elem` [n' | TypeFamily n' _ <- ds] -> return [] | 113 | | n `elem` [n' | TypeFamily n' _ <- ds] -> return [] |
114 | | otherwise -> do | 114 | | otherwise -> do |
115 | cf <- compilegt (SIName_ (mconcat [sourceInfo n | FunAlt n _ _ <- fs]) (nameFixity n) $ sName n) vs [gt | FunAlt _ _ gt <- fs] | 115 | cf <- compilegt (SIName_ (mconcat [sourceInfo n | FunAlt n _ _ <- fs]) (nameFixity n) $ sName n) vs [gt | FunAlt _ _ gt <- fs] |
116 | return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) cf] | 116 | return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) $ SLHS n cf] |
117 | fs -> fail $ "different number of arguments of " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd . head <$> fs) | 117 | fs -> fail $ "different number of arguments of " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd . head <$> fs) |
118 | [Stmt x] -> return [x] | 118 | [Stmt x] -> return [x] |
119 | where | 119 | where |
@@ -134,7 +134,7 @@ desugarValueDef p e = sequence | |||
134 | dns = reverse $ getPVars p | 134 | dns = reverse $ getPVars p |
135 | n = mangleNames dns | 135 | n = mangleNames dns |
136 | 136 | ||
137 | getLet (StLet x Nothing (SRHS dx)) = Just (x, dx) | 137 | getLet (StLet x Nothing (SLHS _ (SRHS dx))) = Just (x, dx) |
138 | getLet _ = Nothing | 138 | getLet _ = Nothing |
139 | 139 | ||
140 | fst' (x, _) = x -- TODO | 140 | fst' (x, _) = x -- TODO |
@@ -144,7 +144,7 @@ desugarMutual [x] = [x] | |||
144 | desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do | 144 | desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do |
145 | ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy) | 145 | ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy) |
146 | return $ | 146 | return $ |
147 | StLet xy Nothing (addFix xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss | 147 | StLet xy Nothing (addFix xy $ SLHS xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss |
148 | where | 148 | where |
149 | xy = mangleNames ns | 149 | xy = mangleNames ns |
150 | desugarMutual xs = error "desugarMutual" | 150 | desugarMutual xs = error "desugarMutual" |