Mercurial > urweb

comparison src/elaborate.sml @ 1732:4a03aa3251cb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial support for reusing elaboration results
author Adam Chlipala <adam@chlipala.net>
date Sun, 29 Apr 2012 13:17:31 -0400
parents 5ecf67553da8
children ab24a7cb2a64
comparison
equal deleted inserted replaced
1731:27e731a65934 1732:4a03aa3251cb
3639 case d of 3639 case d of
3640 L.DCon (x, _, _) => ndelCon (nd, x) 3640 L.DCon (x, _, _) => ndelCon (nd, x)
3641 | L.DClass (x, _, _) => ndelCon (nd, x) 3641 | L.DClass (x, _, _) => ndelCon (nd, x)
3642 | L.DVal (x, _, _) => ndelVal (nd, x) 3642 | L.DVal (x, _, _) => ndelVal (nd, x)
3643 | L.DOpen _ => nempty 3643 | L.DOpen _ => nempty
3644 | L.DStr (x, _, (L.StrConst ds', _)) => 3644 | L.DStr (x, _, _, (L.StrConst ds', _)) =>
3645 (case SM.find (nmods nd, x) of 3645 (case SM.find (nmods nd, x) of
3646 NONE => nd 3646 NONE => nd
3647 | SOME (env, nd') => naddMod (nd, x, (env, removeUsed (nd', ds')))) 3647 | SOME (env, nd') => naddMod (nd, x, (env, removeUsed (nd', ds'))))
3648 | _ => nd) 3648 | _ => nd)
3649 nd ds 3649 nd ds
3709 (L.DCon (x, NONE, cwild), #2 str) 3709 (L.DCon (x, NONE, cwild), #2 str)
3710 end) xs @ ds' 3710 end) xs @ ds'
3711 3711
3712 val ds = ds @ ds' 3712 val ds = ds @ ds'
3713 in 3713 in
3714 map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) => 3714 map (fn d as (L.DStr (x, s, tm, (L.StrConst ds', loc')), loc) =>
3715 (case SM.find (nmods nd, x) of 3715 (case SM.find (nmods nd, x) of
3716 NONE => d 3716 NONE => d
3717 | SOME (env, nd') => 3717 | SOME (env, nd') =>
3718 (L.DStr (x, s, (L.StrConst (extend (env, nd', ds')), loc')), loc)) 3718 (L.DStr (x, s, tm, (L.StrConst (extend (env, nd', ds')), loc')), loc))
3719 | d => d) ds 3719 | d => d) ds
3720 end 3720 end
3721 in 3721 in
3722 (L.StrConst (extend (env, nd, rev dPrefix) @ dSuffix), #2 str) 3722 (L.StrConst (extend (env, nd, rev dPrefix) @ dSuffix), #2 str)
3723 end 3723 end
3921 val (env', n) = E.pushSgnNamed env x sgn' 3921 val (env', n) = E.pushSgnNamed env x sgn'
3922 in 3922 in
3923 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) 3923 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
3924 end 3924 end
3925 3925
3926 | L.DStr (x, sgno, str) => 3926 | L.DStr (x, sgno, tmo, str) =>
3927 let 3927 (case ModDb.lookup dAll of
3928 val () = if x = "Basis" then 3928 SOME d =>
3929 raise Fail "Not allowed to redefine structure 'Basis'" 3929 let
3930 else 3930 val env' = E.declBinds env d
3931 () 3931 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []}
3932 3932 in
3933 val formal = Option.map (elabSgn (env, denv)) sgno 3933 ([d], (env', denv', []))
3934 3934 end
3935 val (str', sgn', gs') = 3935 | NONE =>
3936 case formal of 3936 let
3937 NONE => 3937 val () = if x = "Basis" then
3938 let 3938 raise Fail "Not allowed to redefine structure 'Basis'"
3939 val (str', actual, gs') = elabStr (env, denv) str 3939 else
3940 in 3940 ()
3941 (str', selfifyAt env {str = str', sgn = actual}, gs') 3941
3942 end 3942 val formal = Option.map (elabSgn (env, denv)) sgno
3943 | SOME (formal, gs1) => 3943
3944 let 3944 val (str', sgn', gs') =
3945 val str = wildifyStr env (str, formal) 3945 case formal of
3946 val (str', actual, gs2) = elabStr (env, denv) str 3946 NONE =>
3947 in 3947 let
3948 subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal; 3948 val (str', actual, gs') = elabStr (env, denv) str
3949 (str', formal, enD gs1 @ gs2) 3949 in
3950 end 3950 (str', selfifyAt env {str = str', sgn = actual}, gs')
3951 3951 end
3952 val (env', n) = E.pushStrNamed env x sgn' 3952 | SOME (formal, gs1) =>
3953 val denv' = 3953 let
3954 case #1 str' of 3954 val str = wildifyStr env (str, formal)
3955 L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []} 3955 val (str', actual, gs2) = elabStr (env, denv) str
3956 | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []} 3956 in
3957 | _ => denv 3957 subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal;
3958 in 3958 (str', formal, enD gs1 @ gs2)
3959 case #1 (hnormSgn env sgn') of 3959 end
3960 L'.SgnFun _ => 3960
3961 (case #1 str' of 3961 val (env', n) = E.pushStrNamed env x sgn'
3962 L'.StrFun _ => () 3962 val denv' =
3963 | _ => strError env (FunctorRebind loc)) 3963 case #1 str' of
3964 | _ => (); 3964 L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
3965 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv', gs' @ gs)) 3965 | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
3966 end 3966 | _ => denv
3967 3967
3968 | L.DFfiStr (x, sgn) => 3968 val dNew = (L'.DStr (x, n, sgn', str'), loc)
3969 let 3969 in
3970 val (sgn', gs') = elabSgn (env, denv) sgn 3970 case #1 (hnormSgn env sgn') of
3971 3971 L'.SgnFun _ =>
3972 val (env', n) = E.pushStrNamed env x sgn' 3972 (case #1 str' of
3973 in 3973 L'.StrFun _ => ()
3974 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) 3974 | _ => strError env (FunctorRebind loc))
3975 end 3975 | _ => ();
3976 Option.map (fn tm => ModDb.insert (dNew, tm)) tmo;
3977 ([dNew], (env', denv', gs' @ gs))
3978 end)
3979
3980 | L.DFfiStr (x, sgn, tm) =>
3981 (case ModDb.lookup dAll of
3982 SOME d =>
3983 let
3984 val env' = E.declBinds env d
3985 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []}
3986 in
3987 ([d], (env', denv', []))
3988 end
3989 | NONE =>
3990 let
3991 val (sgn', gs') = elabSgn (env, denv) sgn
3992
3993 val (env', n) = E.pushStrNamed env x sgn'
3994
3995 val dNew = (L'.DFfiStr (x, n, sgn'), loc)
3996 in
3997 ModDb.insert (dNew, tm);
3998 ([dNew], (env', denv, enD gs' @ gs))
3999 end)
3976 4000
3977 | L.DOpen (m, ms) => 4001 | L.DOpen (m, ms) =>
3978 (case E.lookupStr env m of 4002 (case E.lookupStr env m of
3979 NONE => (strError env (UnboundStr (loc, m)); 4003 NONE => (strError env (UnboundStr (loc, m));
3980 ([], (env, denv, gs))) 4004 ([], (env, denv, gs)))
4429 (strerror, sgnerror, [])) 4453 (strerror, sgnerror, []))
4430 end 4454 end
4431 4455
4432 fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env 4456 fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env
4433 4457
4434 fun elabFile basis topStr topSgn env file = 4458 fun elabFile basis basis_tm topStr topSgn top_tm env file =
4435 let 4459 let
4436 val () = mayDelay := true 4460 val () = mayDelay := true
4437 val () = delayedUnifs := [] 4461 val () = delayedUnifs := []
4438 val () = delayedExhaustives := [] 4462 val () = delayedExhaustives := []
4439 4463
4440 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) 4464 val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), basis_tm), ErrorMsg.dummySpan)
4441 val () = case gs of 4465 val (basis_n, env', sgn) =
4442 [] => () 4466 case ModDb.lookup d of
4443 | _ => (app (fn (_, env, _, c1, c2) => 4467 NONE =>
4444 prefaces "Unresolved" 4468 let
4445 [("c1", p_con env c1), 4469 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
4446 ("c2", p_con env c2)]) gs; 4470 val () = case gs of
4447 raise Fail "Unresolved disjointness constraints in Basis") 4471 [] => ()
4448 4472 | _ => (app (fn (_, env, _, c1, c2) =>
4449 val (env', basis_n) = E.pushStrNamed env "Basis" sgn 4473 prefaces "Unresolved"
4474 [("c1", p_con env c1),
4475 ("c2", p_con env c2)]) gs;
4476 raise Fail "Unresolved disjointness constraints in Basis")
4477
4478 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
4479 in
4480 ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm);
4481 (basis_n, env', sgn)
4482 end
4483 | SOME (d' as (L'.DFfiStr (_, basis_n, sgn), _)) =>
4484 (basis_n, E.pushStrNamedAs env "Basis" basis_n sgn, sgn)
4485 | _ => raise Fail "Elaborate: Basis impossible"
4486
4450 val () = basis_r := basis_n 4487 val () = basis_r := basis_n
4451
4452 val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn} 4488 val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn}
4453 4489
4454 fun discoverC r x = 4490 fun discoverC r x =
4455 case E.lookupC env' x of 4491 case E.lookupC env' x of
4456 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis") 4492 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
4461 val () = discoverC float "float" 4497 val () = discoverC float "float"
4462 val () = discoverC string "string" 4498 val () = discoverC string "string"
4463 val () = discoverC char "char" 4499 val () = discoverC char "char"
4464 val () = discoverC table "sql_table" 4500 val () = discoverC table "sql_table"
4465 4501
4466 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) 4502 val d = (L.DStr ("Top", SOME (L.SgnConst topSgn, ErrorMsg.dummySpan),
4467 val () = case gs of 4503 SOME (if Time.< (top_tm, basis_tm) then basis_tm else top_tm),
4468 [] => () 4504 (L.StrConst topStr, ErrorMsg.dummySpan)), ErrorMsg.dummySpan)
4469 | _ => raise Fail "Unresolved disjointness constraints in top.urs" 4505 val (top_n, env', topSgn, topStr) =
4470 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) 4506 case ModDb.lookup d of
4471 val () = case gs of 4507 NONE =>
4472 [] => () 4508 let
4473 | _ => app (fn Disjoint (loc, env, denv, c1, c2) => 4509 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan)
4474 (case D.prove env denv (c1, c2, loc) of 4510 val () = case gs of
4475 [] => () 4511 [] => ()
4476 | _ => 4512 | _ => raise Fail "Unresolved disjointness constraints in top.urs"
4477 (prefaces "Unresolved constraint in top.ur" 4513 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
4478 [("loc", PD.string (ErrorMsg.spanToString loc)), 4514
4479 ("c1", p_con env c1), 4515 val () = case gs of
4480 ("c2", p_con env c2)]; 4516 [] => ()
4481 raise Fail "Unresolved constraint in top.ur")) 4517 | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
4482 | TypeClass (env, c, r, loc) => 4518 (case D.prove env denv (c1, c2, loc) of
4483 let 4519 [] => ()
4484 val c = normClassKey env c 4520 | _ =>
4485 in 4521 (prefaces "Unresolved constraint in top.ur"
4486 case resolveClass env c of 4522 [("loc", PD.string (ErrorMsg.spanToString loc)),
4487 SOME e => r := SOME e 4523 ("c1", p_con env c1),
4488 | NONE => expError env (Unresolvable (loc, c)) 4524 ("c2", p_con env c2)];
4489 end) gs 4525 raise Fail "Unresolved constraint in top.ur"))
4490 4526 | TypeClass (env, c, r, loc) =>
4491 val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn 4527 let
4492 4528 val c = normClassKey env c
4493 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 4529 in
4530 case resolveClass env c of
4531 SOME e => r := SOME e
4532 | NONE => expError env (Unresolvable (loc, c))
4533 end) gs
4534
4535 val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn
4536
4537 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
4538 in
4539 ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm);
4540 (top_n, env', topSgn, topStr)
4541 end
4542 | SOME (d' as (L'.DStr (_, top_n, topSgn, topStr), _)) =>
4543 (top_n, E.declBinds env' d', topSgn, topStr)
4544 | _ => raise Fail "Elaborate: Top impossible"
4545
4494 val () = top_r := top_n 4546 val () = top_r := top_n
4495 4547
4496 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} 4548 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
4497 4549
4498 fun elabDecl' (d, (env, gs)) = 4550 fun elabDecl' (d, (env, gs)) =