X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=a397de41e8fa3b8b82b930968a1ef1251d45baec;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=8d1108abe1dda13b1532a0356a387b97ba40cc1c;hpb=9e010764b6de0d8a268a6ecb83e8e90246bee129;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 8d1108abe..a397de41e 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -35,6 +35,7 @@ module PEH  = ProofEngineHelpers
 module TC   = CicTypeChecker 
 module Un   = CicUniv
 module L    = Librarian
+module Ut   = CicUtil
 
 module H    = ProceduralHelpers
 module Cl   = ProceduralClassify
@@ -45,6 +46,8 @@ let debug = ref false
 
 (* term optimization ********************************************************)
 
+let critical = ref true
+
 type status = {
    dummy: unit;
    info: string
@@ -52,7 +55,7 @@ type status = {
 
 let info st str = {st with info = st.info ^ str ^ "\n"}
 
-let defined_premise = "DEFINED"
+let defined_premise = "LOCAL"
 
 let define c v =
    let name = C.Name defined_premise in
@@ -67,8 +70,8 @@ let clear_absts m =
          aux 0 (pred n) (S.lift (-1) t)
       | t                  when n > 0 ->
          Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t);
-	 assert false 
-      | t                                 -> t
+         assert false
+      | t                             -> t
    in 
    aux m
 
@@ -78,7 +81,7 @@ let rec add_abst k = function
    | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
 
 let rec opt_letin g st es c name v w t =
-   let name = H.mk_fresh_name c name in
+   let name = H.mk_fresh_name true c name in
    let entry = Some (name, C.Def (v, w)) in
    let g st t =
       if DTI.does_not_occur 1 t then
@@ -96,7 +99,9 @@ let rec opt_letin g st es c name v w t =
          | v when H.is_proof c v && H.is_atomic v          ->
 	    let x = S.subst v t in
 	    opt_proof g (info st "Optimizer: remove 5") true c x 
-	 | v                                               ->
+(*	 | v when t = C.Rel 1                              ->
+	    g (info st "Optimizer: remove 6") v 
+*)	 | v                                               ->
 	    g st (C.LetIn (name, v, w, t))
       in
       if es then opt_term g st es c v else g st v
@@ -104,7 +109,7 @@ let rec opt_letin g st es c name v w t =
    if es then opt_proof g st es (entry :: c) t else g st t
 
 and opt_lambda g st es c name w t =
-   let name = H.mk_fresh_name c name in
+   let name = H.mk_fresh_name true c name in
    let entry = Some (name, C.Decl w) in
    let g st t = g st (C.Lambda (name, w, t)) in
    if es then opt_proof g st es (entry :: c) t else g st t
@@ -176,12 +181,16 @@ and opt_appl g st es c t vs =
    in
    if es then H.list_fold_right_cps g map vs (st, []) else g (st, vs)
 
-and opt_mutcase g st es c uri tyno outty arg cases =
+and opt_mutcase_critical g st es c uri tyno outty arg cases =   
    let eliminator = H.get_default_eliminator c uri tyno outty in
    let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
    let ps, sort_disp = H.get_ind_parameters c arg in
    let lps, rps = HEL.split_nth lpsno ps in
    let rpsno = List.length rps in
+   if rpsno = 0 && sort_disp = 0 then
+(* FG: the transformation is not possible, we fall back into the plain case *)
+      opt_mutcase_plain g st es c uri tyno outty arg cases
+   else
    let predicate = clear_absts rpsno (1 - sort_disp) outty in   
    let is_recursive t =
       I.S.mem tyno (I.get_mutinds_of_uri uri t) 
@@ -205,6 +214,19 @@ and opt_mutcase g st es c uri tyno outty arg cases =
    let x = H.refine c (C.Appl args) in
    opt_proof g (info st "Optimizer: remove 3") es c x
 
+and opt_mutcase_plain g st es c uri tyno outty arg cases =
+   let g st v =
+      let g (st, ts) = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+      let map h v (st, vs) =
+         let h st vv = h (st, vv :: vs) in opt_proof h st es c v
+      in
+      if es then H.list_fold_right_cps g map cases (st, []) else g (st, cases)
+   in
+   if es then opt_proof g st es c arg else g st arg
+
+and opt_mutcase g =
+   if !critical then opt_mutcase_critical g else opt_mutcase_plain g 
+
 and opt_cast g st es c t w =
    let g st t = g (info st "Optimizer: remove 4") t in
    if es then opt_proof g st es c t else g st t
@@ -237,23 +259,29 @@ let wrap g st c bo =
 
 let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
+      let count_nodes = I.count_nodes ~meta:false 0 in 
       let st, c = {info = ""; dummy = ()}, [] in
+      L.time_stamp ("PO: OPTIMIZING " ^ name);
+      let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in
+      if !debug then begin 
+         Printf.eprintf "BEGIN: %s\n" name;      
+         Printf.eprintf "Initial : %s\n" (Pp.ppterm bo); 
+	 prerr_string "Ut.pp_term : ";
+	 Ut.pp_term prerr_string [] c bo; prerr_newline ()
+      end;
       let bo, ty = H.cic_bc c bo, H.cic_bc c ty in 
       let g st bo =
 	 if !debug then begin 
 	    Printf.eprintf "Optimized : %s\n" (Pp.ppterm bo); 
-	    prerr_string "H.pp_term : ";
-	    H.pp_term prerr_string [] c bo; prerr_newline ()
+	    prerr_string "Ut.pp_term : ";
+	    Ut.pp_term prerr_string [] c bo; prerr_newline ()
 	 end;
 (*	 let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *)
-         let nodes = Printf.sprintf "Optimized nodes: %u" (I.count_nodes 0 bo) in
+         let nodes = Printf.sprintf "Optimized nodes: %u" (count_nodes bo) in
 	 let st = info st nodes in
 	 L.time_stamp ("PO: DONE       " ^ name);
 	 C.Constant (name, Some bo, ty, pars, attrs), st.info
       in
-      L.time_stamp ("PO: OPTIMIZING " ^ name);
-      if !debug then Printf.eprintf "BEGIN: %s\n" name;
-      let nodes = Printf.sprintf "Initial nodes: %u" (I.count_nodes 0 bo) in
       wrap g (info st nodes) c bo
    | obj                                         -> obj, ""