From fc8f251f8a471249ac6a296c079ccfeb0b535862 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 19 Jul 2007 17:54:40 +0000 Subject: [PATCH] Convertibility now converts machines in place of terms. 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. --- components/cic_proof_checking/cicReduction.ml | 40 ++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml index af5564d07..7f1ec5835 100644 --- a/components/cic_proof_checking/cicReduction.ml +++ b/components/cic_proof_checking/cicReduction.ml @@ -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 *) -- 2.39.2