From 1a4e5a6c9a8fbbdc980cf0661c444ddc2910544a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 30 Jul 2006 00:33:53 +0000 Subject: [PATCH] Domains example --- src/ast.sml | 8 ++--- src/domtool.grm | 38 ++++++++++++++++---- src/domtool.lex | 1 + src/print.sml | 15 ++++---- src/tycheck.sml | 94 ++++++++++++++++++++++++++++++++++++++---------- tests/domain.dtl | 36 +++++++++++++++++++ 6 files changed, 154 insertions(+), 38 deletions(-) create mode 100644 tests/domain.dtl diff --git a/src/ast.sml b/src/ast.sml index b48f13e..0c6ddd1 100644 --- a/src/ast.sml +++ b/src/ast.sml @@ -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 diff --git a/src/domtool.grm b/src/domtool.grm index 4b8405f..349ab7a 100644 --- a/src/domtool.grm +++ b/src/domtool.grm @@ -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) diff --git a/src/domtool.lex b/src/domtool.lex index 66d0185..6bf3475 100644 --- a/src/domtool.lex +++ b/src/domtool.lex @@ -126,6 +126,7 @@ lineComment = #[^\n]*\n; "in" => (Tokens.IN (yypos, yypos + size yytext)); "end" => (Tokens.END (yypos, yypos + size yytext)); "with" => (Tokens.WITH (yypos, yypos + size yytext)); + "where" => (Tokens.WHERE (yypos, yypos + size yytext)); "extern" => (Tokens.EXTERN (yypos, yypos + size yytext)); "type" => (Tokens.TYPE (yypos, yypos + size yytext)); diff --git a/src/print.sml b/src/print.sml index 4acf9f1..4b497bd 100644 --- a/src/print.sml +++ b/src/print.sml @@ -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 "" | 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"] diff --git a/src/tycheck.sml b/src/tycheck.sml index 854b575..5ce94c8 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -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 index 0000000..39f2f78 --- /dev/null +++ b/tests/domain.dtl @@ -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 -- 2.20.1