* - 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. *)
(* 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
| 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
| 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
%right ARROW DARROW
%right COMMA
%nonassoc EQ
+%right WITH
+%right WHERE
%right AND
%nonassoc CARET BANG
| 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))
(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))
| 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)
| 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)
<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));
| 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
| 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"]
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)
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
| (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)) =
(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
| 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'
| (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)
| 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
(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,
--- /dev/null
+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