From b9185037db1db1c73031ce18eb943bdd7e170cdc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 14 Dec 2006 15:38:40 +0000 Subject: [PATCH] content2Procedural.ml: "Intros+LetTac" ok --- .../content_pres/content2Procedural.ml | 37 +++++++++++++++---- .../components/grafite/grafiteAstPp.ml | 6 +-- helm/software/matita/contribs/prova.ma | 7 ++++ 3 files changed, 39 insertions(+), 11 deletions(-) diff --git a/helm/software/components/content_pres/content2Procedural.ml b/helm/software/components/content_pres/content2Procedural.ml index 66a4370f3..99fe8d0b2 100644 --- a/helm/software/components/content_pres/content2Procedural.ml +++ b/helm/software/components/content_pres/content2Procedural.ml @@ -39,22 +39,43 @@ let mk_theorem name t = G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) let mk_tactic tactic = - G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None)) + let sep = G.Dot floc in + G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), Some sep)) +let mk_intros xi ids = + let tactic = G.Intros (floc, xi, ids) in + mk_tactic tactic + let mk_exact t = let tactic = G.Exact (floc, t) in mk_tactic tactic +(* internal functions *******************************************************) + +let mk_intros_arg = function + | `Declaration {C.dec_name = Some name} + | `Hypothesis {C.dec_name = Some name} + | `Definition {C.def_name = Some name} -> name + | _ -> assert false + +let mk_intros_args pc = List.map mk_intros_arg pc + +let rec mk_proof p = + let cmethod = p.C.proof_conclude.C.conclude_method in + let cargs = p.C.proof_conclude.C.conclude_args in + match cmethod, cargs with + | "Intros+LetTac", [C.ArgProof q] -> + let names = mk_intros_args q.C.proof_context in + let num = List.length names in + let text = String.concat " " names in + mk_intros (Some num) [] :: mk_note text :: mk_proof q + | _ -> [mk_note (Printf.sprintf "%s %u" cmethod (List.length cargs))] + (* interface functions ******************************************************) let content2procedural ~ids_to_inner_sorts prefix (_, params, xmenv, obj) = if List.length params > 0 || xmenv <> None then assert false; match obj with - | `Def (C.Const, t, `Proof { - C.proof_name = Some name; C.proof_context = []; - C.proof_apply_context = []; C.proof_conclude = { - C.conclude_conclusion = Some b - } - }) -> - [mk_theorem name t; mk_exact b] + | `Def (C.Const, t, `Proof ({C.proof_name = Some name} as p)) -> + mk_theorem name t :: mk_proof p | _ -> assert false diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index efc007886..0704863f5 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -33,7 +33,7 @@ let tactical_terminator = "" let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator -let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" +let pp_idents idents = "(" ^ String.concat " " idents ^ ")" let pp_reduction_kind ~term_pp = function | `Normalize -> "normalize" @@ -298,9 +298,9 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = function - | Note (_,str) -> sprintf "(* %s *)" str + | Note (_,str) -> sprintf "(* %s *)\n" str | Code (_,code) -> - sprintf "(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) + sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = function diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma index 67c4b1ebf..93b195990 100644 --- a/helm/software/matita/contribs/prova.ma +++ b/helm/software/matita/contribs/prova.ma @@ -14,5 +14,12 @@ set "baseuri" "cic:/matita/tests". +alias id "subst0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1)". +alias id "pr0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1)". +alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)". +alias id "T" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1)". + inline procedural "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con". -- 2.39.2