summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/disjoint.sml2
-rw-r--r--src/elab.sml6
-rw-r--r--src/elab_print.sml18
-rw-r--r--src/elab_util.sml4
-rw-r--r--src/elaborate.sml23
-rw-r--r--src/explify.sml2
-rw-r--r--src/mono_opt.sml8
7 files changed, 45 insertions, 18 deletions
diff --git a/src/disjoint.sml b/src/disjoint.sml
index 5602c8d2..8dff81e7 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -314,7 +314,7 @@ and hnormCon (env, denv) c =
in
case c of
CDisjoint cs => doDisj cs
- | TDisjoint cs => doDisj cs
+ | TDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
| _ => (cAll, [])
end
diff --git a/src/elab.sml b/src/elab.sml
index 8e77d773..6fcb857a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -46,10 +46,14 @@ datatype explicitness =
Explicit
| Implicit
+datatype auto_instantiate =
+ Instantiate
+ | LeaveAlone
+
datatype con' =
TFun of con * con
| TCFun of explicitness * string * kind * con
- | TDisjoint of con * con * con
+ | TDisjoint of auto_instantiate * con * con * con
| TRecord of con
| CRel of int
diff --git a/src/elab_print.sml b/src/elab_print.sml
index f56f57dc..bb1c2a85 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -80,15 +80,15 @@ fun p_con' par env (c, _) =
string "->",
space,
p_con (E.pushCRel env x k) c])
- | TDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
- space,
- string "~",
- space,
- p_con env c2,
- space,
- string "->",
- space,
- p_con env c3])
+ | TDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
+ space,
+ string "~",
+ space,
+ p_con env c2,
+ space,
+ string "->",
+ space,
+ p_con env c3])
| TRecord (CRecord (_, xcs), _) => box [string "{",
p_list (fn (x, c) =>
box [p_name env x,
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 6f56d9c9..242ffdbc 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -119,14 +119,14 @@ fun mapfoldB {kind = fk, con = fc, bind} =
S.map2 (mfc (bind (ctx, Rel (x, k))) c,
fn c' =>
(TCFun (e, x, k', c'), loc)))
- | TDisjoint (c1, c2, c3) =>
+ | TDisjoint (ai, c1, c2, c3) =>
S.bind2 (mfc ctx c1,
fn c1' =>
S.bind2 (mfc ctx c2,
fn c2' =>
S.map2 (mfc ctx c3,
fn c3' =>
- (TDisjoint (c1', c2', c3'), loc))))
+ (TDisjoint (ai, c1', c2', c3'), loc))))
| TRecord c =>
S.map2 (mfc ctx c,
fn c' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2b548969..e6e5453d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -239,7 +239,7 @@ fun elabCon (env, denv) (c, loc) =
checkKind env c1' k1 (L'.KRecord ku1, loc);
checkKind env c2' k2 (L'.KRecord ku2, loc);
- ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
+ ((L'.TDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
end
| L.TRecord c =>
let
@@ -824,7 +824,7 @@ and guessFold (env, denv) (c1, c2, gs, ex) =
and unifyCons' (env, denv) c1 c2 =
case (#1 c1, #1 c2) of
- (L'.TDisjoint (x1, y1, t1), L'.TDisjoint (x2, y2, t2)) =>
+ (L'.TDisjoint (_, x1, y1, t1), L'.TDisjoint (_, x2, y2, t2)) =>
let
val gs1 = unifyCons' (env, denv) x1 x2
val gs2 = unifyCons' (env, denv) y1 y2
@@ -983,7 +983,8 @@ fun foldType (dom, loc) =
(L'.TCFun (L'.Explicit, "v", dom,
(L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
(L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
- (L'.TDisjoint ((L'.CRecord
+ (L'.TDisjoint (L'.Instantiate,
+ (L'.CRecord
((L'.KUnit, loc),
[((L'.CRel 2, loc),
(L'.CUnit, loc))]), loc),
@@ -1523,7 +1524,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
checkKind env c1' k1 (L'.KRecord ku1, loc);
checkKind env c2' k2 (L'.KRecord ku2, loc);
- (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
+ (e', (L'.TDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
end
| L.ERecord xes =>
@@ -2661,6 +2662,17 @@ fun wildifyStr env (str, sgn) =
| _ => str)
| _ => str
+val makeInstantiable =
+ let
+ fun kind k = k
+ fun con c =
+ case c of
+ L'.TDisjoint (L'.LeaveAlone, c1, c2, c) => L'.TDisjoint (L'.Instantiate, c1, c2, c)
+ | _ => c
+ in
+ U.Con.map {kind = kind, con = con}
+ end
+
fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
let
(*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
@@ -2792,6 +2804,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
val gs3 = checkCon (env, denv) e' et c'
val (c', gs4) = normClassConstraint (env, denv) c'
val (env', n) = E.pushENamed env x c'
+ val c' = makeInstantiable c'
in
(*prefaces "DVal" [("x", Print.PD.string x),
("c'", p_con env c')];*)
@@ -2828,6 +2841,8 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
val (e', et, gs1) = elabExp (env, denv) e
val gs2 = checkCon (env, denv) e' et c'
+
+ val c' = makeInstantiable c'
in
if allowable e then
()
diff --git a/src/explify.sml b/src/explify.sml
index 142ddfcb..76ef9551 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -49,7 +49,7 @@ fun explifyCon (c, loc) =
case c of
L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
| L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc)
- | L.TDisjoint (_, _, c) => explifyCon c
+ | L.TDisjoint (_, _, _, c) => explifyCon c
| L.TRecord c => (L'.TRecord (explifyCon c), loc)
| L.CRel n => (L'.CRel n, loc)
diff --git a/src/mono_opt.sml b/src/mono_opt.sml
index 64eef7e3..997bb9be 100644
--- a/src/mono_opt.sml
+++ b/src/mono_opt.sml
@@ -293,6 +293,14 @@ fun exp e =
else
e
+ | EWrite (EQuery {exps, tables, state, query,
+ initial = (EPrim (Prim.String ""), _),
+ body = (EStrcat ((ERel 0, _), e'), _)}, loc) =>
+ EQuery {exps = exps, tables = tables, query = query,
+ state = (TRecord [], loc),
+ initial = (ERecord [], loc),
+ body = (optExp (EWrite e', loc), loc)}
+
| _ => e
and optExp e = #1 (U.Exp.map {typ = typ, exp = exp} e)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-14 09:41:28 +0000