summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elab_env.sig2
-rw-r--r--src/elab_env.sml9
-rw-r--r--src/elab_print.sml2
-rw-r--r--src/elaborate.sml60
-rw-r--r--src/lacweb.grm19
-rw-r--r--src/lacweb.lex2
6 files changed, 69 insertions, 25 deletions
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 32ba7906..1d265991 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -103,4 +103,6 @@ signature ELAB_ENV = sig
val chaseMpath : env -> (int * string list) -> Elab.str * Elab.sgn
+ val patBinds : env -> Elab.pat -> env
+
end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 936d8fce..a1a68974 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1049,4 +1049,13 @@ fun declBinds env (d, loc) =
pushClass env n
end
+fun patBinds env (p, loc) =
+ case p of
+ PWild => env
+ | PVar (x, t) => pushERel env x t
+ | PPrim _ => env
+ | PCon (_, _, _, NONE) => env
+ | PCon (_, _, _, SOME p) => patBinds env p
+ | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
+
end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 72453f29..337b1d8a 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -360,7 +360,7 @@ fun p_exp' par env (e, _) =
space,
string "=>",
space,
- p_exp env e]) pes])
+ p_exp (E.patBinds env p) e]) pes])
| EError => string "<ERROR>"
| EUnif (ref (SOME e)) => p_exp env e
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 746a06b7..b86514e7 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1268,6 +1268,13 @@ datatype coverage =
| Datatype of coverage IM.map
| Record of coverage SM.map list
+fun c2s c =
+ case c of
+ Wild => "Wild"
+ | None => "None"
+ | Datatype _ => "Datatype"
+ | Record _ => "Record"
+
fun exhaustive (env, denv, t, ps) =
let
fun pcCoverage pc =
@@ -1359,26 +1366,39 @@ fun exhaustive (env, denv, t, ps) =
end
fun coverageImp (c1, c2) =
- case (c1, c2) of
- (Wild, _) => true
-
- | (Datatype cmap1, Datatype cmap2) =>
- List.all (fn (n, c2) =>
- case IM.find (cmap1, n) of
- NONE => false
- | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2)
-
- | (Record fmaps1, Record fmaps2) =>
- List.all (fn fmap2 =>
- List.exists (fn fmap1 =>
- List.all (fn (x, c2) =>
- case SM.find (fmap1, x) of
- NONE => true
- | SOME c1 => coverageImp (c1, c2))
- (SM.listItemsi fmap2))
- fmaps1) fmaps2
-
- | _ => false
+ let
+ val r =
+ case (c1, c2) of
+ (Wild, _) => true
+
+ | (Datatype cmap1, Datatype cmap2) =>
+ List.all (fn (n, c2) =>
+ case IM.find (cmap1, n) of
+ NONE => false
+ | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2)
+ | (Datatype cmap1, Wild) =>
+ List.all (fn (n, c1) => coverageImp (c1, Wild)) (IM.listItemsi cmap1)
+
+ | (Record fmaps1, Record fmaps2) =>
+ List.all (fn fmap2 =>
+ List.exists (fn fmap1 =>
+ List.all (fn (x, c2) =>
+ case SM.find (fmap1, x) of
+ NONE => true
+ | SOME c1 => coverageImp (c1, c2))
+ (SM.listItemsi fmap2))
+ fmaps1) fmaps2
+
+ | (Record fmaps1, Wild) =>
+ List.exists (fn fmap1 =>
+ List.all (fn (x, c1) => coverageImp (c1, Wild))
+ (SM.listItemsi fmap1)) fmaps1
+
+ | _ => false
+ in
+ (*TextIO.print ("coverageImp(" ^ c2s c1 ^ ", " ^ c2s c2 ^ ") = " ^ Bool.toString r ^ "\n");*)
+ r
+ end
fun isTotal (c, t) =
case c of
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 87fa4655..feff82df 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -154,7 +154,7 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
| CON | LTYPE | VAL | REC | AND | FUN | FOLD | UNIT | KUNIT | CLASS
| DATATYPE | OF
| TYPE | NAME
- | ARROW | LARROW | DARROW | STAR
+ | ARROW | LARROW | DARROW | STAR | SEMI
| FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE
| STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
| INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE
@@ -277,6 +277,8 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
%name Lacweb
+%right SEMI
+%nonassoc LARROW
%nonassoc IF THEN ELSE
%nonassoc DARROW
%nonassoc COLON
@@ -286,7 +288,7 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
%right OR
%right CAND
%nonassoc EQ NE LT LE GT GE
-%right ARROW LARROW
+%right ARROW
%right PLUSPLUS MINUSMINUS
%right STAR
%left NOT
@@ -586,6 +588,13 @@ eexp : eapps (eapps)
(ECase (eexp1, [((PCon (["Basis"], "True", NONE), loc), eexp2),
((PCon (["Basis"], "False", NONE), loc), eexp3)]), loc)
end)
+ | SYMBOL LARROW eexp SEMI eexp (let
+ val loc = s (SYMBOLleft, eexp2right)
+ val e = (EVar (["Basis"], "bind"), loc)
+ val e = (EApp (e, eexp1), loc)
+ in
+ (EApp (e, (EAbs (SYMBOL, NONE, eexp2), loc)), loc)
+ end)
eargs : earg (earg)
| eargl (eargl)
@@ -725,8 +734,10 @@ pterm : SYMBOL (PVar SYMBOL, s (SYMBOLleft, SYMBOLright
s (LPARENleft, RPARENright))
rpat : CSYMBOL EQ pat ([(CSYMBOL, pat)], false)
+ | INT EQ pat ([(Int64.toString INT, pat)], false)
| DOTDOTDOT ([], true)
| CSYMBOL EQ pat COMMA rpat ((CSYMBOL, pat) :: #1 rpat, #2 rpat)
+ | INT EQ pat COMMA rpat ((Int64.toString INT, pat) :: #1 rpat, #2 rpat)
ptuple : pat COMMA pat ([pat1, pat2])
| pat COMMA ptuple (pat :: ptuple)
@@ -892,12 +903,12 @@ tables : table ([table])
tname : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
| LBRACE cexp RBRACE (cexp)
-table : SYMBOL ((CName SYMBOL, s (SYMBOLleft, SYMBOLright)),
+table : SYMBOL ((CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright)),
(EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright)))
| SYMBOL AS tname (tname, (EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright)))
| LBRACE LBRACE eexp RBRACE RBRACE AS tname (tname, eexp)
-tident : SYMBOL (CName SYMBOL, s (SYMBOLleft, SYMBOLright))
+tident : SYMBOL (CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright))
| CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
| LBRACE LBRACE cexp RBRACE RBRACE (cexp)
diff --git a/src/lacweb.lex b/src/lacweb.lex
index b7459675..e593c5fe 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -266,6 +266,8 @@ notags = [^<{\n]+;
<INITIAL> "~" => (Tokens.TWIDDLE (pos yypos, pos yypos + size yytext));
<INITIAL> "|" => (Tokens.BAR (pos yypos, pos yypos + size yytext));
<INITIAL> "*" => (Tokens.STAR (pos yypos, pos yypos + size yytext));
+<INITIAL> "<-" => (Tokens.LARROW (pos yypos, pos yypos + size yytext));
+<INITIAL> ";" => (Tokens.SEMI (pos yypos, pos yypos + size yytext));
<INITIAL> "con" => (Tokens.CON (pos yypos, pos yypos + size yytext));
<INITIAL> "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-29 14:20:08 +0000