From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- plugins/decl_mode/g_decl_mode.ml4 | 100 ++++++++++++++++---------------------- 1 file changed, 41 insertions(+), 59 deletions(-) (limited to 'plugins/decl_mode/g_decl_mode.ml4') diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 9a1e00ee..03929b3b 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -1,35 +1,33 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + begin Decl_proof_instr.go_to_proof_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () @@ -75,24 +71,18 @@ let vernac_decl_proof () = (* spiwack: some bureaucracy is not performed here *) let vernac_return () = - Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + begin Decl_proof_instr.return_from_tactic_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () end let vernac_proof_instr instr = - Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + begin Decl_proof_instr.proof_instr instr; Vernacentries.print_subgoals () end -(* We create a new parser entry [proof_mode]. The Declarative proof mode - will replace the normal parser entry for tactics with this one. *) -let proof_mode = Gram.entry_create "vernac:proof_command" -(* Auxiliary grammar entry. *) -let proof_instr = Gram.entry_create "proofmode:instr" - (* Before we can write an new toplevel command (see below) which takes a [proof_instr] as argument, we need to declare how to parse it, print it, globalise it and interprete it. @@ -101,33 +91,28 @@ let proof_instr = Gram.entry_create "proofmode:instr" indirect through the [proof_instr] grammar entry. *) (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) -(* [Genarg.create_arg] creates a new embedding into Genarg. *) -let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) = - Genarg.create_arg None "proof_instr" -let _ = Tacinterp.add_interp_genarg "proof_instr" - begin - begin fun e x -> (* declares the globalisation function *) - Genarg.in_gen globwit_proof_instr - (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x)) - end, - begin fun ist gl x -> (* declares the interpretation function *) - Tacmach.project gl , - Genarg.in_gen wit_proof_instr - (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x)) - end, - begin fun _ x -> x end (* declares the substitution function, irrelevant in our case *) - end +(* Only declared at raw level, because only used in vernac commands. *) +let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type = + Genarg.make0 None "proof_instr" + +(* We create a new parser entry [proof_mode]. The Declarative proof mode + will replace the normal parser entry for tactics with this one. *) +let proof_mode : vernac_expr Gram.entry = + Gram.entry_create "vernac:proof_command" +(* Auxiliary grammar entry. *) +let proof_instr : raw_proof_instr Gram.entry = + Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr) -let _ = Pptactic.declare_extra_genarg_pprule - (rawwit_proof_instr, pr_raw_proof_instr) - (globwit_proof_instr, pr_glob_proof_instr) - (wit_proof_instr, pr_proof_instr) +let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr + pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr + +let classify_proof_instr _ = VtProofStep false, VtLater (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. The "-" indicates that the rule does not start with a distinguished string. *) -VERNAC proof_mode EXTEND ProofInstr +VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ] END @@ -140,7 +125,7 @@ GEXTEND Gram GLOBAL: proof_mode ; proof_mode: LAST - [ [ c=G_vernac.subgoal_command -> c (Some 1) ] ] + [ [ c=G_vernac.subgoal_command -> c (Some (Vernacexpr.SelectNth 1)) ] ] ; END @@ -171,12 +156,11 @@ let _ = end } -(* Two new vernacular commands *) VERNAC COMMAND EXTEND DeclProof - [ "proof" ] -> [ vernac_decl_proof () ] +[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ] END VERNAC COMMAND EXTEND DeclReturn - [ "return" ] -> [ vernac_return () ] +[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ] END let none_is_empty = function @@ -192,7 +176,7 @@ GLOBAL: proof_instr; statement : [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} | i=ident -> {st_label=Anonymous; - st_it=Topconstr.CRef (Libnames.Ident (loc, i))} + st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)} | c=constr -> {st_label=Anonymous;st_it=c} ]]; constr_or_thesis : @@ -205,7 +189,7 @@ GLOBAL: proof_instr; | [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} | i=ident -> {st_label=Anonymous; - st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))} + st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))} | c=constr -> {st_label=Anonymous;st_it=This c} ] ]; @@ -273,7 +257,7 @@ GLOBAL: proof_instr; ; (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*) loc_id: - [[ id=ident -> fun x -> (loc,(id,x)) ]]; + [[ id=ident -> fun x -> (!@loc,(id,x)) ]]; hyp: [[ id=loc_id -> id None ; | id=loc_id ; ":" ; c=constr -> id (Some c)]] @@ -405,5 +389,3 @@ GLOBAL: proof_instr; [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]] ; END;; - - -- cgit v1.2.3