| t -> t
;;
+exception WrongShape;;
+let eta_reduce after_beta_expansion after_beta_expansion_body
+ before_beta_expansion
+ =
+ try
+ match before_beta_expansion,after_beta_expansion_body with
+ Cic.Appl l, Cic.Appl l' ->
+ let rec all_but_last check_last =
+ function
+ [] -> assert false
+ | [Cic.Rel 1] -> []
+ | [_] -> if check_last then raise WrongShape else []
+ | he::tl -> he::(all_but_last check_last tl)
+ in
+ let all_but_last check_last l =
+ match all_but_last check_last l with
+ [] -> assert false
+ | [he] -> he
+ | l -> Cic.Appl l
+ in
+ let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
+ let all_but_last = all_but_last false l in
+ (* here we should test alpha-equivalence; however we know by
+ construction that here alpha_equivalence is equivalent to = *)
+ if t = all_but_last then
+ all_but_last
+ else
+ after_beta_expansion
+ | _,_ -> after_beta_expansion
+ with
+ WrongShape -> after_beta_expansion
let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
let module S = CicSubstitution in
let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
let fresh_name =
FreshNamesGenerator.mk_fresh_name ~subst
- metasenv context (Cic.Name "Heta") ~typ:argty
+ metasenv context (Cic.Name "Hbeta") ~typ:argty
in
let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
- subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2
+ let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
+ subst, metasenv, t'', ugraph2
and beta_expand_many test_equality_only metasenv subst context t args ugraph =