diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-05-12 01:03:59 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-05-12 01:03:59 +0200 |
commit | 25c580d8772e2626c4bcb4988e43450ba9bf9d16 (patch) | |
tree | 4dc432cab68332ac42d86956e719557a1888ba84 /src | |
parent | e4725c07ee3e7e3fc010df418d16f37c39b0af0f (diff) |
refactoring
Diffstat (limited to 'src')
-rw-r--r-- | src/LambdaCube/Compiler/Core.hs | 30 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 2 |
2 files changed, 18 insertions, 14 deletions
diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index 487cc4cc..b10f6de9 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs | |||
@@ -324,8 +324,8 @@ instance Subst Exp Exp where | |||
324 | substNeut e = case e of | 324 | substNeut e = case e of |
325 | Var_ k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> up (i - i0) x | 325 | Var_ k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> up (i - i0) x |
326 | CaseFun__ fs s as n -> evalCaseFun (adjustDB i fs) s (f i <$> as) (substNeut n) | 326 | CaseFun__ fs s as n -> evalCaseFun (adjustDB i fs) s (f i <$> as) (substNeut n) |
327 | TyCaseFun_ s as n -> evalTyCaseFun s (f i <$> as) (substNeut n) | 327 | TyCaseFun__ fs s as n -> evalTyCaseFun_ (adjustDB i fs) s (f i <$> as) (substNeut n) |
328 | App_ a b -> app_ (substNeut a) (f i b) | 328 | App__ fs a b -> app__ (adjustDB i fs) (substNeut a) (f i b) |
329 | Fun_ md fn xs v -> mkFun_ (adjustDB i md) fn (f i <$> xs) $ f i v | 329 | Fun_ md fn xs v -> mkFun_ (adjustDB i md) fn (f i <$> xs) $ f i v |
330 | f i e | dbGE i e = e | 330 | f i e | dbGE i e = e |
331 | f i e = case e of | 331 | f i e = case e of |
@@ -576,12 +576,14 @@ evalCaseFun _ a b x = error $ "evalCaseFun: " ++ ppShow (a, x) | |||
576 | 576 | ||
577 | evalCaseFun' a b c = evalCaseFun (getFreeVars c <> foldMap getFreeVars b) a b c | 577 | evalCaseFun' a b c = evalCaseFun (getFreeVars c <> foldMap getFreeVars b) a b c |
578 | 578 | ||
579 | evalTyCaseFun a b (Reduced c) = evalTyCaseFun a b c | 579 | evalTyCaseFun a b c = evalTyCaseFun_ (foldMap getFreeVars b <> getFreeVars c) a b c |
580 | evalTyCaseFun a b (Neut c) = TyCaseFun a b c | 580 | |
581 | evalTyCaseFun (TyCaseFunName FType ty) (_: t: f: _) TType = t | 581 | evalTyCaseFun_ s a b (Reduced c) = evalTyCaseFun_ s a b c |
582 | evalTyCaseFun (TyCaseFunName n ty) (_: t: f: _) (TyCon (TyConName n' _ _ _ _) vs) | n == n' = foldl app_ t vs | 582 | evalTyCaseFun_ s a b (Neut c) = Neut $ TyCaseFun__ s a b c |
583 | evalTyCaseFun_ _ (TyCaseFunName FType ty) (_: t: f: _) TType = t | ||
584 | evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) (TyCon (TyConName n' _ _ _ _) vs) | n == n' = foldl app_ t vs | ||
583 | --evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (DFun (FunName n' _) vs) | n == n' = foldl app_ t vs -- hack | 585 | --evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (DFun (FunName n' _) vs) | n == n' = foldl app_ t vs -- hack |
584 | evalTyCaseFun (TyCaseFunName n ty) (_: t: f: _) _ = f | 586 | evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) _ = f |
585 | 587 | ||
586 | evalCoe a b (Reduced x) d = evalCoe a b x d | 588 | evalCoe a b (Reduced x) d = evalCoe a b x d |
587 | evalCoe a b TT d = d | 589 | evalCoe a b TT d = d |
@@ -636,15 +638,17 @@ t2 _ (hnf -> CEmpty s) = CEmpty s | |||
636 | t2 a b = T2 a b | 638 | t2 a b = T2 a b |
637 | 639 | ||
638 | app_ :: Exp -> Exp -> Exp | 640 | app_ :: Exp -> Exp -> Exp |
639 | app_ (Lam x) a = subst 0 a x | 641 | app_ a b = app__ (getFreeVars a <> getFreeVars b) a b |
640 | app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a]) | 642 | |
641 | app_ (TyCon s xs) a = TyCon s (xs ++ [a]) | 643 | app__ _ (Lam x) a = subst 0 a x |
642 | app_ (SubstLet f) a = app_ f a | 644 | app__ _ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a]) |
643 | app_ (Neut f) a = neutApp f a | 645 | app__ _ (TyCon s xs) a = TyCon s (xs ++ [a]) |
646 | app__ _ (SubstLet f) a = app_ f a | ||
647 | app__ s (Neut f) a = neutApp f a | ||
644 | where | 648 | where |
645 | neutApp (ReducedN x) a = app_ x a | 649 | neutApp (ReducedN x) a = app_ x a |
646 | neutApp (Fun_ db f xs (Lam e)) a = mkFun_ (db <> getFreeVars a) f (a: xs) (subst 0 a e) | 650 | neutApp (Fun_ db f xs (Lam e)) a = mkFun_ (db <> getFreeVars a) f (a: xs) (subst 0 a e) |
647 | neutApp f a = Neut $ App_ f a | 651 | neutApp f a = Neut $ App__ s f a |
648 | 652 | ||
649 | conType (snd . getParams . hnf -> TyCon (TyConName _ _ _ cs _) _) (ConName _ n t) = t --snd $ cs !! n | 653 | conType (snd . getParams . hnf -> TyCon (TyConName _ _ _ cs _) _) (ConName _ n t) = t --snd $ cs !! n |
650 | 654 | ||
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 089392d1..10c73c98 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -468,7 +468,7 @@ recheck' sn e (ET x xt) = ET (recheck_ "main" (checkEnv e) (ET x xt)) xt | |||
468 | 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 | 468 | 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 |
469 | ET (TyCon_ md s as) zt -> checkApps (ppShow s) [] zt (TyCon_ md s) te (nType s) as | 469 | ET (TyCon_ md s as) zt -> checkApps (ppShow s) [] zt (TyCon_ md s) te (nType s) as |
470 | 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]) | 470 | 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]) |
471 | 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] | 471 | 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] |
472 | 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 | 472 | 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 |
473 | 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 | 473 | 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 |
474 | ET (RHS x) zt -> RHS $ recheck_ msg te (ET x zt) | 474 | ET (RHS x) zt -> RHS $ recheck_ msg te (ET x zt) |