From b0eb28d7ea4eb75efce79ab7493b9e21842b80b4 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 12 May 2009 18:02:25 -0400 Subject: Improvements while working on Graftid --- src/c/urweb.c | 2 ++ src/compiler.sml | 2 +- src/elab_err.sml | 2 +- src/elab_util.sig | 19 +++++++++++----- src/elab_util.sml | 67 +++++++++++++++++++++++++++++++----------------------- src/elaborate.sml | 2 +- src/list_util.sig | 4 ++++ src/list_util.sml | 22 ++++++++++++++++++ src/specialize.sml | 40 ++++++++++++++++---------------- 9 files changed, 102 insertions(+), 58 deletions(-) diff --git a/src/c/urweb.c b/src/c/urweb.c index 75d42a6c..2ddc273a 100644 --- a/src/c/urweb.c +++ b/src/c/urweb.c @@ -2289,6 +2289,8 @@ uw_Basis_string uw_Basis_get_cookie(uw_context ctx, uw_Basis_string c) { 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) { diff --git a/src/compiler.sml b/src/compiler.sml index 66e8eda2..f47812ed 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -380,7 +380,7 @@ fun parseUrp' filename = 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) diff --git a/src/elab_err.sml b/src/elab_err.sml index ee8e1fd0..9eafa7df 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -47,7 +47,7 @@ val simplCon = U.Con.mapB {kind = fn _ => fn k => k, #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 diff --git a/src/elab_util.sig b/src/elab_util.sig index 5b4bc46a..fbe208ad 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -45,7 +45,7 @@ structure Con : 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 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, @@ -79,7 +79,7 @@ structure Exp : 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 @@ -112,9 +112,9 @@ structure Sgn : sig 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 @@ structure Sgn : sig 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 diff --git a/src/elab_util.sml b/src/elab_util.sml index f4cbc951..51a203f2 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -113,7 +113,7 @@ structure Con = struct 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 @@ structure Exp = struct 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 @@ structure Sgn = struct 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = | 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 @@ fun mapfold {kind, con, sgn_item, sgn} = 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 @@ structure Decl = struct 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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), diff --git a/src/elaborate.sml b/src/elaborate.sml index 38696976..36706b46 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -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') diff --git a/src/list_util.sig b/src/list_util.sig index 26ec72c1..11af6826 100644 --- a/src/list_util.sig +++ b/src/list_util.sig @@ -46,4 +46,8 @@ signature LIST_UTIL = sig 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 diff --git a/src/list_util.sml b/src/list_util.sml index 235a9654..a2b6aeb2 100644 --- a/src/list_util.sml +++ b/src/list_util.sml @@ -146,6 +146,16 @@ fun mapi f = 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 @@ fun foldliMap f s = 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 diff --git a/src/specialize.sml b/src/specialize.sml index ddaff92e..03c9004a 100644 --- a/src/specialize.sml +++ b/src/specialize.sml @@ -242,32 +242,30 @@ val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} 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 -- cgit v1.2.3