Mercurial > urweb

comparison src/elaborate.sml @ 2280:985c8016b592

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge.
author Ziv Scully <ziv@mit.edu>
date Thu, 12 Nov 2015 08:46:51 -0500
parents 22117edf8fd3
children fb113569519e
comparison
equal deleted inserted replaced
2279:32a407902d3b 2280:985c8016b592
2479 | SOME cs => 2479 | SOME cs =>
2480 case #1 (hnormSgn env sgn) of 2480 case #1 (hnormSgn env sgn) of
2481 L'.SgnConst sgis => 2481 L'.SgnConst sgis =>
2482 foldl (fn (sgi, cs) => 2482 foldl (fn (sgi, cs) =>
2483 case #1 sgi of 2483 case #1 sgi of
2484 L'.SgiStr (x, _, _) => 2484 L'.SgiStr (L'.Import, x, _, _) =>
2485 (case E.projectStr env {sgn = sgn, str = st, field = x} of 2485 (case E.projectStr env {sgn = sgn, str = st, field = x} of
2486 NONE => raise Fail "Elaborate: projectStr in collect" 2486 NONE => raise Fail "Elaborate: projectStr in collect"
2487 | SOME sgn' => 2487 | SOME sgn' =>
2488 List.revAppend (collect false ((L'.StrProj (st, x), loc), sgn'), 2488 List.revAppend (collect false ((L'.StrProj (st, x), loc), sgn'),
2489 cs)) 2489 cs))
2491 | _ => cs 2491 | _ => cs
2492 in 2492 in
2493 foldl (fn ((c1, c2), denv) => 2493 foldl (fn ((c1, c2), denv) =>
2494 D.assert env denv (c1, c2)) denv (collect true (st, sgn)) 2494 D.assert env denv (c1, c2)) denv (collect true (st, sgn))
2495 end 2495 end
2496
2497 fun tcdump env =
2498 Print.preface("Instances", p_list_sep Print.PD.newline
2499 (fn (cl, ls) =>
2500 box [p_con env cl,
2501 box [Print.PD.string "{",
2502 p_list (fn (t, e) =>
2503 box [p_exp env e,
2504 Print.PD.string " : ",
2505 p_con env t]) ls,
2506 Print.PD.string "}"]])
2507 (E.listClasses env))
2496 2508
2497 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 2509 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
2498 ((*Print.preface ("elabSgi", SourcePrint.p_sgn_item (sgi, loc));*) 2510 ((*Print.preface ("elabSgi", SourcePrint.p_sgn_item (sgi, loc));*)
2499 case sgi of 2511 case sgi of
2500 L.SgiConAbs (x, k) => 2512 L.SgiConAbs (x, k) =>
2693 let 2705 let
2694 val (sgn', gs') = elabSgn (env, denv) sgn 2706 val (sgn', gs') = elabSgn (env, denv) sgn
2695 val (env', n) = E.pushStrNamed env x sgn' 2707 val (env', n) = E.pushStrNamed env x sgn'
2696 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} 2708 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []}
2697 in 2709 in
2698 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv', gs' @ gs)) 2710 ([(L'.SgiStr (L'.Import, x, n, sgn'), loc)], (env', denv', gs' @ gs))
2699 end 2711 end
2700 2712
2701 | L.SgiSgn (x, sgn) => 2713 | L.SgiSgn (x, sgn) =>
2702 let 2714 let
2703 val (sgn', gs') = elabSgn (env, denv) sgn 2715 val (sgn', gs') = elabSgn (env, denv) sgn
2812 (if SS.member (sgns, x) then 2824 (if SS.member (sgns, x) then
2813 sgnError env (DuplicateSgn (loc, x)) 2825 sgnError env (DuplicateSgn (loc, x))
2814 else 2826 else
2815 (); 2827 ();
2816 (cons, vals, SS.add (sgns, x), strs)) 2828 (cons, vals, SS.add (sgns, x), strs))
2817 | L'.SgiStr (x, _, _) => 2829 | L'.SgiStr (_, x, _, _) =>
2818 (if SS.member (strs, x) then 2830 (if SS.member (strs, x) then
2819 sgnError env (DuplicateStr (loc, x)) 2831 sgnError env (DuplicateStr (loc, x))
2820 else 2832 else
2821 (); 2833 ();
2822 (cons, vals, sgns, SS.add (strs, x))) 2834 (cons, vals, sgns, SS.add (strs, x)))
2863 List.exists (fn (L'.SgiConAbs (x', _, k), _) => 2875 List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
2864 List.null ms andalso x' = x andalso 2876 List.null ms andalso x' = x andalso
2865 (unifyKinds env k ck 2877 (unifyKinds env k ck
2866 handle KUnify x => sgnError env (WhereWrongKind x); 2878 handle KUnify x => sgnError env (WhereWrongKind x);
2867 true) 2879 true)
2868 | (L'.SgiStr (x', _, sgn''), _) => 2880 | (L'.SgiStr (_, x', _, sgn''), _) =>
2869 (case ms of 2881 (case ms of
2870 [] => false 2882 [] => false
2871 | m :: ms' => 2883 | m :: ms' =>
2872 m = x' andalso 2884 m = x' andalso
2873 checkPath (ms', sgn'')) 2885 checkPath (ms', sgn''))
2912 [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] 2924 [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
2913 | (L'.SgiDatatype dts, loc) => 2925 | (L'.SgiDatatype dts, loc) =>
2914 map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts 2926 map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts
2915 | (L'.SgiClassAbs (x, n, k), loc) => 2927 | (L'.SgiClassAbs (x, n, k), loc) =>
2916 [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] 2928 [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
2917 | (L'.SgiStr (x, n, sgn), loc) => 2929 | (L'.SgiStr (im, x, n, sgn), loc) =>
2918 [(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)] 2930 [(L'.SgiStr (im, x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)]
2919 | x => [x], 2931 | x => [x],
2920 E.sgiBinds env sgi)) env sgis)), #2 sgn) 2932 E.sgiBinds env sgi)) env sgis)), #2 sgn)
2921 | L'.SgnFun _ => sgn 2933 | L'.SgnFun _ => sgn
2922 | L'.SgnWhere _ => sgn 2934 | L'.SgnWhere _ => sgn
2923 | L'.SgnProj (m, ms, x) => 2935 | L'.SgnProj (m, ms, x) =>
2985 | L'.SgiVal (x, n, t) => 2997 | L'.SgiVal (x, n, t) =>
2986 if isVisible x then 2998 if isVisible x then
2987 [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)] 2999 [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)]
2988 else 3000 else
2989 [] 3001 []
2990 | L'.SgiStr (x, n, sgn) => 3002 | L'.SgiStr (_, x, n, sgn) =>
2991 if isVisible x then 3003 if isVisible x then
2992 [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)] 3004 [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)]
2993 else 3005 else
2994 [] 3006 []
2995 | L'.SgiSgn (x, n, sgn) => 3007 | L'.SgiSgn (x, n, sgn) =>
3031 | L'.DDatatype x => [(L'.SgiDatatype x, loc)] 3043 | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
3032 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)] 3044 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
3033 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] 3045 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
3034 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis 3046 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
3035 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] 3047 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
3036 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 3048 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (L'.Import, x, n, sgn), loc)]
3037 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 3049 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (L'.Import, x, n, sgn), loc)]
3038 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 3050 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
3039 | L'.DExport _ => [] 3051 | L'.DExport _ => []
3040 | L'.DTable (tn, x, n, c, _, pc, _, cc) => 3052 | L'.DTable (tn, x, n, c, _, pc, _, cc) =>
3041 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), 3053 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc),
3042 (L'.CConcat (pc, cc), loc)), loc)), loc)] 3054 (L'.CConcat (pc, cc), loc)), loc)), loc)]
3342 SOME env) 3354 SOME env)
3343 else 3355 else
3344 NONE 3356 NONE
3345 | _ => NONE) 3357 | _ => NONE)
3346 3358
3347 | L'.SgiStr (x, n2, sgn2) => 3359 | L'.SgiStr (_, x, n2, sgn2) =>
3348 seek (fn (env, sgi1All as (sgi1, loc)) => 3360 seek (fn (env, sgi1All as (sgi1, loc)) =>
3349 case sgi1 of 3361 case sgi1 of
3350 L'.SgiStr (x', n1, sgn1) => 3362 L'.SgiStr (_, x', n1, sgn1) =>
3351 if x = x' then 3363 if x = x' then
3352 let 3364 let
3353 (* Don't forget to save & restore the 3365 (* Don't forget to save & restore the
3354 * counterparts map around recursive calls! 3366 * counterparts map around recursive calls!
3355 * Otherwise, all sorts of mayhem may result. *) 3367 * Otherwise, all sorts of mayhem may result. *)
3747 if should t then 3759 if should t then
3748 naddVal (nd, x) 3760 naddVal (nd, x)
3749 else 3761 else
3750 nd 3762 nd
3751 end 3763 end
3752 | L'.SgiStr (x, _, s) => 3764 | L'.SgiStr (_, x, _, s) =>
3753 (case #1 (hnormSgn env' s) of 3765 (case #1 (hnormSgn env' s) of
3754 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis')) 3766 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis'))
3755 | _ => nd) 3767 | _ => nd)
3756 | _ => nd, 3768 | _ => nd,
3757 E.sgiBinds env' (sgi, loc))) 3769 E.sgiBinds env' (sgi, loc)))
4494 (SS.add (sgns, x), x) 4506 (SS.add (sgns, x), x)
4495 in 4507 in
4496 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) 4508 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
4497 end 4509 end
4498 4510
4499 | L'.SgiStr (x, n, sgn) => 4511 | L'.SgiStr (im, x, n, sgn) =>
4500 let 4512 let
4501 val (strs, x) = 4513 val (strs, x) =
4502 if SS.member (strs, x) then 4514 if SS.member (strs, x) then
4503 (strs, "?" ^ x) 4515 (strs, "?" ^ x)
4504 else 4516 else
4505 (SS.add (strs, x), x) 4517 (SS.add (strs, x), x)
4506 in 4518 in
4507 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) 4519 ((L'.SgiStr (im, x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
4508 end 4520 end
4509 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) 4521 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
4510 | L'.SgiClassAbs (x, n, k) => 4522 | L'.SgiClassAbs (x, n, k) =>
4511 let 4523 let
4512 val (cons, x) = 4524 val (cons, x) =
4608 * arbitarily many question marks before the module name to 4620 * arbitarily many question marks before the module name to
4609 * avoid a clash, since some other code might depend on 4621 * avoid a clash, since some other code might depend on
4610 * question-mark identifiers generated previously by this 4622 * question-mark identifiers generated previously by this
4611 * very code fragment. *) 4623 * very code fragment. *)
4612 fun mungeName m = 4624 fun mungeName m =
4613 if List.exists (fn (L'.SgiStr (x, _, _), _) => x = m 4625 if List.exists (fn (L'.SgiStr (_, x, _, _), _) => x = m
4614 | _ => false) sgis then 4626 | _ => false) sgis then
4615 mungeName ("?" ^ m) 4627 mungeName ("?" ^ m)
4616 else 4628 else
4617 m 4629 m
4618 4630
4619 val m = mungeName m 4631 val m = mungeName m
4620 in 4632 in
4621 ((L'.StrApp (str1', str2'), loc), 4633 ((L'.StrApp (str1', str2'), loc),
4622 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), 4634 (L'.SgnConst ((L'.SgiStr (L'.Skip, m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
4623 gs1 @ gs2) 4635 gs1 @ gs2)
4624 end 4636 end
4625 | _ => raise Fail "Unable to hnormSgn in functor application") 4637 | _ => raise Fail "Unable to hnormSgn in functor application")
4626 | _ => (strError env (NotFunctor sgn1); 4638 | _ => (strError env (NotFunctor sgn1);
4627 (strerror, sgnerror, [])) 4639 (strerror, sgnerror, []))
4999 ModDb.revert () 5011 ModDb.revert ()
5000 else 5012 else
5001 (); 5013 ();
5002 5014
5003 (*Print.preface("File", ElabPrint.p_file env file);*) 5015 (*Print.preface("File", ElabPrint.p_file env file);*)
5004 5016
5005 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) 5017 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
5006 :: ds 5018 :: ds
5007 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) 5019 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
5008 :: ds' @ file 5020 :: ds' @ file
5009 end 5021 end