git.iko.soy/Idris-dev
on 611dd97 help sign in
Idris-dev/src/IRTS/Defunctionalise.hs
143 lines 6.1 kB history raw
1module IRTS.Defunctionalise where
3import IRTS.Lang
4import Core.TT
6import Debug.Trace
7import Data.Maybe
8import Data.List
10defunctionalise :: Int -> LDefs -> LDefs
11defunctionalise nexttag defs
12 = let all = toAlist defs
13 -- sort newcons so that EVAL and APPLY cons get sequential tags
14 newcons = sortBy conord $ concatMap toCons (getFn all)
15 eval = mkEval newcons
16 app = mkApply newcons
17 condecls = declare nexttag newcons in
18 addAlist (eval : app : condecls ++ (map (addApps defs) all)) emptyContext
19 where conord (n, _, _) (n', _, _) = compare n n'
21getFn :: [(Name, LDecl)] -> [(Name, Int)]
22getFn xs = mapMaybe fnData xs
23 where fnData (n, LFun _ args _) = Just (n, length args)
24 fnData _ = Nothing
26-- To defunctionalise:
27--
28-- 1 Create a data constructor for each function
29-- 2 Create a data constructor for each underapplication of a function
30-- 3 Convert underapplications to their corresponding constructors
31-- 4 Create an EVAL function which calls the appropriate function for data constructors
32-- created as part of step 1
33-- 5 Create an APPLY function which adds an argument to each underapplication (or calls
34-- APPLY again for an exact application)
35-- 6 Wrap overapplications in chains of APPLY
36-- 7 Wrap unknown applications (i.e. applications of local variables) in chains of APPLY
37-- 8 Add explicit EVAL to case, primitives, and foreign calls
39addApps :: LDefs -> (Name, LDecl) -> (Name, LDecl)
40addApps defs o@(n, LConstructor _ _ _) = o
41addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))
42 where
43 aa env (LV (Glob n)) | n `elem` env = LV (Glob n)
44 | otherwise = aa env (LApp False (LV (Glob n)) [])
45-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e
46 aa env (LApp tc (LV (Glob n)) args)
47 = let args' = map (aa env) args in
48 case lookupCtxt Nothing n defs of
49 [LConstructor _ i ar] -> LApp tc (LV (Glob n)) args'
50 [LFun _ as _] -> let arity = length as in
51 fixApply tc n args' arity
52 [] -> chainAPPLY (LV (Glob n)) args'
53 aa env (LLazyApp n args)
54 = let args' = map (aa env) args in
55 case lookupCtxt Nothing n defs of
56 [LConstructor _ i ar] -> LApp False (LV (Glob n)) args'
57 [LFun _ as _] -> let arity = length as in
58 fixLazyApply n args' arity
59 [] -> chainAPPLY (LV (Glob n)) args'
60 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
70 aaF env (t, e) = (t, eEVAL (aa env e))
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)
76 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)
81 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)
86 chainAPPLY f [] = f
87 chainAPPLY f (a : as) = chainAPPLY (LApp False (LV (Glob (MN 0 "APPLY"))) [f, a]) as
89eEVAL x = LApp False (LV (Glob (MN 0 "EVAL"))) [x]
91data EvalApply a = EvalCase a
92 | ApplyCase a
93 deriving Show
95-- For a function name, generate a list of
96-- data constuctors, and whether to handle them in EVAL or APPLY
98toCons :: (Name, Int) -> [(Name, Int, EvalApply LAlt)]
99toCons (n, i)
100 = (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)))))))
103 : mkApplyCase n 0 i
105mkApplyCase fname n ar | n == ar = []
106mkApplyCase fname n ar
107 = 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) ++
111 [MN 0 "arg"])))))
112 : mkApplyCase fname (n + 1) ar
114mkEval :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
115mkEval xs = (MN 0 "EVAL", LFun (MN 0 "EVAL") [MN 0 "arg"]
116 (LCase (LV (Glob (MN 0 "arg")))
117 (mapMaybe evalCase xs ++
118 [LDefaultCase (LV (Glob (MN 0 "arg")))])))
119 where
120 evalCase (n, t, EvalCase x) = Just x
121 evalCase _ = Nothing
123mkApply :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
124mkApply 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"))])
127 (mapMaybe applyCase xs)))
128 where
129 applyCase (n, t, ApplyCase x) = Just x
130 applyCase _ = Nothing
132declare :: Int -> [(Name, Int, EvalApply LAlt)] -> [(Name, LDecl)]
133declare t xs = dec' t xs [] where
134 dec' t [] acc = reverse acc
135 dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, LConstructor n t ar) : acc)
138genArgs i = MN i "P_c" : genArgs (i + 1)
140mkFnCon n = MN 0 ("P_" ++ show n)
141mkUnderCon n 0 = n
142mkUnderCon n missing = MN missing ("U_" ++ show n)