X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2Procedural.ml;h=5c1ca4c157fdaeb459d9dd2e1f47e450e81c7221;hb=0e850ea466d664062ad1999e75c60b90aadaa084;hp=9be504913fc0ffcb628349d0dd30b76218138dd9;hpb=89f4301e7fa016e462fb4a01ad4b777c8f33912f;p=helm.git 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 ->