diff options
Diffstat (limited to 'contrib/subtac/g_subtac.ml4')
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 51 |
1 files changed, 44 insertions, 7 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 243cb191..e31326e9 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -10,7 +10,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) -(* $Id: g_subtac.ml4 9326 2006-10-31 12:57:26Z msozeau $ *) +(* $Id: g_subtac.ml4 9588 2007-02-02 16:17:13Z herbelin $ *) (*i camlp4deps: "parsing/grammar.cma" i*) @@ -37,6 +37,8 @@ struct let gec s = Gram.Entry.create ("Subtac."^s) (* types *) let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc" + + let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt" end open SubtacGram @@ -46,12 +48,17 @@ open Pcoq let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram - GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder; + GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder subtac_nameopt; subtac_gallina_loc: [ [ g = Vernac.gallina -> loc, g ] ] ; + subtac_nameopt: + [ [ "ofb"; id=Prim.ident -> Some (id) + | -> None ] ] + ; + Constr.binder_let: [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in @@ -60,8 +67,12 @@ GEXTEND Gram Constr.binder: [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in - ([id], typ) ] ]; + ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)])) + | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" -> + ([id],c) + | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" -> + (id::lid,c) + ] ]; END @@ -69,16 +80,42 @@ GEXTEND Gram type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype), - (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr) gallina_loc_argtype), + (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr ) gallina_loc_argtype), (rawwit_subtac_gallina_loc : (Genarg.rlevel, Tacexpr.raw_tactic_expr) gallina_loc_argtype) = Genarg.create_arg "subtac_gallina_loc" +type 'a nameopt_argtype = (identifier option, 'a, 'a) Genarg.abstract_argument_type + +let (wit_subtac_nameopt : Genarg.tlevel nameopt_argtype), + (globwit_subtac_nameopt : Genarg.glevel nameopt_argtype), + (rawwit_subtac_nameopt : Genarg.rlevel nameopt_argtype) = + Genarg.create_arg "subtac_nameopt" + VERNAC COMMAND EXTEND Subtac [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ] -| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name) ] -| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None) ] + END + +VERNAC COMMAND EXTEND Subtac_Obligations +| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, Some t) ] +| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ] +| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ] +| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ] +| [ "Next" "Obligation" "of" ident(name) ] -> [ Subtac_obligations.next_obligation (Some name) ] +| [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ] +END + +VERNAC COMMAND EXTEND Subtac_Solve_Obligations | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ] | [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ] +| [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] +| [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] + END + +VERNAC COMMAND EXTEND Subtac_Set_Solver +| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ] +END + +VERNAC COMMAND EXTEND Subtac_Show_Obligations | [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] | [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] END |