Primitive type constants

15 files changed, 158 insertions, 14 deletions

diff --git a/src/compiler.sml b/src/compiler.sml
index 3e39dcc9..6ea5f1dc 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -76,10 +76,10 @@ fun testParse filename =
          print "\n")
 
 fun testElaborate filename =
-    (case elaborate ElabEnv.empty filename of
+    (case elaborate ElabEnv.basis filename of
          NONE => print "Failed\n"
        | SOME (_, file) =>
-         (Print.print (ElabPrint.p_file ElabEnv.empty file);
+         (Print.print (ElabPrint.p_file ElabEnv.basis file);
           print "\n"))
     handle ElabEnv.UnboundNamed n =>
            print ("Unbound named " ^ Int.toString n ^ "\n")
diff --git a/src/elab.sml b/src/elab.sml
index b08d9a6c..fc6ca366 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -65,7 +65,8 @@ datatype con' =
 withtype con = con' located
 
 datatype exp' =
-         ERel of int
+         EPrim of Prim.t
+       | ERel of int
        | ENamed of int
        | EApp of exp * exp
        | EAbs of string * con * exp
diff --git a/src/elab_env.sig b/src/elab_env.sig
index f7f798e5..8fe1da71 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -33,6 +33,7 @@ signature ELAB_ENV = sig
     type env
 
     val empty : env
+    val basis : env
 
     exception UnboundRel of int
     exception UnboundNamed of int
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 417eab74..2308fbb6 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -193,4 +193,13 @@ fun declBinds env (d, _) =
         DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
       | DVal (x, n, t, _) => pushENamedAs env x n t
 
+val ktype = (KType, ErrorMsg.dummySpan)
+
+fun bbind env x = #1 (pushCNamed env x ktype NONE)
+
+val basis = empty
+val basis = bbind basis "int"
+val basis = bbind basis "float"
+val basis = bbind basis "string"
+
 end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 2b9d7920..fcf5e747 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -151,7 +151,8 @@ and p_con env = p_con' false env
 
 fun p_exp' par env (e, _) =
     case e of
-        ERel n =>
+        EPrim p => Prim.p_t p
+      | ERel n =>
         if !debug then
             string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
         else
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 7a40a889..db444f82 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -205,7 +205,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
 
         and mfe' ctx (eAll as (e, loc)) =
             case e of
-                ERel _ => S.return2 eAll
+                EPrim _ => S.return2 eAll
+              | ERel _ => S.return2 eAll
               | ENamed _ => S.return2 eAll
               | EApp (e1, e2) =>
                 S.bind2 (mfe ctx e1,
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 53a45358..cb1f021a 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -27,6 +27,7 @@
 
 structure Elaborate :> ELABORATE = struct
 
+structure P = Prim
 structure L = Source
 structure L' = Elab
 structure E = ElabEnv
@@ -440,8 +441,8 @@ and consEq env (c1, c2) =
 
 and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
     let
-        val () = eprefaces "Summaries" [("#1", p_summary env s1),
-                                        ("#2", p_summary env s2)]
+        (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
+                                          ("#2", p_summary env s2)]*)
 
         fun eatMatching p (ls1, ls2) =
             let
@@ -471,8 +472,8 @@ and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
                                               true)
                                          else
                                              false) (#fields s1, #fields s2)
-        val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
-                                         ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]
+        (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
+                                           ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
         val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
         val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
 
@@ -665,6 +666,20 @@ fun checkCon env e c1 c2 =
     handle CUnify (c1, c2, err) =>
            expError env (Unify (e, c1, c2, err))
 
+fun primType env p =
+    let
+        val s = case p of
+                    P.Int _ => "int"
+                  | P.Float _ => "float"
+                  | P.String _ => "string"
+    in
+        case E.lookupC env s of
+            E.NotBound => raise Fail ("Primitive type " ^ s ^ " unbound")
+          | E.Rel _ => raise Fail ("Primitive type " ^ s ^ " bound as relative")
+          | E.Named (n, (L'.KType, _)) => L'.CNamed n
+          | E.Named _ => raise Fail ("Primitive type " ^ s ^ " bound at non-Type kind")
+    end
+
 fun elabExp env (e, loc) =
     case e of
         L.EAnnot (e, t) =>
@@ -676,6 +691,7 @@ fun elabExp env (e, loc) =
             (e', t')
         end
 
+      | L.EPrim p => ((L'.EPrim p, loc), (primType env p, loc))
       | L.EVar s =>
         (case E.lookupE env s of
              E.NotBound =>
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 80b35510..775cb31c 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -36,6 +36,7 @@ val s = ErrorMsg.spanOf
 
 %term 
    EOF
+ | STRING of string | INT of Int64.int | FLOAT of Real64.real
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH
@@ -155,6 +156,10 @@ eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
        | SYMBOL                         (EVar SYMBOL, s (SYMBOLleft, SYMBOLright))
        | LBRACE rexp RBRACE             (ERecord rexp, s (LBRACEleft, RBRACEright))
 
+       | INT                            (EPrim (Prim.Int INT), s (INTleft, INTright))
+       | FLOAT                          (EPrim (Prim.Float FLOAT), s (FLOATleft, FLOATright))
+       | STRING                         (EPrim (Prim.String STRING), s (STRINGleft, STRINGright))
+
 rexp   :                                ([])
        | ident EQ eexp                  ([(ident, eexp)])
        | ident EQ eexp COMMA rexp       ((ident, eexp) :: rexp)
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 5234db3d..af2ed464 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -59,14 +59,19 @@ in
     end
 end
 
+val str = ref ([] : char list)
+val strStart = ref 0
+
 %%
 %header (functor LacwebLexFn(structure Tokens : Lacweb_TOKENS));
 %full
-%s COMMENT;
+%s COMMENT STRING;
 
 id = [a-z_][A-Za-z0-9_]*;
 cid = [A-Z][A-Za-z0-9_]*;
 ws = [\ \t\012];
+intconst = [0-9]+;
+realconst = [0-9]+\.[0-9]*;
 
 %%
 
@@ -88,6 +93,14 @@ ws = [\ \t\012];
 <COMMENT> "*)"        => (if exitComment () then YYBEGIN INITIAL else ();
 			  continue ());
 
+<INITIAL> "\""        => (YYBEGIN STRING; strStart := yypos; str := []; continue());
+<STRING> "\\\""       => (str := #"\"" :: !str; continue());
+<STRING> "\""         => (YYBEGIN INITIAL;
+			  Tokens.STRING (String.implode (List.rev (!str)), !strStart, yypos + 1));
+<STRING> "\n"         => (ErrorMsg.newline yypos;
+			  str := #"\n" :: !str; continue());
+<STRING> .            => (str := String.sub (yytext, 0) :: !str; continue());
+
 <INITIAL> "("         => (Tokens.LPAREN (yypos, yypos + size yytext));
 <INITIAL> ")"         => (Tokens.RPAREN (yypos, yypos + size yytext));
 <INITIAL> "["         => (Tokens.LBRACK (yypos, yypos + size yytext));
@@ -119,6 +132,17 @@ ws = [\ \t\012];
 <INITIAL> {id}        => (Tokens.SYMBOL (yytext, yypos, yypos + size yytext));
 <INITIAL> {cid}       => (Tokens.CSYMBOL (yytext, yypos, yypos + size yytext));
 
+<INITIAL> {intconst}  => (case Int64.fromString yytext of
+                            SOME x => Tokens.INT (x, yypos, yypos + size yytext)
+                          | NONE   => (ErrorMsg.errorAt' (yypos, yypos)
+                                       ("Expected int, received: " ^ yytext);
+                                       continue ()));
+<INITIAL> {realconst} => (case Real64.fromString yytext of
+                            SOME x => Tokens.FLOAT (x, yypos, yypos + size yytext)
+                          | NONE   => (ErrorMsg.errorAt' (yypos, yypos)
+                                       ("Expected float, received: " ^ yytext);
+                                       continue ()));
+
 <COMMENT> .           => (continue());
 
 <INITIAL> .           => (ErrorMsg.errorAt' (yypos, yypos)
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index ac9c24d6..433b19f2 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -26,5 +26,5 @@
  *)
 
 val () = case CommandLine.arguments () of
-             [filename] => Compiler.testParse filename
+             [filename] => Compiler.testElaborate filename
            | _ => print "Bad arguments"
diff --git a/src/prim.sig b/src/prim.sig
new file mode 100644
index 00000000..6861ec8a
--- /dev/null
+++ b/src/prim.sig
@@ -0,0 +1,37 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature PRIM = sig
+
+    datatype t =
+             Int of Int64.int
+           | Float of Real64.real
+           | String of string
+
+    val p_t : t Print.printer
+
+end
diff --git a/src/prim.sml b/src/prim.sml
new file mode 100644
index 00000000..95228842
--- /dev/null
+++ b/src/prim.sml
@@ -0,0 +1,44 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure Prim :> PRIM = struct
+
+datatype t =
+         Int of Int64.int
+       | Float of Real64.real
+       | String of string
+
+open Print.PD
+open Print
+
+fun p_t t =
+    case t of
+        Int n => string (Int64.toString n)
+      | Float n => string (Real64.toString n)
+      | String s => box [string "\"", string s, string "\""]
+
+end
diff --git a/src/source.sml b/src/source.sml
index 05b2973f..9b0e2a07 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -62,6 +62,7 @@ withtype con = con' located
 datatype exp' =
          EAnnot of exp * con
 
+       | EPrim of Prim.t
        | EVar of string
        | EApp of exp * exp
        | EAbs of string * con option * exp
diff --git a/src/source_print.sml b/src/source_print.sml
index de9e2c7c..3db15ec6 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -131,6 +131,7 @@ fun p_exp' par (e, _) =
                               p_con t,
                               string ")"]        
 
+      | EPrim p => Prim.p_t p
       | EVar s => string s
       | EApp (e1, e2) => parenIf par (box [p_exp e1,
                                            space,
diff --git a/src/sources b/src/sources
index 1c3ae6ff..b9c22fd3 100644
--- a/src/sources
+++ b/src/sources
@@ -7,14 +7,17 @@ list_util.sml
 errormsg.sig
 errormsg.sml
 
+print.sig
+print.sml
+
+prim.sig
+prim.sml
+
 source.sml
 
 lacweb.grm
 lacweb.lex
 
-print.sig
-print.sml
-
 source_print.sig
 source_print.sml