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 () =
in
(* TASSI: sure this is in serial? *)
subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
- | C.LetIn (nn,s,t) ->
+ | C.LetIn (nn,s,ty,t) ->
let subst,metasenv,s',ugraph1 =
aux metasenv subst n context s ugraph in
+ let subst,metasenv,ty',ugraph1 =
+ aux metasenv subst n context ty ugraph in
let subst,metasenv,t',ugraph2 =
- aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+ aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
ugraph1
in
(* TASSI: sure this is in serial? *)
- subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
+ subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
| C.Appl l ->
let subst,metasenv,revl',ugraph1 =
List.fold_left
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
let module S = CicSubstitution in
let t1 = deref subst t1 in
let t2 = deref subst t2 in
- let b,ugraph =
+ let (&&&) a b = (a && b) || ((not a) && (not b)) in
+(* let bef = Sys.time () in *)
+ let b,ugraph =
+ if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
+ false,ugraph
+ else
let foo () =
R.are_convertible ~subst ~metasenv context t1 t2 ugraph
in profiler_are_convertible.HExtlib.profile foo ()
in
+(* let aft = Sys.time () in
+if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
if b then
subst, metasenv, ugraph
else
in
fo_unif_subst test_equality_only
subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
- | (C.LetIn (_,s1,t1), t2)
- | (t2, C.LetIn (_,s1,t1)) ->
+ | (C.LetIn (_,s1,ty1,t1), t2)
+ | (t2, C.LetIn (_,s1,ty1,t1)) ->
fo_unif_subst
test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
| (C.Appl l1, C.Appl l2) ->
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 =
projects / helm.git / blobdiff