let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
+let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
+
let type_of_aux' metasenv subst context term ugraph =
let foo () =
try
- CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
+ profile.HExtlib.profile
+ (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
with
CicTypeChecker.TypeCheckerFailure msg ->
let msg =
(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
with
WrongShape -> after_beta_expansion
-let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
+let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
let module S = CicSubstitution in
let module C = Cic in
let foo () =
let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
let fresh_name =
FreshNamesGenerator.mk_fresh_name ~subst
- metasenv context (Cic.Name "Hbeta") ~typ:argty
+ metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
in
let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
and beta_expand_many test_equality_only metasenv subst context t args ugraph =
- let subst,metasenv,hd,ugraph =
+ let _,subst,metasenv,hd,ugraph =
List.fold_right
- (fun arg (subst,metasenv,t,ugraph) ->
+ (fun arg (num,subst,metasenv,t,ugraph) ->
let subst,metasenv,t,ugraph1 =
- beta_expand test_equality_only
+ beta_expand num test_equality_only
metasenv subst context t arg ugraph
in
- subst,metasenv,t,ugraph1
- ) args (subst,metasenv,t,ugraph)
+ num+1,subst,metasenv,t,ugraph1
+ ) args (1,subst,metasenv,t,ugraph)
in
subst,metasenv,hd,ugraph
(*
(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
(lower m1 m2) (upper m1 m2) ugraph
in
begin
- let subst,metasenv,ugraph1 =
+ let subst,metasenv,ugraph1 =
let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
(try
let tyt,ugraph1 =
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
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
test_equality_only
subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
else
- raise (UnificationFailure (lazy "5"))
- (* (sprintf
+ raise (UnificationFailure
+ (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
fo_unif_l
test_equality_only subst metasenv (lr1, lr2) ugraph
with
- | UnificationFailure _
- | Uncertain _ as exn ->
+ | UnificationFailure s
+ | Uncertain s as exn ->
(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
- CoercGraph.is_a_coercion c1 &&
- CoercGraph.is_a_coercion c2 ->
- let body1, attrs1, ugraph =
- match CicEnvironment.get_obj ugraph uri1 with
- | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
- | _ -> assert false
- in
- let body2, attrs2, ugraph =
- match CicEnvironment.get_obj ugraph uri2 with
- | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
- | _ -> assert false
- in
- let is_composite1 =
- List.exists ((=) (`Class `Coercion)) attrs1 in
- let is_composite2 =
- List.exists ((=) (`Class `Coercion)) attrs2 in
- (match is_composite1, is_composite2 with
- | false, false -> raise exn
- | true, false ->
- let body1 = CicSubstitution.subst_vars ens1 body1 in
- let appl = Cic.Appl (body1::tl1) in
- let redappl = CicReduction.head_beta_reduce appl in
- fo_unif_subst
- test_equality_only subst context metasenv
- redappl t2 ugraph
- | false, true ->
- let body2 = CicSubstitution.subst_vars ens2 body2 in
- let appl = Cic.Appl (body2::tl2) in
- let redappl = CicReduction.head_beta_reduce appl in
- fo_unif_subst
- test_equality_only subst context metasenv
- t1 redappl ugraph
- | true, true ->
- let body1 = CicSubstitution.subst_vars ens1 body1 in
- let appl1 = Cic.Appl (body1::tl1) in
- let redappl1 = CicReduction.head_beta_reduce appl1 in
- let body2 = CicSubstitution.subst_vars ens2 body2 in
- let appl2 = Cic.Appl (body2::tl2) in
- let redappl2 = CicReduction.head_beta_reduce appl2 in
- fo_unif_subst
- test_equality_only subst context metasenv
- redappl1 redappl2 ugraph)
+ CoercDb.is_a_coercion' c1 &&
+ CoercDb.is_a_coercion' c2 &&
+ not (UriManager.eq uri1 uri2) ->
+(*DEBUGGING ONLY:
+prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+let res =
+*)
+ let rec look_for_first_coercion c tl =
+ match
+ CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
+ with
+ Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
+ when CoercDb.is_a_coercion' c' ->
+ look_for_first_coercion c' tl'
+ | last_tl -> c,last_tl
+ in
+ let c1,last_tl1 = look_for_first_coercion c1 tl1 in
+ let c2,last_tl2 = look_for_first_coercion c2 tl2 in
+ let car1 =
+ CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
+ let car2 =
+ CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
+ if CoercDb.eq_carr car1 car2 then
+ (match last_tl1,last_tl2 with
+ C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn
+ | C.Meta _, _
+ | _, C.Meta _ ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1 last_tl2 ugraph
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv (C.Appl l1) (C.Appl l2) ugraph
+ | _ -> raise exn)
+ else
+ let meets =
+ CoercGraph.meets metasenv subst context car1 car2
+ in
+ (match meets with
+ | [] -> raise exn
+ | (carr,metasenv,to1,to2)::xxx ->
+ (match xxx with
+ [] -> ()
+ | (m2,_,c2,c2')::_ ->
+ let m1,_,c1,c1' = carr,metasenv,to1,to2 in
+ let unopt =
+ function Some (_,t) -> CicPp.ppterm t
+ | None -> "id"
+ in
+ HLog.warn
+ ("There are two minimal joins of "^
+ CoercDb.name_of_carr car1^" and "^
+ CoercDb.name_of_carr car2^": " ^
+ CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
+ unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+ unopt c2^" + "^unopt c2'));
+ let last_tl1',(subst,metasenv,ugraph) =
+ match last_tl1,to1 with
+ | Cic.Meta (i1,l1),Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
+ metasenv coerced last_tl1 ugraph
+ | _ -> last_tl1,(subst,metasenv,ugraph)
+ in
+ let last_tl2',(subst,metasenv,ugraph) =
+ match last_tl2,to2 with
+ | Cic.Meta (i2,l2),Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
+ metasenv coerced last_tl2 ugraph
+ | _ -> last_tl2,(subst,metasenv,ugraph)
+ in
+ (*DEBUGGING ONLY:
+prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
+*)
+ let subst,metasenv,ugraph =
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1' last_tl2' ugraph
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv (C.Appl l1) (C.Appl l2) ugraph)
+(*DEBUGGING ONLY:
+in
+let subst,metasenv,ugraph = res in
+prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res
+*)
+ (*CSC: This is necessary because of the "elim H" tactic
+ where the type of H is only reducible to an
+ inductive type. This could be extended from inductive
+ types to any rigid term. However, the code is
+ duplicated in two places: inside applications and
+ outside them. Probably it would be better to
+ work with lambda-bar terms instead. *)
+ | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
+ | (_, Cic.MutInd _::_) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "88")))
+ | (Cic.MutInd _::_,_) ->
+ let t2' = R.whd ~subst context t2 in
+ (match t2' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1 t2' ugraph
+ | _ -> 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
in
fo_unif_subst test_equality_only subst context metasenv
beta_expanded (C.Meta (i,l)) ugraph1
- | (C.Sort _ ,_) | (_, C.Sort _)
- | (C.Const _, _) | (_, C.Const _)
- | (C.MutInd _, _) | (_, C.MutInd _)
- | (C.MutConstruct _, _) | (_, C.MutConstruct _)
- | (C.Fix _, _) | (_, C.Fix _)
- | (C.CoFix _, _) | (_, C.CoFix _) ->
- if t1 = t2 then
- subst, metasenv, ugraph
- else
- let b,ugraph1 =
- R.are_convertible ~subst ~metasenv context t1 t2 ugraph
- in
- if b then
- subst, metasenv, ugraph1
- else
- raise
- (UnificationFailure (lazy (sprintf
- "Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+(* Works iff there are no arguments applied to it; similar to the
+ case below
+ | (_, C.MutInd _) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.MutInd _ ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "8")))
+*)
+(* The following idea could be exploited again; right now we have no
+ longer any example requiring it
| (C.Prod _, t2) ->
let t2' = R.whd ~subst context t2 in
(match t2' with
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)))))
+*)
| (_,_) ->
- raise (UnificationFailure (lazy "10"))
- (* (sprintf
+ (* delta-beta reduction should almost never be a problem for
+ unification since:
+ 1. long computations require iota reduction
+ 2. it is extremely rare that a close term t1 (that could be unified
+ to t2) beta-delta reduces to t1' while t2 does not beta-delta
+ reduces in the same way. This happens only if one meta of t2
+ occurs in head position during beta reduction. In this unluky
+ case too much reduction will be performed on t1 and unification
+ will surely fail. *)
+ let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
+ let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
+ if t1 = t1' && t2 = t2' then
+ 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))))
+ else
+ try
+ fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
+ with
+ UnificationFailure _
+ | Uncertain _ ->
+ raise (UnificationFailure
+ (lazy
+ (sprintf
+ "Can't unify %s with %s because they are not convertible"
+ (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)
)
projects / helm.git / blobdiff