- new tactic applyP for use in the *P*rocedural script reconstruction

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

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index c004fd346b4e2a9ff30714fa3cf84af50a5acf00..b37eef6bbc989034b8dbe2e7fd851dc454baf943 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -153,7 +153,7 @@ with Invalid_argument _ -> failwith "A2P.get_sort"
 *)
 let get_type msg st bo =
 try   
-   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
+   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
@@ -167,7 +167,7 @@ let get_entry st id =
 
 let get_ind_names uri tno =
 try   
-   let ts = match E.get_obj Un.empty_ugraph uri with
+   let ts = match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (ts, _, _, _), _ -> ts 
       | _                                      -> assert false
    in
@@ -347,20 +347,24 @@ and proc_appl st what hd tl =
       let script = List.rev (mk_arg st hd) in
       match rc with
          | Some (i, j, uri, tyno) ->
-           let classes, tl, _, where = split2_last classes tl in
-           let script = List.rev (mk_arg st where) @ script in
-           let synth = I.S.add 1 synth in
+           let classes2, tl2, _, where = split2_last classes tl in
+           let script2 = List.rev (mk_arg st where) @ script in
+           let synth2 = I.S.add 1 synth in
            let names = get_ind_names uri tyno in
-           let qs = proc_bkd_proofs (next st) synth names classes tl in
-            if is_rewrite_right hd then 
-              script @ mk_rewrite st dtext where qs tl false what
+           let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
+            if List.length qs <> List.length names then
+              let qs = proc_bkd_proofs (next st) synth [] classes tl in
+              let hd = mk_exp_args hd tl classes synth in
+              script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+           else if is_rewrite_right hd then 
+              script2 @ mk_rewrite st dtext where qs tl2 false what
            else if is_rewrite_left hd then 
-              script @ mk_rewrite st dtext where qs tl true what
+              script2 @ mk_rewrite st dtext where qs tl2 true what
            else
-              let predicate = List.nth tl (parsno - i) in
+              let predicate = List.nth tl2 (parsno - i) in
                let e = Cn.mk_pattern j predicate in
               let using = Some hd in
-              (* convert_elim st what what e @ *) script @ 
+              (* convert_elim st what what e @ *) script2 @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
         | None        ->
            let qs = proc_bkd_proofs (next st) synth [] classes tl in