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
subst context metasenv te t2 ugraph
| (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
subst context metasenv t1 te ugraph
- | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
- let subst',metasenv',ugraph1 =
- fo_unif_subst true subst context metasenv s1 s2 ugraph
- in
- fo_unif_subst test_equality_only
- subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
| (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
let subst',metasenv',ugraph1 =
fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
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) ->
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
- C.Prod _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1 t2' ugraph
- | _ -> raise (UnificationFailure (lazy "8")))
- | (t1, C.Prod _) ->
- let t1' = R.whd ~subst context t1 in
- (match t1' with
- C.Prod _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1' t2 ugraph
- | _ -> (* raise (UnificationFailure "9")) *)
- 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)))))
-*)
+ | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
+ let subst',metasenv',ugraph1 =
+ fo_unif_subst true subst context metasenv s1 s2 ugraph
+ in
+ fo_unif_subst test_equality_only
+ subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
+ | (C.Prod _, _) ->
+ (match CicReduction.whd ~subst context t2 with
+ | C.Prod _ as t2 ->
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
+ | (_, C.Prod _) ->
+ (match CicReduction.whd ~subst context t1 with
+ | C.Prod _ as t1 ->
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
| (_,_) ->
(* delta-beta reduction should almost never be a problem for
unification since: