- In the case (?i args) vs term the term is now eta-expanded w.r.t. args.

[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 9695d714b7658940392fc4401af71d3701d7298f..512c65d986fa2c48015309faca2a908c7501a654 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -96,6 +96,7 @@ let apply_subst_gen ~appl_fun subst term =
 ;;
 
 let apply_subst =
+(* CSC: old code that never performs beta reduction
   let appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
       begin
@@ -105,19 +106,7 @@ let apply_subst =
       end
   in
   apply_subst_gen ~appl_fun
-;;
-
-(* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
-(* performs as (apply_subst subst t) until it finds an application of   *)
-(* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
-(* a new beta-redex; in this case up to [reductions_no] consecutive     *)
-(* beta-reductions are performed.                                       *)
-(* Hint: this function is usually called when [reductions_no]           *)
-(*  eta-expansions have been performed and the head of the new          *)
-(*  application has been unified with (META [meta_to_reduce]):          *)
-(*  during the unwinding the eta-expansions are undone.                 *)
-
-let apply_subst_reducing meta_to_reduce =
+*)
   let appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
     let t' =
@@ -126,23 +115,24 @@ let apply_subst_reducing meta_to_reduce =
       | he' -> Cic.Appl (he'::tl')
     in
      begin
-      match meta_to_reduce, he with
-         Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr ->
+      match he with
+         Cic.Meta (m,_) ->
           let rec beta_reduce =
            function
-              (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
+              (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
                 let he'' = CicSubstitution.subst he' t in
                  if tl' = [] then
                   he''
                  else
-                  beta_reduce (n-1,Cic.Appl(he''::tl'))
-            | (_,t) -> t
+                  beta_reduce (Cic.Appl(he''::tl'))
+            | t -> t
           in
-           beta_reduce (reductions_no,t')
-       | _,_ -> t'
+           beta_reduce t'
+       | _ -> t'
      end
   in
   apply_subst_gen ~appl_fun
+;;
 
 let rec apply_subst_context subst context =
   List.fold_right