From 32115a531d5ed6cafa25dc7d3b88c2679e5142a5 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 8 Jun 2008 12:27:08 -0400 Subject: Primitive type constants --- src/compiler.sml | 4 ++-- src/elab.sml | 3 ++- src/elab_env.sig | 1 + src/elab_env.sml | 9 +++++++++ src/elab_print.sml | 3 ++- src/elab_util.sml | 3 ++- src/elaborate.sml | 24 ++++++++++++++++++++---- src/lacweb.grm | 5 +++++ src/lacweb.lex | 26 +++++++++++++++++++++++++- src/main.mlton.sml | 2 +- src/prim.sig | 37 +++++++++++++++++++++++++++++++++++++ src/prim.sml | 44 ++++++++++++++++++++++++++++++++++++++++++++ src/source.sml | 1 + src/source_print.sml | 1 + src/sources | 9 ++++++--- 15 files changed, 158 insertions(+), 14 deletions(-) create mode 100644 src/prim.sig create mode 100644 src/prim.sml (limited to 'src') 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]; "*)" => (if exitComment () then YYBEGIN INITIAL else (); continue ()); + "\"" => (YYBEGIN STRING; strStart := yypos; str := []; continue()); + "\\\"" => (str := #"\"" :: !str; continue()); + "\"" => (YYBEGIN INITIAL; + Tokens.STRING (String.implode (List.rev (!str)), !strStart, yypos + 1)); + "\n" => (ErrorMsg.newline yypos; + str := #"\n" :: !str; continue()); + . => (str := String.sub (yytext, 0) :: !str; continue()); + "(" => (Tokens.LPAREN (yypos, yypos + size yytext)); ")" => (Tokens.RPAREN (yypos, yypos + size yytext)); "[" => (Tokens.LBRACK (yypos, yypos + size yytext)); @@ -119,6 +132,17 @@ ws = [\ \t\012]; {id} => (Tokens.SYMBOL (yytext, yypos, yypos + size yytext)); {cid} => (Tokens.CSYMBOL (yytext, yypos, yypos + size yytext)); + {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 ())); + {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 ())); + . => (continue()); . => (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 -- cgit v1.2.3