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
(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 &&
+ CoercDb.is_a_coercion' c1 &&
+ CoercDb.is_a_coercion' c2 &&
not (UriManager.eq uri1 uri2) ->
- 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
- (function `Class (`Coercion _) -> true | _-> false)
- attrs1
- in
- let is_composite2 =
- List.exists
- (function `Class (`Coercion _) -> true | _-> false)
- 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)
+(*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
projects / helm.git / blobdiff