From: Ferruccio Guidi Date: Wed, 20 Dec 2006 20:07:54 +0000 (+0000) Subject: Procedural: method "Apply" ok in forward style X-Git-Tag: make_still_working~6578 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd0b1bb8a2cb5f57f148e6500ea2d5937082a7fa;p=helm.git 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 9be504913..5c1ca4c15 100644 --- 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 1b817c38e..fc6c62b56 100644 --- 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".