Fiddly tweaks

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)