librarian: improved error detection, bug fix in time comparison functions: now the...

[helm.git] / helm / software / components / acic_procedural / proceduralOptimizer.ml

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 776d52645901dbbb316b6caea9ee03a9d9c01637..3ac5670956e91e3c4407985007b3a519b118d386 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -23,32 +23,33 @@
  * http://cs.unibo.it/helm/.
  *)
 
+module UM   = UriManager
 module C    = Cic
 module Pp   = CicPp
 module I    = CicInspect
+module E    = CicEnvironment
 module S    = CicSubstitution
 module DTI  = DoubleTypeInference
 module HEL  = HExtlib
 module PEH  = ProofEngineHelpers
 module TC   = CicTypeChecker 
 module Un   = CicUniv
+module L    = Librarian
 
 module H    = ProceduralHelpers
 module Cl   = ProceduralClassify
 
+(* debugging ****************************************************************)
+
+let debug = ref false
+
 (* term preprocessing: optomization 1 ***************************************)
 
 let defined_premise = "DEFINED"
 
-let get_type msg c bo =
-try   
-   let ty, _ = TC.type_of_aux' [] c bo Un.empty_ugraph in
-   ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
 let define c v =
    let name = C.Name defined_premise in
-   let ty = get_type "define" c v in
+   let ty = H.get_type "define" c v in
    C.LetIn (name, v, ty, C.Rel 1)
 
 let clear_absts m =
@@ -58,7 +59,7 @@ let clear_absts m =
       | C.Lambda (_, _, t) when n > 0 -> 
          aux 0 (pred n) (S.lift (-1) t)
       | t                  when n > 0 ->
-         Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t);
+         Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t);
         assert false 
       | t                                 -> t
    in 
@@ -80,7 +81,7 @@ let rec opt1_letin g es c name v w t =
       let g = function
          | C.LetIn (nname, vv, ww, tt) when H.is_proof c v ->
            let eentry = Some (nname, C.Def (vv, ww)) in
-           let ttw = get_type "opt1_letin 1" (eentry :: c) tt in
+           let ttw = H.get_type "opt1_letin 1" (eentry :: c) tt in
            let x = C.LetIn (nname, vv, ww,
              C.LetIn (name, tt, ttw, S.lift_from 2 1 t)) in
            HLog.warn "Optimizer: swap 1"; opt1_proof g true c x 
@@ -109,7 +110,7 @@ and opt1_appl g es c t vs =
            HLog.warn "Optimizer: swap 2"; opt1_proof g true c x
          | C.Lambda (name, ww, tt) ->
            let v, vs = List.hd vs, List.tl vs in
-            let w = get_type "opt1_appl 1" c v in
+            let w = H.get_type "opt1_appl 1" c v in
            let x = C.Appl (C.LetIn (name, v, w, tt) :: vs) in
            HLog.warn "Optimizer: remove 2"; opt1_proof g true c x
         | C.Appl vvs              ->
@@ -129,7 +130,7 @@ and opt1_appl g es c t vs =
               | _, []                   -> assert false
            in
            let h () =
-              let classes, conclusion = Cl.classify c (H.get_type c t) in
+              let classes, conclusion = Cl.classify c (H.get_type "opt1_appl 3" c t) in
               let csno, vsno = List.length classes, List.length vs in
               if csno < vsno then
                  let vvs, vs = HEL.split_nth csno vs in
@@ -150,7 +151,7 @@ and opt1_appl g es c t vs =
                   let prev = List.map (S.lift 1) prev in
                   let vs = List.map (S.lift 1) vs in
                  let y = C.Appl (t :: List.rev prev @ tt :: vs) in
-                  let ww = get_type "opt1_appl 2" c vv in
+                  let ww = H.get_type "opt1_appl 2" c vv in
                  let x = C.LetIn (name, vv, ww, y) in  
                  HLog.warn "Optimizer: swap 3"; opt1_proof g true c x
               | v :: vs                      -> aux h (v :: prev) vs
@@ -247,9 +248,9 @@ and opt2_appl g c t vs =
    let g vs =
       let x = C.Appl (t :: vs) in
       let vsno = List.length vs in
-      let _, csno = PEH.split_with_whd (c, H.get_type c t) in
+      let _, csno = PEH.split_with_whd (c, H.get_type "opt2_appl 1" c t) in
       if vsno < csno then 
-         let tys, _ = PEH.split_with_whd (c, H.get_type c x) in
+         let tys, _ = PEH.split_with_whd (c, H.get_type "opt2_appl 2" c x) in
         let tys = List.rev (List.tl tys) in
         let tys, _ = HEL.split_nth (csno - vsno) tys in
          HLog.warn "Optimizer: eta 1"; eta_expand g tys x
@@ -258,7 +259,7 @@ and opt2_appl g c t vs =
    H.list_map_cps g (fun h -> opt2_term h c) vs
 
 and opt2_other g c t =
-   let tys, csno = PEH.split_with_whd (c, H.get_type c t) in
+   let tys, csno = PEH.split_with_whd (c, H.get_type "opt2_other" c t) in
    if csno > 0 then begin
       let tys = List.rev (List.tl tys) in      
       HLog.warn "Optimizer: eta 2"; eta_expand g tys t 
@@ -279,13 +280,26 @@ let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
       let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in 
       let g bo = 
-         Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" 
-           (Pp.ppterm bo) (I.count_nodes 0 bo);
-        let _ = H.get_type [] (C.Cast (bo, ty)) in
+         if !debug then begin 
+           Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" 
+              (Pp.ppterm bo) (I.count_nodes 0 bo);
+           prerr_string "H.pp_term : ";
+           H.pp_term prerr_string [] [] bo; prerr_newline ()
+        end;
+(*      let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *)
+        L.time_stamp ("PO: DONE       " ^ name);
         C.Constant (name, Some bo, ty, pars, attrs)
       in
-      Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" 
-         name (I.count_nodes 0 bo);
-      begin try opt1_term g (* (opt2_term g []) *) true [] bo
-      with e -> failwith ("PPP: " ^ Printexc.to_string e) end
+         L.time_stamp ("PO: OPTIMIZING " ^ name);
+      if !debug then
+         Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" 
+            name (I.count_nodes 0 bo);
+      begin try opt1_term g (* (opt2_term g []) *) true [] bo with
+        | E.Object_not_found uri ->
+          let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in
+          failwith msg 
+        | e                      -> 
+          let msg = "optimize_obj: " ^ Printexc.to_string e in
+          failwith msg
+      end
    | obj                                         -> obj