From 0cc6076e7d4d92c1d899d450b2336dadbeb5f1b1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 25 Apr 2008 18:07:44 +0000 Subject: Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve des théorèmes prouvés par récursion ou corécursion mutuelle. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_tactic.ml4 | 17 +++++++++++++---- parsing/g_vernac.ml4 | 8 +++++--- parsing/pptactic.ml | 6 ++++-- parsing/ppvernac.ml | 13 +++++++------ parsing/q_coqast.ml4 | 10 ++++++---- parsing/tactic_printer.ml | 14 +++++++++++--- 6 files changed, 46 insertions(+), 22 deletions(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b6a3c985a..035bdced7 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -297,14 +297,23 @@ GEXTEND Gram | "-" -> false | -> true ]] ; + simple_fix_binder: + [ [ id=name -> ([id],Default Explicit,CHole (loc, None)) + | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) + ] ] + ; fixdecl: - [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot; + [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ann=fixannot; ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] ; fixannot: [ [ "{"; IDENT "struct"; id=name; "}" -> Some id | -> None ] ] ; + cofixdecl: + [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ":"; ty=lconstr; ")" -> + (loc,id,bl,None,ty) ] ] + ; hintbases: [ [ "with"; "*" -> None | "with"; l = LIST1 IDENT -> Some l @@ -387,11 +396,11 @@ GEXTEND Gram | "fix"; n = natural -> TacFix (None,n) | "fix"; id = ident; n = natural -> TacFix (Some id,n) | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> - TacMutualFix (id,n,List.map mk_fix_tac fd) + TacMutualFix (false,id,n,List.map mk_fix_tac fd) | "cofix" -> TacCofix None | "cofix"; id = ident -> TacCofix (Some id) - | "cofix"; id = ident; "with"; fd = LIST1 fixdecl -> - TacMutualCofix (id,List.map mk_cofix_tac fd) + | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> + TacMutualCofix (false,id,List.map mk_cofix_tac fd) | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" -> TacLetTac (Names.Name id,b,nowhere) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index aea0cf27b..8285bbad3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -123,9 +123,11 @@ GEXTEND Gram gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = identref; bl = binders_let; ":"; - c = lconstr -> - VernacStartTheoremProof (thm, id, (bl, c), false, no_hook) + [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr; + l = LIST0 + [ "with"; id = identref; bl = binders_let; ":"; c = lconstr -> + (Some id,(bl,c)) ] -> + VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | stre = assumptions_token; nl = inline; bl = assum_list -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 2a46388c3..d4befac1e 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -687,11 +687,13 @@ and pr_atom1 = function hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb) | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c) | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) - | TacMutualFix (id,n,l) -> + | TacMutualFix (hidden,id,n,l) -> + if hidden then str "idtac" (* should caught before! *) else hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ str"with " ++ prlist_with_sep spc pr_fix_tac l) | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido) - | TacMutualCofix (id,l) -> + | TacMutualCofix (hidden,id,l) -> + if hidden then str "idtac" (* should be caught before! *) else hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++ str"with " ++ prlist_with_sep spc pr_cofix_tac l) | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 9fe24f4d4..57e21c2ce 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -534,12 +534,13 @@ let rec pr_vernac = function | None -> mt() | Some cc -> str" :=" ++ spc() ++ cc)) - | VernacStartTheoremProof (ki,id,(bl,c),b,d) -> - hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++ - (match bl with - | [] -> mt() - | _ -> pr_binders bl ++ spc()) - ++ str":" ++ pr_spc_lconstr c) + | VernacStartTheoremProof (ki,l,_,_) -> + hov 1 (pr_thm_token ki ++ spc() ++ + prlist_with_sep (fun () -> str "with ") (fun (id,(bl,c)) -> hov 0 + (pr_opt pr_lident id ++ spc() ++ + (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ + str":" ++ pr_spc_lconstr c)) l) + | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with | None -> if opac then str"Qed" else str"Defined" diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 6313a553e..a8ddfadb2 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -313,20 +313,22 @@ let rec mlexpr_of_atomic_tactic = function let ido = mlexpr_of_ident_option ido in let n = mlexpr_of_int n in <:expr< Tacexpr.TacFix $ido$ $n$ >> - | Tacexpr.TacMutualFix (id,n,l) -> + | Tacexpr.TacMutualFix (b,id,n,l) -> + let b = mlexpr_of_bool b in let id = mlexpr_of_ident id in let n = mlexpr_of_int n in let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in let l = mlexpr_of_list f l in - <:expr< Tacexpr.TacMutualFix $id$ $n$ $l$ >> + <:expr< Tacexpr.TacMutualFix $b$ $id$ $n$ $l$ >> | Tacexpr.TacCofix ido -> let ido = mlexpr_of_ident_option ido in <:expr< Tacexpr.TacCofix $ido$ >> - | Tacexpr.TacMutualCofix (id,l) -> + | Tacexpr.TacMutualCofix (b,id,l) -> + let b = mlexpr_of_bool b in let id = mlexpr_of_ident id in let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in let l = mlexpr_of_list f l in - <:expr< Tacexpr.TacMutualCofix $id$ $l$ >> + <:expr< Tacexpr.TacMutualCofix $b$ $id$ $l$ >> | Tacexpr.TacCut c -> <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 91c1bc0c4..11b755fa0 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -34,7 +34,7 @@ let pr_rule = function | Nested(cmpd,_) -> begin match cmpd with - Tactic (texp,_) -> hov 0 (pr_tactic texp) + | Tactic (texp,_) -> hov 0 (pr_tactic texp) | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr) end | Daimon -> str "" @@ -50,6 +50,14 @@ let pr_rule_dot = function | r -> pr_rule r ++ if uses_default_tac r then str "..." else str"." +let pr_rule_dot_fnl = function + | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_) + | TacMutualCofix (true,_,_))),_),_) -> + (* Very big hack to not display hidden tactics in "Theorem with" *) + (* (would not scale!) *) + mt () + | r -> pr_rule_dot r ++ fnl () + exception Different (* We remove from the var context of env what is already in osign *) @@ -155,7 +163,7 @@ let rec print_script nochange sigma pf = (print_script nochange sigma) spfl ) | Some(rule,spfl) -> ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot rule ++ fnl () ++ + pr_rule_dot_fnl rule ++ prlist_with_sep pr_fnl (print_script nochange sigma) spfl ) @@ -189,7 +197,7 @@ let print_treescript nochange sigma pf = | Some(r,spfl) -> let indent = if List.length spfl >= 2 then 1 else 0 in (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - hv indent (pr_rule_dot r ++ fnl () ++ prlist_with_sep fnl aux spfl) + hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl aux spfl) in hov 0 (aux pf) let rec print_info_script sigma osign pf = -- cgit v1.2.3