diff options
author | Adam Chlipala <adam@chlipala.net> | 2010-12-16 13:35:40 -0500 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2010-12-16 13:35:40 -0500 |
commit | 6aaa09dfff50fdd22aeef563de63a50926bb553f (patch) | |
tree | ed45e1d909672cac6d74d612f2c9531bb71681fa /src | |
parent | c7996285ff4b1b05a4cecdb2c1e944f7c17b18a7 (diff) |
Fiddly tweaks
Diffstat (limited to 'src')
-rw-r--r-- | src/elab_util.sig | 23 | ||||
-rw-r--r-- | src/elab_util.sml | 43 | ||||
-rw-r--r-- | src/elaborate.sml | 42 |
3 files changed, 71 insertions, 37 deletions
diff --git a/src/elab_util.sig b/src/elab_util.sig index dc0f25e8..88bdc892 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -157,8 +157,8 @@ structure Decl : sig | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con - | Str of string * Elab.sgn - | Sgn of string * Elab.sgn + | 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, @@ -203,6 +203,25 @@ structure Decl : sig decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state, bind : 'context * binder -> 'context} -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state + + val map : {kind : Elab.kind' -> Elab.kind', + con : Elab.con' -> Elab.con', + exp : Elab.exp' -> Elab.exp', + sgn_item : Elab.sgn_item' -> Elab.sgn_item', + sgn : Elab.sgn' -> Elab.sgn', + str : Elab.str' -> Elab.str', + decl : Elab.decl' -> Elab.decl'} + -> Elab.decl -> Elab.decl + + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', + con : 'context -> Elab.con' -> Elab.con', + exp : 'context -> Elab.exp' -> Elab.exp', + sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item', + sgn : 'context -> Elab.sgn' -> Elab.sgn', + str : 'context -> Elab.str' -> Elab.str', + decl : 'context -> Elab.decl' -> Elab.decl', + bind : 'context * binder -> 'context} + -> 'context -> Elab.decl -> Elab.decl end structure File : sig diff --git a/src/elab_util.sml b/src/elab_util.sml index d297ccbc..fd8163c2 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -771,8 +771,8 @@ datatype binder = | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con - | Str of string * Elab.sgn - | Sgn of string * Elab.sgn + | Str of string * int * Elab.sgn + | Sgn of string * int * Elab.sgn fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} = let @@ -808,8 +808,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, _, y) => Sgn (x, y) - | Sgn.Str (x, _, y) => Str (x, y) + | Sgn.Sgn x => Sgn x + | Sgn.Str x => Str x in bind (ctx, b') end @@ -861,12 +861,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f bind (ctx, NamedE (x, c)) | DValRec vis => foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis - | DSgn (x, _, sgn) => - bind (ctx, Sgn (x, sgn)) - | DStr (x, _, sgn, _) => - bind (ctx, Str (x, sgn)) - | DFfiStr (x, _, sgn) => - bind (ctx, Str (x, sgn)) + | DSgn (x, n, sgn) => + bind (ctx, Sgn (x, n, sgn)) + | DStr (x, n, sgn, _) => + bind (ctx, Str (x, n, sgn)) + | DFfiStr (x, n, sgn) => + bind (ctx, Str (x, n, sgn)) | DConstraint _ => ctx | DExport _ => ctx | DTable (tn, x, n, c, _, pc, _, cc) => @@ -1144,6 +1144,29 @@ fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d = S.Continue x => x | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible" +fun map {kind, con, exp, sgn_item, sgn, str, decl} s = + case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), + con = fn c => fn () => S.Continue (con c, ()), + exp = fn e => fn () => S.Continue (exp e, ()), + sgn_item = fn si => fn () => S.Continue (sgn_item si, ()), + sgn = fn s => fn () => S.Continue (sgn s, ()), + str = fn si => fn () => S.Continue (str si, ()), + decl = fn s => fn () => S.Continue (decl s, ())} s () of + S.Return () => raise Fail "Elab_util.Decl.map" + | S.Continue (s, ()) => s + +fun mapB {kind, con, exp, sgn_item, sgn, str, decl, 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, ()), + exp = fn ctx => fn c => fn () => S.Continue (exp 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, ()), + str = fn ctx => fn sgi => fn () => S.Continue (str ctx sgi, ()), + decl = fn ctx => fn s => fn () => S.Continue (decl ctx s, ()), + bind = bind} ctx s () of + S.Continue (s, ()) => s + | S.Return _ => raise Fail "ElabUtil.Decl.mapB: Impossible" + end structure File = struct diff --git a/src/elaborate.sml b/src/elaborate.sml index 3134c3d4..550e3b8f 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -4262,31 +4262,17 @@ fun elabFile basis topStr topSgn env file = val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} - val checks = ref ([] : (unit -> unit) list) - fun elabDecl' (d, (env, gs)) = let val () = resetKunif () val () = resetCunif () - val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs)) + val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs)) in - checks := - (fn () => - (if List.exists kunifsInDecl ds then - declError env (KunifsRemain ds) - else - (); - - case ListUtil.search cunifsInDecl ds of - NONE => () - | SOME loc => - declError env (CunifsRemain ds))) - :: !checks; - - (ds, (env, gs)) + (**) + (ds, (env', gs)) end - val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file + val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file fun oneSummaryRound () = if ErrorMsg.anyErrors () then @@ -4390,10 +4376,10 @@ fun elabFile basis topStr topSgn env file = ("Hnormed 1", p_con env c1'), ("Hnormed 2", p_con env c2')]; - app (fn (loc, env, k, s1, s2) => + (*app (fn (loc, env, k, s1, s2) => eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)), ("s2", p_summary env (normalizeRecordSummary env s2))]) - (!delayedUnifs); + (!delayedUnifs);*) if (isUnif c1' andalso maybeAttr c2') orelse (isUnif c2' andalso maybeAttr c1') then @@ -4422,10 +4408,16 @@ fun elabFile basis topStr topSgn env file = (!delayedUnifs); delayedUnifs := []); - if ErrorMsg.anyErrors () then - () - else - app (fn f => f ()) (!checks); + ignore (List.exists (fn d => if kunifsInDecl d then + (declError env'' (KunifsRemain [d]); + true) + else + false) file); + + ignore (List.exists (fn d => case cunifsInDecl d of + NONE => false + | SOME _ => (declError env'' (CunifsRemain [d]); + true)) file); if ErrorMsg.anyErrors () then () @@ -4437,7 +4429,7 @@ fun elabFile basis topStr topSgn env file = (!delayedExhaustives); (*preface ("file", p_file env' file);*) - + (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) |