some improvements

[helm.git] / components / acic_procedural / acic2Procedural.ml

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index cf8159b0c06c7c6d49d7d97b9224d98ad5786911..8dd8e02aa44051b121511de0806b200b7af6cc65 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -49,8 +49,7 @@ type status = {
    max_depth: int option;
    depth: int;
    context: C.context;
-   intros: string list;
-   ety: C.annterm option
+   intros: string list
 }
 
 (* helpers ******************************************************************)
@@ -87,15 +86,11 @@ let string_of_head = function
    | C.AMeta _         -> "meta"
    | C.AImplicit _     -> "implict"
 
-let clear st = {st with intros = []; ety = None}
+let clear st = {st with intros = []}
 
 let next st = {(clear st) with depth = succ st.depth}
 
-let set_ety st ety =
-   if st.ety = None then {st with ety = ety} else st
-
-let add st entry intro ety = 
-   let st = set_ety st ety in
+let add st entry intro =
    {st with context = entry :: st.context; intros = intro :: st.intros}
 
 let test_depth st =
@@ -164,8 +159,6 @@ let unused_premise = "UNUSED"
 
 let defined_premise = "DEFINED"
 
-let assumed_premise = "ASSUMED"
-
 let expanded_premise = "EXPANDED"
 
 let convert st ?name v = 
@@ -183,7 +176,7 @@ let eta_expand n t =
    let ty = C.AImplicit ("", None) in
    let name i = Printf.sprintf "%s%u" expanded_premise i in 
    let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in
-   let arg i n = T.mk_arel (n - i) (name i) in
+   let arg i n = T.mk_arel (n - i) (name (n - i - 1)) in
    let rec aux i f a =
       if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
    in
@@ -210,11 +203,7 @@ let mk_intros st script =
 try
    if st.intros = [] then script else
    let count = List.length st.intros in
-   let p0 = T.Whd (count, "") in
-   let p1 = T.Intros (Some count, List.rev st.intros, "") in
-   match st.ety with
-      | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script
-      | _                                   -> p1 :: script
+   T.Intros (Some count, List.rev st.intros, "") :: script
 with Invalid_argument _ -> failwith "A2P.mk_intros"
 
 let rec mk_atomic st dtext what =
@@ -229,27 +218,12 @@ let rec mk_atomic st dtext what =
 
 and mk_fwd_rewrite st dtext name tl direction =
    let what, where = List.nth tl 5, List.nth tl 3 in
-   let rewrite premise =
-      let script, what = mk_atomic st dtext what in
-      T.Rewrite (direction, what, Some (premise, name), dtext) :: script
-   in
    match where with
-      | C.ARel (_, _, _, binder) -> rewrite binder
-      | _                        -> assert false
-
-(*      
-        assert (get_inner_sort st where = `Prop);
-        let pred, old = List.nth tl 2, List.nth tl 1 in
-        let pred_name = defined_premise in
-        let pred_text = "extracted" in
-         let p1 = T.LetIn (pred_name, pred, pred_text) in
-        let cut_name = assumed_premise in
-        let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in
-        let cut_text = "" in
-         let p2 = T.Cut (cut_name, cut_type, cut_text) in
-         let qs = [rewrite cut_name; mk_proof (next st) where] in 
-         [T.Branch (qs, ""); p2; p1] 
-*)
+      | C.ARel (_, _, _, premise) ->
+         let script, what = mk_atomic st dtext what in
+         T.Rewrite (direction, what, Some (premise, name), dtext) :: script
+      | _                         -> assert false
+
 and mk_fwd_proof st dtext name = function
    | C.AAppl (_, hd :: tl) as v                         -> 
       if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
@@ -273,20 +247,16 @@ and mk_fwd_proof st dtext name = function
       [T.LetIn (name, v, dtext)]
 
 and mk_proof st = function
-   | C.ALambda (_, name, v, t) as what             ->
+   | C.ALambda (_, name, v, t)                     ->
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
-      let ety = match get_inner_types st what with
-         | Some (_, ety) -> Some ety
-        | None          -> None
-      in
-      mk_proof (add st entry intro ety) t
+      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 t in
-         let q = mk_proof (next (add st entry intro None)) t in
+         let q = mk_proof (next (add st entry intro)) t in
          List.rev_append (mk_fwd_proof st dtext intro v) q
       else
         [T.Apply (what, dtext)]
@@ -369,7 +339,7 @@ let is_theorem pars =
 
 let mk_obj st = function
    | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
-      let ast = mk_proof (set_ety st (Some t)) v in
+      let ast = mk_proof st v in
       let count = T.count_steps 0 ast in
       let text = Printf.sprintf "tactics: %u" count in
       T.Theorem (s, t, text) :: ast @ [T.Qed ""]
@@ -386,8 +356,7 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
       max_depth = depth;
       depth     = 0;
       context   = [];
-      intros    = [];
-      ety       = None
+      intros    = []
    } in
    HLog.debug "Level 2 transformation";
    let steps = mk_obj st aobj in