From: Claudio Sacerdoti Coen Date: Tue, 25 Oct 2005 12:49:21 +0000 (+0000) Subject: * More profiling code X-Git-Tag: V_0_7_2_3~198 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8f146da4ab463bbc6a202bed267a1ae6e5dcd0c0;p=helm.git * More profiling code * Debugging code restructured --- diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index fe0c09aae..29762b86d 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -33,7 +33,8 @@ exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; -let debug_print = fun _ -> () +let debug = true +let debug_print s = if debug then prerr_endline (Lazy.force s) let fdebug = ref 1;; let debug t env s = @@ -509,8 +510,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; unwind_aux m t ;; - let unwind = - unwind' 0 +let profiler_unwind = HExtlib.profile "are_convertible.unwind" + let unwind k e ens t = +let foo () = + unwind' 0 k e ens t +in + profiler_unwind.HExtlib.profile foo () ;; let reduce ~delta ?(subst = []) context : config -> Cic.term = @@ -770,54 +775,39 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; ;; -(* DEBUGGING ONLY -let whd context t = - let res = whd context t in - let rescsc = CicReductionNaif.whd context t in - if not (CicReductionNaif.are_convertible context res rescsc) then - begin - debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ; - flush stderr ; - debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ; - flush stderr ; - debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ; - flush stderr ; -CicReductionNaif.fdebug := 0 ; -let _ = CicReductionNaif.are_convertible context res rescsc in - assert false ; - end - else - res -;; -*) end ;; -(* -module R = Reduction CallByNameStrategy;; -module R = Reduction CallByValueStrategy;; -module R = Reduction CallByValueStrategyByNameOnConstants;; -module R = Reduction LazyCallByValueStrategy;; -module R = Reduction LazyCallByValueStrategyByNameOnConstants;; -module R = Reduction LazyCallByNameStrategy;; +(* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione + senza ridurre la testa +module R = Reduction CallByNameStrategy;; OK 56.368s +module R = Reduction CallByValueStrategy;; ROTTO +module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO +module R = Reduction LazyCallByValueStrategy;; ROTTO +module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO +module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s module R = Reduction LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;; -module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; + OK 59.058s +module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s module R = Reduction - ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; + ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s +module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s *) module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; module U = UriManager;; -let whd = R.whd;; +let profiler_whd = HExtlib.profile "are_convertible.whd" +let whd = R.whd (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then * fallbacks to structural equality *) -let (===) x y = (Pervasives.compare x y = 0) +let (===) x y = + Pervasives.compare x y = 0 (* t1, t2 must be well-typed *) -let are_convertible ?(subst=[]) ?(metasenv=[]) = +let are_convertible whd ?(subst=[]) ?(metasenv=[]) = let rec aux test_equality_only context t1 t2 ugraph = let aux2 test_equality_only t1 t2 ugraph = @@ -1031,8 +1021,18 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = debug_print (lazy (CicPp.ppterm t2)); debug_print (lazy (CicPp.ppterm (whd ~subst context t2))) | _ -> ()); *) - let t1' = whd ~subst context t1 in - let t2' = whd ~subst context t2 in + let t1' = + let foo () = +whd ?delta:(Some true) ?subst:(Some subst) context t1 + in + profiler_whd.HExtlib.profile foo () +in + let t2' = + let foo () = +whd ?delta:(Some true) ?subst:(Some subst) context t2 + in + profiler_whd.HExtlib.profile foo () +in debug t1' [t2'] "POSTWHD"; aux2 test_equality_only t1' t2' ugraph end @@ -1040,6 +1040,35 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = aux false (*c t1 t2 ugraph *) ;; +(* DEBUGGING ONLY +let whd ?(delta=true) ?(subst=[]) context t = + let res = whd ~delta ~subst context t in + let rescsc = CicReductionNaif.whd ~delta ~subst context t in + if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then + begin + debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ; + flush stderr ; + debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ; + flush stderr ; + debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ; + flush stderr ; +fdebug := 0 ; +let _ = are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in + assert false ; + end + else + res +;; +*) + +let are_convertible = are_convertible whd + +let profiler_other_whd = HExtlib.profile "~are_convertible.whd" +let whd ?(delta=true) ?(subst=[]) context t = + let foo () = + whd ~delta ~subst context t + in + profiler_other_whd.HExtlib.profile foo () let rec normalize ?(delta=true) ?(subst=[]) ctx term = let module C = Cic in