Mercurial > urweb

comparison src/reduce.sml @ 508:04053089878a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of new Reduce
author Adam Chlipala <adamc@hcoop.net>
date Wed, 26 Nov 2008 12:13:00 -0500
parents ae03d09043c1
children 140c68046598
comparison
equal deleted inserted replaced
507:ca95f9e4d45f 508:04053089878a
29 29
30 structure Reduce :> REDUCE = struct 30 structure Reduce :> REDUCE = 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 liftConInCon = E.liftConInCon 36 datatype env_item =
38 val subConInCon = E.subConInCon 37 UnknownC
39 val liftConInExp = E.liftConInExp 38 | KnownC of con
40 val liftExpInExp = E.liftExpInExp
41 val subExpInExp = E.subExpInExp
42 val liftConInExp = E.liftConInExp
43 val subConInExp = E.subConInExp
44 39
45 fun bindC (env, b) = 40 | UnknownE
46 case b of 41 | KnownE of exp
47 U.Con.Rel (x, k) => E.pushCRel env x k
48 | U.Con.Named (x, n, k, co) => E.pushCNamed env x n k co
49 42
50 fun bind (env, b) = 43 | Lift of int * int
51 case b of
52 U.Decl.RelC (x, k) => E.pushCRel env x k
53 | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co
54 | U.Decl.RelE (x, t) => E.pushERel env x t
55 | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s
56 44
57 fun kind k = k 45 type env = env_item list
58 46
59 fun con env c = 47 fun conAndExp (namedC, namedE) =
60 case c of 48 let
61 CApp ((CApp ((CApp ((CFold ks, _), f), _), i), loc), (CRecord (k, xcs), _)) => 49 fun con env (all as (c, loc)) =
62 (case xcs of 50 case c of
63 [] => #1 i 51 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
64 | (n, v) :: rest => 52 | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc)
65 #1 (reduceCon env (CApp ((CApp ((CApp (f, n), loc), v), loc), 53 | TRecord c => (TRecord (con env c), loc)
66 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
67 (CRecord (k, rest), loc)), loc)), loc)))
68 | CApp ((CAbs (_, _, c1), loc), c2) =>
69 #1 (reduceCon env (subConInCon (0, c2) c1))
70 | CNamed n =>
71 (case E.lookupCNamed env n of
72 (_, _, SOME c') => #1 c'
73 | _ => c)
74 | CConcat ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => CRecord (k, xcs1 @ xcs2)
75 54
76 | CProj ((CTuple cs, _), n) => #1 (List.nth (cs, n - 1)) 55 | CRel n =>
56 let
57 fun find (n', env, lift) =
58 if n' = 0 then
59 case env of
60 UnknownC :: _ => (CRel (n + lift), loc)
61 | KnownC c :: _ => con (Lift (lift, 0) :: env) c
62 | _ => raise Fail "Reduce.con: CRel [1]"
63 else
64 case env of
65 UnknownC :: rest => find (n' - 1, rest, lift + 1)
66 | KnownC _ :: rest => find (n' - 1, rest, lift)
67 | UnknownE :: rest => find (n' - 1, rest, lift)
68 | KnownE _ :: rest => find (n' - 1, rest, lift)
69 | Lift (lift', _) :: rest => find (n' - 1, rest, lift + lift')
70 | [] => raise Fail "Reduce.con: CRel [2]"
71 in
72 find (n, env, 0)
73 end
74 | CNamed n =>
75 (case IM.find (namedC, n) of
76 NONE => all
77 | SOME c => c)
78 | CFfi _ => all
79 | CApp (c1, c2) =>
80 let
81 val c1 = con env c1
82 val c2 = con env c2
83 in
84 case #1 c1 of
85 CAbs (_, _, b) =>
86 con (KnownC c2 :: env) b
77 87
78 | _ => c 88 | CApp ((CApp (fold as (CFold _, _), f), _), i) =>
89 (case #1 c2 of
90 CRecord (_, []) => i
91 | CRecord (k, (x, c) :: rest) =>
92 con env (CApp ((CApp ((CApp (f, x), loc), c), loc),
93 (CApp ((CApp ((CApp (fold, f), loc), i), loc),
94 (CRecord (k, rest), loc)), loc)), loc)
95 | _ => (CApp (c1, c2), loc))
79 96
80 and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env 97 | _ => (CApp (c1, c2), loc)
98 end
99 | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
81 100
82 fun exp env e = 101 | CName _ => all
83 let
84 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*)
85 102
86 val r = case e of 103 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
87 ENamed n => 104 | CConcat (c1, c2) =>
88 (case E.lookupENamed env n of 105 let
89 (_, _, SOME e', _) => #1 e' 106 val c1 = con env c1
90 | _ => e) 107 val c2 = con env c2
108 in
109 case (#1 c1, #1 c2) of
110 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
111 (CRecord (k, xcs1 @ xcs2), loc)
112 | _ => (CConcat (c1, c2), loc)
113 end
114 | CFold _ => all
91 115
92 | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) => 116 | CUnit => all
93 (case xcs of
94 [] => #1 i
95 | (n, v) :: rest =>
96 #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc),
97 (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc),
98 (CRecord (k, rest), loc)), loc)), loc)))
99 117
100 | EApp ((EAbs (_, _, _, e1), loc), e2) => 118 | CTuple cs => (CTuple (map (con env) cs), loc)
101 #1 (reduceExp env (subExpInExp (0, e2) e1)) 119 | CProj (c, n) =>
102 | ECApp ((ECAbs (_, _, e1), loc), c) => 120 let
103 #1 (reduceExp env (subConInExp (0, c) e1)) 121 val c = con env c
122 in
123 case #1 c of
124 CTuple cs => List.nth (cs, n - 1)
125 | _ => (CProj (c, n), loc)
126 end
104 127
105 | EField ((ERecord xes, _), (CName x, _), _) => 128 fun exp env e = e
106 (case List.find (fn ((CName x', _), _, _) => x' = x
107 | _ => false) xes of
108 SOME (_, e, _) => #1 e
109 | NONE => e)
110 | EConcat (r1 as (_, loc), (CRecord (k, xts1), _), r2, (CRecord (_, xts2), _)) =>
111 let
112 fun fields (r, remaining, passed) =
113 case remaining of
114 [] => []
115 | (x, t) :: rest =>
116 (x,
117 (EField (r, x, {field = t,
118 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
119 t) :: fields (r, rest, (x, t) :: passed)
120 in
121 #1 (reduceExp env (ERecord (fields (r1, xts1, []) @ fields (r2, xts2, [])), loc))
122 end
123 | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
124 let
125 fun fields (remaining, passed) =
126 case remaining of
127 [] => []
128 | (x, t) :: rest =>
129 (x,
130 (EField (r, x, {field = t,
131 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
132 t) :: fields (rest, (x, t) :: passed)
133 in
134 #1 (reduceExp env (ERecord (fields (xts, [])), loc))
135 end
136 | ECutMulti (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
137 let
138 fun fields (remaining, passed) =
139 case remaining of
140 [] => []
141 | (x, t) :: rest =>
142 (x,
143 (EField (r, x, {field = t,
144 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
145 t) :: fields (rest, (x, t) :: passed)
146 in
147 #1 (reduceExp env (ERecord (fields (xts, [])), loc))
148 end
149
150 | _ => e
151 in 129 in
152 (*Print.prefaces "exp'" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan)), 130 {con = con, exp = exp}
153 ("r", CorePrint.p_exp env (r, ErrorMsg.dummySpan))];*)
154
155 r
156 end 131 end
157 132
158 and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env 133 fun con namedC c = #con (conAndExp (namedC, IM.empty)) [] c
134 fun exp (namedC, namedE) e = #exp (conAndExp (namedC, namedE)) [] e
159 135
160 fun decl env d = 136 fun reduce file =
161 case d of 137 let
162 DValRec [vi as (_, n, _, e, _)] => 138 fun doDecl (d as (_, loc), st as (namedC, namedE)) =
163 let 139 case #1 d of
164 fun kind _ = false 140 DCon (x, n, k, c) =>
165 fun con _ = false 141 let
166 fun exp e = 142 val c = con namedC c
167 case e of 143 in
168 ENamed n' => n' = n 144 ((DCon (x, n, k, c), loc),
169 | _ => false 145 (IM.insert (namedC, n, c), namedE))
170 in 146 end
171 if U.Exp.exists {kind = kind, con = con, exp = exp} e then 147 | DDatatype (x, n, ps, cs) =>
172 d 148 ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC) co)) cs), loc),
173 else 149 st)
174 DVal vi 150 | DVal (x, n, t, e, s) =>
175 end 151 let
176 | _ => d 152 val t = con namedC t
153 val e = exp (namedC, namedE) e
154 in
155 ((DVal (x, n, t, e, s), loc),
156 (namedC, IM.insert (namedE, n, e)))
157 end
158 | DValRec vis =>
159 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC t, exp (namedC, namedE) e, s)) vis), loc),
160 st)
161 | DExport _ => (d, st)
162 | DTable (s, n, c, s') => ((DTable (s, n, con namedC c, s'), loc), st)
163 | DSequence _ => (d, st)
164 | DDatabase _ => (d, st)
165 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC c, s'), loc), st)
177 166
178 val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} E.empty 167 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
168 in
169 file
170 end
179 171
180 end 172 end