- 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 18b4f064f71bfaccfadddb83acf4f62d57e3166b..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
@@ -282,7 +282,7 @@ let rec proc_lambda st name v t =
    let intro = get_intro name in
    proc_proof (add st entry intro) t
 
-and proc_letin st what name v t =
+and proc_letin st what name v w t =
    let intro = get_intro name in
    let proceed, dtext = test_depth st in
    let script = if proceed then 
@@ -300,8 +300,7 @@ and proc_letin st what name v t =
            in
            st, C.Decl (H.cic ity), rqv
         | None          ->
-            (*CSC: here we need the type of v *)
-           st, C.Def (H.cic v, assert false), [T.LetIn (intro, v, dtext)]
+           st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in
       let qt = proc_proof (next (add st entry intro)) t in
@@ -322,6 +321,11 @@ and proc_mutconstruct st what =
    let script = [T.Apply (what, dtext)] in 
    mk_intros st what script
 
+and proc_const st what = 
+   let _, dtext = test_depth st in
+   let script = [T.Apply (what, dtext)] in 
+   mk_intros st what script
+
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
    let script = if proceed then
@@ -343,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
@@ -385,12 +393,13 @@ 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.ALetIn (_, name, v, ty, t) as what -> assert false (*proc_letin (f st) what name v t*)
-      | C.ARel _ as what                 -> proc_rel (f st) what
-      | C.AMutConstruct _ as what        -> proc_mutconstruct (f st) what
-      | C.AAppl (_, hd :: tl) as what    -> proc_appl (f st) what hd tl
-      | what                             -> proc_other (f st) what
+      | C.ALambda (_, name, w, t)           -> proc_lambda st 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
+      | C.AConst _ as what                  -> proc_const (f st) what
+      | C.AAppl (_, hd :: tl) as what       -> proc_appl (f st) what hd tl
+      | what                                -> proc_other (f st) what
 
 and proc_bkd_proofs st synth names classes ts =
 try 
@@ -419,7 +428,8 @@ with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 (* object costruction *******************************************************)
 
-let is_theorem pars =   
+let is_theorem pars =
+   pars = [] ||
    List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
    List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars