Mercurial > urweb

comparison src/elab_env.sml @ 1795:d28adceef22a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Allow type class instances with hypotheses via local ('let') definitions
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 14:04:59 -0400
parents fca4a6d05ac1
children 0de0daab5fbb
comparison
equal deleted inserted replaced
1794:4671afac15af 1795:d28adceef22a
161 | _ => e, 161 | _ => e,
162 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) 162 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
163 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) 163 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
164 | (ctx, _) => ctx} 164 | (ctx, _) => ctx}
165 165
166 val openCon =
167 U.Con.existsB {kind = fn ((nk, _), k) =>
168 case k of
169 KRel n => n >= nk
170 | _ => false,
171 con = fn ((_, nc), c) =>
172 case c of
173 CRel n => n >= nc
174 | _ => false,
175 bind = fn (all as (nk, nc), b) =>
176 case b of
177 U.Con.RelK _ => (nk+1, nc)
178 | U.Con.RelC _ => (nk, nc+1)
179 | _ => all}
180 (0, 0)
181
166 (* Back to environments *) 182 (* Back to environments *)
167 183
168 datatype 'a var' = 184 datatype 'a var' =
169 Rel' of int * 'a 185 Rel' of int * 'a
170 | Named' of int * 'a 186 | Named' of int * 'a
206 end 222 end
207 223
208 structure CS = BinarySetFn(CK) 224 structure CS = BinarySetFn(CK)
209 structure CM = BinaryMapFn(CK) 225 structure CM = BinaryMapFn(CK)
210 226
211 type class = {ground : (con * exp) list, 227 type rules = (int * con list * con * exp) list
212 rules : (int * con list * con * exp) list} 228
213 val empty_class = {ground = [], 229 type class = {closedRules : rules,
214 rules = []} 230 openRules : rules}
231 val empty_class = {closedRules = [],
232 openRules = []}
215 233
216 type env = { 234 type env = {
217 renameK : int SM.map, 235 renameK : int SM.map,
218 relK : string list, 236 relK : string list,
219 237
284 namedC = #namedC env, 302 namedC = #namedC env,
285 303
286 datatypes = #datatypes env, 304 datatypes = #datatypes env,
287 constructors = #constructors env, 305 constructors = #constructors env,
288 306
289 classes = CM.map (fn cl => {ground = map (fn (c, e) => 307 classes = CM.map (fn cl => {closedRules = #closedRules cl,
290 (liftKindInCon 0 c, 308 openRules = map (fn (nvs, cs, c, e) =>
291 e)) 309 (nvs,
292 (#ground cl), 310 map (liftKindInCon 0) cs,
293 rules = #rules cl}) 311 liftKindInCon 0 c,
312 liftKindInExp 0 e))
313 (#openRules cl)})
294 (#classes env), 314 (#classes env),
295 315
296 renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c) 316 renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
297 | Named' (n, c) => Named' (n, c)) (#renameE env), 317 | Named' (n, c) => Named' (n, c)) (#renameE env),
298 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), 318 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
326 346
327 datatypes = #datatypes env, 347 datatypes = #datatypes env,
328 constructors = #constructors env, 348 constructors = #constructors env,
329 349
330 classes = CM.map (fn class => 350 classes = CM.map (fn class =>
331 {ground = map (fn (c, e) => 351 {closedRules = #closedRules class,
332 (liftConInCon 0 c, 352 openRules = map (fn (nvs, cs, c, e) =>
333 e)) 353 (nvs,
334 (#ground class), 354 map (liftConInCon 0) cs,
335 rules = #rules class}) 355 liftConInCon 0 c,
356 liftConInExp 0 e))
357 (#openRules class)})
336 (#classes env), 358 (#classes env),
337 359
338 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) 360 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
339 | Named' (n, c) => Named' (n, c)) (#renameE env), 361 | Named' (n, c) => Named' (n, c)) (#renameE env),
340 relE = map (fn (x, c) => (x, lift c)) (#relE env), 362 relE = map (fn (x, c) => (x, lift c)) (#relE env),
439 461
440 fun datatypeArgs (xs, _) = xs 462 fun datatypeArgs (xs, _) = xs
441 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt 463 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
442 464
443 fun listClasses (env : env) = 465 fun listClasses (env : env) =
444 map (fn (cn, {ground, rules}) => 466 map (fn (cn, {closedRules, openRules}) =>
445 (class_name_out cn, 467 (class_name_out cn,
446 ground 468 map (fn (nvs, cs, c, e) =>
447 @ map (fn (nvs, cs, c, e) =>
448 let 469 let
449 val loc = #2 c 470 val loc = #2 c
450 val c = foldr (fn (c', c) => (TFun (c', c), loc)) c cs 471 val c = foldr (fn (c', c) => (TFun (c', c), loc)) c cs
451 val c = ListUtil.foldli (fn (n, (), c) => (TCFun (Explicit, 472 val c = ListUtil.foldli (fn (n, (), c) => (TCFun (Explicit,
452 "x" ^ Int.toString n, 473 "x" ^ Int.toString n,
453 (KError, loc), 474 (KError, loc),
454 c), loc)) 475 c), loc))
455 c (List.tabulate (nvs, fn _ => ())) 476 c (List.tabulate (nvs, fn _ => ()))
456 in 477 in
457 (c, e) 478 (c, e)
458 end) rules)) (CM.listItemsi (#classes env)) 479 end) (closedRules @ openRules))) (CM.listItemsi (#classes env))
459 480
460 fun pushClass (env : env) n = 481 fun pushClass (env : env) n =
461 {renameK = #renameK env, 482 {renameK = #renameK env,
462 relK = #relK env, 483 relK = #relK env,
463 484
651 con = fn d => fn c => 672 con = fn d => fn c =>
652 case c of 673 case c of
653 CRel n => 674 CRel n =>
654 if n < d then 675 if n < d then
655 c 676 c
677 else if n - d >= length rs then
678 CRel (n - d)
656 else 679 else
657 #1 (List.nth (rs, n - d)) 680 #1 (List.nth (rs, n - d))
658 | _ => c, 681 | _ => c,
659 bind = fn (d, U.Con.RelC _) => d + 1 682 bind = fn (d, U.Con.RelC _) => d + 1
660 | (d, _) => d} 683 | (d, _) => d}
727 750
728 fun tryRules rules = 751 fun tryRules rules =
729 case rules of 752 case rules of
730 [] => notFound () 753 [] => notFound ()
731 | (nRs, cs, c', e) :: rules' => 754 | (nRs, cs, c', e) :: rules' =>
732 case tryUnify hnorm nRs (c, c') of 755 case tryUnify hnorm nRs (c, c') of
733 NONE => tryRules rules' 756 NONE => tryRules rules'
734 | SOME rs => 757 | SOME rs =>
735 let 758 let
736 val eos = map (resolve false o unifySubst rs) cs 759 val eos = map (resolve false o unifySubst rs) cs
737 in 760 in
747 val e = foldl (fn (e', e) => (EApp (e, e'), loc)) e es 770 val e = foldl (fn (e', e) => (EApp (e, e'), loc)) e es
748 in 771 in
749 SOME e 772 SOME e
750 end 773 end
751 end 774 end
752
753 fun rules () = tryRules (#rules class)
754
755 fun tryGrounds ces =
756 case ces of
757 [] => rules ()
758 | (c', e) :: ces' =>
759 case tryUnify hnorm 0 (c, c') of
760 NONE => tryGrounds ces'
761 | SOME _ => SOME e
762 in 775 in
763 tryGrounds (#ground class) 776 tryRules (#openRules class @ #closedRules class)
764 end 777 end
765 in 778 in
766 if startsWithUnif c then 779 if startsWithUnif c then
767 notFound () 780 notFound ()
768 else 781 else
798 in 811 in
799 cause := NONE; 812 cause := NONE;
800 resolve true 813 resolve true
801 end 814 end
802 815
803 fun pushERel (env : env) x t =
804 let
805 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
806 | x => x) (#renameE env)
807
808 val classes = CM.map (fn class =>
809 {ground = map (fn (c, e) => (c, liftExp e)) (#ground class),
810 rules = #rules class}) (#classes env)
811 val classes = case class_head_in t of
812 NONE => classes
813 | SOME f =>
814 case CM.find (classes, f) of
815 NONE => classes
816 | SOME class =>
817 let
818 val class = {ground = (t, (ERel 0, #2 t)) :: #ground class,
819 rules = #rules class}
820 in
821 CM.insert (classes, f, class)
822 end
823 in
824 {renameK = #renameK env,
825 relK = #relK env,
826
827 renameC = #renameC env,
828 relC = #relC env,
829 namedC = #namedC env,
830
831 datatypes = #datatypes env,
832 constructors = #constructors env,
833
834 classes = classes,
835
836 renameE = SM.insert (renameE, x, Rel' (0, t)),
837 relE = (x, t) :: #relE env,
838 namedE = #namedE env,
839
840 renameSgn = #renameSgn env,
841 sgn = #sgn env,
842
843 renameStr = #renameStr env,
844 str = #str env}
845 end
846
847 fun lookupERel (env : env) n =
848 (List.nth (#relE env, n))
849 handle Subscript => raise UnboundRel n
850
851 fun rule_in c = 816 fun rule_in c =
852 let 817 let
853 fun quantifiers (c, nvars) = 818 fun quantifiers (c, nvars) =
854 case #1 c of 819 case #1 c of
855 TCFun (_, _, _, c) => quantifiers (c, nvars + 1) 820 CUnif (_, _, _, _, ref (Known c)) => quantifiers (c, nvars)
821 | TCFun (_, _, _, c) => quantifiers (c, nvars + 1)
856 | _ => 822 | _ =>
857 let 823 let
858 fun clauses (c, hyps) = 824 fun clauses (c, hyps) =
859 case #1 c of 825 case #1 c of
860 TFun (hyp, c) => 826 TFun (hyp, c) =>
870 end 836 end
871 in 837 in
872 quantifiers (c, 0) 838 quantifiers (c, 0)
873 end 839 end
874 840
841 fun pushERel (env : env) x t =
842 let
843 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
844 | x => x) (#renameE env)
845
846 val classes = CM.map (fn class =>
847 {openRules = map (fn (nvs, cs, c, e) => (nvs, cs, c, liftExp e)) (#openRules class),
848 closedRules = #closedRules class}) (#classes env)
849 val classes = case rule_in t of
850 NONE => classes
851 | SOME (f, nvs, cs, c) =>
852 case CM.find (classes, f) of
853 NONE => classes
854 | SOME class =>
855 let
856 val rule = (nvs, cs, c, (ERel 0, #2 t))
857
858 val class =
859 if openCon t then
860 {openRules = rule :: #openRules class,
861 closedRules = #closedRules class}
862 else
863 {closedRules = rule :: #closedRules class,
864 openRules = #openRules class}
865 in
866 CM.insert (classes, f, class)
867 end
868 in
869 {renameK = #renameK env,
870 relK = #relK env,
871
872 renameC = #renameC env,
873 relC = #relC env,
874 namedC = #namedC env,
875
876 datatypes = #datatypes env,
877 constructors = #constructors env,
878
879 classes = classes,
880
881 renameE = SM.insert (renameE, x, Rel' (0, t)),
882 relE = (x, t) :: #relE env,
883 namedE = #namedE env,
884
885 renameSgn = #renameSgn env,
886 sgn = #sgn env,
887
888 renameStr = #renameStr env,
889 str = #str env}
890 end
891
892 fun lookupERel (env : env) n =
893 (List.nth (#relE env, n))
894 handle Subscript => raise UnboundRel n
895
875 fun pushENamedAs (env : env) x n t = 896 fun pushENamedAs (env : env) x n t =
876 let 897 let
877 val classes = #classes env 898 val classes = #classes env
878 val classes = case rule_in t of 899 val classes = case rule_in t of
879 NONE => classes 900 NONE => classes
883 | SOME class => 904 | SOME class =>
884 let 905 let
885 val e = (ENamed n, #2 t) 906 val e = (ENamed n, #2 t)
886 907
887 val class = 908 val class =
888 {ground = #ground class, 909 {openRules = #openRules class,
889 rules = (nvs, cs, c, e) :: #rules class} 910 closedRules = (nvs, cs, c, e) :: #closedRules class}
890 in 911 in
891 CM.insert (classes, f, class) 912 CM.insert (classes, f, class)
892 end 913 end
893 in 914 in
894 {renameK = #renameK env, 915 {renameK = #renameK env,
1208 | SOME class => 1229 | SOME class =>
1209 let 1230 let
1210 val e = (EModProj (m1, ms, x), #2 sgn) 1231 val e = (EModProj (m1, ms, x), #2 sgn)
1211 1232
1212 val class = 1233 val class =
1213 {ground = #ground class, 1234 {openRules = #openRules class,
1214 rules = (nvs, 1235 closedRules = (nvs,
1215 map globalize cs, 1236 map globalize cs,
1216 globalize c, 1237 globalize c,
1217 e) :: #rules class} 1238 e) :: #closedRules class}
1218 in 1239 in
1219 CM.insert (classes, cn, class) 1240 CM.insert (classes, cn, class)
1220 end 1241 end
1221 in 1242 in
1222 (classes, 1243 (classes,
1234 | SOME class => 1255 | SOME class =>
1235 let 1256 let
1236 val e = (EModProj (m1, ms, x), #2 sgn) 1257 val e = (EModProj (m1, ms, x), #2 sgn)
1237 1258
1238 val class = 1259 val class =
1239 {ground = #ground class, 1260 {openRules = #openRules class,
1240 rules = (nvs, 1261 closedRules = (nvs,
1241 map globalize cs, 1262 map globalize cs,
1242 globalize c, 1263 globalize c,
1243 e) :: #rules class} 1264 e) :: #closedRules class}
1244 in 1265 in
1245 CM.insert (classes, cn, class) 1266 CM.insert (classes, cn, class)
1246 end 1267 end
1247 in 1268 in
1248 (classes, 1269 (classes,