Procedural: some improvements

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

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 8dd8e02aa44051b121511de0806b200b7af6cc65..6512938df3435ca46ad2273ae89d538f12cc6693 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -167,9 +167,10 @@ let convert st ?name v =
       | Some (st, et) ->
          let cst, cet = cic st, cic et in
         if PER.alpha_equivalence cst cet then [] else 
+        let e = Cn.mk_pattern [] (T.mk_arel 1 "") in
         match name with
-           | None    -> [T.Change (st, et, None, "")]
-           | Some id -> [T.Change (st, et, Some (id, id), ""); T.ClearBody (id, "")]
+           | None    -> [T.Change (st, et, None, e, "")]
+           | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
 
 let eta_expand n t =
    let id = Ut.id_of_annterm t in
@@ -188,7 +189,7 @@ let eta_expand n t =
 let appl_expand n = function
    | C.AAppl (id, ts) -> 
       let before, after = T.list_split (List.length ts + n) ts in
-      C.AAppl ("", C.AAppl (id, before) :: after)
+      C.AAppl (id, C.AAppl ("", before) :: after)
    | _                -> assert false
 
 let get_intro name t = 
@@ -218,13 +219,21 @@ 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 rps, predicate = [List.nth tl 4], List.nth tl 2 in
+   let e = Cn.mk_pattern rps predicate in
    match where with
       | C.ARel (_, _, _, premise) ->
          let script, what = mk_atomic st dtext what in
-         T.Rewrite (direction, what, Some (premise, name), dtext) :: script
+         T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script
       | _                         -> assert false
 
 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
@@ -244,7 +253,12 @@ and mk_fwd_proof st dtext name = function
          | Some v -> mk_fwd_proof st dtext name v
       end
    | v                                                  ->
-      [T.LetIn (name, v, dtext)]
+      match get_inner_types st v with
+         | Some (ity, _) ->
+           let qs = [[T.Id ""]; mk_proof (next st) v] in
+           [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
+         | _             ->
+            [T.LetIn (name, v, dtext)]
 
 and mk_proof st = function
    | C.ALambda (_, name, v, t)                     ->
@@ -289,11 +303,15 @@ and mk_proof st = function
               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 
-                 List.rev script @ convert st t @
-                 [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
+                  let rps, predicate = [List.nth tl 4], List.nth tl 2 in
+                  let e = Cn.mk_pattern rps predicate in
+                 List.rev script @ convert st t @
+                 [T.Rewrite (false, what, None, e, dtext); T.Branch (qs, "")]
               else if is_rewrite_left hd then 
-                 List.rev script @ convert st t @
-                 [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
+                 let rps, predicate = [List.nth tl 4], List.nth tl 2 in
+                  let e = Cn.mk_pattern rps predicate in
+                 List.rev script @ convert st t @
+                 [T.Rewrite (true, what, None, e, dtext); T.Branch (qs, "")]
               else   
                  let using = Some hd in
                  List.rev script @ convert st t @