Mercurial > urweb

comparison src/elab_env.sml @ 467:3f1b9231a37b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Inserted a NULL value
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 15:37:38 -0500
parents d34834af4512
children 20fab0e96217
comparison
equal deleted inserted replaced
466:1626dcba13ee 467:3f1b9231a37b
148 148
149 datatype class_key = 149 datatype class_key =
150 CkNamed of int 150 CkNamed of int
151 | CkRel of int 151 | CkRel of int
152 | CkProj of int * string list * string 152 | CkProj of int * string list * string
153 | CkApp of class_key * class_key
153 154
154 fun ck2s ck = 155 fun ck2s ck =
155 case ck of 156 case ck of
156 CkNamed n => "Named(" ^ Int.toString n ^ ")" 157 CkNamed n => "Named(" ^ Int.toString n ^ ")"
157 | CkRel n => "Rel(" ^ Int.toString n ^ ")" 158 | CkRel n => "Rel(" ^ Int.toString n ^ ")"
158 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" 159 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
160 | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")"
159 161
160 fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")" 162 fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")"
161 163
162 structure KK = struct 164 structure KK = struct
163 type ord_key = class_key 165 type ord_key = class_key
174 176
175 | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) => 177 | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) =>
176 join (Int.compare (m1, m2), 178 join (Int.compare (m1, m2),
177 fn () => join (joinL String.compare (ms1, ms2), 179 fn () => join (joinL String.compare (ms1, ms2),
178 fn () => String.compare (x1, x2))) 180 fn () => String.compare (x1, x2)))
181 | (CkProj _, _) => LESS
182 | (_, CkProj _) => GREATER
183
184 | (CkApp (f1, x1), CkApp (f2, x2)) =>
185 join (compare (f1, f2),
186 fn () => compare (x1, x2))
179 end 187 end
180 188
181 structure KM = BinaryMapFn(KK) 189 structure KM = BinaryMapFn(KK)
182 190
183 type class = { 191 type class = {
249 fun liftClassKey ck = 257 fun liftClassKey ck =
250 case ck of 258 case ck of
251 CkNamed _ => ck 259 CkNamed _ => ck
252 | CkRel n => CkRel (n + 1) 260 | CkRel n => CkRel (n + 1)
253 | CkProj _ => ck 261 | CkProj _ => ck
262 | CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2)
254 263
255 fun pushCRel (env : env) x k = 264 fun pushCRel (env : env) x k =
256 let 265 let
257 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) 266 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
258 | x => x) (#renameC env) 267 | x => x) (#renameC env)
409 case c of 418 case c of
410 CRel n => SOME (CkRel n) 419 CRel n => SOME (CkRel n)
411 | CNamed n => SOME (CkNamed n) 420 | CNamed n => SOME (CkNamed n)
412 | CModProj x => SOME (CkProj x) 421 | CModProj x => SOME (CkProj x)
413 | CUnif (_, _, _, ref (SOME c)) => class_key_in c 422 | CUnif (_, _, _, ref (SOME c)) => class_key_in c
423 | CApp (c1, c2) =>
424 (case (class_key_in c1, class_key_in c2) of
425 (SOME k1, SOME k2) => SOME (CkApp (k1, k2))
426 | _ => NONE)
414 | _ => NONE 427 | _ => NONE
415 428
416 fun class_pair_in (c, _) = 429 fun class_pair_in (c, _) =
417 case c of 430 case c of
418 CApp (f, x) => 431 CApp (f, x) =>
651 in 664 in
652 CModProj (m1, ms, nx) 665 CModProj (m1, ms, nx)
653 end) 666 end)
654 | _ => c 667 | _ => c
655 668
656 fun sgnS_con' (m1, ms', (sgns, strs, cons)) c = 669 fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c =
657 case c of 670 case c of
658 CModProj (m1, ms, x) => 671 CModProj (m1, ms, x) =>
659 (case IM.find (strs, m1) of 672 (case IM.find (strs, m1) of
660 NONE => c 673 NONE => c
661 | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) 674 | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x))
662 | CNamed n => 675 | CNamed n =>
663 (case IM.find (cons, n) of 676 (case IM.find (cons, n) of
664 NONE => c 677 NONE => c
665 | SOME nx => CModProj (m1, ms', nx)) 678 | SOME nx => CModProj (m1, ms', nx))
679 | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1),
680 (sgnS_con' arg (#1 c2), #2 c2))
666 | _ => c 681 | _ => c
667 682
668 fun sgnS_sgn (str, (sgns, strs, cons)) sgn = 683 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
669 case sgn of 684 case sgn of
670 SgnProj (m1, ms, x) => 685 SgnProj (m1, ms, x) =>
1031 let 1046 let
1032 fun seek (n, xs, xncs) = 1047 fun seek (n, xs, xncs) =
1033 ListUtil.search (fn (x, _, to) => 1048 ListUtil.search (fn (x, _, to) =>
1034 if x = field then 1049 if x = field then
1035 SOME (let 1050 SOME (let
1051 val base = (CNamed n, #2 sgn)
1052 val nxs = length xs
1053 val base = ListUtil.foldli (fn (i, _, base) =>
1054 (CApp (base,
1055 (CRel (nxs - i - 1), #2 sgn)),
1056 #2 sgn))
1057 base xs
1058
1036 val t = 1059 val t =
1037 case to of 1060 case to of
1038 NONE => (CNamed n, #2 sgn) 1061 NONE => base
1039 | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn) 1062 | SOME t => (TFun (t, base), #2 sgn)
1040 val k = (KType, #2 sgn) 1063 val k = (KType, #2 sgn)
1041 in 1064 in
1042 foldr (fn (x, t) => (TCFun (Explicit, x, k, t), #2 sgn)) 1065 foldr (fn (x, t) => (TCFun (Implicit, x, k, t), #2 sgn))
1043 t xs 1066 t xs
1044 end) 1067 end)
1045 else 1068 else
1046 NONE) xncs 1069 NONE) xncs
1047 in 1070 in