some bug fixes

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 29b5677312874ccd2ebbf5e1f776261327aeb536..4dd1bf192956edfd75777783e130b2b38f3fb684 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -256,17 +256,29 @@ let mk_arg st = function
    | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
    | _                              -> []
 
-let mk_fwd_rewrite st dtext name tl direction t =   
+let mk_fwd_rewrite st dtext name tl direction v t ity =
+   let compare premise = function
+      | None   -> true
+      | Some s -> s = premise
+   in
    assert (List.length tl = 6);
    let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
    match where with
-      | C.ARel (_, _, i, premise) as v ->
-         let where = Some (premise, name) in
-(*         let _script = convert_elim st ~name:(premise, i) t v e in *) 
-         let script = mk_arg st what @ mk_arg st v (* @ script *) in
-        let st = {st with context = Cn.clear st.context premise} in 
-        st, T.Rewrite (direction, what, where, e, dtext) :: script
+      | C.ARel (_, _, i, premise) as w ->
+(*         let _script = convert_elim st ~name:(premise, i) v w e in *) 
+         let script name =
+            let where = Some (premise, name) in
+           let script = mk_arg st what @ mk_arg st w (* @ script *) in
+           T.Rewrite (direction, what, where, e, dtext) :: script
+        in
+        if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
+           {st with context = Cn.clear st.context premise}, script name
+        else
+           let br1 = [T.Id ""] in
+           let br2 = List.rev (T.Apply (w, "assumption") :: script None) in
+           let text = "non linear rewrite" in
+           st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]
       | _                         -> assert false
 
 let mk_rewrite st dtext where qs tl direction t = 
@@ -276,13 +288,15 @@ let mk_rewrite st dtext where qs tl direction t =
    let script = [] (* convert_elim st t t e *) in
    script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")]
 
-let rec proc_lambda st name v t =
-   let dno = DTI.does_not_occur 1 (H.cic t) in
-   let dno = dno && match get_inner_types st t with
-      | None          -> false
-      | Some (it, et) -> 
-         DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
+let rec proc_lambda st what name v t =
+   let dno, ae = match get_inner_types st t with
+      | None            -> false, true
+      | Some (sty, ety) -> 
+         let sty, ety = H.cic sty, H.cic ety in
+        DTI.does_not_occur 1 sty && DTI.does_not_occur 1 ety,
+         Ut.alpha_equivalence sty ety   
    in
+   let dno = dno && DTI.does_not_occur 1 (H.cic t) in
    let name = match dno, name with
       | true, _            -> C.Anonymous
       | false, C.Anonymous -> H.mk_fresh_name st.context used_premise 
@@ -290,7 +304,10 @@ let rec proc_lambda st name v t =
    in
    let entry = Some (name, C.Decl (H.cic v)) in
    let intro = get_intro name in
-   proc_proof (add st entry intro) t
+   let st = (add st entry intro) in
+   if ae then proc_proof st t else
+   let script = proc_proof (clear st) t in
+   mk_intros st t script
 
 and proc_letin st what name v w t =
    let intro = get_intro name in
@@ -300,9 +317,9 @@ and proc_letin st what name v w t =
          | Some (ity, _) ->
            let st, rqv = match v with
                | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
-                 mk_fwd_rewrite st dtext intro tl true v
+                 mk_fwd_rewrite st dtext intro tl true v t ity
               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
-                 mk_fwd_rewrite st dtext intro tl false v
+                 mk_fwd_rewrite st dtext intro tl false v t ity
               | v                                                     ->
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
                  let ity = H.acic_bc st.context ity in
@@ -405,7 +422,7 @@ and proc_proof st t =
       {st with context = context; clears = clears; clears_note = note; }
    in
    match t with
-      | C.ALambda (_, name, w, t)           -> proc_lambda st name w t
+      | C.ALambda (_, name, w, t) as what   -> proc_lambda (f st) what name w t
       | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
       | C.ARel _ as what                    -> proc_rel (f st) what
       | C.AMutConstruct _ as what           -> proc_mutconstruct (f st) what

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 5e1bc3a24add64ceb4fe31766a8f5d5c828c0611..6534b872538b0912e4e1d8ce75fa72a2a434a604 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -134,8 +134,9 @@ let mk_letin name what punctation =
 let mk_rewrite direction what where pattern punctation =
    let direction = if direction then `RightToLeft else `LeftToRight in 
    let pattern, rename = match where with
-      | None                 -> (None, [], Some pattern), []
-      | Some (premise, name) -> (None, [premise, pattern], None), [name] 
+      | None                      -> (None, [], Some pattern), []
+      | Some (premise, Some name) -> (None, [premise, pattern], None), [Some name]
+      | Some (premise, None)      -> (None, [premise, pattern], None), [] 
    in
    let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
    mk_tactic tactic punctation