changeset 8:a455a9f85cc3

Parsing basic expressions
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 17:10:26 -0500
parents 2ce5bf227d01
children 14b533dbe6cc
files src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/stuff.lac
diffstat 9 files changed, 137 insertions(+), 32 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Sat Jan 26 16:51:39 2008 -0500
+++ b/src/elab.sml	Sat Jan 26 17:10:26 2008 -0500
@@ -52,7 +52,7 @@
        | CRel of int
        | CNamed of int
        | CApp of con * con
-       | CAbs of explicitness * string * kind * con
+       | CAbs of string * kind * con
 
        | CName of string
 
--- a/src/elab_print.sml	Sat Jan 26 16:51:39 2008 -0500
+++ b/src/elab_print.sml	Sat Jan 26 17:10:26 2008 -0500
@@ -91,17 +91,17 @@
       | CApp (c1, c2) => parenIf par (box [p_con env c1,
                                            space,
                                            p_con' true env c2])
-      | CAbs (e, x, k, c) => parenIf par (box [string "fn",
-                                               space,
-                                               string x,
-                                               space,
-                                               p_explicitness e,
-                                               space,
-                                               p_kind k,
-                                               space,
-                                               string "=>",
-                                               space,
-                                               p_con (E.pushCRel env x k) c])
+      | 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])
 
       | CName s => box [string "#", string s]
 
--- a/src/elab_util.sml	Sat Jan 26 16:51:39 2008 -0500
+++ b/src/elab_util.sml	Sat Jan 26 17:10:26 2008 -0500
@@ -111,12 +111,12 @@
                          S.map2 (mfc c2,
                               fn c2' =>
                                  (CApp (c1', c2'), loc)))
-              | CAbs (e, x, k, c) =>
+              | CAbs (x, k, c) =>
                 S.bind2 (mfk k,
                       fn k' =>
                          S.map2 (mfc c,
                               fn c' =>
-                                 (CAbs (e, x, k', c'), loc)))
+                                 (CAbs (x, k', c'), loc)))
 
               | CName _ => S.return2 cAll
 
--- a/src/elaborate.sml	Sat Jan 26 16:51:39 2008 -0500
+++ b/src/elaborate.sml	Sat Jan 26 17:10:26 2008 -0500
@@ -219,14 +219,13 @@
             checkKind env c2' k2 dom;
             ((L'.CApp (c1', c2'), loc), ran)
         end
-      | L.CAbs (e, x, k, t) =>
+      | L.CAbs (x, k, t) =>
         let
-            val e' = elabExplicitness e
             val k' = elabKind k
             val env' = E.pushCRel env x k'
             val (t', tk) = elabCon env' t
         in
-            ((L'.CAbs (e', x, k', t'), loc),
+            ((L'.CAbs (x, k', t'), loc),
              (L'.KArrow (k', tk), loc))
         end
 
--- a/src/lacweb.grm	Sat Jan 26 16:51:39 2008 -0500
+++ b/src/lacweb.grm	Sat Jan 26 17:10:26 2008 -0500
@@ -39,7 +39,7 @@
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH
- | CON | LTYPE
+ | CON | LTYPE | VAL
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | DOLLAR
@@ -59,6 +59,10 @@
  | rcon of (con * con) list
  | rcone of (con * con) list
 
+ | eexp of exp
+ | eapps of exp
+ | eterm of exp
+
 %verbose                                (* print summary of errors *)
 %pos int                                (* positions *)
 %start file
@@ -88,6 +92,8 @@
        | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
        | LTYPE SYMBOL EQ cexp           (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
+       | VAL SYMBOL EQ eexp             (DVal (SYMBOL, NONE, eexp), s (VALleft, eexpright))
+       | VAL SYMBOL COLON cexp EQ eexp  (DVal (SYMBOL, SOME cexp, eexp), s (VALleft, eexpright))
 
 kind   : TYPE                           (KType, s (TYPEleft, TYPEright))
        | NAME                           (KName, s (NAMEleft, NAMEright))
@@ -104,9 +110,9 @@
 
        | cexp PLUSPLUS cexp             (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))
 
-       | FN SYMBOL kcolon kind DARROW cexp (CAbs (kcolon, SYMBOL, kind, cexp), s (FNleft, cexpright))
+       | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, kind, cexp), s (FNleft, cexpright))
 
-       | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, RPARENright))
+       | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
 
 kcolon : DCOLON                         (Explicit)
        | TCOLON                         (Implicit)
@@ -130,3 +136,18 @@
 
 ident  : CSYMBOL                        (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
        | SYMBOL                         (CVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+
+eapps  : eterm                          (eterm)
+       | eapps eterm                    (EApp (eapps, eterm), s (eappsleft, etermright))
+       | eapps LBRACK cexp RBRACK       (ECApp (eapps, cexp), s (eappsleft, RBRACKright))
+
+eexp   : eapps                          (eapps)
+       | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright))
+       | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright))
+       | FN SYMBOL DARROW eexp          (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright))
+
+       | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
+
+eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
+
+       | SYMBOL                         (EVar SYMBOL, s (SYMBOLleft, SYMBOLright))
--- a/src/lacweb.lex	Sat Jan 26 16:51:39 2008 -0500
+++ b/src/lacweb.lex	Sat Jan 26 17:10:26 2008 -0500
@@ -110,6 +110,7 @@
 
 <INITIAL> "con"       => (Tokens.CON (yypos, yypos + size yytext));
 <INITIAL> "type"      => (Tokens.LTYPE (yypos, yypos + size yytext));
+<INITIAL> "val"       => (Tokens.VAL (yypos, yypos + size yytext));
 <INITIAL> "fn"        => (Tokens.FN (yypos, yypos + size yytext));
 
 <INITIAL> "Type"      => (Tokens.TYPE (yypos, yypos + size yytext));
--- a/src/source.sml	Sat Jan 26 16:51:39 2008 -0500
+++ b/src/source.sml	Sat Jan 26 17:10:26 2008 -0500
@@ -50,7 +50,7 @@
 
        | CVar of string
        | CApp of con * con
-       | CAbs of explicitness * string * kind * con
+       | CAbs of string * kind * con
 
        | CName of string
 
@@ -59,8 +59,20 @@
 
 withtype con = con' located
 
+datatype exp' =
+         EAnnot of exp * con
+
+       | EVar of string
+       | EApp of exp * exp
+       | EAbs of string * con option * exp
+       | ECApp of exp * con
+       | ECAbs of explicitness * string * kind * exp
+
+withtype exp = exp' located
+
 datatype decl' =
          DCon of string * kind option * con
+       | DVal of string * con option * exp
 
 withtype decl = decl' located
 
--- a/src/source_print.sml	Sat Jan 26 16:51:39 2008 -0500
+++ b/src/source_print.sml	Sat Jan 26 17:10:26 2008 -0500
@@ -91,17 +91,17 @@
       | CApp (c1, c2) => parenIf par (box [p_con c1,
                                            space,
                                            p_con' true c2])
-      | CAbs (e, x, k, c) => parenIf par (box [string "fn",
-                                               space,
-                                               string x,
-                                               space,
-                                               p_explicitness e,
-                                               space,
-                                               p_kind k,
-                                               space,
-                                               string "=>",
-                                               space,
-                                               p_con c])
+      | CAbs (x, 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]
 
@@ -121,6 +121,57 @@
         
 and p_con c = p_con' false c
 
+fun p_exp' par (e, _) =
+    case e of
+        EAnnot (e, t) => box [string "(",
+                              p_exp e,
+                              space,
+                              string ":",
+                              space,
+                              p_con t,
+                              string ")"]        
+
+      | EVar s => string s
+      | EApp (e1, e2) => parenIf par (box [p_exp e1,
+                                           space,
+                                           p_exp' true e2])
+      | EAbs (x, NONE, e) => parenIf par (box [string "fn",
+                                               space,
+                                               string x,
+                                               space,
+                                               string "=>",
+                                               space,
+                                               p_exp e])
+      | EAbs (x, SOME t, e) => parenIf par (box [string "fn",
+                                                 space,
+                                                 string x,
+                                                 space,
+                                                 string ":",
+                                                 space,
+                                                 p_con t,
+                                                 space,
+                                                 string "=>",
+                                                 space,
+                                                 p_exp e])
+      | ECApp (e, c) => parenIf par (box [p_exp e,
+                                          space,
+                                          string "[",
+                                          p_con c,
+                                          string "]"])
+      | ECAbs (exp, x, k, e) => parenIf par (box [string "fn",
+                                                  space,
+                                                  string x,
+                                                  space,
+                                                  p_explicitness exp,
+                                                  space,
+                                                  p_kind k,
+                                                  space,
+                                                  string "=>",
+                                                  space,
+                                                  p_exp e])
+
+and p_exp e = p_exp' false e
+
 fun p_decl ((d, _) : decl) =
     case d of
         DCon (x, NONE, c) => box [string "con",
@@ -141,6 +192,24 @@
                                     string "=",
                                     space,
                                     p_con c]
+      | DVal (x, NONE, e) => box [string "val",
+                                  space,
+                                  string x,
+                                  space,
+                                  string "=",
+                                  space,
+                                  p_exp e]
+      | DVal (x, SOME t, e) => box [string "val",
+                                    space,
+                                    string x,
+                                    space,
+                                    string ":",
+                                    space,
+                                    p_con t,
+                                    space,
+                                    string "=",
+                                    space,
+                                    p_exp e]
 
 val p_file = p_list_sep newline p_decl
 
--- a/tests/stuff.lac	Sat Jan 26 16:51:39 2008 -0500
+++ b/tests/stuff.lac	Sat Jan 26 17:10:26 2008 -0500
@@ -13,3 +13,6 @@
 
 con c9 = {}
 con c10 = ([]) :: {Type}
+
+val v1 = fn t :: Type => fn x : t => x
+val v2 = v1 [c1] (fn y => y)