From 8cbb96323335d1a2b42a9daac94a9d538ab93536 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 11 Nov 2007 17:12:42 +0000 Subject: [PATCH] Type annotations on environment variable reads --- elisp/domtool-mode-startup.el | 2 +- src/ast.sml | 2 +- src/domtool.grm | 3 ++- src/eval.sml | 2 +- src/order.sml | 6 ++++- src/plugins/apache.sig | 3 +++ src/plugins/apache.sml | 50 ++++++++++++++++------------------- src/plugins/easy_domain.sig | 23 ++++++++++++++++ src/plugins/easy_domain.sml | 35 ++++++++++++++++++++++++ src/printFn.sml | 10 ++++--- src/reduce.sml | 10 +++---- src/sources | 3 +++ src/tycheck.sml | 15 ++++++++--- 13 files changed, 121 insertions(+), 43 deletions(-) create mode 100644 src/plugins/easy_domain.sig create mode 100644 src/plugins/easy_domain.sml diff --git a/elisp/domtool-mode-startup.el b/elisp/domtool-mode-startup.el index c00df20..fc63a0e 100644 --- a/elisp/domtool-mode-startup.el +++ b/elisp/domtool-mode-startup.el @@ -1,4 +1,4 @@ (autoload (quote domtool-mode) "domtool-mode/domtool-mode" "\ Major Mode for editing Domtool files." t nil) -(add-to-list (quote auto-mode-alist) (quote ("\\.\\(com\\|net\\|org\\|edu\\|mil\\|biz\\|info\\|name\\|be\\|ca\\|cc\\|de\\|fr\\|in\\|mu\\|se\\|uk\\|us\\|ws\\)$" . domtool-mode))) +(add-to-list (quote auto-mode-alist) (quote ("\\.\\(dtl\\|com\\|net\\|org\\|edu\\|mil\\|biz\\|info\\|name\\|be\\|ca\\|cc\\|de\\|fr\\|in\\|mu\\|se\\|uk\\|us\\|ws\\)$" . domtool-mode))) diff --git a/src/ast.sml b/src/ast.sml index 0e8688d..ead8531 100644 --- a/src/ast.sml +++ b/src/ast.sml @@ -80,7 +80,7 @@ datatype exp' = (* Do-nothing action *) | ESet of string * exp (* Set an environment variable *) - | EGet of string * string * exp + | EGet of string * typ option * string * exp (* Get an environment variable *) | ESeq of exp list (* Monad sequencer; execute a number of commands in order *) diff --git a/src/domtool.grm b/src/domtool.grm index 3bbc578..532dad9 100644 --- a/src/domtool.grm +++ b/src/domtool.grm @@ -126,7 +126,8 @@ exp : apps (apps) (ESeq ls, (exp1left, exp2right)) end) | exp SEMI (exp) - | SYMBOL LARROW CSYMBOL SEMI exp (EGet (SYMBOL, CSYMBOL, exp), (SYMBOLleft, expright)) + | SYMBOL LARROW CSYMBOL SEMI exp (EGet (SYMBOL, NONE, CSYMBOL, exp), (SYMBOLleft, expright)) + | SYMBOL COLON typ LARROW CSYMBOL SEMI exp (EGet (SYMBOL, SOME typ, CSYMBOL, exp), (SYMBOLleft, expright)) apps : term (term) | apps term (EApp (apps, term), (appsleft, termright)) diff --git a/src/eval.sml b/src/eval.sml index 0cabf34..8789eac 100644 --- a/src/eval.sml +++ b/src/eval.sml @@ -60,7 +60,7 @@ fun exec' evs (eAll as (e, _)) = case e of ESkip => SM.empty | ESet (ev, e) => SM.insert (SM.empty, ev, e) - | EGet (x, ev, e) => exec' evs (Reduce.subst x (lookup (evs, ev)) e) + | EGet (x, _, ev, e) => exec' evs (Reduce.subst x (lookup (evs, ev)) e) | ESeq es => let val (new, _) = diff --git a/src/order.sml b/src/order.sml index 2923c19..422856d 100644 --- a/src/order.sml +++ b/src/order.sml @@ -111,7 +111,11 @@ fun expNeeded G (e, loc) = | ESkip => empty | ESet (_, e) => expNeeded G e - | EGet (x, _, e) => expNeeded (Env.bindVal G (x, dt, NONE)) e + | EGet (x, topt, _, e) => + (case topt of + NONE => expNeeded (Env.bindVal G (x, dt, NONE)) e + | SOME t => unionCTE ((typNeeded G t, SS.empty), + expNeeded (Env.bindVal G (x, dt, NONE)) e)) | ESeq es => foldl (fn (e, ss) => unionCTE (ss, expNeeded G e)) empty es | ELocal (e1, e2) => unionCTE (expNeeded G e1, expNeeded G e2) diff --git a/src/plugins/apache.sig b/src/plugins/apache.sig index a92edcf..2cc2eb5 100644 --- a/src/plugins/apache.sig +++ b/src/plugins/apache.sig @@ -31,4 +31,7 @@ signature APACHE = sig val logDir : {user : string, node : string, vhostId : string} -> string (* Where is a vhost's log directory located? *) + + val defaults : (string * Ast.typ * (unit -> Ast.exp)) list + (* Default environment variables *) end diff --git a/src/plugins/apache.sml b/src/plugins/apache.sml index 54df3d5..64ebc7b 100644 --- a/src/plugins/apache.sml +++ b/src/plugins/apache.sml @@ -89,33 +89,29 @@ fun ssl e = case e of val dl = ErrorMsg.dummyLoc -val _ = Defaults.registerDefault ("WebNodes", - (TList (TBase "web_node", dl), dl), - (fn () => (EList (map (fn s => (EString s, dl)) Config.Apache.webNodes_default), dl))) - -val _ = Defaults.registerDefault ("SSL", - (TBase "ssl", dl), - (fn () => (EVar "no_ssl", dl))) - -val _ = Defaults.registerDefault ("User", - (TBase "your_user", dl), - (fn () => (EString (Domain.getUser ()), dl))) - -val _ = Defaults.registerDefault ("Group", - (TBase "your_group", dl), - (fn () => (EString "nogroup", dl))) - -val _ = Defaults.registerDefault ("DocumentRoot", - (TBase "your_path", dl), - (fn () => (EString (Domain.homedir () ^ "/" ^ Config.Apache.public_html), dl))) - -val _ = Defaults.registerDefault ("ServerAdmin", - (TBase "email", dl), - (fn () => (EString (Domain.getUser () ^ "@" ^ Config.defaultDomain), dl))) - -val _ = Defaults.registerDefault ("SuExec", - (TBase "suexec_flag", dl), - (fn () => (EVar "true", dl))) +val defaults = [("WebNodes", + (TList (TBase "web_node", dl), dl), + (fn () => (EList (map (fn s => (EString s, dl)) Config.Apache.webNodes_default), dl))), + ("SSL", + (TBase "ssl", dl), + (fn () => (EVar "no_ssl", dl))), + ("User", + (TBase "your_user", dl), + (fn () => (EString (Domain.getUser ()), dl))), + ("Group", + (TBase "your_group", dl), + (fn () => (EString "nogroup", dl))), + ("DocumentRoot", + (TBase "your_path", dl), + (fn () => (EString (Domain.homedir () ^ "/" ^ Config.Apache.public_html), dl))), + ("ServerAdmin", + (TBase "email", dl), + (fn () => (EString (Domain.getUser () ^ "@" ^ Config.defaultDomain), dl))), + ("SuExec", + (TBase "suexec_flag", dl), + (fn () => (EVar "true", dl)))] + +val () = app Defaults.registerDefault defaults val redirect_code = fn (EVar "temp", _) => SOME "temp" | (EVar "permanent", _) => SOME "permanent" diff --git a/src/plugins/easy_domain.sig b/src/plugins/easy_domain.sig new file mode 100644 index 0000000..048cab8 --- /dev/null +++ b/src/plugins/easy_domain.sig @@ -0,0 +1,23 @@ +(* 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. + *) + +(* Derived directives of general use *) + +signature EASY_DOMAIN = sig + +end diff --git a/src/plugins/easy_domain.sml b/src/plugins/easy_domain.sml new file mode 100644 index 0000000..dd8d71b --- /dev/null +++ b/src/plugins/easy_domain.sml @@ -0,0 +1,35 @@ +(* HCoop Domtool (http://hcoop.sourceforge.net/) + * Copyright (c) 2007, 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. + *) + +(* Derived directives of general use *) + +structure EasyDomain :> EASY_DOMAIN = struct + +open Ast + +val dl = ErrorMsg.dummyLoc + +val _ = Defaults.registerDefault ("WWW", + (TAction ((CConst "Vhost", dl), + foldl (fn ((v, t, _), r) => + StringMap.insert (r, v, t)) + StringMap.empty Apache.defaults, + StringMap.empty), dl), + (fn () => (ESkip, dl))) + +end diff --git a/src/printFn.sml b/src/printFn.sml index 871c1df..05172da 100644 --- a/src/printFn.sml +++ b/src/printFn.sml @@ -115,9 +115,13 @@ fun p_exp' pn (e, _) = | ESkip => keyword "_" | ESet (x, e) => parenIf pn [exp x, space 1, punct "=", space 1, p_exp e] - | EGet (x1, x2, e) => parenIf pn [dBox [exp x1, space 1, punct "<-", - space 1, exp x2, punct ";", space 1], - p_exp e] + | EGet (x1, NONE, x2, e) => parenIf pn [dBox [exp x1, space 1, punct "<-", + space 1, exp x2, punct ";", space 1], + p_exp e] + | EGet (x1, SOME t, x2, e) => parenIf pn [dBox [exp x1, space 1, punct ":", space 1, p_typ t, + space 1, punct "<-", + space 1, exp x2, punct ";", space 1], + p_exp e] | ESeq es => parenIf pn (valOf (foldr (fn (e, NONE) => SOME [p_exp e] | (e, SOME ds) => SOME (dBox [p_exp e, punct ";", newline] :: ds)) NONE es)) diff --git a/src/reduce.sml b/src/reduce.sml index ab6dafa..5d7a1b9 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -36,7 +36,7 @@ fun freeIn x (b, _) = | ESkip => false | ESet (_, e) => freeIn x e - | EGet (x', _, b') => x <> x' andalso freeIn x b' + | EGet (x', _, _, b') => x <> x' andalso freeIn x b' | ESeq es => List.exists (freeIn x) es | ELocal (e1, e2) => freeIn x e1 orelse freeIn x e2 | EWith (e1, e2) => freeIn x e1 orelse freeIn x e2 @@ -80,17 +80,17 @@ fun subst x e (bAll as (b, loc)) = | ESkip => bAll | ESet (v, b) => (ESet (v, subst x e b), loc) - | EGet (x', v, b') => + | EGet (x', topt, v, b') => if x = x' then bAll else if freeIn x' e then let val x'' = freshVar () in - (EGet (x'', v, subst x e (subst x' (EVar x'', loc) b')), loc) + (EGet (x'', topt, v, subst x e (subst x' (EVar x'', loc) b')), loc) end else - (EGet (x', v, subst x e b'), loc) + (EGet (x', topt, v, subst x e b'), loc) | ESeq es => (ESeq (map (subst x e) es), loc) | ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc) | EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc) @@ -155,7 +155,7 @@ fun reduceExp G (eAll as (e, loc)) = | ESkip => eAll | ESet (v, b) => (ESet (v, reduceExp G b), loc) - | EGet (x, v, b) => (EGet (x, v, reduceExp G b), loc) + | EGet (x, topt, v, b) => (EGet (x, topt, v, reduceExp G b), loc) | ESeq es => (ESeq (map (reduceExp G) es), loc) | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc) | EWith (e1, e2) => diff --git a/src/sources b/src/sources index 3b129fd..eece575 100644 --- a/src/sources +++ b/src/sources @@ -112,6 +112,9 @@ plugins/socketPerm.sml plugins/firewall.sig plugins/firewall.sml +plugins/easy_domain.sig +plugins/easy_domain.sml + mail/vmail.sig mail/vmail.sml diff --git a/src/tycheck.sml b/src/tycheck.sml index e2feb90..8889540 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -248,7 +248,7 @@ fun envVarSetFrom v (e, _) = SOME e else NONE - | EGet (_, _, e) => envVarSetFrom v e + | EGet (_, _, _, e) => envVarSetFrom v e | ESeq es => foldr (fn (e, found) => case found of SOME _ => found @@ -258,6 +258,11 @@ fun envVarSetFrom v (e, _) = | _ => NONE +fun ununify (tAll as (t, _)) = + case t of + TUnif (_, ref (SOME t)) => ununify t + | _ => tAll + fun checkExp G (eAll as (e, loc)) = let val dte = Describe.describe_type_error loc @@ -357,14 +362,18 @@ fun checkExp G (eAll as (e, loc)) = SM.insert (SM.empty, evar, t)), loc) end - | EGet (x, evar, rest) => + | EGet (x, topt, evar, rest) => let val xt = (newUnif (), loc) val G' = bindVal G (x, xt, NONE) val rt = whnorm (checkExp G' rest) in - case rt of + case topt of + NONE => () + | SOME t => subTyp (xt, checkTyp G t); + + case ununify rt of (TAction (p, d, r), _) => (case SM.find (d, evar) of NONE => (TAction (p, SM.insert (d, evar, xt), r), loc) -- 2.20.1