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.

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index de3701e23401e8cec86445ce5ecbbb4a041a9337..d3f5b0106cef3868960126c4f75197e16c3525c0 100644 (file)
--- 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 dfa47e469bbd97d12ddbf6e83ce39935bd90c526..718951c68a579756e4c4bd1d0994c835d28e2bac 100644 (file)
--- 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 890a347b006b879660f9908569c5a0a2de7c83f1..96f87205f4723e715ce84c114c63c500d6cc094f 100644 (file)
--- 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 a3bc1f39a02a6fb76213c7caf54de0bc798c3a3d..9db77c5d526200246379772cd0a9a1d8cf78c67a 100644 (file)
--- 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<BEGIN>%s\n<END>" (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<BEGIN>%s\n<END>" (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<BEGIN>%s\n<END>" (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