From 234b917a6149413bbbeab7dccfaeab5f16e43fe1 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 29 Jul 2006 23:24:08 +0000 Subject: [PATCH] Type-checking goodies in place --- src/ast.sml | 14 ++++ src/domtool.cm | 3 + src/domtool.grm | 32 +++++++-- src/domtool.lex | 15 ++++- src/main.sig | 27 ++++++++ src/main.sml | 46 +++++++++++++ src/parse.sig | 2 +- src/print.sml | 9 ++- src/tycheck.sig | 9 ++- src/tycheck.sml | 170 +++++++++++++++++++++++++++++++++++++++--------- tests/test.dtl | 20 ++++-- 11 files changed, 298 insertions(+), 49 deletions(-) create mode 100644 src/main.sig create mode 100644 src/main.sml diff --git a/src/ast.sml b/src/ast.sml index e62c8fb..b48f13e 100644 --- a/src/ast.sml +++ b/src/ast.sml @@ -48,6 +48,10 @@ datatype typ' = * - Is valid in the given pred * - Expects an environment compatible with the first record * - Modifies it according to the second record *) + | TNested of pred * pred + (* Allow nested configuration, in the form of a function from an action + * satisfying the first predicate to an action satisfying the second and + * with the same environment variable IO behavior. *) | TError (* Marker that something already went wrong, so don't generate further @@ -72,6 +76,8 @@ datatype exp' = | EApp of exp * exp (* Function application *) + | ESkip + (* Do-nothing action *) | ESet of string * exp (* Set an environment variable *) | EGet of string * string * exp @@ -81,7 +87,15 @@ datatype exp' = | ELocal of exp (* Local execution; execute the action and then restore the previous * environment. *) + | EWith of exp * exp + (* Apply a TNested to an action *) withtype exp = exp' * position +datatype decl' = + DExternType of string + | DExternVal of string * typ +type decl = decl' * string option * position + +type file = decl list * exp option end diff --git a/src/domtool.cm b/src/domtool.cm index 440a307..790625c 100644 --- a/src/domtool.cm +++ b/src/domtool.cm @@ -23,3 +23,6 @@ print.sml tycheck.sig tycheck.sml + +main.sig +main.sml diff --git a/src/domtool.grm b/src/domtool.grm index 1ad3a5b..4b8405f 100644 --- a/src/domtool.grm +++ b/src/domtool.grm @@ -26,16 +26,22 @@ open Ast %term EOF | SYMBOL of string | CSYMBOL of string - | STRING of string + | STRING of string | DOC of string | INT of int | ARROW | DARROW | LARROW | COLON | CARET | BANG | AND | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | BSLASH | SEMI | LET | IN | END | ROOT + | EXTERN | TYPE | VAL | WITH %nonterm - file of exp + file of file + | decls of decl list + | decl of decl + | decl' of decl' + | docOpt of string option + | expOpt of exp option | exp of exp | apps of exp | term of exp @@ -67,7 +73,22 @@ open Ast %% -file : exp (exp) +file : decls expOpt (decls, expOpt) + +decls : ([]) + | decl SEMI decls (decl :: decls) + +decl : decl' docOpt (decl', docOpt, (decl'left, docOptright)) + +decl' : EXTERN TYPE SYMBOL (DExternType SYMBOL) + | EXTERN VAL SYMBOL COLON typ (DExternVal (SYMBOL, typ)) + +docOpt : (NONE) + | DOC (SOME DOC) + +expOpt : (NONE) + | exp (SOME (ELocal exp, (expleft, expright))) + exp : apps (apps) | BSLASH SYMBOL COLON LPAREN typ RPAREN ARROW exp (ELam (SYMBOL, SOME typ, exp), @@ -81,7 +102,9 @@ exp : apps (apps) in (ESeq ls, (exp1left, exp2right)) end) - | SYMBOL LARROW CSYMBOL SEMI exp (EGet (SYMBOL, CSYMBOL, exp), (SYMBOLleft, expright)) + | SYMBOL LARROW CSYMBOL SEMI exp (EGet (SYMBOL, CSYMBOL, exp), (SYMBOLleft, expright)) + | apps WITH END (EWith (apps, (ESkip, (WITHleft, ENDright))), (appsleft, ENDright)) + | apps WITH exp END (EWith (apps, exp), (appsleft, ENDright)) apps : term (term) | apps term (EApp (apps, term), (appsleft, termright)) @@ -109,6 +132,7 @@ typ : SYMBOL (TBase SYMBOL, (SYMBOLleft, SYMBOLrig | LBRACK ctxt RBRACK (TAction (ctxt, StringMap.empty, StringMap.empty), (LBRACKleft, ctxtright)) | LPAREN typ RPAREN (typ) + | ctxt DARROW ctxt (TNested (ctxt1, ctxt2), (ctxt1left, ctxt2right)) recd : LBRACE RBRACE (StringMap.empty) | LBRACE recdNe RBRACE (recdNe) diff --git a/src/domtool.lex b/src/domtool.lex index 5130ad9..66d0185 100644 --- a/src/domtool.lex +++ b/src/domtool.lex @@ -54,7 +54,7 @@ val strStart = ref 0 %% %header (functor DomtoolLexFn(structure Tokens : Domtool_TOKENS)); %full -%s COMMENT STRING; +%s COMMENT STRING DOC; id = [a-z_][A-Za-z0-9_]*; cid = [A-Z][A-Za-z0-9_]*; @@ -92,6 +92,14 @@ lineComment = #[^\n]*\n; str := #"\n" :: !str; continue()); . => (str := String.sub (yytext, 0) :: !str; continue()); + "{{" => (YYBEGIN DOC; strStart := yypos; str := []; continue()); + "}}" => (YYBEGIN INITIAL; + Tokens.DOC (String.implode (List.rev (!str)), !strStart, yypos + 1)); + "\n" => (lineNum := !lineNum + 1; + linePos := yypos :: ! linePos; + str := #"\n" :: !str; continue()); + . => (str := String.sub (yytext, 0) :: !str; continue()); + "(" => (Tokens.LPAREN (yypos, yypos + size yytext)); ")" => (Tokens.RPAREN (yypos, yypos + size yytext)); @@ -117,6 +125,11 @@ lineComment = #[^\n]*\n; "let" => (Tokens.LET (yypos, yypos + size yytext)); "in" => (Tokens.IN (yypos, yypos + size yytext)); "end" => (Tokens.END (yypos, yypos + size yytext)); + "with" => (Tokens.WITH (yypos, yypos + size yytext)); + + "extern" => (Tokens.EXTERN (yypos, yypos + size yytext)); + "type" => (Tokens.TYPE (yypos, yypos + size yytext)); + "val" => (Tokens.VAL (yypos, yypos + size yytext)); "Root" => (Tokens.ROOT (yypos, yypos + size yytext)); diff --git a/src/main.sig b/src/main.sig new file mode 100644 index 0000000..a7c3b2d --- /dev/null +++ b/src/main.sig @@ -0,0 +1,27 @@ +(* HCoop Domtool (http://hcoop.sourceforge.net/) + * Copyright (c) 2006, Adam Chlipala + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA. +*) + +(* Main interface *) + +signature MAIN = sig + + val tInit : Ast.typ + + val check : string -> unit + +end diff --git a/src/main.sml b/src/main.sml new file mode 100644 index 0000000..8cf8e67 --- /dev/null +++ b/src/main.sml @@ -0,0 +1,46 @@ +(* HCoop Domtool (http://hcoop.sourceforge.net/) + * Copyright (c) 2006, Adam Chlipala + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA. +*) + +(* Main interface *) + +structure Main :> MAIN = struct + +open Ast + +val dmy = ErrorMsg.dummyLoc + +val tInit = (TAction ((CRoot, dmy), + StringMap.empty, + StringMap.empty), + dmy) + +fun check fname = + let + val prog = Parse.parse fname + in + if !ErrorMsg.anyErrors then + () + else + let + val G' = Tycheck.checkFile Tycheck.empty tInit prog + in + () + end + end + +end diff --git a/src/parse.sig b/src/parse.sig index a708344..fa65151 100644 --- a/src/parse.sig +++ b/src/parse.sig @@ -20,5 +20,5 @@ signature PARSE = sig - val parse : string -> Ast.exp + val parse : string -> Ast.file end diff --git a/src/print.sml b/src/print.sml index 1f661dd..4acf9f1 100644 --- a/src/print.sml +++ b/src/print.sml @@ -58,7 +58,9 @@ fun p_typ' pn (t, _) = parenIf pn [p_typ' true t1, space 1, string "->", space 1, p_typ' true t2] | TAction (p, r1, r2) => parenIf pn [p_predBoxed p, space 1, p_record r1, space 1, - string "->", space 1, p_record r2] + string "=>", space 1, p_record r2] + | TNested (p1, p2) => + parenIf pn [p_pred' false p1, space 1, string "=>", space 1, p_pred' false p2] | TError => string "" | TUnif (_, ref (SOME t)) => p_typ' pn t @@ -101,6 +103,7 @@ fun p_exp (e, _) = | EVar x => string x | EApp (e1, e2) => dBox [string "(", p_exp e1, break {nsp = 1, offset = 0}, p_exp e2, string ")"] + | ESkip => string "_" | ESet (x, e) => dBox [string x, space 1, string "=", space 1, p_exp e] | EGet (x1, x2, e) => dBox [dBox [string x1, space 1, string "<-", space 1, string x2, string ";", space 1], @@ -113,7 +116,9 @@ fun p_exp (e, _) = string "in", space 1, p_exp e2, space 1, string "end"] - | ELocal _ => raise Fail "Unexpected ELocal form" + | ELocal e => dBox [string "local(", space 1, p_exp e, string ")"] + | EWith (e1, (ESkip, _)) => dBox [p_exp e1, space 1, string "with", space 1, string "end"] + | EWith (e1, e2) => dBox [p_exp e1, space 1, string "with", p_exp e2, space 1, string "end"] fun printd d = let diff --git a/src/tycheck.sig b/src/tycheck.sig index 4562e3c..a86ae37 100644 --- a/src/tycheck.sig +++ b/src/tycheck.sig @@ -20,12 +20,17 @@ signature TYCHECK = sig - type env = Ast.typ Ast.StringMap.map + type env val empty : env - val checkExp : env -> Ast.exp -> Ast.typ + val checkTyp : env -> Ast.typ -> Ast.typ + val checkExp : env -> Ast.exp -> Ast.typ val checkUnit : env -> Ast.exp -> Ast.typ (* [checkUnit] checks that all unification variables have been resolved. *) + val checkDecl : env -> Ast.decl -> env + + val checkFile : env -> Ast.typ -> Ast.file -> env + end diff --git a/src/tycheck.sml b/src/tycheck.sml index 03ede40..854b575 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -22,10 +22,18 @@ structure Tycheck :> TYCHECK = struct open Ast Print +structure SS = StringSet structure SM = StringMap -type env = typ SM.map -val empty = SM.empty +type env = SS.set * typ SM.map +val empty : env = (SS.add (SS.singleton "int", "string"), + SM.empty) + +fun lookupType (ts, _) name = SS.member (ts, name) +fun lookupVal (_, vs) name = SM.find (vs, name) + +fun bindType (ts, vs) name = (SS.add (ts, name), vs) +fun bindVal (ts, vs) (name, t) = (ts, SM.insert (vs, name, t)) local val unifCount = ref 0 @@ -90,6 +98,9 @@ fun eqTy (t1All as (t1, _), t2All as (t2, _)) = eqPred (p1, p2) andalso eqRecord eqTy (d1, d2) andalso eqRecord eqTy (r1, r2) + | (TNested (p1, q1), TNested (p2, q2)) => + eqPred (p1, p2) andalso eqPred (q1, q2) + | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All) | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2) @@ -110,6 +121,7 @@ datatype type_error = WrongType of string * exp * typ * typ * unification_error option | WrongForm of string * string * exp * typ * unification_error option | UnboundVariable of string + | WrongPred of string * pred * pred fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0, [PD.string s, PD.space 1, d])) @@ -117,7 +129,7 @@ fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0, fun describe_unification_error t ue = case ue of UnifyPred (p1, p2) => - (print "Reason: Incompatible predicates.\n"; + (print "Reason: Incompatible contexts.\n"; preface ("Have:", p_pred p1); preface ("Need:", p_pred p2)) | UnifyTyp (t1, t2) => @@ -151,6 +163,10 @@ fun describe_type_error loc te = Option.app (describe_unification_error t) ueo) | UnboundVariable name => ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n") + | WrongPred (place, p1, p2) => + (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ "."); + preface ("Have:", p_pred p1); + preface ("Need:", p_pred p2)) fun predImplies (p1All as (p1, _), p2All as (p2, _)) = case (p1, p2) of @@ -162,6 +178,7 @@ fun predImplies (p1All as (p1, _), p2All as (p2, _)) = | (CConst s1, CConst s2) => s1 = s2 | (CPrefix p1, CPrefix p2) => predImplies (p1, p2) + | (_, CPrefix p2) => predImplies (p1All, p2) | (CNot p1, CNot p2) => predImplies (p2, p1) @@ -189,21 +206,17 @@ fun predSimpl (pAll as (p, loc)) = (CAnd (p1', p2'), loc) end -fun unifyPred (p1, p2) = +fun subPred (p1, p2) = if predImplies (p1, p2) then () else raise (Unify (UnifyPred (p1, p2))) -fun unifyRecord f (r1, r2) = - (SM.appi (fn (k, v1) => - case SM.find (r2, k) of - NONE => raise UnequalDomains - | SOME v2 => f (v1, v2)) r1; - SM.appi (fn (k, v2) => - case SM.find (r1, k) of - NONE => raise UnequalDomains - | SOME v1 => f (v1, v2)) r2) +fun subRecord f (r1, r2) = + SM.appi (fn (k, v2) => + case SM.find (r1, k) of + NONE => raise UnequalDomains + | SOME v1 => f (v1, v2)) r2 fun occurs u (t, _) = case t of @@ -213,30 +226,36 @@ fun occurs u (t, _) = | TAction (_, d, r) => List.exists (occurs u) (SM.listItems d) orelse List.exists (occurs u) (SM.listItems r) + | TNested _ => false | TError => false | TUnif (_, ref (SOME t)) => occurs u t | TUnif (_, u') => u = u' -fun unify (t1All as (t1, _), t2All as (t2, _)) = +fun subTyp (t1All as (t1, _), t2All as (t2, _)) = case (t1, t2) of (TBase s1, TBase s2) => if s1 = s2 then () else raise Unify (UnifyTyp (t1All, t2All)) - | (TList t1, TList t2) => unify (t1, t2) + | (TList t1, TList t2) => subTyp (t1, t2) | (TArrow (d1, r1), TArrow (d2, r2)) => - (unify (d1, d2); - unify (r1, r2)) + (subTyp (d2, d1); + subTyp (r1, r2)) | (TAction (p1, d1, r1), TAction (p2, d2, r2)) => - ((unifyPred (p1, p2); - unifyRecord unify (d1, d2); - unifyRecord unify (r1, r2)) + ((subPred (p2, p1); + subRecord subTyp (d2, d1); + subRecord subTyp (r1, r2); + subRecord subTyp (r2, r1)) handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All))) - | (TUnif (_, ref (SOME t1)), _) => unify (t1, t2All) - | (_, TUnif (_, ref (SOME t2))) => unify (t1All, t2) + | (TNested (d1, r1), TNested (d2, r2)) => + (subPred (d2, d1); + subPred (r1, r2)) + + | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All) + | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2) | (TUnif (_, r1), TUnif (_, r2)) => if r1 = r2 then @@ -271,6 +290,26 @@ fun whnorm (tAll as (t, loc)) = TUnif (_, ref (SOME tAll)) => whnorm tAll | _ => tAll +fun checkTyp G (tAll as (t, loc)) = + let + val err = ErrorMsg.error (SOME loc) + in + case t of + TBase name => + if lookupType G name then + tAll + else + (err ("Unbound type name " ^ name); + (TError, loc)) + | TList t => (TList (checkTyp G t), loc) + | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc) + | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d, + SM.map (checkTyp G) r), loc) + | TNested _ => tAll + | TError => raise Fail "TError in parser-generated type" + | TUnif _ => raise Fail "TUnif in parser-generated type" + end + fun checkExp G (eAll as (e, loc)) = let val dte = describe_type_error loc @@ -286,7 +325,7 @@ fun checkExp G (eAll as (e, loc)) = let val t' = checkExp G e' in - (unify (t', t); + (subTyp (t', t); if isError t' then (TList (TError, loc), loc) else @@ -306,15 +345,15 @@ fun checkExp G (eAll as (e, loc)) = val t = case to of NONE => (newUnif (), loc) - | SOME t => t + | SOME t => checkTyp G t - val G' = SM.insert (G, x, t) + val G' = bindVal G (x, t) val t' = checkExp G' e in (TArrow (t, t'), loc) end | EVar x => - (case SM.find (G, x) of + (case lookupVal G x of NONE => (dte (UnboundVariable x); (TError, loc)) | SOME t => t) @@ -326,8 +365,8 @@ fun checkExp G (eAll as (e, loc)) = val tf = checkExp G func val ta = checkExp G arg in - (unify (tf, (TArrow (dom, ran), loc)); - unify (ta, dom) + (subTyp (tf, (TArrow (dom, ran), loc)); + subTyp (ta, dom) handle Unify ue => dte (WrongType ("Function argument", arg, @@ -356,7 +395,7 @@ fun checkExp G (eAll as (e, loc)) = | EGet (x, evar, rest) => let val xt = (newUnif (), loc) - val G' = SM.insert (G, x, xt) + val G' = bindVal G (x, xt) val rt = whnorm (checkExp G' rest) in @@ -365,7 +404,7 @@ fun checkExp G (eAll as (e, loc)) = (case SM.find (d, evar) of NONE => (TAction (p, SM.insert (d, evar, xt), r), loc) | SOME xt' => - (unify (xt', xt) + (subTyp (xt', xt) handle Unify ue => dte (WrongType ("Retrieved environment variable", (EVar x, loc), @@ -373,6 +412,7 @@ fun checkExp G (eAll as (e, loc)) = xt, SOME ue)); rt)) + | (TError, _) => rt | _ => (dte (WrongForm ("Body of environment variable read", "action", rest, @@ -403,7 +443,7 @@ fun checkExp G (eAll as (e, loc)) = (case SM.find (d', name) of NONE => SM.insert (d', name, t) | SOME t' => - (unify (t, t') + (subTyp (t, t') handle Unify ue => dte (WrongType ("Shared environment variable", (EVar name, loc), @@ -412,7 +452,7 @@ fun checkExp G (eAll as (e, loc)) = SOME ue)); d')) | SOME t' => - (unify (t, t') + (subTyp (t, t') handle Unify ue => dte (WrongType ("Shared environment variable", (EVar name, loc), @@ -427,12 +467,14 @@ fun checkExp G (eAll as (e, loc)) = in (TAction (p', d', r'), loc) end + | (TError, _) => t2 | _ => (dte (WrongForm ("Action to be sequenced", "action", e2, t2, NONE)); (TError, loc))) + | (TError, _) => t1 | _ => (dte (WrongForm ("Action to be sequenced", "action", e1, @@ -448,6 +490,7 @@ fun checkExp G (eAll as (e, loc)) = case rt of (TAction (p, d, _), _) => (TAction (p, d, SM.empty), loc) + | (TError, _) => rt | _ => (dte (WrongForm ("Body of local action", "action", e, @@ -455,6 +498,43 @@ fun checkExp G (eAll as (e, loc)) = NONE)); (TError, loc)) end + + | EWith (e1, e2) => + let + val t1 = whnorm (checkExp G e1) + val t2 = whnorm (checkExp G e2) + in + case t1 of + (TNested (pd, pr), _) => + (case t2 of + (TAction (p, d, r), _) => + if predImplies (pd, p) then + (TAction (pr, d, r), loc) + else + (dte (WrongPred ("nested action", + pd, + p)); + (TError, loc)) + | (TError, _) => t2 + | _ => + (dte (WrongForm ("Body of nested action", + "action", + e2, + t2, + NONE)); + (TError, loc))) + | (TError, _) => t1 + | _ => + (dte (WrongForm ("Container of nested action", + "action", + e1, + t1, + NONE)); + (TError, loc)) + end + + | ESkip => (TAction ((CPrefix (CRoot, loc), loc), + SM.empty, SM.empty), loc) end exception Ununif @@ -466,6 +546,7 @@ fun ununif (tAll as (t, loc)) = | TArrow (d, r) => (TArrow (ununif d, ununif r), loc) | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc) | TUnif (_, ref (SOME t)) => ununif t + | TNested _ => tAll | TError => tAll | TUnif (_, ref NONE) => raise Ununif @@ -477,6 +558,7 @@ fun hasError (t, _) = | TArrow (d, r) => hasError d orelse hasError r | TAction (p, d, r) => List.exists hasError (SM.listItems d) orelse List.exists hasError (SM.listItems r) + | TNested _ => false | TError => false | TUnif (_, ref (SOME t)) => hasError t | TUnif (_, ref NONE) => false @@ -497,4 +579,28 @@ fun checkUnit G (eAll as (_, loc)) = t) end +fun checkDecl G (d, _, loc) = + case d of + DExternType name => bindType G name + | DExternVal (name, t) => bindVal G (name, checkTyp G t) + +fun checkFile G tInit (ds, eo) = + let + val G' = foldl (fn (d, G) => checkDecl G d) G ds + in + case eo of + NONE => () + | SOME (e as (_, loc)) => + let + val t = checkExp G' e + in + subTyp (t, tInit) + handle Unify ue => + (ErrorMsg.error (SOME loc) "Bad type for final expression of source file."; + preface ("Actual:", p_typ t); + preface ("Needed:", p_typ tInit)) + end; + G' + end + end diff --git a/tests/test.dtl b/tests/test.dtl index 38c1af7..c3c2a19 100644 --- a/tests/test.dtl +++ b/tests/test.dtl @@ -1,8 +1,14 @@ -name <- Name; -Name = (\x : (int) -> "Freddy") name; -let - Name = 17 -in - Name = 13 -end +extern val tweak : int -> [Root]; + +extern val tickle : string -> A => Root; +extern val tackle : [A]; +extern val twitch : int -> [A]; +tweak 42; +Choice = 19; +tickle "yourself" with + tackle; + tackle; + choice <- Choice; + twitch choice +end -- 2.20.1