aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/corify.sml2
-rw-r--r--src/elab_print.sml22
-rw-r--r--src/elaborate.sml112
-rw-r--r--tests/gform.lac13
4 files changed, 26 insertions, 123 deletions
diff --git a/src/corify.sml b/src/corify.sml
index 0b0e9787..30b4a7df 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -488,7 +488,7 @@ fun corifyDecl ((d, loc : EM.span), st) =
case sgi of
L.SgiVal (s, _, t as (L.TFun (dom, ran), _)) =>
(case (#1 dom, #1 ran) of
- (L.TRecord _,
+ (L.TRecord (L.CRecord (_, []), _),
L.CApp
((L.CApp
((L.CApp ((L.CModProj (_, [], "xml"), _),
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 1da98c7a..81cbae69 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -125,17 +125,17 @@ fun p_con' par env (c, _) =
| CApp (c1, c2) => parenIf par (box [p_con env c1,
space,
p_con' true env c2])
- | CAbs (x, k, c) => parenIf par (box [string "fn",
- space,
- string x,
- space,
- string "::",
- space,
- p_kind k,
- space,
- string "=>",
- space,
- p_con (E.pushCRel env x k) c])
+ | CAbs (x, k, c) => parenIf true (box [string "fn",
+ space,
+ string x,
+ space,
+ string "::",
+ space,
+ p_kind k,
+ space,
+ string "=>",
+ space,
+ p_con (E.pushCRel env x k) c])
| CDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
space,
string "~",
diff --git a/src/elaborate.sml b/src/elaborate.sml
index b5794ecd..b48a69f6 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -469,7 +469,7 @@ fun cunifyError env err =
[("Con 1", p_con env c1),
("Con 2", p_con env c2)]
| CKindof (k, c) =>
- eprefaces "Kind unification variable blocks kindof calculation"
+ eprefaces "Unexpected kind for kindof calculation"
[("Kind", p_kind k),
("Con", p_con env c)]
| CRecordFailure =>
@@ -550,7 +550,7 @@ val hnormCon = D.hnormCon
fun unifyRecordCons (env, denv) (c1, c2) =
let
fun rkindof c =
- case kindof env c of
+ case hnormKind (kindof env c) of
(L'.KRecord k, _) => k
| (L'.KError, _) => kerror
| k => raise CUnify' (CKindof (k, c))
@@ -873,7 +873,7 @@ fun typeof env (e, loc) =
val (_, sgn) = E.lookupStrNamed env n
val (str, sgn) = foldl (fn (m, (str, sgn)) =>
case E.projectStr env {sgn = sgn, str = str, field = m} of
- NONE => raise Fail "kindof: Unknown substructure"
+ NONE => raise Fail "typeof: Unknown substructure"
| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
((L'.StrVar n, loc), sgn) ms
in
@@ -966,112 +966,6 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((L'.EModProj (n, ms, s), loc), t, [])
end)
- (*| L.EApp (arg as ((L.EApp ((L.ECApp ((L.EVar (["Basis"], "join"), _), (L.CWild _, _)), _), xml1), _), xml2)) =>
- let
- val (xml1', t1, gs1) = elabExp (env, denv) xml1
- val (xml2', t2, gs2) = elabExp (env, denv) xml2
-
- val kunit = (L'.KUnit, loc)
- val k = (L'.KRecord kunit, loc)
- val kt = (L'.KRecord (L'.KType, loc), loc)
-
- val basis =
- case E.lookupStr env "Basis" of
- NONE => raise Fail "elabExp: Unbound Basis"
- | SOME (n, _) => n
-
- fun xml () =
- let
- val ns = cunif (loc, k)
- val use = cunif (loc, kt)
- val bind = cunif (loc, kt)
-
- val t = (L'.CModProj (basis, [], "xml"), loc)
- val t = (L'.CApp (t, ns), loc)
- val t = (L'.CApp (t, use), loc)
- val t = (L'.CApp (t, bind), loc)
- in
- (ns, use, bind, t)
- end
-
- val (ns1, use1, bind1, c1) = xml ()
- val (ns2, use2, bind2, c2) = xml ()
-
- val gs3 = checkCon (env, denv) xml1' t1 c1
- val gs4 = checkCon (env, denv) xml2' t2 c2
-
- val (ns1, gs5) = hnormCon (env, denv) ns1
- val (ns2, gs6) = hnormCon (env, denv) ns2
-
- val cemp = (L'.CRecord (kunit, []), loc)
-
- val (shared, ctx1, ctx2) =
- case (#1 ns1, #1 ns2) of
- (L'.CRecord (_, ns1), L'.CRecord (_, ns2)) =>
- let
- val ns = List.filter (fn ((nm, _), _) =>
- case nm of
- L'.CName s =>
- List.exists (fn ((L'.CName s', _), _) => s' = s
- | _ => false) ns2
- | _ => false) ns1
- in
- ((L'.CRecord (kunit, ns), loc), cunif (loc, k), cunif (loc, k))
- end
- | (_, L'.CRecord _) => (ns2, cemp, cemp)
- | _ => (ns1, cemp, cemp)
-
- val ns1' = (L'.CConcat (shared, ctx1), loc)
- val ns2' = (L'.CConcat (shared, ctx2), loc)
-
- val e = (L'.EModProj (basis, [], "join"), loc)
- val e = (L'.ECApp (e, shared), loc)
- val e = (L'.ECApp (e, ctx1), loc)
- val e = (L'.ECApp (e, ctx2), loc)
- val e = (L'.ECApp (e, use1), loc)
- val e = (L'.ECApp (e, use2), loc)
- val e = (L'.ECApp (e, bind1), loc)
- val e = (L'.ECApp (e, bind2), loc)
- val e = (L'.EApp (e, xml1'), loc)
- val e = (L'.EApp (e, xml2'), loc)
-
- val t = (L'.CModProj (basis, [], "xml"), loc)
- val t = (L'.CApp (t, shared), loc)
- val t = (L'.CApp (t, (L'.CConcat (use1, use2), loc)), loc)
- val t = (L'.CApp (t, (L'.CConcat (bind1, bind2), loc)), loc)
-
- fun doUnify (ns, ns') =
- let
- fun setEmpty c =
- let
- val ((c, _), gs) = hnormCon (env, denv) c
- in
- case c of
- L'.CUnif (_, _, _, r) =>
- (r := SOME cemp;
- gs)
- | L'.CConcat (_, c') => setEmpty c' @ gs
- | _ => gs
- end
-
- val gs1 = unifyCons (env, denv) ns ns'
- val gs2 = setEmpty ns'
- val gs3 = unifyCons (env, denv) ns ns'
- in
- gs1 @ gs2 @ gs3
- end handle CUnify _ => (expError env (IncompatibleCons (ns, ns'));
- [])
-
- val gs7 = doUnify (ns1, ns1')
- val gs8 = doUnify (ns2, ns2')
- in
- (e, t, (loc, env, denv, shared, ctx1)
- :: (loc, env, denv, shared, ctx2)
- :: (loc, env, denv, use1, use2)
- :: (loc, env, denv, bind1, bind2)
- :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8)
- end*)
-
| L.EApp (e1, e2) =>
let
val (e1', t1, gs1) = elabExp (env, denv) e1
diff --git a/tests/gform.lac b/tests/gform.lac
index 51df468c..4ce75e3e 100644
--- a/tests/gform.lac
+++ b/tests/gform.lac
@@ -19,12 +19,21 @@ functor F (M : S) : S' where con rs = M.rs = struct
</body></html>
val page = fn () => <html><body>
-
+ <lform>
+ {fold [fn rs :: {Unit} => xml lform [] (stringify rs)]
+ (fn nm :: Name => fn u :: Unit => fn rest :: {Unit} =>
+ fn frag : xml lform [] (stringify rest) =>
+ <lform><li>{frag} <textbox{nm}/></li></lform>)
+ <lform></lform>
+ [rs]}
+
+ <submit action={handler}/>
+ </lform>
</body></html>
end
structure M = F(struct
- con rs = []
+ con rs = [A, B, C]
end)
open M
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 10:17:01 +0000