Mercurial > urweb

comparison src/disjoint.sml @ 207:cc68da3801bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Non-star SELECT
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 18:35:08 -0400
parents 94ef20a31550
children 326fb4686f60
comparison
equal deleted inserted replaced
206:cb8493759a7b 207:cc68da3801bc
28 structure Disjoint :> DISJOINT = struct 28 structure Disjoint :> DISJOINT = struct
29 29
30 open Elab 30 open Elab
31 open ElabOps 31 open ElabOps
32 32
33 datatype piece = 33 datatype piece_fst =
34 NameC of string 34 NameC of string
35 | NameR of int 35 | NameR of int
36 | NameN of int 36 | NameN of int
37 | NameM of int * string list * string 37 | NameM of int * string list * string
38 | RowR of int 38 | RowR of int
39 | RowN of int 39 | RowN of int
40 | RowM of int * string list * string 40 | RowM of int * string list * string
41
42 type piece = piece_fst * int list
41 43
42 fun p2s p = 44 fun p2s p =
43 case p of 45 case p of
44 NameC s => "NameC(" ^ s ^ ")" 46 NameC s => "NameC(" ^ s ^ ")"
45 | NameR n => "NameR(" ^ Int.toString n ^ ")" 47 | NameR n => "NameR(" ^ Int.toString n ^ ")"
53 55
54 structure PK = struct 56 structure PK = struct
55 57
56 type ord_key = piece 58 type ord_key = piece
57 59
58 fun join (o1, o2) = 60 open Order
59 case o1 of 61
60 EQUAL => o2 () 62 fun compare' (p1, p2) =
61 | v => v
62
63 fun joinL f (os1, os2) =
64 case (os1, os2) of
65 (nil, nil) => EQUAL
66 | (nil, _) => LESS
67 | (h1 :: t1, h2 :: t2) =>
68 join (f (h1, h2), fn () => joinL f (t1, t2))
69 | (_ :: _, nil) => GREATER
70
71 fun compare (p1, p2) =
72 case (p1, p2) of 63 case (p1, p2) of
73 (NameC s1, NameC s2) => String.compare (s1, s2) 64 (NameC s1, NameC s2) => String.compare (s1, s2)
74 | (NameR n1, NameR n2) => Int.compare (n1, n2) 65 | (NameR n1, NameR n2) => Int.compare (n1, n2)
75 | (NameN n1, NameN n2) => Int.compare (n1, n2) 66 | (NameN n1, NameN n2) => Int.compare (n1, n2)
76 | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) => 67 | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) =>
100 | (_, RowR _) => GREATER 91 | (_, RowR _) => GREATER
101 92
102 | (RowN _, _) => LESS 93 | (RowN _, _) => LESS
103 | (_, RowN _) => GREATER 94 | (_, RowN _) => GREATER
104 95
96 fun compare ((p1, ns1), (p2, ns2)) =
97 join (compare' (p1, p2),
98 fn () => joinL Int.compare (ns1, ns2))
99
105 end 100 end
106 101
107 structure PS = BinarySetFn(PK) 102 structure PS = BinarySetFn(PK)
108 structure PM = BinaryMapFn(PK) 103 structure PM = BinaryMapFn(PK)
109 104
114 val empty = PM.empty 109 val empty = PM.empty
115 110
116 fun nameToRow (c, loc) = 111 fun nameToRow (c, loc) =
117 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) 112 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
118 113
119 fun pieceToRow (p, loc) = 114 fun pieceToRow' (p, loc) =
120 case p of 115 case p of
121 NameC s => nameToRow (CName s, loc) 116 NameC s => nameToRow (CName s, loc)
122 | NameR n => nameToRow (CRel n, loc) 117 | NameR n => nameToRow (CRel n, loc)
123 | NameN n => nameToRow (CNamed n, loc) 118 | NameN n => nameToRow (CNamed n, loc)
124 | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc) 119 | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc)
125 | RowR n => (CRel n, loc) 120 | RowR n => (CRel n, loc)
126 | RowN n => (CNamed n, loc) 121 | RowN n => (CNamed n, loc)
127 | RowM (n, xs, x) => (CModProj (n, xs, x), loc) 122 | RowM (n, xs, x) => (CModProj (n, xs, x), loc)
128 123
124 fun pieceToRow ((p, ns), loc) =
125 foldl (fn (n, c) => (CProj (c, n), loc)) (pieceToRow' (p, loc)) ns
126
129 datatype piece' = 127 datatype piece' =
130 Piece of piece 128 Piece of piece
131 | Unknown of con 129 | Unknown of con
132 130
133 fun pieceEnter p = 131 fun pieceEnter' p =
134 case p of 132 case p of
135 NameR n => NameR (n + 1) 133 NameR n => NameR (n + 1)
136 | RowR n => RowR (n + 1) 134 | RowR n => RowR (n + 1)
137 | _ => p 135 | _ => p
138 136
137 fun pieceEnter (p, n) = (pieceEnter' p, n)
138
139 fun enter denv = 139 fun enter denv =
140 PM.foldli (fn (p, pset, denv') => 140 PM.foldli (fn (p, pset, denv') =>
141 PM.insert (denv', pieceEnter p, PS.map pieceEnter pset)) 141 PM.insert (denv', pieceEnter p, PS.map pieceEnter pset))
142 PM.empty denv 142 PM.empty denv
143 143
144 fun prove1 denv (p1, p2) = 144 fun prove1 denv (p1, p2) =
145 case (p1, p2) of 145 case (p1, p2) of
146 (NameC s1, NameC s2) => s1 <> s2 146 ((NameC s1, _), (NameC s2, _)) => s1 <> s2
147 | _ => 147 | _ =>
148 case PM.find (denv, p1) of 148 case PM.find (denv, p1) of
149 NONE => false 149 NONE => false
150 | SOME pset => PS.member (pset, p2) 150 | SOME pset => PS.member (pset, p2)
151 151
152 fun decomposeRow (env, denv) c = 152 fun decomposeRow (env, denv) c =
153 let 153 let
154 fun decomposeProj c =
155 let
156 val (c, gs) = hnormCon (env, denv) c
157 in
158 case #1 c of
159 CProj (c, n) =>
160 let
161 val (c', ns, gs') = decomposeProj c
162 in
163 (c', ns @ [n], gs @ gs')
164 end
165 | _ => (c, [], gs)
166 end
167
154 fun decomposeName (c, (acc, gs)) = 168 fun decomposeName (c, (acc, gs)) =
155 let 169 let
156 val (cAll as (c, _), gs') = hnormCon (env, denv) c 170 val (cAll as (c, _), ns, gs') = decomposeProj c
157 171
158 val acc = case c of 172 val acc = case c of
159 CName s => Piece (NameC s) :: acc 173 CName s => Piece (NameC s, ns) :: acc
160 | CRel n => Piece (NameR n) :: acc 174 | CRel n => Piece (NameR n, ns) :: acc
161 | CNamed n => Piece (NameN n) :: acc 175 | CNamed n => Piece (NameN n, ns) :: acc
162 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x)) :: acc 176 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc
163 | _ => Unknown cAll :: acc 177 | _ => Unknown cAll :: acc
164 in 178 in
165 (acc, gs' @ gs) 179 (acc, gs' @ gs)
166 end 180 end
167 181
168 fun decomposeRow (c, (acc, gs)) = 182 fun decomposeRow (c, (acc, gs)) =
169 let 183 let
170 val (cAll as (c, _), gs') = hnormCon (env, denv) c 184 val (cAll as (c, _), ns, gs') = decomposeProj c
171 val gs = gs' @ gs 185 val gs = gs' @ gs
172 in 186 in
173 case c of 187 case c of
174 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs 188 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs
175 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, (acc, gs))) 189 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, (acc, gs)))
176 | CRel n => (Piece (RowR n) :: acc, gs) 190 | CRel n => (Piece (RowR n, ns) :: acc, gs)
177 | CNamed n => (Piece (RowN n) :: acc, gs) 191 | CNamed n => (Piece (RowN n, ns) :: acc, gs)
178 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x)) :: acc, gs) 192 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs)
179 | _ => (Unknown cAll :: acc, gs) 193 | _ => (Unknown cAll :: acc, gs)
180 end 194 end
181 in 195 in
182 decomposeRow (c, ([], [])) 196 decomposeRow (c, ([], []))
183 end 197 end
198 212
199 fun assertPiece ps (p, denv) = 213 fun assertPiece ps (p, denv) =
200 let 214 let
201 val pset = Option.getOpt (PM.find (denv, p), PS.empty) 215 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
202 val ps = case p of 216 val ps = case p of
203 NameC _ => List.filter (fn NameC _ => false | _ => true) ps 217 (NameC _, _) => List.filter (fn (NameC _, _) => false | _ => true) ps
204 | _ => ps 218 | _ => ps
205 val pset = PS.addList (pset, ps) 219 val pset = PS.addList (pset, ps)
206 in 220 in
207 PM.insert (denv, p, pset) 221 PM.insert (denv, p, pset)
208 end 222 end