Mercurial > urweb

comparison src/reduce.sml @ 942:280f81731426

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Escape character constants; lift indices properly in Reduce 'case' simplification
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 12:41:54 -0400
parents be6585b4058b
children 2a50da66ffd8
comparison
equal deleted inserted replaced
941:b8d7a47b8e0c 942:280f81731426
102 | x => [x]) 102 | x => [x])
103 103
104 datatype result = Yes of env | No | Maybe 104 datatype result = Yes of env | No | Maybe
105 105
106 fun match (env, p : pat, e : exp) = 106 fun match (env, p : pat, e : exp) =
107 case (#1 p, #1 e) of 107 let
108 (PWild, _) => Yes env 108 val baseline = length env
109 | (PVar (x, t), _) => Yes (KnownE e :: env) 109
110 110 fun match (env, p, e) =
111 | (PPrim p, EPrim p') => 111 case (#1 p, #1 e) of
112 if Prim.equal (p, p') then 112 (PWild, _) => Yes env
113 Yes env 113 | (PVar (x, t), _) => Yes (KnownE (multiLiftExpInExp (length env - baseline) e) :: env)
114 else 114
115 No 115 | (PPrim p, EPrim p') =>
116 116 if Prim.equal (p, p') then
117 | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) => 117 Yes env
118 if n1 = n2 then 118 else
119 Yes env 119 No
120 else 120
121 No 121 | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) =>
122 122 if n1 = n2 then
123 | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) => 123 Yes env
124 if n1 = n2 then 124 else
125 match (env, p, e) 125 No
126 else 126
127 No 127 | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) =>
128 128 if n1 = n2 then
129 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE), 129 match (env, p, e)
130 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) => 130 else
131 if m1 = m2 andalso con1 = con2 then 131 No
132 Yes env 132
133 else 133 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE),
134 No 134 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) =>
135 135 if m1 = m2 andalso con1 = con2 then
136 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep), 136 Yes env
137 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) => 137 else
138 if m1 = m2 andalso con1 = con2 then 138 No
139 match (env, p, e) 139
140 else 140 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep),
141 No 141 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) =>
142 142 if m1 = m2 andalso con1 = con2 then
143 | (PRecord xps, ERecord xes) => 143 match (env, p, e)
144 if List.exists (fn ((CName _, _), _, _) => false 144 else
145 | _ => true) xes then 145 No
146 Maybe 146
147 else 147 | (PRecord xps, ERecord xes) =>
148 let 148 if List.exists (fn ((CName _, _), _, _) => false
149 fun consider (xps, env) = 149 | _ => true) xes then
150 case xps of 150 Maybe
151 [] => Yes env 151 else
152 | (x, p, _) :: rest => 152 let
153 case List.find (fn ((CName x', _), _, _) => x' = x 153 fun consider (xps, env) =
154 | _ => false) xes of 154 case xps of
155 NONE => No 155 [] => Yes env
156 | SOME (_, e, _) => 156 | (x, p, _) :: rest =>
157 case match (env, p, e) of 157 case List.find (fn ((CName x', _), _, _) => x' = x
158 No => No 158 | _ => false) xes of
159 | Maybe => Maybe 159 NONE => No
160 | Yes env => consider (rest, env) 160 | SOME (_, e, _) =>
161 in 161 case match (env, p, e) of
162 consider (xps, env) 162 No => No
163 end 163 | Maybe => Maybe
164 164 | Yes env => consider (rest, env)
165 | _ => Maybe 165 in
166 consider (xps, env)
167 end
168
169 | _ => Maybe
170 in
171 match (env, p, e)
172 end
166 173
167 fun kindConAndExp (namedC, namedE) = 174 fun kindConAndExp (namedC, namedE) =
168 let 175 let
169 fun kind env (all as (k, loc)) = 176 fun kind env (all as (k, loc)) =
170 case k of 177 case k of