open Printf
-exception AssertFailure of string;;
exception UnificationFailure of string;;
+exception Uncertain of string;;
+exception AssertFailure of string;;
let debug_print = prerr_endline
| CicMetaSubst.MetaSubstFailure msg ->
raise (AssertFailure
((sprintf
- "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
+ "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
(CicMetaSubst.ppterm subst term)
- (CicMetaSubst.ppcontext subst context) msg)))
+ (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppmetasenv metasenv subst) msg)))
(* NUOVA UNIFICAZIONE *)
(* A substitution is a (int * Cic.term) list that associates a
fo_unif_subst subst context metasenv lifted_oldt t
with Not_found ->
let t',metasenv',subst' =
+ try
CicMetaSubst.delift n subst context metasenv l t
+ with
+ (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
+ | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
in
(n, t')::subst', metasenv'
in
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different constants"
- (CicPp.ppterm t1) (CicPp.ppterm t1)))
+ (CicPp.ppterm t1) (CicPp.ppterm 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 subst context metasenv