Mercurial > urweb
changeset 792:d20d6afc1206
Improvements while working on Graftid
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 12 May 2009 18:02:25 -0400 |
| parents | 5368deb3764b |
| children | 3e5d1c6ae30c |
| files | src/c/urweb.c src/compiler.sml src/elab_err.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/list_util.sig src/list_util.sml src/specialize.sml |
| diffstat | 9 files changed, 102 insertions(+), 58 deletions(-) [+] |
line wrap: on
line diff
--- a/src/c/urweb.c Sun May 10 10:13:41 2009 -0400 +++ b/src/c/urweb.c Tue May 12 18:02:25 2009 -0400 @@ -2289,6 +2289,8 @@ return NULL; } } + + return NULL; } uw_unit uw_Basis_set_cookie(uw_context ctx, uw_Basis_string prefix, uw_Basis_string c, uw_Basis_string v) {
--- a/src/compiler.sml Sun May 10 10:13:41 2009 -0400 +++ b/src/compiler.sml Tue May 12 18:02:25 2009 -0400 @@ -380,7 +380,7 @@ rewrites = #rewrites old @ #rewrites new, filterUrl = #filterUrl old @ #filterUrl new, filterMime = #filterMime old @ #filterMime new, - sources = #sources old @ #sources new + sources = #sources new @ #sources old } in foldr (fn (fname, job) => merge (job, parseUrp' fname)) job (!libs)
--- a/src/elab_err.sml Sun May 10 10:13:41 2009 -0400 +++ b/src/elab_err.sml Tue May 12 18:02:25 2009 -0400 @@ -47,7 +47,7 @@ #1 c' end, bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k - | (env, U.Con.NamedC (x, n, k)) => E.pushCNamedAs env x n k NONE + | (env, U.Con.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co | (env, _) => env} val p_kind = P.p_kind
--- a/src/elab_util.sig Sun May 10 10:13:41 2009 -0400 +++ b/src/elab_util.sig Tue May 12 18:02:25 2009 -0400 @@ -45,7 +45,7 @@ datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, @@ -79,7 +79,7 @@ datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con @@ -112,9 +112,9 @@ datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind - | Str of string * Elab.sgn - | Sgn of string * Elab.sgn + | NamedC of string * int * Elab.kind * Elab.con option + | Str of string * int * Elab.sgn + | Sgn of string * int * Elab.sgn val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, @@ -136,13 +136,20 @@ sgn : Elab.sgn' -> Elab.sgn'} -> Elab.sgn -> Elab.sgn + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', + con : 'context -> Elab.con' -> Elab.con', + sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item', + sgn : 'context -> Elab.sgn' -> Elab.sgn', + bind : 'context * binder -> 'context} + -> 'context -> Elab.sgn -> Elab.sgn + end structure Decl : sig datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con | Str of string * Elab.sgn
--- a/src/elab_util.sml Sun May 10 10:13:41 2009 -0400 +++ b/src/elab_util.sml Tue May 12 18:02:25 2009 -0400 @@ -113,7 +113,7 @@ datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option fun mapfoldB {kind = fk, con = fc, bind} = let @@ -287,7 +287,7 @@ datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con @@ -534,9 +534,9 @@ datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind - | Str of string * Elab.sgn - | Sgn of string * Elab.sgn + | NamedC of string * int * Elab.kind * Elab.con option + | Str of string * int * Elab.sgn + | Sgn of string * int * Elab.sgn fun mapfoldB {kind, con, sgn_item, sgn, bind} = let @@ -624,23 +624,24 @@ S.map2 (ListUtil.mapfoldB (fn (ctx, si) => (case #1 si of SgiConAbs (x, n, k) => - bind (ctx, NamedC (x, n, k)) - | SgiCon (x, n, k, _) => - bind (ctx, NamedC (x, n, k)) + bind (ctx, NamedC (x, n, k, NONE)) + | SgiCon (x, n, k, c) => + bind (ctx, NamedC (x, n, k, SOME c)) | SgiDatatype (x, n, _, xncs) => - bind (ctx, NamedC (x, n, (KType, loc))) - | SgiDatatypeImp (x, n, _, _, _, _, _) => - bind (ctx, NamedC (x, n, (KType, loc))) + bind (ctx, NamedC (x, n, (KType, loc), NONE)) + | SgiDatatypeImp (x, n, m1, ms, s, _, _) => + bind (ctx, NamedC (x, n, (KType, loc), + SOME (CModProj (m1, ms, s), loc))) | SgiVal _ => ctx - | SgiStr (x, _, sgn) => - bind (ctx, Str (x, sgn)) - | SgiSgn (x, _, sgn) => - bind (ctx, Sgn (x, sgn)) + | SgiStr (x, n, sgn) => + bind (ctx, Str (x, n, sgn)) + | SgiSgn (x, n, sgn) => + bind (ctx, Sgn (x, n, sgn)) | SgiConstraint _ => ctx | SgiClassAbs (x, n, k) => - bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))) - | SgiClass (x, n, k, _) => - bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))), + bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), NONE)) + | SgiClass (x, n, k, c) => + bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c)), sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -649,7 +650,7 @@ | SgnFun (m, n, s1, s2) => S.bind2 (sg ctx s1, fn s1' => - S.map2 (sg (bind (ctx, Str (m, s1'))) s2, + S.map2 (sg (bind (ctx, Str (m, n, s1'))) s2, fn s2' => (SgnFun (m, n, s1', s2'), loc))) | SgnProj _ => S.return2 sAll @@ -671,6 +672,15 @@ sgn = fn () => sgn, bind = fn ((), _) => ()} () +fun mapB {kind, con, sgn_item, sgn, bind} ctx s = + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), + con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), + sgn_item = fn ctx => fn sgi => fn () => S.Continue (sgn_item ctx sgi, ()), + sgn = fn ctx => fn s => fn () => S.Continue (sgn ctx s, ()), + bind = bind} ctx s () of + S.Continue (s, ()) => s + | S.Return _ => raise Fail "ElabUtil.Sgn.mapB: Impossible" + fun map {kind, con, sgn_item, sgn} s = case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), con = fn c => fn () => S.Continue (con c, ()), @@ -686,7 +696,7 @@ datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con | Str of string * Elab.sgn @@ -726,8 +736,8 @@ Sgn.RelK x => RelK x | Sgn.RelC x => RelC x | Sgn.NamedC x => NamedC x - | Sgn.Sgn x => Sgn x - | Sgn.Str x => Str x + | Sgn.Sgn (x, _, y) => Sgn (x, y) + | Sgn.Str (x, _, y) => Str (x, y) in bind (ctx, b') end @@ -741,11 +751,11 @@ StrConst ds => S.map2 (ListUtil.mapfoldB (fn (ctx, d) => (case #1 d of - DCon (x, n, k, _) => - bind (ctx, NamedC (x, n, k)) + DCon (x, n, k, c) => + bind (ctx, NamedC (x, n, k, SOME c)) | DDatatype (x, n, xs, xncs) => let - val ctx = bind (ctx, NamedC (x, n, (KType, loc))) + val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE)) in foldl (fn ((x, _, co), ctx) => let @@ -768,7 +778,8 @@ ctx xncs end | DDatatypeImp (x, n, m, ms, x', _, _) => - bind (ctx, NamedC (x, n, (KType, loc))) + bind (ctx, NamedC (x, n, (KType, loc), + SOME (CModProj (m, ms, x'), loc))) | DVal (x, _, c, _) => bind (ctx, NamedE (x, c)) | DValRec vis => @@ -798,8 +809,8 @@ in bind (ctx, NamedE (x, ct)) end - | DClass (x, n, k, _) => - bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))) + | DClass (x, n, k, c) => + bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c)) | DDatabase _ => ctx | DCookie (tn, x, n, c) => bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
--- a/src/elaborate.sml Sun May 10 10:13:41 2009 -0400 +++ b/src/elaborate.sml Tue May 12 18:02:25 2009 -0400 @@ -1171,7 +1171,7 @@ | (L'.TDisjoint (r1, r2, t'), loc) => if infer <> L.TypesOnly then let - val gs = D.prove env denv (r1, r2, loc) + val gs = D.prove env denv (r1, r2, #2 e) val (e, t, gs') = unravel (t', e) in (e, t, enD gs @ gs')
--- a/src/list_util.sig Sun May 10 10:13:41 2009 -0400 +++ b/src/list_util.sig Tue May 12 18:02:25 2009 -0400 @@ -46,4 +46,8 @@ val foldliMap : (int * 'data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state + val appi : (int * 'a -> unit) -> 'a list -> unit + + val appn : (int -> unit) -> int -> unit + end
--- a/src/list_util.sml Sun May 10 10:13:41 2009 -0400 +++ b/src/list_util.sml Tue May 12 18:02:25 2009 -0400 @@ -146,6 +146,16 @@ m 0 [] end +fun appi f = + let + fun m i ls = + case ls of + [] => () + | h :: t => (f (i, h); m (i + 1) t) + in + m 0 + end + fun foldli f = let fun m i acc ls = @@ -178,4 +188,16 @@ fm (0, [], s) end +fun appn f n = + let + fun iter m = + if m >= n then + () + else + (f m; + iter (m + 1)) + in + iter 0 + end + end
--- a/src/specialize.sml Sun May 10 10:13:41 2009 -0400 +++ b/src/specialize.sml Tue May 12 18:02:25 2009 -0400 @@ -242,32 +242,30 @@ fun specialize file = let - fun doDecl (all as (d, _), st : state) = + fun doDecl (d, st) = let (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*) + val (d, st) = specDecl st d in - case d of + case #1 d of DDatatype (x, n, xs, xnts) => - ([all], {count = #count st, - datatypes = IM.insert (#datatypes st, n, - {name = x, - params = length xs, - constructors = xnts, - specializations = CM.empty}), - constructors = foldl (fn ((_, n', _), constructors) => - IM.insert (constructors, n', n)) - (#constructors st) xnts, - decls = []}) + (rev (d :: #decls st), + {count = #count st, + datatypes = IM.insert (#datatypes st, n, + {name = x, + params = length xs, + constructors = xnts, + specializations = CM.empty}), + constructors = foldl (fn ((_, n', _), constructors) => + IM.insert (constructors, n', n)) + (#constructors st) xnts, + decls = []}) | _ => - let - val (d, st) = specDecl st all - in - (rev (d :: #decls st), - {count = #count st, - datatypes = #datatypes st, - constructors = #constructors st, - decls = []}) - end + (rev (d :: #decls st), + {count = #count st, + datatypes = #datatypes st, + constructors = #constructors st, + decls = []}) end val (ds, _) = ListUtil.foldlMapConcat doDecl