diff options
| -rw-r--r-- | pretyping/pretyping.ml | 1 | ||||
| -rw-r--r-- | toplevel/g_obligations.ml4 | 147 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 2 | ||||
| -rw-r--r-- | toplevel/obligations.mli | 2 |
4 files changed, 149 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 08eaa8867..a9581e8ba 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -138,7 +138,6 @@ let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) = (* Side-effect *) !evdref,c -<<<<<<< HEAD (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 new file mode 100644 index 000000000..7d155ab41 --- /dev/null +++ b/toplevel/g_obligations.ml4 @@ -0,0 +1,147 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \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 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 + +GEXTEND Gram + GLOBAL: withtac; + + withtac: + [ [ "with"; t = Tactic.tactic -> Some t + | -> None ] ] + ; + + 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 "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/obligations.ml b/toplevel/obligations.ml index ae25b4fde..529228d01 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -804,7 +804,7 @@ let rec solve_obligation prg num tac = | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) -and subtac_obligation (user_num, name, typ) tac = +and obligation (user_num, name, typ) tac = let num = pred user_num in let prg = get_prog_err name in let obls, rem = prg.prg_obligations in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index de020f8e3..1758082e8 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -92,7 +92,7 @@ val add_mutual_definitions : notations -> fixpoint_kind -> unit -val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> +val obligation : int * Names.identifier option * Topconstr.constr_expr option -> Tacexpr.raw_tactic_expr option -> unit val next_obligation : Names.identifier option -> Tacexpr.raw_tactic_expr option -> unit |