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
metasenv (C.Appl l1) (C.Appl l2) ugraph
| _ -> raise exn)
else
- let meets = CoercGraph.meets car1 car2 in
+ let meets =
+ CoercGraph.meets metasenv subst context car1 car2
+ in
(match meets with
| [] -> raise exn
- | _::_::_ ->
-prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-let m1::m2::_ = meets in
-prerr_endline ("M1 = " ^ CoercDb.name_of_carr m1 ^ "\nM2 = " ^ CoercDb.name_of_carr m2);
-assert false
- | [m] ->
+ | (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 with
- | Cic.Meta (i1,l1)
- when not (CoercDb.eq_carr m car1) ->
- (match
- CoercGraph.look_for_coercion' metasenv subst
- context m car1
- with
- | CoercGraph.SomeCoercion [metasenv,last,coerced]
- ->
- last,
- fo_unif_subst test_equality_only subst context
+ 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
- | _ ->
-prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
- | _ -> last_tl1,(subst,metasenv,ugraph) in
+ | _ -> last_tl1,(subst,metasenv,ugraph)
+ in
let last_tl2',(subst,metasenv,ugraph) =
- match last_tl2 with
- Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) ->
- (match
- CoercGraph.look_for_coercion' metasenv subst
- context m car2
- with
- (*CSC: bu here: I am considering only the first one*)
- | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
- ->
- last,
- fo_unif_subst test_equality_only subst context
+ 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
- | _ ->
-prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
- | _ -> last_tl2,(subst,metasenv,ugraph)
+ | _ -> last_tl2,(subst,metasenv,ugraph)
in
-(*DEBUGGING ONLY:
+ (*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 =