diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-05-14 02:03:33 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-05-14 02:03:33 +0200 |
commit | ed2b64667428a737ef67c1632d408633d2717509 (patch) | |
tree | 88b2d002572b2f9623c91de931defc0f859e7d0c | |
parent | 472c3b8d66c3f3065e8a6715c59c5295cb16d435 (diff) |
refactoring
-rw-r--r-- | src/LambdaCube/Compiler/Core.hs | 132 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 2 |
2 files changed, 71 insertions, 63 deletions
diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index 3fca8b45..e86e205a 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs | |||
@@ -149,6 +149,7 @@ pattern TyCaseFun a b c = Neut (TyCaseFun_ a b c) | |||
149 | pattern Var a = Neut (Var_ a) | 149 | pattern Var a = Neut (Var_ a) |
150 | pattern App a b <- Neut (App_ (Neut -> a) b) | 150 | pattern App a b <- Neut (App_ (Neut -> a) b) |
151 | pattern DFun a b = Neut (DFunN a b) | 151 | pattern DFun a b = Neut (DFunN a b) |
152 | pattern DFun_ s a b = Neut (DFunN_ s a b) | ||
152 | 153 | ||
153 | -- unreducable function application | 154 | -- unreducable function application |
154 | pattern UFun a b <- Neut (Fun (FunName (FTag a) _ _ _) b NoRHS) | 155 | pattern UFun a b <- Neut (Fun (FunName (FTag a) _ _ _) b NoRHS) |
@@ -157,6 +158,9 @@ pattern UFun a b <- Neut (Fun (FunName (FTag a) _ _ _) b NoRHS) | |||
157 | pattern DFunN a xs <- Fun (FunName (FTag a) _ _ _) xs _ | 158 | pattern DFunN a xs <- Fun (FunName (FTag a) _ _ _) xs _ |
158 | where DFunN a xs = Fun (mkFunDef' (FTag a)) xs delta | 159 | where DFunN a xs = Fun (mkFunDef' (FTag a)) xs delta |
159 | 160 | ||
161 | pattern DFunN_ s a xs <- Fun_ s (FunName (FTag a) _ _ _) xs _ | ||
162 | where DFunN_ s a xs = Fun_ s (mkFunDef' (FTag a)) xs delta | ||
163 | |||
160 | mkFunDef' a@(FTag f) = mkFunDef a $ funTy f | 164 | mkFunDef' a@(FTag f) = mkFunDef a $ funTy f |
161 | 165 | ||
162 | funTy = \case | 166 | funTy = \case |
@@ -210,8 +214,9 @@ pattern CstrT t a b = Neut (CstrT' t a b) | |||
210 | pattern CstrT' t a b = DFunN F'EqCT [b, a, t] | 214 | pattern CstrT' t a b = DFunN F'EqCT [b, a, t] |
211 | pattern Coe a b w x = DFun Fcoe [x,w,b,a] | 215 | pattern Coe a b w x = DFun Fcoe [x,w,b,a] |
212 | pattern ParEval t a b = DFun FparEval [b, a, t] | 216 | pattern ParEval t a b = DFun FparEval [b, a, t] |
213 | pattern T2 a b = DFun F'T2 [b, a] | 217 | pattern T2 s a b = DFun_ s F'T2 [b, a] |
214 | pattern CW a = DFun F'CW [a] | 218 | pattern CW a = DFun F'CW [a] |
219 | pattern CW_ s a = DFun_ s F'CW [a] | ||
215 | pattern CSplit a b c <- UFun F'Split [c, b, a] | 220 | pattern CSplit a b c <- UFun F'Split [c, b, a] |
216 | 221 | ||
217 | pattern HLit a <- (hnf -> ELit a) | 222 | pattern HLit a <- (hnf -> ELit a) |
@@ -464,74 +469,73 @@ instance MkDoc Neutral where | |||
464 | 469 | ||
465 | mkFunDef a@(FTag FprimFix) t = fn | 470 | mkFunDef a@(FTag FprimFix) t = fn |
466 | where | 471 | where |
467 | fn = FunName a 0 (DeltaDef (length $ fst $ getParams t) fx) t | 472 | fn = FunName a 0 (DeltaDef 2 fx) t |
468 | fx s xs = Neut $ Fun_ s fn xs $ case xs of | 473 | fx s xs@(f: _) = x where x = Neut $ Fun_ s fn xs $ RHS $ f `app_` x |
469 | f: _{-1-} -> RHS x where x = f `app_` Neut (Fun_ s fn xs $ RHS x) | ||
470 | _ -> delta | ||
471 | 474 | ||
472 | mkFunDef a@(FTag tag) t = fn | 475 | mkFunDef a@(FTag tag) t = fn |
473 | where | 476 | where |
474 | f xs = Neut $ Fun fn xs delta | 477 | fn = FunName a 0 (maybe NoDef (DeltaDef (length $ fst $ getParams t)) $ getFunDef tag) t |
475 | fn = FunName a 0 (maybe NoDef (DeltaDef (length $ fst $ getParams t) . const) $ getFunDef tag) t | 478 | |
476 | 479 | getFunDef tag = case tag of | |
477 | getFunDef = \case | 480 | F'EqCT -> Just $ \s -> \case (b: a: t: _) -> cstr t a b |
478 | F'EqCT -> Just $ \case (b: a: t: _) -> cstr t a b | 481 | F'T2 -> Just $ \s -> \case (b: a: _) -> t2_ s a b |
479 | F'T2 -> Just $ \case (b: a: _) -> t2 a b | 482 | F'CW -> Just $ \s -> \case (a: _) -> cw_ s a |
480 | F'CW -> Just $ \case (a: _) -> cw a | 483 | Ft2C -> Just $ \s -> \case (b: a: _) -> t2C a b |
481 | Ft2C -> Just $ \case (b: a: _) -> t2C a b | 484 | Fcoe -> Just $ \s -> \case (d: t: b: a: _) -> evalCoe a b t d |
482 | Fcoe -> Just $ \case (d: t: b: a: _) -> evalCoe a b t d | 485 | FparEval -> Just $ \s -> \case (b: a: t: _) -> parEval t a b |
483 | FparEval -> Just $ \case (b: a: t: _) -> parEval t a b | ||
484 | where | 486 | where |
485 | parEval _ x@RHS{} _ = x | 487 | parEval _ x@RHS{} _ = x |
486 | parEval _ _ x@RHS{} = x | 488 | parEval _ _ x@RHS{} = x |
487 | parEval t a b = ParEval t a b | 489 | parEval t a b = ParEval t a b |
488 | 490 | ||
489 | FunsafeCoerce -> Just $ \case xs@(x@(hnf -> NonNeut): _{-2-}) -> x; xs -> f xs | 491 | FunsafeCoerce -> Just $ \s -> \case xs@(x@(hnf -> NonNeut): _{-2-}) -> x; xs -> f s xs |
490 | FreflCstr -> Just $ \case _ -> TT | 492 | FreflCstr -> Just $ \s -> \case _ -> TT |
491 | FhlistNilCase -> Just $ \case ((hnf -> Con n@(ConName _ 0 _) _ _): x: _{-1-}) -> x; xs -> f xs | 493 | FhlistNilCase -> Just $ \s -> \case ((hnf -> Con n@(ConName _ 0 _) _ _): x: _{-1-}) -> x; xs -> f s xs |
492 | FhlistConsCase -> Just $ \case ((hnf -> Con n@(ConName _ 1 _) _ (b: a: _{-2-})): x: _{-3-}) -> x `app_` a `app_` b; xs -> f xs | 494 | FhlistConsCase -> Just $ \s -> \case ((hnf -> Con n@(ConName _ 1 _) _ (b: a: _{-2-})): x: _{-3-}) -> x `app_` a `app_` b; xs -> f s xs |
493 | 495 | ||
494 | -- general compiler primitives | 496 | -- general compiler primitives |
495 | FprimAddInt -> Just $ \case (HInt j: HInt i: _) -> HInt (i + j); xs -> f xs | 497 | FprimAddInt -> Just $ \s -> \case (HInt j: HInt i: _) -> HInt (i + j); xs -> f s xs |
496 | FprimSubInt -> Just $ \case (HInt j: HInt i: _) -> HInt (i - j); xs -> f xs | 498 | FprimSubInt -> Just $ \s -> \case (HInt j: HInt i: _) -> HInt (i - j); xs -> f s xs |
497 | FprimModInt -> Just $ \case (HInt j: HInt i: _) -> HInt (i `mod` j); xs -> f xs | 499 | FprimModInt -> Just $ \s -> \case (HInt j: HInt i: _) -> HInt (i `mod` j); xs -> f s xs |
498 | FprimSqrtFloat -> Just $ \case (HFloat i: _) -> HFloat $ sqrt i; xs -> f xs | 500 | FprimSqrtFloat -> Just $ \s -> \case (HFloat i: _) -> HFloat $ sqrt i; xs -> f s xs |
499 | FprimRound -> Just $ \case (HFloat i: _) -> HInt $ round i; xs -> f xs | 501 | FprimRound -> Just $ \s -> \case (HFloat i: _) -> HInt $ round i; xs -> f s xs |
500 | FprimIntToFloat -> Just $ \case (HInt i: _) -> HFloat $ fromIntegral i; xs -> f xs | 502 | FprimIntToFloat -> Just $ \s -> \case (HInt i: _) -> HFloat $ fromIntegral i; xs -> f s xs |
501 | FprimIntToNat -> Just $ \case (HInt i: _) -> ENat $ fromIntegral i; xs -> f xs | 503 | FprimIntToNat -> Just $ \s -> \case (HInt i: _) -> ENat $ fromIntegral i; xs -> f s xs |
502 | FprimCompareInt -> Just $ \case (HInt y: HInt x: _) -> mkOrdering $ x `compare` y; xs -> f xs | 504 | FprimCompareInt -> Just $ \s -> \case (HInt y: HInt x: _) -> mkOrdering $ x `compare` y; xs -> f s xs |
503 | FprimCompareFloat -> Just $ \case (HFloat y: HFloat x: _) -> mkOrdering $ x `compare` y; xs -> f xs | 505 | FprimCompareFloat -> Just $ \s -> \case (HFloat y: HFloat x: _) -> mkOrdering $ x `compare` y; xs -> f s xs |
504 | FprimCompareChar -> Just $ \case (HChar y: HChar x: _) -> mkOrdering $ x `compare` y; xs -> f xs | 506 | FprimCompareChar -> Just $ \s -> \case (HChar y: HChar x: _) -> mkOrdering $ x `compare` y; xs -> f s xs |
505 | FprimCompareString -> Just $ \case (HString y: HString x: _) -> mkOrdering $ x `compare` y; xs -> f xs | 507 | FprimCompareString -> Just $ \s -> \case (HString y: HString x: _) -> mkOrdering $ x `compare` y; xs -> f s xs |
506 | 508 | ||
507 | -- LambdaCube 3D specific primitives | 509 | -- LambdaCube 3D specific primitives |
508 | FPrimGreaterThan -> Just $ \case (y: x: _{-7-}) | Just r <- twoOpBool (>) x y -> r; xs -> f xs | 510 | FPrimGreaterThan -> Just $ \s -> \case (y: x: _{-7-}) | Just r <- twoOpBool (>) x y -> r; xs -> f s xs |
509 | FPrimGreaterThanEqual | 511 | FPrimGreaterThanEqual |
510 | -> Just $ \case (y: x: _{-7-}) | Just r <- twoOpBool (>=) x y -> r; xs -> f xs | 512 | -> Just $ \s -> \case (y: x: _{-7-}) | Just r <- twoOpBool (>=) x y -> r; xs -> f s xs |
511 | FPrimLessThan -> Just $ \case (y: x: _{-7-}) | Just r <- twoOpBool (<) x y -> r; xs -> f xs | 513 | FPrimLessThan -> Just $ \s -> \case (y: x: _{-7-}) | Just r <- twoOpBool (<) x y -> r; xs -> f s xs |
512 | FPrimLessThanEqual -> Just $ \case (y: x: _{-7-}) | Just r <- twoOpBool (<=) x y -> r; xs -> f xs | 514 | FPrimLessThanEqual -> Just $ \s -> \case (y: x: _{-7-}) | Just r <- twoOpBool (<=) x y -> r; xs -> f s xs |
513 | FPrimEqualV -> Just $ \case (y: x: _{-7-}) | Just r <- twoOpBool (==) x y -> r; xs -> f xs | 515 | FPrimEqualV -> Just $ \s -> \case (y: x: _{-7-}) | Just r <- twoOpBool (==) x y -> r; xs -> f s xs |
514 | FPrimNotEqualV -> Just $ \case (y: x: _{-7-}) | Just r <- twoOpBool (/=) x y -> r; xs -> f xs | 516 | FPrimNotEqualV -> Just $ \s -> \case (y: x: _{-7-}) | Just r <- twoOpBool (/=) x y -> r; xs -> f s xs |
515 | FPrimEqual -> Just $ \case (y: x: _{-3-}) | Just r <- twoOpBool (==) x y -> r; xs -> f xs | 517 | FPrimEqual -> Just $ \s -> \case (y: x: _{-3-}) | Just r <- twoOpBool (==) x y -> r; xs -> f s xs |
516 | FPrimNotEqual -> Just $ \case (y: x: _{-3-}) | Just r <- twoOpBool (/=) x y -> r; xs -> f xs | 518 | FPrimNotEqual -> Just $ \s -> \case (y: x: _{-3-}) | Just r <- twoOpBool (/=) x y -> r; xs -> f s xs |
517 | FPrimSubS -> Just $ \case (y: x: _{-4-}) | Just r <- twoOp (-) x y -> r; xs -> f xs | 519 | FPrimSubS -> Just $ \s -> \case (y: x: _{-4-}) | Just r <- twoOp (-) x y -> r; xs -> f s xs |
518 | FPrimSub -> Just $ \case (y: x: _{-2-}) | Just r <- twoOp (-) x y -> r; xs -> f xs | 520 | FPrimSub -> Just $ \s -> \case (y: x: _{-2-}) | Just r <- twoOp (-) x y -> r; xs -> f s xs |
519 | FPrimAddS -> Just $ \case (y: x: _{-4-}) | Just r <- twoOp (+) x y -> r; xs -> f xs | 521 | FPrimAddS -> Just $ \s -> \case (y: x: _{-4-}) | Just r <- twoOp (+) x y -> r; xs -> f s xs |
520 | FPrimAdd -> Just $ \case (y: x: _{-2-}) | Just r <- twoOp (+) x y -> r; xs -> f xs | 522 | FPrimAdd -> Just $ \s -> \case (y: x: _{-2-}) | Just r <- twoOp (+) x y -> r; xs -> f s xs |
521 | FPrimMulS -> Just $ \case (y: x: _{-4-}) | Just r <- twoOp (*) x y -> r; xs -> f xs | 523 | FPrimMulS -> Just $ \s -> \case (y: x: _{-4-}) | Just r <- twoOp (*) x y -> r; xs -> f s xs |
522 | FPrimMul -> Just $ \case (y: x: _{-2-}) | Just r <- twoOp (*) x y -> r; xs -> f xs | 524 | FPrimMul -> Just $ \s -> \case (y: x: _{-2-}) | Just r <- twoOp (*) x y -> r; xs -> f s xs |
523 | FPrimDivS -> Just $ \case (y: x: _{-5-}) | Just r <- twoOp_ (/) div x y -> r; xs -> f xs | 525 | FPrimDivS -> Just $ \s -> \case (y: x: _{-5-}) | Just r <- twoOp_ (/) div x y -> r; xs -> f s xs |
524 | FPrimDiv -> Just $ \case (y: x: _{-5-}) | Just r <- twoOp_ (/) div x y -> r; xs -> f xs | 526 | FPrimDiv -> Just $ \s -> \case (y: x: _{-5-}) | Just r <- twoOp_ (/) div x y -> r; xs -> f s xs |
525 | FPrimModS -> Just $ \case (y: x: _{-5-}) | Just r <- twoOp_ modF mod x y -> r; xs -> f xs | 527 | FPrimModS -> Just $ \s -> \case (y: x: _{-5-}) | Just r <- twoOp_ modF mod x y -> r; xs -> f s xs |
526 | FPrimMod -> Just $ \case (y: x: _{-5-}) | Just r <- twoOp_ modF mod x y -> r; xs -> f xs | 528 | FPrimMod -> Just $ \s -> \case (y: x: _{-5-}) | Just r <- twoOp_ modF mod x y -> r; xs -> f s xs |
527 | FPrimNeg -> Just $ \case (x: _{-1-}) | Just r <- oneOp negate x -> r; xs -> f xs | 529 | FPrimNeg -> Just $ \s -> \case (x: _{-1-}) | Just r <- oneOp negate x -> r; xs -> f s xs |
528 | FPrimAnd -> Just $ \case (EBool y: EBool x: _) -> EBool (x && y); xs -> f xs | 530 | FPrimAnd -> Just $ \s -> \case (EBool y: EBool x: _) -> EBool (x && y); xs -> f s xs |
529 | FPrimOr -> Just $ \case (EBool y: EBool x: _) -> EBool (x || y); xs -> f xs | 531 | FPrimOr -> Just $ \s -> \case (EBool y: EBool x: _) -> EBool (x || y); xs -> f s xs |
530 | FPrimXor -> Just $ \case (EBool y: EBool x: _) -> EBool (x /= y); xs -> f xs | 532 | FPrimXor -> Just $ \s -> \case (EBool y: EBool x: _) -> EBool (x /= y); xs -> f s xs |
531 | FPrimNot -> Just $ \case (EBool x: _: _: (hnf -> TNat): _) -> EBool $ not x; xs -> f xs | 533 | FPrimNot -> Just $ \s -> \case (EBool x: _: _: (hnf -> TNat): _) -> EBool $ not x; xs -> f s xs |
532 | 534 | ||
533 | _ -> Nothing | 535 | _ -> Nothing |
534 | 536 | ||
537 | f s xs = Neut $ Fun_ s fn xs delta | ||
538 | |||
535 | twoOpBool :: (forall a . Ord a => a -> a -> Bool) -> Exp -> Exp -> Maybe Exp | 539 | twoOpBool :: (forall a . Ord a => a -> a -> Bool) -> Exp -> Exp -> Maybe Exp |
536 | twoOpBool f (HFloat x) (HFloat y) = Just $ EBool $ f x y | 540 | twoOpBool f (HFloat x) (HFloat y) = Just $ EBool $ f x y |
537 | twoOpBool f (HInt x) (HInt y) = Just $ EBool $ f x y | 541 | twoOpBool f (HInt x) (HInt y) = Just $ EBool $ f x y |
@@ -621,16 +625,20 @@ nonNeut _ = True | |||
621 | t2C (hnf -> TT) (hnf -> TT) = TT | 625 | t2C (hnf -> TT) (hnf -> TT) = TT |
622 | t2C a b = DFun Ft2C [b, a] | 626 | t2C a b = DFun Ft2C [b, a] |
623 | 627 | ||
624 | cw (hnf -> CUnit) = Unit | 628 | cw_ _ (hnf -> CUnit) = Unit |
625 | cw (hnf -> CEmpty a) = Empty a | 629 | cw_ _ (hnf -> CEmpty a) = Empty a |
626 | cw a = CW a | 630 | cw_ s a = CW_ s a |
631 | |||
632 | cw a = cw_ (getFreeVars a) a | ||
633 | |||
634 | t2_ _ (hnf -> CUnit) a = a | ||
635 | t2_ _ a (hnf -> CUnit) = a | ||
636 | t2_ _ (hnf -> CEmpty a) (hnf -> CEmpty b) = CEmpty (a <> b) | ||
637 | t2_ _ (hnf -> CEmpty s) _ = CEmpty s | ||
638 | t2_ _ _ (hnf -> CEmpty s) = CEmpty s | ||
639 | t2_ s a b = T2 s a b | ||
627 | 640 | ||
628 | t2 (hnf -> CUnit) a = a | 641 | t2 a b = t2_ (getFreeVars a <> getFreeVars b) a b |
629 | t2 a (hnf -> CUnit) = a | ||
630 | t2 (hnf -> CEmpty a) (hnf -> CEmpty b) = CEmpty (a <> b) | ||
631 | t2 (hnf -> CEmpty s) _ = CEmpty s | ||
632 | t2 _ (hnf -> CEmpty s) = CEmpty s | ||
633 | t2 a b = T2 a b | ||
634 | 642 | ||
635 | app_ :: Exp -> Exp -> Exp | 643 | app_ :: Exp -> Exp -> Exp |
636 | app_ a b = app__ (getFreeVars a <> getFreeVars b) a b | 644 | app_ a b = app__ (getFreeVars a <> getFreeVars b) a b |
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index a03ac8f9..5067487c 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -356,7 +356,7 @@ inferN_ tellTrace = infer where | |||
356 | | ELHS n te' <- te -> refocus (ELHS n $ EBind2_ si BMeta tt_ te') eet | 356 | | ELHS n te' <- te -> refocus (ELHS n $ EBind2_ si BMeta tt_ te') eet |
357 | | Unit <- tt -> refocus te $ subst 0 TT eet | 357 | | Unit <- tt -> refocus te $ subst 0 TT eet |
358 | | Empty msg <- tt -> throwError' $ ETypeError (text msg) si | 358 | | Empty msg <- tt -> throwError' $ ETypeError (text msg) si |
359 | | CW (hnf -> T2 x y) <- tt, let te' = EBind2_ si BMeta (up 1 $ cw y) $ EBind2_ si BMeta (cw x) te | 359 | | CW (hnf -> T2 _ x y) <- tt, let te' = EBind2_ si BMeta (up 1 $ cw y) $ EBind2_ si BMeta (cw x) te |
360 | -> refocus te' $ subst 2 (t2C (Var 1) (Var 0)) $ up 2 eet | 360 | -> refocus te' $ subst 2 (t2C (Var 1) (Var 0)) $ up 2 eet |
361 | | CW (hnf -> CstrT t a b) <- tt, Just r <- cst (ET a t) b -> r | 361 | | CW (hnf -> CstrT t a b) <- tt, Just r <- cst (ET a t) b -> r |
362 | | CW (hnf -> CstrT t a b) <- tt, Just r <- cst (ET b t) a -> r | 362 | | CW (hnf -> CstrT t a b) <- tt, Just r <- cst (ET b t) a -> r |