X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=d5262f44ba8520739a54d16de52890a2df6304c1;hb=9945374a5594c068883fa6c775f17b640fcac64d;hp=7cf16ee53403f1d908c20984a3834d42f445e514;hpb=3fec2330f2d30d47ebca0decd30bd2a457a9cbd3;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 7cf16ee53..d5262f44b 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -25,6 +25,7 @@
 
 open Printf
 
+
 exception MetaSubstFailure of string
 exception Uncertain of string
 exception AssertFailure of string
@@ -41,7 +42,11 @@ let apply_subst_gen ~appl_fun subst term =
   let module S = CicSubstitution in 
    function
       C.Rel _ as t -> t
-    | C.Var _  as t -> t
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+       in
+       C.Var (uri, exp_named_subst')
     | C.Meta (i, l) -> 
         (try
           let t = List.assoc i subst in
@@ -92,6 +97,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
@@ -101,19 +107,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' =
@@ -122,23 +116,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
@@ -245,6 +240,7 @@ let are_convertible subst context t1 t2 =
   CicReduction.are_convertible context t1 t2
 
 let tempi_type_of_aux_subst = ref 0.0;;
+let tempi_subst = ref 0.0;;
 let tempi_type_of_aux = ref 0.0;;
 
 let type_of_aux' metasenv subst context term =
@@ -267,7 +263,8 @@ let res =
 in
 let time3 = Unix.gettimeofday () in
  tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; 
- tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; 
+ tempi_subst := !tempi_subst +. time2 -. time1 ; 
+ tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ; 
  res
 
 (**** DELIFT ****)
@@ -598,7 +595,6 @@ let delift n subst context metasenv l t =
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
 debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
-print_string "\nCicMetaSubst: UNCERTAIN" ;
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)