diff options
-rw-r--r-- | prototypes/TCReduce.hs | 10 | ||||
-rw-r--r-- | prototypes/primes.lam | 15 |
2 files changed, 8 insertions, 17 deletions
diff --git a/prototypes/TCReduce.hs b/prototypes/TCReduce.hs index 269d4d0f..e74b58e0 100644 --- a/prototypes/TCReduce.hs +++ b/prototypes/TCReduce.hs | |||
@@ -564,7 +564,6 @@ evv = \case | |||
564 | Snd -> \(_, x) -> x | 564 | Snd -> \(_, x) -> x |
565 | NY (evv1 -> a) Fst -> \(x, _) -> a x | 565 | NY (evv1 -> a) Fst -> \(x, _) -> a x |
566 | 566 | ||
567 | Skip (Init (T2 Snd)) -> \a0 a1 -> a1 | ||
568 | Skip (Init (T2 (evv -> x))) -> \a0 a1 -> x ((), a1) | 567 | Skip (Init (T2 (evv -> x))) -> \a0 a1 -> x ((), a1) |
569 | Skip Id -> \_ x -> x | 568 | Skip Id -> \_ x -> x |
570 | Skip (evv -> x) -> \_ -> x | 569 | Skip (evv -> x) -> \_ -> x |
@@ -661,6 +660,9 @@ Id `ny` x = x | |||
661 | x `ny` Id = x | 660 | x `ny` Id = x |
662 | x `ny` y = NY x y | 661 | x `ny` y = NY x y |
663 | 662 | ||
663 | init' (T2 Snd) = Id | ||
664 | init' x = Init x | ||
665 | |||
664 | -------------------------------------------------------------------------------- | 666 | -------------------------------------------------------------------------------- |
665 | 667 | ||
666 | uGV :: GV a -> GV b | 668 | uGV :: GV a -> GV b |
@@ -703,7 +705,7 @@ evva_ ss = \case | |||
703 | z@(getLams -> Just (i, x)) | 705 | z@(getLams -> Just (i, x)) |
704 | | b -> Skip $ case i of | 706 | | b -> Skip $ case i of |
705 | False -> uGV evva'x | 707 | False -> uGV evva'x |
706 | True -> uGV $ Init $ T2 $ uGV evva'x | 708 | True -> uGV $ init' $ T2 $ uGV evva'x |
707 | | otherwise -> case i of | 709 | | otherwise -> case i of |
708 | False -> uGV $ SkipYN $ uGV evva'x | 710 | False -> uGV $ SkipYN $ uGV evva'x |
709 | True -> uGV $ T2 $ uGV evva'x | 711 | True -> uGV $ T2 $ uGV evva'x |
@@ -742,8 +744,8 @@ evval ((x, _), ty) = (uGV y, tr ty $ evv y) | |||
742 | y = init' $ uGV $ evva_ [] x | 744 | y = init' $ uGV $ evva_ [] x |
743 | tr (VCon (TConName Int _ _ _ _ _) _) x = VInt (unsafeCoerce x :: Int) | 745 | tr (VCon (TConName Int _ _ _ _ _) _) x = VInt (unsafeCoerce x :: Int) |
744 | 746 | ||
745 | init' :: GV (() -> b) -> GV b | 747 | init' :: GV (() -> b) -> GV b |
746 | init' (Skip x) = x | 748 | init' (Skip x) = x |
747 | 749 | ||
748 | -------------------------------------------------------------------------------- interpreter | 750 | -------------------------------------------------------------------------------- interpreter |
749 | 751 | ||
diff --git a/prototypes/primes.lam b/prototypes/primes.lam index f0b7a6b5..c652bbd7 100644 --- a/prototypes/primes.lam +++ b/prototypes/primes.lam | |||
@@ -91,23 +91,12 @@ let tail = | |||
91 | :: forall {a :: *} . List a -> List a | 91 | :: forall {a :: *} . List a -> List a |
92 | 92 | ||
93 | let nth = | 93 | let nth = |
94 | (\a -> fix (Int -> List a -> a) (\f n xs -> | ||
95 | listCase a (\ _ -> a) | ||
96 | (undefined a) | ||
97 | (\ x xs -> boolCase (\ _ -> a) | ||
98 | (f (primSub n #1) xs) | ||
99 | x | ||
100 | (primIntEq #0 n)) | ||
101 | xs)) | ||
102 | :: forall {a :: *} . Int -> List a -> a | ||
103 | {- | ||
104 | let nth = | ||
105 | (\a -> fix (Int -> List a -> a) (\f n xs -> boolCase (\ _ -> a) | 94 | (\a -> fix (Int -> List a -> a) (\f n xs -> boolCase (\ _ -> a) |
106 | (f (primSub n #1) (tail a xs)) | 95 | (listCase a (\ _ -> a) (undefined a) (\x xs -> f (primSub n #1) xs) xs) |
107 | (head a xs) | 96 | (head a xs) |
108 | (primIntEq #0 n))) | 97 | (primIntEq #0 n))) |
109 | :: forall {a :: *} . Int -> List a -> a | 98 | :: forall {a :: *} . Int -> List a -> a |
110 | -} | 99 | |
111 | let takeWhile = | 100 | let takeWhile = |
112 | (\a p -> fix (List a -> List a) (\tw -> listCase a (\ _ -> List a) (Nil a) | 101 | (\a p -> fix (List a -> List a) (\tw -> listCase a (\ _ -> List a) (Nil a) |
113 | (\x xs -> boolCase (\ _ -> List a) | 102 | (\x xs -> boolCase (\ _ -> List a) |