diff options
Diffstat (limited to 'plugins/subtac/g_subtac.ml4')
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 167 |
1 files changed, 0 insertions, 167 deletions
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 deleted file mode 100644 index c89d135f..00000000 --- a/plugins/subtac/g_subtac.ml4 +++ /dev/null @@ -1,167 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -(* - Syntax for the subtac terms and types. - Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) - - -open Flags -open Util -open Names -open Nameops -open Vernacentries -open Reduction -open Term -open Libnames -open Topconstr - -(* We define new entries for programs, with the use of this module - * Subtac. These entries are named Subtac.<foo> - *) - -module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic - -module SubtacGram = -struct - let gec s = Gram.entry_create ("Subtac."^s) - (* types *) - let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc" - - let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac" -end - -open Glob_term -open SubtacGram -open Util -open Pcoq -open Prim -open Constr -let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) - -GEXTEND Gram - GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac; - - subtac_gallina_loc: - [ [ g = Vernac.gallina -> loc, g - | g = Vernac.gallina_ext -> loc, g ] ] - ; - - subtac_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 gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstract_argument_type - -let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype), - (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype), - (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) = - Genarg.create_arg None "subtac_gallina_loc" - -type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type - -let (wit_subtac_withtac : Genarg.tlevel withtac_argtype), - (globwit_subtac_withtac : Genarg.glevel withtac_argtype), - (rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) = - Genarg.create_arg None "subtac_withtac" - -VERNAC COMMAND EXTEND Subtac -[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ] - END - -let try_catch_exn f e = - try f e - with exn when Errors.noncritical exn -> - errorlabstrm "Program" (Errors.print exn) - -let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e -let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e -let try_solve_obligation e = try_catch_exn Subtac_obligations.try_solve_obligation e -let try_solve_obligations e = try_catch_exn Subtac_obligations.try_solve_obligations e -let solve_all_obligations e = try_catch_exn Subtac_obligations.solve_all_obligations e -let admit_obligations e = try_catch_exn Subtac_obligations.admit_obligations e - -VERNAC COMMAND EXTEND Subtac_Obligations -| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) subtac_withtac(tac) ] -> - [ subtac_obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) subtac_withtac(tac) ] -> - [ subtac_obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lconstr(t) subtac_withtac(tac) ] -> - [ subtac_obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) subtac_withtac(tac) ] -> - [ subtac_obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) subtac_withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" subtac_withtac(tac) ] -> [ next_obligation None tac ] -END - -VERNAC COMMAND EXTEND Subtac_Solve_Obligation -| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] - END - -VERNAC COMMAND EXTEND Subtac_Solve_Obligations -| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "using" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] - END - -VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations -| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] - END - -VERNAC COMMAND EXTEND Subtac_Admit_Obligations -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] - END - -VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - Subtac_obligations.set_default_tactic - (Vernacexpr.use_section_locality ()) - (Tacinterp.glob_tactic t) ] -END - -open Pp - -VERNAC COMMAND EXTEND Subtac_Show_Solver -| [ "Show" "Obligation" "Tactic" ] -> [ - msgnl (str"Program obligation tactic is " ++ Subtac_obligations.print_default_tactic ()) ] -END - -VERNAC COMMAND EXTEND Subtac_Show_Obligations -| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] -| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] -END - -VERNAC COMMAND EXTEND Subtac_Show_Preterm -| [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ] -| [ "Preterm" ] -> [ Subtac_obligations.show_term None ] -END |