From ce1a28081c93b5b5699ffd2e3f9129819beade50 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 10 Nov 2004 12:01:39 +0000 Subject: [PATCH] commented out some timing messages --- helm/ocaml/cic_omdoc/cic2acic.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index f86e22f84..071950543 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -81,9 +81,10 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts let module D = DoubleTypeInference in let module C = Cic in let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in - let time1 = Sys.time () in +(* let time1 = Sys.time () in *) let terms_to_types = let time0 = Sys.time () in +(* let prova = CicTypeChecker.type_of_aux' metasenv context t in let time1 = Sys.time () in prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0))); @@ -91,10 +92,14 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts let time2 = Sys.time () in prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1))); res +*) + D.double_type_of metasenv context t expectedty in +(* let time2 = Sys.time () in prerr_endline ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ; +*) let rec aux computeinnertypes father context idrefs tt = let fresh_id'' = fresh_id' father tt in (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) @@ -329,12 +334,15 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) ) fresh_idrefs funs ) in +(* let timea = Sys.time () in let res = aux true None context idrefs t in let timeb = Sys.time () in prerr_endline ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ; res +*) + aux true None context idrefs t ;; let acic_of_cic_context metasenv context idrefs t = @@ -518,18 +526,21 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = in (cid,i,(List.rev revacanonical_context),aterm) ) conjectures' in *) - let time1 = Sys.time () in +(* let time1 = Sys.time () in *) let bo' = eta_fix conjectures' [] bo in let ty' = eta_fix conjectures' [] ty in +(* let time2 = Sys.time () in prerr_endline ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ; hashtbl_add_time := 0.0 ; type_of_aux'_add_time := 0.0 ; DoubleTypeInference.syntactic_equality_add_time := 0.0 ; +*) let abo = acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in +(* let time3 = Sys.time () in prerr_endline ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ; @@ -543,6 +554,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ; prerr_endline ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ; +*) C.ACurrentProof ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params) | C.InductiveDefinition (tys,params,paramsno) -> -- 2.39.2