]> matita.cs.unibo.it Git - helm.git/commitdiff
Convertibility now converts machines in place of terms.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jul 2007 17:54:40 +0000 (17:54 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jul 2007 17:54:40 +0000 (17:54 +0000)
Actually, the heads of the machines (i.e. everything but the stack) are
still unwinded and converted as terms. Thus there is much space for
improvement.

helm/software/components/cic_proof_checking/cicReduction.ml

index af5564d0754c32c39a594bdef0ad2ba6552dd298..7f1ec58359b728857fb4536258e7f33de7b934f1 100644 (file)
@@ -796,9 +796,10 @@ module R = Reduction
 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
@@ -1067,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 *)