let exists_a_meta l =
List.exists (function Cic.Meta _ -> true | _ -> false) l
-let rec beta_reduce =
- function
- (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
- let he'' = CicSubstitution.subst he' t in
- if tl' = [] then
- he''
- else
- beta_reduce (Cic.Appl(he''::tl'))
- | t -> t
-(*
-let rec deref subst =
- let snd (_,a,_) = a in
- function
- Cic.Meta(n,l) as t ->
- (try
- deref subst
- (CicSubstitution.subst_meta
- l (snd (CicUtil.lookup_subst n subst)))
- with
- CicUtil.Subst_not_found _ -> t)
- | t -> t
-;; *)
-
let rec deref subst t =
let snd (_,a,_) = a in
match t with
| Cic.Appl(Cic.Meta(n,l)::args) ->
(match deref subst (Cic.Meta(n,l)) with
| Cic.Lambda _ as t ->
- deref subst (beta_reduce (Cic.Appl(t::args)))
+ deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
| r -> Cic.Appl(r::args))
| Cic.Appl(((Cic.Lambda _) as t)::args) ->
- deref subst (beta_reduce (Cic.Appl(t::args)))
+ deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
| t -> t
;;
(try
let (_,t,_) = CicUtil.lookup_subst i subst in
let lifted = S.subst_meta l t in
- let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+ let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
fo_unif_subst
test_equality_only
subst context metasenv reduced t2 ugraph
(* (try
let (_,t,_) = CicUtil.lookup_subst i subst in
let lifted = S.subst_meta l t in
- let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+ let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
fo_unif_subst
test_equality_only
subst context metasenv t1 reduced ugraph