Improvements while working on Graftid

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