diff options
-rw-r--r-- | src/LambdaCube/Compiler/Core.hs | 44 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/CoreToIR.hs | 4 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 12 |
3 files changed, 28 insertions, 32 deletions
diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index eb7c59cf..4f04a2ae 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs | |||
@@ -73,8 +73,8 @@ data Exp | |||
73 | = ELit Lit | 73 | = ELit Lit |
74 | | TType_ Freq | 74 | | TType_ Freq |
75 | | Lam_ FreeVars Exp | 75 | | Lam_ FreeVars Exp |
76 | | Con_ FreeVars ConName !Int{-number of ereased arguments applied-} [Exp] | 76 | | Con_ FreeVars ConName !Int{-number of ereased arguments applied-} [Exp]{-args reversed-} |
77 | | TyCon_ FreeVars TyConName [Exp] | 77 | | TyCon_ FreeVars TyConName [Exp]{-args reversed-} |
78 | | Pi_ FreeVars Visibility Exp Exp | 78 | | Pi_ FreeVars Visibility Exp Exp |
79 | | Neut Neutral | 79 | | Neut Neutral |
80 | | RHS Exp{-always in hnf-} | 80 | | RHS Exp{-always in hnf-} |
@@ -160,8 +160,7 @@ pattern DFunN_ a t xs <- Fun (FunName' a t) xs _ | |||
160 | where DFunN_ a t xs = Fun (FunName' a t) xs delta | 160 | where DFunN_ a t xs = Fun (FunName' a t) xs delta |
161 | 161 | ||
162 | conParams (conTypeName -> TyConName _ _ _ _ (CaseFunName _ _ pars)) = pars | 162 | conParams (conTypeName -> TyConName _ _ _ _ (CaseFunName _ _ pars)) = pars |
163 | mkConPars n (snd . getParams . hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) = take (min n pars) xs | 163 | mkConPars n (snd . getParams . hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) = take (min n pars) $ reverse xs |
164 | --mkConPars 0 TType = [] -- ? | ||
165 | mkConPars n x@Neut{} = error $ "mkConPars!: " ++ ppShow x | 164 | mkConPars n x@Neut{} = error $ "mkConPars!: " ++ ppShow x |
166 | mkConPars n x = error $ "mkConPars: " ++ ppShow (n, x) | 165 | mkConPars n x = error $ "mkConPars: " ++ ppShow (n, x) |
167 | 166 | ||
@@ -169,11 +168,8 @@ pattern ConN s a <- Con (ConName (FTag s) _ _) _ a | |||
169 | tCon s i t a = Con (ConName (FTag s) i t) 0 a | 168 | tCon s i t a = Con (ConName (FTag s) i t) 0 a |
170 | tCon_ k s i t a = Con (ConName (FTag s) i t) k a | 169 | tCon_ k s i t a = Con (ConName (FTag s) i t) k a |
171 | pattern TyConN s a <- TyCon (TyConName s _ _ _ _) a | 170 | pattern TyConN s a <- TyCon (TyConName s _ _ _ _) a |
172 | pattern TTyCon s t a <- TyCon (TyConName s _ t _ _) a | ||
173 | 171 | ||
174 | pattern TTyCon0 s <- TyCon (TyConName (FTag s) _ _ _ _) [] | 172 | pattern TTyCon0 s <- TyCon (TyConName (FTag s) _ _ _ _) [] |
175 | |||
176 | tTyCon s t a cs = TyCon (TyConName s (error "todo: inum") t (map ((,) (error "tTyCon")) cs) $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a | ||
177 | tTyCon0 s cs = TyCon (TyConName (FTag s) 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) [] | 173 | tTyCon0 s cs = TyCon (TyConName (FTag s) 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) [] |
178 | 174 | ||
179 | pattern a :~> b = Pi Visible a b | 175 | pattern a :~> b = Pi Visible a b |
@@ -189,9 +185,9 @@ pattern TFloat <- TTyCon0 F'Float where TFloat = tTyCon0 F'Float $ | |||
189 | pattern TString <- TTyCon0 F'String where TString = tTyCon0 F'String $ error "cs 6" | 185 | pattern TString <- TTyCon0 F'String where TString = tTyCon0 F'String $ error "cs 6" |
190 | pattern TChar <- TTyCon0 F'Char where TChar = tTyCon0 F'Char $ error "cs 7" | 186 | pattern TChar <- TTyCon0 F'Char where TChar = tTyCon0 F'Char $ error "cs 7" |
191 | pattern TOrdering <- TTyCon0 F'Ordering where TOrdering = tTyCon0 F'Ordering $ error "cs 8" | 187 | pattern TOrdering <- TTyCon0 F'Ordering where TOrdering = tTyCon0 F'Ordering $ error "cs 8" |
192 | pattern TVec a b <- TyConN (FTag F'VecS) [b, a] | 188 | pattern TVec a b <- TyConN (FTag F'VecS) [a, b] |
193 | 189 | ||
194 | pattern Empty s <- TyCon (TyConName (FTag F'Empty) _ _ _ _) [HString{-hnf?-} s] | 190 | pattern Empty s <- TyCon (TyConName (FTag F'Empty) _ _ _ _) (HString{-hnf?-} s: _) |
195 | where Empty s = TyCon (TyConName (FTag F'Empty) (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [HString s] | 191 | where Empty s = TyCon (TyConName (FTag F'Empty) (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [HString s] |
196 | 192 | ||
197 | pattern TT <- Con _ _ _ | 193 | pattern TT <- Con _ _ _ |
@@ -232,7 +228,7 @@ pattern ENat n <- (fromNatE -> Just n) | |||
232 | 228 | ||
233 | fromNatE :: Exp -> Maybe Int | 229 | fromNatE :: Exp -> Maybe Int |
234 | fromNatE (hnf -> ConN FZero _) = Just 0 | 230 | fromNatE (hnf -> ConN FZero _) = Just 0 |
235 | fromNatE (hnf -> ConN FSucc (n:_)) = succ <$> fromNatE n | 231 | fromNatE (hnf -> ConN FSucc (n: _)) = succ <$> fromNatE n |
236 | fromNatE _ = Nothing | 232 | fromNatE _ = Nothing |
237 | 233 | ||
238 | mkOrdering x = case x of | 234 | mkOrdering x = case x of |
@@ -404,12 +400,12 @@ instance MkDoc Exp where | |||
404 | Pi h TType b -> shLam_ (usedVar 0 b) (BPi h) Nothing (mkDoc pr b) | 400 | Pi h TType b -> shLam_ (usedVar 0 b) (BPi h) Nothing (mkDoc pr b) |
405 | Pi h a b -> shLam (usedVar 0 b) (BPi h) (mkDoc pr a) (mkDoc pr b) | 401 | Pi h a b -> shLam (usedVar 0 b) (BPi h) (mkDoc pr a) (mkDoc pr b) |
406 | ENat n -> pShow n | 402 | ENat n -> pShow n |
407 | Con s@(ConName _ i _) _ xs | body -> text $ "<<" ++ showNth i ++ " constructor of " ++ show (conTypeName s) ++ ">>" | 403 | Con s@(ConName _ i _) _ _ | body -> text $ "<<" ++ showNth i ++ " constructor of " ++ show (conTypeName s) ++ ">>" |
408 | ConN FHCons [_, _, x, xs] -> foldl DApp (text "HCons") (mkDoc pr <$> [x, xs]) | 404 | ConN FHCons (xs: x: _{-2-}) -> foldl DApp (text "HCons") (mkDoc pr <$> [x, xs]) |
409 | Con s _ xs -> foldl DApp (pShow s) (mkDoc pr <$> xs) | 405 | Con s _ xs -> foldlrev DApp (pShow s) (mkDoc pr <$> xs) |
410 | TyCon s@(TyConName _ i _ cs _) xs | body | 406 | TyCon s@(TyConName _ i _ cs _) _ | body |
411 | -> text $ "<<type constructor with " ++ show i ++ " indices; constructors: " ++ intercalate ", " (show . fst <$> cs) ++ ">>" | 407 | -> text $ "<<type constructor with " ++ show i ++ " indices; constructors: " ++ intercalate ", " (show . fst <$> cs) ++ ">>" |
412 | TyConN s xs -> foldl DApp (pShow s) (mkDoc pr <$> xs) | 408 | TyConN s xs -> foldlrev DApp (pShow s) (mkDoc pr <$> xs) |
413 | TType -> text "Type" | 409 | TType -> text "Type" |
414 | ELit l -> pShow l | 410 | ELit l -> pShow l |
415 | Neut x -> mkDoc pr x | 411 | Neut x -> mkDoc pr x |
@@ -446,7 +442,7 @@ instance MkDoc Neutral where | |||
446 | where (_h, v) = splitAt loc $ mkDoc pr <$> reverse xs | 442 | where (_h, v) = splitAt loc $ mkDoc pr <$> reverse xs |
447 | Var_ k -> shVar k | 443 | Var_ k -> shVar k |
448 | App_ a b -> mkDoc pr a `DApp` mkDoc pr b | 444 | App_ a b -> mkDoc pr a `DApp` mkDoc pr b |
449 | CaseFun_ s@(CaseFunName _ _ p) xs n | body -> text $ "<<case function of a type with " ++ show p ++ " parameters>>" | 445 | CaseFun_ s@(CaseFunName _ _ p) _ n | body -> text $ "<<case function of a type with " ++ show p ++ " parameters>>" |
450 | CaseFun_ s xs n -> foldl DApp (pShow s) (map (mkDoc pr) $ xs ++ [Neut n]) | 446 | CaseFun_ s xs n -> foldl DApp (pShow s) (map (mkDoc pr) $ xs ++ [Neut n]) |
451 | TyCaseFun_ _ _ _ | body -> text "<<type case function>>" | 447 | TyCaseFun_ _ _ _ | body -> text "<<type case function>>" |
452 | TyCaseFun_ s [m, t, f] n -> foldl DApp (pShow s) (mkDoc pr <$> [m, t, Neut n, f]) | 448 | TyCaseFun_ s [m, t, f] n -> foldl DApp (pShow s) (mkDoc pr <$> [m, t, Neut n, f]) |
@@ -494,8 +490,8 @@ getFunDef t s f = case show s of | |||
494 | 490 | ||
495 | "unsafeCoerce" -> Just $ \case xs@(x@(hnf -> NonNeut): _{-2-}) -> x; xs -> f xs | 491 | "unsafeCoerce" -> Just $ \case xs@(x@(hnf -> NonNeut): _{-2-}) -> x; xs -> f xs |
496 | "reflCstr" -> Just $ \case _ -> TT | 492 | "reflCstr" -> Just $ \case _ -> TT |
497 | "hlistNilCase" -> Just $ \case ((hnf -> Con n@(ConName _ 0 _) _ _): x: _{-1-}) -> x; xs -> f xs | 493 | "hlistNilCase" -> Just $ \case ((hnf -> ConN FHCons _): x: _{-1-}) -> x; xs -> f xs |
498 | "hlistConsCase" -> Just $ \case ((hnf -> Con n@(ConName _ 1 _) _ (_: _: a: b: _)): x: _{-3-}) -> x `app_` a `app_` b; xs -> f xs | 494 | "hlistConsCase" -> Just $ \case ((hnf -> ConN FHNil (b: a: _{-2-})): x: _{-3-}) -> x `app_` a `app_` b; xs -> f xs |
499 | 495 | ||
500 | -- general compiler primitives | 496 | -- general compiler primitives |
501 | "primAddInt" -> Just $ \case (HInt j: HInt i: _) -> HInt (i + j); xs -> f xs | 497 | "primAddInt" -> Just $ \case (HInt j: HInt i: _) -> HInt (i + j); xs -> f xs |
@@ -564,7 +560,7 @@ getFunDef t s f = case show s of | |||
564 | modF x y = x - fromIntegral (floor (x / y)) * y | 560 | modF x y = x - fromIntegral (floor (x / y)) * y |
565 | 561 | ||
566 | evalCaseFun _ a ps (Con n@(ConName _ i _) _ vs) | 562 | evalCaseFun _ a ps (Con n@(ConName _ i _) _ vs) |
567 | | i /= (-1) = foldl app_ (ps !!! (i + 1)) vs | 563 | | i /= (-1) = foldlrev app_ (ps !!! (i + 1)) vs |
568 | | otherwise = error "evcf" | 564 | | otherwise = error "evcf" |
569 | where | 565 | where |
570 | xs !!! i | i >= length xs = error $ "!!! " ++ ppShow a ++ " " ++ show i ++ " " ++ ppShow n ++ "\n" ++ ppShow ps | 566 | xs !!! i | i >= length xs = error $ "!!! " ++ ppShow a ++ " " ++ show i ++ " " ++ ppShow n ++ "\n" ++ ppShow ps |
@@ -580,7 +576,7 @@ evalTyCaseFun a b c = evalTyCaseFun_ (foldMap getFreeVars b <> getFreeVars c) a | |||
580 | evalTyCaseFun_ s a b (Reduced c) = evalTyCaseFun_ s a b c | 576 | evalTyCaseFun_ s a b (Reduced c) = evalTyCaseFun_ s a b c |
581 | evalTyCaseFun_ s a b (Neut c) = Neut $ TyCaseFun__ s a b c | 577 | evalTyCaseFun_ s a b (Neut c) = Neut $ TyCaseFun__ s a b c |
582 | evalTyCaseFun_ _ (TyCaseFunName (FTag F'Type) ty) (_: t: f: _) TType = t | 578 | evalTyCaseFun_ _ (TyCaseFunName (FTag F'Type) ty) (_: t: f: _) TType = t |
583 | evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) (TyCon (TyConName n' _ _ _ _) vs) | n == n' = foldl app_ t vs | 579 | evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) (TyCon (TyConName n' _ _ _ _) vs) | n == n' = foldlrev app_ t vs |
584 | --evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (DFun (FunName n' _) vs) | n == n' = foldl app_ t vs -- hack | 580 | --evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (DFun (FunName n' _) vs) | n == n' = foldl app_ t vs -- hack |
585 | evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) _ = f | 581 | evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) _ = f |
586 | 582 | ||
@@ -597,9 +593,9 @@ cstr = f [] | |||
597 | f_ _ _ a a' | a == a' = CUnit | 593 | f_ _ _ a a' | a == a' = CUnit |
598 | f_ ns typ (RHS a) (RHS a') = f ns typ a a' | 594 | f_ ns typ (RHS a) (RHS a') = f ns typ a a' |
599 | f_ ns typ (Con a n xs) (Con a' n' xs') | a == a' && n == n' && length xs == length xs' = | 595 | f_ ns typ (Con a n xs) (Con a' n' xs') | a == a' && n == n' && length xs == length xs' = |
600 | ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ zip xs xs' | 596 | ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ reverse $ zip xs xs' |
601 | f_ ns typ (TyCon a xs) (TyCon a' xs') | a == a' && length xs == length xs' = | 597 | f_ ns typ (TyCon a xs) (TyCon a' xs') | a == a' && length xs == length xs' = |
602 | ff ns (nType a) $ zip xs xs' | 598 | ff ns (nType a) $ reverse $ zip xs xs' |
603 | f_ (_: ns) typ{-down?-} (down 0 -> Just a) (down 0 -> Just a') = f ns typ a a' | 599 | f_ (_: ns) typ{-down?-} (down 0 -> Just a) (down 0 -> Just a') = f ns typ a a' |
604 | f_ ns TType (Pi h a b) (Pi h' a' b') | h == h' = t2 (f ns TType a a') (f ((a, a'): ns) TType b b') | 600 | f_ ns TType (Pi h a b) (Pi h' a' b') | h == h' = t2 (f ns TType a a') (f ((a, a'): ns) TType b b') |
605 | 601 | ||
@@ -640,8 +636,8 @@ app_ :: Exp -> Exp -> Exp | |||
640 | app_ a b = app__ (getFreeVars a <> getFreeVars b) a b | 636 | app_ a b = app__ (getFreeVars a <> getFreeVars b) a b |
641 | 637 | ||
642 | app__ _ (Lam x) a = subst 0 a x | 638 | app__ _ (Lam x) a = subst 0 a x |
643 | app__ _ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a]) | 639 | app__ _ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (a: xs) |
644 | app__ _ (TyCon s xs) a = TyCon s (xs ++ [a]) | 640 | app__ _ (TyCon s xs) a = TyCon s (a: xs) |
645 | app__ _ (SubstLet f) a = app_ f a | 641 | app__ _ (SubstLet f) a = app_ f a |
646 | app__ s (Neut f) a = neutApp f a | 642 | app__ s (Neut f) a = neutApp f a |
647 | where | 643 | where |
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs index 6dd39a93..892eda2e 100644 --- a/src/LambdaCube/Compiler/CoreToIR.hs +++ b/src/LambdaCube/Compiler/CoreToIR.hs | |||
@@ -862,8 +862,8 @@ mkPi _ = Nothing | |||
862 | mkLam (ExpTV (I.Lam y) (I.Pi b x yt) vs) = Just (b, x .@ vs, ExpTV y yt $ addToEnv x vs) | 862 | mkLam (ExpTV (I.Lam y) (I.Pi b x yt) vs) = Just (b, x .@ vs, ExpTV y yt $ addToEnv x vs) |
863 | mkLam _ = Nothing | 863 | mkLam _ = Nothing |
864 | 864 | ||
865 | mkCon (ExpTV (I.Con s n xs) et vs) = Just (untick $ show s, chain vs (I.conType et s) $ I.mkConPars n et ++ xs) | 865 | mkCon (ExpTV (I.Con s n (reverse -> xs)) et vs) = Just (untick $ show s, chain vs (I.conType et s) $ I.mkConPars n et ++ xs) |
866 | mkCon (ExpTV (I.TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs) | 866 | mkCon (ExpTV (I.TyCon s (reverse -> xs)) et vs) = Just (untick $ show s, chain vs (nType s) xs) |
867 | mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ loc _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, drop loc $ chain vs (nType s) xs) | 867 | mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ loc _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, drop loc $ chain vs (nType s) xs) |
868 | mkCon (ExpTV (I.CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [I.Neut n]) | 868 | mkCon (ExpTV (I.CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [I.Neut n]) |
869 | mkCon (ExpTV (I.TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, I.Neut n, f]) | 869 | mkCon (ExpTV (I.TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, I.Neut n, f]) |
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index f726f30b..6d26cedd 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -201,11 +201,11 @@ neutType' te = \case | |||
201 | Fun s a _ -> foldlrev appTy (nType s) a | 201 | Fun s a _ -> foldlrev appTy (nType s) a |
202 | 202 | ||
203 | makeCaseFunPars te n = case neutType te n of | 203 | makeCaseFunPars te n = case neutType te n of |
204 | (hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) -> take pars xs | 204 | (hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) -> take pars $ reverse xs |
205 | x -> error $ "makeCaseFunPars: " ++ ppShow x | 205 | x -> error $ "makeCaseFunPars: " ++ ppShow x |
206 | 206 | ||
207 | makeCaseFunPars' te n = case neutType' te n of | 207 | makeCaseFunPars' te n = case neutType' te n of |
208 | (hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) -> take pars xs | 208 | (hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) -> take pars $ reverse xs |
209 | 209 | ||
210 | -------------------------------------------------------------------------------- inference | 210 | -------------------------------------------------------------------------------- inference |
211 | 211 | ||
@@ -261,7 +261,7 @@ inferN_ tellTrace = infer where | |||
261 | = infer te $ x `SAppV` SLamV (STyped (ET (substTo (v+1) (Var 0) $ up 1 t) TType)) `SAppV` a `SAppV` b `SAppV` SVar siv v | 261 | = infer te $ x `SAppV` SLamV (STyped (ET (substTo (v+1) (Var 0) $ up 1 t) TType)) `SAppV` a `SAppV` b `SAppV` SVar siv v |
262 | -- temporal hack | 262 | -- temporal hack |
263 | | x@(SGlobal (sName -> CaseName "'VecS")) `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar siv v <- e | 263 | | x@(SGlobal (sName -> CaseName "'VecS")) `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar siv v <- e |
264 | , TyConN (FTag F'VecS) [_, Var n'] <- snd $ varType "xx" v te | 264 | , TyConN (FTag F'VecS) [Var n', _] <- snd $ varType "xx" v te |
265 | = infer te $ x `SAppV` SLamV (SLamV (STyped (ET (substTo (n'+2) (Var 1) $ up 2 t) TType))) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar siv v | 265 | = infer te $ x `SAppV` SLamV (SLamV (STyped (ET (substTo (n'+2) (Var 1) $ up 2 t) TType))) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar siv v |
266 | 266 | ||
267 | {- | 267 | {- |
@@ -471,8 +471,8 @@ recheck' sn e (ET x xt) = ET (recheck_ "main" (checkEnv e) (ET x xt)) xt | |||
471 | ET (Neut (App__ md a b)) zt | 471 | ET (Neut (App__ md a b)) zt |
472 | | ET (Neut a') at <- recheck'' "app1" te $ ET (Neut a) (neutType te a) | 472 | | ET (Neut a') at <- recheck'' "app1" te $ ET (Neut a) (neutType te a) |
473 | -> checkApps "a" [] zt (Neut . App__ md a' . head) te at [b] | 473 | -> checkApps "a" [] zt (Neut . App__ md a' . head) te at [b] |
474 | ET (Con_ md s n as) zt -> checkApps (ppShow s) [] zt (Con_ md s n . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ as | 474 | ET (Con_ md s n as) zt -> checkApps (ppShow s) [] zt (Con_ md s n . reverse . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ reverse as |
475 | ET (TyCon_ md s as) zt -> checkApps (ppShow s) [] zt (TyCon_ md s) te (nType s) as | 475 | ET (TyCon_ md s as) zt -> checkApps (ppShow s) [] zt (TyCon_ md s . reverse) te (nType s) $ reverse as |
476 | ET (Neut (CaseFun__ fs s@(CaseFunName _ t pars) as n)) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun fs s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n]) | 476 | ET (Neut (CaseFun__ fs s@(CaseFunName _ t pars) as n)) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun fs s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n]) |
477 | ET (Neut (TyCaseFun__ fs s [m, t, f] n)) zt -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun_ fs s [m, t, f] n) te (nType s) [m, t, Neut n, f] | 477 | ET (Neut (TyCaseFun__ fs s [m, t, f] n)) zt -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun_ fs s [m, t, f] n) te (nType s) [m, t, Neut n, f] |
478 | 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 | 478 | 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 |
@@ -564,7 +564,7 @@ handleStmt = \case | |||
564 | e2 <- addToEnv (SIName (sourceInfo s) $ CaseName (sName s)) $ ET (lamify ct $ \xs -> evalCaseFun' cfn (init $ drop (length ps) xs) (last xs)) ct | 564 | e2 <- addToEnv (SIName (sourceInfo s) $ CaseName (sName s)) $ ET (lamify ct $ \xs -> evalCaseFun' cfn (init $ drop (length ps) xs) (last xs)) ct |
565 | let ps' = fst $ getParams vty | 565 | let ps' = fst $ getParams vty |
566 | t = (TType :~> TType) | 566 | t = (TType :~> TType) |
567 | :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps')) | 567 | :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo' 0 $ length ps')) |
568 | :~> TType | 568 | :~> TType |
569 | :~> Var 2 `app_` Var 0 | 569 | :~> Var 2 `app_` Var 0 |
570 | :~> Var 3 `app_` Var 1 | 570 | :~> Var 3 `app_` Var 1 |