Procedural: method "Apply" ok in forward style

diff --git a/helm/software/components/content_pres/content2Procedural.ml b/helm/software/components/content_pres/content2Procedural.ml
index 9be504913fc0ffcb628349d0dd30b76218138dd9..5c1ca4c157fdaeb459d9dd2e1f47e450e81c7221 100644 (file)
--- a/helm/software/components/content_pres/content2Procedural.ml
+++ b/helm/software/components/content_pres/content2Procedural.ml
@@ -62,6 +62,7 @@ type step = Note of note
          | Intros of count option * name list * note
          | Elim of what * using option * note
          | LetIn of name * what * note
+         | Apply of what * note
          | Exact of what * note
          | Branch of step list list * note
 
@@ -90,36 +91,40 @@ let split_inductive n tl =
 
 let rec mk_apply_term aref ac ds cargs =
    let step0 = mk_arg true (ac, [], ds) (List.hd cargs) in
-   let _, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in
-   Cic.AAppl (aref, List.rev row), ds 
-
-and mk_delta p ds =
-   let cmethod = p.C.proof_conclude.C.conclude_method in
-   let cargs = p.C.proof_conclude.C.conclude_args in
-   let capply = p.C.proof_apply_context in
-   let ccont = p.C.proof_context in
-   let caref = p.C.proof_conclude.C.conclude_aref in
-   match cmethod with
-      | "Exact"
-      | "Apply" when ccont = [] ->
-         let what, ds = mk_apply_term caref capply ds cargs in
-        let name = "PREVIOUS" in
-        mk_arel 1 name, LetIn (name, what, "") :: ds
-      | _ -> mk_arel 1 "COMPOUND", ds
+   let ac, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in
+   ac, ds, Cic.AAppl (aref, List.rev row) 
+
+and mk_delta ac ds = match ac with
+   | p :: ac ->
+      let cmethod = p.C.proof_conclude.C.conclude_method in
+      let cargs = p.C.proof_conclude.C.conclude_args in
+      let capply = p.C.proof_apply_context in
+      let ccont = p.C.proof_context in
+      let caref = p.C.proof_conclude.C.conclude_aref in
+      begin match cmethod with
+         | "Exact"
+         | "Apply" when ccont = [] && capply = [] ->
+           let ac, ds, what = mk_apply_term caref ac ds cargs in
+           let name = "PREVIOUS" in
+           ac, mk_arel 1 name, LetIn (name, what, "") :: ds
+         | _ -> ac, mk_arel 1 "COMPOUND", ds
+      end
+   | _ -> assert false
 
 and mk_arg first (ac, row, ds) = function
    | C.Lemma {C.lemma_id = aref; C.lemma_uri = uri} ->
-      ac, Cic.AConst (aref, U.uri_of_string uri, []) :: row, ds 
+      let t = match CicUtil.term_of_uri (U.uri_of_string uri) with
+         | Cic.Const (uri, _) -> Cic.AConst (aref, uri, [])
+        | Cic.MutConstruct (uri, tno, cno, _) -> 
+           Cic.AMutConstruct (aref, uri, tno, cno, [])
+         | _ -> assert false
+      in
+      ac, t :: row, ds 
    | C.Premise {C.premise_n = Some i; C.premise_binder = Some b} -> 
       ac, mk_arel i b :: row, ds
    | C.Premise {C.premise_n = None; C.premise_binder = None} -> 
-      begin match first, ac with
-         | _, hd :: tl -> 
-           let arg, ds = mk_delta hd ds in 
-           tl, arg :: row, ds
-        | false, []   -> ac, Cic.AImplicit ("", None) :: row, ds
-         | _           -> assert false
-      end
+      let ac, arg, ds = mk_delta ac ds in
+      ac, arg :: row, ds
    | C.Term t when first -> ac, t :: row, ds
    | C.Term _            -> ac, Cic.AImplicit ("", None) :: row, ds
    | C.Premise _         -> assert false
@@ -137,22 +142,32 @@ and mk_proof_body p =
    let cmethod = p.C.proof_conclude.C.conclude_method in
    let cargs = p.C.proof_conclude.C.conclude_args in
    let capply = p.C.proof_apply_context in
+   let caref = p.C.proof_conclude.C.conclude_aref in
    match cmethod, cargs with
       | "Intros+LetTac", [C.ArgProof p] -> mk_proof p 
       | "ByInduction", C.Aux n :: C.Term (Cic.AAppl (_, using :: _)) :: tl ->
         let whatm, ms = split_inductive n tl in (* actual rx params here *)
          let _, row, ds = mk_arg true (List.rev capply, [], []) whatm in
-        let what, qs = List.hd row, List.map mk_subproof ms in
+        let what, qs = List.hd row, mk_subproofs ms in
         List.rev ds @ [Elim (what, Some using, ""); Branch (qs, "")] 
+      | "Apply", _ -> 
+        let ac, ds, what = mk_apply_term caref (List.rev capply) [] cargs in
+         let qs = List.map mk_proof ac in
+        List.rev ds @ [Apply (what, ""); Branch (qs, "")]
       | _ ->  
         let text = 
            Printf.sprintf "UNEXPANDED %s %u" cmethod (List.length cargs)
         in [Note text] 
 
-and mk_subproof = function
-   | C.ArgProof ({C.proof_name = Some n} as p) -> Note n :: mk_proof p
-   | C.ArgProof ({C.proof_name = None} as p)   -> Note "" :: mk_proof p
-   | _                                         -> assert false
+and mk_subproofs cargs =
+   let mk_subproof proofs = function
+      | C.ArgProof ({C.proof_name = Some n} as p) -> 
+         (Note n :: mk_proof p) :: proofs
+      | C.ArgProof ({C.proof_name = None} as p)   -> 
+         (Note "" :: mk_proof p) :: proofs
+      | _                                         -> proofs
+   in
+   List.rev (List.fold_left mk_subproof [] cargs)
 
 let mk_obj ids_to_inner_sorts prefix (_, params, xmenv, obj) =
    if List.length params > 0 || xmenv <> None then assert false;
@@ -189,6 +204,10 @@ let mk_letin name what =
    let tactic = G.LetIn (floc, what, name) in
    mk_tactic tactic
 
+let mk_apply t =
+   let tactic = G.Apply (floc, t) in
+   mk_tactic tactic
+
 let mk_exact t =
    let tactic = G.Exact (floc, t) in
    mk_tactic tactic
@@ -212,6 +231,7 @@ let rec render_step sep a = function
    | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
    | Elim (t, xu, s)   -> mk_note s :: cont sep (mk_elim t xu :: a)
    | LetIn (n, t, s)   -> mk_note s :: cont sep (mk_letin n t :: a)
+   | Apply (t, s)      -> mk_note s :: cont sep (mk_apply t :: a)
    | Exact (t, s)      -> mk_note s :: cont sep (mk_exact t :: a)
    | Branch ([], s)    -> a
    | Branch ([ps], s)  -> render_steps a ps
@@ -225,6 +245,8 @@ and render_steps a = function
    | [p]                                         -> render_step None a p
    | (Note _ | Theorem _ | Qed _ as p) :: ps     ->
       render_steps (render_step None a p) ps 
+   | p :: ((Branch ([], _) :: _) as ps) ->
+      render_steps (render_step None a p) ps
    | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
       render_steps (render_step (Some mk_sc) a p) ps
    | p :: ps                                     ->

diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index 1b817c38e4a9920d9dea5919376dd2cb8c350e19..fc6c62b560d5ec3ae22c81f992481e6e6f8dad40 100644 (file)
--- a/helm/software/matita/contribs/prova.ma
+++ b/helm/software/matita/contribs/prova.ma
@@ -26,6 +26,9 @@ alias id "or3_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/or3_ind.c
 alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con".
 alias id "ex3_2_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/ex3_2_ind.con".
 alias id "subst0_gen_lift_ge" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_lift_ge.con".
+alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
+alias id "pr0_subst0_fwd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0_fwd.con".
+alias id "ex2_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/props/ex2_sym.con".
 
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".