aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/coretactics.ml42
-rw-r--r--ltac/evar_tactics.ml4
-rw-r--r--ltac/extraargs.ml418
-rw-r--r--ltac/extratactics.ml49
-rw-r--r--ltac/g_auto.ml44
-rw-r--r--ltac/g_class.ml44
-rw-r--r--ltac/g_ltac.ml449
-rw-r--r--ltac/g_obligations.ml418
-rw-r--r--ltac/g_rewrite.ml44
-rw-r--r--ltac/g_tactic.ml4665
-rw-r--r--ltac/ltac.mllib5
-rw-r--r--ltac/pltac.ml65
-rw-r--r--ltac/pltac.mli38
-rw-r--r--ltac/pptactic.ml1361
-rw-r--r--ltac/pptactic.mli67
-rw-r--r--ltac/pptacticsig.mli81
-rw-r--r--ltac/rewrite.ml16
-rw-r--r--ltac/tacarg.ml26
-rw-r--r--ltac/tacarg.mli27
-rw-r--r--ltac/taccoerce.ml1
-rw-r--r--ltac/tacentries.ml48
-rw-r--r--ltac/tacentries.mli2
-rw-r--r--ltac/tacenv.ml2
-rw-r--r--ltac/tacexpr.mli396
-rw-r--r--ltac/tacintern.ml57
-rw-r--r--ltac/tacinterp.ml58
-rw-r--r--ltac/tacsubst.ml3
-rw-r--r--ltac/tactic_matching.ml377
-rw-r--r--ltac/tactic_matching.mli49
29 files changed, 3330 insertions, 126 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 618666758..28ff6df83 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -13,7 +13,7 @@ open Names
open Locus
open Misctypes
open Genredexpr
-open Constrarg
+open Stdarg
open Extraargs
open Sigma.Notations
diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index 30aeba3bb..c5b26e6d5 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -18,6 +18,8 @@ open Sigma.Notations
open Proofview.Notations
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
(* The instantiate tactic *)
let instantiate_evar evk (ist,rawc) sigma =
@@ -48,7 +50,7 @@ let instantiate_tac n c ido =
| _ -> error
"Please be more specific: in type or value?")
| InHypTypeOnly ->
- evar_list (get_type decl)
+ evar_list (NamedDecl.get_type decl)
| InHypValueOnly ->
(match decl with
| LocalDef (_,body,_) -> evar_list body
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 0db1cd7ba..53b726432 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -11,7 +11,7 @@
open Pp
open Genarg
open Stdarg
-open Constrarg
+open Tacarg
open Pcoq.Prim
open Pcoq.Constr
open Names
@@ -31,15 +31,15 @@ let create_generic_quotation name e wit =
let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
-let () = create_generic_quotation "ident" Pcoq.Prim.ident Constrarg.wit_ident
-let () = create_generic_quotation "reference" Pcoq.Prim.reference Constrarg.wit_ref
-let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr
-let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr
-let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern
-let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr
+let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
+let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
+let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
+let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr
+let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern
+let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
let () =
let inject (loc, v) = Tacexpr.Tacexp v in
- Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+ Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5)
(** Backward-compatible tactic notation entry names *)
@@ -262,7 +262,7 @@ let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl
let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl
-let in_clause' = Pcoq.Tactic.in_clause
+let in_clause' = Pltac.in_clause
ARGUMENT EXTEND in_clause
TYPED AS clause_dft_concl
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index d6ba670d8..23ce5fb4e 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -11,10 +11,10 @@
open Pp
open Genarg
open Stdarg
-open Constrarg
+open Tacarg
open Extraargs
open Pcoq.Prim
-open Pcoq.Tactic
+open Pltac
open Mod_subst
open Names
open Tacexpr
@@ -27,7 +27,6 @@ open Equality
open Misctypes
open Sigma.Notations
open Proofview.Notations
-open Constrarg
DECLARE PLUGIN "extratactics"
@@ -53,7 +52,7 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
let replace_term ist dir_opt c cl =
with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
-let clause = Pcoq.Tactic.clause_dft_concl
+let clause = Pltac.clause_dft_concl
TACTIC EXTEND replace
["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
@@ -984,7 +983,7 @@ let pr_cmp' _prc _prlc _prt = pr_cmp
let pr_test_gen f (Test(c,x,y)) =
Pp.(f x ++ pr_cmp c ++ f y)
-let pr_test = pr_test_gen (Pptactic.pr_or_var Pp.int)
+let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int)
let pr_test' _prc _prlc _prt = pr_test
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 8bc2ffd65..82ba63871 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -11,10 +11,10 @@
open Pp
open Genarg
open Stdarg
-open Constrarg
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
+open Hints
open Tacexpr
DECLARE PLUGIN "g_auto"
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 18df596eb..f8654d390 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -10,9 +10,9 @@
open Misctypes
open Class_tactics
-open Pcoq.Tactic
+open Pltac
open Stdarg
-open Constrarg
+open Tacarg
DECLARE PLUGIN "g_class"
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index a3ca4ebc4..54229bb2a 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -19,8 +19,10 @@ open Genredexpr
open Tok (* necessary for camlp4 *)
open Pcoq
+open Pcoq.Constr
+open Pcoq.Vernac_
open Pcoq.Prim
-open Pcoq.Tactic
+open Pltac
let fail_default_value = ArgArg 0
@@ -30,14 +32,15 @@ let arg_of_expr = function
let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
-let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
-let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
+let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat
+let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
+let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
let reference_to_id = function
| Libnames.Ident (loc, id) -> (loc, id)
| Libnames.Qualid (loc,_) ->
- CErrors.user_err_loc (loc, "",
- str "This expression should be a simple identifier.")
+ CErrors.user_err ~loc
+ (str "This expression should be a simple identifier.")
let tactic_mode = Gram.entry_create "vernac:tactic_command"
@@ -71,14 +74,17 @@ let test_bracket_ident =
(* Tactics grammar rules *)
+let hint = G_proofs.hint
+
let warn_deprecated_appcontext =
CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated"
(fun () -> strbrk "appcontext is deprecated and will be removed " ++
strbrk "in a future version")
GEXTEND Gram
- GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
- tactic_mode constr_may_eval constr_eval toplevel_selector;
+ GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint
+ tactic_mode constr_may_eval constr_eval toplevel_selector
+ operconstr;
tactic_then_last:
[ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
@@ -286,15 +292,15 @@ GEXTEND Gram
(* Definitions for tactics *)
tacdef_body:
[ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
- if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body))
+ if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
else
let id = reference_to_id name in
- Vernacexpr.TacticDefinition (id, TacFun (it, body))
+ Tacexpr.TacticDefinition (id, TacFun (it, body))
| name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
- if redef then Vernacexpr.TacticRedefinition (name, body)
+ if redef then Tacexpr.TacticRedefinition (name, body)
else
let id = reference_to_id name in
- Vernacexpr.TacticDefinition (id, body)
+ Tacexpr.TacticDefinition (id, body)
] ]
;
tactic:
@@ -329,9 +335,28 @@ GEXTEND Gram
tactic_mode:
[ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ]
;
+ command:
+ [ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
+ l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+ Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l)
+ | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
+ ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] ->
+ Vernacexpr.VernacProof (ta,Some l) ] ]
+ ;
+ hint:
+ [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
+ tac = Pltac.tactic ->
+ Vernacexpr.HintsExtern (n,c, in_tac tac) ] ]
+ ;
+ operconstr: LEVEL "0"
+ [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
+ let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
+ CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
+ ;
END
-open Constrarg
+open Stdarg
+open Tacarg
open Vernacexpr
open Vernac_classifier
open Goptions
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index 987b9d538..d286a5870 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -17,7 +17,7 @@ open Libnames
open Constrexpr
open Constrexpr_ops
open Stdarg
-open Constrarg
+open Tacarg
open Extraargs
let (set_default_tactic, get_default_tactic, print_default_tactic) =
@@ -30,12 +30,23 @@ let () =
end in
Obligations.default_tactic := tac
+let with_tac f tac =
+ let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in
+ let tac = match tac with
+ | None -> None
+ | Some tac ->
+ let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in
+ let _, tac = Genintern.generic_intern env tac in
+ Some tac
+ in
+ f tac
+
(* We define new entries for programs, with the use of this module
* Subtac. These entries are named Subtac.<foo>
*)
module Gram = Pcoq.Gram
-module Tactic = Pcoq.Tactic
+module Tactic = Pltac
open Pcoq
@@ -66,6 +77,9 @@ GEXTEND Gram
open Obligations
+let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
+
let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 82b79c883..3168898a3 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -21,10 +21,10 @@ open Tacmach
open Tacticals
open Rewrite
open Stdarg
-open Constrarg
+open Pcoq.Vernac_
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
DECLARE PLUGIN "g_rewrite"
diff --git a/ltac/g_tactic.ml4 b/ltac/g_tactic.ml4
new file mode 100644
index 000000000..685c07c9a
--- /dev/null
+++ b/ltac/g_tactic.ml4
@@ -0,0 +1,665 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Tacexpr
+open Genredexpr
+open Constrexpr
+open Libnames
+open Tok
+open Compat
+open Misctypes
+open Locus
+open Decl_kinds
+
+open Pcoq
+
+
+let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
+
+let tactic_kw = [ "->"; "<-" ; "by" ]
+let _ = List.iter CLexer.add_keyword tactic_kw
+
+let err () = raise Stream.Failure
+
+(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
+(* admissible notation "(x t)" *)
+let test_lpar_id_coloneq =
+ Gram.Entry.of_parser "lpar_id_coloneq"
+ (fun strm ->
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "(" ->
+ (match get_tok (stream_nth 1 strm) with
+ | IDENT _ ->
+ (match get_tok (stream_nth 2 strm) with
+ | KEYWORD ":=" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
+(* Hack to recognize "(x)" *)
+let test_lpar_id_rpar =
+ Gram.Entry.of_parser "lpar_id_coloneq"
+ (fun strm ->
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "(" ->
+ (match get_tok (stream_nth 1 strm) with
+ | IDENT _ ->
+ (match get_tok (stream_nth 2 strm) with
+ | KEYWORD ")" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
+(* idem for (x:=t) and (1:=t) *)
+let test_lpar_idnum_coloneq =
+ Gram.Entry.of_parser "test_lpar_idnum_coloneq"
+ (fun strm ->
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "(" ->
+ (match get_tok (stream_nth 1 strm) with
+ | IDENT _ | INT _ ->
+ (match get_tok (stream_nth 2 strm) with
+ | KEYWORD ":=" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
+(* idem for (x:t) *)
+let test_lpar_id_colon =
+ Gram.Entry.of_parser "lpar_id_colon"
+ (fun strm ->
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "(" ->
+ (match get_tok (stream_nth 1 strm) with
+ | IDENT _ ->
+ (match get_tok (stream_nth 2 strm) with
+ | KEYWORD ":" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
+(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
+let check_for_coloneq =
+ Gram.Entry.of_parser "lpar_id_colon"
+ (fun strm ->
+ let rec skip_to_rpar p n =
+ match get_tok (List.last (Stream.npeek n strm)) with
+ | KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
+ | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1)
+ | KEYWORD "." -> err ()
+ | _ -> skip_to_rpar p (n+1) in
+ let rec skip_names n =
+ match get_tok (List.last (Stream.npeek n strm)) with
+ | IDENT _ | KEYWORD "_" -> skip_names (n+1)
+ | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
+ | _ -> err () in
+ let rec skip_binders n =
+ match get_tok (List.last (Stream.npeek n strm)) with
+ | KEYWORD "(" -> skip_binders (skip_names (n+1))
+ | IDENT _ | KEYWORD "_" -> skip_binders (n+1)
+ | KEYWORD ":=" -> ()
+ | _ -> err () in
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "(" -> skip_binders 2
+ | _ -> err ())
+
+let lookup_at_as_comma =
+ Gram.Entry.of_parser "lookup_at_as_comma"
+ (fun strm ->
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD (","|"at"|"as") -> ()
+ | _ -> err ())
+
+open Constr
+open Prim
+open Pltac
+
+let mk_fix_tac (loc,id,bl,ann,ty) =
+ let n =
+ match bl,ann with
+ [([_],_,_)], None -> 1
+ | _, Some x ->
+ let ids = List.map snd (List.flatten (List.map pi1 bl)) in
+ (try List.index Names.Name.equal (snd x) ids
+ with Not_found -> error "No such fix variable.")
+ | _ -> error "Cannot guess decreasing argument of fix." in
+ (id,n,CProdN(loc,bl,ty))
+
+let mk_cofix_tac (loc,id,bl,ann,ty) =
+ let _ = Option.map (fun (aloc,_) ->
+ user_err ~loc:aloc
+ ~hdr:"Constr:mk_cofix_tac"
+ (Pp.str"Annotation forbidden in cofix expression.")) ann in
+ (id,CProdN(loc,bl,ty))
+
+(* Functions overloaded by quotifier *)
+let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
+ | NoBindings ->
+ begin
+ try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c))
+ with e when CErrors.noncritical e -> ElimOnConstr clbind
+ end
+ | _ -> ElimOnConstr clbind
+
+let mkTacCase with_evar = function
+ | [(clear,ElimOnConstr cl),(None,None),None],None ->
+ TacCase (with_evar,(clear,cl))
+ (* Reinterpret numbers as a notation for terms *)
+ | [(clear,ElimOnAnonHyp n),(None,None),None],None ->
+ TacCase (with_evar,
+ (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
+ NoBindings)))
+ (* Reinterpret ident as notations for variables in the context *)
+ (* because we don't know if they are quantified or not *)
+ | [(clear,ElimOnIdent id),(None,None),None],None ->
+ TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings)))
+ | ic ->
+ if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
+ then
+ error "Use of numbers as direct arguments of 'case' is not supported.";
+ TacInductionDestruct (false,with_evar,ic)
+
+let rec mkCLambdaN_simple_loc loc bll c =
+ match bll with
+ | ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
+ | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
+ | [] -> c
+
+let mkCLambdaN_simple bl c = match bl with
+ | [] -> c
+ | h :: _ ->
+ let loc = Loc.merge (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in
+ mkCLambdaN_simple_loc loc bl c
+
+let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (List.last l))
+
+let map_int_or_var f = function
+ | ArgArg x -> ArgArg (f x)
+ | ArgVar _ as y -> y
+
+let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }
+
+let merge_occurrences loc cl = function
+ | None ->
+ if Locusops.clause_with_generic_occurrences cl then (None, cl)
+ else
+ user_err ~loc (str "Found an \"at\" clause without \"with\" clause.")
+ | Some (occs, p) ->
+ let ans = match occs with
+ | AllOccurrences -> cl
+ | _ ->
+ begin match cl with
+ | { onhyps = Some []; concl_occs = AllOccurrences } ->
+ { onhyps = Some []; concl_occs = occs }
+ | { onhyps = Some [(AllOccurrences, id), l]; concl_occs = NoOccurrences } ->
+ { cl with onhyps = Some [(occs, id), l] }
+ | _ ->
+ if Locusops.clause_with_generic_occurrences cl then
+ user_err ~loc (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
+ else
+ user_err ~loc (str "Cannot use clause \"at\" twice.")
+ end
+ in
+ (Some p, ans)
+
+let warn_deprecated_eqn_syntax =
+ CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated"
+ (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg))
+
+(* Auxiliary grammar rules *)
+
+open Vernac_
+
+GEXTEND Gram
+ GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
+ bindings red_expr int_or_var open_constr uconstr
+ simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
+
+ int_or_var:
+ [ [ n = integer -> ArgArg n
+ | id = identref -> ArgVar id ] ]
+ ;
+ nat_or_var:
+ [ [ n = natural -> ArgArg n
+ | id = identref -> ArgVar id ] ]
+ ;
+ (* An identifier or a quotation meta-variable *)
+ id_or_meta:
+ [ [ id = identref -> id ] ]
+ ;
+ open_constr:
+ [ [ c = constr -> c ] ]
+ ;
+ uconstr:
+ [ [ c = constr -> c ] ]
+ ;
+ destruction_arg:
+ [ [ n = natural -> (None,ElimOnAnonHyp n)
+ | test_lpar_id_rpar; c = constr_with_bindings ->
+ (Some false,destruction_arg_of_constr c)
+ | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c
+ ] ]
+ ;
+ constr_with_bindings_arg:
+ [ [ ">"; c = constr_with_bindings -> (Some true,c)
+ | c = constr_with_bindings -> (None,c) ] ]
+ ;
+ quantified_hypothesis:
+ [ [ id = ident -> NamedHyp id
+ | n = natural -> AnonHyp n ] ]
+ ;
+ conversion:
+ [ [ c = constr -> (None, c)
+ | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2)
+ | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
+ (Some (occs,c1), c2) ] ]
+ ;
+ occs_nums:
+ [ [ nl = LIST1 nat_or_var -> OnlyOccurrences nl
+ | "-"; n = nat_or_var; nl = LIST0 int_or_var ->
+ (* have used int_or_var instead of nat_or_var for compatibility *)
+ AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ]
+ ;
+ occs:
+ [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ]
+ ;
+ pattern_occ:
+ [ [ c = constr; nl = occs -> (nl,c) ] ]
+ ;
+ ref_or_pattern_occ:
+ (* If a string, it is interpreted as a ref
+ (anyway a Coq string does not reduce) *)
+ [ [ c = smart_global; nl = occs -> nl,Inl c
+ | c = constr; nl = occs -> nl,Inr c ] ]
+ ;
+ unfold_occ:
+ [ [ c = smart_global; nl = occs -> (nl,c) ] ]
+ ;
+ intropatterns:
+ [ [ l = LIST0 nonsimple_intropattern -> l ]]
+ ;
+ ne_intropatterns:
+ [ [ l = LIST1 nonsimple_intropattern -> l ]]
+ ;
+ or_and_intropattern:
+ [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc
+ | "()" -> IntroAndPattern []
+ | "("; si = simple_intropattern; ")" -> IntroAndPattern [si]
+ | "("; si = simple_intropattern; ",";
+ tc = LIST1 simple_intropattern SEP "," ; ")" ->
+ IntroAndPattern (si::tc)
+ | "("; si = simple_intropattern; "&";
+ tc = LIST1 simple_intropattern SEP "&" ; ")" ->
+ (* (A & B & C) is translated into (A,(B,C)) *)
+ let rec pairify = function
+ | ([]|[_]|[_;_]) as l -> l
+ | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
+ in IntroAndPattern (pairify (si::tc)) ] ]
+ ;
+ equality_intropattern:
+ [ [ "->" -> IntroRewrite true
+ | "<-" -> IntroRewrite false
+ | "[="; tc = intropatterns; "]" -> IntroInjection tc ] ]
+ ;
+ naming_intropattern:
+ [ [ prefix = pattern_ident -> IntroFresh prefix
+ | "?" -> IntroAnonymous
+ | id = ident -> IntroIdentifier id ] ]
+ ;
+ nonsimple_intropattern:
+ [ [ l = simple_intropattern -> l
+ | "*" -> !@loc, IntroForthcoming true
+ | "**" -> !@loc, IntroForthcoming false ]]
+ ;
+ simple_intropattern:
+ [ [ pat = simple_intropattern_closed;
+ l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
+ let loc0,pat = pat in
+ let f c pat =
+ let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
+ IntroAction (IntroApplyOn (c,(loc,pat))) in
+ !@loc, List.fold_right f l pat ] ]
+ ;
+ simple_intropattern_closed:
+ [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
+ | pat = equality_intropattern -> !@loc, IntroAction pat
+ | "_" -> !@loc, IntroAction IntroWildcard
+ | pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
+ ;
+ simple_binding:
+ [ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c)
+ | "("; n = natural; ":="; c = lconstr; ")" -> (!@loc, AnonHyp n, c) ] ]
+ ;
+ bindings:
+ [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
+ ExplicitBindings bl
+ | bl = LIST1 constr -> ImplicitBindings bl ] ]
+ ;
+ constr_with_bindings:
+ [ [ c = constr; l = with_bindings -> (c, l) ] ]
+ ;
+ with_bindings:
+ [ [ "with"; bl = bindings -> bl | -> NoBindings ] ]
+ ;
+ red_flags:
+ [ [ IDENT "beta" -> [FBeta]
+ | IDENT "iota" -> [FMatch;FFix;FCofix]
+ | IDENT "match" -> [FMatch]
+ | IDENT "fix" -> [FFix]
+ | IDENT "cofix" -> [FCofix]
+ | IDENT "zeta" -> [FZeta]
+ | IDENT "delta"; d = delta_flag -> [d]
+ ] ]
+ ;
+ delta_flag:
+ [ [ "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl
+ | "["; idl = LIST1 smart_global; "]" -> FConst idl
+ | -> FDeltaBut []
+ ] ]
+ ;
+ strategy_flag:
+ [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s)
+ | d = delta_flag -> all_with d
+ ] ]
+ ;
+ red_expr:
+ [ [ IDENT "red" -> Red false
+ | IDENT "hnf" -> Hnf
+ | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
+ | IDENT "cbv"; s = strategy_flag -> Cbv s
+ | IDENT "cbn"; s = strategy_flag -> Cbn s
+ | IDENT "lazy"; s = strategy_flag -> Lazy s
+ | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
+ | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
+ | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
+ | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
+ | IDENT "fold"; cl = LIST1 constr -> Fold cl
+ | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl
+ | s = IDENT -> ExtraRedExpr s ] ]
+ ;
+ hypident:
+ [ [ id = id_or_meta ->
+ id,InHyp
+ | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
+ id,InHypTypeOnly
+ | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
+ id,InHypValueOnly
+ ] ]
+ ;
+ hypident_occ:
+ [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ]
+ ;
+ in_clause:
+ [ [ "*"; occs=occs ->
+ {onhyps=None; concl_occs=occs}
+ | "*"; "|-"; occs=concl_occ ->
+ {onhyps=None; concl_occs=occs}
+ | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
+ {onhyps=Some hl; concl_occs=occs}
+ | hl=LIST0 hypident_occ SEP"," ->
+ {onhyps=Some hl; concl_occs=NoOccurrences} ] ]
+ ;
+ clause_dft_concl:
+ [ [ "in"; cl = in_clause -> cl
+ | occs=occs -> {onhyps=Some[]; concl_occs=occs}
+ | -> all_concl_occs_clause ] ]
+ ;
+ clause_dft_all:
+ [ [ "in"; cl = in_clause -> cl
+ | -> {onhyps=None; concl_occs=AllOccurrences} ] ]
+ ;
+ opt_clause:
+ [ [ "in"; cl = in_clause -> Some cl
+ | "at"; occs = occs_nums -> Some {onhyps=Some[]; concl_occs=occs}
+ | -> None ] ]
+ ;
+ concl_occ:
+ [ [ "*"; occs = occs -> occs
+ | -> NoOccurrences ] ]
+ ;
+ in_hyp_list:
+ [ [ "in"; idl = LIST1 id_or_meta -> idl
+ | -> [] ] ]
+ ;
+ in_hyp_as:
+ [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
+ | -> None ] ]
+ ;
+ orient:
+ [ [ "->" -> true
+ | "<-" -> false
+ | -> true ]]
+ ;
+ simple_binder:
+ [ [ na=name -> ([na],Default Explicit,CHole (!@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
+ | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
+ ] ]
+ ;
+ fixdecl:
+ [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot;
+ ":"; ty=lconstr; ")" -> (!@loc, id, bl, ann, ty) ] ]
+ ;
+ fixannot:
+ [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
+ | -> None ] ]
+ ;
+ cofixdecl:
+ [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" ->
+ (!@loc, id, bl, None, ty) ] ]
+ ;
+ bindings_with_parameters:
+ [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder;
+ ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ]
+ ;
+ eliminator:
+ [ [ "using"; el = constr_with_bindings -> el ] ]
+ ;
+ as_ipat:
+ [ [ "as"; ipat = simple_intropattern -> Some ipat
+ | -> None ] ]
+ ;
+ or_and_intropattern_loc:
+ [ [ ipat = or_and_intropattern -> ArgArg (!@loc,ipat)
+ | locid = identref -> ArgVar locid ] ]
+ ;
+ as_or_and_ipat:
+ [ [ "as"; ipat = or_and_intropattern_loc -> Some ipat
+ | -> None ] ]
+ ;
+ eqn_ipat:
+ [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
+ | IDENT "_eqn"; ":"; pat = naming_intropattern ->
+ let loc = !@loc in
+ warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat)
+ | IDENT "_eqn" ->
+ let loc = !@loc in
+ warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous)
+ | -> None ] ]
+ ;
+ as_name:
+ [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
+ ;
+ by_tactic:
+ [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
+ | -> None ] ]
+ ;
+ rewriter :
+ [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c)
+ | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
+ | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c)
+ | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c)
+ | n = natural; c = constr_with_bindings_arg -> (Precisely n,c)
+ | c = constr_with_bindings_arg -> (Precisely 1, c)
+ ] ]
+ ;
+ oriented_rewriter :
+ [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
+ ;
+ induction_clause:
+ [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
+ cl = opt_clause -> (c,(eq,pat),cl) ] ]
+ ;
+ induction_clause_list:
+ [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator;
+ cl_tolerance = opt_clause ->
+ (* Condition for accepting "in" at the end by compatibility *)
+ match ic,el,cl_tolerance with
+ | [c,pat,None],Some _,Some _ -> ([c,pat,cl_tolerance],el)
+ | _,_,Some _ -> err ()
+ | _,_,None -> (ic,el) ]]
+ ;
+ simple_tactic:
+ [ [
+ (* Basic tactics *)
+ IDENT "intros"; pl = ne_intropatterns ->
+ TacAtom (!@loc, TacIntroPattern (false,pl))
+ | IDENT "intros" ->
+ TacAtom (!@loc, TacIntroPattern (false,[!@loc,IntroForthcoming false]))
+ | IDENT "eintros"; pl = ne_intropatterns ->
+ TacAtom (!@loc, TacIntroPattern (true,pl))
+
+ | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
+ inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
+ | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
+ inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,true,cl,inhyp))
+ | IDENT "simple"; IDENT "apply";
+ cl = LIST1 constr_with_bindings_arg SEP ",";
+ inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,false,cl,inhyp))
+ | IDENT "simple"; IDENT "eapply";
+ cl = LIST1 constr_with_bindings_arg SEP",";
+ inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,true,cl,inhyp))
+ | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
+ TacAtom (!@loc, TacElim (false,cl,el))
+ | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
+ TacAtom (!@loc, TacElim (true,cl,el))
+ | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl)
+ | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl)
+ | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
+ TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd))
+ | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
+ TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd))
+
+ | IDENT "pose"; (id,b) = bindings_with_parameters ->
+ TacAtom (!@loc, TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
+ | IDENT "pose"; b = constr; na = as_name ->
+ TacAtom (!@loc, TacLetTac (na,b,Locusops.nowhere,true,None))
+ | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
+ TacAtom (!@loc, TacLetTac (Names.Name id,c,p,true,None))
+ | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
+ TacAtom (!@loc, TacLetTac (na,c,p,true,None))
+ | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
+ p = clause_dft_all ->
+ TacAtom (!@loc, TacLetTac (na,c,p,false,e))
+
+ (* Alternative syntax for "pose proof c as id" *)
+ | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+ c = lconstr; ")" ->
+ TacAtom (!@loc, TacAssert (true,None,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+
+ (* Alternative syntax for "assert c as id by tac" *)
+ | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ c = lconstr; ")"; tac=by_tactic ->
+ TacAtom (!@loc, TacAssert (true,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+
+ (* Alternative syntax for "enough c as id by tac" *)
+ | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ c = lconstr; ")"; tac=by_tactic ->
+ TacAtom (!@loc, TacAssert (false,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+
+ | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
+ TacAtom (!@loc, TacAssert (true,Some tac,ipat,c))
+ | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
+ TacAtom (!@loc, TacAssert (true,None,ipat,c))
+ | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
+ TacAtom (!@loc, TacAssert (false,Some tac,ipat,c))
+
+ | IDENT "generalize"; c = constr ->
+ TacAtom (!@loc, TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
+ | IDENT "generalize"; c = constr; l = LIST1 constr ->
+ let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in
+ TacAtom (!@loc, TacGeneralize (List.map gen_everywhere (c::l)))
+ | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
+ na = as_name;
+ l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
+ TacAtom (!@loc, TacGeneralize (((nl,c),na)::l))
+
+ (* Derived basic tactics *)
+ | IDENT "induction"; ic = induction_clause_list ->
+ TacAtom (!@loc, TacInductionDestruct (true,false,ic))
+ | IDENT "einduction"; ic = induction_clause_list ->
+ TacAtom (!@loc, TacInductionDestruct(true,true,ic))
+ | IDENT "destruct"; icl = induction_clause_list ->
+ TacAtom (!@loc, TacInductionDestruct(false,false,icl))
+ | IDENT "edestruct"; icl = induction_clause_list ->
+ TacAtom (!@loc, TacInductionDestruct(false,true,icl))
+
+ (* Equality and inversion *)
+ | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
+ cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
+ | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
+ cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t))
+ | IDENT "dependent"; k =
+ [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
+ | IDENT "inversion" -> FullInversion
+ | IDENT "inversion_clear" -> FullInversionClear ];
+ hyp = quantified_hypothesis;
+ ids = as_or_and_ipat; co = OPT ["with"; c = constr -> c] ->
+ TacAtom (!@loc, TacInversion (DepInversion (k,co,ids),hyp))
+ | IDENT "simple"; IDENT "inversion";
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
+ cl = in_hyp_list ->
+ TacAtom (!@loc, TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
+ | IDENT "inversion";
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
+ cl = in_hyp_list ->
+ TacAtom (!@loc, TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
+ | IDENT "inversion_clear";
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
+ cl = in_hyp_list ->
+ TacAtom (!@loc, TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
+ | IDENT "inversion"; hyp = quantified_hypothesis;
+ "using"; c = constr; cl = in_hyp_list ->
+ TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
+
+ (* Conversion *)
+ | IDENT "red"; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Red false, cl))
+ | IDENT "hnf"; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Hnf, cl))
+ | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl))
+ | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbv s, cl))
+ | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbn s, cl))
+ | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Lazy s, cl))
+ | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl))
+ | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (CbvVm po, cl))
+ | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (CbvNative po, cl))
+ | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Unfold ul, cl))
+ | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Fold l, cl))
+ | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Pattern pl, cl))
+
+ (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
+ | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
+ let p,cl = merge_occurrences (!@loc) cl oc in
+ TacAtom (!@loc, TacChange (p,c,cl))
+ ] ]
+ ;
+END;;
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index fc51e48ae..af1c7149d 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -1,3 +1,6 @@
+Tacarg
+Pptactic
+Pltac
Taccoerce
Tacsubst
Tacenv
@@ -5,6 +8,7 @@ Tactic_debug
Tacintern
Tacentries
Profile_ltac
+Tactic_matching
Tacinterp
Evar_tactics
Tactic_option
@@ -19,4 +23,5 @@ Rewrite
G_rewrite
Tauto
G_eqdecide
+G_tactic
G_ltac
diff --git a/ltac/pltac.ml b/ltac/pltac.ml
new file mode 100644
index 000000000..1d21118ae
--- /dev/null
+++ b/ltac/pltac.ml
@@ -0,0 +1,65 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Pcoq
+
+(* Main entry for extensions *)
+let simple_tactic = Gram.entry_create "tactic:simple_tactic"
+
+let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name)
+
+(* Entries that can be referred via the string -> Gram.entry table *)
+(* Typically for tactic user extensions *)
+let open_constr =
+ make_gen_entry utactic "open_constr"
+let constr_with_bindings =
+ make_gen_entry utactic "constr_with_bindings"
+let bindings =
+ make_gen_entry utactic "bindings"
+let hypident = Gram.entry_create "hypident"
+let constr_may_eval = make_gen_entry utactic "constr_may_eval"
+let constr_eval = make_gen_entry utactic "constr_eval"
+let uconstr =
+ make_gen_entry utactic "uconstr"
+let quantified_hypothesis =
+ make_gen_entry utactic "quantified_hypothesis"
+let destruction_arg = make_gen_entry utactic "destruction_arg"
+let int_or_var = make_gen_entry utactic "int_or_var"
+let simple_intropattern =
+ make_gen_entry utactic "simple_intropattern"
+let in_clause = make_gen_entry utactic "in_clause"
+let clause_dft_concl =
+ make_gen_entry utactic "clause"
+
+
+(* Main entries for ltac *)
+let tactic_arg = Gram.entry_create "tactic:tactic_arg"
+let tactic_expr = make_gen_entry utactic "tactic_expr"
+let binder_tactic = make_gen_entry utactic "binder_tactic"
+
+let tactic = make_gen_entry utactic "tactic"
+
+(* Main entry for quotations *)
+let tactic_eoi = eoi_entry tactic
+
+let () =
+ let open Stdarg in
+ let open Tacarg in
+ register_grammar wit_int_or_var (int_or_var);
+ register_grammar wit_intro_pattern (simple_intropattern);
+ register_grammar wit_quant_hyp (quantified_hypothesis);
+ register_grammar wit_uconstr (uconstr);
+ register_grammar wit_open_constr (open_constr);
+ register_grammar wit_constr_with_bindings (constr_with_bindings);
+ register_grammar wit_bindings (bindings);
+ register_grammar wit_tactic (tactic);
+ register_grammar wit_ltac (tactic);
+ register_grammar wit_clause_dft_concl (clause_dft_concl);
+ register_grammar wit_destruction_arg (destruction_arg);
+ ()
diff --git a/ltac/pltac.mli b/ltac/pltac.mli
new file mode 100644
index 000000000..810e1ec39
--- /dev/null
+++ b/ltac/pltac.mli
@@ -0,0 +1,38 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Ltac parsing entries *)
+
+open Loc
+open Names
+open Pcoq
+open Libnames
+open Constrexpr
+open Tacexpr
+open Genredexpr
+open Misctypes
+
+val open_constr : constr_expr Gram.entry
+val constr_with_bindings : constr_expr with_bindings Gram.entry
+val bindings : constr_expr bindings Gram.entry
+val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
+val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
+val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
+val uconstr : constr_expr Gram.entry
+val quantified_hypothesis : quantified_hypothesis Gram.entry
+val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
+val int_or_var : int or_var Gram.entry
+val simple_tactic : raw_tactic_expr Gram.entry
+val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
+val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry
+val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
+val tactic_arg : raw_tactic_arg Gram.entry
+val tactic_expr : raw_tactic_expr Gram.entry
+val binder_tactic : raw_tactic_expr Gram.entry
+val tactic : raw_tactic_expr Gram.entry
+val tactic_eoi : raw_tactic_expr Gram.entry
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
new file mode 100644
index 000000000..6230fa060
--- /dev/null
+++ b/ltac/pptactic.ml
@@ -0,0 +1,1361 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Names
+open Namegen
+open CErrors
+open Util
+open Constrexpr
+open Tacexpr
+open Genarg
+open Geninterp
+open Stdarg
+open Tacarg
+open Libnames
+open Ppextend
+open Misctypes
+open Locus
+open Decl_kinds
+open Genredexpr
+open Pputils
+open Ppconstr
+open Printer
+
+let pr_global x = Nametab.pr_global_env Id.Set.empty x
+
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
+
+type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
+
+type pp_tactic = {
+ pptac_level : int;
+ pptac_prods : grammar_terminals;
+}
+
+(* Tactic notations *)
+let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
+
+let declare_notation_tactic_pprule kn pt =
+ prnotation_tab := KNmap.add kn pt !prnotation_tab
+
+type 'a raw_extra_genarg_printer =
+ (constr_expr -> std_ppcmds) ->
+ (constr_expr -> std_ppcmds) ->
+ (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+ 'a -> std_ppcmds
+
+type 'a glob_extra_genarg_printer =
+ (glob_constr_and_expr -> std_ppcmds) ->
+ (glob_constr_and_expr -> std_ppcmds) ->
+ (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ 'a -> std_ppcmds
+
+type 'a extra_genarg_printer =
+ (Term.constr -> std_ppcmds) ->
+ (Term.constr -> std_ppcmds) ->
+ (tolerability -> Val.t -> std_ppcmds) ->
+ 'a -> std_ppcmds
+
+module Make
+ (Ppconstr : Ppconstrsig.Pp)
+ (Taggers : sig
+ val tag_keyword
+ : std_ppcmds -> std_ppcmds
+ val tag_primitive
+ : std_ppcmds -> std_ppcmds
+ val tag_string
+ : std_ppcmds -> std_ppcmds
+ val tag_glob_tactic_expr
+ : glob_tactic_expr -> std_ppcmds -> std_ppcmds
+ val tag_glob_atomic_tactic_expr
+ : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
+ val tag_raw_tactic_expr
+ : raw_tactic_expr -> std_ppcmds -> std_ppcmds
+ val tag_raw_atomic_tactic_expr
+ : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
+ val tag_atomic_tactic_expr
+ : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
+ end)
+= struct
+
+ open Taggers
+
+ let keyword x = tag_keyword (str x)
+ let primitive x = tag_primitive (str x)
+
+ let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with
+ | None -> false
+ | Some _ -> true
+
+ let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t ->
+ match Val.eq tag t with
+ | None -> assert false
+ | Some Refl -> x
+
+ let rec pr_value lev v : std_ppcmds =
+ if has_type v Val.typ_list then
+ pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list)
+ else if has_type v Val.typ_opt then
+ pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt)
+ else if has_type v Val.typ_pair then
+ let (v1, v2) = unbox v Val.typ_pair in
+ str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")"
+ else
+ let Val.Dyn (tag, x) = v in
+ let name = Val.repr tag in
+ let default = str "<" ++ str name ++ str ">" in
+ match ArgT.name name with
+ | None -> default
+ | Some (ArgT.Any arg) ->
+ let wit = ExtraArg arg in
+ match val_tag (Topwit wit) with
+ | Val.Base t ->
+ begin match Val.eq t tag with
+ | None -> default
+ | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+ end
+ | _ -> default
+
+ let pr_with_occurrences pr c = pr_with_occurrences pr keyword c
+ let pr_red_expr pr c = pr_red_expr pr keyword c
+
+ let pr_may_eval test prc prlc pr2 pr3 = function
+ | ConstrEval (r,c) ->
+ hov 0
+ (keyword "eval" ++ brk (1,1) ++
+ pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
+ keyword "in" ++ spc() ++ prc c)
+ | ConstrContext ((_,id),c) ->
+ hov 0
+ (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
+ str "[" ++ prlc c ++ str "]")
+ | ConstrTypeOf c ->
+ hov 1 (keyword "type of" ++ spc() ++ prc c)
+ | ConstrTerm c when test c ->
+ h 0 (str "(" ++ prc c ++ str ")")
+ | ConstrTerm c ->
+ prc c
+
+ let pr_may_eval a =
+ pr_may_eval (fun _ -> false) a
+
+ let pr_arg pr x = spc () ++ pr x
+
+ let pr_and_short_name pr (c,_) = pr c
+
+ let pr_or_by_notation f = function
+ | AN v -> f v
+ | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+
+ let pr_located pr (loc,x) = pr x
+
+ let pr_evaluable_reference = function
+ | EvalVarRef id -> pr_id id
+ | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
+
+ let pr_quantified_hypothesis = function
+ | AnonHyp n -> int n
+ | NamedHyp id -> pr_id id
+
+ let pr_binding prc = function
+ | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
+ | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+ let pr_bindings prc prlc = function
+ | ImplicitBindings l ->
+ brk (1,1) ++ keyword "with" ++ brk (1,1) ++
+ hv 0 (prlist_with_sep spc prc l)
+ | ExplicitBindings l ->
+ brk (1,1) ++ keyword "with" ++ brk (1,1) ++
+ hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l)
+ | NoBindings -> mt ()
+
+ let pr_bindings_no_with prc prlc = function
+ | ImplicitBindings l ->
+ brk (0,1) ++
+ prlist_with_sep spc prc l
+ | ExplicitBindings l ->
+ brk (0,1) ++
+ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+ let pr_clear_flag clear_flag pp x =
+ match clear_flag with
+ | Some false -> surround (pp x)
+ | Some true -> str ">" ++ pp x
+ | None -> pp x
+
+ let pr_with_bindings prc prlc (c,bl) =
+ prc c ++ pr_bindings prc prlc bl
+
+ let pr_with_bindings_arg prc prlc (clear_flag,c) =
+ pr_clear_flag clear_flag (pr_with_bindings prc prlc) c
+
+ let pr_with_constr prc = function
+ | None -> mt ()
+ | Some c -> spc () ++ hov 1 (keyword "with" ++ spc () ++ prc c)
+
+ let pr_message_token prid = function
+ | MsgString s -> tag_string (qs s)
+ | MsgInt n -> int n
+ | MsgIdent id -> prid id
+
+ let pr_fresh_ids =
+ prlist (fun s -> spc() ++ pr_or_var (fun s -> tag_string (qs s)) s)
+
+ let with_evars ev s = if ev then "e" ^ s else s
+
+ let rec tacarg_using_rule_token pr_gen = function
+ | [] -> []
+ | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l
+ | TacNonTerm (_, (symb, arg), _) :: l ->
+ pr_gen symb arg :: tacarg_using_rule_token pr_gen l
+
+ let pr_tacarg_using_rule pr_gen l =
+ let l = match l with
+ | TacTerm s :: l ->
+ (** First terminal token should be considered as the name of the tactic,
+ so we tag it differently than the other terminal tokens. *)
+ primitive s :: tacarg_using_rule_token pr_gen l
+ | _ -> tacarg_using_rule_token pr_gen l
+ in
+ pr_sequence (fun x -> x) l
+
+ let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+ let name =
+ str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
+ str "@" ++ int i
+ in
+ let args = match l with
+ | [] -> mt ()
+ | _ -> spc() ++ pr_sequence pr_gen l
+ in
+ str "<" ++ name ++ str ">" ++ args
+
+ let rec pr_user_symbol = function
+ | Extend.Ulist1 tkn -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist1sep (tkn, _) -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist0 tkn -> pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist0sep (tkn, _) -> pr_user_symbol tkn ^ "_list"
+ | Extend.Uopt tkn -> pr_user_symbol tkn ^ "_opt"
+ | Extend.Uentry tag ->
+ let ArgT.Any tag = tag in
+ ArgT.repr tag
+ | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl
+
+ let pr_alias_key key =
+ try
+ let prods = (KNmap.find key !prnotation_tab).pptac_prods in
+ let rec pr = function
+ | TacTerm s -> primitive s
+ | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
+ in
+ pr_sequence pr prods
+ with Not_found ->
+ KerName.print key
+
+ let pr_alias_gen pr_gen lev key l =
+ try
+ let pp = KNmap.find key !prnotation_tab in
+ let rec pack prods args = match prods, args with
+ | [], [] -> []
+ | TacTerm s :: prods, args -> TacTerm s :: pack prods args
+ | TacNonTerm (loc, symb, id) :: prods, arg :: args ->
+ TacNonTerm (loc, (symb, arg), id) :: pack prods args
+ | _ -> raise Not_found
+ in
+ let prods = pack pp.pptac_prods l in
+ let p = pr_tacarg_using_rule pr_gen prods in
+ if pp.pptac_level > lev then surround p else p
+ with Not_found ->
+ let pr arg = str "_" in
+ KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
+
+ let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg))
+
+ let is_genarg tag wit =
+ let ArgT.Any tag = tag in
+ argument_type_eq (ArgumentType (ExtraArg tag)) wit
+
+ let get_list : type l. l generic_argument -> l generic_argument list option =
+ function (GenArg (wit, arg)) -> match wit with
+ | Rawwit (ListArg wit) -> Some (List.map (in_gen (rawwit wit)) arg)
+ | Glbwit (ListArg wit) -> Some (List.map (in_gen (glbwit wit)) arg)
+ | _ -> None
+
+ let get_opt : type l. l generic_argument -> l generic_argument option option =
+ function (GenArg (wit, arg)) -> match wit with
+ | Rawwit (OptArg wit) -> Some (Option.map (in_gen (rawwit wit)) arg)
+ | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg)
+ | _ -> None
+
+ let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds =
+ fun prtac symb arg -> match symb with
+ | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
+ | Extend.Ulist1 s | Extend.Ulist0 s ->
+ begin match get_list arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> pr_sequence (pr_any_arg prtac s) l
+ end
+ | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) ->
+ begin match get_list arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l
+ end
+ | Extend.Uopt s ->
+ begin match get_opt arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> pr_opt (pr_any_arg prtac s) l
+ end
+ | Extend.Uentry _ | Extend.Uentryl _ ->
+ str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+
+ let rec pr_targ prtac symb arg = match symb with
+ | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
+ prtac (1, Any) arg
+ | Extend.Uentryl (_, l) -> prtac (l, Any) arg
+ | _ ->
+ match arg with
+ | TacGeneric arg ->
+ let pr l arg = prtac l (TacGeneric arg) in
+ pr_any_arg pr symb arg
+ | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+
+ let pr_raw_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_farg prtac)
+ let pr_glob_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_farg prtac)
+
+ let pr_raw_alias prc prlc prtac prpat lev key args =
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
+ let pr_glob_alias prc prlc prtac prpat lev key args =
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
+
+ (**********************************************************************)
+ (* The tactic printer *)
+
+ let strip_prod_binders_expr n ty =
+ let rec strip_ty acc n ty =
+ match ty with
+ Constrexpr.CProdN(_,bll,a) ->
+ let nb =
+ List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
+ let bll = List.map (fun (x, _, y) -> x, y) bll in
+ if nb >= n then (List.rev (bll@acc)), a
+ else strip_ty (bll@acc) (n-nb) a
+ | _ -> error "Cannot translate fix tactic: not enough products" in
+ strip_ty [] n ty
+
+ let pr_ltac_or_var pr = function
+ | ArgArg x -> pr x
+ | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
+
+ let pr_ltac_constant kn =
+ if !Flags.in_debugger then pr_kn kn
+ else try
+ pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+ with Not_found -> (* local tactic not accessible anymore *)
+ str "<" ++ pr_kn kn ++ str ">"
+
+ let pr_evaluable_reference_env env = function
+ | EvalVarRef id -> pr_id id
+ | EvalConstRef sp ->
+ Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
+
+ let pr_esubst prc l =
+ let pr_qhyp = function
+ (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
+ | (_,NamedHyp id,c) ->
+ str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
+ in
+ prlist_with_sep spc pr_qhyp l
+
+ let pr_bindings_gen for_ex prc prlc = function
+ | ImplicitBindings l ->
+ spc () ++
+ hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
+ prlist_with_sep spc prc l)
+ | ExplicitBindings l ->
+ spc () ++
+ hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
+ pr_esubst prlc l)
+ | NoBindings -> mt ()
+
+ let pr_bindings prc prlc = pr_bindings_gen false prc prlc
+
+ let pr_with_bindings prc prlc (c,bl) =
+ hov 1 (prc c ++ pr_bindings prc prlc bl)
+
+ let pr_as_disjunctive_ipat prc ipatl =
+ keyword "as" ++ spc () ++
+ pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
+
+ let pr_eqn_ipat (_,ipat) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
+
+ let pr_with_induction_names prc = function
+ | None, None -> mt ()
+ | Some eqpat, None -> hov 1 (pr_eqn_ipat eqpat)
+ | None, Some ipat -> hov 1 (pr_as_disjunctive_ipat prc ipat)
+ | Some eqpat, Some ipat ->
+ hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat)
+
+ let pr_as_intro_pattern prc ipat =
+ spc () ++ hov 1 (keyword "as" ++ spc () ++ Miscprint.pr_intro_pattern prc ipat)
+
+ let pr_with_inversion_names prc = function
+ | None -> mt ()
+ | Some ipat -> pr_as_disjunctive_ipat prc ipat
+
+ let pr_as_ipat prc = function
+ | None -> mt ()
+ | Some ipat -> pr_as_intro_pattern prc ipat
+
+ let pr_as_name = function
+ | Anonymous -> mt ()
+ | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.ghost,id)
+
+ let pr_pose_as_style prc na c =
+ spc() ++ prc c ++ pr_as_name na
+
+ let pr_pose prc prlc na c = match na with
+ | Anonymous -> spc() ++ prc c
+ | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
+
+ let pr_assertion prc prdc _prlc ipat c = match ipat with
+ (* Use this "optimisation" or use only the general case ?
+ | IntroIdentifier id ->
+ spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+ *)
+ | ipat ->
+ spc() ++ prc c ++ pr_as_ipat prdc ipat
+
+ let pr_assumption prc prdc prlc ipat c = match ipat with
+ (* Use this "optimisation" or use only the general case ?*)
+ (* it seems that this "optimisation" is somehow more natural *)
+ | Some (_,IntroNaming (IntroIdentifier id)) ->
+ spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
+ | ipat ->
+ spc() ++ prc c ++ pr_as_ipat prdc ipat
+
+ let pr_by_tactic prt = function
+ | Some tac -> keyword "by" ++ spc () ++ prt tac
+ | None -> mt()
+
+ let pr_hyp_location pr_id = function
+ | occs, InHyp -> pr_with_occurrences pr_id occs
+ | occs, InHypTypeOnly ->
+ pr_with_occurrences (fun id ->
+ str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")"
+ ) occs
+ | occs, InHypValueOnly ->
+ pr_with_occurrences (fun id ->
+ str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
+ ) occs
+
+ let pr_in pp = hov 0 (keyword "in" ++ pp)
+
+ let pr_simple_hyp_clause pr_id = function
+ | [] -> mt ()
+ | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+
+ let pr_in_hyp_as prc pr_id = function
+ | None -> mt ()
+ | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+
+ let pr_in_clause pr_id = function
+ | { onhyps=None; concl_occs=NoOccurrences } ->
+ (str "* |-")
+ | { onhyps=None; concl_occs=occs } ->
+ (pr_with_occurrences (fun () -> str "*") (occs,()))
+ | { onhyps=Some l; concl_occs=NoOccurrences } ->
+ prlist_with_sep (fun () -> str ", ") (pr_hyp_location pr_id) l
+ | { onhyps=Some l; concl_occs=occs } ->
+ let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in
+ (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
+
+ let pr_clauses default_is_concl pr_id = function
+ | { onhyps=Some []; concl_occs=occs }
+ when (match default_is_concl with Some true -> true | _ -> false) ->
+ pr_with_occurrences mt (occs,())
+ | { onhyps=None; concl_occs=AllOccurrences }
+ when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
+ | { onhyps=None; concl_occs=NoOccurrences } ->
+ pr_in (str " * |-")
+ | { onhyps=None; concl_occs=occs } ->
+ pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
+ | { onhyps=Some l; concl_occs=occs } ->
+ let pr_occs = match occs with
+ | NoOccurrences -> mt ()
+ | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
+ in
+ pr_in
+ (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
+
+ let pr_orient b = if b then mt () else str "<- "
+
+ let pr_multi = function
+ | Precisely 1 -> mt ()
+ | Precisely n -> int n ++ str "!"
+ | UpTo n -> int n ++ str "?"
+ | RepeatStar -> str "?"
+ | RepeatPlus -> str "!"
+
+ let pr_core_destruction_arg prc prlc = function
+ | ElimOnConstr c -> pr_with_bindings prc prlc c
+ | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
+ | ElimOnAnonHyp n -> int n
+
+ let pr_destruction_arg prc prlc (clear_flag,h) =
+ pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h
+
+ let pr_inversion_kind = function
+ | SimpleInversion -> primitive "simple inversion"
+ | FullInversion -> primitive "inversion"
+ | FullInversionClear -> primitive "inversion_clear"
+
+ let pr_range_selector (i, j) =
+ if Int.equal i j then int i
+ else int i ++ str "-" ++ int j
+
+ let pr_goal_selector = function
+ | SelectNth i -> int i ++ str ":"
+ | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
+ str "]" ++ str ":"
+ | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+ | SelectAll -> str "all" ++ str ":"
+
+ let pr_lazy = function
+ | General -> keyword "multi"
+ | Select -> keyword "lazy"
+ | Once -> mt ()
+
+ let pr_match_pattern pr_pat = function
+ | Term a -> pr_pat a
+ | Subterm (b,None,a) ->
+ (** ppedrot: we don't make difference between [appcontext] and [context]
+ anymore, and the interpretation is governed by a flag instead. *)
+ keyword "context" ++ str" [" ++ pr_pat a ++ str "]"
+ | Subterm (b,Some id,a) ->
+ keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+
+ let pr_match_hyps pr_pat = function
+ | Hyp (nal,mp) ->
+ pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+ | Def (nal,mv,mp) ->
+ pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv
+ ++ str ":" ++ pr_match_pattern pr_pat mp
+
+ let pr_match_rule m pr pr_pat = function
+ | Pat ([],mp,t) when m ->
+ pr_match_pattern pr_pat mp ++
+ spc () ++ str "=>" ++ brk (1,4) ++ pr t
+ (*
+ | Pat (rl,mp,t) ->
+ hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl ++
+ (if rl <> [] then spc () else mt ()) ++
+ hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+ str "=>" ++ brk (1,4) ++ pr t))
+ *)
+ | Pat (rl,mp,t) ->
+ hov 0 (
+ hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++
+ (if not (List.is_empty rl) then spc () else mt ()) ++
+ hov 0 (
+ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+ str "=>" ++ brk (1,4) ++ pr t))
+ | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
+
+ let pr_funvar = function
+ | None -> spc () ++ str "_"
+ | Some id -> spc () ++ pr_id id
+
+ let pr_let_clause k pr (id,(bl,t)) =
+ hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
+ str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t)))
+
+ let pr_let_clauses recflag pr = function
+ | hd::tl ->
+ hv 0
+ (pr_let_clause (if recflag then "let rec" else "let") pr hd ++
+ prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl)
+ | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
+
+ let pr_seq_body pr tl =
+ hv 0 (str "[ " ++
+ prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+ str " ]")
+
+ let pr_dispatch pr tl =
+ hv 0 (str "[>" ++
+ prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+ str " ]")
+
+ let pr_opt_tactic pr = function
+ | TacId [] -> mt ()
+ | t -> pr t
+
+ let pr_tac_extend_gen pr tf tm tl =
+ prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
+ pr_opt_tactic pr tm ++ str ".." ++
+ prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl
+
+ let pr_then_gen pr tf tm tl =
+ hv 0 (str "[ " ++
+ pr_tac_extend_gen pr tf tm tl ++
+ str " ]")
+
+ let pr_tac_extend pr tf tm tl =
+ hv 0 (str "[>" ++
+ pr_tac_extend_gen pr tf tm tl ++
+ str " ]")
+
+ let pr_hintbases = function
+ | None -> keyword "with" ++ str" *"
+ | Some [] -> mt ()
+ | Some l -> hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
+
+ let pr_auto_using prc = function
+ | [] -> mt ()
+ | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
+
+ let pr_then () = str ";"
+
+ let ltop = (5,E)
+ let lseq = 4
+ let ltactical = 3
+ let lorelse = 2
+ let llet = 5
+ let lfun = 5
+ let lcomplete = 1
+ let labstract = 3
+ let lmatch = 1
+ let latom = 0
+ let lcall = 1
+ let leval = 1
+ let ltatom = 1
+ let linfo = 5
+
+ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
+
+ (** A printer for tactics that polymorphically works on the three
+ "raw", "glob" and "typed" levels *)
+
+ type 'a printer = {
+ pr_tactic : tolerability -> 'tacexpr -> std_ppcmds;
+ pr_constr : 'trm -> std_ppcmds;
+ pr_lconstr : 'trm -> std_ppcmds;
+ pr_dconstr : 'dtrm -> std_ppcmds;
+ pr_pattern : 'pat -> std_ppcmds;
+ pr_lpattern : 'pat -> std_ppcmds;
+ pr_constant : 'cst -> std_ppcmds;
+ pr_reference : 'ref -> std_ppcmds;
+ pr_name : 'nam -> std_ppcmds;
+ pr_generic : 'lev generic_argument -> std_ppcmds;
+ pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
+ pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
+ }
+
+ constraint 'a = <
+ term :'trm;
+ dterm :'dtrm;
+ pattern :'pat;
+ constant :'cst;
+ reference :'ref;
+ name :'nam;
+ tacexpr :'tacexpr;
+ level :'lev
+ >
+
+ let pr_atom pr strip_prod_binders tag_atom =
+ let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+ let pr_with_bindings_arg_full = pr_with_bindings_arg in
+ let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
+ let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+
+ let _pr_constrarg c = spc () ++ pr.pr_constr c in
+ let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+ let pr_intarg n = spc () ++ int n in
+
+ (* Some printing combinators *)
+ let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
+
+ let pr_binder_fix (nal,t) =
+ (* match t with
+ | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
+ | _ ->*)
+ let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+ spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+ let pr_fix_tac (id,n,c) =
+ let rec set_nth_name avoid n = function
+ (nal,ty)::bll ->
+ if n <= List.length nal then
+ match List.chop (n-1) nal with
+ _, (_,Name id) :: _ -> id, (nal,ty)::bll
+ | bef, (loc,Anonymous) :: aft ->
+ let id = next_ident_away (Id.of_string"y") avoid in
+ id, ((bef@(loc,Name id)::aft, ty)::bll)
+ | _ -> assert false
+ else
+ let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+ (id,(nal,ty)::bll')
+ | [] -> assert false in
+ let (bll,ty) = strip_prod_binders n c in
+ let names =
+ List.fold_left
+ (fun ln (nal,_) -> List.fold_left
+ (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+ ln nal)
+ [] bll in
+ let idarg,bll = set_nth_name names n bll in
+ let annot = match names with
+ | [_] ->
+ mt ()
+ | _ ->
+ spc() ++ str"{"
+ ++ keyword "struct" ++ spc ()
+ ++ pr_id idarg ++ str"}"
+ in
+ hov 1 (str"(" ++ pr_id id ++
+ prlist pr_binder_fix bll ++ annot ++ str" :" ++
+ pr_lconstrarg ty ++ str")") in
+ (* spc() ++
+ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg
+ c)
+ *)
+ let pr_cofix_tac (id,c) =
+ hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
+
+ (* Printing tactics as arguments *)
+ let rec pr_atom0 a = tag_atom a (match a with
+ | TacIntroPattern (false,[]) -> primitive "intros"
+ | TacIntroPattern (true,[]) -> primitive "eintros"
+ | t -> str "(" ++ pr_atom1 t ++ str ")"
+ )
+
+ (* Main tactic printer *)
+ and pr_atom1 a = tag_atom a (match a with
+ (* Basic tactics *)
+ | TacIntroPattern (ev,[]) as t ->
+ pr_atom0 t
+ | TacIntroPattern (ev,(_::_ as p)) ->
+ hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++
+ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
+ | TacApply (a,ev,cb,inhyp) ->
+ hov 1 (
+ (if a then mt() else primitive "simple ") ++
+ primitive (with_evars ev "apply") ++ spc () ++
+ prlist_with_sep pr_comma pr_with_bindings_arg cb ++
+ pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp
+ )
+ | TacElim (ev,cb,cbo) ->
+ hov 1 (
+ primitive (with_evars ev "elim")
+ ++ pr_arg pr_with_bindings_arg cb
+ ++ pr_opt pr_eliminator cbo)
+ | TacCase (ev,cb) ->
+ hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
+ | TacMutualFix (id,n,l) ->
+ hov 1 (
+ primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
+ ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
+ | TacMutualCofix (id,l) ->
+ hov 1 (
+ primitive "cofix" ++ spc () ++ pr_id id ++ spc()
+ ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
+ )
+ | TacAssert (b,Some tac,ipat,c) ->
+ hov 1 (
+ primitive (if b then "assert" else "enough") ++
+ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
+ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
+ )
+ | TacAssert (_,None,ipat,c) ->
+ hov 1 (
+ primitive "pose proof"
+ ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
+ )
+ | TacGeneralize l ->
+ hov 1 (
+ primitive "generalize" ++ spc ()
+ ++ prlist_with_sep pr_comma (fun (cl,na) ->
+ pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
+ l
+ )
+ | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
+ hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+ | TacLetTac (na,c,cl,b,e) ->
+ hov 1 (
+ (if b then primitive "set" else primitive "remember") ++
+ (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
+ else pr_pose_as_style pr.pr_constr na c) ++
+ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
+ pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl)
+ (* | TacInstantiate (n,c,ConclLocation ()) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg c ++ str ")" ))
+ | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg c ++ str ")" )
+ ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
+ *)
+
+ (* Derived basic tactics *)
+ | TacInductionDestruct (isrec,ev,(l,el)) ->
+ hov 1 (
+ primitive (with_evars ev (if isrec then "induction" else "destruct"))
+ ++ spc ()
+ ++ prlist_with_sep pr_comma (fun (h,ids,cl) ->
+ pr_destruction_arg pr.pr_dconstr pr.pr_dconstr h ++
+ pr_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++
+ pr_opt (pr_clauses None pr.pr_name) cl) l ++
+ pr_opt pr_eliminator el
+ )
+
+ (* Conversion *)
+ | TacReduce (r,h) ->
+ hov 1 (
+ pr_red_expr r
+ ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+ )
+ | TacChange (op,c,h) ->
+ hov 1 (
+ primitive "change" ++ brk (1,1)
+ ++ (
+ match op with
+ None ->
+ mt ()
+ | Some p ->
+ pr.pr_pattern p ++ spc ()
+ ++ keyword "with" ++ spc ()
+ ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+ )
+
+ (* Equality and inversion *)
+ | TacRewrite (ev,l,cl,tac) ->
+ hov 1 (
+ primitive (with_evars ev "rewrite") ++ spc ()
+ ++ prlist_with_sep
+ (fun () -> str ","++spc())
+ (fun (b,m,c) ->
+ pr_orient b ++ pr_multi m ++
+ pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
+ l
+ ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
+ ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
+ )
+ | TacInversion (DepInversion (k,c,ids),hyp) ->
+ hov 1 (
+ primitive "dependent " ++ pr_inversion_kind k ++ spc ()
+ ++ pr_quantified_hypothesis hyp
+ ++ pr_with_inversion_names pr.pr_dconstr ids
+ ++ pr_with_constr pr.pr_constr c
+ )
+ | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+ hov 1 (
+ pr_inversion_kind k ++ spc ()
+ ++ pr_quantified_hypothesis hyp
+ ++ pr_non_empty_arg (pr_with_inversion_names pr.pr_dconstr) ids
+ ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+ )
+ | TacInversion (InversionUsing (c,cl),hyp) ->
+ hov 1 (
+ primitive "inversion" ++ spc()
+ ++ pr_quantified_hypothesis hyp ++ spc ()
+ ++ keyword "using" ++ spc () ++ pr.pr_constr c
+ ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+ )
+ )
+ in
+ pr_atom1
+
+ let make_pr_tac pr strip_prod_binders tag_atom tag =
+
+ let extract_binders = function
+ | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+ | body -> ([],body) in
+ let rec pr_tac inherited tac =
+ let return (doc, l) = (tag tac doc, l) in
+ let (strm, prec) = return (match tac with
+ | TacAbstract (t,None) ->
+ keyword "abstract " ++ pr_tac (labstract,L) t, labstract
+ | TacAbstract (t,Some s) ->
+ hov 0 (
+ keyword "abstract"
+ ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc ()
+ ++ keyword "using" ++ spc () ++ pr_id s),
+ labstract
+ | TacLetIn (recflag,llc,u) ->
+ let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
+ v 0
+ (hv 0 (
+ pr_let_clauses recflag (pr_tac ltop) llc
+ ++ spc () ++ keyword "in"
+ ) ++ fnl () ++ pr_tac (llet,E) u),
+ llet
+ | TacMatch (lz,t,lrul) ->
+ hov 0 (
+ pr_lazy lz ++ keyword "match" ++ spc ()
+ ++ pr_tac ltop t ++ spc () ++ keyword "with"
+ ++ prlist (fun r ->
+ fnl () ++ str "| "
+ ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r
+ ) lrul
+ ++ fnl() ++ keyword "end"),
+ lmatch
+ | TacMatchGoal (lz,lr,lrul) ->
+ hov 0 (
+ pr_lazy lz
+ ++ keyword (if lr then "match reverse goal with" else "match goal with")
+ ++ prlist (fun r ->
+ fnl () ++ str "| "
+ ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r
+ ) lrul ++ fnl() ++ keyword "end"),
+ lmatch
+ | TacFun (lvar,body) ->
+ hov 2 (
+ keyword "fun"
+ ++ prlist pr_funvar lvar ++ str " =>" ++ spc ()
+ ++ pr_tac (lfun,E) body),
+ lfun
+ | TacThens (t,tl) ->
+ hov 1 (
+ pr_tac (lseq,E) t ++ pr_then () ++ spc ()
+ ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl),
+ lseq
+ | TacThen (t1,t2) ->
+ hov 1 (
+ pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
+ ++ pr_tac (lseq,L) t2),
+ lseq
+ | TacDispatch tl ->
+ pr_dispatch (pr_tac ltop) tl, lseq
+ | TacExtendTac (tf,t,tr) ->
+ pr_tac_extend (pr_tac ltop) tf t tr , lseq
+ | TacThens3parts (t1,tf,t2,tl) ->
+ hov 1 (
+ pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
+ ++ pr_then_gen (pr_tac ltop) tf t2 tl),
+ lseq
+ | TacTry t ->
+ hov 1 (
+ keyword "try" ++ spc () ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacDo (n,t) ->
+ hov 1 (
+ str "do" ++ spc ()
+ ++ pr_or_var int n ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacTimeout (n,t) ->
+ hov 1 (
+ keyword "timeout "
+ ++ pr_or_var int n ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacTime (s,t) ->
+ hov 1 (
+ keyword "time"
+ ++ pr_opt str s ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacRepeat t ->
+ hov 1 (
+ keyword "repeat" ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacProgress t ->
+ hov 1 (
+ keyword "progress" ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacShowHyps t ->
+ hov 1 (
+ keyword "infoH" ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacInfo t ->
+ hov 1 (
+ keyword "info" ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ linfo
+ | TacOr (t1,t2) ->
+ hov 1 (
+ pr_tac (lorelse,L) t1 ++ spc ()
+ ++ str "+" ++ brk (1,1)
+ ++ pr_tac (lorelse,E) t2),
+ lorelse
+ | TacOnce t ->
+ hov 1 (
+ keyword "once" ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacExactlyOnce t ->
+ hov 1 (
+ keyword "exactly_once" ++ spc ()
+ ++ pr_tac (ltactical,E) t),
+ ltactical
+ | TacIfThenCatch (t,tt,te) ->
+ hov 1 (
+ str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++
+ str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++
+ str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)),
+ ltactical
+ | TacOrelse (t1,t2) ->
+ hov 1 (
+ pr_tac (lorelse,L) t1 ++ spc ()
+ ++ str "||" ++ brk (1,1)
+ ++ pr_tac (lorelse,E) t2),
+ lorelse
+ | TacFail (g,n,l) ->
+ let arg =
+ match n with
+ | ArgArg 0 -> mt ()
+ | _ -> pr_arg (pr_or_var int) n
+ in
+ let name =
+ match g with
+ | TacGlobal -> keyword "gfail"
+ | TacLocal -> keyword "fail"
+ in
+ hov 1 (
+ name ++ arg
+ ++ prlist (pr_arg (pr_message_token pr.pr_name)) l),
+ latom
+ | TacFirst tl ->
+ keyword "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+ | TacSolve tl ->
+ keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+ | TacComplete t ->
+ pr_tac (lcomplete,E) t, lcomplete
+ | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom
+ | TacId l ->
+ keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
+ | TacAtom (loc,t) ->
+ pr_with_comments loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
+ | TacArg(_,Tacexp e) ->
+ pr.pr_tactic (latom,E) e, latom
+ | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
+ keyword "constr:" ++ pr.pr_constr c, latom
+ | TacArg(_,ConstrMayEval c) ->
+ pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
+ | TacArg(_,TacFreshId l) ->
+ primitive "fresh" ++ pr_fresh_ids l, latom
+ | TacArg(_,TacGeneric arg) ->
+ pr.pr_generic arg, latom
+ | TacArg(_,TacCall(loc,f,[])) ->
+ pr.pr_reference f, latom
+ | TacArg(_,TacCall(loc,f,l)) ->
+ pr_with_comments loc (hov 1 (
+ pr.pr_reference f ++ spc ()
+ ++ prlist_with_sep spc pr_tacarg l)),
+ lcall
+ | TacArg (_,a) ->
+ pr_tacarg a, latom
+ | TacML (loc,s,l) ->
+ pr_with_comments loc (pr.pr_extend 1 s l), lcall
+ | TacAlias (loc,kn,l) ->
+ pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom
+ )
+ in
+ if prec_less prec inherited then strm
+ else str"(" ++ strm ++ str")"
+
+ and pr_tacarg = function
+ | Reference r ->
+ pr.pr_reference r
+ | ConstrMayEval c ->
+ pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
+ | TacFreshId l ->
+ keyword "fresh" ++ pr_fresh_ids l
+ | TacPretype c ->
+ keyword "type_term" ++ pr.pr_constr c
+ | TacNumgoals ->
+ keyword "numgoals"
+ | (TacCall _|Tacexp _ | TacGeneric _) as a ->
+ keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+
+ in pr_tac
+
+ let strip_prod_binders_glob_constr n (ty,_) =
+ let rec strip_ty acc n ty =
+ if Int.equal n 0 then (List.rev acc, (ty,None)) else
+ match ty with
+ Glob_term.GProd(loc,na,Explicit,a,b) ->
+ strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
+ | _ -> error "Cannot translate fix tactic: not enough products" in
+ strip_ty [] n ty
+
+ let raw_printers =
+ (strip_prod_binders_expr)
+
+ let rec pr_raw_tactic_level n (t:raw_tactic_expr) =
+ let pr = {
+ pr_tactic = pr_raw_tactic_level;
+ pr_constr = pr_constr_expr;
+ pr_dconstr = pr_constr_expr;
+ pr_lconstr = pr_lconstr_expr;
+ pr_pattern = pr_constr_pattern_expr;
+ pr_lpattern = pr_lconstr_pattern_expr;
+ pr_constant = pr_or_by_notation pr_reference;
+ pr_reference = pr_reference;
+ pr_name = pr_lident;
+ pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
+ pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+ pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+ } in
+ make_pr_tac
+ pr raw_printers
+ tag_raw_atomic_tactic_expr tag_raw_tactic_expr
+ n t
+
+ let pr_raw_tactic = pr_raw_tactic_level ltop
+
+ let pr_and_constr_expr pr (c,_) = pr c
+
+ let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c
+
+ let pr_glob_tactic_level env n t =
+ let glob_printers =
+ (strip_prod_binders_glob_constr)
+ in
+ let rec prtac n (t:glob_tactic_expr) =
+ let pr = {
+ pr_tactic = prtac;
+ pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
+ pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
+ pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
+ pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
+ pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+ pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
+ pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
+ pr_name = pr_lident;
+ pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg);
+ pr_extend = pr_glob_extend_rec
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+ pr_alias = pr_glob_alias
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+ } in
+ make_pr_tac
+ pr glob_printers
+ tag_glob_atomic_tactic_expr tag_glob_tactic_expr
+ n t
+ in
+ prtac n t
+
+ let pr_glob_tactic env = pr_glob_tactic_level env ltop
+
+ let strip_prod_binders_constr n ty =
+ let rec strip_ty acc n ty =
+ if n=0 then (List.rev acc, ty) else
+ match Term.kind_of_term ty with
+ Term.Prod(na,a,b) ->
+ strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
+ | _ -> error "Cannot translate fix tactic: not enough products" in
+ strip_ty [] n ty
+
+ let pr_atomic_tactic_level env n t =
+ let prtac n (t:atomic_tactic_expr) =
+ let pr = {
+ pr_tactic = (fun _ _ -> str "<tactic>");
+ pr_constr = pr_constr_env env Evd.empty;
+ pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
+ pr_lconstr = pr_lconstr_env env Evd.empty;
+ pr_pattern = pr_constr_pattern_env env Evd.empty;
+ pr_lpattern = pr_lconstr_pattern_env env Evd.empty;
+ pr_constant = pr_evaluable_reference_env env;
+ pr_reference = pr_located pr_ltac_constant;
+ pr_name = pr_id;
+ (** Those are not used by the atomic printer *)
+ pr_generic = (fun _ -> assert false);
+ pr_extend = (fun _ _ _ -> assert false);
+ pr_alias = (fun _ _ _ -> assert false);
+ }
+ in
+ pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
+ in
+ prtac n t
+
+ let pr_raw_generic = Pputils.pr_raw_generic
+
+ let pr_glb_generic = Pputils.pr_glb_generic
+
+ let pr_raw_extend env = pr_raw_extend_rec
+ pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+
+ let pr_glob_extend env = pr_glob_extend_rec
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+ let pr_alias pr lev key args =
+ pr_alias_gen (fun _ arg -> pr arg) lev key args
+
+ let pr_extend pr lev ml args =
+ pr_extend_gen pr lev ml args
+
+ let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
+
+end
+
+module Tag =
+struct
+ let keyword =
+ let style = Terminal.make ~bold:true () in
+ Ppstyle.make ~style ["tactic"; "keyword"]
+
+ let primitive =
+ let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
+ Ppstyle.make ~style ["tactic"; "primitive"]
+
+ let string =
+ let style = Terminal.make ~fg_color:`LIGHT_RED () in
+ Ppstyle.make ~style ["tactic"; "string"]
+
+end
+
+include Make (Ppconstr) (struct
+ let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
+ let do_not_tag _ x = x
+ let tag_keyword = tag Tag.keyword
+ let tag_primitive = tag Tag.primitive
+ let tag_string = tag Tag.string
+ let tag_glob_tactic_expr = do_not_tag
+ let tag_glob_atomic_tactic_expr = do_not_tag
+ let tag_raw_tactic_expr = do_not_tag
+ let tag_raw_atomic_tactic_expr = do_not_tag
+ let tag_atomic_tactic_expr = do_not_tag
+end)
+
+let declare_extra_genarg_pprule wit
+ (f : 'a raw_extra_genarg_printer)
+ (g : 'b glob_extra_genarg_printer)
+ (h : 'c extra_genarg_printer) =
+ let s = match wit with
+ | ExtraArg s -> ArgT.repr s
+ | _ -> error
+ "Can declare a pretty-printing rule only for extra argument types."
+ in
+ let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
+ let g x =
+ let env = Global.env () in
+ g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x
+ in
+ let h x =
+ let env = Global.env () in
+ h (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
+ in
+ Genprint.register_print0 wit f g h
+
+(** Registering *)
+
+let run_delayed c =
+ Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
+
+let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
+ | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (fst (run_delayed g))
+ | clear_flag,ElimOnAnonHyp n as x -> x
+ | clear_flag,ElimOnIdent id as x -> x
+
+let () =
+ let pr_bool b = if b then str "true" else str "false" in
+ let pr_unit _ = str "()" in
+ let pr_string s = str "\"" ++ str s ++ str "\"" in
+ Genprint.register_print0 wit_int_or_var
+ (pr_or_var int) (pr_or_var int) int;
+ Genprint.register_print0 wit_ref
+ pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+ Genprint.register_print0 wit_ident
+ pr_id pr_id pr_id;
+ Genprint.register_print0 wit_var
+ (pr_located pr_id) (pr_located pr_id) pr_id;
+ Genprint.register_print0
+ wit_intro_pattern
+ (Miscprint.pr_intro_pattern pr_constr_expr)
+ (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
+ (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
+ Genprint.register_print0
+ wit_clause_dft_concl
+ (pr_clauses (Some true) pr_lident)
+ (pr_clauses (Some true) pr_lident)
+ (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
+ ;
+ Genprint.register_print0
+ wit_constr
+ Ppconstr.pr_constr_expr
+ (fun (c, _) -> Printer.pr_glob_constr c)
+ Printer.pr_constr
+ ;
+ Genprint.register_print0
+ wit_uconstr
+ Ppconstr.pr_constr_expr
+ (fun (c,_) -> Printer.pr_glob_constr c)
+ Printer.pr_closed_glob
+ ;
+ Genprint.register_print0
+ wit_open_constr
+ Ppconstr.pr_constr_expr
+ (fun (c, _) -> Printer.pr_glob_constr c)
+ Printer.pr_constr
+ ;
+ Genprint.register_print0 wit_red_expr
+ (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
+ (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
+ (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
+ Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+ Genprint.register_print0 wit_bindings
+ (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
+ (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
+ Genprint.register_print0 wit_constr_with_bindings
+ (pr_with_bindings pr_constr_expr pr_lconstr_expr)
+ (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
+ Genprint.register_print0 Tacarg.wit_destruction_arg
+ (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
+ (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg it));
+ Genprint.register_print0 Stdarg.wit_int int int int;
+ Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
+ Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
+ Genprint.register_print0 Stdarg.wit_pre_ident str str str;
+ Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string
+
+let () =
+ let printer _ _ prtac = prtac (0, E) in
+ declare_extra_genarg_pprule wit_tactic printer printer printer
+
+let () =
+ let pr_unit _ _ _ () = str "()" in
+ let printer _ _ prtac = prtac (0, E) in
+ declare_extra_genarg_pprule wit_ltac printer printer pr_unit
+
+module Richpp = struct
+
+ include Make (Ppconstr.Richpp) (struct
+ open Ppannotation
+ open Genarg
+ let do_not_tag _ x = x
+ let tag e s = Pp.tag (Pp.Tag.inj e tag) s
+ let tag_keyword = tag AKeyword
+ let tag_primitive = tag AKeyword
+ let tag_string = do_not_tag ()
+ let tag_glob_tactic_expr e = tag (AGlbGenArg (in_gen (glbwit wit_ltac) e))
+ let tag_glob_atomic_tactic_expr = do_not_tag
+ let tag_raw_tactic_expr e = tag (ARawGenArg (in_gen (rawwit wit_ltac) e))
+ let tag_raw_atomic_tactic_expr = do_not_tag
+ let tag_atomic_tactic_expr = do_not_tag
+ end)
+
+end
diff --git a/ltac/pptactic.mli b/ltac/pptactic.mli
new file mode 100644
index 000000000..86e3ea548
--- /dev/null
+++ b/ltac/pptactic.mli
@@ -0,0 +1,67 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This module implements pretty-printers for tactic_expr syntactic
+ objects and their subcomponents. *)
+
+open Pp
+open Genarg
+open Geninterp
+open Names
+open Constrexpr
+open Tacexpr
+open Ppextend
+
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
+
+type 'a raw_extra_genarg_printer =
+ (constr_expr -> std_ppcmds) ->
+ (constr_expr -> std_ppcmds) ->
+ (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+ 'a -> std_ppcmds
+
+type 'a glob_extra_genarg_printer =
+ (glob_constr_and_expr -> std_ppcmds) ->
+ (glob_constr_and_expr -> std_ppcmds) ->
+ (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ 'a -> std_ppcmds
+
+type 'a extra_genarg_printer =
+ (Term.constr -> std_ppcmds) ->
+ (Term.constr -> std_ppcmds) ->
+ (tolerability -> Val.t -> std_ppcmds) ->
+ 'a -> std_ppcmds
+
+val declare_extra_genarg_pprule :
+ ('a, 'b, 'c) genarg_type ->
+ 'a raw_extra_genarg_printer ->
+ 'b glob_extra_genarg_printer ->
+ 'c extra_genarg_printer -> unit
+
+type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
+
+type pp_tactic = {
+ pptac_level : int;
+ pptac_prods : grammar_terminals;
+}
+
+val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
+
+(** The default pretty-printers produce {!Pp.std_ppcmds} that are
+ interpreted as raw strings. *)
+include Pptacticsig.Pp
+
+(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
+ interpreted as annotated strings. The annotations can be
+ retrieved using {!RichPp.rich_pp}. Their definitions are
+ located in {!Ppannotation.t}. *)
+module Richpp : Pptacticsig.Pp
+
+val ltop : tolerability
diff --git a/ltac/pptacticsig.mli b/ltac/pptacticsig.mli
new file mode 100644
index 000000000..74ddd377a
--- /dev/null
+++ b/ltac/pptacticsig.mli
@@ -0,0 +1,81 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Genarg
+open Geninterp
+open Tacexpr
+open Ppextend
+open Environ
+open Misctypes
+
+module type Pp = sig
+
+ val pr_with_occurrences :
+ ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
+ val pr_red_expr :
+ ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+ ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
+ val pr_may_eval :
+ ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+ ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
+
+ val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
+
+ val pr_in_clause :
+ ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+ val pr_clauses : bool option ->
+ ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+ val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+ val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+ val pr_raw_extend: env -> int ->
+ ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+
+ val pr_glob_extend: env -> int ->
+ ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
+
+ val pr_extend :
+ (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+
+ val pr_alias_key : Names.KerName.t -> std_ppcmds
+
+ val pr_alias : (Val.t -> std_ppcmds) ->
+ int -> Names.KerName.t -> Val.t list -> std_ppcmds
+
+ val pr_alias_key : Names.KerName.t -> std_ppcmds
+
+ val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+
+ val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
+
+ val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
+
+ val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
+
+ val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
+
+ val pr_hintbases : string list option -> std_ppcmds
+
+ val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
+
+ val pr_bindings :
+ ('constr -> std_ppcmds) ->
+ ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
+
+ val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+ val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+ ('b, 'a) match_rule -> std_ppcmds
+
+ val pr_value : tolerability -> Val.t -> std_ppcmds
+
+end
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 69f45e1ae..a332e2871 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -36,6 +36,9 @@ open Sigma.Notations
open Proofview.Notations
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+module RelDecl = Context.Rel.Declaration
+
(** Typeclass-based generalized rewriting. *)
(** Constants used by the tactic. *)
@@ -1499,7 +1502,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
Evar.Set.fold
(fun ev acc ->
if not (Evd.is_defined acc ev) then
- errorlabstrm "rewrite"
+ user_err ~hdr:"rewrite"
(str "Unsolved constraint remaining: " ++ spc () ++
Evd.pr_evar_info (Evd.find acc ev))
else Evd.remove acc ev)
@@ -1527,7 +1530,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
let rec insert_dependent env decl accu hyps = match hyps with
| [] -> List.rev_append accu [decl]
| ndecl :: rem ->
- if occur_var_in_decl env (get_id ndecl) decl then
+ if occur_var_in_decl env (NamedDecl.get_id ndecl) decl then
List.rev_append accu (decl :: hyps)
else
insert_dependent env decl (ndecl :: accu) rem
@@ -1537,17 +1540,17 @@ let assert_replacing id newt tac =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let ctx = Environ.named_context env in
- let after, before = List.split_when (Id.equal id % get_id) ctx in
+ let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in
let nc = match before with
| [] -> assert false
- | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem
+ | d :: rem -> insert_dependent env (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem
in
let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
Refine.refine ~unsafe:false { run = begin fun sigma ->
let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
let map d =
- let n = get_id d in
+ let n = NamedDecl.get_id d in
if Id.equal n id then ev' else mkVar n
in
let (e, _) = destEvar ev in
@@ -2087,9 +2090,8 @@ let setoid_proof ty fn fallback =
begin
try
let rel, _, _ = decompose_app_rel env sigma concl in
- let open Context.Rel.Declaration in
let (sigma, t) = Typing.type_of env sigma rel in
- let car = get_type (List.hd (fst (Reduction.dest_prod env t))) in
+ let car = RelDecl.get_type (List.hd (fst (Reduction.dest_prod env t))) in
(try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
with e -> Proofview.tclZERO e
diff --git a/ltac/tacarg.ml b/ltac/tacarg.ml
new file mode 100644
index 000000000..42552c484
--- /dev/null
+++ b/ltac/tacarg.ml
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Generic arguments based on Ltac. *)
+
+open Genarg
+open Geninterp
+open Tacexpr
+
+let make0 ?dyn name =
+ let wit = Genarg.make0 name in
+ let () = Geninterp.register_val0 wit dyn in
+ wit
+
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
+ make0 "tactic"
+
+let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
+
+let wit_destruction_arg =
+ make0 "destruction_arg"
diff --git a/ltac/tacarg.mli b/ltac/tacarg.mli
new file mode 100644
index 000000000..bfa423db2
--- /dev/null
+++ b/ltac/tacarg.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Genarg
+open Tacexpr
+open Constrexpr
+open Misctypes
+
+(** Generic arguments based on Ltac. *)
+
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
+
+(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
+ toplevel interpretation. The one of [wit_ltac] forces the tactic and
+ discards the result. *)
+val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
+
+val wit_destruction_arg :
+ (constr_expr with_bindings Tacexpr.destruction_arg,
+ glob_constr_and_expr with_bindings Tacexpr.destruction_arg,
+ delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type
+
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
index b0a80ef73..df38a42cb 100644
--- a/ltac/taccoerce.ml
+++ b/ltac/taccoerce.ml
@@ -13,7 +13,6 @@ open Pattern
open Misctypes
open Genarg
open Stdarg
-open Constrarg
open Geninterp
exception CannotCoerceTo of string
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 673ac832a..2e2b55be7 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -43,8 +43,8 @@ let coincide s pat off =
!break
let atactic n =
- if n = 5 then Aentry Tactic.binder_tactic
- else Aentryl (Tactic.tactic_expr, n)
+ if n = 5 then Aentry Pltac.binder_tactic
+ else Aentryl (Pltac.tactic_expr, n)
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
@@ -56,9 +56,9 @@ let get_tacentry n m =
&& not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
&& not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
in
- if check_lvl n then EntryName (rawwit Constrarg.wit_tactic, Aself)
- else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext)
- else EntryName (rawwit Constrarg.wit_tactic, atactic n)
+ if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
+ else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+ else EntryName (rawwit Tacarg.wit_tactic, atactic n)
let get_separator = function
| None -> error "Missing separator."
@@ -108,11 +108,11 @@ let interp_entry_name interp symb =
let get_tactic_entry n =
if Int.equal n 0 then
- Tactic.simple_tactic, None
+ Pltac.simple_tactic, None
else if Int.equal n 5 then
- Tactic.binder_tactic, None
+ Pltac.binder_tactic, None
else if 1<=n && n<5 then
- Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
+ Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
else
error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
@@ -163,7 +163,7 @@ let add_tactic_entry (kn, ml, tg) state =
let mkact loc l =
let map arg =
(** HACK to handle especially the tactic(...) entry *)
- let wit = Genarg.rawwit Constrarg.wit_tactic in
+ let wit = Genarg.rawwit Tacarg.wit_tactic in
if Genarg.has_type arg wit && not ml then
Tacexp (Genarg.out_gen wit arg)
else
@@ -218,7 +218,7 @@ let interp_prod_item = function
| Some n ->
(** FIXME: do better someday *)
assert (String.equal s "tactic");
- begin match Constrarg.wit_tactic with
+ begin match Tacarg.wit_tactic with
| ExtraArg tag -> ArgT.Any tag
| _ -> assert false
end
@@ -405,7 +405,7 @@ let create_ltac_quotation name cast (e, l) =
in
let action _ v _ _ _ loc = cast (loc, v) in
let gram = (level, assoc, [Rule (rule, action)]) in
- Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
+ Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
(** Command *)
@@ -425,29 +425,29 @@ let warn_unusable_identifier =
let register_ltac local tacl =
let map tactic_body =
match tactic_body with
- | TacticDefinition ((loc,id), body) ->
+ | Tacexpr.TacticDefinition ((loc,id), body) ->
let kn = Lib.make_kn id in
let id_pp = pr_id id in
let () = if is_defined_tac kn then
- CErrors.user_err_loc (loc, "",
- str "There is already an Ltac named " ++ id_pp ++ str".")
+ CErrors.user_err ~loc
+ (str "There is already an Ltac named " ++ id_pp ++ str".")
in
let is_shadowed =
try
- match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
+ match Pcoq.parse_string Pltac.tactic (Id.to_string id) with
| Tacexpr.TacArg _ -> false
| _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
in
let () = if is_shadowed then warn_unusable_identifier id in
NewTac id, body
- | TacticRedefinition (ident, body) ->
+ | Tacexpr.TacticRedefinition (ident, body) ->
let loc = loc_of_reference ident in
let kn =
try Nametab.locate_tactic (snd (qualid_of_reference ident))
with Not_found ->
- CErrors.user_err_loc (loc, "",
- str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+ CErrors.user_err ~loc
+ (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
in
UpdateTac kn, body
in
@@ -511,3 +511,15 @@ let print_ltacs () =
hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
in
Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
+
+(** Grammar *)
+
+let () =
+ let open Metasyntax in
+ let entries = [
+ AnyEntry Pltac.tactic_expr;
+ AnyEntry Pltac.binder_tactic;
+ AnyEntry Pltac.simple_tactic;
+ AnyEntry Pltac.tactic_arg;
+ ] in
+ register_grammar "tactic" entries
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 27df819ee..969c118fb 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -13,7 +13,7 @@ open Tacexpr
(** {5 Tactic Definitions} *)
-val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit
+val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
(** Adds new Ltac definitions to the environment. *)
(** {5 Tactic Notations} *)
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index c709ab114..e3c2b4ad5 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
let () = if Array.length tacs <= i then raise Not_found in
tacs.(i)
with Not_found ->
- CErrors.errorlabstrm ""
+ CErrors.user_err
(str "The tactic " ++ pr_tacname s ++ str " is not installed.")
(***************************************************************************)
diff --git a/ltac/tacexpr.mli b/ltac/tacexpr.mli
new file mode 100644
index 000000000..9c25a1645
--- /dev/null
+++ b/ltac/tacexpr.mli
@@ -0,0 +1,396 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Loc
+open Names
+open Constrexpr
+open Libnames
+open Nametab
+open Genredexpr
+open Genarg
+open Pattern
+open Misctypes
+open Locus
+
+type direction_flag = bool (* true = Left-to-right false = right-to-right *)
+type lazy_flag =
+ | General (* returns all possible successes *)
+ | Select (* returns all successes of the first matching branch *)
+ | Once (* returns the first success in a maching branch
+ (not necessarily the first) *)
+type global_flag = (* [gfail] or [fail] *)
+ | TacGlobal
+ | TacLocal
+type evars_flag = bool (* true = pose evars false = fail on evars *)
+type rec_flag = bool (* true = recursive false = not recursive *)
+type advanced_flag = bool (* true = advanced false = basic *)
+type letin_flag = bool (* true = use local def false = use Leibniz *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
+type goal_selector = Vernacexpr.goal_selector =
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
+type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
+ | ElimOnConstr of 'a
+ | ElimOnIdent of Id.t located
+ | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+ clear_flag * 'a core_destruction_arg
+
+type inversion_kind = Misctypes.inversion_kind =
+ | SimpleInversion
+ | FullInversion
+ | FullInversionClear
+
+type ('c,'d,'id) inversion_strength =
+ | NonDepInversion of
+ inversion_kind * 'id list * 'd or_and_intro_pattern_expr located or_var option
+ | DepInversion of
+ inversion_kind * 'c option * 'd or_and_intro_pattern_expr located or_var option
+ | InversionUsing of 'c * 'id list
+
+type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
+
+type 'id message_token =
+ | MsgString of string
+ | MsgInt of int
+ | MsgIdent of 'id
+
+type ('dconstr,'id) induction_clause =
+ 'dconstr with_bindings destruction_arg *
+ (intro_pattern_naming_expr located option (* eqn:... *)
+ * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *)
+ * 'id clause_expr option (* in ... *)
+
+type ('constr,'dconstr,'id) induction_clause_list =
+ ('dconstr,'id) induction_clause list
+ * 'constr with_bindings option (* using ... *)
+
+type 'a with_bindings_arg = clear_flag * 'a with_bindings
+
+(* Type of patterns *)
+type 'a match_pattern =
+ | Term of 'a
+ | Subterm of bool * Id.t option * 'a
+
+(* Type of hypotheses for a Match Context rule *)
+type 'a match_context_hyps =
+ | Hyp of Name.t located * 'a match_pattern
+ | Def of Name.t located * 'a match_pattern * 'a match_pattern
+
+(* Type of a Match rule for Match Context and Match *)
+type ('a,'t) match_rule =
+ | Pat of 'a match_context_hyps list * 'a match_pattern * 't
+ | All of 't
+
+(** Extension indentifiers for the TACTIC EXTEND mechanism. *)
+type ml_tactic_name = {
+ (** Name of the plugin where the tactic is defined, typically coming from a
+ DECLARE PLUGIN statement in the source. *)
+ mltac_plugin : string;
+ (** Name of the tactic entry where the tactic is defined, typically found
+ after the TACTIC EXTEND statement in the source. *)
+ mltac_tactic : string;
+}
+
+type ml_tactic_entry = {
+ mltac_name : ml_tactic_name;
+ mltac_index : int;
+}
+
+(** Composite types *)
+
+type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+
+type open_constr_expr = unit * constr_expr
+type open_glob_constr = unit * glob_constr_and_expr
+
+type binding_bound_vars = Constr_matching.binding_bound_vars
+type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
+
+type 'a delayed_open = 'a Tactypes.delayed_open =
+ { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
+
+type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
+
+type delayed_open_constr = Term.constr delayed_open
+
+type intro_pattern = delayed_open_constr intro_pattern_expr located
+type intro_patterns = delayed_open_constr intro_pattern_expr located list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
+type intro_pattern_naming = intro_pattern_naming_expr located
+
+(** Generic expressions for atomic tactics *)
+
+type 'a gen_atomic_tactic_expr =
+ (* Basic tactics *)
+ | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr located list
+ | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
+ ('nam * 'dtrm intro_pattern_expr located option) option
+ | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
+ | TacCase of evars_flag * 'trm with_bindings_arg
+ | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
+ | TacMutualCofix of Id.t * (Id.t * 'trm) list
+ | TacAssert of
+ bool * 'tacexpr option option *
+ 'dtrm intro_pattern_expr located option * 'trm
+ | TacGeneralize of ('trm with_occurrences * Name.t) list
+ | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
+ intro_pattern_naming_expr located option
+
+ (* Derived basic tactics *)
+ | TacInductionDestruct of
+ rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
+
+ (* Conversion *)
+ | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
+ | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+
+ (* Equality and inversion *)
+ | TacRewrite of evars_flag *
+ (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+ (* spiwack: using ['dtrm] here is a small hack, may not be
+ stable by a change in the representation of delayed
+ terms. Because, in fact, it is the whole "with_bindings"
+ which is delayed. But because the "t" level for ['dtrm] is
+ uninterpreted, it works fine here too, and avoid more
+ disruption of this file. *)
+ 'tacexpr option
+ | TacInversion of ('trm,'dtrm,'nam) inversion_strength * quantified_hypothesis
+
+constraint 'a = <
+ term:'trm;
+ dterm: 'dtrm;
+ pattern:'pat;
+ constant:'cst;
+ reference:'ref;
+ name:'nam;
+ tacexpr:'tacexpr;
+ level:'lev
+>
+
+(** Possible arguments of a tactic definition *)
+
+type 'a gen_tactic_arg =
+ | TacGeneric of 'lev generic_argument
+ | ConstrMayEval of ('trm,'cst,'pat) may_eval
+ | Reference of 'ref
+ | TacCall of Loc.t * 'ref *
+ 'a gen_tactic_arg list
+ | TacFreshId of string or_var list
+ | Tacexp of 'tacexpr
+ | TacPretype of 'trm
+ | TacNumgoals
+
+constraint 'a = <
+ term:'trm;
+ dterm: 'dtrm;
+ pattern:'pat;
+ constant:'cst;
+ reference:'ref;
+ name:'nam;
+ tacexpr:'tacexpr;
+ level:'lev
+>
+
+(** Generic ltac expressions.
+ 't : terms, 'p : patterns, 'c : constants, 'i : inductive,
+ 'r : ltac refs, 'n : idents, 'l : levels *)
+
+and 'a gen_tactic_expr =
+ | TacAtom of Loc.t * 'a gen_atomic_tactic_expr
+ | TacThen of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr
+ | TacDispatch of
+ 'a gen_tactic_expr list
+ | TacExtendTac of
+ 'a gen_tactic_expr array *
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr array
+ | TacThens of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr list
+ | TacThens3parts of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr array *
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr array
+ | TacFirst of 'a gen_tactic_expr list
+ | TacComplete of 'a gen_tactic_expr
+ | TacSolve of 'a gen_tactic_expr list
+ | TacTry of 'a gen_tactic_expr
+ | TacOr of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr
+ | TacOnce of
+ 'a gen_tactic_expr
+ | TacExactlyOnce of
+ 'a gen_tactic_expr
+ | TacIfThenCatch of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr
+ | TacOrelse of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr
+ | TacDo of int or_var * 'a gen_tactic_expr
+ | TacTimeout of int or_var * 'a gen_tactic_expr
+ | TacTime of string option * 'a gen_tactic_expr
+ | TacRepeat of 'a gen_tactic_expr
+ | TacProgress of 'a gen_tactic_expr
+ | TacShowHyps of 'a gen_tactic_expr
+ | TacAbstract of
+ 'a gen_tactic_expr * Id.t option
+ | TacId of 'n message_token list
+ | TacFail of global_flag * int or_var * 'n message_token list
+ | TacInfo of 'a gen_tactic_expr
+ | TacLetIn of rec_flag *
+ (Id.t located * 'a gen_tactic_arg) list *
+ 'a gen_tactic_expr
+ | TacMatch of lazy_flag *
+ 'a gen_tactic_expr *
+ ('p,'a gen_tactic_expr) match_rule list
+ | TacMatchGoal of lazy_flag * direction_flag *
+ ('p,'a gen_tactic_expr) match_rule list
+ | TacFun of 'a gen_tactic_fun_ast
+ | TacArg of 'a gen_tactic_arg located
+ | TacSelect of goal_selector * 'a gen_tactic_expr
+ (* For ML extensions *)
+ | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
+ (* For syntax extensions *)
+ | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list
+
+constraint 'a = <
+ term:'t;
+ dterm: 'dtrm;
+ pattern:'p;
+ constant:'c;
+ reference:'r;
+ name:'n;
+ tacexpr:'tacexpr;
+ level:'l
+>
+
+and 'a gen_tactic_fun_ast =
+ Id.t option list * 'a gen_tactic_expr
+
+constraint 'a = <
+ term:'t;
+ dterm: 'dtrm;
+ pattern:'p;
+ constant:'c;
+ reference:'r;
+ name:'n;
+ tacexpr:'te;
+ level:'l
+>
+
+(** Globalized tactics *)
+
+type g_trm = glob_constr_and_expr
+type g_pat = glob_constr_pattern_and_expr
+type g_cst = evaluable_global_reference and_short_name or_var
+type g_ref = ltac_constant located or_var
+type g_nam = Id.t located
+
+type g_dispatch = <
+ term:g_trm;
+ dterm:g_trm;
+ pattern:g_pat;
+ constant:g_cst;
+ reference:g_ref;
+ name:g_nam;
+ tacexpr:glob_tactic_expr;
+ level:glevel
+>
+
+and glob_tactic_expr =
+ g_dispatch gen_tactic_expr
+
+type glob_atomic_tactic_expr =
+ g_dispatch gen_atomic_tactic_expr
+
+type glob_tactic_arg =
+ g_dispatch gen_tactic_arg
+
+(** Raw tactics *)
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = reference or_by_notation
+type r_ref = reference
+type r_nam = Id.t located
+type r_lev = rlevel
+
+type r_dispatch = <
+ term:r_trm;
+ dterm:r_trm;
+ pattern:r_pat;
+ constant:r_cst;
+ reference:r_ref;
+ name:r_nam;
+ tacexpr:raw_tactic_expr;
+ level:rlevel
+>
+
+and raw_tactic_expr =
+ r_dispatch gen_tactic_expr
+
+type raw_atomic_tactic_expr =
+ r_dispatch gen_atomic_tactic_expr
+
+type raw_tactic_arg =
+ r_dispatch gen_tactic_arg
+
+(** Interpreted tactics *)
+
+type t_trm = Term.constr
+type t_pat = constr_pattern
+type t_cst = evaluable_global_reference
+type t_ref = ltac_constant located
+type t_nam = Id.t
+
+type t_dispatch = <
+ term:t_trm;
+ dterm:g_trm;
+ pattern:t_pat;
+ constant:t_cst;
+ reference:t_ref;
+ name:t_nam;
+ tacexpr:unit;
+ level:tlevel
+>
+
+type atomic_tactic_expr =
+ t_dispatch gen_atomic_tactic_expr
+
+(** Misc *)
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
+type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
+
+(** Traces *)
+
+type ltac_call_kind =
+ | LtacMLCall of glob_tactic_expr
+ | LtacNotationCall of KerName.t
+ | LtacNameCall of ltac_constant
+ | LtacAtomCall of glob_atomic_tactic_expr
+ | LtacVarCall of Id.t * glob_tactic_expr
+ | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
+
+type ltac_trace = (Loc.t * ltac_call_kind) list
+
+type tacdef_body =
+ | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index c5bb0ed07..763e0dc22 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -23,7 +23,8 @@ open Constrexpr
open Termops
open Tacexpr
open Genarg
-open Constrarg
+open Stdarg
+open Tacarg
open Misctypes
open Locus
@@ -32,11 +33,8 @@ open Locus
let dloc = Loc.ghost
-let error_global_not_found_loc (loc,qid) =
- error_global_not_found_loc loc qid
-
-let error_tactic_expected loc =
- user_err_loc (loc,"",str "Tactic expected.")
+let error_tactic_expected ?loc =
+ user_err ?loc (str "Tactic expected.")
(** Generic arguments *)
@@ -85,7 +83,7 @@ let intern_hyp ist (loc,id as locid) =
else if find_ident id ist then
(dloc,id)
else
- Pretype_errors.error_var_not_found_loc loc id
+ Pretype_errors.error_var_not_found ~loc id
let intern_or_var f ist = function
| ArgVar locid -> ArgVar (intern_hyp ist locid)
@@ -99,7 +97,7 @@ let intern_global_reference ist = function
| r ->
let loc,_ as lqid = qualid_of_reference r in
try ArgArg (loc,locate_global_with_alias lqid)
- with Not_found -> error_global_not_found_loc lqid
+ with Not_found -> error_global_not_found (snd lqid)
let intern_ltac_variable ist = function
| Ident (loc,id) ->
@@ -143,7 +141,7 @@ let intern_isolated_tactic_reference strict ist r =
try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
with Not_found ->
(* Reference not found *)
- error_global_not_found_loc (qualid_of_reference r)
+ error_global_not_found (snd (qualid_of_reference r))
(* Internalize an applied tactic reference *)
@@ -159,7 +157,7 @@ let intern_applied_tactic_reference ist r =
try intern_applied_global_tactic_reference r
with Not_found ->
(* Reference not found *)
- error_global_not_found_loc (qualid_of_reference r)
+ error_global_not_found (snd (qualid_of_reference r))
(* Intern a reference parsed in a non-tactic entry *)
@@ -180,7 +178,7 @@ let intern_non_tactic_reference strict ist r =
TacGeneric ipat
| _ ->
(* Reference not found *)
- error_global_not_found_loc (qualid_of_reference r)
+ error_global_not_found (snd (qualid_of_reference r))
let intern_message_token ist = function
| (MsgString _ | MsgInt _ as x) -> x
@@ -291,7 +289,7 @@ let intern_evaluable_global_reference ist r =
with Not_found ->
match r with
| Ident (loc,id) when not !strict_check -> EvalVarRef id
- | _ -> error_global_not_found_loc lqid
+ | _ -> error_global_not_found (snd lqid)
let intern_evaluable_reference_or_by_notation ist = function
| AN r -> intern_evaluable_global_reference ist r
@@ -463,8 +461,8 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
(* Utilities *)
let extract_let_names lrc =
let fold accu ((loc, name), _) =
- if Id.Set.mem name accu then user_err_loc
- (loc, "glob_tactic", str "This variable is bound several times.")
+ if Id.Set.mem name accu then user_err ~loc
+ ~hdr:"glob_tactic" (str "This variable is bound several times.")
else Id.Set.add name accu
in
List.fold_left fold Id.Set.empty lrc
@@ -641,7 +639,7 @@ and intern_tactic_as_arg loc onlytac ist a =
| TacGeneric _ as a -> TacArg (loc,a)
| Tacexp a -> a
| ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
- if onlytac then error_tactic_expected loc else TacArg (loc,a)
+ if onlytac then error_tactic_expected ~loc else TacArg (loc,a)
and intern_tactic_or_tacarg ist = intern_tactic false ist
@@ -751,7 +749,7 @@ let print_ltac id =
++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
with
Not_found ->
- errorlabstrm "print_ltac"
+ user_err ~hdr:"print_ltac"
(pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
(** Registering *)
@@ -778,13 +776,16 @@ let intern_ident' ist id =
let lf = ref Id.Set.empty in
(ist, intern_ident lf ist id)
+let intern_ltac ist tac =
+ Flags.with_option strict_check (fun () -> intern_pure_tactic ist tac) ()
+
let () =
Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_ident intern_ident';
Genintern.register_intern0 wit_var (lift intern_hyp);
Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
- Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg);
+ Genintern.register_intern0 wit_ltac (lift intern_ltac);
Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c));
Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c));
@@ -795,15 +796,17 @@ let () =
Genintern.register_intern0 wit_destruction_arg (lift intern_destruction_arg);
()
-(***************************************************************************)
-(* Backwarding recursive needs of tactic glob/interp/eval functions *)
+(** Substitution for notations containing tactic-in-terms *)
-let _ =
- let f l =
- let ltacvars =
- List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l
- in
- Flags.with_option strict_check
- (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars })
+let notation_subst bindings tac =
+ let fold id c accu =
+ let loc = Glob_ops.loc_of_glob_constr (fst c) in
+ let c = ConstrMayEval (ConstrTerm c) in
+ ((loc, id), c) :: accu
in
- Hook.set Hints.extern_intern_tac f
+ let bindings = Id.Map.fold fold bindings [] in
+ (** This is theoretically not correct due to potential variable capture, but
+ Ltac has no true variables so one cannot simply substitute *)
+ TacLetIn (false, bindings, tac)
+
+let () = Genintern.register_ntn_subst0 wit_tactic notation_subst
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 08e67a0c2..92a403c58 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -31,7 +31,7 @@ open Tacexpr
open Genarg
open Geninterp
open Stdarg
-open Constrarg
+open Tacarg
open Printer
open Pretyping
open Misctypes
@@ -168,7 +168,7 @@ module Value = struct
let pr_v = Pptactic.pr_value Pptactic.ltop v in
let Val.Dyn (tag, _) = v in
let tag = Val.pr tag in
- errorlabstrm "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
+ user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
++ str " while type " ++ Val.pr wit ++ str " was expected.")
let unbox wit v ans = match ans with
@@ -315,8 +315,8 @@ let append_trace trace v =
(* Dynamically check that an argument is a tactic *)
let coerce_to_tactic loc id v =
let v = Value.normalize v in
- let fail () = user_err_loc
- (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
+ let fail () = user_err ~loc
+ (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
in
let v = Value.normalize v in
if has_type v (topwit wit_tacvalue) then
@@ -371,7 +371,7 @@ let debugging_exception_step ist signal_anomaly e pp =
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
let error_ltac_variable loc id env v s =
- user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
+ user_err ~loc (str "Ltac variable " ++ pr_id id ++
strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
strbrk "which cannot be coerced to " ++ str s ++ str".")
@@ -388,8 +388,6 @@ let interp_ident ist env sigma id =
try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id)
with Not_found -> id
-let pf_interp_ident id gl = interp_ident id (pf_env gl) (project gl)
-
(* Interprets an optional identifier, bound or fresh *)
let interp_name ist env sigma = function
| Anonymous -> Anonymous
@@ -406,8 +404,8 @@ let interp_intro_pattern_naming_var loc ist env sigma id =
let interp_int ist locid =
try try_interp_ltac_var coerce_to_int ist None locid
with Not_found ->
- user_err_loc(fst locid,"interp_int",
- str "Unbound variable " ++ pr_id (snd locid) ++ str".")
+ user_err ~loc:(fst locid) ~hdr:"interp_int"
+ (str "Unbound variable " ++ pr_id (snd locid) ++ str".")
let interp_int_or_var ist = function
| ArgVar locid -> interp_int ist locid
@@ -429,7 +427,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
with Not_found ->
(* Then look if bound in the proof context at calling time *)
if is_variable env id then id
- else Loc.raise loc (Logic.RefinerError (Logic.NoSuchHyp id))
+ else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id))
let interp_hyp_list_as_list ist env sigma (loc,id as x) =
try coerce_to_hyp_list env (Id.Map.find id ist.lfun)
@@ -451,7 +449,7 @@ let interp_reference ist env sigma = function
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
- with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
+ with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
let try_interp_evaluable env (loc, id) =
let v = Environ.lookup_named id env in
@@ -467,14 +465,14 @@ let interp_evaluable ist env sigma = function
with Not_found ->
match r with
| EvalConstRef _ -> r
- | _ -> error_global_not_found_loc loc (qualid_of_ident id)
+ | _ -> error_global_not_found ~loc (qualid_of_ident id)
end
| ArgArg (r,None) -> r
| ArgVar (loc, id) ->
try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id)
with Not_found ->
try try_interp_evaluable env (loc, id)
- with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
+ with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -696,9 +694,6 @@ let interp_typed_pattern ist env sigma (_,c,_) =
pattern_of_constr env sigma c
(* Interprets a constr expression *)
-let pf_interp_constr ist gl =
- interp_constr ist (pf_env gl) (project gl)
-
let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
let try_expand_ltac_var sigma x =
try match dest_fun x with
@@ -720,10 +715,6 @@ let interp_constr_list ist env sigma c =
let interp_open_constr_list =
interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_open_constr
-(* Interprets a type expression *)
-let pf_interp_type ist env sigma =
- interp_type ist env sigma
-
(* Interprets a reduction expression *)
let interp_unfold ist env sigma (occs,qid) =
(interp_occurrences ist occs,interp_evaluable ist env sigma qid)
@@ -748,7 +739,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
Inr (pattern_of_constr env sigma c) in
(try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
with Not_found ->
- error_global_not_found_loc loc (qualid_of_ident id))
+ error_global_not_found ~loc (qualid_of_ident id))
| Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (interp_typed_pattern ist env sigma c) in
interp_occurrences ist occs, p
@@ -804,8 +795,8 @@ let interp_may_eval f ist env sigma = function
!evdref , c
with
| Not_found ->
- user_err_loc (loc, "interp_may_eval",
- str "Unbound context identifier" ++ pr_id s ++ str"."))
+ user_err ~loc ~hdr:"interp_may_eval"
+ (str "Unbound context identifier" ++ pr_id s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
Typing.type_of ~refresh:true env sigma c_interp
@@ -1041,8 +1032,8 @@ let interp_destruction_arg ist gl arg =
}
| keep,ElimOnAnonHyp n as x -> x
| keep,ElimOnIdent (loc,id) ->
- let error () = user_err_loc (loc, "",
- strbrk "Cannot coerce " ++ pr_id id ++
+ let error () = user_err ~loc
+ (strbrk "Cannot coerce " ++ pr_id id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
let try_cast_id id' =
@@ -1052,7 +1043,7 @@ let interp_destruction_arg ist gl arg =
(keep, ElimOnConstr { delayed = begin fun env sigma ->
try Sigma.here (constr_of_id env id', NoBindings) sigma
with Not_found ->
- user_err_loc (loc, "interp_destruction_arg",
+ user_err ~loc ~hdr:"interp_destruction_arg" (
pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
end })
in
@@ -1120,7 +1111,7 @@ let read_pattern lfun ist env sigma = function
(* Reads the hypotheses of a Match Context rule *)
let cons_and_check_name id l =
if Id.List.mem id l then
- user_err_loc (dloc,"read_match_goal_hyps",
+ user_err ~hdr:"read_match_goal_hyps" (
str "Hypothesis pattern-matching variable " ++ pr_id id ++
str " used twice in the same pattern.")
else id::l
@@ -1220,7 +1211,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
end
| TacAbstract (tac,ido) ->
Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT
- (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac)
+ (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
end }
| TacThen (t1,t) ->
Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
@@ -1706,7 +1697,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let env = pf_env gl in
let f sigma (id,n,c) =
- let (sigma,c_interp) = pf_interp_type ist env sigma c in
+ let (sigma,c_interp) = interp_type ist env sigma c in
sigma , (interp_ident ist env sigma id,n,c_interp) in
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
@@ -1721,7 +1712,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let env = pf_env gl in
let f sigma (id,c) =
- let (sigma,c_interp) = pf_interp_type ist env sigma c in
+ let (sigma,c_interp) = interp_type ist env sigma c in
sigma , (interp_ident ist env sigma id,c_interp) in
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
@@ -1763,7 +1754,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in
if Locusops.is_nowhere clp then
(* We try to fully-typecheck the term *)
- let (sigma,c_interp) = pf_interp_constr ist gl c in
+ let (sigma,c_interp) = interp_constr ist env sigma c in
let let_tac b na c cl eqpat =
let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
@@ -1876,7 +1867,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let (sigma, c) = interp_constr ist env sigma c in
Sigma.Unsafe.of_pair (c, sigma)
with e when to_catch e (* Hack *) ->
- errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+ user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
end } in
Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
end }
@@ -1911,7 +1902,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
match c with
| None -> sigma , None
| Some c ->
- let (sigma,c_interp) = pf_interp_constr ist gl c in
+ let (sigma,c_interp) = interp_constr ist env sigma c in
sigma , Some c_interp
in
let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
@@ -1978,7 +1969,6 @@ let interp_tac_gen lfun avoid_ids debug t =
end }
let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
-let _ = Proof_global.set_interp_tac interp
(* Used to hide interpretation for pretty-print, now just launch tactics *)
(* [global] means that [t] should be internalized outside of goals. *)
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index cce4382c2..55de58361 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -10,7 +10,8 @@ open Util
open Tacexpr
open Mod_subst
open Genarg
-open Constrarg
+open Stdarg
+open Tacarg
open Misctypes
open Globnames
open Term
diff --git a/ltac/tactic_matching.ml b/ltac/tactic_matching.ml
new file mode 100644
index 000000000..ef45ee47e
--- /dev/null
+++ b/ltac/tactic_matching.ml
@@ -0,0 +1,377 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This file extends Matching with the main logic for Ltac's
+ (lazy)match and (lazy)match goal. *)
+
+open Names
+open Tacexpr
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
+
+(** [t] is the type of matching successes. It ultimately contains a
+ {!Tacexpr.glob_tactic_expr} representing the left-hand side of the
+ corresponding matching rule, a matching substitution to be
+ applied, a context substitution mapping identifier to context like
+ those of {!Matching.matching_result}), and a {!Term.constr}
+ substitution mapping corresponding to matched hypotheses. *)
+type 'a t = {
+ subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
+ context : Term.constr Id.Map.t;
+ terms : Term.constr Id.Map.t;
+ lhs : 'a;
+}
+
+
+
+(** {6 Utilities} *)
+
+
+(** Some of the functions of {!Matching} return the substitution with a
+ [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces
+ substitution of the former type to the latter. *)
+let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map ->
+ Constr_matching.bound_ident_map * Pattern.extended_patvar_map =
+ fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc)
+
+
+(** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *)
+let id_map_try_add id x m =
+ match id with
+ | Some id -> Id.Map.add id x m
+ | None -> m
+
+(** Adds a binding to a {!Id.Map.t} if the name is [Name id] *)
+let id_map_try_add_name id x m =
+ match id with
+ | Name id -> Id.Map.add id x m
+ | Anonymous -> m
+
+(** Takes the union of two {!Id.Map.t}. If there is conflict,
+ the binding of the right-hand argument shadows that of the left-hand
+ argument. *)
+let id_map_right_biased_union m1 m2 =
+ if Id.Map.is_empty m1 then m2 (** Don't reconstruct the whole map *)
+ else Id.Map.fold Id.Map.add m2 m1
+
+(** Tests whether the substitution [s] is empty. *)
+let is_empty_subst (ln,lm) =
+ Id.Map.(is_empty ln && is_empty lm)
+
+(** {6 Non-linear patterns} *)
+
+
+(** The patterns of Ltac are not necessarily linear. Non-linear
+ pattern are partially handled by the {!Matching} module, however
+ goal patterns are not primitive to {!Matching}, hence we must deal
+ with non-linearity between hypotheses and conclusion. Subterms are
+ considered equal up to the equality implemented in
+ [equal_instances]. *)
+(* spiwack: it doesn't seem to be quite the same rule for non-linear
+ term patterns and non-linearity between hypotheses and/or
+ conclusion. Indeed, in [Matching], matching is made modulo
+ syntactic equality, and here we merge modulo conversion. It may be
+ a good idea to have an entry point of [Matching] with a partial
+ substitution as argument instead of merging substitution here. That
+ would ensure consistency. *)
+let equal_instances env sigma (ctx',c') (ctx,c) =
+ (* How to compare instances? Do we want the terms to be convertible?
+ unifiable? Do we want the universe levels to be relevant?
+ (historically, conv_x is used) *)
+ CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma c' c
+
+
+(** Merges two substitutions. Raises [Not_coherent_metas] when
+ encountering two instances of the same metavariable which are not
+ equal according to {!equal_instances}. *)
+exception Not_coherent_metas
+let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
+ let merge id oc1 oc2 = match oc1, oc2 with
+ | None, None -> None
+ | None, Some c | Some c, None -> Some c
+ | Some c1, Some c2 ->
+ if equal_instances env sigma c1 c2 then Some c1
+ else raise Not_coherent_metas
+ in
+ let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 in
+ (** ppedrot: Is that even correct? *)
+ let merged = ln +++ ln1 in
+ (merged, Id.Map.merge merge lcm lm)
+
+let matching_error =
+ CErrors.UserError (Some "tactic matching" , Pp.str "No matching clauses for match.")
+
+let imatching_error = (matching_error, Exninfo.null)
+
+(** A functor is introduced to share the environment and the
+ evar_map. They do not change and it would be a pity to introduce
+ closures everywhere just for the occasional calls to
+ {!equal_instances}. *)
+module type StaticEnvironment = sig
+ val env : Environ.env
+ val sigma : Evd.evar_map
+end
+module PatternMatching (E:StaticEnvironment) = struct
+
+
+ (** {6 The pattern-matching monad } *)
+
+
+ (** To focus on the algorithmic portion of pattern-matching, the
+ bookkeeping is relegated to a monad: the composition of the
+ bactracking monad of {!IStream.t} with a "writer" effect. *)
+ (* spiwack: as we don't benefit from the various stream optimisations
+ of Haskell, it may be costly to give the monad in direct style such as
+ here. We may want to use some continuation passing style. *)
+ type 'a tac = 'a Proofview.tactic
+ type 'a m = { stream : 'r. ('a -> unit t -> 'r tac) -> unit t -> 'r tac }
+
+ (** The empty substitution. *)
+ let empty_subst = Id.Map.empty , Id.Map.empty
+
+ (** Composes two substitutions using {!verify_metas_coherence}. It
+ must be a monoid with neutral element {!empty_subst}. Raises
+ [Not_coherent_metas] when composition cannot be achieved. *)
+ let subst_prod s1 s2 =
+ if is_empty_subst s1 then s2
+ else if is_empty_subst s2 then s1
+ else verify_metas_coherence E.env E.sigma s1 s2
+
+ (** The empty context substitution. *)
+ let empty_context_subst = Id.Map.empty
+
+ (** Compose two context substitutions, in case of conflict the
+ right hand substitution shadows the left hand one. *)
+ let context_subst_prod = id_map_right_biased_union
+
+ (** The empty term substitution. *)
+ let empty_term_subst = Id.Map.empty
+
+ (** Compose two terms substitutions, in case of conflict the
+ right hand substitution shadows the left hand one. *)
+ let term_subst_prod = id_map_right_biased_union
+
+ (** Merge two writers (and ignore the first value component). *)
+ let merge m1 m2 =
+ try Some {
+ subst = subst_prod m1.subst m2.subst;
+ context = context_subst_prod m1.context m2.context;
+ terms = term_subst_prod m1.terms m2.terms;
+ lhs = m2.lhs;
+ }
+ with Not_coherent_metas -> None
+
+ (** Monadic [return]: returns a single success with empty substitutions. *)
+ let return (type a) (lhs:a) : a m =
+ { stream = fun k ctx -> k lhs ctx }
+
+ (** Monadic bind: each success of [x] is replaced by the successes
+ of [f x]. The substitutions of [x] and [f x] are composed,
+ dropping the apparent successes when the substitutions are not
+ coherent. *)
+ let (>>=) (type a) (type b) (m:a m) (f:a -> b m) : b m =
+ { stream = fun k ctx -> m.stream (fun x ctx -> (f x).stream k ctx) ctx }
+
+ (** A variant of [(>>=)] when the first argument returns [unit]. *)
+ let (<*>) (type a) (m:unit m) (y:a m) : a m =
+ { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
+
+ (** Failure of the pattern-matching monad: no success. *)
+ let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
+
+ let run (m : 'a m) =
+ let ctx = {
+ subst = empty_subst ;
+ context = empty_context_subst ;
+ terms = empty_term_subst ;
+ lhs = ();
+ } in
+ let eval lhs ctx = Proofview.tclUNIT { ctx with lhs } in
+ m.stream eval ctx
+
+ (** Chooses in a list, in the same order as the list *)
+ let rec pick (l:'a list) (e, info) : 'a m = match l with
+ | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
+ | x :: l ->
+ { stream = fun k ctx -> Proofview.tclOR (k x ctx) (fun e -> (pick l e).stream k ctx) }
+
+ let pick l = pick l imatching_error
+
+ (** Declares a subsitution, a context substitution and a term substitution. *)
+ let put subst context terms : unit m =
+ let s = { subst ; context ; terms ; lhs = () } in
+ { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
+
+ (** Declares a substitution. *)
+ let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
+
+ (** Declares a term substitution. *)
+ let put_terms terms : unit m = put empty_subst empty_context_subst terms
+
+
+
+ (** {6 Pattern-matching} *)
+
+
+ (** [wildcard_match_term lhs] matches a term against a wildcard
+ pattern ([_ => lhs]). It has a single success with an empty
+ substitution. *)
+ let wildcard_match_term = return
+
+ (** [pattern_match_term refresh pat term lhs] returns the possible
+ matchings of [term] with the pattern [pat => lhs]. If refresh is
+ true, refreshes the universes of [term]. *)
+ let pattern_match_term refresh pat term lhs =
+(* let term = if refresh then Termops.refresh_universes_strict term else term in *)
+ match pat with
+ | Term p ->
+ begin
+ try
+ put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
+ return lhs
+ with Constr_matching.PatternMatchingFailure -> fail
+ end
+ | Subterm (with_app_context,id_ctxt,p) ->
+
+ let rec map s (e, info) =
+ { stream = fun k ctx -> match IStream.peek s with
+ | IStream.Nil -> Proofview.tclZERO ~info e
+ | IStream.Cons ({ Constr_matching.m_sub ; m_ctx }, s) ->
+ let subst = adjust m_sub in
+ let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in
+ let terms = empty_term_subst in
+ let nctx = { subst ; context ; terms ; lhs = () } in
+ match merge ctx nctx with
+ | None -> (map s (e, info)).stream k ctx
+ | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
+ }
+ in
+ map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
+
+
+ (** [rule_match_term term rule] matches the term [term] with the
+ matching rule [rule]. *)
+ let rule_match_term term = function
+ | All lhs -> wildcard_match_term lhs
+ | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs
+ | Pat _ ->
+ (** Rules with hypotheses, only work in match goal. *)
+ fail
+
+ (** [match_term term rules] matches the term [term] with the set of
+ matching rules [rules].*)
+ let rec match_term (e, info) term rules = match rules with
+ | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
+ | r :: rules ->
+ { stream = fun k ctx ->
+ let head = rule_match_term term r in
+ let tail e = match_term e term rules in
+ Proofview.tclOR (head.stream k ctx) (fun e -> (tail e).stream k ctx)
+ }
+
+
+ (** [hyp_match_type hypname pat hyps] matches a single
+ hypothesis pattern [hypname:pat] against the hypotheses in
+ [hyps]. Tries the hypotheses in order. For each success returns
+ the name of the matched hypothesis. *)
+ let hyp_match_type hypname pat hyps =
+ pick hyps >>= fun decl ->
+ let id = NamedDecl.get_id decl in
+ let refresh = is_local_def decl in
+ pattern_match_term refresh pat (NamedDecl.get_type decl) () <*>
+ put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+ return id
+
+ (** [hyp_match_type hypname bodypat typepat hyps] matches a single
+ hypothesis pattern [hypname := bodypat : typepat] against the
+ hypotheses in [hyps].Tries the hypotheses in order. For each
+ success returns the name of the matched hypothesis. *)
+ let hyp_match_body_and_type hypname bodypat typepat hyps =
+ pick hyps >>= function
+ | LocalDef (id,body,hyp) ->
+ pattern_match_term false bodypat body () <*>
+ pattern_match_term true typepat hyp () <*>
+ put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+ return id
+ | LocalAssum (id,hyp) -> fail
+
+ (** [hyp_match pat hyps] dispatches to
+ {!hyp_match_type} or {!hyp_match_body_and_type} depending on whether
+ [pat] is [Hyp _] or [Def _]. *)
+ let hyp_match pat hyps =
+ match pat with
+ | Hyp ((_,hypname),typepat) ->
+ hyp_match_type hypname typepat hyps
+ | Def ((_,hypname),bodypat,typepat) ->
+ hyp_match_body_and_type hypname bodypat typepat hyps
+
+ (** [hyp_pattern_list_match pats hyps lhs], matches the list of
+ patterns [pats] against the hypotheses in [hyps], and eventually
+ returns [lhs]. *)
+ let rec hyp_pattern_list_match pats hyps lhs =
+ match pats with
+ | pat::pats ->
+ hyp_match pat hyps >>= fun matched_hyp ->
+ (* spiwack: alternatively it is possible to return the list
+ with the matched hypothesis removed directly in
+ [hyp_match]. *)
+ let select_matched_hyp decl = Id.equal (NamedDecl.get_id decl) matched_hyp in
+ let hyps = CList.remove_first select_matched_hyp hyps in
+ hyp_pattern_list_match pats hyps lhs
+ | [] -> return lhs
+
+ (** [rule_match_goal hyps concl rule] matches the rule [rule]
+ against the goal [hyps|-concl]. *)
+ let rule_match_goal hyps concl = function
+ | All lhs -> wildcard_match_term lhs
+ | Pat (hyppats,conclpat,lhs) ->
+ (* the rules are applied from the topmost one (in the concrete
+ syntax) to the bottommost. *)
+ let hyppats = List.rev hyppats in
+ pattern_match_term false conclpat concl () <*>
+ hyp_pattern_list_match hyppats hyps lhs
+
+ (** [match_goal hyps concl rules] matches the goal [hyps|-concl]
+ with the set of matching rules [rules]. *)
+ let rec match_goal (e, info) hyps concl rules = match rules with
+ | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
+ | r :: rules ->
+ { stream = fun k ctx ->
+ let head = rule_match_goal hyps concl r in
+ let tail e = match_goal e hyps concl rules in
+ Proofview.tclOR (head.stream k ctx) (fun e -> (tail e).stream k ctx)
+ }
+
+end
+
+(** [match_term env sigma term rules] matches the term [term] with the
+ set of matching rules [rules]. The environment [env] and the
+ evar_map [sigma] are not currently used, but avoid code
+ duplication. *)
+let match_term env sigma term rules =
+ let module E = struct
+ let env = env
+ let sigma = sigma
+ end in
+ let module M = PatternMatching(E) in
+ M.run (M.match_term imatching_error term rules)
+
+
+(** [match_goal env sigma hyps concl rules] matches the goal
+ [hyps|-concl] with the set of matching rules [rules]. The
+ environment [env] and the evar_map [sigma] are used to check
+ convertibility for pattern variables shared between hypothesis
+ patterns or the conclusion pattern. *)
+let match_goal env sigma hyps concl rules =
+ let module E = struct
+ let env = env
+ let sigma = sigma
+ end in
+ let module M = PatternMatching(E) in
+ M.run (M.match_goal imatching_error hyps concl rules)
diff --git a/ltac/tactic_matching.mli b/ltac/tactic_matching.mli
new file mode 100644
index 000000000..090207bcc
--- /dev/null
+++ b/ltac/tactic_matching.mli
@@ -0,0 +1,49 @@
+ (************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This file extends Matching with the main logic for Ltac's
+ (lazy)match and (lazy)match goal. *)
+
+
+(** [t] is the type of matching successes. It ultimately contains a
+ {!Tacexpr.glob_tactic_expr} representing the left-hand side of the
+ corresponding matching rule, a matching substitution to be
+ applied, a context substitution mapping identifier to context like
+ those of {!Matching.matching_result}), and a {!Term.constr}
+ substitution mapping corresponding to matched hypotheses. *)
+type 'a t = {
+ subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
+ context : Term.constr Names.Id.Map.t;
+ terms : Term.constr Names.Id.Map.t;
+ lhs : 'a;
+}
+
+
+(** [match_term env sigma term rules] matches the term [term] with the
+ set of matching rules [rules]. The environment [env] and the
+ evar_map [sigma] are not currently used, but avoid code
+ duplication. *)
+val match_term :
+ Environ.env ->
+ Evd.evar_map ->
+ Term.constr ->
+ (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+ Tacexpr.glob_tactic_expr t Proofview.tactic
+
+(** [match_goal env sigma hyps concl rules] matches the goal
+ [hyps|-concl] with the set of matching rules [rules]. The
+ environment [env] and the evar_map [sigma] are used to check
+ convertibility for pattern variables shared between hypothesis
+ patterns or the conclusion pattern. *)
+val match_goal:
+ Environ.env ->
+ Evd.evar_map ->
+ Context.Named.t ->
+ Term.constr ->
+ (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+ Tacexpr.glob_tactic_expr t Proofview.tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 19:41:38 +0000