(sprintf
"Kernel Type checking error:
%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
(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)
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."
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)
| Invalid_argument _ ->
raise
(UnificationFailure (lazy "2")))
(*
(sprintf
"Error trying to unify %s with %s: the lengths of the two local contexts do not match."
| Invalid_argument _ ->
raise
(UnificationFailure (lazy "2")))
(*
(sprintf
"Error trying to unify %s with %s: the lengths of the two local contexts do not match."
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
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
C.Sort (C.Type u) when not test_equality_only ->
let u' = CicUniv.fresh () in
let s = C.Sort (C.Type u') in
| 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
test_equality_only
subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
else
| 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
test_equality_only
subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
else
- raise (UnificationFailure (lazy "4"))
- (* (sprintf
- "Can't unify %s with %s due to different inductive principles"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))) *)
+ raise (UnificationFailure
+ (lazy
+ (sprintf
+ "Can't unify %s with %s due to different inductive principles"
+ (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
| 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
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
subst context metasenv te t2 ugraph
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
subst context metasenv te t2 ugraph
(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
CoercGraph.is_a_coercion c1 &&
(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
CoercGraph.is_a_coercion c1 &&
let body1, attrs1, ugraph =
match CicEnvironment.get_obj ugraph uri1 with
| Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
let body1, attrs1, ugraph =
match CicEnvironment.get_obj ugraph uri1 with
| Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
(match is_composite1, is_composite2 with
| false, false -> raise exn
| true, false ->
(match is_composite1, is_composite2 with
| false, false -> raise exn
| true, false ->
C.Appl (C.MutInd _::_) ->
fo_unif_subst test_equality_only
subst context metasenv t1 t2' ugraph
C.Appl (C.MutInd _::_) ->
fo_unif_subst test_equality_only
subst context metasenv t1 t2' ugraph
| _ -> raise exn)))
| (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
let subst', metasenv',ugraph1 =
| _ -> 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."
raise (UnificationFailure (lazy "6.1")))
(* (sprintf
"Error trying to unify %s with %s: the number of branches is not the same."
| (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
let subst,metasenv,beta_expanded,ugraph1 =
beta_expand_many
| (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
let subst,metasenv,beta_expanded,ugraph1 =
beta_expand_many
and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
exp_named_subst1 exp_named_subst2 ugraph
and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
exp_named_subst1 exp_named_subst2 ugraph