Mercurial > urweb

comparison src/reduce_local.sml @ 512:40b19310ea9a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port Reduce improvements to ReduceLocal
author Adam Chlipala <adamc@hcoop.net>
date Wed, 26 Nov 2008 15:42:00 -0500
parents 9117a7bf229c
children 0dd40b6bfdf3
comparison
equal deleted inserted replaced
511:6d6222e045b0 512:40b19310ea9a
29 29
30 structure ReduceLocal :> REDUCE_LOCAL = struct 30 structure ReduceLocal :> REDUCE_LOCAL = struct
31 31
32 open Core 32 open Core
33 33
34 structure E = CoreEnv 34 structure IM = IntBinaryMap
35 structure U = CoreUtil
36 35
37 val subExpInExp = E.subExpInExp 36 datatype env_item =
37 Unknown
38 | Known of exp
38 39
39 fun default x = x 40 | Lift of int
40 41
41 fun exp (e : exp') = 42 type env = env_item list
43
44 val deKnown = List.filter (fn Known _ => false
45 | _ => true)
46
47 fun exp env (all as (e, loc)) =
48 case e of
49 EPrim _ => all
50 | ERel n =>
51 let
52 fun find (n', env, nudge, lift) =
53 case env of
54 [] => raise Fail "ReduceLocal.exp: ERel"
55 | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift')
56 | Unknown :: rest =>
57 if n' = 0 then
58 (ERel (n + nudge), loc)
59 else
60 find (n' - 1, rest, nudge, lift + 1)
61 | Known e :: rest =>
62 if n' = 0 then
63 ((*print "SUBSTITUTING\n";*)
64 exp (Lift lift :: rest) e)
65 else
66 find (n' - 1, rest, nudge - 1, lift)
67 in
68 find (n, env, 0, 0)
69 end
70 | ENamed _ => all
71 | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc)
72 | EFfi _ => all
73 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
74
75 | EApp (e1, e2) =>
76 let
77 val e1 = exp env e1
78 val e2 = exp env e2
79 in
80 case #1 e1 of
81 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
82 | _ => (EApp (e1, e2), loc)
83 end
84
85 | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
86
87 | ECApp (e, c) => (ECApp (exp env e, c), loc)
88
89 | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
90
91 | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc)
92 | EField (e, c, others) =>
93 let
94 val e = exp env e
95
96 fun default () = (EField (e, c, others), loc)
97 in
98 case (#1 e, #1 c) of
99 (ERecord xcs, CName x) =>
100 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
101 NONE => default ()
102 | SOME (_, e, _) => e)
103 | _ => default ()
104 end
105
106 | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc)
107 | ECut (e, c, others) => (ECut (exp env e, c, others), loc)
108 | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
109
110 | EFold _ => all
111
112 | ECase (e, pes, others) =>
113 let
114 fun patBinds (p, _) =
115 case p of
116 PWild => 0
117 | PVar _ => 1
118 | PPrim _ => 0
119 | PCon (_, _, _, NONE) => 0
120 | PCon (_, _, _, SOME p) => patBinds p
121 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
122 in
123 (ECase (exp env e,
124 map (fn (p, e) => (p,
125 exp (List.tabulate (patBinds p, fn _ => Unknown) @ env) e))
126 pes, others), loc)
127 end
128
129 | EWrite e => (EWrite (exp env e), loc)
130 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
131
132 | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc)
133
134 fun reduce file =
42 let 135 let
43 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*) 136 fun doDecl (d as (_, loc)) =
44 137 case #1 d of
45 val r = case e of 138 DCon _ => d
46 EApp ((EAbs (x, t, _, e1), loc), e2) => 139 | DDatatype _ => d
47 ((*Print.prefaces "Substitute" [("x", Print.PD.string x), 140 | DVal (x, n, t, e, s) =>
48 ("t", CorePrint.p_con CoreEnv.empty t)];*) 141 let
49 #1 (reduceExp (subExpInExp (0, e2) e1))) 142 val e = exp [] e
50 143 in
51 | EField ((ERecord xes, _), (CName x, _), _) => 144 (DVal (x, n, t, e, s), loc)
52 (case List.find (fn ((CName x', _), _, _) => x' = x 145 end
53 | _ => false) xes of 146 | DValRec vis =>
54 SOME (_, (e, _), _) => e 147 (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc)
55 | NONE => e) 148 | DExport _ => d
56 149 | DTable _ => d
57 | _ => e 150 | DSequence _ => d
151 | DDatabase _ => d
152 | DCookie _ => d
58 in 153 in
59 (*Print.prefaces "exp'" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan)), 154 map doDecl file
60 ("r", CorePrint.p_exp env (r, ErrorMsg.dummySpan))];*)
61
62 r
63 end 155 end
64 156
65 and reduceExp e = U.Exp.map {kind = default, con = default, exp = exp} e
66
67 val reduce = U.File.map {kind = default, con = default, exp = exp, decl = default}
68
69 end 157 end