From e1b99e23f8d30efc7842ee006e0ff3ef0347b7df Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 26 May 2007 16:11:32 +0000 Subject: [PATCH] Factor error message generation into a separate file; add '-tc' flag to domtool-client --- src/ast.sml | 13 +++++ src/describe.sig | 26 +++++++++ src/describe.sml | 125 ++++++++++++++++++++++++++++++++++++++++++++ src/main-client.sml | 13 +++-- src/main.sig | 1 + src/main.sml | 14 +++-- src/sources | 3 ++ src/tycheck.sml | 71 +++---------------------- 8 files changed, 195 insertions(+), 71 deletions(-) create mode 100644 src/describe.sig create mode 100644 src/describe.sml diff --git a/src/ast.sml b/src/ast.sml index ba00f78..0e8688d 100644 --- a/src/ast.sml +++ b/src/ast.sml @@ -105,4 +105,17 @@ type file = string option * decl list * exp option fun multiApp (f, loc, args) = foldl (fn (arg, e) => (EApp (e, arg), loc)) f args +datatype unification_error = + UnifyPred of pred * pred + | UnifyTyp of typ * typ + | UnifyOccurs of string * typ + +exception Unify of unification_error + +datatype type_error = + WrongType of string * exp * typ * typ * unification_error option + | WrongForm of string * string * exp * typ * unification_error option + | UnboundVariable of string + | WrongPred of string * pred * pred + end diff --git a/src/describe.sig b/src/describe.sig new file mode 100644 index 0000000..43be39a --- /dev/null +++ b/src/describe.sig @@ -0,0 +1,26 @@ +(* HCoop Domtool (http://hcoop.sourceforge.net/) + * Copyright (c) 2006-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. + *) + +(* Error message generation *) + +signature DESCRIBE = sig + + val describe_unification_error : Ast.typ -> Ast.unification_error -> unit + + val describe_type_error : Ast.position -> Ast.type_error -> unit +end diff --git a/src/describe.sml b/src/describe.sml new file mode 100644 index 0000000..a39faeb --- /dev/null +++ b/src/describe.sml @@ -0,0 +1,125 @@ +(* HCoop Domtool (http://hcoop.sourceforge.net/) + * Copyright (c) 2006-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. + *) + +(* Error message generation *) + +structure Describe :> DESCRIBE = struct + +open Ast Print + +structure SM = StringMap + +exception UnequalDomains + +fun eqRecord f (r1, r2) = + (SM.appi (fn (k, v1) => + case SM.find (r2, k) of + NONE => raise UnequalDomains + | SOME v2 => + if f (v1, v2) then + () + else + raise UnequalDomains) r1; + SM.appi (fn (k, v2) => + case SM.find (r1, k) of + NONE => raise UnequalDomains + | SOME v1 => + if f (v1, v2) then + () + else + raise UnequalDomains) r2; + true) + handle UnequalDomains => false + +fun eqPred ((p1, _), (p2, _)) = + case (p1, p2) of + (CRoot, CRoot) => true + | (CConst s1, CConst s2) => s1 = s2 + | (CPrefix p1, CPrefix p2) => eqPred (p1, p2) + | (CNot p1, CNot p2) => eqPred (p1, p2) + | (CAnd (p1, q1), CAnd (p2, q2)) => + eqPred (p1, p2) andalso eqPred (q1, q2) + + | _ => false + +fun eqTy (t1All as (t1, _), t2All as (t2, _)) = + case (t1, t2) of + (TBase s1, TBase s2) => s1 = s2 + | (TList t1, TList t2) => eqTy (t1, t2) + | (TArrow (d1, r1), TArrow (d2, r2)) => + eqTy (d1, d2) andalso eqTy (r1, r2) + + | (TAction (p1, d1, r1), TAction (p2, d2, r2)) => + eqPred (p1, p2) andalso eqRecord eqTy (d1, d2) + andalso eqRecord eqTy (r1, r2) + + | (TNested (p1, q1), TNested (p2, q2)) => + eqPred (p1, p2) andalso eqTy (q1, q2) + + | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All) + | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2) + + | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2 + + | (TError, TError) => true + + | _ => false + +fun describe_unification_error t ue = + case ue of + UnifyPred (p1, p2) => + (print "Reason: Incompatible contexts.\n"; + preface ("Have:", p_pred p1); + preface ("Need:", p_pred p2)) + | UnifyTyp (t1, t2) => + if eqTy (t, t1) then + () + else + (print "Reason: Incompatible types.\n"; + preface ("Have:", p_typ t1); + preface ("Need:", p_typ t2)) + | UnifyOccurs (name, t') => + if eqTy (t, t') then + () + else + (print "Reason: Occurs check failed for "; + print name; + print " in:\n"; + printd (p_typ t)) + +fun describe_type_error loc te = + case te of + WrongType (place, e, t1, t2, ueo) => + (ErrorMsg.error (SOME loc) (place ^ " has wrong type."); + preface (" Expression:", p_exp e); + preface ("Actual type:", p_typ t1); + preface ("Needed type:", p_typ t2); + Option.app (describe_unification_error t1) ueo) + | WrongForm (place, form, e, t, ueo) => + (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type."); + preface ("Expression:", p_exp e); + preface (" Type:", p_typ t); + Option.app (describe_unification_error t) ueo) + | UnboundVariable name => + ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n") + | WrongPred (place, p1, p2) => + (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ "."); + preface ("Have:", p_pred p1); + preface ("Need:", p_pred p2)) + +end diff --git a/src/main-client.sml b/src/main-client.sml index 29db1b4..f0a6f69 100644 --- a/src/main-client.sml +++ b/src/main-client.sml @@ -27,13 +27,18 @@ fun domtoolRoot () = file = "domtool"} end -val _ = +val (doit, args) = case CommandLine.arguments () of + "-tc" :: args => (fn fname => (Main.setupUser (); ignore (Main.check fname)), args) + | args => (Main.request, args) + +val _ = + case args of [fname] => if Posix.FileSys.access (fname, []) then - Main.request fname + doit fname else - Main.request (OS.Path.joinDirFile {dir = domtoolRoot (), - file = fname}) + doit (OS.Path.joinDirFile {dir = domtoolRoot (), + file = fname}) | [] => Main.requestDir (domtoolRoot ()) | _ => print "Invalid command-line arguments\n" diff --git a/src/main.sig b/src/main.sig index 3b0c791..78bb42f 100644 --- a/src/main.sig +++ b/src/main.sig @@ -21,6 +21,7 @@ signature MAIN = sig val init : unit -> unit + val setupUser : unit -> string val check : string -> Env.env * Ast.exp option val check' : Env.env -> string -> Env.env diff --git a/src/main.sml b/src/main.sml index 51b8347..a8cf180 100644 --- a/src/main.sml +++ b/src/main.sml @@ -176,7 +176,7 @@ fun context x = (print "Couldn't find your certificate.\nYou probably haven't been given any Domtool privileges.\n"; raise e) -fun requestContext f = +fun setupUser () = let val user = case Posix.ProcEnv.getenv "DOMTOOL_USER" of @@ -187,9 +187,15 @@ fun requestContext f = Posix.SysDB.Passwd.name (Posix.SysDB.getpwuid uid) end | SOME user => user - - val () = Acl.read Config.aclFile - val () = Domain.setUser user + in + Acl.read Config.aclFile; + Domain.setUser user; + user + end + +fun requestContext f = + let + val user = setupUser () val () = f () diff --git a/src/sources b/src/sources index a544a3b..7809a93 100644 --- a/src/sources +++ b/src/sources @@ -24,6 +24,9 @@ print.sml env.sig env.sml +describe.sig +describe.sml + tycheck.sig tycheck.sml diff --git a/src/tycheck.sml b/src/tycheck.sml index 007a0fe..6f62a6c 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -1,5 +1,5 @@ (* HCoop Domtool (http://hcoop.sourceforge.net/) - * Copyright (c) 2006, Adam Chlipala + * Copyright (c) 2006-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 @@ -103,61 +103,6 @@ fun eqTy (t1All as (t1, _), t2All as (t2, _)) = | _ => false -datatype unification_error = - UnifyPred of pred * pred - | UnifyTyp of typ * typ - | UnifyOccurs of string * typ - -exception Unify of unification_error - -datatype type_error = - WrongType of string * exp * typ * typ * unification_error option - | WrongForm of string * string * exp * typ * unification_error option - | UnboundVariable of string - | WrongPred of string * pred * pred - -fun describe_unification_error t ue = - case ue of - UnifyPred (p1, p2) => - (print "Reason: Incompatible contexts.\n"; - preface ("Have:", p_pred p1); - preface ("Need:", p_pred p2)) - | UnifyTyp (t1, t2) => - if eqTy (t, t1) then - () - else - (print "Reason: Incompatible types.\n"; - preface ("Have:", p_typ t1); - preface ("Need:", p_typ t2)) - | UnifyOccurs (name, t') => - if eqTy (t, t') then - () - else - (print "Reason: Occurs check failed for "; - print name; - print " in:\n"; - printd (p_typ t)) - -fun describe_type_error loc te = - case te of - WrongType (place, e, t1, t2, ueo) => - (ErrorMsg.error (SOME loc) (place ^ " has wrong type."); - preface (" Expression:", p_exp e); - preface ("Actual type:", p_typ t1); - preface ("Needed type:", p_typ t2); - Option.app (describe_unification_error t1) ueo) - | WrongForm (place, form, e, t, ueo) => - (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type."); - preface ("Expression:", p_exp e); - preface (" Type:", p_typ t); - Option.app (describe_unification_error t) ueo) - | UnboundVariable name => - ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n") - | WrongPred (place, p1, p2) => - (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ "."); - preface ("Have:", p_pred p1); - preface ("Need:", p_pred p2)) - fun predImplies (p1All as (p1, _), p2All as (p2, _)) = case (p1, p2) of (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2) @@ -359,7 +304,7 @@ fun envVarSetFrom v (e, _) = fun checkExp G (eAll as (e, loc)) = let - val dte = describe_type_error loc + val dte = Describe.describe_type_error loc in case e of EInt _ => (TBase "int", loc) @@ -730,12 +675,12 @@ fun checkDecl G (d, _, loc) = in hasTyp (e, t, to) handle Unify ue => - describe_type_error loc - (WrongType ("Bound value", - e, - t, - to, - SOME ue)); + Describe.describe_type_error loc + (WrongType ("Bound value", + e, + t, + to, + SOME ue)); bindVal G (name, to, SOME e) end | DContext name => bindContext G name -- 2.20.1