git.iko.soy/Idris-dev
on master help sign in
New datatype for defunctionalised programs

...so that we can't make something ill formed by accident

commit783d45fa25c2c61ace800c80bc3a7e1dd418a5be authorEdwin Brady <edwin@dyn-207-205.cs.st-andrews.ac.uk> dateFri 5 Oct 2012, 12:23 (14 years ago) parentbfa8cc2
2 files changed+123−75
compare with master
unifiedsplit
src/IRTS/Defunctionalise.hs+92−44 src/IRTS/Simplified.hs+31−31
src/IRTS/Defunctionalise.hs+92−44
@@ -7,7 +7,30 @@ import Debug.Trace
77import Data.Maybe
88import Data.List
99
10−defunctionalise :: Int -> LDefs -> LDefs
10+data DExp = DV LVar
11+ | DApp Bool Name [DExp] -- True = tail call
12+ | DLet Name DExp DExp -- name just for pretty printing
13+ | DLam [Name] DExp -- lambda, lifted out before compiling
14+ | DC Int Name [DExp]
15+ | DCase DExp [DAlt]
16+ | DConst Const
17+ | DForeign FLang FType String [(FType, DExp)]
18+ | DOp PrimFn [DExp]
19+ | DError String
20+ deriving Eq
21+
22+data DAlt = DConCase Int Name [Name] DExp
23+ | DConstCase Const DExp
24+ | DDefaultCase DExp
25+ deriving (Show, Eq)
26+
27+data DDecl = DFun Name [Name] DExp -- name, arg names, definition
28+ | DConstructor Name Int Int -- constructor name, tag, arity
29+ deriving (Show, Eq)
30+
31+type DDefs = Ctxt DDecl
32+
33+defunctionalise :: Int -> LDefs -> DDefs
1134defunctionalise nexttag defs
1235 = let all = toAlist defs
1336 -- sort newcons so that EVAL and APPLY cons get sequential tags
@@ -36,57 +59,58 @@ getFn xs = mapMaybe fnData xs
3659-- 7 Wrap unknown applications (i.e. applications of local variables) in chains of APPLY
3760-- 8 Add explicit EVAL to case, primitives, and foreign calls
3861
39−addApps :: LDefs -> (Name, LDecl) -> (Name, LDecl)
40−addApps defs o@(n, LConstructor _ _ _) = o
41−addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))
62+addApps :: LDefs -> (Name, LDecl) -> (Name, DDecl)
63+addApps defs o@(n, LConstructor _ t a) = (n, DConstructor n t a)
64+addApps defs (n, LFun _ args e) = (n, DFun n args (aa args e))
4265 where
43− aa env (LV (Glob n)) | n `elem` env = LV (Glob n)
66+ aa :: [Name] -> LExp -> DExp
67+ aa env (LV (Glob n)) | n `elem` env = DV (Glob n)
4468 | otherwise = aa env (LApp False (LV (Glob n)) [])
4569-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e
4670 aa env (LApp tc (LV (Glob n)) args)
4771 = let args' = map (aa env) args in
4872 case lookupCtxt Nothing n defs of
49− [LConstructor _ i ar] -> LApp tc (LV (Glob n)) args'
73+ [LConstructor _ i ar] -> DApp tc n args'
5074 [LFun _ as _] -> let arity = length as in
5175 fixApply tc n args' arity
52− [] -> chainAPPLY (LV (Glob n)) args'
76+ [] -> chainAPPLY (DV (Glob n)) args'
5377 aa env (LLazyApp n args)
5478 = let args' = map (aa env) args in
5579 case lookupCtxt Nothing n defs of
56− [LConstructor _ i ar] -> LApp False (LV (Glob n)) args'
80+ [LConstructor _ i ar] -> DApp False n args'
5781 [LFun _ as _] -> let arity = length as in
5882 fixLazyApply n args' arity
59− [] -> chainAPPLY (LV (Glob n)) args'
83+ [] -> chainAPPLY (DV (Glob n)) args'
6084 aa env (LForce e) = eEVAL (aa env e)
61− aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc)
62− aa env (LCon i n args) = LCon i n (map (aa env) args)
63− aa env (LCase e alts) = LCase (eEVAL (aa env e)) (map (aaAlt env) alts)
64− aa env (LConst c) = LConst c
65− aa env (LForeign l t n args) = LForeign l t n (map (aaF env) args)
66− aa env (LOp LFork args) = LOp LFork (map (aa env) args)
67− aa env (LOp f args) = LOp f (map (eEVAL . (aa env)) args)
68− aa env (LError e) = LError e
85+ aa env (LLet n v sc) = DLet n (aa env v) (aa (n : env) sc)
86+ aa env (LCon i n args) = DC i n (map (aa env) args)
87+ aa env (LCase e alts) = DCase (eEVAL (aa env e)) (map (aaAlt env) alts)
88+ aa env (LConst c) = DConst c
89+ aa env (LForeign l t n args) = DForeign l t n (map (aaF env) args)
90+ aa env (LOp LFork args) = DOp LFork (map (aa env) args)
91+ aa env (LOp f args) = DOp f (map (eEVAL . (aa env)) args)
92+ aa env (LError e) = DError e
6993
7094 aaF env (t, e) = (t, eEVAL (aa env e))
7195
72− aaAlt env (LConCase i n args e) = LConCase i n args (aa (args ++ env) e)
73− aaAlt env (LConstCase c e) = LConstCase c (aa env e)
74− aaAlt env (LDefaultCase e) = LDefaultCase (aa env e)
96+ aaAlt env (LConCase i n args e) = DConCase i n args (aa (args ++ env) e)
97+ aaAlt env (LConstCase c e) = DConstCase c (aa env e)
98+ aaAlt env (LDefaultCase e) = DDefaultCase (aa env e)
7599
76100 fixApply tc n args ar
77− | length args == ar = LApp tc (LV (Glob n)) args
78− | length args < ar = LApp tc (LV (Glob (mkUnderCon n (ar - length args)))) args
79− | length args > ar = chainAPPLY (LApp tc (LV (Glob n)) (take ar args)) (drop ar args)
101+ | length args == ar = DApp tc n args
102+ | length args < ar = DApp tc (mkUnderCon n (ar - length args)) args
103+ | length args > ar = chainAPPLY (DApp tc n (take ar args)) (drop ar args)
80104
81105 fixLazyApply n args ar
82− | length args == ar = LApp False (LV (Glob (mkFnCon n))) args
83− | length args < ar = LApp False (LV (Glob (mkUnderCon n (ar - length args)))) args
84− | length args > ar = chainAPPLY (LApp False (LV (Glob n)) (take ar args)) (drop ar args)
106+ | length args == ar = DApp False (mkFnCon n) args
107+ | length args < ar = DApp False (mkUnderCon n (ar - length args)) args
108+ | length args > ar = chainAPPLY (DApp False n (take ar args)) (drop ar args)
85109
86110 chainAPPLY f [] = f
87− chainAPPLY f (a : as) = chainAPPLY (LApp False (LV (Glob (MN 0 "APPLY"))) [f, a]) as
111+ chainAPPLY f (a : as) = chainAPPLY (DApp False (MN 0 "APPLY") [f, a]) as
88112
89−eEVAL x = LApp False (LV (Glob (MN 0 "EVAL"))) [x]
113+eEVAL x = DApp False (MN 0 "EVAL") [x]
90114
91115data EvalApply a = EvalCase a
92116 | ApplyCase a
@@ -95,44 +119,44 @@ data EvalApply a = EvalCase a
95119-- For a function name, generate a list of
96120-- data constuctors, and whether to handle them in EVAL or APPLY
97121
98−toCons :: (Name, Int) -> [(Name, Int, EvalApply LAlt)]
122+toCons :: (Name, Int) -> [(Name, Int, EvalApply DAlt)]
99123toCons (n, i)
100124 = (mkFnCon n, i,
101− EvalCase (LConCase (-1) (mkFnCon n) (take i (genArgs 0))
102− (eEVAL (LApp False (LV (Glob n)) (map (LV . Glob) (take i (genArgs 0)))))))
125+ EvalCase (DConCase (-1) (mkFnCon n) (take i (genArgs 0))
126+ (eEVAL (DApp False n (map (DV . Glob) (take i (genArgs 0)))))))
103127 : mkApplyCase n 0 i
104128
105129mkApplyCase fname n ar | n == ar = []
106130mkApplyCase fname n ar
107131 = let nm = mkUnderCon fname (ar - n) in
108− (nm, n, ApplyCase (LConCase (-1) nm (take n (genArgs 0))
109− (LApp False (LV (Glob (mkUnderCon fname (ar - (n + 1)))))
110− (map (LV . Glob) (take n (genArgs 0) ++
132+ (nm, n, ApplyCase (DConCase (-1) nm (take n (genArgs 0))
133+ (DApp False (mkUnderCon fname (ar - (n + 1)))
134+ (map (DV . Glob) (take n (genArgs 0) ++
111135 [MN 0 "arg"])))))
112136 : mkApplyCase fname (n + 1) ar
113137
114−mkEval :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
115−mkEval xs = (MN 0 "EVAL", LFun (MN 0 "EVAL") [MN 0 "arg"]
116− (LCase (LV (Glob (MN 0 "arg")))
138+mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
139+mkEval xs = (MN 0 "EVAL", DFun (MN 0 "EVAL") [MN 0 "arg"]
140+ (DCase (DV (Glob (MN 0 "arg")))
117141 (mapMaybe evalCase xs ++
118− [LDefaultCase (LV (Glob (MN 0 "arg")))])))
142+ [DDefaultCase (DV (Glob (MN 0 "arg")))])))
119143 where
120144 evalCase (n, t, EvalCase x) = Just x
121145 evalCase _ = Nothing
122146
123−mkApply :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
124−mkApply xs = (MN 0 "APPLY", LFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]
125− (LCase (LApp False (LV (Glob (MN 0 "EVAL")))
126− [LV (Glob (MN 0 "fn"))])
147+mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
148+mkApply xs = (MN 0 "APPLY", DFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]
149+ (DCase (DApp False (MN 0 "EVAL")
150+ [DV (Glob (MN 0 "fn"))])
127151 (mapMaybe applyCase xs)))
128152 where
129153 applyCase (n, t, ApplyCase x) = Just x
130154 applyCase _ = Nothing
131155
132−declare :: Int -> [(Name, Int, EvalApply LAlt)] -> [(Name, LDecl)]
156+declare :: Int -> [(Name, Int, EvalApply DAlt)] -> [(Name, DDecl)]
133157declare t xs = dec' t xs [] where
134158 dec' t [] acc = reverse acc
135− dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, LConstructor n t ar) : acc)
159+ dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, DConstructor n t ar) : acc)
136160
137161
138162genArgs i = MN i "P_c" : genArgs (i + 1)
@@ -141,3 +165,27 @@ mkFnCon n = MN 0 ("P_" ++ show n)
141165mkUnderCon n 0 = n
142166mkUnderCon n missing = MN missing ("U_" ++ show n)
143167
168+instance Show DExp where
169+ show e = show' [] e where
170+ show' env (DV (Loc i)) = env!!i
171+ show' env (DV (Glob n)) = show n
172+ show' env (DApp _ e args) = show e ++ "(" ++
173+ showSep ", " (map (show' env) args) ++")"
174+ show' env (DLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++
175+ show' (env ++ [show n]) e
176+ show' env (DLam args e) = "\\ " ++ showSep "," (map show args) ++ " => " ++
177+ show' (env ++ (map show args)) e
178+ show' env (DC i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")"
179+ show' env (DCase e alts) = "case " ++ show' env e ++ " of {\n\t" ++
180+ showSep "\n\t| " (map (showAlt env) alts)
181+ show' env (DConst c) = show c
182+ show' env (DForeign lang ty n args)
183+ = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"
184+ show' env (DOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"
185+ show' env (DError str) = "error " ++ show str
186+
187+ showAlt env (DConCase _ n args e)
188+ = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "
189+ ++ show' env e
190+ showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e
191+ showAlt env (DDefaultCase e) = "_ => " ++ show' env e
src/IRTS/Simplified.hs+31−31
@@ -1,6 +1,7 @@
11module IRTS.Simplified where
22
33import IRTS.Lang
4+import IRTS.Defunctionalise
45import Core.TT
56import Data.Maybe
67import Control.Monad.State
@@ -27,51 +28,50 @@ data SAlt = SConCase Int Int Name [Name] SExp
2728data SDecl = SFun Name [Name] Int SExp
2829 deriving Show
2930
30−hvar :: State (LDefs, Int) Int
31+hvar :: State (DDefs, Int) Int
3132hvar = do (l, h) <- get
3233 put (l, h + 1)
3334 return h
3435
35−ldefs :: State (LDefs, Int) LDefs
36+ldefs :: State (DDefs, Int) DDefs
3637ldefs = do (l, h) <- get
3738 return l
3839
39−simplify :: Bool -> LExp -> State (LDefs, Int) SExp
40−simplify tl (LV (Loc i)) = return (SV (Loc i))
41−simplify tl (LV (Glob x))
40+simplify :: Bool -> DExp -> State (DDefs, Int) SExp
41+simplify tl (DV (Loc i)) = return (SV (Loc i))
42+simplify tl (DV (Glob x))
4243 = do ctxt <- ldefs
4344 case lookupCtxt Nothing x ctxt of
44− [LConstructor _ t 0] -> return $ SCon t x []
45+ [DConstructor _ t 0] -> return $ SCon t x []
4546 _ -> return $ SV (Glob x)
46−simplify tl (LApp tc (LV (Glob n)) args)
47− = do args' <- mapM sVar args
47+simplify tl (DApp tc n args) = do args' <- mapM sVar args
4848 mkapp (SApp (tl || tc) n) args'
49−simplify tl (LForeign lang ty fn args)
49+simplify tl (DForeign lang ty fn args)
5050 = do args' <- mapM sVar (map snd args)
5151 let fargs = zip (map fst args) args'
5252 mkfapp (SForeign lang ty fn) fargs
53−simplify tl (LLet n v e) = do v' <- simplify False v
53+simplify tl (DLet n v e) = do v' <- simplify False v
5454 e' <- simplify tl e
5555 return (SLet (Glob n) v' e')
56−simplify tl (LCon i n args) = do args' <- mapM sVar args
57− mkapp (SCon i n) args'
58−simplify tl (LCase e alts) = do v <- sVar e
56+simplify tl (DC i n args) = do args' <- mapM sVar args
57+ mkapp (SCon i n) args'
58+simplify tl (DCase e alts) = do v <- sVar e
5959 alts' <- mapM (sAlt tl) alts
6060 case v of
6161 (x, Nothing) -> return (SCase x alts')
6262 (Glob x, Just e) ->
6363 return (SLet (Glob x) e (SCase (Glob x) alts'))
64−simplify tl (LConst c) = return (SConst c)
65−simplify tl (LOp p args) = do args' <- mapM sVar args
64+simplify tl (DConst c) = return (SConst c)
65+simplify tl (DOp p args) = do args' <- mapM sVar args
6666 mkapp (SOp p) args'
67−simplify tl (LError str) = return $ SError str
67+simplify tl (DError str) = return $ SError str
6868
69−sVar (LV (Glob x))
69+sVar (DV (Glob x))
7070 = do ctxt <- ldefs
7171 case lookupCtxt Nothing x ctxt of
72− [LConstructor _ t 0] -> sVar (LCon t x [])
72+ [DConstructor _ t 0] -> sVar (DC t x [])
7373 _ -> return (Glob x, Nothing)
74−sVar (LV x) = return (x, Nothing)
74+sVar (DV x) = return (x, Nothing)
7575sVar e = do e' <- simplify False e
7676 i <- hvar
7777 return (Glob (MN i "R"), Just e')
@@ -90,19 +90,19 @@ mkfapp f args = mkapp' f args [] where
9090 = do sc <- mkapp' f xs ((ty, x) : args)
9191 return (SLet x e sc)
9292
93−sAlt tl (LConCase i n args e) = do e' <- simplify tl e
93+sAlt tl (DConCase i n args e) = do e' <- simplify tl e
9494 return (SConCase (-1) i n args e')
95−sAlt tl (LConstCase c e) = do e' <- simplify tl e
95+sAlt tl (DConstCase c e) = do e' <- simplify tl e
9696 return (SConstCase c e')
97−sAlt tl (LDefaultCase e) = do e' <- simplify tl e
97+sAlt tl (DDefaultCase e) = do e' <- simplify tl e
9898 return (SDefaultCase e')
9999
100−checkDefs :: LDefs -> [(Name, LDecl)] -> TC [(Name, SDecl)]
100+checkDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]
101101checkDefs ctxt [] = return []
102−checkDefs ctxt (con@(n, LConstructor _ _ _) : xs)
102+checkDefs ctxt (con@(n, DConstructor _ _ _) : xs)
103103 = do xs' <- checkDefs ctxt xs
104104 return xs'
105−checkDefs ctxt ((n, LFun n' args exp) : xs)
105+checkDefs ctxt ((n, DFun n' args exp) : xs)
106106 = do let sexp = evalState (simplify True exp) (ctxt, 0)
107107 (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)
108108 xs' <- checkDefs ctxt xs
@@ -111,13 +111,13 @@ checkDefs ctxt ((n, LFun n' args exp) : xs)
111111lvar v = do i <- get
112112 put (max i v)
113113
114−scopecheck :: LDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp
114+scopecheck :: DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp
115115scopecheck ctxt env tm = sc env tm where
116116 sc env (SV (Glob n)) =
117117 case lookup n (reverse env) of -- most recent first
118118 Just i -> do lvar i; return (SV (Loc i))
119119 Nothing -> case lookupCtxt Nothing n ctxt of
120− [LConstructor _ i ar] ->
120+ [DConstructor _ i ar] ->
121121 if True -- ar == 0
122122 then return (SCon i n [])
123123 else fail $ "Codegen error: Constructor " ++ show n ++
@@ -127,7 +127,7 @@ scopecheck ctxt env tm = sc env tm where
127127 sc env (SApp tc f args)
128128 = do args' <- mapM (scVar env) args
129129 case lookupCtxt Nothing f ctxt of
130− [LConstructor n tag ar] ->
130+ [DConstructor n tag ar] ->
131131 if True -- (ar == length args)
132132 then return $ SCon tag n args'
133133 else fail $ "Codegen error: Constructor " ++ show f ++
@@ -141,7 +141,7 @@ scopecheck ctxt env tm = sc env tm where
141141 sc env (SCon tag f args)
142142 = do args' <- mapM (scVar env) args
143143 case lookupCtxt Nothing f ctxt of
144− [LConstructor n tag ar] ->
144+ [DConstructor n tag ar] ->
145145 if True -- (ar == length args)
146146 then return $ SCon tag n args'
147147 else fail $ "Codegen error: Constructor " ++ show f ++
@@ -166,7 +166,7 @@ scopecheck ctxt env tm = sc env tm where
166166 case lookup n (reverse env) of -- most recent first
167167 Just i -> do lvar i; return (Loc i)
168168 Nothing -> case lookupCtxt Nothing n ctxt of
169− [LConstructor _ i ar] ->
169+ [DConstructor _ i ar] ->
170170 fail $ "Codegen error : can't pass constructor here"
171171 [_] -> return (Glob n)
172172 [] -> fail $ "Codegen error: No such variable " ++ show n
@@ -175,7 +175,7 @@ scopecheck ctxt env tm = sc env tm where
175175 scalt env (SConCase _ i n args e)
176176 = do let env' = env ++ zip args [length env..]
177177 tag <- case lookupCtxt Nothing n ctxt of
178− [LConstructor _ i ar] ->
178+ [DConstructor _ i ar] ->
179179 if True -- (length args == ar)
180180 then return i
181181 else fail $ "Codegen error: Constructor " ++ show n ++