Mercurial > urweb

comparison src/elaborate.sml @ 1733:ab24a7cb2a64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'urweb daemon start' and 'urweb daemon stop'
author Adam Chlipala <adam@chlipala.net>
date Sun, 29 Apr 2012 16:23:03 -0400
parents 4a03aa3251cb
children 7ec8dab190a7
comparison
equal deleted inserted replaced
1732:4a03aa3251cb 1733:ab24a7cb2a64
38 open ElabPrint 38 open ElabPrint
39 open ElabErr 39 open ElabErr
40 40
41 val dumpTypes = ref false 41 val dumpTypes = ref false
42 val unifyMore = ref false 42 val unifyMore = ref false
43 val incremental = ref false
43 44
44 structure IS = IntBinarySet 45 structure IS = IntBinarySet
45 structure IM = IntBinaryMap 46 structure IM = IntBinaryMap
46 47
47 structure SK = struct 48 structure SK = struct
3975 | _ => (); 3976 | _ => ();
3976 Option.map (fn tm => ModDb.insert (dNew, tm)) tmo; 3977 Option.map (fn tm => ModDb.insert (dNew, tm)) tmo;
3977 ([dNew], (env', denv', gs' @ gs)) 3978 ([dNew], (env', denv', gs' @ gs))
3978 end) 3979 end)
3979 3980
3980 | L.DFfiStr (x, sgn, tm) => 3981 | L.DFfiStr (x, sgn, tmo) =>
3981 (case ModDb.lookup dAll of 3982 (case ModDb.lookup dAll of
3982 SOME d => 3983 SOME d =>
3983 let 3984 let
3984 val env' = E.declBinds env d 3985 val env' = E.declBinds env d
3985 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} 3986 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []}
3992 3993
3993 val (env', n) = E.pushStrNamed env x sgn' 3994 val (env', n) = E.pushStrNamed env x sgn'
3994 3995
3995 val dNew = (L'.DFfiStr (x, n, sgn'), loc) 3996 val dNew = (L'.DFfiStr (x, n, sgn'), loc)
3996 in 3997 in
3997 ModDb.insert (dNew, tm); 3998 Option.map (fn tm => ModDb.insert (dNew, tm)) tmo;
3998 ([dNew], (env', denv, enD gs' @ gs)) 3999 ([dNew], (env', denv, enD gs' @ gs))
3999 end) 4000 end)
4000 4001
4001 | L.DOpen (m, ms) => 4002 | L.DOpen (m, ms) =>
4002 (case E.lookupStr env m of 4003 (case E.lookupStr env m of
4459 let 4460 let
4460 val () = mayDelay := true 4461 val () = mayDelay := true
4461 val () = delayedUnifs := [] 4462 val () = delayedUnifs := []
4462 val () = delayedExhaustives := [] 4463 val () = delayedExhaustives := []
4463 4464
4464 val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), basis_tm), ErrorMsg.dummySpan) 4465 val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), SOME basis_tm), ErrorMsg.dummySpan)
4465 val (basis_n, env', sgn) = 4466 val (basis_n, env', sgn) =
4466 case ModDb.lookup d of 4467 case (if !incremental then ModDb.lookup d else NONE) of
4467 NONE => 4468 NONE =>
4468 let 4469 let
4469 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) 4470 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
4470 val () = case gs of 4471 val () = case gs of
4471 [] => () 4472 [] => ()
4501 4502
4502 val d = (L.DStr ("Top", SOME (L.SgnConst topSgn, ErrorMsg.dummySpan), 4503 val d = (L.DStr ("Top", SOME (L.SgnConst topSgn, ErrorMsg.dummySpan),
4503 SOME (if Time.< (top_tm, basis_tm) then basis_tm else top_tm), 4504 SOME (if Time.< (top_tm, basis_tm) then basis_tm else top_tm),
4504 (L.StrConst topStr, ErrorMsg.dummySpan)), ErrorMsg.dummySpan) 4505 (L.StrConst topStr, ErrorMsg.dummySpan)), ErrorMsg.dummySpan)
4505 val (top_n, env', topSgn, topStr) = 4506 val (top_n, env', topSgn, topStr) =
4506 case ModDb.lookup d of 4507 case (if !incremental then ModDb.lookup d else NONE) of
4507 NONE => 4508 NONE =>
4508 let 4509 let
4509 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) 4510 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan)
4510 val () = case gs of 4511 val () = case gs of
4511 [] => () 4512 [] => ()