diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-05-24 15:58:19 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-05-24 15:58:19 +0200 |
commit | 2fcc441833425f2e013c43fbfd90e0ef2cb67422 (patch) | |
tree | 1d657119ff03f35bde799d9e22c8d7789fdaa1db | |
parent | 45981b9a6233df6f53680f6011159ce2631e93da (diff) |
refactoring; add hnf marks
-rw-r--r-- | prototypes/FreeVars.hs | 156 | ||||
-rw-r--r-- | prototypes/Inspector.hs | 5 | ||||
-rw-r--r-- | prototypes/LamMachine.hs | 277 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Core.hs | 2 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Pretty.hs | 1 |
5 files changed, 247 insertions, 194 deletions
diff --git a/prototypes/FreeVars.hs b/prototypes/FreeVars.hs new file mode 100644 index 00000000..4ee5eb35 --- /dev/null +++ b/prototypes/FreeVars.hs | |||
@@ -0,0 +1,156 @@ | |||
1 | {-# LANGUAGE OverloadedStrings #-} | ||
2 | {-# LANGUAGE PatternSynonyms #-} | ||
3 | {-# LANGUAGE PatternGuards #-} | ||
4 | {-# LANGUAGE ViewPatterns #-} | ||
5 | {-# LANGUAGE LambdaCase #-} | ||
6 | {-# LANGUAGE ScopedTypeVariables #-} | ||
7 | {-# LANGUAGE TypeSynonymInstances #-} | ||
8 | {-# LANGUAGE FlexibleInstances #-} | ||
9 | {-# LANGUAGE GeneralizedNewtypeDeriving #-} | ||
10 | {-# LANGUAGE BangPatterns #-} | ||
11 | |||
12 | module FreeVars where | ||
13 | |||
14 | import Data.List | ||
15 | import Data.Word | ||
16 | import Data.Int | ||
17 | import Data.Monoid | ||
18 | import Data.Maybe | ||
19 | import Data.Bits | ||
20 | import Control.Arrow | ||
21 | import Control.Category hiding ((.), id) | ||
22 | --import Debug.Trace | ||
23 | |||
24 | import LambdaCube.Compiler.Pretty | ||
25 | |||
26 | newtype Nat = Nat_ Int --Word32 | ||
27 | deriving (Eq, Ord, Enum) | ||
28 | |||
29 | pattern Nat i <- (fromEnum -> i) | ||
30 | where Nat i = toEnum i | ||
31 | |||
32 | instance Num Nat where | ||
33 | fromInteger n = Nat $ fromInteger n | ||
34 | Nat a + Nat b = Nat (a + b) | ||
35 | Nat a - Nat b = Nat (a - b) | ||
36 | negate (Nat b) = Nat $ negate b -- error "negate @Nat" | ||
37 | _ * _ = error "(*) @Nat" | ||
38 | abs _ = error "abs @Nat" | ||
39 | signum _ = error "signum @Nat" | ||
40 | |||
41 | instance PShow Nat where | ||
42 | pShow (Nat i) = pShow i | ||
43 | |||
44 | data FV | ||
45 | -- = FV !Nat !Nat !FV | ||
46 | = FV_ !Int !FV | ||
47 | | FE | ||
48 | deriving (Eq) | ||
49 | |||
50 | pattern FV :: Nat -> Nat -> FV -> FV | ||
51 | pattern FV i j x <- FV_ (splitInt -> (i, j)) x | ||
52 | where FV (Nat i) (Nat j) x = FV_ (i `shiftL` 32 .|. j) x | ||
53 | |||
54 | splitInt x = (Nat $ x `shiftR` 32, Nat $ x .&. 0xffffffff) | ||
55 | |||
56 | instance PShow FV where | ||
57 | pShow FE = "0" | ||
58 | pShow (FV i j x) = pShow i <> "|" <> pShow j <> "|" <> pShow x | ||
59 | |||
60 | {- | ||
61 | newtype FV = FV_ Integer | ||
62 | |||
63 | pattern FV :: Nat -> Nat -> FV -> FV | ||
64 | pattern FV i j x <- FV_ (ff -> Just (x, i, j)) | ||
65 | where FV i j (FV_ x) = FV_ (x `shiftL` 32 .|. fromIntegral (i `shiftL` 16 .|. j)) | ||
66 | |||
67 | ff 0 = Nothing | ||
68 | ff x = Just (FV_ (x `shiftR` 32), (fromIntegral x `shiftR` 16) .&. 0xffff, fromIntegral x .&. 0xffff) | ||
69 | |||
70 | pattern FE :: FV | ||
71 | pattern FE = FV_ 0 | ||
72 | -} | ||
73 | |||
74 | fv :: Nat -> Nat -> FV -> FV | ||
75 | fv 0 0 xs = xs | ||
76 | fv a 0 FE = FE | ||
77 | fv a 0 (FV b c xs) = FV (a+b) c xs | ||
78 | fv a b (FV 0 c xs) = FV a (b+c) xs | ||
79 | fv a b xs = FV a b xs | ||
80 | |||
81 | pattern VarFV i <- FV i _ _ | ||
82 | where VarFV i = FV i 1 FE | ||
83 | |||
84 | del1 :: FV -> FV | ||
85 | del1 FE = FE | ||
86 | del1 (FV 0 n us) = fv 0 (n-1) us | ||
87 | del1 (FV n i us) = FV (n-1) i us | ||
88 | |||
89 | compact :: FV -> FV | ||
90 | compact xs@(FV 0 _ _) = delUnused xs | ||
91 | compact xs = fv 1 0 $ delUnused xs | ||
92 | |||
93 | usedFVs :: FV -> [Nat] | ||
94 | usedFVs = f 0 | ||
95 | where | ||
96 | f _ FE = [] | ||
97 | f s (FV i a xs) = [s+i..(s+i+a)-1] ++ f (s+i+a) xs | ||
98 | |||
99 | usedFV :: Nat -> FV -> Bool | ||
100 | usedFV i FE = False | ||
101 | usedFV i (FV n l us) = i >= n && (i < l || usedFV (i - l - n) us) | ||
102 | |||
103 | downFV :: Nat -> FV -> Maybe FV | ||
104 | downFV i FE = Just FE | ||
105 | downFV i (FV n j us) | ||
106 | | i < n = Just $ FV (n - 1) j us | ||
107 | | i - n < j = Nothing | ||
108 | | otherwise = fv n j <$> downFV (i - n - j) us | ||
109 | |||
110 | instance Monoid FV where | ||
111 | mempty = FE | ||
112 | |||
113 | mappend x FE = x | ||
114 | mappend FE x = x | ||
115 | mappend (FV a b us) (FV a' b' us') | ||
116 | | a + b <= a' = fv a b $ mappend us (FV (a' - (a + b)) b' us') | ||
117 | | a + b - a' <= b' = fv c (a + b - c) $ mappend us (FV 0 (b' - (a + b - a')) us') | ||
118 | | a' + b' <= a = fv a' b' $ mappend (FV (a - (a' + b')) b us) us' | ||
119 | | otherwise = fv c (a' + b' - c) $ mappend (FV 0 ((a + b) - (a' + b')) us) us' | ||
120 | where | ||
121 | c = min a a' | ||
122 | |||
123 | delFV :: FV -> FV -> FV | ||
124 | delFV FE x = FE | ||
125 | delFV (FV a b us) (FV a' b' us') | ||
126 | | a' + b' <= a = fv b' 0 $ delFV (FV (a - (a' + b')) b us) us' | ||
127 | | otherwise = fv (a - a') b $ delFV us (FV 0 ((a' + b') - (a + b)) us') | ||
128 | |||
129 | -- delUnused x = delFV x x | ||
130 | delUnused :: FV -> FV | ||
131 | delUnused xs = fv 0 (altersum xs) FE | ||
132 | where | ||
133 | altersum FE = 0 | ||
134 | altersum (FV _ a cs) = a + altersum cs | ||
135 | |||
136 | compFV :: FV -> FV -> FV | ||
137 | compFV _ FE = FE | ||
138 | compFV FE x = x | ||
139 | compFV (FV a b xs) (FV c d ys) | ||
140 | | c + d <= b = fv (a + c) d $ compFV (FV 0 (b - (c + d)) xs) ys | ||
141 | | c <= b = fv (a + c) (b - c) $ compFV xs (FV 0 (d - (b - c)) ys) | ||
142 | | otherwise = fv (a + b) 0 $ compFV xs (FV (c - b) d ys) | ||
143 | |||
144 | incFV :: FV -> FV | ||
145 | incFV = FV{-ok-} 0 1 | ||
146 | |||
147 | --upFV l n = compFV (fv 0 l $ fv n 0{-buggy-} FE) | ||
148 | upFV :: Nat -> Nat -> FV -> FV | ||
149 | upFV l n FE = FE | ||
150 | upFV l n (FV n' l' us) | ||
151 | | l <= n' = FV (n' + n) l' us | ||
152 | | l' <= l - n' = FV n' l' $ upFV (l - n' - l') n us | ||
153 | | otherwise = FV n' (l - n') $ FV n (l' - (l - n')) us | ||
154 | |||
155 | |||
156 | |||
diff --git a/prototypes/Inspector.hs b/prototypes/Inspector.hs index 60389b97..663594f8 100644 --- a/prototypes/Inspector.hs +++ b/prototypes/Inspector.hs | |||
@@ -33,7 +33,8 @@ data StepTree a b | |||
33 | deriving Show | 33 | deriving Show |
34 | 34 | ||
35 | stepTree :: MSt -> StepTree StepTag MSt | 35 | stepTree :: MSt -> StepTree StepTag MSt |
36 | stepTree = fst . steps (runState $ return NoStep) | 36 | stepTree = fst . steps 0 |
37 | (runState $ return NoStep) | ||
37 | (\t c -> runState $ Step t <$> get <*> state c) | 38 | (\t c -> runState $ Step t <$> get <*> state c) |
38 | (\t c2 c1 -> runState $ Steps t <$> state c1 <*> state c2) | 39 | (\t c2 c1 -> runState $ Steps t <$> state c1 <*> state c2) |
39 | 40 | ||
@@ -91,7 +92,7 @@ main = do | |||
91 | (LeftArrow, st@(_, _:_:_)) -> cycle' $ iterate goLeft st !! 100 | 92 | (LeftArrow, st@(_, _:_:_)) -> cycle' $ iterate goLeft st !! 100 |
92 | (RightArrow, st@(_:_, _)) -> cycle' $ iterate goRight st !! 100 | 93 | (RightArrow, st@(_:_, _)) -> cycle' $ iterate goRight st !! 100 |
93 | (IntArg n, _) -> cycle' ([], stepList $ t' n) | 94 | (IntArg n, _) -> cycle' ([], stepList $ t' n) |
94 | (ProgramChange, _) -> cycle' ([], stepList $ t'' 1000) | 95 | (ProgramChange, _) -> cycle' ([], stepList $ t'' 0) |
95 | _ -> cycle False st | 96 | _ -> cycle False st |
96 | 97 | ||
97 | cycle' st@(h, (_, x): _) = do | 98 | cycle' st@(h, (_, x): _) = do |
diff --git a/prototypes/LamMachine.hs b/prototypes/LamMachine.hs index f88062b0..e95960d2 100644 --- a/prototypes/LamMachine.hs +++ b/prototypes/LamMachine.hs | |||
@@ -11,43 +11,51 @@ | |||
11 | module LamMachine where | 11 | module LamMachine where |
12 | 12 | ||
13 | import Data.List | 13 | import Data.List |
14 | import Data.Word | ||
15 | import Data.Int | ||
16 | import Data.Monoid | ||
14 | import Data.Maybe | 17 | import Data.Maybe |
15 | import Control.Arrow | 18 | import Control.Arrow hiding ((<+>)) |
16 | import Control.Category hiding ((.), id) | 19 | import Control.Category hiding ((.), id) |
17 | --import Debug.Trace | 20 | import Control.Monad |
21 | import Debug.Trace | ||
18 | 22 | ||
19 | import LambdaCube.Compiler.Pretty | 23 | import LambdaCube.Compiler.Pretty |
20 | 24 | ||
25 | import FreeVars | ||
26 | |||
21 | --------------------------------------------------------------------- data structures | 27 | --------------------------------------------------------------------- data structures |
22 | 28 | ||
23 | data Exp_ | 29 | data Exp_ |
24 | = Var_ | 30 | = Var_ |
25 | | Int_ !Int -- ~ constructor with 0 args | 31 | | Int_ !Int -- ~ constructor with 0 args |
26 | | Lam_ Exp | 32 | | Lam_ !Exp |
27 | | Con_ String Int [Exp] | 33 | | Op1_ !Op1 !Exp |
28 | | Case_ [String]{-for pretty print-} Exp [Exp] -- --> simplify | 34 | | Con_ String !Int [Exp] |
29 | | Op1_ !Op1 Exp | 35 | | Case_ [String]{-for pretty print-} !Exp ![Exp] -- --> simplify |
30 | | Op2_ !Op2 Exp Exp | 36 | | Op2_ !Op2 !Exp !Exp |
31 | 37 | deriving Eq | |
32 | data Op1 = YOp | Round | 38 | |
39 | data Op1 = HNF_ !Int | YOp | Round | ||
33 | deriving (Eq, Show) | 40 | deriving (Eq, Show) |
34 | 41 | ||
35 | data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt | 42 | data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt |
36 | deriving (Eq, Show) | 43 | deriving (Eq, Show) |
37 | 44 | ||
38 | -- cached and compressed free variables set | 45 | -- cached and compressed free variables set |
39 | type FV = [Int] | 46 | data Exp = Exp_ !FV !Exp_ |
40 | 47 | deriving Eq | |
41 | data Exp = Exp !FV Exp_ | ||
42 | 48 | ||
43 | -- state of the machine | 49 | -- state of the machine |
44 | data MSt = MSt Exp Exp [Exp] | 50 | data MSt = MSt Exp Exp ![Exp] |
51 | deriving Eq | ||
45 | 52 | ||
46 | --------------------------------------------------------------------- toolbox: pretty print | 53 | --------------------------------------------------------------------- toolbox: pretty print |
47 | 54 | ||
48 | instance PShow Exp where | 55 | instance PShow Exp where |
49 | pShow e@(Exp _ x) = case e of -- shUps' u t $ case Exp [] t x of | 56 | pShow e@(Exp_ fv _) = --(("[" <> pShow fv <> "]") <+>) $ |
50 | Var i -> DVar i | 57 | case e of |
58 | Var (Nat i) -> DVar i | ||
51 | Let a b -> shLet (pShow a) $ pShow b | 59 | Let a b -> shLet (pShow a) $ pShow b |
52 | App a b -> DApp (pShow a) (pShow b) | 60 | App a b -> DApp (pShow a) (pShow b) |
53 | Seq a b -> DOp "`seq`" (Infix 1) (pShow a) (pShow b) | 61 | Seq a b -> DOp "`seq`" (Infix 1) (pShow a) (pShow b) |
@@ -55,6 +63,7 @@ instance PShow Exp where | |||
55 | Con s i xs -> foldl DApp (text s) $ pShow <$> xs | 63 | Con s i xs -> foldl DApp (text s) $ pShow <$> xs |
56 | Int i -> pShow i | 64 | Int i -> pShow i |
57 | Y e -> "Y" `DApp` pShow e | 65 | Y e -> "Y" `DApp` pShow e |
66 | Op1 (HNF_ i) x -> DGlue (InfixL 40) (onred $ white $ if i == -1 then "this" else pShow i) $ DBrace (pShow x) | ||
58 | Op1 o x -> text (show o) `DApp` pShow x | 67 | Op1 o x -> text (show o) `DApp` pShow x |
59 | Op2 EqInt x y -> DOp "==" (Infix 4) (pShow x) (pShow y) | 68 | Op2 EqInt x y -> DOp "==" (Infix 4) (pShow x) (pShow y) |
60 | Op2 Add x y -> DOp "+" (InfixL 6) (pShow x) (pShow y) | 69 | Op2 Add x y -> DOp "+" (InfixL 6) (pShow x) (pShow y) |
@@ -63,8 +72,7 @@ instance PShow Exp where | |||
63 | $ foldr1 DSemi [DArr_ "->" (text a) (pShow b) | (a, b) <- zip cn xs] | 72 | $ foldr1 DSemi [DArr_ "->" (text a) (pShow b) | (a, b) <- zip cn xs] |
64 | 73 | ||
65 | instance PShow MSt where | 74 | instance PShow MSt where |
66 | pShow (MSt as b bs) = case foldl (flip (:)) (DBrace (pShow b): [pShow x | x <- bs]) $ [pShow as] of | 75 | pShow (MSt as b bs) = pShow $ foldl (flip Let) (Let (HNF (-1) b) as) bs |
67 | x: xs -> foldl (flip shLet) x xs | ||
68 | 76 | ||
69 | shUps a b = DPreOp (-20) (SimpleAtom $ show a) b | 77 | shUps a b = DPreOp (-20) (SimpleAtom $ show a) b |
70 | shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) b | 78 | shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) b |
@@ -84,48 +92,29 @@ showLet x y = DLet' x y | |||
84 | 92 | ||
85 | --------------------------------------------------------------------- pattern synonyms | 93 | --------------------------------------------------------------------- pattern synonyms |
86 | 94 | ||
87 | pattern Int i <- Exp _ (Int_ i) | 95 | pattern Int i <- Exp_ _ (Int_ i) |
88 | where Int i = Exp [0] $ Int_ i | 96 | where Int i = Exp_ mempty $ Int_ i |
89 | pattern Op2 op a b <- Exp u (Op2_ op (upp u -> a) (upp u -> b)) | 97 | pattern Op2 op a b <- Exp_ u (Op2_ op (upp u -> a) (upp u -> b)) |
90 | where Op2 op a b = Exp s $ Op2_ op az bz where (s, az, bz) = delta2 a b | 98 | where Op2 op a b = Exp_ s $ Op2_ op az bz where (s, az, bz) = delta2 a b |
91 | pattern Op1 op a <- Exp u (Op1_ op (upp u -> a)) | 99 | pattern Op1 op a <- Exp_ u (Op1_ op (upp u -> a)) |
92 | where Op1 op a = dup1 (Op1_ op) a | 100 | where Op1 op (Exp_ ab x) = Exp_ ab $ Op1_ op $ Exp_ (delUnused ab) x |
93 | pattern Var i <- Exp (varIndex -> i) Var_ | 101 | pattern Var' i = Exp_ (VarFV i) Var_ |
94 | where Var 0 = Exp [1] Var_ | 102 | pattern Var i = Var' i |
95 | Var i = Exp [0, i, i+1] Var_ | 103 | pattern Lam i <- Exp_ u (Lam_ (upp (incFV u) -> i)) |
96 | pattern Lam i <- Exp u (Lam_ (upp ((+1) <$> u) -> i)) | 104 | where Lam (Exp_ vs ax) = Exp_ (del1 vs) $ Lam_ $ Exp_ (compact vs) ax |
97 | where Lam i = dupLam i | 105 | pattern Con a b i <- Exp_ u (Con_ a b (map (upp u) -> i)) |
98 | pattern Con a b i <- Exp u (Con_ a b (map (upp u) -> i)) | 106 | where Con a b x = Exp_ s $ Con_ a b bz where (s, bz) = deltas x |
99 | where Con a b [] = Exp [0] $ Con_ a b [] | 107 | pattern Case a b c <- Exp_ u (Case_ a (upp u -> b) (map (upp u) -> c)) |
100 | Con a b [x] = dup1 (Con_ a b . (:[])) x | 108 | where Case cn a b = Exp_ s $ Case_ cn az bz where (s, az: bz) = deltas $ a: b |
101 | Con a b [x, y] = Exp s $ Con_ a b [xz, yz] where (s, xz, yz) = delta2 x y | ||
102 | Con a b x = Exp s $ Con_ a b bz where (s, bz) = deltas x | ||
103 | pattern Case a b c <- Exp u (Case_ a (upp u -> b) (map (upp u) -> c)) | ||
104 | where Case cn a b = Exp s $ Case_ cn az bz where (s, az: bz) = deltas $ a: b | ||
105 | 109 | ||
106 | pattern Let i x = App (Lam x) i | 110 | pattern Let i x = App (Lam x) i |
107 | pattern Y a = Op1 YOp a | 111 | pattern Y a = Op1 YOp a |
112 | pattern HNF i a = Op1 (HNF_ i) a | ||
108 | pattern App a b = Op2 AppOp a b | 113 | pattern App a b = Op2 AppOp a b |
109 | pattern Seq a b = Op2 SeqOp a b | 114 | pattern Seq a b = Op2 SeqOp a b |
110 | 115 | ||
111 | infixl 4 `App` | 116 | infixl 4 `App` |
112 | 117 | ||
113 | varIndex (_: i: _) = i | ||
114 | varIndex _ = 0 | ||
115 | |||
116 | dupLam (Exp vs ax) = Exp (f vs) $ Lam_ $ Exp (g vs) ax | ||
117 | where | ||
118 | f (0: nus) = 0 .: map (+(-1)) nus | ||
119 | f us = map (+(-1)) us | ||
120 | |||
121 | g xs@(0: _) = [0, 1, altersum xs + 1] | ||
122 | g xs = [altersum xs] | ||
123 | |||
124 | dup1 f (Exp ab x) = Exp ab $ f $ Exp [altersum ab] x | ||
125 | |||
126 | altersum [x] = x | ||
127 | altersum (a: b: cs) = a - b + altersum cs | ||
128 | |||
129 | initSt :: Exp -> MSt | 118 | initSt :: Exp -> MSt |
130 | initSt e = MSt (Var 0) e [] | 119 | initSt e = MSt (Var 0) e [] |
131 | 120 | ||
@@ -136,98 +125,50 @@ size (MSt xs _ ys) = length (getLets xs) + length ys | |||
136 | getLets (Let x y) = x: getLets y | 125 | getLets (Let x y) = x: getLets y |
137 | getLets x = [x] | 126 | getLets x = [x] |
138 | 127 | ||
139 | --------------------------------------------------------------------- toolbox: de bruijn index shifting | 128 | delta2 (Exp_ ua a) (Exp_ ub b) = (s, Exp_ (delFV ua s) a, Exp_ (delFV ub s) b) |
140 | |||
141 | upp [k] ys = ys | ||
142 | upp (x: y: xs) ys = upp xs (up x (y - x) ys) | ||
143 | |||
144 | up i 0 e = e | ||
145 | up i num (Exp us x) = Exp (f i (i + num) us) x | ||
146 | where | 129 | where |
147 | f l n [s] | 130 | s = ua <> ub |
148 | | l >= s = [s] | ||
149 | | otherwise = [l, n, s+n-l] | ||
150 | f l n us_@(l': n': us) | ||
151 | | l < l' = l : n: map (+(n-l)) us_ | ||
152 | | l <= n' = l': n' + n - l: map (+(n-l)) us | ||
153 | | otherwise = l': n': f l n us | ||
154 | 131 | ||
155 | -- free variables set | 132 | deltas [] = (mempty, []) |
156 | fvs (Exp us _) = gen 0 us where | 133 | deltas [Exp_ x e] = (x, [Exp_ (delUnused x) e]) |
157 | gen i (a: xs) = [i..a-1] ++ gen' xs | 134 | deltas [Exp_ ua a, Exp_ ub b] = (s, [Exp_ (delFV ua s) a, Exp_ (delFV ub s) b]) |
158 | gen' [] = [] | ||
159 | gen' (a: xs) = gen a xs | ||
160 | |||
161 | (.:) :: Int -> [Int] -> [Int] | ||
162 | a .: (x: y: xs) | a == x = y: xs | ||
163 | a .: xs = a: xs | ||
164 | |||
165 | usedVar i (Exp us _) = f us where | ||
166 | f [fv] = i < fv | ||
167 | f (l: n: us) = i < l || i >= n && f us | ||
168 | |||
169 | down i (Exp us e) = Exp <$> f us <*> pure e where | ||
170 | f [fv] | ||
171 | | i < fv = Nothing | ||
172 | | otherwise = Just [fv] | ||
173 | f vs@(j: vs'@(n: us)) | ||
174 | | i < j = Nothing | ||
175 | | i < n = Just $ j .: map (+(-1)) vs' | ||
176 | | otherwise = (j:) . (n .:) <$> f us | ||
177 | |||
178 | delta2 (Exp (add0 -> ua) a) (Exp (add0 -> ub) b) = (add0 s, Exp (dLadders 0 ua s) a, Exp (dLadders 0 ub s) b) | ||
179 | where | 135 | where |
180 | s = iLadders ua ub | 136 | s = ua <> ub |
181 | 137 | deltas es = (s, [Exp_ (delFV u s) e | (u, Exp_ _ e) <- zip xs es]) | |
182 | deltas [] = ([0], []) | ||
183 | deltas es = (add0 s, [Exp (dLadders 0 u s) e | (u, Exp _ e) <- zip xs es]) | ||
184 | where | 138 | where |
185 | xs = [add0 ue | Exp ue _ <- es] | 139 | xs = [ue | Exp_ ue _ <- es] |
186 | 140 | ||
187 | s = foldr1 iLadders xs | 141 | s = mconcat xs |
188 | 142 | ||
189 | iLadders :: [Int] -> [Int] -> [Int] | 143 | upp :: FV -> Exp -> Exp |
190 | iLadders x [] = x | 144 | upp a (Exp_ b e) = Exp_ (compFV a b) e |
191 | iLadders [] x = x | ||
192 | iLadders x@(a: b: us) x'@(a': b': us') | ||
193 | | b <= a' = addL a b $ iLadders us x' | ||
194 | | b' <= a = addL a' b' $ iLadders x us' | ||
195 | | otherwise = addL (min a a') c $ iLadders (addL c b us) (addL c b' us') | ||
196 | where | ||
197 | c = min b b' | ||
198 | 145 | ||
199 | addL a b cs | a == b = cs | 146 | up l n (Exp_ us x) = Exp_ (upFV l n us) x |
200 | addL a b (c: cs) | b == c = a: cs | 147 | |
201 | addL a b cs = a: b: cs | 148 | -- free variables set |
149 | fvs (Exp_ us _) = usedFVs us | ||
202 | 150 | ||
203 | add0 [] = [0] | 151 | usedVar i (Exp_ us _) = usedFV i us |
204 | add0 (0: cs) = cs | ||
205 | add0 cs = 0: cs | ||
206 | 152 | ||
207 | dLadders :: Int -> [Int] -> [Int] -> [Int] | 153 | down i (Exp_ us e) = Exp_ <$> downFV i us <*> pure e |
208 | dLadders s [] x = [s] | ||
209 | dLadders s x@(a: b: us) x'@(a': b': us') | ||
210 | | b' <= a = addL s (s + b' - a') $ dLadders (s + b' - a') x us' | ||
211 | | a' < a = addL s (s + a - a') $ dLadders (s + a - a') x (addL a b' us') | ||
212 | | a' == a = dLadders (s + b - a) us (addL b b' us') | ||
213 | 154 | ||
214 | --------------------------- | 155 | --------------------------- |
215 | 156 | ||
216 | tryRemoves xs = tryRemoves_ (Var <$> xs) | 157 | tryRemoves xs = tryRemoves_ (Var' <$> xs) |
217 | 158 | ||
218 | tryRemoves_ [] dt = dt | 159 | tryRemoves_ [] dt = dt |
219 | tryRemoves_ (Var i: vs) dt = maybe (tryRemoves_ vs dt) (\(is, st) -> tryRemoves_ (is ++ catMaybes (down i <$> vs)) st) $ tryRemove_ i dt | 160 | tryRemoves_ (Var' i: vs) dt = maybe (tryRemoves_ vs dt) (\(is, st) -> tryRemoves_ (is ++ catMaybes (down i <$> vs)) st) $ tryRemove_ i dt |
220 | where | 161 | where |
221 | tryRemove_ i (MSt xs e es) = (\a b (is, c) -> (is, MSt a b c)) <$> down (i+1) xs <*> down i e <*> downDown i es | 162 | tryRemove_ i (MSt xs e es) = (\a b (is, c) -> (is, MSt a b c)) <$> down (i+1) xs <*> down i e <*> downDown i es |
222 | 163 | ||
223 | downDown i [] = Just ([], []) | 164 | downDown i [] = Just ([], []) |
224 | downDown 0 (x: xs) = Just (Var <$> fvs x, xs) | 165 | downDown 0 (x: xs) = Just (Var' <$> fvs x, xs) |
225 | downDown i (x: xs) = (\x (is, xs) -> (up 0 1 <$> is, x: xs)) <$> down (i-1) x <*> downDown (i-1) xs | 166 | downDown i (x: xs) = (\x (is, xs) -> (up 0 1 <$> is, x: xs)) <$> down (i-1) x <*> downDown (i-1) xs |
226 | 167 | ||
227 | ----------------------------------------------------------- machine code begins here | 168 | ----------------------------------------------------------- machine code begins here |
228 | 169 | ||
229 | justResult :: MSt -> MSt | 170 | justResult :: MSt -> MSt |
230 | justResult = steps id (const ($)) (const (.)) | 171 | justResult = steps 0 id (const ($)) (const (.)) |
231 | 172 | ||
232 | hnf = justResult . initSt | 173 | hnf = justResult . initSt |
233 | 174 | ||
@@ -242,23 +183,23 @@ type GenSteps e | |||
242 | 183 | ||
243 | type StepTag = String | 184 | type StepTag = String |
244 | 185 | ||
245 | steps :: forall e . GenSteps e | 186 | steps :: forall e . Int -> GenSteps e |
246 | steps nostep {-ready-} bind cont dt@(MSt t e vs) = case e of | 187 | steps lev nostep {-ready-} bind cont dt@(MSt t e vs) = case e of |
247 | 188 | ||
248 | Int{} -> nostep dt --ready "hnf int" | 189 | Int{} -> nostep dt --ready "hnf int" |
249 | Lam{} -> nostep dt --ready "hnf lam" | 190 | Lam{} -> nostep dt --ready "hnf lam" |
250 | 191 | ||
251 | Con cn i xs | 192 | Con cn i xs |
252 | | lz /= 0 -> step "copy con" $ MSt (up 1 lz t) (Con cn i xs') $ zs ++ vs -- share complex constructor arguments | 193 | | lz > 0 -> step "copy con" $ MSt (up 1 lz t) (Con cn i xs') $ zs ++ vs -- share complex constructor arguments |
253 | | otherwise -> nostep dt --ready "hnf con" | 194 | | otherwise -> nostep dt --ready "hnf con" |
254 | where | 195 | where |
255 | lz = length zs | 196 | lz = Nat $ length zs |
256 | (xs', concat -> zs) = unzip $ f 0 xs | 197 | (xs', concat -> zs) = unzip $ f 0 xs |
257 | f i [] = [] | 198 | f i [] = [] |
258 | f i (x: xs) | simple x = (up 0 lz x, []): f i xs | 199 | f i (x: xs) | simple x = (up 0 lz x, []): f i xs |
259 | | otherwise = (Var i, [up 0 (lz - i - 1) x]): f (i+1) xs | 200 | | otherwise = (Var' i, [up 0 (lz - i - 1) x]): f (i+1) xs |
260 | 201 | ||
261 | Var i -> lookupHNF_ rec "var" const i dt | 202 | Var i -> lookupHNF_ nostep "var" const i dt |
262 | 203 | ||
263 | Seq a b -> case a of | 204 | Seq a b -> case a of |
264 | Int{} -> step "seq" $ MSt t b vs | 205 | Int{} -> step "seq" $ MSt t b vs |
@@ -297,27 +238,29 @@ steps nostep {-ready-} bind cont dt@(MSt t e vs) = case e of | |||
297 | (_, Int{}) -> step "op2" $ MSt (up 1 1 t) (Op2 op (Var 0) y) $ x: vs | 238 | (_, Int{}) -> step "op2" $ MSt (up 1 1 t) (Op2 op (Var 0) y) $ x: vs |
298 | _ -> step "op2" $ MSt (up 1 2 t) (Op2 op (Var 0) (Var 1)) $ x: y: vs | 239 | _ -> step "op2" $ MSt (up 1 2 t) (Op2 op (Var 0) (Var 1)) $ x: y: vs |
299 | where | 240 | where |
300 | rec = steps nostep bind cont | 241 | rec i = steps i nostep bind cont |
301 | 242 | ||
302 | step :: StepTag -> MSt -> e | 243 | step :: StepTag -> MSt -> e |
303 | step t = bind t rec | 244 | step t = bind t (rec lev) |
304 | 245 | ||
305 | hnf :: (MSt -> e) -> MSt -> e | 246 | hnf :: (MSt -> e) -> MSt -> e |
306 | hnf f = cont "hnf" f rec | 247 | hnf f = cont "hnf" f (rec $ 1 + lev) |
248 | |||
249 | hnfTag (MSt a b c) = MSt a (HNF lev b) c | ||
307 | 250 | ||
308 | -- lookup var in head normal form | 251 | -- lookup var in head normal form |
309 | lookupHNF_ :: (MSt -> e) -> StepTag -> (Exp -> Exp -> Exp) -> Int -> MSt -> e | 252 | lookupHNF_ :: (MSt -> e) -> StepTag -> (Exp -> Exp -> Exp) -> Nat -> MSt -> e |
310 | lookupHNF_ end msg f i dt = bind msg (hnf shiftLookup) $ iterate shiftL dt !! (i+1) | 253 | lookupHNF_ end msg f i@(Nat i') dt = bind msg (hnf shiftLookup) $ iterate shiftL (hnfTag dt) !! (i'+1) |
311 | where | 254 | where |
312 | shiftLookup dt@(MSt _ e _) | 255 | shiftLookup dt@(MSt _ e _) |
313 | = case iterate shiftR dt !! (i+1) of | 256 | = case iterate shiftR dt !! (i'+1) of |
314 | MSt xs z es -> bind "shiftR" (tryRemove i) $ MSt xs (f (up 0 (i+1) e) z) es | 257 | MSt xs (HNF lev z) es -> bind "shiftR" (tryRemove i) $ MSt xs (f (up 0 (i+1) e) z) es |
315 | 258 | ||
316 | tryRemove i st = {-maybe (end st)-} (bind "remove" end) $ tryRemoves [i] st | 259 | tryRemove i st = {-maybe (end st)-} (bind "remove" end) $ tryRemoves [i] st |
317 | 260 | ||
318 | -- lookup & step | 261 | -- lookup & step |
319 | lookupHNF' :: StepTag -> (Exp -> Exp -> Exp) -> Int -> MSt -> e | 262 | lookupHNF' :: StepTag -> (Exp -> Exp -> Exp) -> Nat -> MSt -> e |
320 | lookupHNF' msg f i dt = lookupHNF_ rec msg f i dt | 263 | lookupHNF' msg f i dt = lookupHNF_ (rec lev) msg f i dt |
321 | 264 | ||
322 | shiftL (MSt xs x (e: es)) = MSt (Let x xs) e es | 265 | shiftL (MSt xs x (e: es)) = MSt (Let x xs) e es |
323 | 266 | ||
@@ -348,9 +291,9 @@ if_ b t f = caseBool b f t | |||
348 | 291 | ||
349 | not_ x = caseBool x T F | 292 | not_ x = caseBool x T F |
350 | 293 | ||
351 | test = runMachinePure (id_ `App` id_ `App` id_ `App` id_ `App` Con "()" 0 []) | 294 | test = hnf (id_ `App` id_ `App` id_ `App` id_ `App` Int 13) |
352 | 295 | ||
353 | test' = runMachinePure (id_ `App` (id_ `App` Con "()" 0 [])) | 296 | test' = hnf (id_ `App` (id_ `App` Int 14)) |
354 | 297 | ||
355 | foldr_ f e = Y $ Lam $ Lam $ caseList (Var 0) (up 0 2 e) (Lam $ Lam $ up 0 4 f `App` Var 1 `App` (Var 3 `App` Var 0)) | 298 | foldr_ f e = Y $ Lam $ Lam $ caseList (Var 0) (up 0 2 e) (Lam $ Lam $ up 0 4 f `App` Var 1 `App` (Var 3 `App` Var 0)) |
356 | 299 | ||
@@ -401,60 +344,12 @@ primes = 2:3: filter (\n -> and $ map (\p -> n `mod` p /= 0) (takeWhile (\x -> x | |||
401 | main = primes !! 3000 | 344 | main = primes !! 3000 |
402 | -} | 345 | -} |
403 | 346 | ||
347 | tests | ||
348 | = test == hnf (Int 13) | ||
349 | && test' == hnf (Int 14) | ||
350 | && hnf (Lam (Int 4) `App` Int 3) == hnf (Int 4) | ||
351 | && hnf (t' 10) == hnf (Int 55) | ||
352 | && hnf (t'' 10) == hnf (Int 55) | ||
404 | 353 | ||
405 | 354 | ||
406 | ------------------------------------------------------------- | ||
407 | |||
408 | {- alternative presentation | ||
409 | |||
410 | sect [] xs = xs | ||
411 | sect xs [] = xs | ||
412 | sect (x:xs) (y:ys) = (x || y): sect xs ys | ||
413 | |||
414 | diffUps a b = diffUps' 0 (back a) (back b) | ||
415 | |||
416 | diffUps' n u [] = (+(-n)) <$> u | ||
417 | diffUps' n [] _ = [] | ||
418 | diffUps' n (x: xs) (y: ys) | ||
419 | | x < y = (x - n): diffUps' n xs (y: ys) | ||
420 | | x == y = diffUps' (n+1) xs ys | ||
421 | |||
422 | back = map fst . filter (not . snd) . zip [0..] | ||
423 | |||
424 | mkUps = f 0 | ||
425 | where | ||
426 | f i [] = [] | ||
427 | f i (x: xs) = insertUp (Up (x-i) 1) $ f (i+1) xs | ||
428 | |||
429 | showUps us n = foldr f (replicate n True) us where | ||
430 | f (Up l n) is = take l is ++ replicate n False ++ drop l is | ||
431 | |||
432 | deltaUps_ (map $ uncurry showUps -> us) = (mkUps $ back s, [mkUps $ u `diffUps` s | u <- us]) | ||
433 | where | ||
434 | s = foldr1 sect $ us | ||
435 | |||
436 | joinUps a b = foldr insertUp b a | ||
437 | |||
438 | diffUpsTest xs | ||
439 | | and $ zipWith (\a (b, _) -> s `joinUps` a == b) ys xs = show (s, ys) | ||
440 | | otherwise = error $ unlines $ map (show . toLadder) xs ++ "----": map show xs ++ "-----": show s: show s_: "-----": map show ys ++ "------": map (show . joinUps s) ys | ||
441 | where | ||
442 | (s, ys) = deltaUps_ xs | ||
443 | s_ = foldr1 iLadders $ toLadder <$> xs | ||
444 | |||
445 | diffUpsTest' = diffUpsTest [x,y] --diffUpsTest x y | ||
446 | |||
447 | --x = ([Up 8 2], 200) | ||
448 | --y = ([], 28) | ||
449 | x = ([Up 1 2, Up 3 4, Up 8 2], 200) | ||
450 | y = ([Up 2 2, Up 5 1, Up 6 2, Up 7 2], 28) | ||
451 | |||
452 | -- TODO: remove | ||
453 | insertUp (Up l 0) us = us | ||
454 | insertUp u [] = [u] | ||
455 | insertUp u@(Up l n) us_@(u'@(Up l' n'): us) | ||
456 | | l < l' = u: us_ | ||
457 | | l >= l' && l <= l' + n' = Up l' (n' + n): us | ||
458 | | otherwise = u': insertUp (Up (l-n') n) us | ||
459 | -} | ||
460 | 355 | ||
diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index 6446aeb2..b6a1c1c4 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs | |||
@@ -192,7 +192,7 @@ delta = ELit (LString "<<delta function>>") -- TODO: build an error call | |||
192 | 192 | ||
193 | pattern TConstraint <- TTyCon0 F'Constraint where TConstraint = tTyCon0 F'Constraint $ error "cs 1" | 193 | pattern TConstraint <- TTyCon0 F'Constraint where TConstraint = tTyCon0 F'Constraint $ error "cs 1" |
194 | pattern Unit <- TTyCon0 F'Unit where Unit = tTyCon0 F'Unit [Unit] | 194 | pattern Unit <- TTyCon0 F'Unit where Unit = tTyCon0 F'Unit [Unit] |
195 | pattern TInt <- TTyCon0 F'Int --where TInt = tTyCon0 F'Int $ error "cs 1" | 195 | pattern TInt <- TTyCon0 F'Int where TInt = tTyCon0 F'Int $ error "cs 1" |
196 | pattern TNat <- TTyCon0 F'Nat where TNat = tTyCon0 F'Nat $ error "cs 3" | 196 | pattern TNat <- TTyCon0 F'Nat where TNat = tTyCon0 F'Nat $ error "cs 3" |
197 | pattern TBool <- TTyCon0 F'Bool where TBool = tTyCon0 F'Bool $ error "cs 4" | 197 | pattern TBool <- TTyCon0 F'Bool where TBool = tTyCon0 F'Bool $ error "cs 4" |
198 | pattern TFloat <- TTyCon0 F'Float where TFloat = tTyCon0 F'Float $ error "cs 5" | 198 | pattern TFloat <- TTyCon0 F'Float where TFloat = tTyCon0 F'Float $ error "cs 5" |
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs index a357a9eb..12964b6b 100644 --- a/src/LambdaCube/Compiler/Pretty.hs +++ b/src/LambdaCube/Compiler/Pretty.hs | |||
@@ -280,6 +280,7 @@ isOpName _ = False | |||
280 | red = DFormat P.dullred | 280 | red = DFormat P.dullred |
281 | green = DFormat P.dullgreen | 281 | green = DFormat P.dullgreen |
282 | blue = DFormat P.dullblue | 282 | blue = DFormat P.dullblue |
283 | white = DFormat P.white | ||
283 | onred = DFormat P.ondullred | 284 | onred = DFormat P.ondullred |
284 | ongreen = DFormat P.ondullgreen | 285 | ongreen = DFormat P.ondullgreen |
285 | onblue = DFormat P.ondullblue | 286 | onblue = DFormat P.ondullblue |