From 5c3ae2f17d55098676bd50270ddef0bec93618bf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 19 Nov 2005 17:51:54 +0000 Subject: [PATCH] Less verbose error messages (= substitution applied everywhere, terms pretty printed in their context) are now printed by default. There is a flag in cicUnification.ml to set the error messages to the verbose mode. --- helm/ocaml/cic_disambiguation/disambiguate.ml | 4 +-- helm/ocaml/cic_unification/cicMetaSubst.ml | 24 +++++++++------ helm/ocaml/cic_unification/cicMetaSubst.mli | 4 ++- helm/ocaml/cic_unification/cicUnification.ml | 30 +++++++++++++++++-- 4 files changed, 47 insertions(+), 15 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index de3701e23..d3f5b0106 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -70,11 +70,11 @@ let refine_term metasenv context uri term ugraph = with | CicRefine.Uncertain msg -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph + Uncertain (lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)),ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) (Lazy.force msg))); - Ko (lazy ("Error trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph + Ko (lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)),ugraph let refine_obj metasenv context uri obj ugraph = assert (context = []); diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index dfa47e469..718951c68 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -191,8 +191,8 @@ let apply_subst_gen ~appl_fun subst term = List.map (function None -> None | Some t -> Some (um_aux t)) l in C.Meta (i,l')) - | C.Sort _ as t -> t - | C.Implicit _ -> assert false + | C.Sort _ + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) @@ -288,9 +288,15 @@ let apply_subst_metasenv subst metasenv = let ppterm subst term = CicPp.ppterm (apply_subst subst term) -let ppterm_in_context subst term name_context = +let ppterm_in_name_context subst term name_context = CicPp.pp (apply_subst subst term) name_context +let ppterm_in_context subst term context = + let name_context = + List.map (function None -> None | Some (n,_) -> Some n) context + in + ppterm_in_name_context subst term name_context + let ppcontext' ?(sep = "\n") subst context = let separate s = if s = "" then "" else s ^ sep in List.fold_right @@ -298,13 +304,13 @@ let ppcontext' ?(sep = "\n") subst context = match context_entry with Some (n,Cic.Decl t) -> sprintf "%s%s : %s" (separate i) (CicPp.ppname n) - (ppterm_in_context subst t name_context), (Some n)::name_context + (ppterm_in_name_context subst t name_context), (Some n)::name_context | Some (n,Cic.Def (bo,ty)) -> sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) (match ty with None -> "_" - | Some ty -> ppterm_in_context subst ty name_context) - (ppterm_in_context subst bo name_context), (Some n)::name_context + | Some ty -> ppterm_in_name_context subst ty name_context) + (ppterm_in_name_context subst bo name_context), (Some n)::name_context | None -> sprintf "%s_ :? _" (separate i), None::name_context ) context ("",[]) @@ -315,7 +321,7 @@ let ppsubst_unfolded subst = (fun (idx, (c, t,_)) -> let context,name_context = ppcontext' ~sep:"; " subst c in sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_context subst t name_context)) + (ppterm_in_name_context subst t name_context)) subst) (* Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) @@ -328,7 +334,7 @@ let ppsubst subst = (fun (idx, (c, t, _)) -> let context,name_context = ppcontext' ~sep:"; " [] c in sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_context [] t name_context)) + (ppterm_in_name_context [] t name_context)) subst) ;; @@ -340,7 +346,7 @@ let ppmetasenv ?(sep = "\n") subst metasenv = (fun (i, c, t) -> let context,name_context = ppcontext' ~sep:"; " subst c in sprintf "%s |- ?%d: %s" context i - (ppterm_in_context subst t name_context)) + (ppterm_in_name_context subst t name_context)) (List.filter (fun (i, _, _) -> not (List.mem_assoc i subst)) metasenv)) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 890a347b0..96f87205f 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -65,8 +65,10 @@ val ppsubst_unfolded: Cic.substitution -> string val ppsubst: Cic.substitution -> string val ppterm: Cic.substitution -> Cic.term -> string val ppcontext: ?sep: string -> Cic.substitution -> Cic.context -> string -val ppterm_in_context: +val ppterm_in_name_context: Cic.substitution -> Cic.term -> (Cic.name option) list -> string +val ppterm_in_context: + Cic.substitution -> Cic.term -> Cic.context -> string val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string (** {2 Format-like pretty printers} diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index a3bc1f39a..9db77c5d5 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -29,6 +29,7 @@ exception UnificationFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +let verbose = false;; let debug_print = fun _ -> () let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'" @@ -691,8 +692,9 @@ let fo_unif metasenv context t1 t2 ugraph = fo_unif_subst false [] context metasenv t1 t2 ugraph ;; let enrich_msg msg subst context metasenv t1 t2 ugraph = - lazy - (sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" + lazy ( + if verbose then + sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" (CicMetaSubst.ppterm subst t1) (try let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in @@ -711,7 +713,29 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph = | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) (Lazy.force msg)) + (CicMetaSubst.ppsubst subst) (Lazy.force msg) + else + sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" + (CicMetaSubst.ppterm_in_context subst t1 context) + (try + let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in + CicMetaSubst.ppterm_in_context subst ty_t1 context + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) + (CicMetaSubst.ppterm_in_context subst t2 context) + (try + let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in + CicMetaSubst.ppterm_in_context subst ty_t2 context + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) + (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppmetasenv subst metasenv) + (Lazy.force msg) + ) let fo_unif_subst subst context metasenv t1 t2 ugraph = try -- 2.39.2