@@ -3,8 +3,22 @@ module IRTS.Defunctionalise where
33import IRTS.Lang
44import Core.TT
55
6−defunctionalise :: [(Name, LDecl)] -> [(Name, LDecl)]
7−defunctionalise defs = defs -- TODO!
6+import Debug.Trace
7+import Data.Maybe
8+
9+defunctionalise :: Int -> LDefs -> LDefs
10+defunctionalise nexttag defs
11+ = let all = toAlist defs
12+ newcons = concatMap toCons (getFn all)
13+ eval = mkEval newcons
14+ app = mkApply newcons
15+ condecls = declare nexttag newcons in
16+ addAlist (eval : app : condecls ++ (map (addApps defs) all)) emptyContext
17+
18+getFn :: [(Name, LDecl)] -> [(Name, Int)]
19+getFn xs = mapMaybe fnData xs
20+ where fnData (n, LFun _ args _) = Just (n, length args)
21+ fnData _ = Nothing
822
923-- To defunctionalise:
1024--
@@ -16,5 +30,95 @@ defunctionalise defs = defs -- TODO!
1630-- 5 Create an APPLY function which adds an argument to each underapplication (or calls
1731-- APPLY again for an exact application)
1832-- 6 Wrap overapplications in chains of APPLY
33+-- 7 Wrap unknown applications (i.e. applications of local variables) in chains of APPLY
34+-- 8 Add explicit EVAL to case, primitives, and foreign calls
35+
36+addApps :: LDefs -> (Name, LDecl) -> (Name, LDecl)
37+addApps defs o@(n, LConstructor _ _ _) = o
38+addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))
39+ where
40+ aa env (LV (Glob n)) | n `elem` env = LV (Glob n)
41+ | otherwise = aa env (LApp False n [])
42+-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e
43+ aa env (LApp tc n args)
44+ = let args' = map (aa env) args in
45+ case lookupCtxt Nothing n defs of
46+ [LConstructor _ i ar] -> LApp tc n args'
47+ [LFun _ as _] -> let arity = length as in
48+ fixApply tc n args' arity
49+ [] -> chainAPPLY (LV (Glob n)) args'
50+ aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc)
51+ aa env (LCon i n args) = LCon i n (map (aa env) args)
52+ aa env (LCase e alts) = LCase (eEVAL (aa env e)) (map (aaAlt env) alts)
53+ aa env (LConst c) = LConst c
54+ aa env (LForeign l t n args) = LForeign l t n (map (aaF env) args)
55+ aa env (LOp f args) = LOp f (map (eEVAL . (aa env)) args)
56+
57+ aaF env (t, e) = (t, eEVAL (aa env e))
58+
59+ aaAlt env (LConCase i n args e) = LConCase i n args (aa (args ++ env) e)
60+ aaAlt env (LConstCase c e) = LConstCase c (aa env e)
61+ aaAlt env (LDefaultCase e) = LDefaultCase (aa env e)
62+
63+ eEVAL x = LApp False (MN 0 "EVAL") [x]
64+
65+ fixApply tc n args ar
66+ | length args == ar = LApp tc n args
67+ | length args < ar = LApp tc (mkUnderCon n (ar - length args)) args
68+ | length args > ar = chainAPPLY (LApp tc n (take ar args)) (drop ar args)
69+
70+ chainAPPLY f [] = f
71+ chainAPPLY f (a : as) = chainAPPLY (LApp False (MN 0 "APPLY") [f, a]) as
72+
73+data EvalApply a = EvalCase a
74+ | ApplyCase a
75+ deriving Show
76+
77+-- For a function name, generate a list of
78+-- data constuctors, and whether to handle them in EVAL or APPLY
79+
80+toCons :: (Name, Int) -> [(Name, Int, EvalApply LAlt)]
81+toCons (n, i) = (mkFnCon n, i,
82+ EvalCase (LConCase (-1) (mkFnCon n) (take i (genArgs 0))
83+ (LApp False n (map (LV . Glob) (take i (genArgs 0))))))
84+ :
85+ mkApplyCase n 0 i
86+
87+mkApplyCase fname n ar | n == ar = []
88+mkApplyCase fname n ar
89+ = let nm = mkUnderCon fname (ar - n) in
90+ (nm, n, ApplyCase (LConCase (-1) nm (take n (genArgs 0))
91+ (LApp False (mkUnderCon fname (ar - (n + 1)))
92+ (map (LV . Glob) (take n (genArgs 0) ++
93+ [MN 0 "arg"])))))
94+ : mkApplyCase fname (n + 1) ar
95+
96+mkEval :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
97+mkEval xs = (MN 0 "EVAL", LFun (MN 0 "EVAL") [MN 0 "arg"]
98+ (LCase (LV (Glob (MN 0 "arg")))
99+ (mapMaybe evalCase xs ++
100+ [LDefaultCase (LV (Glob (MN 0 "arg")))])))
101+ where
102+ evalCase (n, t, EvalCase x) = Just x
103+ evalCase _ = Nothing
104+
105+mkApply :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
106+mkApply xs = (MN 0 "APPLY", LFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]
107+ (LCase (LApp False (MN 0 "EVAL") [LV (Glob (MN 0 "fn"))])
108+ (mapMaybe applyCase xs)))
109+ where
110+ applyCase (n, t, ApplyCase x) = Just x
111+ applyCase _ = Nothing
112+
113+declare :: Int -> [(Name, Int, EvalApply LAlt)] -> [(Name, LDecl)]
114+declare t xs = dec' t xs [] where
115+ dec' t [] acc = reverse acc
116+ dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, LConstructor n t ar) : acc)
117+
118+
119+genArgs i = MN i "P_c" : genArgs (i + 1)
19120
121+mkFnCon n = MN 0 ("P_" ++ show n)
122+mkUnderCon n 0 = n
123+mkUnderCon n missing = MN missing ("U_" ++ show n)
20124