X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicReduction.ml;h=7f1ec58359b728857fb4536258e7f33de7b934f1;hb=b44a732a930584aa08f4a78371dd9ac5b405f31e;hp=f4880e426de66ffd74b78808eea763cb4b761a71;hpb=b7387d913f7dddf52d1e73173bca3fc8729723ba;p=helm.git

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index f4880e426..7f1ec5835 100644
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -55,8 +55,14 @@ module type Strategy =
   type env_term
   type ens_term
   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  val to_env : config -> env_term
-  val to_ens : config -> ens_term
+  val to_env :
+   reduce: (config -> config) ->
+   unwind: (config -> Cic.term) ->
+   config -> env_term
+  val to_ens :
+   reduce: (config -> config) ->
+   unwind: (config -> Cic.term) ->
+   config -> ens_term
   val from_stack : stack_term -> config
   val from_stack_list_for_unwind :
    unwind: (config -> Cic.term) ->
@@ -106,6 +112,28 @@ module CallByValueByNameForUnwind =
  end
 ;;
 
+module CallByValueByNameForUnwind' =
+ struct
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
+  and stack_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+  and env_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+  and ens_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+
+  let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
+  let to_ens ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
+  let from_stack (c,_) = Lazy.force c
+  let from_stack_list_for_unwind ~unwind l = List.map (function (_,c) -> Lazy.force c) l
+  let from_env (c,_) = Lazy.force c
+  let from_ens (c,_) = Lazy.force c
+  let from_env_for_unwind ~unwind (_,c) = Lazy.force c
+  let from_ens_for_unwind ~unwind (_,c) = Lazy.force c
+  let stack_to_env ~reduce ~unwind config = config
+  let compute_to_env ~reduce ~unwind k e ens t =
+   lazy (reduce (k,e,ens,t,[])), lazy (unwind (k,e,ens,t,[]))
+  let compute_to_stack ~reduce ~unwind config = lazy (reduce config), lazy (unwind config)
+ end
+;;
+
 
 (* Old Machine
 module CallByNameStrategy =
@@ -712,12 +740,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
                     let leng = List.length fl in
                     let new_env =
                      let counter = ref 0 in
-                     let rec build_env e =
-                      if !counter = leng then e
+                     let rec build_env e' =
+                      if !counter = leng then e'
                       else
                        (incr counter ;
                         build_env
-                         ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e))
+                         ((RS.to_env ~reduce ~unwind (k,e,ens,C.Fix (!counter -1, fl),[]))::e'))
                      in
                       build_env e
                     in
@@ -738,7 +766,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
     function
        [] -> ens
      | (uri,t)::tl ->
-         push_exp_named_subst k e ((uri,RS.to_ens (k,e,ens,t,[]))::ens) tl
+         push_exp_named_subst k e ((uri,RS.to_ens ~reduce ~unwind (k,e,ens,t,[]))::ens) tl
    in
     reduce
   ;;
@@ -767,9 +795,11 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
-module R = Reduction(CallByValueByNameForUnwind);;
+(*module R = Reduction(CallByValueByNameForUnwind);;*)
+module RS = CallByValueByNameForUnwind';;
 (*module R = Reduction(CallByNameStrategy);;*)
 (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
+module R = Reduction(RS);;
 module U = UriManager;;
 
 let whd = R.whd
@@ -973,8 +1003,12 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-            let tys =
-              List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+            let tys,_ =
+              List.fold_left
+                (fun (types,len) (n,_,ty,_) ->
+                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                    len+1)
+	        ) ([],0) fl1
             in
             if i1 = i2 then
              List.fold_right2
@@ -992,9 +1026,13 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-           let tys =
-            List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
-           in
+            let tys,_ =
+              List.fold_left
+                (fun (types,len) (n,ty,_) ->
+                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                    len+1)
+	        ) ([],0) fl1
+            in
             if i1 = i2 then
               List.fold_right2
               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
@@ -1030,11 +1068,48 @@ begin
    (* heuristic := false; *)
    debug t1 [t2] "PREWHD";
 (*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
+(*
+prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
    let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
    let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
     debug t1' [t2'] "POSTWHD";
+*)
+let rec convert_machines ugraph =
+ function
+    [] -> true,ugraph
+  | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
+     let (b,ugraph) as res =
+      aux2 test_equality_only
+       (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph
+     in
+      if b then
+       let problems =
+        try
+         Some
+          (List.combine
+            (List.map
+              (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
+              s1)
+            (List.map
+              (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
+              s2)
+          @ tl)
+        with
+         Invalid_argument _ -> None
+       in
+        match problems with
+           None -> false,ugraph
+         | Some problems -> convert_machines ugraph problems
+      else
+       res
+in
+ convert_machines ugraph
+  [R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
+   R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
 (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)
+(*
     aux2 test_equality_only t1' t2' ugraph
+*)
 end
  in
   aux false (*c t1 t2 ugraph *)
@@ -1120,46 +1195,49 @@ let normalize ?delta ?subst ctx term =
   
   
 (* performs an head beta/cast reduction *)
-let rec head_beta_reduce ?(delta=false) =
- function
-    (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-      let he'' = CicSubstitution.subst he' t in
-       if tl' = [] then
-        he''
-       else
-        let he''' =
-         match he'' with
-            Cic.Appl l -> Cic.Appl (l@tl')
-          | _ -> Cic.Appl (he''::tl')
+let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t =
+ match upto with
+    0 -> t
+  | n ->
+    match t with
+       (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+         let he'' = CicSubstitution.subst he' t in
+          if tl' = [] then
+           he''
+          else
+           let he''' =
+            match he'' with
+               Cic.Appl l -> Cic.Appl (l@tl')
+             | _ -> Cic.Appl (he''::tl')
+           in
+            head_beta_reduce ~delta ~upto:(upto - 1) he'''
+     | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te
+     | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
+        let bo =
+         match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+            Cic.Constant (_,bo,_,_,_) -> bo
+          | Cic.Variable _ -> raise ReferenceToVariable
+          | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+          | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
         in
-         head_beta_reduce ~delta he'''
-  | Cic.Cast (te,_) -> head_beta_reduce ~delta te
-  | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
-     let bo =
-      match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
-         Cic.Constant (_,bo,_,_,_) -> bo
-       | Cic.Variable _ -> raise ReferenceToVariable
-       | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
-       | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-     in
-      (match bo with
-          None -> t
-        | Some bo ->
-           head_beta_reduce
-            ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
-  | Cic.Const (uri,ens) as t when delta=true ->
-     let bo =
-      match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
-         Cic.Constant (_,bo,_,_,_) -> bo
-       | Cic.Variable _ -> raise ReferenceToVariable
-       | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
-       | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-     in
-      (match bo with
-          None -> t
-        | Some bo ->
-           head_beta_reduce ~delta (CicSubstitution.subst_vars ens bo))
-  | t -> t
+         (match bo with
+             None -> t
+           | Some bo ->
+              head_beta_reduce ~upto
+               ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
+     | Cic.Const (uri,ens) as t when delta=true ->
+        let bo =
+         match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+            Cic.Constant (_,bo,_,_,_) -> bo
+          | Cic.Variable _ -> raise ReferenceToVariable
+          | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+          | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+        in
+         (match bo with
+             None -> t
+           | Some bo ->
+              head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
+     | t -> t
 
 (*
 let are_convertible ?subst ?metasenv context t1 t2 ugraph =