X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=3ac5670956e91e3c4407985007b3a519b118d386;hb=2b53a3735b2a6130726e0a0451993cd679fd5935;hp=67b3af94091650d924b0269fe2af8d1f04c077c7;hpb=e64013e67dc485047940b77022078a2fcaad1813;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 67b3af940..3ac567095 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -23,24 +23,34 @@
  * 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 define v =
+let define c v =
    let name = C.Name defined_premise in
-   C.LetIn (name, v, C.Rel 1)
+   let ty = H.get_type "define" c v in
+   C.LetIn (name, v, ty, C.Rel 1)
 
 let clear_absts m =
    let rec aux k n = function
@@ -49,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 
@@ -60,20 +70,26 @@ let rec add_abst k = function
    | t when k > 0 -> assert false
    | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
 
-let rec opt1_letin g es c name v t =
+let rec opt1_letin g es c name v w t =
    let name = H.mk_fresh_name c name in
-   let entry = Some (name, C.Def (v, None)) in
+   let entry = Some (name, C.Def (v, w)) in
    let g t =
       if DTI.does_not_occur 1 t then begin	    
          let x = S.lift (-1) t in
 	 HLog.warn "Optimizer: remove 1"; opt1_proof g true c x 
       end else 
       let g = function
-         | C.LetIn (nname, vv, tt) when H.is_proof c v ->
-	    let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
+         | C.LetIn (nname, vv, ww, tt) when H.is_proof c v ->
+	    let eentry = Some (nname, C.Def (vv, ww)) 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 
-         | v                               -> 
-	    g (C.LetIn (name, v, t))
+         | v when H.is_proof c v && H.is_atomic v     ->
+	    let x = S.subst v t in
+	    HLog.warn "Optimizer: remove 5"; opt1_proof g true c x 
+	 | v                                           ->
+	    g (C.LetIn (name, v, w, t))
       in
       if es then opt1_term g es c v else g v
    in
@@ -82,22 +98,20 @@ let rec opt1_letin g es c name v t =
 and opt1_lambda g es c name w t =
    let name = H.mk_fresh_name c name in
    let entry = Some (name, C.Decl w) in
-   let g t = 
-      let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
-      g (C.Lambda (name, w, t))
-   in
+   let g t = g (C.Lambda (name, w, t)) in
    if es then opt1_proof g es (entry :: c) t else g t
 
 and opt1_appl g es c t vs =
    let g vs = 
       let g = function      
-         | C.LetIn (mame, vv, tt) ->
+         | C.LetIn (mame, vv, tyty, tt) ->
             let vs = List.map (S.lift 1) vs in
-	    let x = C.LetIn (mame, vv, C.Appl (tt :: vs)) in
+	    let x = C.LetIn (mame, vv, tyty, C.Appl (tt :: vs)) in
 	    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 x = C.Appl (C.LetIn (name, v, tt) :: vs) 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              ->
             let x = C.Appl (vvs @ vs) in
@@ -110,21 +124,21 @@ and opt1_appl g es c t vs =
 	       | v :: vs, (cc, bb) :: cs ->
 	          if H.is_not_atomic v && I.S.mem 0 cc && bb then begin 
 		     HLog.warn "Optimizer: anticipate 1"; 
-                     aux true (define v :: rvs) (vs, cs)
+                     aux true (define c v :: rvs) (vs, cs)
 		  end else 
 		     aux d (v :: rvs) (vs, cs)
 	       | _, []                   -> 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
-		  let x = C.Appl (define (C.Appl (t :: vvs)) :: vs) in
+		  let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in
 	          HLog.warn "Optimizer: anticipate 2"; opt1_proof g true c x
 	       else match conclusion, List.rev vs with
 	          | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv ->
-		     let x = C.Appl (t :: List.rev rvs @ [define rv]) in
+		     let x = C.Appl (t :: List.rev rvs @ [define c rv]) in
 		     HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x
 	          | _ (* Some _, _ *)                                             ->
 		     g (C.Appl (t :: vs))
@@ -132,12 +146,13 @@ and opt1_appl g es c t vs =
 	             aux false [] (vs, classes)
 *)	    in
 	    let rec aux h prev = function
-	       | C.LetIn (name, vv, tt) :: vs ->
+	       | C.LetIn (name, vv, tyty, tt) :: vs ->
 	          let t = S.lift 1 t in
                   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 x = C.LetIn (name, vv, y) 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
 	       | []                           -> h ()
@@ -184,7 +199,7 @@ and opt1_cast g es c t w =
 and opt1_other g es c t = g t 
 
 and opt1_proof g es c = function 
-   | C.LetIn (name, v, t)       -> opt1_letin g es c name v t
+   | C.LetIn (name, v, ty, t)   -> opt1_letin g es c name v ty t
    | C.Lambda (name, w, t)      -> opt1_lambda g es c name w t
    | C.Appl (t :: v :: vs)      -> opt1_appl g es c t (v :: vs)
    | C.Appl [t]                 -> opt1_proof g es c t
@@ -216,10 +231,10 @@ let eta_expand g tys t =
    in
    g (absts t)
 
-let rec opt2_letin g c name v t =
-   let entry = Some (name, C.Def (v, None)) in
+let rec opt2_letin g c name v w t =
+   let entry = Some (name, C.Def (v, w)) in
    let g t = 
-      let g v = g (C.LetIn (name, v, t)) in
+      let g v = g (C.LetIn (name, v, w, t)) in
       opt2_term g c v
    in
    opt2_proof g (entry :: c) t
@@ -233,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
@@ -244,17 +259,17 @@ 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 
    end else g t
 
 and opt2_proof g c = function 
-   | C.LetIn (name, v, t)  -> opt2_letin g c name v t
-   | C.Lambda (name, w, t) -> opt2_lambda g c name w t
-   | C.Appl (t :: vs)      -> opt2_appl g c t vs
-   | t                     -> opt2_other g c t
+   | C.LetIn (name, v, w, t) -> opt2_letin g c name v w t
+   | C.Lambda (name, w, t)   -> opt2_lambda g c name w t
+   | C.Appl (t :: vs)        -> opt2_appl g c t vs
+   | t                       -> opt2_other g c t
 
 and opt2_term g c t = 
    if H.is_proof c t then opt2_proof g c t else g t
@@ -263,12 +278,28 @@ and opt2_term g c t =
 
 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\n" (Pp.ppterm 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\n" name;
-      begin try opt1_term (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