- new implementation of the apply case in fo_unif using beta expansion

[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 83daf60a636309401e7637a9d2bdbc30caca9093..d5262f44ba8520739a54d16de52890a2df6304c1 100644 (file)
--- 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 ****)
@@ -504,14 +501,19 @@ let delift n subst context metasenv l t =
                     (*CSC: deliftato la regola per il LetIn                 *)
                     (*CSC: FALSO! La regola per il LetIn non lo fa          *)
          else
-          (match List.nth context (m-k-1) with
-            Some (_,C.Def (t,_)) ->
-             (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
-             (*CSC: first order unification. Does it help or does it harm? *)
-             deliftaux k (S.lift m t)
-          | Some (_,C.Decl t) ->
-             C.Rel ((position (m-k) l) + k)
-          | None -> raise (MetaSubstFailure "RelToHiddenHypothesis"))
+          (try
+            match List.nth context (m-k-1) with
+               Some (_,C.Def (t,_)) ->
+                (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
+                (*CSC: first order unification. Does it help or does it harm? *)
+                deliftaux k (S.lift m t)
+             | Some (_,C.Decl t) ->
+                C.Rel ((position (m-k) l) + k)
+             | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
+           with
+            Failure _ ->
+             raise (MetaSubstFailure "Unbound variable found in deliftaux")
+          )
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
@@ -593,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 !!!!!!!!!!!!!!!!" ;
-debug_print "\nCicMetaSubst: UNCERTAIN" ;
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)