From 845d6f167a0b2f31bd77cd98de0522873c0683a7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 26 Apr 2012 09:54:18 +0000 Subject: migrate g_obligations.ml4 in parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15248 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_obligations.ml4 | 154 ++++++++++++++++++++++++++++++++++++++++++++ parsing/highparsing.mllib | 1 + toplevel/g_obligations.ml4 | 155 --------------------------------------------- toplevel/toplevel.mllib | 1 - 4 files changed, 155 insertions(+), 156 deletions(-) create mode 100644 parsing/g_obligations.ml4 delete mode 100644 toplevel/g_obligations.ml4 diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 new file mode 100644 index 0000000000..f86fd0fecd --- /dev/null +++ b/parsing/g_obligations.ml4 @@ -0,0 +1,154 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + *) + +module Gram = Pcoq.Gram +module Vernac = Pcoq.Vernac_ +module Tactic = Pcoq.Tactic + +module ObligationsGram = +struct + let gec s = Gram.entry_create s + + let withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "withtac" +end + +open Glob_term +open ObligationsGram +open Util +open Tok +open Pcoq +open Prim +open Constr + +let sigref = mkRefC (Qualid (Pp.dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) + +GEXTEND Gram + GLOBAL: withtac; + + withtac: + [ [ "with"; t = Tactic.tactic -> Some t + | -> None ] ] + ; + + Constr.closed_binder: + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + [LocalRawAssum ([id], default_binder_kind, typ)] + ] ]; + + END + +type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type + +let (wit_withtac : Genarg.tlevel withtac_argtype), + (globwit_withtac : Genarg.glevel withtac_argtype), + (rawwit_withtac : Genarg.rlevel withtac_argtype) = + Genarg.create_arg None "withtac" + +open Obligations + +VERNAC COMMAND EXTEND Obligations +| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> + [ obligation (num, Some name, Some t) tac ] +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> + [ obligation (num, Some name, None) tac ] +| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] -> + [ obligation (num, None, Some t) tac ] +| [ "Obligation" integer(num) withtac(tac) ] -> + [ obligation (num, None, None) tac ] +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> + [ next_obligation (Some name) tac ] +| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] +END + +VERNAC COMMAND EXTEND Solve_Obligation +| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> + [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> + [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] + END + +VERNAC COMMAND EXTEND Solve_Obligations +| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> + [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligations" "with" tactic(t) ] -> + [ try_solve_obligations None (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligations" ] -> + [ try_solve_obligations None None ] + END + +VERNAC COMMAND EXTEND Solve_All_Obligations +| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> + [ solve_all_obligations (Some (Tacinterp.interp t)) ] +| [ "Solve" "All" "Obligations" ] -> + [ solve_all_obligations None ] + END + +VERNAC COMMAND EXTEND Admit_Obligations +| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] +| [ "Admit" "Obligations" ] -> [ admit_obligations None ] + END + +VERNAC COMMAND EXTEND Set_Solver +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ + set_default_tactic + (Vernacexpr.use_section_locality ()) + (Tacinterp.glob_tactic t) ] +END + +open Pp + +VERNAC COMMAND EXTEND Show_Solver +| [ "Show" "Obligation" "Tactic" ] -> [ + msgnl (str"Program obligation tactic is " ++ print_default_tactic ()) ] +END + +VERNAC COMMAND EXTEND Show_Obligations +| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] +| [ "Obligations" ] -> [ show_obligations None ] +END + +VERNAC COMMAND EXTEND Show_Preterm +| [ "Preterm" "of" ident(name) ] -> [ show_term (Some name) ] +| [ "Preterm" ] -> [ show_term None ] +END + +open Pp + +(* Declare a printer for the content of Program tactics *) +let () = + let printer _ _ _ = function + | None -> mt () + | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic (Global.env ()) tac + in + (* should not happen *) + let dummy _ _ _ expr = assert false in + Pptactic.declare_extra_genarg_pprule + (rawwit_withtac, printer) + (globwit_withtac, dummy) + (wit_withtac, dummy) diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index eed6caea30..6ccbdb7523 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -4,3 +4,4 @@ G_prim G_proofs G_tactic G_ltac +G_obligations \ No newline at end of file diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 deleted file mode 100644 index 7f5991d385..0000000000 --- a/toplevel/g_obligations.ml4 +++ /dev/null @@ -1,155 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - *) - -module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic - -module ObligationsGram = -struct - let gec s = Gram.entry_create s - - let withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "withtac" -end - -open Glob_term -open ObligationsGram -open Util -open Tok -open Pcoq -open Prim -open Constr - -let sigref = mkRefC (Qualid (Pp.dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) - -GEXTEND Gram - GLOBAL: withtac; - - withtac: - [ [ "with"; t = Tactic.tactic -> Some t - | -> None ] ] - ; - - Constr.closed_binder: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [LocalRawAssum ([id], default_binder_kind, typ)] - ] ]; - - END - -type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type - -let (wit_withtac : Genarg.tlevel withtac_argtype), - (globwit_withtac : Genarg.glevel withtac_argtype), - (rawwit_withtac : Genarg.rlevel withtac_argtype) = - Genarg.create_arg None "withtac" - -open Obligations - -VERNAC COMMAND EXTEND Obligations -| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> - [ obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> - [ obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] -> - [ obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) withtac(tac) ] -> - [ obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] -END - -VERNAC COMMAND EXTEND Solve_Obligation -| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] - END - -VERNAC COMMAND EXTEND Solve_Obligations -| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "with" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] - END - -VERNAC COMMAND EXTEND Solve_All_Obligations -| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] - END - -VERNAC COMMAND EXTEND Admit_Obligations -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] - END - -VERNAC COMMAND EXTEND Set_Solver -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - set_default_tactic - (Vernacexpr.use_section_locality ()) - (Tacinterp.glob_tactic t) ] -END - -open Pp - -VERNAC COMMAND EXTEND Show_Solver -| [ "Show" "Obligation" "Tactic" ] -> [ - msgnl (str"Program obligation tactic is " ++ print_default_tactic ()) ] -END - -VERNAC COMMAND EXTEND Show_Obligations -| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] -| [ "Obligations" ] -> [ show_obligations None ] -END - -VERNAC COMMAND EXTEND Show_Preterm -| [ "Preterm" "of" ident(name) ] -> [ show_term (Some name) ] -| [ "Preterm" ] -> [ show_term None ] -END - -open Pp - -(* Declare a printer for the content of Program tactics *) -let () = - let printer _ _ _ = function - | None -> mt () - | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic (Global.env ()) tac - in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule - (rawwit_withtac, printer) - (globwit_withtac, dummy) - (wit_withtac, dummy) diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index b46d8fa8a3..d242036f7f 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -18,7 +18,6 @@ Backtrack Vernacinterp Mltop Vernacentries -G_obligations Whelp Vernac Ide_slave -- cgit v1.2.3