summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_print.sml1
-rw-r--r--src/elab_util.sml6
-rw-r--r--src/elaborate.sml50
-rw-r--r--src/explify.sml1
-rw-r--r--src/lacweb.grm6
-rw-r--r--src/lacweb.lex1
-rw-r--r--src/source.sml3
-rw-r--r--src/source_print.sml30
9 files changed, 80 insertions, 19 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 43837413..ea00d199 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -59,6 +59,7 @@ datatype con' =
| CRecord of kind * (con * con) list
| CConcat of con * con
+ | CFold of kind * kind
| CError
| CUnif of kind * string * con option ref
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 4c02c495..2b515a03 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -152,6 +152,7 @@ fun p_con' par env (c, _) =
string "++",
space,
p_con env c2])
+ | CFold _ => string "fold"
| CError => string "<ERROR>"
| CUnif (_, _, ref (SOME c)) => p_con' par env c
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 2d075fb4..7892211c 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -143,6 +143,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
S.map2 (mfc ctx c2,
fn c2' =>
(CConcat (c1', c2'), loc)))
+ | CFold (k1, k2) =>
+ S.bind2 (mfk k1,
+ fn k1' =>
+ S.map2 (mfk k2,
+ fn k2' =>
+ (CFold (k1', k2'), loc)))
| CError => S.return2 cAll
| CUnif (_, _, ref (SOME c)) => mfc' ctx c
diff --git a/src/elaborate.sml b/src/elaborate.sml
index cc9c2f80..d6e3085d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -115,6 +115,7 @@ datatype con_error =
UnboundCon of ErrorMsg.span * string
| UnboundStrInCon of ErrorMsg.span * string
| WrongKind of L'.con * L'.kind * L'.kind * kunify_error
+ | DuplicateField of ErrorMsg.span * string
fun conError env err =
case err of
@@ -128,6 +129,8 @@ fun conError env err =
("Have kind", p_kind k1),
("Need kind", p_kind k2)];
kunifyError kerr)
+ | DuplicateField (loc, s) =>
+ ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
fun checkKind env c k1 k2 =
unifyKinds k1 k2
@@ -198,6 +201,14 @@ fun elabKind (k, loc) =
| L.KRecord k => (L'.KRecord (elabKind k), loc)
| L.KWild => kunif ()
+fun foldKind (dom, ran, loc)=
+ (L'.KArrow ((L'.KArrow ((L'.KName, loc),
+ (L'.KArrow (dom,
+ (L'.KArrow (ran, ran), loc)), loc)), loc),
+ (L'.KArrow (ran,
+ (L'.KArrow ((L'.KRecord dom, loc),
+ ran), loc)), loc)), loc)
+
fun elabCon env (c, loc) =
case c of
L.CAnnot (c, k) =>
@@ -278,9 +289,11 @@ fun elabCon env (c, loc) =
checkKind env c2' k2 dom;
((L'.CApp (c1', c2'), loc), ran)
end
- | L.CAbs (x, k, t) =>
+ | L.CAbs (x, ko, t) =>
let
- val k' = elabKind k
+ val k' = case ko of
+ NONE => kunif ()
+ | SOME k => elabKind k
val env' = E.pushCRel env x k'
val (t', tk) = elabCon env' t
in
@@ -304,8 +317,11 @@ fun elabCon env (c, loc) =
checkKind env c' ck k;
(x', c')
end) xcs
+
+ val rc = (L'.CRecord (k, xcs'), loc)
+ (* Add duplicate field checking later. *)
in
- ((L'.CRecord (k, xcs'), loc), (L'.KRecord k, loc))
+ (rc, (L'.KRecord k, loc))
end
| L.CConcat (c1, c2) =>
let
@@ -318,6 +334,14 @@ fun elabCon env (c, loc) =
checkKind env c2' k2 k;
((L'.CConcat (c1', c2'), loc), k)
end
+ | L.CFold =>
+ let
+ val dom = kunif ()
+ val ran = kunif ()
+ in
+ ((L'.CFold (dom, ran), loc),
+ foldKind (dom, ran, loc))
+ end
| L.CWild k =>
let
@@ -473,6 +497,7 @@ fun kindof env (c, loc) =
| L'.CRecord (k, _) => (L'.KRecord k, loc)
| L'.CConcat (c, _) => kindof env c
+ | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
| L'.CError => kerror
| L'.CUnif (k, _, _) => k
@@ -624,10 +649,25 @@ and hnormCon env (cAll as (c, loc)) =
end
| L'.CApp (c1, c2) =>
- (case hnormCon env c1 of
- (L'.CAbs (_, _, cb), _) =>
+ (case #1 (hnormCon env c1) of
+ L'.CAbs (_, _, cb) =>
((hnormCon env (subConInCon (0, c2) cb))
handle SynUnif => cAll)
+ | L'.CApp (c', i) =>
+ (case #1 (hnormCon env c') of
+ L'.CApp (c', f) =>
+ (case #1 (hnormCon env c') of
+ L'.CFold ks =>
+ (case #1 (hnormCon env c2) of
+ L'.CRecord (_, []) => hnormCon env i
+ | L'.CRecord (k, (x, c) :: rest) =>
+ hnormCon env
+ (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
+ (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
+ (L'.CRecord (k, rest), loc)), loc)), loc)
+ | _ => cAll)
+ | _ => cAll)
+ | _ => cAll)
| _ => cAll)
| L'.CConcat (c1, c2) =>
diff --git a/src/explify.sml b/src/explify.sml
index 0c3f5f1f..79e3b07f 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -59,6 +59,7 @@ fun explifyCon (c, loc) =
| L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc)
| L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)
+ | L.CFold _ => raise Fail "Explify CFold"
| L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
| L.CUnif (_, _, ref (SOME c)) => explifyCon c
diff --git a/src/lacweb.grm b/src/lacweb.grm
index e36630ae..c1cf6712 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -40,7 +40,7 @@ val s = ErrorMsg.spanOf
| SYMBOL of string | CSYMBOL of string
| LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
| EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
- | CON | LTYPE | VAL
+ | CON | LTYPE | VAL | FOLD
| TYPE | NAME
| ARROW | LARROW | DARROW
| FN | PLUSPLUS | DOLLAR
@@ -190,7 +190,8 @@ cexp : capps (capps)
| cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))
- | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, kind, cexp), s (FNleft, cexpright))
+ | FN SYMBOL DARROW cexp (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright))
+ | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright))
| LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
@@ -214,6 +215,7 @@ cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright))
| path (CVar path, s (pathleft, pathright))
| UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
+ | FOLD (CFold, s (FOLDleft, FOLDright))
rcon : ([])
| ident EQ cexp ([(ident, cexp)])
diff --git a/src/lacweb.lex b/src/lacweb.lex
index a821cc9e..038e591f 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -146,6 +146,7 @@ realconst = [0-9]+\.[0-9]*;
<INITIAL> "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
<INITIAL> "val" => (Tokens.VAL (pos yypos, pos yypos + size yytext));
<INITIAL> "fn" => (Tokens.FN (pos yypos, pos yypos + size yytext));
+<INITIAL> "fold" => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
<INITIAL> "structure" => (Tokens.STRUCTURE (pos yypos, pos yypos + size yytext));
<INITIAL> "signature" => (Tokens.SIGNATURE (pos yypos, pos yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index 9ea1ea20..2246399b 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -51,12 +51,13 @@ datatype con' =
| CVar of string list * string
| CApp of con * con
- | CAbs of string * kind * con
+ | CAbs of string * kind option * con
| CName of string
| CRecord of (con * con) list
| CConcat of con * con
+ | CFold
| CWild of kind
diff --git a/src/source_print.sml b/src/source_print.sml
index ca72c014..b4496a7a 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -92,17 +92,24 @@ fun p_con' par (c, _) =
| CApp (c1, c2) => parenIf par (box [p_con c1,
space,
p_con' true c2])
- | CAbs (x, k, c) => parenIf par (box [string "fn",
- space,
- string x,
- space,
- string "::",
- space,
- p_kind k,
- space,
- string "=>",
- space,
- p_con c])
+ | CAbs (x, NONE, c) => parenIf par (box [string "fn",
+ space,
+ string x,
+ space,
+ string "=>",
+ space,
+ p_con c])
+ | CAbs (x, SOME k, c) => parenIf par (box [string "fn",
+ space,
+ string x,
+ space,
+ string "::",
+ space,
+ p_kind k,
+ space,
+ string "=>",
+ space,
+ p_con c])
| CName s => box [string "#", string s]
@@ -119,6 +126,7 @@ fun p_con' par (c, _) =
string "++",
space,
p_con c2])
+ | CFold => string "fold"
| CWild k => box [string "(_",
space,
string "::",
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 23:12:37 +0000