Type-checking goodies in place

diff --git a/src/ast.sml b/src/ast.sml
index e62c8fb..b48f13e 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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());
 <STRING> .            => (str := String.sub (yytext, 0) :: !str; continue());
 
+<INITIAL> "{{"        => (YYBEGIN DOC; strStart := yypos; str := []; continue());
+<DOC> "}}"            => (YYBEGIN INITIAL;
+                         Tokens.DOC (String.implode (List.rev (!str)), !strStart, yypos + 1));
+<DOC> "\n"            => (lineNum := !lineNum + 1;
+                         linePos := yypos :: ! linePos;
+                         str := #"\n" :: !str; continue());
+<DOC> .               => (str := String.sub (yytext, 0) :: !str; continue());
+
 <INITIAL> "("         => (Tokens.LPAREN (yypos, yypos + size yytext));
 <INITIAL> ")"         => (Tokens.RPAREN (yypos, yypos + size yytext));
 
@@ -117,6 +125,11 @@ lineComment = #[^\n]*\n;
 <INITIAL> "let"       => (Tokens.LET (yypos, yypos + size yytext));
 <INITIAL> "in"        => (Tokens.IN (yypos, yypos + size yytext));
 <INITIAL> "end"       => (Tokens.END (yypos, yypos + size yytext));
+<INITIAL> "with"      => (Tokens.WITH (yypos, yypos + size yytext));
+
+<INITIAL> "extern"    => (Tokens.EXTERN (yypos, yypos + size yytext));
+<INITIAL> "type"      => (Tokens.TYPE (yypos, yypos + size yytext));
+<INITIAL> "val"       => (Tokens.VAL (yypos, yypos + size yytext));
 
 <INITIAL> "Root"      => (Tokens.ROOT (yypos, yypos + size yytext));
 

diff --git a/src/main.sig b/src/main.sig
new file mode 100644 (file)
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 (file)
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 (file)
--- 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 (file)
--- 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 "<error>"
       | 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 (file)
--- 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 (file)
--- 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 (file)
--- 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