summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/c/urweb.c2
-rw-r--r--src/compiler.sml2
-rw-r--r--src/elab_err.sml2
-rw-r--r--src/elab_util.sig19
-rw-r--r--src/elab_util.sml67
-rw-r--r--src/elaborate.sml2
-rw-r--r--src/list_util.sig4
-rw-r--r--src/list_util.sml22
-rw-r--r--src/specialize.sml40
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 18:44:52 +0000