...

[helm.git] / components / cic_proof_checking / cicReduction.ml

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index bfba135cf992cb6c44c9cba58364f9f42e9c3f61..7f1ec58359b728857fb4536258e7f33de7b934f1 100644 (file)
--- 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
@@ -1038,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 *)