Mercurial > urweb

comparison src/elab_ops.sml @ 329:eec65c11d3e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
foldTR2
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 10:30:45 -0400
parents 58f1260f293f
children 075b36dbb1a4
comparison
equal deleted inserted replaced
328:58f1260f293f 329:eec65c11d3e2
125 hnormCon env 125 hnormCon env
126 (CApp ((CApp ((CApp (f, x), loc), c), loc), 126 (CApp ((CApp ((CApp (f, x), loc), c), loc),
127 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), 127 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
128 rest''), loc)), loc) 128 rest''), loc)), loc)
129 end 129 end
130 | _ => default ()) 130 | _ =>
131 let
132 fun cunif () =
133 let
134 val r = ref NONE
135 in
136 (r, (CUnif (loc, (KType, loc), "_", r), loc))
137 end
138
139 val (nmR, nm) = cunif ()
140 val (vR, v) = cunif ()
141 val (rR, r) = cunif ()
142
143 val c = f
144 val c = (CApp (c, nm), loc)
145 val c = (CApp (c, v), loc)
146 val c = (CApp (c, r), loc)
147 fun unconstraint c =
148 case hnormCon env c of
149 (CDisjoint (_, _, c), _) => unconstraint c
150 | c => c
151 val c = unconstraint c
152 in
153 (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
154 case (hnormCon env i, unconstraint c) of
155 ((CRecord (_, []), _),
156 (CConcat (c1, c2'), _)) =>
157 (case (hnormCon env c1, hnormCon env c2') of
158 ((CRecord (_, [(nm', v')]), _),
159 (CUnif (_, _, _, rR'), _)) =>
160 (case (hnormCon env nm', hnormCon env v') of
161 ((CUnif (_, _, _, nmR'), _),
162 (CUnif (_, _, _, vR'), _)) =>
163 if nmR' = nmR andalso vR' = vR andalso rR' = rR then
164 hnormCon env c2
165 else
166 default ()
167 | _ => default ())
168 | _ => default ())
169 | _ => default ()
170 end)
131 | _ => default ()) 171 | _ => default ())
132 | _ => default () 172 | _ => default ()
133 end 173 end
134 | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) 174 | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
135 175
139 (CRecord (k, xcs1 @ xcs2), loc) 179 (CRecord (k, xcs1 @ xcs2), loc)
140 | ((CRecord (_, []), _), c2') => c2' 180 | ((CRecord (_, []), _), c2') => c2'
141 | ((CConcat (c11, c12), loc), c2') => 181 | ((CConcat (c11, c12), loc), c2') =>
142 hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc) 182 hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
143 | (c1', (CRecord (_, []), _)) => c1' 183 | (c1', (CRecord (_, []), _)) => c1'
144 | _ => cAll) 184 | (c1', c2') => (CConcat (c1', c2'), loc))
145 185
146 | CProj (c, n) => 186 | CProj (c, n) =>
147 (case hnormCon env c of 187 (case hnormCon env c of
148 (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1)) 188 (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1))
149 | _ => cAll) 189 | _ => cAll)