1. profiling code added

2. debug_print made lazy to avoid computation of the argument when profiling
   is disabled. This really speeds up disambiguation!

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 11d1952050205ba29987690e29c0762be40a933f..6dbd312481a0c50e52ef7173787895a0a60bfb14 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -38,7 +38,7 @@ exception Try_again
 type aliases = bool * DisambiguateTypes.environment
 
 let debug = false
-let debug_print = if debug then prerr_endline else ignore
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (*
   (** print benchmark information *)
@@ -64,34 +64,34 @@ let refine_term metasenv context uri term ugraph =
   assert (uri=None);
   let metasenv, term = 
     CicMkImplicit.expand_implicits metasenv [] context term in
-    debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
+    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
     try
       let term', _, metasenv',ugraph1 = 
        CicRefine.type_of_aux' metasenv context term ugraph in
        (Ok (term', metasenv')),ugraph1
     with
       | CicRefine.Uncertain s ->
-          debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
+          debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term)) ;
           Uncertain,ugraph
       | CicRefine.RefineFailure msg ->
-          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
-            (CicPp.ppterm term) (CicRefine.explain_error msg));
+          debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+            (CicPp.ppterm term) (CicRefine.explain_error msg)));
           Ko,ugraph
 
 let refine_obj metasenv context uri obj ugraph =
  assert (context = []);
  let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in
-   debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj));
+   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
    try
      let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
        (Ok (obj', metasenv)),ugraph
    with
      | CicRefine.Uncertain s ->
-         debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj) ;
+         debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj)) ;
          Uncertain,ugraph
      | CicRefine.RefineFailure msg ->
-         debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
-           (CicPp.ppobj obj) (CicRefine.explain_error msg));
+         debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+           (CicPp.ppobj obj) (CicRefine.explain_error msg))) ;
          Ko,ugraph
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
@@ -102,7 +102,7 @@ let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?
       (DisambiguateTypes.string_of_domain_item item))
 
   (* TODO move it to Cic *)
-let find_in_environment name (context: Cic.name list) =
+let find_in_context name (context: Cic.name list) =
   let rec aux acc = function
     | [] -> raise Not_found
     | Cic.Name hd :: tl when hd = name -> acc
@@ -233,7 +233,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
         (try
           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
-          let index = find_in_environment name context in
+          let index = find_in_context name context in
           if subst <> None then
             CicNotationPt.fail loc "Explicit substitutions not allowed here";
           Cic.Rel index
@@ -292,13 +292,13 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->
 (*
-                debug_print (sprintf
+                debug_print (lazy (sprintf
                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
                   (CicPp.ppterm t)
                   (String.concat "; "
                     (List.map
                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
-                      subst)));
+                      subst))));
 *)
                 t
             | _ ->
@@ -536,7 +536,7 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function
       where_dom @ defs_dom
   | CicNotationPt.Ident (name, subst) ->
       (try
-        let index = find_in_environment name context in
+        let index = find_in_context name context in
         if subst <> None then
           CicNotationPt.fail loc "Explicit substitutions not allowed here"
         else
@@ -683,31 +683,34 @@ module Make (C: Callbacks) =
              try
                CicUtil.term_of_uri uri
              with exn ->
-               debug_print (UriManager.string_of_uri uri);
-               debug_print (Printexc.to_string exn);
+               debug_print (lazy (UriManager.string_of_uri uri));
+               debug_print (lazy (Printexc.to_string exn));
                assert false
             in
            fun _ _ _ -> term))
         uris
 
+let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing"
+let disambiguate_environment_merge_profiler = CicUtil.profile "disambiguate_thing.disambiguate_environment_merge"
+
     let disambiguate_thing ~dbd ~context ~metasenv
       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
     =
-      debug_print "DISAMBIGUATE INPUT";
+      debug_print (lazy "DISAMBIGUATE INPUT");
       let disambiguate_context =  (* cic context -> disambiguate context *)
         List.map
           (function None -> Cic.Anonymous | Some (name, _) -> name)
           context
       in
-      debug_print ("TERM IS: " ^ (pp_thing thing));
+      debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
-      debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
-        (string_of_domain thing_dom));
-      debug_print (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
-        (DisambiguatePp.pp_environment aliases));
-      debug_print (sprintf "DISAMBIGUATION UNIVERSE: %s"
-        (match universe with None -> "None" | Some _ -> "Some _"));
+      debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"
+        (string_of_domain thing_dom)));
+      debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
+        (DisambiguatePp.pp_environment aliases)));
+      debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
+        (match universe with None -> "None" | Some _ -> "Some _")));
       let current_dom =
         Environment.fold (fun item _ dom -> item :: dom) aliases []
       in
@@ -745,8 +748,8 @@ module Make (C: Callbacks) =
               (fun dom_item ->
                 try
                   let len = List.length (lookup_choices dom_item) in
-                  debug_print (sprintf "BENCHMARK %s: %d"
-                    (string_of_domain_item dom_item) len);
+                  debug_print (lazy (sprintf "BENCHMARK %s: %d"
+                    (string_of_domain_item dom_item) len));
                   len
                 with No_choices _ -> 0)
               thing_dom
@@ -779,8 +782,10 @@ module Make (C: Callbacks) =
             interpretate_thing ~context:disambiguate_context ~env:filled_env
              ~uri ~is_path:false thing
           in
+let foo () =
           let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
             (k , ugraph1 )
+in refine_profiler.CicUtil.profile foo ()
         with
         | Try_again -> Uncertain, ugraph
         | Invalid_choice -> Ko, ugraph
@@ -794,16 +799,14 @@ module Make (C: Callbacks) =
                [ aliases, metasenv, thing, new_univ ]
             | Ko,_ | Uncertain,_ -> [])
         | item :: remaining_dom ->
-            debug_print (sprintf "CHOOSED ITEM: %s"
-             (string_of_domain_item item));
+            debug_print (lazy (sprintf "CHOOSED ITEM: %s"
+             (string_of_domain_item item)));
             let choices = lookup_choices item in
             let rec filter univ = function 
               | [] -> []
               | codomain_item :: tl ->
-                  debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
-                  let new_env =
-                    Environment.add item codomain_item aliases
-                  in
+                  debug_print (lazy (sprintf "%s CHOSEN" (fst codomain_item))) ;
+                  let new_env = Environment.add item codomain_item aliases in
                   (match test_env new_env remaining_dom univ with
                   | Ok (thing, metasenv),new_univ ->
                       (match remaining_dom with
@@ -825,10 +828,10 @@ module Make (C: Callbacks) =
          match aux aliases todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
          | [ e,me,t,u ] ->
-             debug_print "SINGLE INTERPRETATION";
+             debug_print (lazy "SINGLE INTERPRETATION");
              [ e,me,t,u ], false
          | l ->
-             debug_print (sprintf "MANY INTERPRETATIONS (%d)" (List.length l));
+             debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
              let choices =
                List.map
                  (fun (env, _, _, _) ->
@@ -847,20 +850,22 @@ module Make (C: Callbacks) =
 (*
         (if benchmark then
           let res_size = List.length res in
-          debug_print (sprintf
+          debug_print (lazy (sprintf
             ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
             "BENCHMARK:   estimated %.2f")
             !actual_refinements !max_refinements !domain_size res_size
             !choices_avg
-            (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
+            (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg))));
 *)
       let choices, b = res in
+let foo () =
       (List.map
         (fun (env, metasenv, t, ugraph) ->
           Environment.fold Environment.add env aliases,
           metasenv, t, ugraph)
         choices),
       b
+in disambiguate_environment_merge_profiler.CicUtil.profile foo ()
      with
       CicEnvironment.CircularDependency s -> 
         failwith "Disambiguate: circular dependency"