diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-04-06 17:28:17 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-04-06 17:28:17 +0200 |
commit | 205fd10c52e933557bedf0e8af1454ba88928313 (patch) | |
tree | 6c6221253fb71901d775a9a2bd5c52ffbe6a66ee /prototypes | |
parent | 200d77d107277ce4d747e64dbe3ec01a679cea08 (diff) |
simplification
Diffstat (limited to 'prototypes')
-rw-r--r-- | prototypes/ShiftReducer.hs | 160 |
1 files changed, 69 insertions, 91 deletions
diff --git a/prototypes/ShiftReducer.hs b/prototypes/ShiftReducer.hs index ae515b08..97e589a7 100644 --- a/prototypes/ShiftReducer.hs +++ b/prototypes/ShiftReducer.hs | |||
@@ -433,66 +433,30 @@ instance Show Lit where | |||
433 | 433 | ||
434 | ------------------------------------------------------------ expressions | 434 | ------------------------------------------------------------ expressions |
435 | 435 | ||
436 | data Exp_ a b c d e | 436 | data Exp e |
437 | = ELit_ Lit | 437 | = ELit Lit |
438 | | EVar_ a -- a = () means that the variable de bruijn index is 0 (the only possible index if the exprssion is compact) | 438 | | EVar |
439 | -- a = Int is the de bruijn index (in cases when the exprssion is not compactified) | 439 | | ELamD (Exp e) -- lambda with unused argument |
440 | | ELamD_ b -- lambda with unused argument | 440 | | ELam (WithLet (Exp e)) -- lambda with used argument |
441 | -- b is usually (Exp_ a b c d e) | 441 | | EApp (Shift (Exp e)) (Shift (Exp e)) -- application |
442 | | ELam_ c -- lambda with used argument | 442 | | RHS e -- marks the beginning of right hand side (parts right to the equal sign) in fuction definitions |
443 | -- c usually contains a MaybeLet layer | 443 | -- e is either RHSExp or Void; Void means that this constructor cannot be used |
444 | | EApp_ d d -- application | 444 | deriving (Eq, Show) |
445 | -- d usually contains a Shift layer | ||
446 | | RHS_ e -- marks the beginning of right hand side (parts right to the equal sign) in fuction definitions | ||
447 | -- e is usually (Exp_ a b c d e) | ||
448 | -- e = Void means that this constructor cannot be used | ||
449 | deriving (Eq, Show) --, Generic) | ||
450 | |||
451 | -------------------------------------------------------- | ||
452 | |||
453 | type WithLet a = MaybeLet (Shift LHSExp) a a | ||
454 | |||
455 | -- right-hand-side expression (no RHS constructors inside) | ||
456 | newtype Exp = Exp (Exp_ () Exp (WithLet Exp) (Shift Exp) Void) | ||
457 | deriving (Eq) | ||
458 | |||
459 | pattern ELit l = Exp (ELit_ l) | ||
460 | pattern EApp a b = Exp (EApp_ a b) | ||
461 | pattern ELam i = Exp (ELam_ i) | ||
462 | pattern ELamD i = Exp (ELamD_ i) | ||
463 | pattern EVar i = Exp (EVar_ i) | ||
464 | |||
465 | pattern EInt i = ELit (LInt i) | ||
466 | 445 | ||
446 | -- right-hand-side expression (no RHS constructor) | ||
447 | type RHSExp = Exp Void | ||
467 | -- left-hand-side expression (allows RHS constructor) | 448 | -- left-hand-side expression (allows RHS constructor) |
468 | newtype LHSExp = LHSExp (Exp_ () LHSExp (WithLet LHSExp) (Shift LHSExp) Exp) | 449 | type LHSExp = Exp RHSExp |
469 | deriving (Eq, Show) | ||
470 | 450 | ||
471 | pattern RHS i = LHSExp (RHS_ i) | 451 | type WithLet a = MaybeLet (Shift LHSExp) a a |
472 | 452 | ||
473 | -------------------------------------------------------- | 453 | -------------------------------------------------------- |
474 | 454 | ||
475 | type SExp = Shift Exp | 455 | type SExp = Shift RHSExp |
476 | type LExp = WithLet Exp | 456 | type LExp = WithLet RHSExp |
477 | 457 | type SLExp = Shift (WithLet RHSExp) -- SLExp is *the* expression type in the user API | |
478 | -- SLExp is *the* expression type in the user API | ||
479 | type SLExp = Shift (WithLet Exp) | ||
480 | 458 | ||
481 | sFun p s xs c = parens $ \c -> s ++ foldr (\f c -> ' ': f c) c xs | 459 | instance GetDBUsed RHSExp where |
482 | where | ||
483 | parens x | ||
484 | | p < 10 = x c | ||
485 | | otherwise = '(': x (')': c) | ||
486 | |||
487 | instance Show Exp where | ||
488 | showsPrec p = \case | ||
489 | ELit i -> shows i | ||
490 | EApp a b -> sFun p "EApp" [showsPrec 10 a, showsPrec 10 b] | ||
491 | ELam a -> sFun p "ELam" [showsPrec 10 a] | ||
492 | ELamD a -> sFun p "ELamD" [showsPrec 10 a] | ||
493 | EVar () -> ("EVar" ++) | ||
494 | |||
495 | instance GetDBUsed Exp where | ||
496 | getDBUsed = \case | 460 | getDBUsed = \case |
497 | EApp (Shift ua a) (Shift ub b) -> ua <> ub | 461 | EApp (Shift ua a) (Shift ub b) -> ua <> ub |
498 | ELit{} -> mempty | 462 | ELit{} -> mempty |
@@ -500,7 +464,7 @@ instance GetDBUsed Exp where | |||
500 | ELamD e -> sTail $ getDBUsed e | 464 | ELamD e -> sTail $ getDBUsed e |
501 | ELam e -> sTail $ getDBUsed e | 465 | ELam e -> sTail $ getDBUsed e |
502 | 466 | ||
503 | instance Arbitrary Exp where | 467 | instance Arbitrary RHSExp where |
504 | arbitrary = (\(Shift _ (NoLet e)) -> e) . getSimpleExp <$> arbitrary | 468 | arbitrary = (\(Shift _ (NoLet e)) -> e) . getSimpleExp <$> arbitrary |
505 | -- shrink = genericShrink | 469 | -- shrink = genericShrink |
506 | 470 | ||
@@ -516,15 +480,17 @@ instance Arbitrary SimpleExp where | |||
516 | , lam <$> (getSimpleExp <$> arbitrary) | 480 | , lam <$> (getSimpleExp <$> arbitrary) |
517 | ] | 481 | ] |
518 | 482 | ||
483 | pattern SLLit l <- (getLit -> Just l) where SLLit = Shift mempty . NoLet . ELit | ||
484 | |||
519 | getLit :: SLExp -> Maybe Lit | 485 | getLit :: SLExp -> Maybe Lit |
520 | getLit (Shift _ (NoLet (ELit l))) = Just l | 486 | getLit (Shift _ (NoLet (ELit l))) = Just l |
521 | getLit (Shift _ (HasLet (Let _ (Shift _ (ELit l))))) = Just l | 487 | getLit (Shift _ (HasLet (Let _ (Shift _ (ELit l))))) = Just l |
522 | getLit _ = Nothing | 488 | getLit _ = Nothing |
523 | 489 | ||
524 | pattern Int i <- (getLit -> Just (LInt i)) where Int = Shift mempty . NoLet . EInt | 490 | pattern Int i = SLLit (LInt i) |
525 | 491 | ||
526 | var :: Int -> SLExp | 492 | var :: Int -> SLExp |
527 | var i = fmap NoLet $ up_ 0 i $ mkShift $ EVar () | 493 | var i = fmap NoLet $ up_ 0 i $ mkShift EVar |
528 | 494 | ||
529 | prop_upVar (getNonNegative -> k) (getNonNegative -> n) (getNonNegative -> i) = up_ k n (var i) == var (if k <= i then n + i else i) | 495 | prop_upVar (getNonNegative -> k) (getNonNegative -> n) (getNonNegative -> i) = up_ k n (var i) == var (if k <= i then n + i else i) |
530 | prop_downVar (getNonNegative -> k) (getNonNegative -> i) = down_ k (var i) == case compare k i of LT -> Just (var $ i-1); EQ -> Nothing; GT -> Just (var i) | 496 | prop_downVar (getNonNegative -> k) (getNonNegative -> i) = down_ k (var i) == case compare k i of LT -> Just (var $ i-1); EQ -> Nothing; GT -> Just (var i) |
@@ -534,7 +500,7 @@ lam (Shift u e) = Shift (sTail u) $ if sHead u then eLam e else eLamD e | |||
534 | where | 500 | where |
535 | eLam (NoLet e) = NoLet $ ELam $ NoLet e | 501 | eLam (NoLet e) = NoLet $ ELam $ NoLet e |
536 | -- TODO: improve this by let-floating | 502 | -- TODO: improve this by let-floating |
537 | eLam x = NoLet $ ELam x | 503 | eLam (HasLet (Let m (Shift u x))) = NoLet $ ELam (HasLet (Let m (Shift u x))) |
538 | 504 | ||
539 | eLamD (NoLet e) = NoLet $ ELamD e | 505 | eLamD (NoLet e) = NoLet $ ELamD e |
540 | -- TODO: review | 506 | -- TODO: review |
@@ -552,7 +518,7 @@ app x y = f x y | |||
552 | f (Shift ula la) (Shift ulb (HasLet lb)) = g app ula la ulb lb | 518 | f (Shift ula la) (Shift ulb (HasLet lb)) = g app ula la ulb lb |
553 | f (Shift ulb (HasLet lb)) (Shift ula la) = g (flip app) ula la ulb lb | 519 | f (Shift ulb (HasLet lb)) (Shift ula la) = g (flip app) ula la ulb lb |
554 | 520 | ||
555 | g :: (SLExp -> SLExp -> SLExp) -> DBUsed -> LExp -> DBUsed -> Let (Shift LHSExp) (Shift Exp) -> SLExp | 521 | g :: (SLExp -> SLExp -> SLExp) -> DBUsed -> LExp -> DBUsed -> Let (Shift LHSExp) (Shift RHSExp) -> SLExp |
556 | g app ula la ulb lb | 522 | g app ula la ulb lb |
557 | = up u $ lets {-Shift u $-} | 523 | = up u $ lets {-Shift u $-} |
558 | -- app (Shift ula' la) (Shift ulb' lb) | 524 | -- app (Shift ula' la) (Shift ulb' lb) |
@@ -580,25 +546,25 @@ let1 i (Shift u (HasLet l)) = lets $ m <> Map.singleton i' (RHS <$> e) | |||
580 | 546 | ||
581 | --------------------------------------------------------- | 547 | --------------------------------------------------------- |
582 | {- | 548 | {- |
583 | newtype ExpS = ExpS (Exp_ Int ExpS (MaybeLet SExp ExpS Exp) SExp) | 549 | newtype ExpS = ExpS (Exp Int ExpS (MaybeLet SExp ExpS RHSExp) SExp) |
584 | deriving (Eq, Show) | 550 | deriving (Eq, Show) |
585 | 551 | ||
586 | pushShift :: SExp -> ExpS | 552 | pushShift :: SExp -> ExpS |
587 | pushShift (Shift u e) = ExpS $ case e of | 553 | pushShift (Shift u e) = ExpS $ case e of |
588 | EApp a b -> EApp_ (up u a) (up u b) | 554 | EApp a b -> EApp (up u a) (up u b) |
589 | ELit i -> ELit_ i | 555 | ELit i -> ELit i |
590 | EVar{} -> EVar_ $ fromJust $ indexTrans u 0 | 556 | EVar{} -> EVar $ fromJust $ indexTrans u 0 |
591 | ELamD e -> ELamD_ $ pushShift $ Shift (cons False u) e | 557 | ELamD e -> ELamD $ pushShift $ Shift (cons False u) e |
592 | ELam (NoLet e) -> ELam_ $ NoLet $ pushShift $ Shift (cons True u) e | 558 | ELam (NoLet e) -> ELam $ NoLet $ pushShift $ Shift (cons True u) e |
593 | LHS a b -> LHS_ a (up u <$> b) -- ??? $ SData (pushShift $ Shift u c) | 559 | LHS a b -> LHS_ a (up u <$> b) -- ??? $ SData (pushShift $ Shift u c) |
594 | -- Delta x -> Delta_ $ SData x | 560 | -- Delta x -> Delta_ $ SData x |
595 | 561 | ||
596 | prop_var (getNonNegative -> i) = case pushShift (fromLet $ var i) of | 562 | prop_var (getNonNegative -> i) = case pushShift (fromLet $ var i) of |
597 | ExpS (EVar_ i') -> i == i' | 563 | ExpS (EVar i') -> i == i' |
598 | _ -> False | 564 | _ -> False |
599 | 565 | ||
600 | prop_app (getSimpleExp -> a) (getSimpleExp -> b) = case pushShift $ fromLet $ app a b of | 566 | prop_app (getSimpleExp -> a) (getSimpleExp -> b) = case pushShift $ fromLet $ app a b of |
601 | ExpS (EApp_ a' b') -> (a', b') == (fromLet a, fromLet b) | 567 | ExpS (EApp a' b') -> (a', b') == (fromLet a, fromLet b) |
602 | _ -> False | 568 | _ -> False |
603 | 569 | ||
604 | --prop_lam (getNonNegative -> i) = elimShift undefined undefined undefined (==i) (var i) | 570 | --prop_lam (getNonNegative -> i) = elimShift undefined undefined undefined (==i) (var i) |
@@ -607,39 +573,39 @@ prop_app (getSimpleExp -> a) (getSimpleExp -> b) = case pushShift $ fromLet $ ap | |||
607 | 573 | ||
608 | --------------------------------------------------------- | 574 | --------------------------------------------------------- |
609 | 575 | ||
610 | newtype ExpL = ExpL (Exp_ Int SLExp SLExp SLExp) | 576 | newtype ExpL = ExpL (Exp Int SLExp SLExp SLExp) |
611 | deriving (Eq, Show) | 577 | deriving (Eq, Show) |
612 | {- | 578 | {- |
613 | pushLet :: LExp -> ExpL | 579 | pushLet :: LExp -> ExpL |
614 | pushLet (NoLet e) = ExpL $ case e of | 580 | pushLet (NoLet e) = ExpL $ case e of |
615 | EInt i -> EInt_ i | 581 | EInt i -> EInt_ i |
616 | EApp a b -> EApp_ (NoLet <$> a) (NoLet <$> b) | 582 | EApp a b -> EApp (NoLet <$> a) (NoLet <$> b) |
617 | EVar{} -> EVar_ 0 | 583 | EVar{} -> EVar 0 |
618 | -- ELam a -> ELam_ $ mkShift a | 584 | -- ELam a -> ELam $ mkShift a |
619 | ELamD a -> ELamD_ $ NoLet <$> mkShift a | 585 | ELamD a -> ELamD $ NoLet <$> mkShift a |
620 | pushLet (HasLet (Let m e)) = ExpL $ case pushShift e of | 586 | pushLet (HasLet (Let m e)) = ExpL $ case pushShift e of |
621 | ExpS e' -> case e' of | 587 | ExpS e' -> case e' of |
622 | EApp_ a b -> EApp_ (fmap HasLet (mkLet m a)) (fmap HasLet (mkLet m b)) | 588 | EApp a b -> EApp (fmap HasLet (mkLet m a)) (fmap HasLet (mkLet m b)) |
623 | EInt_ i -> EInt_ i | 589 | EInt_ i -> EInt_ i |
624 | EVar_ i -> EVar_ i | 590 | EVar i -> EVar i |
625 | -} | 591 | -} |
626 | pushLet' :: SLExp -> ExpL | 592 | pushLet' :: SLExp -> ExpL |
627 | pushLet' (Shift u l) = case l of | 593 | pushLet' (Shift u l) = case l of |
628 | NoLet e -> {-case pushShift (Shift u e) of | 594 | NoLet e -> {-case pushShift (Shift u e) of |
629 | ExpS e -> -} ExpL $ case e of | 595 | ExpS e -> -} ExpL $ case e of |
630 | ELit i -> ELit_ i | 596 | ELit i -> ELit i |
631 | EApp a b -> EApp_ (NoLet <$> up u a) (NoLet <$> up u b) | 597 | EApp a b -> EApp (NoLet <$> up u a) (NoLet <$> up u b) |
632 | EVar () -> EVar_ $ fromJust $ indexTrans u 0 | 598 | EVar () -> EVar $ fromJust $ indexTrans u 0 |
633 | ELam a -> ELam_ $ Shift (cons True u) a | 599 | ELam a -> ELam $ Shift (cons True u) a |
634 | -- ELamD_ a -> ELamD_ $ NoLet a | 600 | -- ELamD a -> ELamD $ NoLet a |
635 | LHS a b -> LHS_ a ((fmap NoLet . up u) <$> b) | 601 | LHS a b -> LHS_ a ((fmap NoLet . up u) <$> b) |
636 | HasLet l -> case Shift u l of | 602 | HasLet l -> case Shift u l of |
637 | PShiftLet m e -> case pushShift e of | 603 | PShiftLet m e -> case pushShift e of |
638 | ExpS e' -> case e' of | 604 | ExpS e' -> case e' of |
639 | EApp_ a b -> ExpL $ EApp_ (fmap HasLet (mkLet m a)) (fmap HasLet (mkLet m b)) | 605 | EApp a b -> ExpL $ EApp (fmap HasLet (mkLet m a)) (fmap HasLet (mkLet m b)) |
640 | ELit_ i -> ExpL $ ELit_ i | 606 | ELit i -> ExpL $ ELit i |
641 | EVar_ i -> case Map.lookup i m of | 607 | EVar i -> case Map.lookup i m of |
642 | Nothing -> ExpL $ EVar_ i | 608 | Nothing -> ExpL $ EVar i |
643 | Just x -> pushLet' $ lets m $ NoLet <$> x | 609 | Just x -> pushLet' $ lets m $ NoLet <$> x |
644 | LHS_ a b -> error "efun" | 610 | LHS_ a b -> error "efun" |
645 | -- Delta_ f -> ExpL $ Delta_ f | 611 | -- Delta_ f -> ExpL $ Delta_ f |
@@ -649,17 +615,27 @@ pushLet' (Shift u l) = case l of | |||
649 | hnf :: SLExp -> ExpL | 615 | hnf :: SLExp -> ExpL |
650 | hnf e = case pushLet' e of | 616 | hnf e = case pushLet' e of |
651 | (ExpL (LHS_ "add" [_, _])) -> error "ok" | 617 | (ExpL (LHS_ "add" [_, _])) -> error "ok" |
652 | x@(ExpL (EApp_ a b)) -> case hnf a of | 618 | x@(ExpL (EApp a b)) -> case hnf a of |
653 | ExpL (ELam_ a) -> hnf $ let1 0 b a | 619 | ExpL (ELam a) -> hnf $ let1 0 b a |
654 | ExpL (LHS_ n acc) -> hnf $ LHS n (_ b: acc) | 620 | ExpL (LHS_ n acc) -> hnf $ LHS n (_ b: acc) |
655 | _ -> x | 621 | _ -> x |
656 | x -> x | 622 | x -> x |
657 | 623 | ||
658 | ----------------------------------------------------------------------------------- | 624 | {- pattern synonyms |
625 | |||
626 | - BReduce e : at least one step of beta reduction, e is the result | ||
627 | - Lit: a literal, after all kind of possible reductions | ||
628 | - App | ||
629 | - after reduction | ||
630 | - before reduction | ||
631 | |||
632 | -} | ||
659 | 633 | ||
634 | ----------------------------------------------------------------------------------- | ||
635 | -} | ||
660 | idE :: SLExp | 636 | idE :: SLExp |
661 | idE = lam $ var 0 | 637 | idE = lam $ var 0 |
662 | 638 | {- | |
663 | add :: SLExp | 639 | add :: SLExp |
664 | add = NoLet <$> mkShift (LHS "add" []) -- $ ELam $ NoLet $ ELam $ NoLet $ Delta f) | 640 | add = NoLet <$> mkShift (LHS "add" []) -- $ ELam $ NoLet $ ELam $ NoLet $ Delta f) |
665 | where | 641 | where |
@@ -681,16 +657,18 @@ runTests = $quickCheckAll | |||
681 | {- | 657 | {- |
682 | TODO | 658 | TODO |
683 | 659 | ||
684 | - primes example running | 660 | - primes example running ~ 3 days |
685 | - speed up eliminators with caching | 661 | - speed up eliminators with caching ~ 3 days |
686 | - write performance tests | 662 | - write performance tests (primes + ?) |
687 | - speed up Boolean streams with compression | 663 | - speed up Boolean streams with compression ~ 3 days |
688 | - check that all operations is available and efficient | 664 | - gc speedup ~ 2 days |
665 | - check that all operations is available and efficient ~ 1 day | ||
689 | - up, down | 666 | - up, down |
690 | - subst | 667 | - subst |
691 | - constructions | 668 | - constructions |
692 | - lam, pi, app, var, lit, ... | 669 | - lam, pi, app, var, lit, ... |
693 | - eliminations | 670 | - eliminations |
671 | |||
694 | - intergrate into the compiler | 672 | - intergrate into the compiler |
695 | -} | 673 | -} |
696 | 674 | ||