* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
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'"
fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
exp_named_subst1 exp_named_subst2 ugraph
else
- raise (UnificationFailure (lazy "3"))
- (* (sprintf
+ raise (UnificationFailure (lazy
+ (sprintf
"Can't unify %s with %s due to different constants"
(CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))) *)
+ (CicMetaSubst.ppterm subst t2))))
| C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
if UriManager.eq uri1 uri2 && i1 = i2 then
fo_unif_subst_exp_named_subst
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
CicPp.ppterm ty_t1
- with _ -> "MALFORMED")
+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
(CicMetaSubst.ppterm subst t2)
(try
let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
CicPp.ppterm ty_t2
- with _ -> "MALFORMED")
+ 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)
+ (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)
- (CicMetaSubst.ppsubst subst) (Lazy.force msg))
+ (Lazy.force msg)
+ )
let fo_unif_subst subst context metasenv t1 t2 ugraph =
try