From: Adam Chlipala Date: Sun, 30 Jul 2006 19:30:35 +0000 (+0000) Subject: Evaluating a test with automatic inclusion of basis X-Git-Tag: release_2010-11-19~378 X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/commitdiff_plain/d189ec0eee8569e5811335e7fc93a921e14c2b1f?hp=095de39e1be653dcb6438d19c719bd7797e0772a Evaluating a test with automatic inclusion of basis --- diff --git a/configDefault/domtool.cfg b/configDefault/domtool.cfg index 1f9f8fe..79fab00 100644 --- a/configDefault/domtool.cfg +++ b/configDefault/domtool.cfg @@ -1,2 +1,2 @@ -val configRoot = "/home/adamc/cvs/domtool2/lib" +val libRoot = "/home/adamc/cvs/domtool2/lib" val resultRoot = "/home/adamc/domtool" diff --git a/configDefault/domtool.cfs b/configDefault/domtool.cfs index 7d24e60..f8a2aec 100644 --- a/configDefault/domtool.cfs +++ b/configDefault/domtool.cfs @@ -1,7 +1,7 @@ -val configRoot : string -(* Root directory for a directory hierarchy corresponding to domain structure, - * where each node contains files related to that domain's configuration. *) +val libRoot : string +(* Basis library root directory *) val resultRoot : string (* Root directory for a directory hierarchy corresponding to domain structure, * where each node contains Domtool-generated result files for that domain. *) + diff --git a/lib/alias.dtl b/lib/alias.dtl index 0ced362..c591aaf 100644 --- a/lib/alias.dtl +++ b/lib/alias.dtl @@ -29,7 +29,7 @@ extern val dropTarget : aliasTarget; {{Silently delete all mail to the associated source.}} extern val aliasPrim : aliasSource -> aliasTarget -> [Domain]; -{{Request redirection of all mail from the source to the target.} +{{Request redirection of all mail from the source to the target.}} val alias = \user -> \email -> aliasPrim (userSource user) (addressTarget email); {{Redirect mail for the user at the current domain to the e-mail address.}} @@ -41,7 +41,7 @@ val aliasDrop = \user -> aliasPrim (userSource user) dropTarget; val defaultAlias = \email -> aliasPrim defaultSource (addressTarget email); {{When a message to the current domain doesn't match any other alias, and it - doesn't match any systemwide username, send it to this e-mail address + doesn't match any systemwide username, send it to this e-mail address.}} val catchAllAlias = \email -> aliasPrim catchAllSource (addressTarget email); {{When a message to the current domain doesn't match any other alias, send it to this e-mail address, even if it matches a systemwide username.}} diff --git a/src/main.sig b/src/main.sig index 46aedfb..45510b7 100644 --- a/src/main.sig +++ b/src/main.sig @@ -22,8 +22,12 @@ signature MAIN = sig val tInit : Ast.typ - val check : string -> unit - val reduce : string -> unit + val check : string -> Env.env * Ast.exp option + val check' : Env.env -> string -> Env.env + + val basis : unit -> Env.env + + val reduce : string -> Ast.exp option val eval : string -> unit end diff --git a/src/main.sml b/src/main.sml index e00562a..86da95f 100644 --- a/src/main.sml +++ b/src/main.sml @@ -28,73 +28,91 @@ val tInit = (TAction ((CRoot, dmy), StringMap.empty, StringMap.empty), dmy) + + -fun check fname = +fun check' G fname = let + (*val _ = print ("Check " ^ fname ^ "\n")*) val prog = Parse.parse fname in if !ErrorMsg.anyErrors then - () + G else - let - val G' = Tycheck.checkFile Env.empty tInit prog - in - () - end + Tycheck.checkFile G tInit prog end -fun reduce fname = +fun basis () = let - val prog = Parse.parse fname + val dir = Posix.FileSys.opendir Config.libRoot + + fun loop files = + case Posix.FileSys.readdir dir of + NONE => files + | SOME fname => + if String.isSuffix ".dtl" fname then + loop (String.concatWith "/" [Config.libRoot, fname] + :: files) + else + loop files + + val files = loop [] + val files = Order.order files + in + foldl (fn (fname, G) => check' G fname) Env.empty files + end + +fun check fname = + let + val _ = ErrorMsg.reset () + + val b = basis () in if !ErrorMsg.anyErrors then - () + (b, NONE) else let - val G' = Tycheck.checkFile Env.empty tInit prog + val prog = Parse.parse fname in if !ErrorMsg.anyErrors then - () + (Env.empty, NONE) else - case prog of - (_, _, SOME body) => - let - val body' = Reduce.reduceExp G' body - in - printd (PD.hovBox (PD.PPS.Rel 0, - [PD.string "Result:", - PD.space 1, - p_exp body'])) - end - | _ => () + let + val G' = Tycheck.checkFile b tInit prog + in + (G', #3 prog) + end end end -fun eval fname = +fun reduce fname = let - val prog = Parse.parse fname + val (G, body) = check fname in if !ErrorMsg.anyErrors then - () + NONE else - let - val G' = Tycheck.checkFile Env.empty tInit prog - in - if !ErrorMsg.anyErrors then - () - else - case prog of - (_, _, SOME body) => - let - val body' = Reduce.reduceExp G' body - in - if !ErrorMsg.anyErrors then - () - else - Eval.exec StringMap.empty body' - end - | _ => () - end + case body of + SOME body => + let + val body' = Reduce.reduceExp G body + in + (*printd (PD.hovBox (PD.PPS.Rel 0, + [PD.string "Result:", + PD.space 1, + p_exp body']))*) + SOME body' + end + | _ => NONE end +fun eval fname = + case reduce fname of + (SOME body') => + if !ErrorMsg.anyErrors then + () + else + Eval.exec StringMap.empty body' + | NONE => () + end diff --git a/tests/domain2.dtl b/tests/domain2.dtl dissimilarity index 83% index 520abd1..75ffec8 100644 --- a/tests/domain2.dtl +++ b/tests/domain2.dtl @@ -1,33 +1,8 @@ -extern type domain; -extern val domain : domain -> Domain => [Root]; - -extern type emailUser; -extern type email; - -extern type aliasSource; -extern val userSource : emailUser -> aliasSource; -extern val defaultSource : aliasSource; -extern val catchAllSource : aliasSource; - -extern type aliasTarget; -extern val addressTarget : email -> aliasTarget; -extern val addressesTarget : [email] -> aliasTarget; -extern val dropTarget : aliasTarget; - -extern val aliasPrim : aliasSource -> aliasTarget -> [Domain]; - -val alias = \user -> \email -> aliasPrim (userSource user) (addressTarget email); -val aliasMulti = \user -> \emails -> aliasPrim (userSource user) (addressesTarget emails); -val aliasDrop = \user -> aliasPrim (userSource user) dropTarget; - -val defaultAlias = \email -> aliasPrim defaultSource (addressTarget email); -val catchAllAlias = \email -> aliasPrim catchAllSource (addressTarget email); - -domain "hcoop.net" with - alias "schmeppo" "dlonker"; - aliasMulti "me" ["nowhere","smelly@yikes"]; - aliasDrop "yippo"; - - defaultAlias "billy"; - catchAllAlias "bonkers" -end +domain "hcoop.net" with + alias "schmeppo" "dlonker"; + aliasMulti "me" ["nowhere","smelly@yikes"]; + aliasDrop "yippo"; + + defaultAlias "billy"; + catchAllAlias "bonkers" +end diff --git a/tests/testAlias.dtl b/tests/testAlias.dtl new file mode 100644 index 0000000..75ffec8 --- /dev/null +++ b/tests/testAlias.dtl @@ -0,0 +1,8 @@ +domain "hcoop.net" with + alias "schmeppo" "dlonker"; + aliasMulti "me" ["nowhere","smelly@yikes"]; + aliasDrop "yippo"; + + defaultAlias "billy"; + catchAllAlias "bonkers" +end