Domains example
authorAdam Chlipala <adamc@hcoop.net>
Sun, 30 Jul 2006 00:33:53 +0000 (00:33 +0000)
committerAdam Chlipala <adamc@hcoop.net>
Sun, 30 Jul 2006 00:33:53 +0000 (00:33 +0000)
src/ast.sml
src/domtool.grm
src/domtool.lex
src/print.sml
src/tycheck.sml
tests/domain.dtl [new file with mode: 0644]

index b48f13e..0c6ddd1 100644 (file)
@@ -48,7 +48,7 @@ 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
+       | TNested of pred * typ
        (* 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. *)
@@ -84,9 +84,9 @@ datatype exp' =
        (* Get an environment variable *)
        | ESeq of exp list
        (* Monad sequencer; execute a number of commands in order *)
-       | ELocal of exp
-       (* Local execution; execute the action and then restore the previous
-       * environment. *)
+       | ELocal of exp * exp
+       (* Local execution; like ESeq, but the writes of the first
+       * action are abandoned *)
        | EWith of exp * exp
        (* Apply a TNested to an action *)
 withtype exp = exp' * position
index 4b8405f..349ab7a 100644 (file)
@@ -33,7 +33,7 @@ open Ast
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | BSLASH | SEMI | LET | IN | END
  | ROOT
- | EXTERN | TYPE | VAL | WITH
+ | EXTERN | TYPE | VAL | WITH | WHERE
 
 %nonterm 
    file of file
@@ -45,6 +45,7 @@ open Ast
  | exp of exp
  | apps of exp
  | term of exp
+ | sets of exp list
  | elist of exp list
  | elistNe of exp list
  | clist of exp list
@@ -68,6 +69,8 @@ open Ast
 %right ARROW DARROW
 %right COMMA
 %nonassoc EQ
+%right WITH
+%right WHERE
 %right AND
 %nonassoc CARET BANG
 
@@ -87,10 +90,24 @@ docOpt :                                   (NONE)
        | DOC                               (SOME DOC)
 
 expOpt :                                   (NONE)
-       | exp                               (SOME (ELocal exp, (expleft, expright)))
+       | exp                               (SOME (ELocal (exp, (ESkip, (expleft, expright))),
+                                                 (expleft, expright)))
 
 
 exp    : apps                              (apps)
+       | apps WHERE sets END               (ELocal ((ESeq sets, (setsleft, setsright)), apps),
+                                           (appsleft, ENDright))
+       | apps WITH END                     (EWith (apps, (ESkip, (WITHleft, ENDright))),
+                                           (appsleft, ENDright))
+       | apps WITH exp END                 (EWith (apps, exp), (appsleft, ENDright))
+       | apps WHERE sets WITH END          (ELocal ((ESeq sets, (setsleft, setsright)),
+                                                   (EWith (apps, (ESkip, (WITHleft, ENDright))),
+                                                    (appsleft, ENDright))),
+                                           (appsleft, ENDright))
+       | apps WHERE sets WITH exp END      (ELocal ((ESeq sets, (setsleft, setsright)),
+                                                   (EWith (apps, exp), (appsleft, ENDright))),
+                                           (appsleft, ENDright))
+
        | BSLASH SYMBOL COLON LPAREN typ RPAREN ARROW exp (ELam (SYMBOL, SOME typ, exp),
                                                          (BSLASHleft, expright))
        | BSLASH SYMBOL ARROW exp           (ELam (SYMBOL, NONE, exp), (BSLASHleft, expright))
@@ -103,8 +120,12 @@ exp    : apps                              (apps)
                                                (ESeq ls, (exp1left, exp2right))
                                            end)
        | 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))
+       (*| exp WHERE exp END                 (ELocal (exp1, exp2), (exp1left, ENDright))
+       | exp WHERE exp WITH END            (EWith ((ELocal (exp1, exp2), (exp1left, ENDright)),
+                                                  (ESkip, (WITHleft, ENDright))),
+                                           (exp1left, ENDright))
+       | exp WITH END                      (EWith (exp, (ESkip, (WITHleft, ENDright))), (expleft, ENDright))
+       | exp WITH exp END                  (EWith (exp1, exp2), (exp1left, ENDright))*)
 
 apps   : term                              (term)
        | apps term                         (EApp (apps, term), (appsleft, termright))
@@ -113,10 +134,13 @@ term   : LPAREN exp RPAREN                 (exp)
        | INT                               (EInt INT, (INTleft, INTright))
        | STRING                            (EString STRING, (STRINGleft, STRINGright))
        | LBRACK elist RBRACK               (EList elist, (LBRACKleft, RBRACKright))
-       | LET exp IN exp END                (ELocal (ESeq [exp1, exp2], (LETleft, ENDright)),
-                                                   (LETleft, ENDright))
+       | LET exp IN exp END                (ELocal (exp1, exp2), (LETleft, ENDright))
        | SYMBOL                            (EVar SYMBOL, (SYMBOLleft, SYMBOLright))
 
+sets   : CSYMBOL EQ apps                   ([(ESet (CSYMBOL, apps), (CSYMBOLleft, appsright))])
+       | CSYMBOL EQ apps SEMI sets         ((ESet (CSYMBOL, apps), (CSYMBOLleft, appsright))
+                                           :: sets)
+
 elist  :                                   ([])
        | elistNe                           (elistNe)
 
@@ -132,7 +156,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))
+       | ctxt DARROW typ                   (TNested (ctxt, typ), (ctxtleft, typright))
 
 recd   : LBRACE RBRACE                     (StringMap.empty)
        | LBRACE recdNe RBRACE              (recdNe)
index 66d0185..6bf3475 100644 (file)
@@ -126,6 +126,7 @@ lineComment = #[^\n]*\n;
 <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> "where"     => (Tokens.WHERE (yypos, yypos + size yytext));
 
 <INITIAL> "extern"    => (Tokens.EXTERN (yypos, yypos + size yytext));
 <INITIAL> "type"      => (Tokens.TYPE (yypos, yypos + size yytext));
index 4acf9f1..4b497bd 100644 (file)
@@ -59,8 +59,8 @@ fun p_typ' pn (t, _) =
       | TAction (p, r1, r2) =>
        parenIf pn [p_predBoxed p, space 1, p_record r1, space 1,
                    string "=>", space 1, p_record r2]
-      | TNested (p1, p2) =>
-       parenIf pn [p_pred' false p1, space 1, string "=>", space 1, p_pred' false p2]
+      | TNested (p, t) =>
+       parenIf pn [p_pred' false p, space 1, string "=>", space 1, p_typ' false t]
 
       | TError => string "<error>"
       | TUnif (_, ref (SOME t)) => p_typ' pn t
@@ -111,12 +111,11 @@ fun p_exp (e, _) =
       | ESeq es => dBox (valOf (foldr (fn (e, NONE) => SOME [p_exp e]
                                        | (e, SOME ds) => SOME (dBox [p_exp e, string ";", space 1] :: ds))
                                      NONE es))
-      | ELocal (ESeq [e1, e2], _) => dBox [string "let", space 1,
-                                          p_exp e1, space 1,
-                                          string "in", space 1,
-                                          p_exp e2, space 1,
-                                          string "end"]
-      | ELocal e => dBox [string "local(", space 1, p_exp e, string ")"]
+      | ELocal (e1, e2) => dBox [string "let", space 1,
+                                p_exp e1, space 1,
+                                string "in", space 1,
+                                p_exp e2, space 1,
+                                string "end"]
       | 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"]
 
index 854b575..5ce94c8 100644 (file)
@@ -99,7 +99,7 @@ fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
        andalso eqRecord eqTy (r1, r2)
 
       | (TNested (p1, q1), TNested (p2, q2)) =>
-       eqPred (p1, p2) andalso eqPred (q1, q2)
+       eqPred (p1, p2) andalso eqTy (q1, q2)
 
       | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
       | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
@@ -170,7 +170,10 @@ fun describe_type_error loc te =
 
 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
     case (p1, p2) of
-       (_, CPrefix (CRoot, _)) => true
+       (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
+      | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
+
+      | (_, CPrefix (CRoot, _)) => true
       | (CNot (CPrefix (CRoot, _), _), _) => true
 
       | (CRoot, CRoot) => true
@@ -182,9 +185,6 @@ fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
 
       | (CNot p1, CNot p2) => predImplies (p2, p1)
 
-      | (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
-      | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
-
       | _ => false
 
 fun predSimpl (pAll as (p, loc)) =
@@ -202,6 +202,8 @@ fun predSimpl (pAll as (p, loc)) =
                (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
              | _ => if predImplies (p2', p1') then
                         p2'
+                    else if predImplies (p1', p2') then
+                        p1'
                     else
                         (CAnd (p1', p2'), loc)
        end
@@ -226,7 +228,7 @@ fun occurs u (t, _) =
       | TAction (_, d, r) =>
        List.exists (occurs u) (SM.listItems d)
        orelse List.exists (occurs u) (SM.listItems r)
-      | TNested _ => false
+      | TNested (_, t) => occurs u t
       | TError => false
       | TUnif (_, ref (SOME t)) => occurs u t
       | TUnif (_, u') => u = u'
@@ -252,7 +254,7 @@ fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
 
       | (TNested (d1, r1), TNested (d2, r2)) =>
        (subPred (d2, d1);
-        subPred (r1, r2))
+        subTyp (r1, r2))
 
       | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
       | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
@@ -305,7 +307,7 @@ fun checkTyp G (tAll as (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
+         | TNested (p, t) => (TNested (p, checkTyp G t), loc)
          | TError => raise Fail "TError in parser-generated type"
          | TUnif _ => raise Fail "TUnif in parser-generated type"
     end
@@ -483,33 +485,87 @@ fun checkExp G (eAll as (e, loc)) =
                          (TError, loc))
            end
 
-         | ELocal e =>
+         | ELocal (e1, e2) =>
            let
-               val rt = whnorm (checkExp G e)
+               val t1 = whnorm (checkExp G e1)
+               val t2 = whnorm (checkExp G e2)
            in
-               case rt of
-                   (TAction (p, d, _), _) =>
-                   (TAction (p, d, SM.empty), loc)
-                 | (TError, _) => rt
-                 | _ => (dte (WrongForm ("Body of local action",
+               case t1 of
+                   (TAction (p1, d1, r1), _) =>
+                   (case t2 of
+                        (TAction (p2, d2, r2), _) =>
+                        let
+                            val p' = predSimpl (CAnd (p1, p2), loc)
+
+                            val d' = SM.foldli (fn (name, t, d') =>
+                                                   case SM.find (r1, name) of
+                                                       NONE =>
+                                                       (case SM.find (d', name) of
+                                                            NONE => SM.insert (d', name, t)
+                                                          | SOME t' =>
+                                                            (subTyp (t, t')
+                                                             handle Unify ue =>
+                                                                    dte (WrongType ("Shared environment variable",
+                                                                                    (EVar name, loc),
+                                                                                    t,
+                                                                                    t',
+                                                                                    SOME ue));
+                                                             d'))
+                                                     | SOME t' =>
+                                                       (subTyp (t, t')
+                                                        handle Unify ue =>
+                                                               dte (WrongType ("Shared environment variable",
+                                                                               (EVar name, loc),
+                                                                               t,
+                                                                               t',
+                                                                               SOME ue));
+                                                        d'))
+                                               d1 d2
+                        in
+                            (TAction (p', d', r2), 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",
-                                         e,
-                                         rt,
+                                         e1,
+                                         t1,
                                          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), _) =>
+                   (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
                    (case t2 of
                         (TAction (p, d, r), _) =>
                         if predImplies (pd, p) then
-                            (TAction (pr, d, r), loc)
+                            let
+                                val combineRecs =
+                                    SM.unionWithi (fn (name, t1, t2) =>
+                                                      (subTyp (t1, t2)
+                                                       handle Unify ue =>
+                                                              dte (WrongType ("Environment variable",
+                                                                              (EVar name, loc),
+                                                                              t1,
+                                                                              t2,
+                                                                              SOME ue));
+                                                       t2))
+                            in
+                                (TAction (pr, combineRecs (d, d1),
+                                          combineRecs (r, r1)), loc)
+                            end
                         else
                             (dte (WrongPred ("nested action",
                                              pd,
diff --git a/tests/domain.dtl b/tests/domain.dtl
new file mode 100644 (file)
index 0000000..39f2f78
--- /dev/null
@@ -0,0 +1,36 @@
+extern val domain : string -> Domain => [Root];
+
+extern val host : string -> string -> [Domain];
+
+extern val vhost : string -> Vhost => [Domain] {DocRoot : string};
+
+extern val directory : string -> ^Vhost & Directory => [Vhost];
+
+extern val ssi : [^Vhost];
+extern val fancy : [Directory];
+extern val risky : [Vhost];
+
+domain "hcoop.net" with
+       host "frumpkin" "1.2.3.4";
+       host "bumpkin" "1.2.3.5";
+
+       vhost "www" where
+               DocRoot = "/home/boopie"
+       with
+               risky
+       end;
+
+       DocRoot = "/etc/default";
+
+       vhost "smelly" with
+               directory "/etc/default/here" with
+                       ssi;
+                       fancy
+               end;
+               ssi
+       end;
+
+       vhost "rank" with
+               ssi
+       end
+end