]> matita.cs.unibo.it Git - helm.git/commitdiff
Optimizer: refactored according to its formal description
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 30 Mar 2007 21:54:45 +0000 (21:54 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 30 Mar 2007 21:54:45 +0000 (21:54 +0000)
helm/software/components/acic_procedural/.depend
helm/software/components/acic_procedural/.depend.opt
helm/software/components/acic_procedural/Makefile
helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralClassify.ml
helm/software/components/acic_procedural/proceduralClassify.mli
helm/software/components/acic_procedural/proceduralPreprocess.ml

index 3bb617fbda4d8834a3e6e0fbada711cd69798fa0..c1c6561c2e348270548de73450a92b54550bd84f 100644 (file)
@@ -1,9 +1,9 @@
-proceduralPreprocess.cmo: proceduralPreprocess.cmi 
-proceduralPreprocess.cmx: proceduralPreprocess.cmi 
-proceduralTypes.cmo: proceduralTypes.cmi 
-proceduralTypes.cmx: proceduralTypes.cmi 
 proceduralClassify.cmo: proceduralClassify.cmi 
 proceduralClassify.cmx: proceduralClassify.cmi 
+proceduralPreprocess.cmo: proceduralClassify.cmi proceduralPreprocess.cmi 
+proceduralPreprocess.cmx: proceduralClassify.cmx proceduralPreprocess.cmi 
+proceduralTypes.cmo: proceduralTypes.cmi 
+proceduralTypes.cmx: proceduralTypes.cmi 
 proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
@@ -11,8 +11,6 @@ proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
 proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
     proceduralMode.cmx proceduralConversion.cmi 
 acic2Procedural.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
-    proceduralMode.cmi proceduralConversion.cmi proceduralClassify.cmi \
-    acic2Procedural.cmi 
+    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
 acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
-    proceduralMode.cmx proceduralConversion.cmx proceduralClassify.cmx \
-    acic2Procedural.cmi 
+    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
index 3bb617fbda4d8834a3e6e0fbada711cd69798fa0..c1c6561c2e348270548de73450a92b54550bd84f 100644 (file)
@@ -1,9 +1,9 @@
-proceduralPreprocess.cmo: proceduralPreprocess.cmi 
-proceduralPreprocess.cmx: proceduralPreprocess.cmi 
-proceduralTypes.cmo: proceduralTypes.cmi 
-proceduralTypes.cmx: proceduralTypes.cmi 
 proceduralClassify.cmo: proceduralClassify.cmi 
 proceduralClassify.cmx: proceduralClassify.cmi 
+proceduralPreprocess.cmo: proceduralClassify.cmi proceduralPreprocess.cmi 
+proceduralPreprocess.cmx: proceduralClassify.cmx proceduralPreprocess.cmi 
+proceduralTypes.cmo: proceduralTypes.cmi 
+proceduralTypes.cmx: proceduralTypes.cmi 
 proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
@@ -11,8 +11,6 @@ proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
 proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
     proceduralMode.cmx proceduralConversion.cmi 
 acic2Procedural.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
-    proceduralMode.cmi proceduralConversion.cmi proceduralClassify.cmi \
-    acic2Procedural.cmi 
+    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
 acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
-    proceduralMode.cmx proceduralConversion.cmx proceduralClassify.cmx \
-    acic2Procedural.cmi 
+    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
index 379f5518bdccedb66f1b616e374915e5e9590557..780462786136d3b9a909e020cba1097882737829 100644 (file)
@@ -2,9 +2,9 @@ PACKAGE = acic_procedural
 PREDICATES =
 
 INTERFACE_FILES =               \
+       proceduralClassify.mli   \
        proceduralPreprocess.mli \
        proceduralTypes.mli      \
-       proceduralClassify.mli   \
        proceduralMode.mli       \
        proceduralConversion.mli \
        acic2Procedural.mli      \
index d6638b3f07f5f294d227150f2ad908aca997e38e..3cf4bb596b38a4cd36c20262bc28b2ce67fc6929 100644 (file)
@@ -37,10 +37,10 @@ module Ut   = CicUtil
 module E    = CicEnvironment
 module PEH  = ProofEngineHelpers
 module PER  = ProofEngineReduction
+module Pp   = CicPp
 
 module P    = ProceduralPreprocess
 module Cl   = ProceduralClassify
-module M    = ProceduralMode
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
 
@@ -161,8 +161,6 @@ with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
 let unused_premise = "UNUSED"
 
-let defined_premise = "DEFINED"
-
 let convert st ?name v = 
    match get_inner_types st v with
       | None          -> []
@@ -174,13 +172,9 @@ let convert st ?name v =
            | None    -> [T.Change (st, et, None, e, "")]
            | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
 
-let get_intro name t = 
-try
-match name with 
+let get_intro = function 
    | C.Anonymous -> unused_premise
-   | C.Name s    -> 
-      if DTI.does_not_occur 1 (cic t) then unused_premise else s
-with Invalid_argument _ -> failwith "A2P.get_intro"
+   | C.Name s    -> s
 
 let mk_intros st script =
 try
@@ -189,15 +183,9 @@ try
    T.Intros (Some count, List.rev st.intros, "") :: script
 with Invalid_argument _ -> failwith "A2P.mk_intros"
 
-let rec mk_atomic st dtext what =
-   if T.is_atomic what then 
-      match what with 
-      | C.ARel (_, _, _, name) -> convert st ~name what, what
-      | _                      -> [], what
-   else
-      let name = defined_premise in
-      let script = convert st ~name what in  
-      script @ mk_fwd_proof st dtext name what, T.mk_arel 0 name
+let rec mk_arg st = function
+   | C.ARel (_, _, _, name) as what -> convert st ~name what, what
+   | what                           -> [], what
 
 and mk_fwd_rewrite st dtext name tl direction =   
    assert (List.length tl = 6);
@@ -205,7 +193,7 @@ and mk_fwd_rewrite st dtext name tl direction =
    let e = Cn.mk_pattern 1 predicate in
    match where with
       | C.ARel (_, _, _, premise) ->
-         let script, what = mk_atomic st dtext what in
+         let script, what = mk_arg st what in
          T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script
       | _                         -> assert false
 
@@ -217,21 +205,15 @@ and mk_rewrite st dtext script t what qs tl direction =
    [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
 
 and mk_fwd_proof st dtext name = function
-   | C.ALetIn (_, n, v, t)      ->
-      let entry = Some (n, C.Def (cic v, None)) in
-      let intro = get_intro n t in
-      let qt = mk_fwd_proof (add st entry intro) dtext name t in
-      let qv = mk_fwd_proof st "" intro v in
-      List.append qt qv
    | C.AAppl (_, hd :: tl) as v -> 
       if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
       if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else
       let ty = get_type "TC1" st hd in
       begin match get_inner_types st v with
-         | Some (ity, _) when M.bkd st.context ty ->
+         | Some (ity, _) ->
            let qs = [[T.Id ""]; mk_proof (next st) v] in
            [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
-         | _                                      ->
+         | _             ->
             let (classes, rc) as h = Cl.classify st.context ty in
             let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
            [T.LetIn (name, v, dtext ^ text)]
@@ -249,13 +231,13 @@ and mk_fwd_proof st dtext name = function
 and mk_proof st = function
    | C.ALambda (_, name, v, t)        ->
       let entry = Some (name, C.Decl (cic v)) in
-      let intro = get_intro name in
+      let intro = get_intro name in
       mk_proof (add st entry intro) t
    | C.ALetIn (_, name, v, t) as what ->
       let proceed, dtext = test_depth st in
       let script = if proceed then 
          let entry = Some (name, C.Def (cic v, None)) in
-         let intro = get_intro name in
+         let intro = get_intro name in
          let q = mk_proof (next (add st entry intro)) t in
          List.rev_append (mk_fwd_proof st dtext intro v) q
       else
@@ -276,14 +258,19 @@ and mk_proof st = function
       let script = if proceed then
          let ty = get_type "TC2" st hd in
          let (classes, rc) as h = Cl.classify st.context ty in
-         let premises, _ = PEH.split_with_whd (st.context, ty) in
-        assert (List.length classes - List.length tl = 0);
+        let decurry = List.length classes - List.length tl in
+        if decurry <> 0 then begin
+           let msg = Printf.sprintf "Decurry: %i\nTerm: %s\nContext: %s"
+              decurry (Pp.ppterm (cic t)) (Pp.ppcontext st.context)
+           in
+           HLog.warn msg; assert false
+        end;
         let synth = I.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
          match rc with
-            | Some (i, j) when i > 1 && i <= List.length classes && M.is_eliminator premises ->
+            | Some (i, j) ->
               let classes, tl, _, what = split2_last classes tl in
-              let script, what = mk_atomic st dtext what in
+              let script, what = mk_arg st what in
               let synth = I.S.add 1 synth in
               let qs = mk_bkd_proofs (next st) synth classes tl in
                if is_rewrite_right hd then 
@@ -293,13 +280,13 @@ and mk_proof st = function
               else   
                   let l = succ (List.length tl) in
                  let predicate = List.nth tl (l - i) in
-                  let e = Cn.mk_pattern j predicate in
+                  let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in
                  let using = Some hd in
                  List.rev script @ convert st t @
                  [T.Elim (what, using, e, dtext ^ text); T.Branch (qs, "")]
-           | _                                                  ->
+           | None        ->
               let qs = mk_bkd_proofs (next st) synth classes tl in
-              let script, hd = mk_atomic st dtext hd in               
+              let script, hd = mk_arg st hd in               
               List.rev script @ convert st t @        
               [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
       else
@@ -316,7 +303,7 @@ and mk_proof st = function
 and mk_bkd_proofs st synth classes ts =
 try 
    let _, dtext = test_depth st in   
-   let aux inv v =
+   let aux (inv, _) v =
       if I.overlaps synth inv then None else
       if I.S.is_empty inv then Some (mk_proof st v) else
       Some [T.Apply (v, dtext ^ "dependent")]
index d21c14601f5108502d27de3c34f1511e3b89c3ab..6c1e482c2ff4d86aee5ee01cb988e50ece825630 100644 (file)
@@ -28,12 +28,14 @@ module D   = Deannotate
 module I   = CicInspect
 module PEH = ProofEngineHelpers
 
+type dependence = I.S.t * bool
+
 type conclusion = (int * int) option
 
 (* debugging ****************************************************************)
 
-let string_of_entry inverse =
-   if I.S.mem 0 inverse then "C" else
+let string_of_entry (inverse, b) =
+   if I.S.mem 0 inverse then begin if b then "CF" else "C" end else
    if I.S.is_empty inverse then "I" else "P"
 
 let to_string (classes, rc) =
@@ -53,25 +55,43 @@ let out_table b =
    
 (****************************************************************************)
 
-let id x = x
+let identity x = x
 
-let classify_conclusion = function
-   | _, C.Rel i                -> Some (i, 0)
-   | _, C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
-   | _                         -> None
+let fst3 (x, _, _) = x
 
+let classify_conclusion vs = 
+   let rec get_argsno = function
+      | c, C.Appl (t :: vs) -> 
+         let hd, argsno = get_argsno (c, t) in 
+         hd, argsno + List.length vs
+      | _, t                -> t, 0
+   in
+   let inside i = i > 1 && i <= List.length vs in
+   match vs with
+      | v0 :: v1 :: _ ->
+         let hd0, argsno0 = get_argsno v0 in
+        let hd1, argsno1 = get_argsno v1 in
+        begin match hd0, hd1 with
+           | C.Rel i, C.MutInd _ when inside i -> Some (i, argsno0)
+           | _                                 -> None
+        end
+      | _             -> None
 let classify c t =
 try   
    let vs, h = PEH.split_with_whd (c, t) in
-   let rc = classify_conclusion (List.hd vs) in
-   let map (b, h) (_, v) = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in
+   let rc = classify_conclusion vs in
+   let map (b, h) (c, v) = 
+      let _, argsno = PEH.split_with_whd (c, v) in
+      (I.get_rels_from_premise h v, I.S.empty, argsno > 0) :: b, succ h
+   in
    let l, h = List.fold_left map ([], 0) vs in
    let b = Array.of_list (List.rev l) in
    let mk_closure b h =
-      let map j = if j < h then I.S.union (fst b.(j)) else id in 
+      let map j = if j < h then I.S.union (fst3 b.(j)) else identity in 
       for i = pred h downto 0 do
-         let direct, unused = b.(i) in
-        b.(i) <- I.S.fold map direct direct, unused 
+         let direct, unused, fa = b.(i) in
+        b.(i) <- I.S.fold map direct direct, unused, fa 
       done; b
    in
    let b = mk_closure b h in
@@ -79,13 +99,14 @@ try
       if I.S.is_empty direct then () else
       let j = I.S.choose direct in
       if j < h then
-         let unused, inverse = b.(j) in 
-         b.(j) <- unused, I.S.add i inverse
+         let unused, inverse, fa = b.(j) in 
+         b.(j) <- unused, I.S.add i inverse, fa
        else ();
        mk_inverse i (I.S.remove j direct)
    in
-   let map i (direct, _) = mk_inverse i direct in
+   let map i (direct, _, _) = mk_inverse i direct in
    Array.iteri map b;
 (*   out_table b; *)
-   List.rev_map snd (List.tl (Array.to_list b)), rc
+   let extract (x, y, z) = y, z in
+   List.rev_map extract (List.tl (Array.to_list b)), rc
 with Invalid_argument _ -> failwith "Classify.classify"
index 90c2c785262819efebab53563ff1bc3dea4056b4..9e478ca622c595cdb40d905f031f2c906674a029 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
+type dependence = CicInspect.S.t * bool
+
 type conclusion = (int * int) option
 
-val classify: Cic.context -> Cic.term -> CicInspect.S.t list * conclusion
+val classify: Cic.context -> Cic.term -> dependence list * conclusion
 
-val to_string: CicInspect.S.t list * conclusion -> string
+val to_string: dependence list * conclusion -> string
index d3e655da70ea6ee20f54674c8782bb5f0deed028..6b84dd9b9a823757fe06858147c5ab47500203d7 100644 (file)
@@ -36,19 +36,23 @@ module DTI  = DoubleTypeInference
 module HEL  = HExtlib
 module PEH  = ProofEngineHelpers
 
+module Cl   = ProceduralClassify
+
 (* helper functions *********************************************************)
 
+let rec list_map_cps g map = function
+   | []       -> g []
+   | hd :: tl -> 
+      let h hd =
+         let g tl = g (hd :: tl) in
+         list_map_cps g map tl  
+      in
+      map h hd
+
 let identity x = x
 
 let comp f g x = f (g x)
 
-let get_type c t =
-   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
-   with e -> 
-      Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
-      Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
-      raise e
-
 let refine c t =
    try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
    with e -> 
@@ -57,6 +61,13 @@ let refine c t =
       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
       raise e
 
+let get_type c t =
+   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+   with e -> 
+      Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
+      Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
+      raise e
+
 let get_tail c t =
    match PEH.split_with_whd (c, t) with
       | (_, hd) :: _, _ -> hd
@@ -77,43 +88,11 @@ let is_not_atomic = function
    | C.MutConstruct _ -> false
    | _                -> true
 
-let clear_absts m =
-   let rec aux k n = function
-      | C.Lambda (s, v, t) when k > 0    -> 
-         C.Lambda (s, v, aux (pred k) n t)
-      | 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);
-        assert false 
-      | t                                 -> t
-   in 
-   aux m
-
-let rec add_abst k = function 
-   | C.Lambda (s, v, t) when k > 0 -> C.Lambda (s, v, add_abst (pred k) t)
-   | t when k > 0 -> assert false
-   | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
-
 let get_ind_type uri tyno =
    match E.get_obj Un.empty_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
       | _                                           -> assert false
 
-let get_ind_parameters c t =
-   let ty = get_type c t in
-   let ps = match get_tail c ty with
-      | C.MutInd _                  -> []
-      | C.Appl (C.MutInd _ :: args) -> args
-      | _                           -> assert false
-   in
-   let disp = match get_tail c (get_type c ty) with
-      | C.Sort C.Prop -> 0
-      | C.Sort _      -> 1
-      | _             -> assert false
-   in
-   ps, disp
-
 let get_default_eliminator context uri tyno ty =
    let _, (name, _, _, _) = get_ind_type uri tyno in
    let ext = match get_tail context (get_type context ty) with
@@ -129,123 +108,133 @@ let get_default_eliminator context uri tyno ty =
    let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
    C.Const (uri, [])
 
-let add g htbl t proof decurry =
-   if proof then C.CicHash.add htbl t decurry; 
-   g t proof decurry
-
-let find g htbl t = 
-   try 
-      let decurry = C.CicHash.find htbl t in g t true decurry
-   with Not_found -> g t false 0
-
-(* term preprocessing *******************************************************)
+let get_ind_parameters c t =
+   let ty = get_type c t in
+   let ps = match get_tail c ty with
+      | C.MutInd _                  -> []
+      | C.Appl (C.MutInd _ :: args) -> args
+      | _                           -> assert false
+   in
+   let disp = match get_tail c (get_type c ty) with
+      | C.Sort C.Prop -> 0
+      | C.Sort _      -> 1
+      | _             -> assert false
+   in
+   ps, disp
 
-let expanded_premise = "EXPANDED"
+(* term preprocessing: optomization 1 ***************************************)
 
 let defined_premise = "DEFINED"
 
-let eta_expand g tys t =
-   assert (tys <> []);
-   let name i = Printf.sprintf "%s%u" expanded_premise i in 
-   let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
-   let arg i = C.Rel (succ i) in
-   let rec aux i f a = function
-      | []            -> f, a 
-      | (_, ty) :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
-   in
-   let n = List.length tys in
-   let absts, args = aux 0 identity [] tys in
-   let t = match S.lift n t with
-      | C.Appl ts -> C.Appl (ts @ args)
-      | t         -> C.Appl (t :: args)
-   in
-   g (absts t)
+let define c v =
+   let name = C.Name defined_premise in
+   C.LetIn (name, v, C.Rel 1)
 
-let get_tys c decurry =
-   let rec aux n = function
-(*      | C.Appl (hd :: tl) -> aux (n + List.length tl) hd *)
-      | t                 ->
-         let tys, _ = PEH.split_with_whd (c, get_type c t) in
-         let _, tys = HEL.split_nth n (List.rev tys) in
-        let tys, _ = HEL.split_nth decurry tys in
-         tys
-   in
-   aux 0
-
-let eta_fix c t proof decurry =
-   let rec aux g c = function
-      | C.LetIn (name, v, t) ->
-         let g t = g (C.LetIn (name, v, t)) in
-        let entry = Some (name, C.Def (v, None)) in
-         aux g (entry :: c) t
-      | t                    -> eta_expand g (get_tys c decurry t) t 
+let clear_absts m =
+   let rec aux k n = function
+      | C.Lambda (s, v, t) when k > 0    -> 
+         C.Lambda (s, v, aux (pred k) n t)
+      | 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);
+        assert false 
+      | t                                 -> t
    in 
-   if proof && decurry > 0 then aux identity c t else t
-
-let rec pp_cast g ht es c t v =
-   if true then pp_proof g ht es c t else find g ht t
+   aux m
 
-and pp_lambda g ht es c name v t =
-   let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
-   let entry = Some (name, C.Decl v) in
-   let g t _ decurry = 
-      let t = eta_fix (entry :: c) t true decurry in
-      g (C.Lambda (name, v, t)) true 0 in
-   if true then pp_proof g ht es (entry :: c) t else find g ht t
+let rec add_abst k = function 
+   | C.Lambda (s, v, t) when k > 0 -> C.Lambda (s, v, add_abst (pred k) t)
+   | t when k > 0 -> assert false
+   | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
 
-and pp_letin g ht es c name v t =
+let rec opt1_letin g es c name v t =
    let entry = Some (name, C.Def (v, None)) in
-   let g t _ decurry =
-      if DTI.does_not_occur 1 t then g (S.lift (-1) t) true decurry else 
-      let g v proof d = match v with
-         | C.LetIn (mame, w, u) when proof ->
-            let x = C.LetIn (mame, w, C.LetIn (name, u, S.lift_from 2 1 t)) in
-           pp_proof g ht false c x 
+   let g t =
+      if DTI.does_not_occur 1 t then begin         
+         HLog.warn "Optimizer: remove 1"; g (S.lift (-1) t)
+      end else 
+      let g = function
+         | C.LetIn (nname, vv, tt) when is_proof c v ->
+            let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
+           HLog.warn "Optimizer: swap 1"; opt1_proof g false c x 
          | v                               -> 
-            let v = eta_fix c v proof d in
-           g (C.LetIn (name, v, t)) true decurry
+           g (C.LetIn (name, v, t))
       in
-      if true then pp_term g ht es c v else find g ht v
+      if es then opt1_term g es c v else g v
+   in
+   if es then opt1_proof g es (entry :: c) t else g t
+
+and opt1_lambda g es c name w t =
+   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
-   if true then pp_proof g ht es (entry :: c) t else find g ht t
-
-and pp_appl_one g ht es c t v =
-   let g t _ decurry =
-      let g v proof d =
-         match t, v with
-           | t, C.LetIn (mame, w, u) when proof ->
-               let x = C.LetIn (mame, w, C.Appl [S.lift 1 t; u]) in
-              pp_proof g ht false c x 
-            | C.LetIn (mame, w, u), v            ->
-               let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in
-              pp_proof g ht false c x
-           | C.Appl ts, v when decurry > 0      ->
-              let v = eta_fix c v proof d in
-              g (C.Appl (List.append ts [v])) true (pred decurry)
-           | t, v  when is_not_atomic t         ->
-              let mame = C.Name defined_premise in
-              let x = C.LetIn (mame, t, C.Appl [C.Rel 1; S.lift 1 v]) in
-              pp_proof g ht false c x
-           | t, v                               ->
-              let v = eta_fix c v proof d in
-               g (C.Appl [t; v]) true (pred decurry)
+   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) ->
+            let vs = List.map (S.lift 1) vs in
+           let x = C.LetIn (mame, vv, C.Appl (tt :: vs)) in
+           HLog.warn "Optimizer: swap 2"; opt1_proof g false 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
+           HLog.warn "Optimizer: remove 2"; opt1_proof g false c x
+        | C.Appl vvs              ->
+            let x = C.Appl (vvs @ vs) in
+           HLog.warn "Optimizer: nested application"; opt1_proof g false c x
+        | t                       ->
+           let rec aux d rvs = function
+              | [], _                 -> 
+                 let x = C.Appl (t :: List.rev rvs) in
+                 if d then opt1_proof g false c x else g x
+              | v :: vs, (c, b) :: cs ->
+                 if is_not_atomic v && I.S.mem 0 c && b then begin 
+                    HLog.warn "Optimizer: anticipate 1"; 
+                    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 (get_type c t) in
+              let csno, vsno = List.length classes, List.length vs in
+              if csno < vsno && csno > 0 then
+                 let vvs, vs = HEL.split_nth csno vs in
+                 let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in
+                 HLog.warn "Optimizer: anticipate 2"; opt1_proof g false c x
+              else match conclusion, List.rev vs with
+                 | Some _, rv :: rvs when csno = vsno && is_not_atomic rv ->
+                    let x = C.Appl (t :: List.rev rvs @ [define c rv]) in
+                    HLog.warn "Optimizer: anticipate 3"; opt1_proof g false c x
+                 | Some _, _                                              ->
+                    g (C.Appl (t :: vs))
+                 | None, _                                                ->
+                    if csno > 0 then aux false [] (vs, classes)
+                    else g (C.Appl (t :: vs))
+           in
+           let rec aux h prev = function
+              | C.LetIn (name, vv, 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  
+                 HLog.warn "Optimizer: swap 3"; opt1_proof g false c x
+              | v :: vs                      -> aux h (v :: prev) vs
+              | []                           -> h ()
+           in 
+           aux h [] vs
       in
-      if true then pp_term g ht es c v else find g ht v
+      if es then opt1_proof g es c t else g t
    in
-   if true then pp_proof g ht es c t else find g ht t
-
-and pp_appl g ht es c t = function
-   | []             -> pp_proof g ht es c t
-   | [v]            -> pp_appl_one g ht es c t v
-   | v1 :: v2 :: vs ->
-      let x = C.Appl (C.Appl [t; v1] :: v2 :: vs) in 
-      pp_proof g ht es c x
+   if es then list_map_cps g (fun h -> opt1_term h es c) vs else g vs
 
-and pp_atomic g ht es c t =
-   let _, premsno = PEH.split_with_whd (c, get_type c t) in
-   g t true premsno
-
-and pp_mutcase g ht es c uri tyno outty arg cases =
+and opt1_mutcase g es c uri tyno outty arg cases =
    let eliminator = get_default_eliminator c uri tyno outty in
    let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in
    let ps, sort_disp = get_ind_parameters c arg in
@@ -272,36 +261,96 @@ and pp_mutcase g ht es c uri tyno outty arg cases =
    let lifted_cases = List.map2 map2 cases constructors in
    let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
    let x = refine c (C.Appl args) in
-   pp_proof g ht es c x
-
-and pp_proof g ht es c t = 
-(*  Printf.eprintf "IN: |- %s\n" (*CicPp.ppcontext c*) (CicPp.ppterm t);
-  let g t proof decurry = 
-     Printf.eprintf "OUT: %b %u |- %s\n" proof decurry (CicPp.ppterm t);
-     g t proof decurry
-  in *)
-(*   let g t proof decurry = add g ht t proof decurry in *)
-   match t with
-      | C.Cast (t, v)              -> pp_cast g ht es c t v
-      | C.Lambda (name, v, t)      -> pp_lambda g ht es c name v t
-      | C.LetIn (name, v, t)       -> pp_letin g ht es c name v t
-      | C.Appl (t :: vs)           -> pp_appl g ht es c t vs
-      | C.MutCase (u, n, t, v, ws) -> pp_mutcase g ht es c u n t v ws
-      | t                          -> pp_atomic g ht es c t
-
-and pp_term g ht es c t =
-   if is_proof c t then pp_proof g ht es c t else g t false 0
+   HLog.warn "Optimizer: remove 3"; opt1_proof g es c x
+
+and opt1_cast g es c t w =
+   let g t = HLog.warn "Optimizer: remove 4"; g t in
+   if es then  opt1_proof g es c t else g t
+
+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.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
+   | C.MutCase (u, n, t, v, ws) -> opt1_mutcase g es c u n t v ws
+   | C.Cast (t, w)              -> opt1_cast g es c t w
+   | t                          -> opt1_other g es c t
+
+and opt1_term g es c t = 
+   if is_proof c t then opt1_proof g es c t else g t
+
+(* term preprocessing: optomization 2 ***************************************)
+
+let expanded_premise = "EXPANDED"
+
+let eta_expand g tys t =
+   assert (tys <> []);
+   let name i = Printf.sprintf "%s%u" expanded_premise i in 
+   let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
+   let arg i = C.Rel (succ i) in
+   let rec aux i f a = function
+      | []            -> f, a 
+      | (_, ty) :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
+   in
+   let n = List.length tys in
+   let absts, args = aux 0 identity [] tys in
+   let t = match S.lift n t with
+      | C.Appl ts -> C.Appl (ts @ args)
+      | t         -> C.Appl (t :: args)
+   in
+   g (absts t)
+
+let rec opt2_letin g c name v t =
+   let entry = Some (name, C.Def (v, None)) in
+   let g t = 
+      let g v = g (C.LetIn (name, v, t)) in
+      opt2_term g c v
+   in
+   opt2_proof g (entry :: c) t
+
+and opt2_lambda g c name w t =
+   let entry = Some (name, C.Decl w) in
+   let g t = g (C.Lambda (name, w, t)) in
+   opt2_proof g (entry :: c) t
+
+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, get_type c t) in
+      if vsno < csno then 
+         let tys, _ = PEH.split_with_whd (c, get_type 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
+      else g x 
+   in
+   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, get_type 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
+
+and opt2_term g c t = 
+   if is_proof c t then opt2_proof g c t else g t
 
 (* object preprocessing *****************************************************)
 
 let pp_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
-      let g bo proof decurry = 
-         let bo = eta_fix [] bo proof decurry in
-         C.Constant (name, Some bo, ty, pars, attrs)
-      in
-      let ht = C.CicHash.create 1 in
+      let g bo = C.Constant (name, Some bo, ty, pars, attrs) in
       Printf.eprintf "BEGIN: %s\n" name;
-      begin try pp_term g ht true [] bo
+      begin try opt1_term (opt2_term g []) true [] bo
       with e -> failwith ("PPP: " ^ Printexc.to_string e) end
    | obj                                         -> obj