From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:35 +0000 Subject: Uniformization of the "anomaly" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/xml/acic2Xml.ml4 | 2 +- plugins/xml/cic2acic.ml | 18 ++++++++++-------- plugins/xml/xmlcommand.ml | 6 +++--- 3 files changed, 14 insertions(+), 12 deletions(-) (limited to 'plugins/xml') diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index 34bb1d51f..9d3a10dba 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -21,7 +21,7 @@ let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";; let rec find_last_id = function - [] -> Errors.anomaly "find_last_id: empty list" + [] -> Errors.anomaly ~label:"find_last_id" (Pp.str "empty list") | [id,_,_] -> id | _::tl -> find_last_id tl ;; diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 4a8436d76..2772779d4 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -12,6 +12,8 @@ (* http://helm.cs.unibo.it *) (************************************************************************) +open Pp + (* Utility Functions *) exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;; @@ -162,7 +164,7 @@ let family_of_term ty = match Term.kind_of_term ty with Term.Sort s -> Coq_sort (Term.family_of_sort s) | Term.Const _ -> CProp (* I could check that the constant is CProp *) - | _ -> Errors.anomaly "family_of_term" + | _ -> Errors.anomaly (Pp.str "family_of_term") ;; module CPropRetyping = @@ -177,7 +179,7 @@ module CPropRetyping = | h::rest -> match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest - | _ -> Errors.anomaly "Non-functional construction" + | _ -> Errors.anomaly (Pp.str "Non-functional construction") let sort_of_atomic_type env sigma ft args = @@ -193,7 +195,7 @@ let typeur sigma metamap = match Term.kind_of_term cstr with | T.Meta n -> (try T.strip_outer_cast (List.assoc n metamap) - with Not_found -> Errors.anomaly "type_of: this is not a well-typed term") + with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in T.lift n ty @@ -202,7 +204,7 @@ let typeur sigma metamap = let (_,_,ty) = Environ.lookup_named id env in ty with Not_found -> - Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound")) + Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) @@ -212,7 +214,7 @@ let typeur sigma metamap = | T.Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> Errors.anomaly "type_of: Bad recursive type" in + with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "Bad recursive type") in let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) @@ -253,7 +255,7 @@ let typeur sigma metamap = | _, (CProp as s) -> s) | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly "sort_of: Not a type (1)" + Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") | _ -> outsort env sigma (type_of env t) and sort_family_of env t = @@ -265,7 +267,7 @@ let typeur sigma metamap = | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly "sort_of: Not a type (1)" + Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") | _ -> outsort env sigma (type_of env t) in type_of, sort_of, sort_family_of @@ -514,7 +516,7 @@ print_endline "PASSATO" ; flush stdout ; add_inner_type fresh_id'' ; A.AEvar (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | T.Meta _ -> Errors.anomaly "Meta met during exporting to XML" + | T.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML") | T.Sort s -> A.ASort (fresh_id'', s) | T.Cast (v,_, t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index e16f9dd19..479b04228 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -289,7 +289,7 @@ let kind_of_variable id = | IsAssumption Conjectural -> "VARIABLE","Conjecture" | IsDefinition Definition -> "VARIABLE","LocalDefinition" | IsProof _ -> "VARIABLE","LocalFact" - | _ -> Errors.anomaly "Unsupported variable kind" + | _ -> Errors.anomaly (Pp.str "Unsupported variable kind") ;; let kind_of_constant kn = @@ -423,7 +423,7 @@ let print_ref qid fn = (* pretty prints via Xml.pp the proof in progress on dest *) let show_pftreestate internal fn (kind,pftst) id = if true then - Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version." + Errors.anomaly (Pp.str "Xmlcommand.show_pftreestate is not supported in this version.") let show fn = let pftst = Pfedit.get_pftreestate () in @@ -519,7 +519,7 @@ let _ = let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then - Errors.anomaly ("Error executing \"" ^ cmd ^ "\"") + Errors.anomaly (Pp.str ("Error executing \"" ^ cmd ^ "\"")) in command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); command ("rm "^fn^".v "^fn^".glob"); -- cgit v1.2.3