some improvements

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index cf8159b0c06c7c6d49d7d97b9224d98ad5786911..8dd8e02aa44051b121511de0806b200b7af6cc65 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/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

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 4e43164cb0c0b5694b87e09167c81cad2c18390e..b3ce560707348f38f7bd9de27306bd0cc3dc6bdc 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -65,12 +65,6 @@ let rec list_sub start length = function
 
 (* proof construction *******************************************************)
 
-let rec need_whd i = function
-   | C.ACast (_, t, _)               -> need_whd i t
-   | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
-   | _                    when i > 0 -> true
-   | _                               -> false
-
 let lift k n =
    let rec lift_xns k (uri, t) = uri, lift_term k t
    and lift_ms k = function

diff --git a/helm/software/components/acic_procedural/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli
index fef3ad07b0aba093fb3d4342bf93c098ceac11e8..f27d73aabf0ee8802b5be1806f96b097cb129337 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.mli
+++ b/helm/software/components/acic_procedural/proceduralConversion.mli
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val need_whd: int -> Cic.annterm -> bool
-
 val lift: int -> int -> Cic.annterm -> Cic.annterm
 
 val mk_ind: 

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index b81a7c3dead0ebe02105c854bf45706e133b91bc..6aa769b03aa11ec4c209b3b5f60e0e0a1b3ddb68 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -87,7 +87,6 @@ type step = Note of note
          | Rewrite of how * what * where * note
          | Elim of what * using option * note
          | Apply of what * note
-         | Whd of count * note
          | Change of inferred * what * where * note 
          | ClearBody of name * note
          | Branch of step list list * note
@@ -147,11 +146,6 @@ let mk_apply t =
    let tactic = G.Apply (floc, t) in
    mk_tactic tactic
 
-let mk_whd i =
-   let pattern = None, [], Some hole in
-   let tactic = G.Reduce (floc, `Whd, pattern) in
-   mk_tactic tactic
-
 let mk_change t where =
    let pattern = match where with
       | None              -> None, [], Some hole
@@ -187,7 +181,6 @@ let rec render_step sep a = function
    | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
    | Elim (t, xu, s)      -> mk_note s :: cont sep (mk_elim t xu :: a)
    | Apply (t, s)         -> mk_note s :: cont sep (mk_apply t :: a)
-   | Whd (c, s)           -> mk_note s :: cont sep (mk_whd c :: a)
    | Change (t, _, w, s)  -> mk_note s :: cont sep (mk_change t w :: a)
    | ClearBody (n, s)     -> mk_note s :: cont sep (mk_clearbody n :: a)
    | Branch ([], s)       -> a

diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli
index f26c19d87e8383d447184d1608d3336048f8204c..980bc1bc1c71796fe462829b96caa0414968775d 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.mli
+++ b/helm/software/components/acic_procedural/proceduralTypes.mli
@@ -54,7 +54,6 @@ type step = Note of note
          | Rewrite of how * what * where * note
          | Elim of what * using option * note
          | Apply of what * note
-         | Whd of count * note
          | Change of inferred * what * where * note
          | ClearBody of name * note
          | Branch of step list list * note