(sprintf
"Kernel Type checking error:
%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
- (CicMetaSubst.ppterm subst term)
- (CicMetaSubst.ppterm [] term)
- (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppterm ~metasenv subst term)
+ (CicMetaSubst.ppterm ~metasenv [] term)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
(CicMetaSubst.ppmetasenv subst metasenv)
- (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+ (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
raise (AssertFailure msg)
| CicTypeChecker.AssertFailure msg ->
let msg = lazy
(sprintf
"Kernel Type checking assertion failure:
%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
- (CicMetaSubst.ppterm subst term)
- (CicMetaSubst.ppterm [] term)
- (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppterm ~metasenv subst term)
+ (CicMetaSubst.ppterm ~metasenv [] term)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
(CicMetaSubst.ppmetasenv subst metasenv)
- (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+ (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
raise (AssertFailure msg)
in profiler_toa.HExtlib.profile foo ()
;;
let exists_a_meta l =
- List.exists (function Cic.Meta _ -> true | _ -> false) l
+ List.exists
+ (function
+ | Cic.Meta _
+ | Cic.Appl (Cic.Meta _::_) -> true
+ | _ -> false) l
let rec deref subst t =
let snd (_,a,_) = a in
(*
(sprintf
"Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))) *)
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))) *)
| Invalid_argument _ ->
raise
(UnificationFailure (lazy "2")))
(*
(sprintf
"Error trying to unify %s with %s: the lengths of the two local contexts do not match."
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2)))) *)
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
in subst,metasenv,ugraph1
| (C.Meta (n,_), C.Meta (m,_)) when n>m ->
fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
C.Sort (C.Type u) when not test_equality_only ->
let u' = CicUniv.fresh () in
let s = C.Sort (C.Type u') in
- let ugraph2 =
- CicUniv.add_ge (upper u u') (lower u u') ugraph1
- in
- s,ugraph2
+ (try
+ let ugraph2 =
+ CicUniv.add_ge (upper u u') (lower u u') ugraph1
+ in
+ s,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg ->
+ raise (UnificationFailure msg))
| _ -> t',ugraph1
in
(* Unifying the types may have already instantiated n. Let's check *)
raise (UnificationFailure (lazy
(sprintf
"Can't unify %s with %s due to different constants"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv 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
(lazy
(sprintf
"Can't unify %s with %s due to different inductive principles"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
| C.MutConstruct (uri1,i1,j1,exp_named_subst1),
C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
(lazy
(sprintf
"Can't unify %s with %s due to different inductive constructors"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
subst context metasenv te t2 ugraph
C.Appl (C.MutInd _::_) ->
fo_unif_subst test_equality_only
subst context metasenv t1 t2' ugraph
- | _ -> raise (UnificationFailure (lazy "99")))
+ | _ -> raise
+ (UnificationFailure
+ (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
| _ -> raise exn)))
| (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
let subst', metasenv',ugraph1 =
raise (UnificationFailure (lazy "6.1")))
(* (sprintf
"Error trying to unify %s with %s: the number of branches is not the same."
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2)))) *)
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
| (C.Rel _, _) | (_, C.Rel _) ->
if t1 = t2 then
subst, metasenv,ugraph
raise (UnificationFailure (lazy
(sprintf
"Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
| (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
let subst,metasenv,beta_expanded,ugraph1 =
beta_expand_many
raise
(UnificationFailure (lazy (sprintf
"Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2)))))
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2)))))
*)
| (_,_) ->
(* delta-beta reduction should almost never be a problem for
(lazy
(sprintf
"Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
else
try
fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
(lazy
(sprintf
"Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
exp_named_subst1 exp_named_subst2 ugraph
String.concat " ; "
(List.map
(fun (uri,t) ->
- UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
+ UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
) ens)
in
raise (UnificationFailure (lazy (sprintf
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)
+ (CicMetaSubst.ppterm ~metasenv subst t1)
(try
let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
CicPp.ppterm ty_t1
| UnificationFailure s
| Uncertain s
| AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
- (CicMetaSubst.ppterm subst t2)
+ (CicMetaSubst.ppterm ~metasenv subst t2)
(try
let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
CicPp.ppterm ty_t2
| UnificationFailure s
| Uncertain s
| AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
- (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
(CicMetaSubst.ppmetasenv subst metasenv)
- (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+ (CicMetaSubst.ppsubst ~metasenv 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)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
(try
let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
- CicMetaSubst.ppterm_in_context subst ty_t1 context
+ CicMetaSubst.ppterm_in_context ~metasenv 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)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
(try
let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
- CicMetaSubst.ppterm_in_context subst ty_t2 context
+ CicMetaSubst.ppterm_in_context ~metasenv 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.ppcontext ~metasenv subst context)
(CicMetaSubst.ppmetasenv subst metasenv)
(Lazy.force msg)
)