Mercurial > urweb

comparison src/disjoint.sml @ 90:94ef20a31550

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fancier head normalization pushed inside of Disjoint
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jul 2008 11:04:25 -0400
parents 7bab29834cd6
children cc68da3801bc
comparison
equal deleted inserted replaced
89:d3ee072fa609 90:94ef20a31550
107 structure PS = BinarySetFn(PK) 107 structure PS = BinarySetFn(PK)
108 structure PM = BinaryMapFn(PK) 108 structure PM = BinaryMapFn(PK)
109 109
110 type env = PS.set PM.map 110 type env = PS.set PM.map
111 111
112 type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con
113
112 val empty = PM.empty 114 val empty = PM.empty
113 115
114 fun nameToRow (c, loc) = 116 fun nameToRow (c, loc) =
115 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) 117 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
116 118
126 128
127 datatype piece' = 129 datatype piece' =
128 Piece of piece 130 Piece of piece
129 | Unknown of con 131 | Unknown of con
130 132
131 fun decomposeRow env c =
132 let
133 fun decomposeName (c, acc) =
134 case #1 (hnormCon env c) of
135 CName s => Piece (NameC s) :: acc
136 | CRel n => Piece (NameR n) :: acc
137 | CNamed n => Piece (NameN n) :: acc
138 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x)) :: acc
139 | _ => Unknown c :: acc
140
141 fun decomposeRow (c, acc) =
142 case #1 (hnormCon env c) of
143 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
144 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
145 | CRel n => Piece (RowR n) :: acc
146 | CNamed n => Piece (RowN n) :: acc
147 | CModProj (m1, ms, x) => Piece (RowM (m1, ms, x)) :: acc
148 | _ => Unknown c :: acc
149 in
150 decomposeRow (c, [])
151 end
152
153 fun assert env denv (c1, c2) =
154 let
155 val ps1 = decomposeRow env c1
156 val ps2 = decomposeRow env c2
157
158 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
159 val ps1 = unUnknown ps1
160 val ps2 = unUnknown ps2
161
162 (*val () = print "APieces1:\n"
163 val () = app pp ps1
164 val () = print "APieces2:\n"
165 val () = app pp ps2*)
166
167 fun assertPiece ps (p, denv) =
168 let
169 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
170 val pset = PS.addList (pset, ps)
171 in
172 PM.insert (denv, p, pset)
173 end
174
175 val denv = foldl (assertPiece ps2) denv ps1
176 in
177 foldl (assertPiece ps1) denv ps2
178 end
179
180 fun pieceEnter p = 133 fun pieceEnter p =
181 case p of 134 case p of
182 NameR n => NameR (n + 1) 135 NameR n => NameR (n + 1)
183 | RowR n => RowR (n + 1) 136 | RowR n => RowR (n + 1)
184 | _ => p 137 | _ => p
194 | _ => 147 | _ =>
195 case PM.find (denv, p1) of 148 case PM.find (denv, p1) of
196 NONE => false 149 NONE => false
197 | SOME pset => PS.member (pset, p2) 150 | SOME pset => PS.member (pset, p2)
198 151
199 fun prove env denv (c1, c2, loc) = 152 fun decomposeRow (env, denv) c =
200 let 153 let
201 val ps1 = decomposeRow env c1 154 fun decomposeName (c, (acc, gs)) =
202 val ps2 = decomposeRow env c2 155 let
156 val (cAll as (c, _), gs') = hnormCon (env, denv) c
157
158 val acc = case c of
159 CName s => Piece (NameC s) :: acc
160 | CRel n => Piece (NameR n) :: acc
161 | CNamed n => Piece (NameN n) :: acc
162 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x)) :: acc
163 | _ => Unknown cAll :: acc
164 in
165 (acc, gs' @ gs)
166 end
167
168 fun decomposeRow (c, (acc, gs)) =
169 let
170 val (cAll as (c, _), gs') = hnormCon (env, denv) c
171 val gs = gs' @ gs
172 in
173 case c of
174 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs
175 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, (acc, gs)))
176 | CRel n => (Piece (RowR n) :: acc, gs)
177 | CNamed n => (Piece (RowN n) :: acc, gs)
178 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x)) :: acc, gs)
179 | _ => (Unknown cAll :: acc, gs)
180 end
181 in
182 decomposeRow (c, ([], []))
183 end
184
185 and assert env denv (c1, c2) =
186 let
187 val (ps1, gs1) = decomposeRow (env, denv) c1
188 val (ps2, gs2) = decomposeRow (env, denv) c2
189
190 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
191 val ps1 = unUnknown ps1
192 val ps2 = unUnknown ps2
193
194 (*val () = print "APieces1:\n"
195 val () = app pp ps1
196 val () = print "APieces2:\n"
197 val () = app pp ps2*)
198
199 fun assertPiece ps (p, denv) =
200 let
201 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
202 val ps = case p of
203 NameC _ => List.filter (fn NameC _ => false | _ => true) ps
204 | _ => ps
205 val pset = PS.addList (pset, ps)
206 in
207 PM.insert (denv, p, pset)
208 end
209
210 val denv = foldl (assertPiece ps2) denv ps1
211 in
212 (foldl (assertPiece ps1) denv ps2, gs1 @ gs2)
213 end
214
215 and prove env denv (c1, c2, loc) =
216 let
217 val (ps1, gs1) = decomposeRow (env, denv) c1
218 val (ps2, gs2) = decomposeRow (env, denv) c2
203 219
204 val hasUnknown = List.exists (fn Unknown _ => true | _ => false) 220 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
205 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) 221 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
206 in 222 in
207 if hasUnknown ps1 orelse hasUnknown ps2 then 223 if hasUnknown ps1 orelse hasUnknown ps2 then
208 [(c1, c2)] 224 [(loc, env, denv, c1, c2)]
209 else 225 else
210 let 226 let
211 val ps1 = unUnknown ps1 227 val ps1 = unUnknown ps1
212 val ps2 = unUnknown ps2 228 val ps2 = unUnknown ps2
213 229
220 foldl (fn (p1, rem) => 236 foldl (fn (p1, rem) =>
221 foldl (fn (p2, rem) => 237 foldl (fn (p2, rem) =>
222 if prove1 denv (p1, p2) then 238 if prove1 denv (p1, p2) then
223 rem 239 rem
224 else 240 else
225 (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2) 241 (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
226 [] ps1 242 (gs1 @ gs2) ps1
227 end 243 end
244 end
245
246 and hnormCon (env, denv) c =
247 let
248 val cAll as (c, loc) = ElabOps.hnormCon env c
249
250 fun doDisj (c1, c2, c) =
251 let
252 val (c, gs) = hnormCon (env, denv) c
253 in
254 (c, prove env denv (c1, c2, loc) @ gs)
255 end
256 in
257 case c of
258 CDisjoint cs => doDisj cs
259 | TDisjoint cs => doDisj cs
260 | _ => (cAll, [])
228 end 261 end
229 262
230 end 263 end