aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorherbelin2002-05-29 10:48:37 +0000
committerherbelin2002-05-29 10:48:37 +0000
commit32170384190168856efeac5bcf90edf1170b54d6 (patch)
tree0ea86b672df93d997fa1cab70b678ea7abdcf171 /tactics
parent1e5182e9d5c29ae9adeed20dae32969785758809 (diff)
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml352
-rw-r--r--tactics/auto.mli47
-rw-r--r--tactics/autorewrite.ml46
-rw-r--r--tactics/autorewrite.mli4
-rw-r--r--tactics/contradiction.mli19
-rw-r--r--tactics/dhyp.ml119
-rw-r--r--tactics/dhyp.mli11
-rw-r--r--tactics/elim.ml110
-rw-r--r--tactics/elim.mli15
-rw-r--r--tactics/equality.ml203
-rw-r--r--tactics/equality.mli41
-rw-r--r--tactics/extraargs.mli21
-rw-r--r--tactics/extratactics.mli19
-rw-r--r--tactics/hiddentac.ml104
-rw-r--r--tactics/hiddentac.mli91
-rw-r--r--tactics/hipattern.ml21
-rw-r--r--tactics/inv.ml105
-rw-r--r--tactics/inv.mli13
-rw-r--r--tactics/leminv.ml99
-rw-r--r--tactics/leminv.mli15
-rw-r--r--tactics/refine.ml17
-rw-r--r--tactics/refine.mli2
-rw-r--r--tactics/setoid_replace.ml105
-rw-r--r--tactics/setoid_replace.mli5
-rw-r--r--tactics/tacinterp.ml1738
-rw-r--r--tactics/tacinterp.mli115
-rw-r--r--tactics/tactics.ml831
-rw-r--r--tactics/tactics.mli129
-rw-r--r--tactics/wcclausenv.ml7
-rw-r--r--tactics/wcclausenv.mli2
30 files changed, 2818 insertions, 1588 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b9d09f7173..256914d4cb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -32,10 +32,10 @@ open Clenv
open Hiddentac
open Libobject
open Library
-open Vernacinterp
open Printer
open Nametab
open Declarations
+open Tacexpr
(****************************************************************************)
(* The Type of Constructions Autotactic Hints *)
@@ -47,7 +47,7 @@ type auto_tactic =
| Give_exact of constr
| Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
| Unfold_nth of global_reference (* Hint Unfold *)
- | Extern of Coqast.t (* Hint Extern *)
+ | Extern of raw_tactic_expr (* Hint Extern *)
type pri_auto_tactic = {
hname : identifier; (* name of the hint *)
@@ -136,6 +136,8 @@ type frozen_hint_db_table = Hint_db.t Stringmap.t
type hint_db_table = Hint_db.t Stringmap.t ref
+type hint_db_name = string
+
let searchtable = (ref Stringmap.empty : hint_db_table)
let searchtable_map name =
@@ -300,7 +302,10 @@ let make_extern name pri pat tacast =
let add_extern name pri (patmetas,pat) tacast dbname =
(* We check that all metas that appear in tacast have at least
one occurence in the left pattern pat *)
- let tacmetas = Coqast.collect_metas tacast in
+(* TODO
+ let tacmetas = Coqast.collect_metas tacast in
+*)
+ let tacmetas = [] in
match (list_subtract tacmetas patmetas) with
| i::_ ->
errorlabstrm "add_extern"
@@ -328,150 +333,8 @@ let add_trivials l dbnames =
Lib.add_anonymous_leaf (inAutoHint(dbname, List.map make_trivial l)))
dbnames
-let _ =
- vinterp_add
- "HintUnfold"
- (function
- | [ VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_QUALID qid] ->
- let dbnames = if l = [] then ["core"] else
- List.map
- (function VARG_IDENTIFIER i -> string_of_id i
- | _ -> bad_vernac_args "HintUnfold") l in
- fun () ->
- let ref = Nametab.global dummy_loc qid in
- add_unfolds [(hintname, ref)] dbnames
- | _-> bad_vernac_args "HintUnfold")
-
-let _ =
- vinterp_add
- "HintResolve"
- (function
- | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] ->
- let env = Global.env() and sigma = Evd.empty in
- let c1 = Astterm.interp_constr sigma env c in
- let dbnames = if l = [] then ["core"] else
- List.map (function VARG_IDENTIFIER i -> string_of_id i
- | _ -> bad_vernac_args "HintResolve") l in
- fun () -> add_resolves env sigma [hintname, c1] dbnames
- | _-> bad_vernac_args "HintResolve" )
-
-let _ =
- vinterp_add
- "HintImmediate"
- (function
- | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] ->
- let c1 = Astterm.interp_constr Evd.empty (Global.env()) c in
- let dbnames = if l = [] then ["core"] else
- List.map (function VARG_IDENTIFIER i -> string_of_id i
- | _ -> bad_vernac_args "HintImmediate") l in
- fun () -> add_trivials [hintname, c1] dbnames
- | _ -> bad_vernac_args "HintImmediate")
-
-
-let _ =
- vinterp_add
- "HintConstructors"
- (function
- | [VARG_IDENTIFIER idr; VARG_VARGLIST l; VARG_QUALID qid] ->
- begin
- try
- let env = Global.env() and sigma = Evd.empty in
- let isp = destInd (Declare.global_qualified_reference qid) in
- let conspaths =
- let (mib,mip) = Global.lookup_inductive isp in
- mip.mind_consnames in
- let lcons =
- array_map_to_list
- (fun id ->
- let sp = make_path (dirpath (fst isp)) id in
- let c = Declare.global_absolute_reference sp in
- (id, c))
- conspaths in
- let dbnames = if l = [] then ["core"] else
- List.map (function VARG_IDENTIFIER i -> string_of_id i
- | _ -> bad_vernac_args "HintConstructors") l in
- fun () -> add_resolves env sigma lcons dbnames
- with Invalid_argument("mind_specif_of_mind") ->
- error ((Nametab.string_of_qualid qid) ^ " is not an inductive type")
- end
- | _ -> bad_vernac_args "HintConstructors")
-
-let _ =
- vinterp_add
- "HintExtern"
- (function
- | [VARG_IDENTIFIER hintname; VARG_VARGLIST l;
- VARG_NUMBER pri; VARG_CONSTR patcom; VARG_TACTIC tacexp] ->
- let pat =
- Astterm.interp_constrpattern Evd.empty (Global.env()) patcom in
- let dbnames = if l = [] then ["core"] else
- List.map (function VARG_IDENTIFIER i -> string_of_id i
- | _ -> bad_vernac_args "HintConstructors") l in
- fun () -> add_externs hintname pri pat tacexp dbnames
- | _ -> bad_vernac_args "HintExtern")
-
-let _ =
- vinterp_add
- "HintsResolve"
- (function
- | (VARG_VARGLIST l)::lh ->
- let env = Global.env() and sigma = Evd.empty in
- let lhints =
- List.map
- (function
- | VARG_QUALID qid ->
- let ref = Nametab.global dummy_loc qid in
- let env = Global.env() in
- let c = Declare.constr_of_reference ref in
- let _,i = Nametab.repr_qualid qid in
- (i, c)
- | _-> bad_vernac_args "HintsResolve") lh in
- let dbnames = if l = [] then ["core"] else
- List.map (function VARG_IDENTIFIER i -> string_of_id i
- | _-> bad_vernac_args "HintsResolve") l in
- fun () -> add_resolves env sigma lhints dbnames
- | _-> bad_vernac_args "HintsResolve")
-
-let _ =
- vinterp_add
- "HintsUnfold"
- (function
- | (VARG_VARGLIST l)::lh ->
- let lhints =
- List.map (function
- | VARG_QUALID qid ->
- let _,n = Nametab.repr_qualid qid in
- (n, Nametab.global dummy_loc qid)
- | _ -> bad_vernac_args "HintsUnfold") lh in
- let dbnames = if l = [] then ["core"] else
- List.map (function
- | VARG_IDENTIFIER i -> string_of_id i
- | _ -> bad_vernac_args "HintsUnfold") l in
- fun () -> add_unfolds lhints dbnames
- | _ -> bad_vernac_args "HintsUnfold")
-
-let _ =
- vinterp_add
- "HintsImmediate"
- (function
- | (VARG_VARGLIST l)::lh ->
- let lhints =
- List.map
- (function
- | VARG_QUALID qid ->
- let _,n = Nametab.repr_qualid qid in
- let ref = Nametab.locate qid in
- let env = Global.env () in
- let c = Declare.constr_of_reference ref in
- (n, c)
- | _ -> bad_vernac_args "HintsImmediate") lh in
- let dbnames = if l = [] then ["core"] else
- List.map (function
- | VARG_IDENTIFIER i -> string_of_id i
- | _ -> bad_vernac_args "HintsImmediate") l in
- fun () -> add_trivials lhints dbnames
- | _-> bad_vernac_args "HintsImmediate")
-
+open Vernacexpr
+
(**************************************************************************)
(* Functions for printing the hints *)
(**************************************************************************)
@@ -483,7 +346,7 @@ let fmt_autotactic = function
| Res_pf_THEN_trivial_fail (c,clenv) ->
(str"Apply " ++ prterm c ++ str" ; Trivial")
| Unfold_nth c -> (str"Unfold " ++ pr_global c)
- | Extern coqast -> (str "Extern " ++ gentacpr coqast)
+ | Extern coqast -> (str "Extern " ++ Pptactic.pr_raw_tactic coqast)
let fmt_hint v =
(fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ())
@@ -514,7 +377,7 @@ let fmt_hint_list_for_head c =
let fmt_hint_ref ref = fmt_hint_list_for_head (label_of_ref ref)
(* Print all hints associated to head id in any database *)
-let print_hint_qid qid = ppnl(fmt_hint_ref (Nametab.global dummy_loc qid))
+let print_hint_ref ref = ppnl(fmt_hint_ref ref)
let fmt_hint_term cl =
try
@@ -574,30 +437,44 @@ let print_searchtable () =
print_hint_db db)
!searchtable
-let _ =
- vinterp_add "PrintHint"
- (function
- | [] -> fun () -> print_searchtable()
- | _ -> bad_vernac_args "PrintHint")
-
-let _ =
- vinterp_add "PrintHintDb"
- (function
- | [(VARG_IDENTIFIER id)] ->
- fun () -> print_hint_db_by_name (string_of_id id)
- | _ -> bad_vernac_args "PrintHintDb")
-
-let _ =
- vinterp_add "PrintHintGoal"
- (function
- | [] -> fun () -> print_applicable_hint()
- | _ -> bad_vernac_args "PrintHintGoal")
-
-let _ =
- vinterp_add "PrintHintId"
- (function
- | [(VARG_QUALID qid)] -> fun () -> print_hint_qid qid
- | _ -> bad_vernac_args "PrintHintId")
+let add_hints dbnames h =
+ let dbnames = if dbnames = [] then ["core"] else dbnames in match h with
+ | HintsResolve lhints ->
+ let env = Global.env() and sigma = Evd.empty in
+ let f (n,c) =
+ let c = Astterm.interp_constr sigma env c in
+ let n = match n with
+ | None -> basename (sp_of_global env (Declare.reference_of_constr c))
+ | Some n -> n in
+ (n,c) in
+ add_resolves env sigma (List.map f lhints) dbnames
+ | HintsImmediate lhints ->
+ let env = Global.env() and sigma = Evd.empty in
+ let f (n,c) =
+ let c = Astterm.interp_constr sigma env c in
+ let n = match n with
+ | None -> basename (sp_of_global env (Declare.reference_of_constr c))
+ | Some n -> n in
+ (n,c) in
+ add_trivials (List.map f lhints) dbnames
+ | HintsUnfold lhints ->
+ let f (n,locqid) =
+ let r = Nametab.global locqid in
+ let n = match n with
+ | None -> basename (sp_of_global (Global.env()) r)
+ | Some n -> n in
+ (n,r) in
+ add_unfolds (List.map f lhints) dbnames
+ | HintsConstructors (hintname, qid) ->
+ let env = Global.env() and sigma = Evd.empty in
+ let isp = global_inductive qid in
+ let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
+ let lcons = list_tabulate (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in
+ let lcons = List.map2 (fun id c -> (id,c)) (Array.to_list consnames) lcons in
+ add_resolves env sigma lcons dbnames
+ | HintsExtern (hintname, pri, patcom, tacexp) ->
+ let pat = Astterm.interp_constrpattern Evd.empty (Global.env()) patcom in
+ add_externs hintname pri pat tacexp dbnames
(**************************************************************************)
(* Automatic tactics *)
@@ -627,6 +504,29 @@ let make_local_hint_db g =
in Hint_db.add_list hintlist Hint_db.empty
+(* Serait-ce possible de compiler d'abord la tactique puis de faire la
+ substitution sans passer par bdize dont l'objectif est de préparer un
+ terme pour l'affichage ? (HH) *)
+
+(* Si on enlève le dernier argument (gl) conclPattern est calculé une
+fois pour toutes : en particulier si Pattern.somatch produit une UserError
+Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
+si après Intros la conclusion matche le pattern.
+*)
+
+(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
+
+let forward_tac_interp =
+ ref (fun _ -> failwith "tac_interp is not installed for Auto")
+
+let set_extern_interp f = forward_tac_interp := f
+
+let conclPattern concl pat tac gl =
+ let constr_bindings =
+ try Pattern.matches pat concl
+ with PatternMatchingFailure -> error "conclPattern" in
+ !forward_tac_interp constr_bindings tac gl
+
(**************************************************************************)
(* The Trivial tactic *)
(**************************************************************************)
@@ -697,16 +597,11 @@ let full_trivial gl =
let db_list = List.map (fun x -> searchtable_map x) dbnames in
tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
-let dyn_trivial = function
- | [] -> trivial []
- | [Quoted_string "*"] -> full_trivial
- | l -> trivial (List.map
- (function
- | Identifier id -> (string_of_id id)
- | other -> bad_tactic_args "dyn_trivial" [other])
- l)
-
-let h_trivial = hide_tactic "Trivial" dyn_trivial
+let gen_trivial = function
+ | None -> full_trivial
+ | Some l -> trivial l
+
+let h_trivial l = Refiner.abstract_tactic (TacTrivial l) (gen_trivial l)
(**************************************************************************)
(* The classical Auto tactic *)
@@ -807,24 +702,13 @@ let full_auto n gl =
let default_full_auto gl = full_auto !default_search_depth gl
-let dyn_auto l = match l with
- | [] -> auto !default_search_depth []
- | [Integer n] -> auto n []
- | [Quoted_string "*"] -> default_full_auto
- | [Integer n; Quoted_string "*"] -> full_auto n
- | (Integer n)::l1 ->
- auto n (List.map
- (function
- | Identifier id -> (string_of_id id)
- | other -> bad_tactic_args "dyn_auto" [other]) l1)
- | _ ->
- auto !default_search_depth
- (List.map
- (function
- | Identifier id -> (string_of_id id)
- | other -> bad_tactic_args "dyn_auto" [other]) l)
+let gen_auto n dbnames =
+ let n = match n with None -> !default_search_depth | Some n -> n in
+ match dbnames with
+ | None -> full_auto n
+ | Some l -> auto n l
-let h_auto = hide_tactic "Auto" dyn_auto
+let h_auto n l = Refiner.abstract_tactic (TacAuto (n,l)) (gen_auto n l)
(**************************************************************************)
(* The "destructing Auto" from Eduardo *)
@@ -845,19 +729,13 @@ let dautomatic des_opt n = tclTRY (destruct_auto des_opt n)
let default_dauto = dautomatic !default_search_decomp !default_search_depth
-let dyn_dauto = function
- | [] -> default_dauto
- | [Integer n] -> dautomatic !default_search_decomp n
- | [Integer n; Integer p] -> dautomatic p n
- | _ -> invalid_arg "DAuto: non numeric arguments"
-
-let dauto =
- let gentac = hide_tactic "DAuto" dyn_dauto in
- function
- | (None, None) -> gentac []
- | (Some n, None) -> gentac [Integer n]
- | (Some n, Some p) -> gentac [Integer n; Integer p]
- | _ -> assert false
+let dauto = function
+ | None, None -> default_dauto
+ | Some n, None -> dautomatic !default_search_decomp n
+ | Some n, Some p -> dautomatic p n
+ | None, Some p -> dautomatic p !default_search_depth
+
+let h_dauto (n,p) = Refiner.abstract_tactic (TacDAuto (n,p)) (dauto (n,p))
(***************************************)
(*** A new formulation of Auto *********)
@@ -888,8 +766,8 @@ let compileAutoArg contac = function
(tclTHEN
(Tacticals.tryAllClauses
(function
- | Some id -> Dhyp.dHyp id
- | None -> Dhyp.dConcl))
+ | Some id -> Dhyp.h_destructHyp false id
+ | None -> Dhyp.h_destructConcl))
contac)
let compileAutoArgList contac = List.map (compileAutoArg contac)
@@ -931,33 +809,17 @@ let superauto n to_add argl =
let default_superauto g = superauto !default_search_depth [] [] g
-let cvt_autoArg = function
- | "Destructing" -> [Destructing]
- | "UsingTDB" -> [UsingTDB]
- | "NoAutoArg" -> []
- | x -> errorlabstrm "cvt_autoArg"
- (str "Unexpected argument for Auto!" ++ str x)
-
-let cvt_autoArgs =
- list_join_map
- (function
- | Quoted_string s -> (cvt_autoArg s)
- | _ -> errorlabstrm "cvt_autoArgs" (str "String expected"))
-
-let interp_to_add gl = function
- | Qualid qid ->
- let _,id = Nametab.repr_qualid qid in
- (next_ident_away id (pf_ids_of_hyps gl),
- Declare.constr_of_reference (Nametab.global dummy_loc qid))
- | _ -> errorlabstrm "cvt_autoArgs" (str "Qualid expected")
-
-let dyn_superauto l g =
- match l with
- | (Integer n)::a::b::c::to_add ->
- superauto n (List.map (interp_to_add g) to_add) (cvt_autoArgs [a;b;c])g
- | _::a::b::c::to_add ->
- superauto !default_search_depth (List.map (interp_to_add g) to_add)
- (cvt_autoArgs [a;b;c]) g
- | l -> bad_tactic_args "SuperAuto" l g
-
-let h_superauto = hide_tactic "SuperAuto" dyn_superauto
+let interp_to_add gl locqid =
+ let r = Nametab.global locqid in
+ let id = basename (sp_of_global (Global.env()) r) in
+ (next_ident_away id (pf_ids_of_hyps gl), Declare.constr_of_reference r)
+
+let gen_superauto nopt l a b gl =
+ let n = match nopt with Some n -> n | None -> !default_search_depth in
+ let al = (if a then [Destructing] else [])@(if b then [UsingTDB] else []) in
+ superauto n (List.map (interp_to_add gl) l) al gl
+
+let h_superauto no l a b =
+ Refiner.abstract_tactic (TacSuperAuto (no,l,a,b)) (gen_superauto no l a b)
+
+
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 20f770b833..c5266bc583 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -28,7 +28,7 @@ type auto_tactic =
| Give_exact of constr
| Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
| Unfold_nth of global_reference (* Hint Unfold *)
- | Extern of Coqast.t (* Hint Extern *)
+ | Extern of Tacexpr.raw_tactic_expr (* Hint Extern *)
open Rawterm
@@ -59,6 +59,18 @@ type frozen_hint_db_table = Hint_db.t Stringmap.t
type hint_db_table = Hint_db.t Stringmap.t ref
+type hint_db_name = string
+
+val add_hints : hint_db_name list -> Vernacexpr.hints -> unit
+
+val print_searchtable : unit -> unit
+
+val print_applicable_hint : unit -> unit
+
+val print_hint_ref : global_reference -> unit
+
+val print_hint_db_by_name : hint_db_name -> unit
+
val searchtable : hint_db_table
(* [make_exact_entry hint_name (c, ctyp)].
@@ -99,12 +111,15 @@ val make_resolve_hyp :
env -> evar_map -> named_declaration ->
(constr_label * pri_auto_tactic) list
-(* [make_extern name pri pattern tactic_ast] *)
+(* [make_extern name pri pattern tactic_expr] *)
val make_extern :
- identifier -> int -> constr_pattern -> Coqast.t
+ identifier -> int -> constr_pattern -> Tacexpr.raw_tactic_expr
-> constr_label * pri_auto_tactic
+val set_extern_interp :
+ ((int * constr) list -> Tacexpr.raw_tactic_expr -> tactic) -> unit
+
(* Create a Hint database from the pairs (name, constr).
Useful to take the current goal hypotheses as hints *)
@@ -117,9 +132,16 @@ val default_search_depth : int ref
(* Try unification with the precompiled clause, then use registered Apply *)
val unify_resolve : (constr * unit clausenv) -> tactic
+(* [ConclPattern concl pat tacast]:
+ if the term concl matches the pattern pat, (in sense of
+ [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
+ right values to build a tactic *)
+
+val conclPattern : constr -> constr_pattern -> Tacexpr.raw_tactic_expr -> tactic
+
(* The Auto tactic *)
-val auto : int -> string list -> tactic
+val auto : int -> hint_db_name list -> tactic
(* auto with default search depth and with the hint database "core" *)
val default_auto : tactic
@@ -131,14 +153,19 @@ val full_auto : int -> tactic
except the "v62" compatibility database *)
val default_full_auto : tactic
+(* The generic form of auto (second arg [None] means all bases) *)
+val gen_auto : int option -> hint_db_name list option -> tactic
+
(* The hidden version of auto *)
-val h_auto : tactic_arg list -> tactic
+val h_auto : int option -> hint_db_name list option -> tactic
(* Trivial *)
-val trivial : string list -> tactic
+val trivial : hint_db_name list -> tactic
+val gen_trivial : hint_db_name list option -> tactic
val full_trivial : tactic
-val h_trivial : tactic_arg list -> tactic
+val h_trivial : hint_db_name list option -> tactic
+val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
(*s The following is not yet up to date -- Papageno. *)
@@ -147,13 +174,15 @@ val dauto : int option * int option -> tactic
val default_search_decomp : int ref
val default_dauto : tactic
+val h_dauto : int option * int option -> tactic
(* SuperAuto *)
type autoArguments =
| UsingTDB
| Destructing
-val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
-
+(*
val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic
+*)
+val h_superauto : int option -> qualid located list -> bool -> bool -> tactic
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3216a6065b..75c7509ac3 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -5,6 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
+
open Ast
open Coqast
open Equality
@@ -12,12 +13,13 @@ open Hipattern
open Names
open Pp
open Proof_type
-open Tacmach
+open Tacticals
open Tacinterp
open Tactics
open Term
open Util
open Vernacinterp
+open Tacexpr
(* Rewriting rules *)
type rew_rule = constr * bool * tactic
@@ -37,7 +39,7 @@ let _ =
Summary.survive_section = false }
(* Rewriting rules before tactic interpretation *)
-type raw_rew_rule = constr * bool * t
+type raw_rew_rule = constr * bool * raw_tactic_expr
(* Applies all the rules of one base *)
let one_base tac_main bas =
@@ -48,8 +50,8 @@ let one_base tac_main bas =
else
tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
tclTHEN tac
- (if dir then tclREPEAT_MAIN (tclTHENST (rewriteLR csr) [tac_main] tc)
- else tclREPEAT_MAIN (tclTHENST (rewriteRL csr) [tac_main] tc)))
+ (tclREPEAT_MAIN
+ (tclTHENSFIRSTn (general_rewrite dir csr) [|tac_main|] tc)))
tclIDTAC lrul))
(* The AutoRewrite tactic *)
@@ -77,39 +79,3 @@ let (in_hintrewrite,out_hintrewrite)=
(* To add rewriting rules to a base *)
let add_rew_rules base lrul =
Lib.add_anonymous_leaf (in_hintrewrite (base,lrul))
-
-(* The vernac declaration of HintRewrite *)
-let _ = vinterp_add "HintRewrite"
- (function
- | [VARG_STRING ort;VARG_CONSTRLIST lcom;VARG_IDENTIFIER id;VARG_TACTIC t]
- when ort = "LR" || ort = "RL" ->
- (fun () ->
- let (evc,env) = Command.get_current_context () in
- let lcsr =
- List.map (function
- | Node(loc,"CONSTR",l) ->
- let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
- goalopt=None; debug=Tactic_debug.DebugOff } in
- constr_of_Constr (interp_tacarg ist (Node(loc,"COMMAND",l)))
- | _ -> bad_vernac_args "HintRewrite") lcom in
- add_rew_rules (string_of_id id)
- (List.map (fun csr -> (csr,ort = "LR",t)) lcsr))
- | _ -> bad_vernac_args "HintRewrite")
-
-(* To get back the tactic arguments and call AutoRewrite *)
-let v_autorewrite = function
- | (Tac (t,_))::l ->
- let lbas =
- List.map (function
- | Identifier id -> string_of_id id
- | _ -> Tacinterp.bad_tactic_args "AutoRewrite") l in
- autorewrite t lbas
- | l ->
- let lbas =
- List.map (function
- | Identifier id -> string_of_id id
- | _ -> Tacinterp.bad_tactic_args "AutoRewrite") l in
- autorewrite tclIDTAC lbas
-
-(* Declaration of AutoRewrite *)
-let _ = hide_tactic "AutoRewrite" v_autorewrite
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index ce92658661..b24ecb18b9 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -8,10 +8,12 @@
(*i $Id$ i*)
+(*i*)
open Tacmach
+(*i*)
(* Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Term.constr * bool * Coqast.t
+type raw_rew_rule = Term.constr * bool * Tacexpr.raw_tactic_expr
(* To add rewriting rules to a base *)
val add_rew_rules : string -> raw_rew_rule list -> unit
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
new file mode 100644
index 0000000000..27b926d7a7
--- /dev/null
+++ b/tactics/contradiction.mli
@@ -0,0 +1,19 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Term
+open Proof_type
+(*i*)
+
+val absurd : constr -> tactic
+val contradiction_on_hyp : identifier -> tactic
+val contradiction : tactic
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 10e4230d65..720cb6f5f1 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -120,25 +120,24 @@ open Reduction
open Proof_type
open Rawterm
open Tacmach
+open Refiner
open Tactics
open Clenv
open Tactics
open Tacticals
open Libobject
open Library
-open Vernacinterp
open Pattern
open Coqast
open Ast
open Pcoq
+open Tacexpr
(* two patterns - one for the type, and one for the type of the type *)
type destructor_pattern = {
d_typ: constr_pattern;
d_sort: constr_pattern }
-type ('a,'b) location = Hyp of 'a | Concl of 'b
-
(* hypothesis patterns might need to do matching on the conclusion, too.
* conclusion-patterns only need to do matching on the hypothesis *)
type located_destructor_pattern =
@@ -150,7 +149,7 @@ type located_destructor_pattern =
type destructor_data = {
d_pat : located_destructor_pattern;
d_pri : int;
- d_code : Ast.act } (* should be of phylum tactic *)
+ d_code : raw_tactic_expr } (* should be of phylum tactic *)
type t = (identifier,destructor_data) Nbtermdn.t
type frozen_t = (identifier,destructor_data) Nbtermdn.frozen_t
@@ -170,8 +169,8 @@ let rollback f x =
let add (na,dd) =
let pat = match dd.d_pat with
- | Hyp(_,p,_) -> p.d_typ
- | Concl p -> p.d_typ
+ | HypLocation(_,p,_) -> p.d_typ
+ | ConclLocation p -> p.d_typ
in
if Nbtermdn.in_dn tactab na then begin
msgnl (str "Warning [Overriding Destructor Entry " ++
@@ -207,67 +206,59 @@ let ((inDD : destructor_data_object->obj),
open_function = cache_dd;
export_function = export_dd })
-let add_destructor_hint na pat pri code =
+let add_destructor_hint na loc pat pri code =
+ begin match loc, code with
+ | HypLocation _, TacFun ([id],body) -> ()
+ | ConclLocation _, _ -> ()
+ | _ ->
+ errorlabstrm "add_destructor_hint"
+ (str "The tactic should be a function of the hypothesis name") end;
+ let (_,pat) = Astterm.interp_constrpattern Evd.empty (Global.env()) pat in
+ let pat = match loc with
+ | HypLocation b ->
+ HypLocation
+ (b,{d_typ=pat;d_sort=PMeta(Some (Clenv.new_meta()))},
+ {d_typ=PMeta(Some (Clenv.new_meta()));
+ d_sort=PMeta(Some (Clenv.new_meta())) })
+ | ConclLocation () ->
+ ConclLocation({d_typ=pat;d_sort=PMeta(Some (Clenv.new_meta()))}) in
Lib.add_anonymous_leaf
(inDD (na,{ d_pat = pat; d_pri=pri; d_code=code }))
-let _ =
- vinterp_add "HintDestruct"
- (function
- | [VARG_IDENTIFIER na; VARG_AST location; VARG_CONSTR patcom;
- VARG_NUMBER pri; VARG_AST tacexp] ->
- let loc = match location with
- | Node(_,"CONCL",[]) -> Concl()
- | Node(_,"DiscardableHYP",[]) -> Hyp true
- | Node(_,"PreciousHYP",[]) -> Hyp false
- | _ -> assert false
- in
- fun () ->
- let (_,pat) = Astterm.interp_constrpattern
- Evd.empty (Global.env()) patcom in
- let code = Ast.to_act_check_vars ["$0",ETast] ETast tacexp in
- add_destructor_hint na
- (match loc with
- | Hyp b ->
- Hyp(b,{d_typ=pat;d_sort=PMeta(Some (Clenv.new_meta()))},
- { d_typ=PMeta(Some (Clenv.new_meta()));
- d_sort=PMeta(Some (Clenv.new_meta())) })
- | Concl () ->
- Concl({d_typ=pat;d_sort=PMeta(Some (Clenv.new_meta()))}))
- pri code
- | _ -> bad_vernac_args "HintDestruct")
-
let match_dpat dp cls gls =
let cltyp = clause_type cls gls in
match (cls,dp) with
- | (Some id,Hyp(_,hypd,concld)) ->
+ | (Some id,HypLocation(_,hypd,concld)) ->
(matches hypd.d_typ cltyp)@
(matches hypd.d_sort (pf_type_of gls cltyp))@
(matches concld.d_typ (pf_concl gls))@
(matches concld.d_sort (pf_type_of gls (pf_concl gls)))
- | (None,Concl concld) ->
+ | (None,ConclLocation concld) ->
(matches concld.d_typ (pf_concl gls))@
(matches concld.d_sort (pf_type_of gls (pf_concl gls)))
| _ -> error "ApplyDestructor"
+let forward_tac_interp =
+ ref (fun _ -> failwith "tac_interp is not installed for DHyp")
+
+let set_extern_interp f = forward_tac_interp := f
+
let applyDestructor cls discard dd gls =
let mvb = match_dpat dd.d_pat cls gls in
- let astb = match cls with
- | Some id -> ["$0", Vast (nvar id)]
- | None -> ["$0", Vast (nvar (id_of_string "$0"))] in
- (* TODO: find the real location *)
- let tcom = match Ast.eval_act dummy_loc astb dd.d_code with
- | Vast tcom -> tcom
- | _ -> assert false
- in
+ let tac = match cls with
+ | Some id ->
+ let arg = Reference (RIdent (dummy_loc,id)) in
+ TacCall (dummy_loc, Tacexp dd.d_code, [arg])
+ | None -> Tacexp dd.d_code in
let discard_0 =
match (cls,dd.d_pat) with
- | (Some id,Hyp(discardable,_,_)) ->
+ | (Some id,HypLocation(discardable,_,_)) ->
if discard & discardable then thin [id] else tclIDTAC
- | (None,Concl _) -> tclIDTAC
+ | (None,ConclLocation _) -> tclIDTAC
| _ -> error "ApplyDestructor"
in
- (tclTHEN (Tacinterp.interp tcom) discard_0) gls
+ tclTHEN (!forward_tac_interp (TacArg tac)) discard_0 gls
+
(* [DHyp id gls]
@@ -284,19 +275,8 @@ let destructHyp discard id gls =
let cDHyp id gls = destructHyp true id gls
let dHyp id gls = destructHyp false id gls
-open Tacinterp
-
-let _=
- add_tactic "DHyp"
- (function
- | [Identifier id] -> dHyp id
- | l -> bad_tactic_args "DHyp" l)
-
-let _=
- add_tactic "CDHyp"
- (function
- | [Identifier id] -> cDHyp id
- | l -> bad_tactic_args "CDHyp" l)
+let h_destructHyp b id =
+ abstract_tactic (TacDestructHyp (b,(dummy_loc,id))) (destructHyp b id)
(* [DConcl gls]
@@ -309,11 +289,7 @@ let dConcl gls =
let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
tclFIRST (List.map (applyDestructor None false) sorted_ddl) gls
-let _=
- add_tactic "DConcl"
- (function
- | [] -> dConcl
- | l -> bad_tactic_args "DConcl" l)
+let h_destructConcl = abstract_tactic TacDestructConcl dConcl
let to2Lists (table : t) = Nbtermdn.to2lists table
@@ -331,11 +307,10 @@ let rec search n =
let auto_tdb n = tclTRY (tclCOMPLETE (search n))
-let sarch_depth_tdb = ref(5)
-
-let dyn_auto_tdb = function
- | [Integer n] -> auto_tdb n
- | [] -> auto_tdb !sarch_depth_tdb
- | l -> bad_tactic_args "AutoTDB" l
-
-let h_auto_tdb = hide_tactic "AutoTDB" dyn_auto_tdb
+let search_depth_tdb = ref(5)
+
+let depth_tdb = function
+ | None -> !search_depth_tdb
+ | Some n -> n
+
+let h_auto_tdb n = abstract_tactic (TacAutoTDB n) (auto_tdb (depth_tdb n))
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index 4879bafc7b..bedbb26c9e 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -15,5 +15,16 @@ open Tacmach
(* Programmable destruction of hypotheses and conclusions. *)
+val set_extern_interp : (Tacexpr.raw_tactic_expr -> tactic) -> unit
+
+(*
val dHyp : identifier -> tactic
val dConcl : tactic
+*)
+val h_destructHyp : bool -> identifier -> tactic
+val h_destructConcl : tactic
+val h_auto_tdb : int option -> tactic
+
+val add_destructor_hint :
+ identifier -> (bool,unit) Tacexpr.location ->
+ Genarg.constr_ast -> int -> Tacexpr.raw_tactic_expr -> unit
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 4008f10f7c..cbe18ba367 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -23,6 +23,7 @@ open Tacmach
open Tacticals
open Tactics
open Hiddentac
+open Tacexpr
let introElimAssumsThen tac ba =
let nassums =
@@ -85,12 +86,12 @@ let up_to_delta = ref false (* true *)
let general_decompose recognizer c gl =
let typc = pf_type_of gl c in
- (tclTHENS (cut typc)
- [tclTHEN (intro_using tmphyp_name)
- (onLastHyp
- (ifOnHyp recognizer (general_decompose recognizer)
- (fun id -> clear [id])));
- exact_no_check c]) gl
+ tclTHENSV (cut typc)
+ [| tclTHEN (intro_using tmphyp_name)
+ (onLastHyp
+ (ifOnHyp recognizer (general_decompose recognizer)
+ (fun id -> clear [id])));
+ exact_no_check c |] gl
let head_in gls indl t =
try
@@ -101,19 +102,14 @@ let head_in gls indl t =
in List.mem ity indl
with Not_found -> false
-let inductive_of_qualid gls qid =
- let c =
- try Declare.construct_qualified_reference qid
- with Not_found -> Nametab.error_global_not_found qid
- in
- match kind_of_term c with
- | Ind ity -> ity
- | _ ->
- errorlabstrm "Decompose"
- (Nametab.pr_qualid qid ++ str " is not an inductive type")
+let inductive_of = function
+ | Nametab.IndRef ity -> ity
+ | r ->
+ errorlabstrm "Decompose"
+ (Printer.pr_global r ++ str " is not an inductive type")
let decompose_these c l gls =
- let indl = List.map (inductive_of_qualid gls) l in
+ let indl = (*List.map inductive_of*) l in
general_decompose (fun (_,t) -> head_in gls indl t) c gls
let decompose_nonrec c gls =
@@ -131,27 +127,23 @@ let decompose_or c gls =
(fun (_,t) -> is_disjunction t)
c gls
-let dyn_decompose args gl =
- let out_qualid = function
- | Qualid qid -> qid
- | l -> bad_tactic_args "DecomposeThese" [l] gl in
- match args with
- | Command c :: ids ->
- decompose_these (pf_interp_constr gl c) (List.map out_qualid ids) gl
- | Constr c :: ids ->
- decompose_these c (List.map out_qualid ids) gl
- | l -> bad_tactic_args "DecomposeThese" l gl
-
-let h_decompose =
- let v_decompose = hide_tactic "DecomposeThese" dyn_decompose in
- fun ids c ->
- v_decompose
- (Constr c :: List.map (fun x -> Qualid (Nametab.qualid_of_sp x)) ids)
+let inj x = Rawterm.AN (Rawterm.dummy_loc,x)
+let h_decompose l c =
+ Refiner.abstract_tactic
+ (TacDecompose (List.map inj l,c)) (decompose_these c l)
+let h_decompose_or c =
+ Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c)
+
+let h_decompose_and c =
+ Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c)
+
+(*
let vernac_decompose_and =
hide_constr_tactic "DecomposeAnd" decompose_and
let vernac_decompose_or =
hide_constr_tactic "DecomposeOr" decompose_or
+*)
(* The tactic Double performs a double induction *)
@@ -181,7 +173,13 @@ let induction_trailer abs_i abs_j bargs =
[bring_hyps hyps; clear ids; simple_elimination (mkVar id)])
gls))
-let double_ind abs_i abs_j gls =
+let double_ind h1 h2 gls =
+ let abs_i = depth_of_quantified_hypothesis true h1 gls in
+ let abs_j = depth_of_quantified_hypothesis true h2 gls in
+ let (abs_i,abs_j) =
+ if abs_i < abs_j then (abs_i,abs_j) else
+ if abs_i > abs_j then (abs_j,abs_i) else
+ error "Both hypotheses are the same" in
let cl = pf_concl gls in
(tclTHEN (tclDO abs_i intro)
(onLastHyp
@@ -190,38 +188,32 @@ let double_ind abs_i abs_j gls =
(introElimAssumsThen (induction_trailer abs_i abs_j))
([],[]) (mkVar id)))) gls
-let dyn_double_ind = function
- | [Integer i; Integer j] -> double_ind i j
- | _ -> assert false
-
-let _ = add_tactic "DoubleInd" dyn_double_ind
-
+let h_double_induction h1 h2 =
+ Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2)
(*****************************)
(* Decomposing introductions *)
(*****************************)
-let rec intro_pattern p =
- let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
- and case_last = tclLAST_HYP h_simplest_case in
- match p with
- | WildPat -> tclTHEN intro clear_last
- | IdPat id -> intro_mustbe_force id
- | DisjPat l -> tclTHEN introf
- (tclTHENS
- (tclTHEN case_last clear_last)
- (List.map intro_pattern l))
- | ConjPat l ->
- tclTHENSEQ [introf; case_last; clear_last; intros_pattern l]
- | ListPat l -> intros_pattern l
+let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
+let case_last = tclLAST_HYP h_simplest_case
+
+let rec intro_pattern = function
+ | IntroWildcard ->
+ tclTHEN intro clear_last
+ | IntroIdentifier id ->
+ intro_mustbe_force id
+ | IntroOrAndPattern l ->
+ tclTHEN introf
+ (tclTHENS
+ (tclTHEN case_last clear_last)
+ (List.map intros_pattern l))
and intros_pattern l = tclMAP intro_pattern l
-let dyn_intro_pattern = function
- | [] -> intros
- | [Intropattern p] -> intro_pattern p
- | l -> bad_tactic_args "Elim.dyn_intro_pattern" l
+let intro_patterns = function
+ | [] -> tclREPEAT intro
+ | l -> tclMAP intro_pattern l
-let v_intro_pattern = hide_tactic "Intros" dyn_intro_pattern
+let h_intro_patterns l = Refiner.abstract_tactic (TacIntroPattern l) (intro_patterns l)
-let h_intro_pattern p = v_intro_pattern [Intropattern p]
diff --git a/tactics/elim.mli b/tactics/elim.mli
index b67055d27a..c42b27edc1 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -28,12 +28,17 @@ val general_decompose : (identifier * constr -> bool) -> constr -> tactic
val decompose_nonrec : constr -> tactic
val decompose_and : constr -> tactic
val decompose_or : constr -> tactic
-val h_decompose : section_path list -> constr -> tactic
+val h_decompose : inductive list -> constr -> tactic
+val h_decompose_or : constr -> tactic
+val h_decompose_and : constr -> tactic
-val double_ind : int -> int -> tactic
+val double_ind : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis -> tactic
+val h_double_induction : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis->tactic
-val intro_pattern : intro_pattern -> tactic
-val intros_pattern : intro_pattern list -> tactic
+val intro_pattern : Tacexpr.intro_pattern_expr -> tactic
+val intros_pattern : Tacexpr.intro_pattern_expr list -> tactic
+(*
val dyn_intro_pattern : tactic_arg list -> tactic
val v_intro_pattern : tactic_arg list -> tactic
-val h_intro_pattern : intro_pattern -> tactic
+*)
+val h_intro_patterns : Tacexpr.intro_pattern_expr list -> tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c3eb158465..346b9dccbd 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -34,8 +34,10 @@ open Tacticals
open Tactics
open Tacinterp
open Tacred
+open Rawterm
open Vernacinterp
open Coqlib
+open Vernacexpr
open Setoid_replace
open Declarations
@@ -56,7 +58,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
let _,t = splay_prod env sigma ctype in
match match_with_equation t with
| None ->
- if l = []
+ if l = NoBindings
then general_s_rewrite lft2rgt c gl
else error "The term provided does not end with an equation"
| Some (hdcncl,_) ->
@@ -68,18 +70,19 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
else
pf_global gl (id_of_string (hdcncls^suffix))
in
- tclNOTSAMEGOAL (general_elim (c,l) (elim,[])) gl
+ tclNOTSAMEGOAL (general_elim (c,l) (elim,NoBindings)) gl
(* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal
and did not fail for useless conditional rewritings generating an
extra condition *)
(* Conditional rewriting, the success of a rewriting is related
to the resolution of the conditions by a given tactic *)
+
let conditional_rewrite lft2rgt tac (c,bl) =
- tclTHEN_i (general_rewrite_bindings lft2rgt (c,bl))
- (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)
+ tclTHENSFIRSTn (general_rewrite_bindings lft2rgt (c,bl))
+ [|tclIDTAC|] (tclCOMPLETE tac)
-let general_rewrite lft2rgt c = general_rewrite_bindings lft2rgt (c,[])
+let general_rewrite lft2rgt c = general_rewrite_bindings lft2rgt (c,NoBindings)
let rewriteLR_bindings = general_rewrite_bindings true
let rewriteRL_bindings = general_rewrite_bindings false
@@ -87,43 +90,6 @@ let rewriteRL_bindings = general_rewrite_bindings false
let rewriteLR = general_rewrite true
let rewriteRL = general_rewrite false
-let dyn_rewriteLR = function
- | [Command com; Bindings binds] ->
- tactic_com_bind_list rewriteLR_bindings (com,binds)
- | [Constr c; Cbindings binds] ->
- rewriteLR_bindings (c,binds)
- | _ -> assert false
-
-let dyn_rewriteRL = function
- | [Command com; Bindings binds] ->
- tactic_com_bind_list rewriteRL_bindings (com,binds)
- | [Constr c; Cbindings binds] ->
- rewriteRL_bindings (c,binds)
- | _ -> assert false
-
-let dyn_conditional_rewrite lft2rgt = function
- | [(Tacexp tac); (Command com);(Bindings binds)] ->
- tactic_com_bind_list
- (conditional_rewrite lft2rgt (Tacinterp.interp tac))
- (com,binds)
- | [(Tac (tac,_)); (Constr c);(Cbindings binds)] ->
- conditional_rewrite lft2rgt tac (c,binds)
- | _ -> assert false
-
-let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR
-let h_rewriteLR_bindings (c,bl) = v_rewriteLR [(Constr c);(Cbindings bl)]
-let h_rewriteLR c = h_rewriteLR_bindings (c,[])
-
-let v_rewriteRL = hide_tactic "RewriteRL" dyn_rewriteRL
-let h_rewriteRL_bindings (c,bl) = v_rewriteRL [(Constr c);(Cbindings bl)]
-let h_rewriteRL c = h_rewriteRL_bindings (c,[])
-
-let v_conditional_rewriteLR =
- hide_tactic "CondRewriteLR" (dyn_conditional_rewrite true)
-let v_conditional_rewriteRL =
- hide_tactic "CondRewriteRL" (dyn_conditional_rewrite false)
-
-
(* The Rewrite in tactic *)
let general_rewrite_in lft2rgt id (c,l) gl =
let ctype = pf_type_of gl c in
@@ -146,37 +112,15 @@ let general_rewrite_in lft2rgt id (c,l) gl =
try pf_global gl (id_of_string rwr_thm)
with Not_found ->
error ("Cannot find rewrite principle "^rwr_thm) in
- general_elim_in id (c,l) (elim,[]) gl
-
-let conditional_rewrite_in lft2rgt id tac (c,bl) =
- tclTHEN_i (general_rewrite_in lft2rgt id (c,bl))
- (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)
+ general_elim_in id (c,l) (elim,NoBindings) gl
+let rewriteLRin = general_rewrite_in true
+let rewriteRLin = general_rewrite_in false
-let dyn_rewrite_in lft2rgt = function
- | [Identifier id;(Command com);(Bindings binds)] ->
- tactic_com_bind_list (general_rewrite_in lft2rgt id) (com,binds)
- | [Identifier id;(Constr c);(Cbindings binds)] ->
- general_rewrite_in lft2rgt id (c,binds)
- | _ -> assert false
+let conditional_rewrite_in lft2rgt id tac (c,bl) =
+ tclTHENSFIRSTn (general_rewrite_in lft2rgt id (c,bl))
+ [|tclIDTAC|] (tclCOMPLETE tac)
-let dyn_conditional_rewrite_in lft2rgt = function
- | [(Tacexp tac); Identifier id; (Command com);(Bindings binds)] ->
- tactic_com_bind_list
- (conditional_rewrite_in lft2rgt id (Tacinterp.interp tac))
- (com,binds)
- | [(Tac (tac,_)); Identifier id; (Constr c);(Cbindings binds)] ->
- conditional_rewrite_in lft2rgt id tac (c,binds)
- | _ -> assert false
-
-let rewriteLR_in_tac = hide_tactic "RewriteLRin" (dyn_rewrite_in true)
-let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false)
-let v_conditional_rewriteLR_in =
- hide_tactic "CondRewriteLRin" (dyn_conditional_rewrite_in true)
-let v_conditional_rewriteRL_in =
- hide_tactic "CondRewriteRLin" (dyn_conditional_rewrite_in false)
-
-
(* Replacing tactics *)
(* eq,symeq : equality on Set and its symmetry theorem
@@ -195,7 +139,7 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =
| Sort (Type(_)) -> (eqt,sym_eqt)
| _ -> error "replace"
in
- (tclTHENL (elim_type (applist (e, [t1;c1;c2])))
+ (tclTHENLAST (elim_type (applist (e, [t1;c1;c2])))
(tclORELSE assumption
(tclTRY (tclTHEN (apply sym) assumption)))) gl
else
@@ -207,17 +151,6 @@ let replace c2 c1 gl =
let eqT = build_coq_eqT_data.eq () in
let eqT_sym = build_coq_eqT_data.sym () in
abstract_replace (eq,eq_sym) (eqT,eqT_sym) c2 c1 false gl
-
-let dyn_replace args gl =
- match args with
- | [(Command c1);(Command c2)] ->
- replace (pf_interp_constr gl c1) (pf_interp_constr gl c2) gl
- | [(Constr c1);(Constr c2)] ->
- replace c1 c2 gl
- | _ -> assert false
-
-let v_replace = hide_tactic "Replace" dyn_replace
-let h_replace c1 c2 = v_replace [(Constr c1);(Constr c2)]
(* End of Eduardo's code. The rest of this file could be improved
using the functions match_with_equation, etc that I defined
@@ -616,14 +549,18 @@ let discrEverywhere =
(fun gls ->
errorlabstrm "DiscrEverywhere" (str" No discriminable equalities"))
+let discr_tac = function
+ | None -> discrEverywhere
+ | Some id -> discr id
+
let discrConcl gls = discrClause None gls
let discrHyp id gls = discrClause (Some id) gls
-(**)
+(*
let h_discr = hide_atomic_tactic "Discr" discrEverywhere
let h_discrConcl = hide_atomic_tactic "DiscrConcl" discrConcl
let h_discrHyp = hide_ident_or_numarg_tactic "DiscrHyp" discrHyp
-(**)
+*)
(* returns the sigma type (sigS, sigT) with the respective
constructor depending on the sort *)
@@ -870,10 +807,10 @@ let injClause = function
let injConcl gls = injClause None gls
let injHyp id gls = injClause (Some id) gls
-(**)
+(*
let h_injConcl = hide_atomic_tactic "Inj" injConcl
let h_injHyp = hide_ident_or_numarg_tactic "InjHyp" injHyp
-(**)
+*)
let decompEqThen ntac id gls =
let eqn = pf_whd_betadeltaiota gls (clause_type (Some id) gls) in
@@ -935,10 +872,10 @@ let dEq = dEqThen (fun x -> tclIDTAC)
let dEqConcl gls = dEq None gls
let dEqHyp id gls = dEq (Some id) gls
-(**)
+(*
let dEqConcl_tac = hide_atomic_tactic "DEqConcl" dEqConcl
let dEqHyp_tac = hide_ident_or_numarg_tactic "DEqHyp" dEqHyp
-(**)
+*)
let rewrite_msg = function
| None ->
@@ -1094,7 +1031,9 @@ let subst_tuple_term env sigma dep_pair b =
|- (P e1)
|- (eq T e1 e2)
*)
-let revSubstInConcl eqn gls =
+(* Redondant avec Replace ! *)
+
+let substInConcl_RL eqn gls =
let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in
let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in
assert (dependent (mkRel 1) body);
@@ -1105,12 +1044,14 @@ let revSubstInConcl eqn gls =
|- (P e2)
|- (eq T e1 e2)
*)
-let substInConcl eqn gls =
- (tclTHENS (revSubstInConcl (swap_equands gls eqn))
+let substInConcl_LR eqn gls =
+ (tclTHENS (substInConcl_RL (swap_equands gls eqn))
([tclIDTAC;
swapEquandsInConcl])) gls
-let substInHyp eqn id gls =
+let substInConcl l2r = if l2r then substInConcl_LR else substInConcl_RL
+
+let substInHyp_LR eqn id gls =
let (lbeq,(t,e1,e2)) = (find_eq_data_decompose eqn) in
let body = subst_term e1 (clause_type (Some id) gls) in
if not (dependent (mkRel 1) body) then errorlabstrm "SubstInHyp" (mt ());
@@ -1119,11 +1060,13 @@ let substInHyp eqn id gls =
(tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2))
([exact_no_check (mkVar id);tclIDTAC]))])) gls
-let revSubstInHyp eqn id gls =
- (tclTHENS (substInHyp (swap_equands gls eqn) id)
+let substInHyp_RL eqn id gls =
+ (tclTHENS (substInHyp_LR (swap_equands gls eqn) id)
([tclIDTAC;
swapEquandsInConcl])) gls
+let substInHyp l2r = if l2r then substInHyp_LR else substInHyp_RL
+
let try_rewrite tac gls =
try
tac gls
@@ -1138,20 +1081,21 @@ let try_rewrite tac gls =
errorlabstrm "try_rewrite"
(str "Cannot find a well type generalisation of the goal that" ++
str " makes progress the proof.")
-
-let subst eqn cls gls =
+let subst l2r eqn cls gls =
match cls with
- | None -> substInConcl eqn gls
- | Some id -> substInHyp eqn id gls
+ | None -> substInConcl l2r eqn gls
+ | Some id -> substInHyp l2r eqn id gls
(* |- (P a)
- * Subst_Concl a=b
+ * SubstConcl_LR a=b
* |- (P b)
* |- a=b
*)
-let substConcl_LR eqn gls = try_rewrite (subst eqn None) gls
+let substConcl l2r eqn gls = try_rewrite (subst l2r eqn None) gls
+let substConcl_LR = substConcl true
+(*
let substConcl_LR_tac =
let gentac =
hide_tactic "SubstConcl_LR"
@@ -1162,6 +1106,7 @@ let substConcl_LR_tac =
| _ -> assert false)
in
fun eqn -> gentac [Command eqn]
+*)
(* id:(P a) |- G
* SubstHyp a=b id
@@ -1169,20 +1114,24 @@ let substConcl_LR_tac =
* id:(P a) |-a=b
*)
-let hypSubst id cls gls =
+let hypSubst l2r id cls gls =
match cls with
| None ->
- (tclTHENS (substInConcl (clause_type (Some id) gls))
+ (tclTHENS (substInConcl l2r (clause_type (Some id) gls))
([tclIDTAC; exact_no_check (mkVar id)])) gls
| Some hypid ->
- (tclTHENS (substInHyp (clause_type (Some id) gls) hypid)
+ (tclTHENS (substInHyp l2r (clause_type (Some id) gls) hypid)
([tclIDTAC;exact_no_check (mkVar id)])) gls
+let hypSubst_LR = hypSubst true
+
(* id:a=b |- (P a)
* HypSubst id.
* id:a=b |- (P b)
*)
-let substHypInConcl_LR id gls = try_rewrite (hypSubst id None) gls
+let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id None) gls
+let substHypInConcl_LR = substHypInConcl true
+(*
let substHypInConcl_LR_tac =
let gentac =
hide_tactic "SubstHypInConcl_LR"
@@ -1191,22 +1140,19 @@ let substHypInConcl_LR_tac =
| _ -> assert false)
in
fun id -> gentac [Identifier id]
+*)
(* id:a=b H:(P a) |- G
SubstHypInHyp id H.
id:a=b H:(P b) |- G
*)
-let revSubst eqn cls gls =
- match cls with
- | None -> revSubstInConcl eqn gls
- | Some id -> revSubstInHyp eqn id gls
-
(* |- (P b)
SubstConcl_RL a=b
|- (P a)
|- a=b
*)
-let substConcl_RL eqn gls = try_rewrite (revSubst eqn None) gls
+let substConcl_RL = substConcl false
+(*
let substConcl_RL_tac =
let gentac =
hide_tactic "SubstConcl_RL"
@@ -1217,28 +1163,24 @@ let substConcl_RL_tac =
| _ -> assert false)
in
fun eqn -> gentac [Command eqn]
+*)
(* id:(P b) |-G
SubstHyp_RL a=b id
id:(P a) |- G
|- a=b
*)
-let substHyp_RL eqn id gls = try_rewrite (revSubst eqn (Some id)) gls
+let substHyp l2r eqn id gls = try_rewrite (subst l2r eqn (Some id)) gls
+let substHyp_RL = substHyp false
-let revHypSubst id cls gls =
- match cls with
- | None ->
- (tclTHENS (revSubstInConcl (clause_type (Some id) gls))
- ([tclIDTAC; exact_no_check (mkVar id)])) gls
- | Some hypid ->
- (tclTHENS (revSubstInHyp (clause_type (Some id) gls) hypid)
- ([tclIDTAC;exact_no_check (mkVar id)])) gls
+let hypSubst_RL = hypSubst false
(* id:a=b |- (P b)
* HypSubst id.
* id:a=b |- (P a)
*)
-let substHypInConcl_RL id gls = try_rewrite (revHypSubst id None) gls
+let substHypInConcl_RL = substHypInConcl false
+(*
let substHypInConcl_RL_tac =
let gentac =
hide_tactic "SubstHypInConcl_RL"
@@ -1247,6 +1189,7 @@ let substHypInConcl_RL_tac =
| _ -> assert false)
in
fun id -> gentac [Identifier id]
+*)
(* id:a=b H:(P b) |- G
SubstHypInHyp id H.
@@ -1301,26 +1244,6 @@ let (in_autorewrite_rule,out_autorewrite_rule)=
Libobject.cache_function = cache_autorewrite_rule;
Libobject.export_function = export_autorewrite_rule })
-(* Semantic of the HintRewrite vernacular command *)
-let _ =
- vinterp_add "HintRewrite"
- (let rec lrules_arg lrl = function
- | [] -> lrl
- | (VARG_VARGLIST [VARG_CONSTR rule; VARG_STRING ort])::a
- when ort="LR" or ort="RL" ->
- lrules_arg (lrl@[(Astterm.interp_constr Evd.empty
- (Global.env()) rule,ort="LR")]) a
- | _ -> bad_vernac_args "HintRewrite"
- and lbases_arg lbs = function
- | [] -> lbs
- | (VARG_VARGLIST ((VARG_IDENTIFIER rbase)::b))::a ->
- lbases_arg (lbs@[(rbase,lrules_arg [] b)]) a
- | _ -> bad_vernac_args "HintRewrite"
- in
- fun largs () ->
- List.iter (fun c -> Lib.add_anonymous_leaf
- (in_autorewrite_rule c)) (lbases_arg [] largs))
-
(****The tactic****)
(*To build the validation function. Length=number of unproven goals, Valid=a
diff --git a/tactics/equality.mli b/tactics/equality.mli
index cfda6dc345..47ec783742 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -21,29 +21,24 @@ open Pattern
open Wcclausenv
open Tacticals
open Tactics
+open Tacexpr
+open Rawterm
(*i*)
val find_eq_pattern : sorts -> sorts -> constr
-val general_rewrite_bindings : bool -> (constr * constr substitution) -> tactic
+val general_rewrite_bindings : bool -> constr with_bindings -> tactic
val general_rewrite : bool -> constr -> tactic
-val rewriteLR_bindings : (constr * constr substitution) -> tactic
-val h_rewriteLR_bindings : (constr * constr substitution) -> tactic
-val rewriteRL_bindings : (constr * constr substitution) -> tactic
-val h_rewriteRL_bindings : (constr * constr substitution) -> tactic
+val rewriteLR_bindings : constr with_bindings -> tactic
+val rewriteRL_bindings : constr with_bindings -> tactic
val rewriteLR : constr -> tactic
-val h_rewriteLR : constr -> tactic
val rewriteRL : constr -> tactic
-val h_rewriteRL : constr -> tactic
-val conditional_rewrite :
- bool -> tactic -> (constr * constr substitution) -> tactic
-val general_rewrite_in :
- bool -> identifier -> (constr * constr substitution) -> tactic
+val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
+val general_rewrite_in : bool -> identifier -> constr with_bindings -> tactic
val conditional_rewrite_in :
- bool -> identifier -> tactic -> (constr * constr substitution) -> tactic
-
+ bool -> identifier -> tactic -> constr with_bindings -> tactic
(* usage : abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl
@@ -58,7 +53,6 @@ val abstract_replace :
constr * constr -> constr * constr -> constr -> constr -> bool -> tactic
val replace : constr -> constr -> tactic
-val h_replace : constr -> constr -> tactic
type elimination_types =
| Set_Type
@@ -75,13 +69,9 @@ val discrClause : clause -> tactic
val discrConcl : tactic
val discrHyp : identifier -> tactic
val discrEverywhere : tactic
-val h_discrConcl : tactic
-val h_discrHyp : identifier -> tactic
-val h_discrConcl : tactic
-val h_discr : tactic
+val discr_tac : identifier option -> tactic
val inj : identifier -> tactic
-val h_injHyp : identifier -> tactic
-val h_injConcl : tactic
+val injClause : clause -> tactic
val dEq : clause -> tactic
val dEqThen : (int -> tactic) -> clause -> tactic
@@ -90,10 +80,12 @@ val make_iterated_tuple :
env -> evar_map -> (constr * constr) -> (constr * constr)
-> constr * constr * constr
-val subst : constr -> clause -> tactic
-val hypSubst : identifier -> clause -> tactic
-val revSubst : constr -> clause -> tactic
-val revHypSubst : identifier -> clause -> tactic
+val substHypInConcl : bool -> identifier -> tactic
+val substConcl : bool -> constr -> tactic
+val substHyp : bool -> constr -> identifier -> tactic
+
+val hypSubst_LR : identifier -> clause -> tactic
+val hypSubst_RL : identifier -> clause -> tactic
val discriminable : env -> evar_map -> constr -> constr -> bool
@@ -132,4 +124,3 @@ val explicit_hint_base : goal sigma -> hint_base -> rewriting_rule list
val autorewrite :
hint_base list -> tactic list option -> option_step
-> tactic list option -> bool -> int -> tactic
-
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
new file mode 100644
index 0000000000..d5a2b98868
--- /dev/null
+++ b/tactics/extraargs.mli
@@ -0,0 +1,21 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Tacexpr
+open Term
+open Proof_type
+
+val rawwit_orient : bool raw_abstract_argument_type
+val wit_orient : bool closed_abstract_argument_type
+val orient : bool Pcoq.Gram.Entry.e
+
+val rawwit_with_constr : Coqast.t option raw_abstract_argument_type
+val wit_with_constr : constr option closed_abstract_argument_type
+val with_constr : Coqast.t option Pcoq.Gram.Entry.e
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
new file mode 100644
index 0000000000..0e178b52b4
--- /dev/null
+++ b/tactics/extratactics.mli
@@ -0,0 +1,19 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Names
+open Term
+open Proof_type
+
+val h_discrHyp : identifier -> tactic
+val h_injHyp : identifier -> tactic
+val h_rewriteLR : constr -> tactic
+
+val refine_tac : Genarg.open_constr -> tactic
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index bc07c9a4d6..f745570e9a 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -11,34 +11,110 @@
open Term
open Proof_type
open Tacmach
-open Tacentries
+open Rawterm
+open Refiner
+open Tacexpr
+open Tactics
+open Util
+
+let inj_id id = (dummy_loc,id)
+
+(* Basic tactics *)
+let h_intro_move x y =
+ abstract_tactic (TacIntroMove (x, option_app inj_id y)) (intro_move x y)
+let h_intro x = h_intro_move (Some x) None
+let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
+let h_assumption = abstract_tactic TacAssumption assumption
+let h_exact c = abstract_tactic (TacExact c) (exact_check c)
+let h_apply cb = abstract_tactic (TacApply cb) (apply_with_bindings cb)
+let h_elim cb cbo = abstract_tactic (TacElim (cb,cbo)) (elim cb cbo)
+let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c)
+let h_case cb = abstract_tactic (TacCase cb) (general_case_analysis cb)
+let h_case_type c = abstract_tactic (TacCaseType c) (case_type c)
+let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n)
+let h_mutual_fix id n l =
+ abstract_tactic (TacMutualFix (id,n,l)) (mutual_fix id n l)
+let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido)
+let h_mutual_cofix id l =
+ abstract_tactic (TacMutualCofix (id,l)) (mutual_cofix id l)
+
+let h_cut c = abstract_tactic (TacCut c) (cut c)
+let h_true_cut ido c = abstract_tactic (TacTrueCut (ido,c)) (true_cut ido c)
+let h_forward b na c = abstract_tactic (TacForward (b,na,c)) (forward b na c)
+let h_generalize cl = abstract_tactic (TacGeneralize cl) (generalize cl)
+let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
+let h_let_tac id c cl =
+ abstract_tactic (TacLetTac (id,c,cl)) (letin_tac true (Names.Name id) c cl)
+let h_instantiate n c =
+ abstract_tactic (TacInstantiate (n,c)) (Evar_refiner.instantiate n c)
+
+(* Derived basic tactics *)
+let h_old_induction h = abstract_tactic (TacOldInduction h) (old_induct h)
+let h_old_destruct h = abstract_tactic (TacOldDestruct h) (old_destruct h)
+let h_new_induction c = abstract_tactic (TacNewInduction c) (new_induct c)
+let h_new_destruct c = abstract_tactic (TacNewDestruct c) (new_destruct c)
+let h_specialize n (c,bl as d) =
+ abstract_tactic (TacSpecialize (n,d)) (new_hyp n c bl)
+let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
+
+(* Context management *)
+let inj x = AN (Rawterm.dummy_loc,x)
+let h_clear l = abstract_tactic (TacClear (List.map inj l)) (clear l)
+let h_clear_body l =
+ abstract_tactic (TacClearBody (List.map inj l)) (clear_body l)
+let h_move dep id1 id2 =
+ abstract_tactic (TacMove (dep,inj_id id1,inj_id id2)) (move_hyp dep id1 id2)
+let h_rename id1 id2 =
+ abstract_tactic (TacRename (inj_id id1,inj_id id2)) (rename_hyp id1 id2)
+
+(* Constructors *)
+let h_left l = abstract_tactic (TacLeft l) (left l)
+let h_right l = abstract_tactic (TacLeft l) (right l)
+let h_split l = abstract_tactic (TacSplit l) (split l)
+(* Moved to tacinterp because of dependence in Tacinterp.interp
+let h_any_constructor t =
+ abstract_tactic (TacAnyConstructor t) (any_constructor t)
+*)
+let h_constructor n l =
+ abstract_tactic (TacConstructor(AI n,l))(constructor_tac None n l)
+let h_one_constructor n = h_constructor n NoBindings
+let h_simplest_left = h_left NoBindings
+let h_simplest_right = h_right NoBindings
+
+(* Conversion *)
+let h_reduce r cl = abstract_tactic (TacReduce (r,cl)) (reduce r cl)
+let h_change c cl = abstract_tactic (TacChange (c,cl)) (change c cl)
+
+(* Equivalence relations *)
+let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity
+let h_symmetry = abstract_tactic TacSymmetry intros_symmetry
+let h_transitivity c =
+ abstract_tactic (TacTransitivity c) (intros_transitivity c)
+
+(*
let h_clear ids = v_clear [(Clause (List.map (fun x -> InHyp x) ids))]
let h_move dep id1 id2 =
(if dep then v_move else v_move_dep) [Identifier id1;Identifier id2]
-let h_contradiction = v_contradiction []
let h_reflexivity = v_reflexivity []
let h_symmetry = v_symmetry []
-let h_assumption = v_assumption []
-let h_absurd c = v_absurd [(Constr c)]
-let h_exact c = v_exact [(Constr c)]
let h_one_constructor i = v_constructor [(Integer i)]
let h_any_constructor = v_constructor []
let h_transitivity c = v_transitivity [(Constr c)]
let h_simplest_left = v_left [(Cbindings [])]
let h_simplest_right = v_right [(Cbindings [])]
let h_split c = v_split [(Constr c);(Cbindings [])]
-let h_apply c s = v_apply [(Constr c);(Cbindings s)]
-let h_simplest_apply c = v_apply [(Constr c);(Cbindings [])]
-let h_cut c = v_cut [(Constr c)]
-let h_simplest_elim c = v_elim [(Constr c);(Cbindings [])]
-let h_elimType c = v_elimType [(Constr c)]
+*)
+
+let h_simplest_apply c = h_apply (c,NoBindings)
+let h_simplest_elim c = h_elim (c,NoBindings) None
+(*
let h_inductionInt i = v_induction[(Integer i)]
let h_inductionId id = v_induction[(Identifier id)]
-let h_simplest_case c = v_case [(Constr c);(Cbindings [])]
-let h_caseType c = v_caseType [(Constr c)]
+*)
+let h_simplest_case c = h_case (c,NoBindings)
+(*
let h_destructInt i = v_destruct [(Integer i)]
let h_destructId id = v_destruct [(Identifier id)]
-
-
+*)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 517889c167..7a83eff5eb 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -13,35 +13,98 @@ open Names
open Term
open Proof_type
open Tacmach
-open Tacentries
+open Tacexpr
+open Rawterm
(*i*)
(* Tactics for the interpreter. They left a trace in the proof tree
when they are called. *)
-val h_clear : identifier list -> tactic
-val h_move : bool -> identifier -> identifier -> tactic
-val h_contradiction : tactic
-val h_reflexivity : tactic
-val h_symmetry : tactic
+(* Basic tactics *)
+
+val h_intro_move : identifier option -> identifier option -> tactic
+val h_intro : identifier -> tactic
+val h_intros_until : quantified_hypothesis -> tactic
+
val h_assumption : tactic
-val h_absurd : constr -> tactic
val h_exact : constr -> tactic
+
+val h_apply : constr with_bindings -> tactic
+
+val h_elim : constr with_bindings ->
+ constr with_bindings option -> tactic
+val h_elim_type : constr -> tactic
+val h_case : constr with_bindings -> tactic
+val h_case_type : constr -> tactic
+
+val h_mutual_fix : identifier -> int ->
+ (identifier * int * constr) list -> tactic
+val h_fix : identifier option -> int -> tactic
+val h_mutual_cofix : identifier -> (identifier * constr) list -> tactic
+val h_cofix : identifier option -> tactic
+
+val h_cut : constr -> tactic
+val h_true_cut : identifier option -> constr -> tactic
+val h_generalize : constr list -> tactic
+val h_generalize_dep : constr -> tactic
+val h_forward : bool -> name -> constr -> tactic
+val h_let_tac : identifier -> constr -> identifier clause_pattern -> tactic
+val h_instantiate : int -> constr -> tactic
+
+(* Derived basic tactics *)
+
+val h_old_induction : quantified_hypothesis -> tactic
+val h_old_destruct : quantified_hypothesis -> tactic
+val h_new_induction : constr induction_arg -> tactic
+val h_new_destruct : constr induction_arg -> tactic
+val h_specialize : int option -> constr with_bindings -> tactic
+val h_lapply : constr -> tactic
+
+(* Automation tactic : see Auto *)
+
+
+(* Context management *)
+val h_clear : identifier list -> tactic
+val h_clear_body : identifier list -> tactic
+val h_move : bool -> identifier -> identifier -> tactic
+val h_rename : identifier -> identifier -> tactic
+
+
+(* Constructors *)
+(*
+val h_any_constructor : tactic -> tactic
+*)
+val h_constructor : int -> constr substitution -> tactic
+val h_left : constr substitution -> tactic
+val h_right : constr substitution -> tactic
+val h_split : constr substitution -> tactic
+
val h_one_constructor : int -> tactic
-val h_any_constructor : tactic
-val h_transitivity : constr -> tactic
val h_simplest_left : tactic
val h_simplest_right : tactic
-val h_split : constr -> tactic
-val h_apply : constr -> constr substitution -> tactic
+
+
+(* Conversion *)
+val h_reduce : Tacred.red_expr -> hyp_location list -> tactic
+val h_change : constr -> hyp_location list -> tactic
+
+(* Equivalence relations *)
+val h_reflexivity : tactic
+val h_symmetry : tactic
+val h_transitivity : constr -> tactic
+
+(*
+val h_reflexivity : tactic
+val h_symmetry : tactic
+val h_transitivity : constr -> tactic
+*)
val h_simplest_apply : constr -> tactic
-val h_cut : constr -> tactic
val h_simplest_elim : constr -> tactic
-val h_elimType : constr -> tactic
val h_simplest_case : constr -> tactic
-val h_caseType : constr -> tactic
+(*
val h_inductionInt : int -> tactic
val h_inductionId : identifier -> tactic
val h_destructInt : int -> tactic
val h_destructId : identifier -> tactic
+*)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 39c2bd8f77..8e76487045 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -125,6 +125,17 @@ let is_unit_type t = op2bool (match_with_unit_type t)
inductive binary relation R, so that R has only one constructor
establishing its reflexivity. *)
+(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *)
+let x = Name (id_of_string "x")
+let y = Name (id_of_string "y")
+let name_A = Name (id_of_string "A")
+let coq_refl_rel1_pattern =
+ PProd
+ (name_A, PMeta None,
+ PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|])))
+let coq_refl_rel2_pattern =
+ PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|]))
+
let match_with_equation t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
@@ -133,8 +144,8 @@ let match_with_equation t =
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
if nconstr = 1 &&
- (is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0) ||
- is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0))
+ (is_matching coq_refl_rel1_pattern constr_types.(0) ||
+ is_matching coq_refl_rel1_pattern constr_types.(0))
then
Some (hdapp,args)
else
@@ -143,9 +154,13 @@ let match_with_equation t =
let is_equation t = op2bool (match_with_equation t)
+(* ["(?1 -> ?2)"] *)
+let imp a b = PProd (Anonymous, a, b)
+let coq_arrow_pattern = imp (PMeta (Some 1)) (PMeta (Some 2))
+
let match_with_nottype t =
try
- match matches (build_coq_arrow_pattern ()) t with
+ match matches coq_arrow_pattern t with
| [(1,arg);(2,mind)] ->
if is_empty_type mind then Some (mind,arg) else None
| _ -> anomaly "Incorrect pattern matching"
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 07466c4975..5cd54c80e2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -241,8 +241,8 @@ let generalizeRewriteIntros tac depids id gls =
let projectAndApply thin id depids gls =
let env = pf_env gls in
- let subst_hyp_LR id = tclTRY(hypSubst id None) in
- let subst_hyp_RL id = tclTRY(revHypSubst id None) in
+ let subst_hyp_LR id = tclTRY(hypSubst_LR id None) in
+ let subst_hyp_RL id = tclTRY(hypSubst_RL id None) in
let subst_hyp gls =
let orient_rule id =
let (t,t1,t2) = dest_eq gls (pf_get_hyp_typ gls id) in
@@ -372,7 +372,7 @@ let raw_inversion inv_kind indbinding id status gl =
case_nodep_then_using
in
(tclTHENS
- (true_cut_anon cut_concl)
+ (true_cut None cut_concl)
[case_tac (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
(Some elim_predicate) ([],[]) newc;
onLastHyp
@@ -421,6 +421,11 @@ let inversion inv_kind status id gls =
(* Specializing it... *)
+let inv_gen gene thin status = try_intros_until (inversion (gene,thin) status)
+
+open Tacexpr
+
+(*
let hinv_kind = Quoted_string "HalfInversion"
let inv_kind = Quoted_string "Inversion"
let invclr_kind = Quoted_string "InversionClear"
@@ -429,69 +434,19 @@ let com_of_id id =
if id = hinv_kind then None
else if id = inv_kind then Some false
else Some true
+*)
-(* Inv generates nodependent inversion *)
-let (half_inv_tac, inv_tac, inv_clear_tac) =
- let gentac =
- hide_tactic "Inv"
- (function
- | ic :: [id_or_num] ->
- tactic_try_intros_until
- (inversion (false, com_of_id ic) NoDep)
- id_or_num
- | l -> bad_tactic_args "Inv" l)
- in
- ((fun id -> gentac [hinv_kind; Identifier id]),
- (fun id -> gentac [inv_kind; Identifier id]),
- (fun id -> gentac [invclr_kind; Identifier id]))
-
-
-(* Inversion without intros. No vernac entry yet! *)
-let named_inv =
- let gentac =
- hide_tactic "NamedInv"
- (function
- | [ic; Identifier id] -> inversion (true, com_of_id ic) NoDep id
- | l -> bad_tactic_args "NamedInv" l)
- in
- (fun ic id -> gentac [ic; Identifier id])
-
-(* Generates a dependent inversion with a certain generalisation of the goal *)
-let (half_dinv_tac, dinv_tac, dinv_clear_tac) =
- let gentac =
- hide_tactic "DInv"
- (function
- | ic :: [id_or_num] ->
- tactic_try_intros_until
- (inversion (false, com_of_id ic) (Dep None))
- id_or_num
- | l -> bad_tactic_args "DInv" l)
- in
- ((fun id -> gentac [hinv_kind; Identifier id]),
- (fun id -> gentac [inv_kind; Identifier id]),
- (fun id -> gentac [invclr_kind; Identifier id]))
-
-(* generates a dependent inversion using a given generalisation of the goal *)
-let (half_dinv_with, dinv_with, dinv_clear_with) =
- let gentac =
- hide_tactic "DInvWith"
- (function
- | [ic; id_or_num; Command com] ->
- tactic_try_intros_until
- (fun id gls ->
- inversion (false, com_of_id ic)
- (Dep (Some (pf_interp_constr gls com))) id gls)
- id_or_num
- | [ic; id_or_num; Constr c] ->
- tactic_try_intros_until
- (fun id gls ->
- inversion (false, com_of_id ic) (Dep (Some c)) id gls)
- id_or_num
- | l -> bad_tactic_args "DInvWith" l)
- in
- ((fun id c -> gentac [hinv_kind; Identifier id; Constr c]),
- (fun id c -> gentac [inv_kind; Identifier id; Constr c]),
- (fun id c -> gentac [invclr_kind; Identifier id; Constr c]))
+let inv k id = inv_gen false k NoDep id
+
+let half_inv_tac id = inv None (Rawterm.NamedHyp id)
+let inv_tac id = inv (Some false) (Rawterm.NamedHyp id)
+let inv_clear_tac id = inv (Some true) (Rawterm.NamedHyp id)
+
+let dinv k c id = inv_gen false k (Dep c) id
+
+let half_dinv_tac id = dinv None None (Rawterm.NamedHyp id)
+let dinv_tac id = dinv (Some false) None (Rawterm.NamedHyp id)
+let dinv_clear_tac id = dinv (Some true) None (Rawterm.NamedHyp id)
(* InvIn will bring the specified clauses into the conclusion, and then
* perform inversion on the named hypothesis. After, it will intro them
@@ -515,22 +470,4 @@ let invIn com id ids gls =
gls
with e -> wrap_inv_error id e
-let invIn_tac =
- let gentac =
- hide_tactic "InvIn"
- (function
- | (com::(Identifier id)::hl as ll) ->
- let hl' =
- List.map
- (function
- | Identifier id -> id
- | _ -> bad_tactic_args "InvIn" ll) hl
- in
- invIn (com_of_id com) id hl'
- | ll -> bad_tactic_args "InvIn" ll)
- in
- fun com id hl ->
- gentac
- ((Identifier com)
- ::(Identifier id)
- ::(List.map (fun id -> (Identifier id)) hl))
+let invIn_gen com id idl = try_intros_until (fun id -> invIn com id idl) id
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 792f132613..9375efdea2 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -14,14 +14,25 @@ open Term
open Tacmach
(*i*)
+type inversion_status = Dep of constr option | NoDep
+
+val inv_gen :
+ bool -> bool option -> inversion_status -> Rawterm.quantified_hypothesis -> tactic
+val invIn_gen : bool option -> Rawterm.quantified_hypothesis -> identifier list -> tactic
+
+val inv : bool option -> Rawterm.quantified_hypothesis -> tactic
+val dinv : bool option -> constr option -> Rawterm.quantified_hypothesis -> tactic
val half_inv_tac : identifier -> tactic
val inv_tac : identifier -> tactic
val inv_clear_tac : identifier -> tactic
val half_dinv_tac : identifier -> tactic
val dinv_tac : identifier -> tactic
val dinv_clear_tac : identifier -> tactic
+(*
val half_dinv_with : identifier -> constr -> tactic
val dinv_with : identifier -> constr -> tactic
val dinv_clear_with : identifier -> constr -> tactic
-
+*)
+(*
val invIn_tac : identifier -> identifier -> identifier list -> tactic
+*)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 3433618153..1a83dbb5dc 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -32,6 +32,7 @@ open Wcclausenv
open Tacticals
open Tactics
open Inv
+open Vernacexpr
open Safe_typing
let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
@@ -246,7 +247,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
(ConstantEntry { const_entry_body = invProof;
const_entry_type = None;
const_entry_opaque = false },
- NeverDischarge)
+ Nametab.NeverDischarge)
in ()
(* open Pfedit *)
@@ -269,17 +270,6 @@ let inversion_lemma_from_goal n na id sort dep_option inv_op =
str"which are not free in its instance"); *)
add_inversion_lemma na env sigma t sort dep_option inv_op
-open Vernacinterp
-
-let _ =
- vinterp_add
- "MakeInversionLemmaFromHyp"
- (function
- | [VARG_NUMBER n; VARG_IDENTIFIER na; VARG_IDENTIFIER id] ->
- fun () ->
- inversion_lemma_from_goal n na id mk_Prop false inv_clear_tac
- | _ -> bad_vernac_args "MakeInversionLemmaFromHyp")
-
let add_inversion_lemma_exn na com comsort bool tac =
let env = Global.env () and sigma = Evd.empty in
let c = Astterm.interp_type sigma env com in
@@ -290,51 +280,6 @@ let add_inversion_lemma_exn na com comsort bool tac =
| UserError ("Case analysis",s) -> (* référence à Indrec *)
errorlabstrm "Inv needs Nodep Prop Set" s
-let _ =
- vinterp_add
- "MakeInversionLemma"
- (function
- | [VARG_IDENTIFIER na; VARG_CONSTR com; VARG_CONSTR sort] ->
- fun () ->
- add_inversion_lemma_exn na com sort false inv_clear_tac
- | _ -> bad_vernac_args "MakeInversionLemma")
-
-let _ =
- vinterp_add
- "MakeSemiInversionLemmaFromHyp"
- (function
- | [VARG_NUMBER n; VARG_IDENTIFIER na; VARG_IDENTIFIER id] ->
- fun () ->
- inversion_lemma_from_goal n na id mk_Prop false half_inv_tac
- | _ -> bad_vernac_args "MakeSemiInversionLemmaFromHyp")
-
-let _ =
- vinterp_add
- "MakeSemiInversionLemma"
- (function
- | [VARG_IDENTIFIER na; VARG_CONSTR com; VARG_CONSTR sort] ->
- fun () ->
- add_inversion_lemma_exn na com sort false half_inv_tac
- | _ -> bad_vernac_args "MakeSemiInversionLemma")
-
-let _ =
- vinterp_add
- "MakeDependentInversionLemma"
- (function
- | [VARG_IDENTIFIER na; VARG_CONSTR com; VARG_CONSTR sort] ->
- fun () ->
- add_inversion_lemma_exn na com sort true dinv_clear_tac
- | _ -> bad_vernac_args "MakeDependentInversionLemma")
-
-let _ =
- vinterp_add
- "MakeDependentSemiInversionLemma"
- (function
- | [VARG_IDENTIFIER na; VARG_CONSTR com; VARG_CONSTR sort] ->
- fun () ->
- add_inversion_lemma_exn na com sort true half_dinv_tac
- | _ -> bad_vernac_args "MakeDependentSemiInversionLemma")
-
(* ================================= *)
(* Applying a given inversion lemma *)
(* ================================= *)
@@ -355,21 +300,7 @@ let lemInv id c gls =
(str "Cannot refine current goal with the lemma " ++
prterm_env (Global.env()) c)
-let useInversionLemma =
- let gentac =
- hide_tactic "UseInversionLemma"
- (function
- | [id_or_num; Command com] ->
- tactic_try_intros_until
- (fun id gls -> lemInv id (pf_interp_constr gls com) gls)
- id_or_num
- | [id_or_num; Constr c] ->
- tactic_try_intros_until
- (fun id gls -> lemInv id c gls)
- id_or_num
- | l -> bad_vernac_args "useInversionLemma" l)
- in
- fun id c -> gentac [Identifier id;Constr c]
+let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
let lemInvIn id c ids gls =
let hyps = List.map (pf_get_hyp gls) ids in
@@ -387,26 +318,4 @@ let lemInvIn id c ids gls =
| UserError(a,b) -> errorlabstrm "LemInvIn" b
*)
-let useInversionLemmaIn =
- let gentac =
- hide_tactic "UseInversionLemmaIn"
- (function
- | ((Identifier id)::(Command com)::hl as ll) ->
- fun gls ->
- lemInvIn id (pf_interp_constr gls com)
- (List.map
- (function
- | (Identifier id) -> id
- | _ -> bad_vernac_args "UseInversionLemmaIn" ll) hl) gls
- | ((Identifier id)::(Constr c)::hl as ll) ->
- fun gls ->
- lemInvIn id c
- (List.map
- (function
- | (Identifier id) -> id
- | _ -> bad_vernac_args "UseInversionLemmaIn" ll) hl) gls
- | ll -> bad_vernac_args "UseInversionLemmaIn" ll)
- in
- fun id c hl ->
- gentac ((Identifier id)::(Constr c)
- ::(List.map (fun id -> (Identifier id)) hl))
+let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
new file mode 100644
index 0000000000..3d5f33c66a
--- /dev/null
+++ b/tactics/leminv.mli
@@ -0,0 +1,15 @@
+
+open Names
+open Term
+open Rawterm
+open Proof_type
+
+val lemInv_gen : quantified_hypothesis -> constr -> tactic
+val lemInvIn_gen : quantified_hypothesis -> constr -> identifier list -> tactic
+
+val inversion_lemma_from_goal :
+ int -> identifier -> identifier -> sorts -> bool ->
+ (identifier -> tactic) -> unit
+val add_inversion_lemma_exn :
+ identifier -> Coqast.t -> Coqast.t -> bool -> (identifier -> tactic) -> unit
+
diff --git a/tactics/refine.ml b/tactics/refine.ml
index a942b37b71..d1f380e494 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -340,20 +340,3 @@ let refine oc gl =
let th = compute_metamap env gmm c in
tcc_aux th gl
-let refine_tac = Tacmach.hide_openconstr_tactic "Refine" refine
-
-open Proof_type
-
-let dyn_tcc args gl = match args with
- | [Command com] ->
- let env = pf_env gl in
- refine
- (Astterm.interp_casted_openconstr (project gl) env com (pf_concl gl))
- gl
- | [OpenConstr c] ->
- refine c gl
- | _ -> assert false
-
-let tcc_tac = hide_tactic "Tcc" dyn_tcc
-
-
diff --git a/tactics/refine.mli b/tactics/refine.mli
index ec251b8ee9..4f72a26223 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -12,4 +12,6 @@ open Term
open Tacmach
val refine : Pretyping.open_constr -> tactic
+(*
val refine_tac : Pretyping.open_constr -> tactic
+*)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 1362ba2cc0..a147997ba5 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -24,6 +24,8 @@ open Environ
open Termast
open Command
open Tactics
+open Tacticals
+open Vernacexpr
open Safe_typing
open Nametab
@@ -237,14 +239,14 @@ let add_setoid a aeq th =
let eq_ext_name2 = gen_eq_lem_name () in
let _ = Declare.declare_constant eq_ext_name
((ConstantEntry {const_entry_body = eq_morph;
- const_entry_type = None;
+ const_entry_type = None;
const_entry_opaque = true}),
- Declare.NeverDischarge) in
+ Nametab.NeverDischarge) in
let _ = Declare.declare_constant eq_ext_name2
((ConstantEntry {const_entry_body = eq_morph2;
const_entry_type = None;
const_entry_opaque = true}),
- Declare.NeverDischarge) in
+ Nametab.NeverDischarge) in
let eqmorph = (current_constant eq_ext_name) in
let eqmorph2 = (current_constant eq_ext_name2) in
(Lib.add_anonymous_leaf
@@ -257,21 +259,9 @@ let add_setoid a aeq th =
else errorlabstrm "Add Setoid" (str "Not a valid setoid theory")
(* The vernac command "Add Setoid" *)
+let add_setoid a aeq th =
+ add_setoid (constr_of a) (constr_of aeq) (constr_of th)
-let constr_of_comarg = function
- | VARG_CONSTR c -> constr_of c
- | _ -> anomaly "Add Setoid"
-
-let _ =
- vinterp_add "AddSetoid"
- (function
- | [(VARG_CONSTR a); (VARG_CONSTR aeq); (VARG_CONSTR th)] ->
- (fun () -> (add_setoid
- (constr_of a)
- (constr_of aeq)
- (constr_of th)))
- | _ -> anomaly "AddSetoid")
-
(***************** Adding a morphism to the database ****************************)
(* We maintain a table of the currently edited proofs of morphism lemma
@@ -347,7 +337,7 @@ let gen_compat_lemma env m body larg lisset =
| _ -> assert false
in aux larg lisset 0
-let new_morphism m id =
+let new_morphism m id hook =
if morphism_table_mem m
then errorlabstrm "New Morphism"
(str "The term " ++ prterm m ++ str " is already declared as a morphism")
@@ -368,9 +358,9 @@ let new_morphism m id =
let poss = (List.map setoid_table_mem args_t) in
let lem = (gen_compat_lemma env m body args_t poss) in
let lemast = (ast_of_constr true env lem) in
- new_edited id m poss;
- start_proof_com (Some id) Declare.NeverDischarge lemast;
- (Options.if_verbose Vernacentries.show_open_subgoals ()))
+ new_edited id m poss;
+ start_proof_com (Some id) (false,Nametab.NeverDischarge) lemast hook;
+ (Options.if_verbose Vernacentries.show_open_subgoals ()))
let rec sub_bool l1 n = function
| [] -> []
@@ -464,7 +454,7 @@ let add_morphism lem_name (m,profil) =
((ConstantEntry {const_entry_body = lem_2;
const_entry_type = None;
const_entry_opaque = true}),
- Declare.NeverDischarge) in
+ Nametab.NeverDischarge) in
let lem2 = (current_constant lem2_name) in
(Lib.add_anonymous_leaf
(morphism_to_obj (m,
@@ -481,54 +471,13 @@ let add_morphism lem_name (m,profil) =
arg_types = args_t;
lem2 = None}))));
Options.if_verbose ppnl (prterm m ++str " is registered as a morphism")
-
-let _ =
- let current_save = vinterp_map "SaveNamed" in
- overwriting_vinterp_add "SaveNamed"
- (function
- |[] -> (fun () ->
- let pf_id = Pfedit.get_current_proof_name () in
- current_save [] ();
- if (is_edited pf_id)
- then
- (add_morphism pf_id (what_edited pf_id);
- no_more_edited pf_id))
- | _ -> assert false)
+let morphism_hook stre ref =
+ let pf_id = basename (sp_of_global (Global.env()) ref) in
+ if (is_edited pf_id)
+ then
+ (add_morphism pf_id (what_edited pf_id); no_more_edited pf_id)
-let _ =
- let current_defined = vinterp_map "DefinedNamed" in
- overwriting_vinterp_add "DefinedNamed"
- (function
- |[] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in
- current_defined [] ();
- if (is_edited pf_id)
- then
- (add_morphism pf_id (what_edited pf_id);
- no_more_edited pf_id))
- | _ -> assert false)
-
-(*
-let _ =
- vinterp_add "NewMorphism"
- (function
- | [(VARG_IDENTIFIER s)] ->
- (fun () ->
- try
- (let m = Declare.global_reference CCI s in
- new_morphism m (gen_lem_name m))
- with
- Not_found ->
- errorlabstrm "New Morphism"
- (str "The term " ++ str(string_of_id s) ++ str" is not a known name"))
- | _ -> anomaly "NewMorphism")
-*)
-
-let _ =
- vinterp_add "NamedNewMorphism"
- (function
- | [(VARG_IDENTIFIER s);(VARG_CONSTR m)] ->
- (fun () -> new_morphism (constr_of m) s)
- | _ -> anomaly "NewMorphism")
+let new_named_morphism id m = new_morphism (constr_of m) id morphism_hook
(****************************** The tactic itself *******************************)
@@ -670,21 +619,3 @@ let general_s_rewrite lft2rgt c gl =
let setoid_rewriteLR = general_s_rewrite true
let setoid_rewriteRL = general_s_rewrite false
-
-let dyn_setoid_replace = function
- | [(Constr c1);(Constr c2)] -> (fun gl -> setoid_replace c1 c2 None gl)
- | _ -> invalid_arg "Setoid_replace : Bad arguments"
-
-let h_setoid_replace = hide_tactic "Setoid_replace" dyn_setoid_replace
-
-let dyn_setoid_rewriteLR = function
- | [(Constr c)] -> setoid_rewriteLR c
- | _ -> invalid_arg "Setoid_rewrite : Bad arguments"
-
-let h_setoid_rewriteLR = hide_tactic "Setoid_rewriteLR" dyn_setoid_rewriteLR
-
-let dyn_setoid_rewriteRL = function
- | [(Constr c)] -> setoid_rewriteRL c
- | _ -> invalid_arg "Setoid_rewrite : Bad arguments"
-
-let h_setoid_rewriteRL = hide_tactic "Setoid_rewriteRL" dyn_setoid_rewriteRL
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index c280bb269f..d8bc556562 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -10,6 +10,7 @@
open Term
open Proof_type
+open Genarg
val equiv_list : unit -> constr list
@@ -20,3 +21,7 @@ val setoid_rewriteLR : constr -> tactic
val setoid_rewriteRL : constr -> tactic
val general_s_rewrite : bool -> constr -> tactic
+
+val add_setoid : constr_ast -> constr_ast -> constr_ast -> unit
+
+val new_named_morphism : Names.identifier -> constr_ast -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
new file mode 100644
index 0000000000..2d8f7c9048
--- /dev/null
+++ b/tactics/tacinterp.ml
@@ -0,0 +1,1738 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Astterm
+open Closure
+open RedFlags
+open Declarations
+open Dyn
+open Libobject
+open Pattern
+open Pp
+open Rawterm
+open Sign
+open Tacred
+open Util
+open Names
+open Nameops
+open Nametab
+open Pfedit
+open Proof_type
+open Refiner
+open Tacmach
+open Tactic_debug
+open Coqast
+open Ast
+open Term
+open Termops
+open Declare
+open Tacexpr
+open Safe_typing
+open Typing
+open Hiddentac
+open Genarg
+
+let err_msg_tactic_not_found macro_loc macro =
+ user_err_loc
+ (macro_loc,"macro_expand",
+ (str "Tactic macro " ++ str macro ++ spc () ++ str "not found"))
+
+let error_syntactic_metavariables_not_allowed loc =
+ user_err_loc
+ (loc,"out_ident",
+ str "Syntactic metavariables allowed only in quotations")
+
+let skip_metaid = function
+ | AI x -> x
+ | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
+
+(* Values for interpretation *)
+type value =
+ | VClosure of interp_sign * raw_tactic_expr
+ | VTactic of tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *)
+ | VFTactic of value list * (value list->tactic)
+ | VRTactic of (goal list sigma * validation)
+ | VContext of interp_sign * direction_flag
+ * (pattern_ast,raw_tactic_expr) match_rule list
+ | VFun of (identifier * value) list * identifier option list *raw_tactic_expr
+ | VVoid
+ | VInteger of int
+ | VIdentifier of identifier (* idents which are not refs, as in "Intro H" *)
+ | VConstr of constr
+ | VConstr_context of constr
+ | VRec of value ref
+
+(* Signature for interpretation: val_interp and interpretation functions *)
+and interp_sign =
+ { evc : Evd.evar_map;
+ env : Environ.env;
+ lfun : (identifier * value) list;
+ lmatch : (int * constr) list;
+ goalopt : goal sigma option;
+ debug : debug_info }
+
+(* For tactic_of_value *)
+exception NotTactic
+
+(* Gives the constr corresponding to a Constr tactic_arg *)
+let constr_of_VConstr = function
+ | VConstr c -> c
+ | _ -> anomalylabstrm "constr_of_VConstr" (str "Not a Constr tactic_arg")
+
+(* Gives the constr corresponding to a Constr_context tactic_arg *)
+let constr_of_VConstr_context = function
+ | VConstr_context c -> c
+ | _ ->
+ anomalylabstrm "constr_of_VConstr_context" (str
+ "Not a Constr_context tactic_arg")
+
+(*
+(* Gives identifiers and makes the possible injection constr -> ident *)
+let make_ids ast = function
+ | Identifier id -> id
+ | Constr c ->
+ (try destVar c with
+ | Invalid_argument "destVar" ->
+ anomalylabstrm "make_ids"
+ (str "This term cannot be reduced to an identifier" ++ fnl () ++
+ print_ast ast))
+ | _ -> anomalylabstrm "make_ids" (str "Not an identifier")
+*)
+
+let pr_value env = function
+ | VVoid -> str "()"
+ | VInteger n -> int n
+ | VIdentifier id -> pr_id id
+ | VConstr c -> Printer.prterm_env env c
+ | VConstr_context c -> Printer.prterm_env env c
+ | (VClosure _ | VTactic _ | VFTactic _ | VRTactic _ |
+ VContext _ | VFun _ | VRec _) -> str "<fun>"
+
+(* Transforms a named_context into a (string * constr) list *)
+let make_hyps = List.map (fun (id,_,typ) -> (id,body_of_type typ))
+
+(* Transforms an id into a constr if possible *)
+let constr_of_id ist id =
+ match ist.goalopt with
+ | None -> construct_reference ist.env id
+ | Some goal ->
+ let hyps = pf_hyps goal in
+ if mem_named_context id hyps then
+ mkVar id
+ else
+ let csr = global_qualified_reference (make_short_qualid id) in
+ (match kind_of_term csr with
+ | Var _ -> raise Not_found
+ | _ -> csr)
+
+(* To embed several objects in Coqast.t *)
+let ((tactic_in : (interp_sign -> raw_tactic_expr) -> Dyn.t),
+ (tactic_out : Dyn.t -> (interp_sign -> raw_tactic_expr))) =
+ create "tactic"
+
+let ((value_in : value -> Dyn.t),
+ (value_out : Dyn.t -> value)) = create "value"
+
+let tacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t))
+let tacticOut = function
+ | TacArg (TacDynamic (_,d)) ->
+ if (tag d) = "tactic" then
+ tactic_out d
+ else
+ anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic")
+ | ast ->
+ anomalylabstrm "tacticOut"
+ (str "Not a Dynamic ast: " (* ++ print_ast ast*) )
+
+let valueIn t = TacDynamic (dummy_loc,value_in t)
+let valueOut = function
+ | TacDynamic (_,d) ->
+ if (tag d) = "value" then
+ value_out d
+ else
+ anomalylabstrm "valueOut" (str "Dynamic tag should be value")
+ | ast ->
+ anomalylabstrm "valueOut"
+ (str "Not a Dynamic ast: " (* ++ print_ast ast*) )
+
+let constrIn c = constrIn c
+let constrOut = constrOut
+
+let loc = dummy_loc
+
+(* Table of interpretation functions *)
+let interp_tab =
+ (Hashtbl.create 17 : (string , interp_sign -> Coqast.t -> value) Hashtbl.t)
+
+(* Adds an interpretation function *)
+let interp_add (ast_typ,interp_fun) =
+ try
+ Hashtbl.add interp_tab ast_typ interp_fun
+ with
+ Failure _ ->
+ errorlabstrm "interp_add"
+ (str "Cannot add the interpretation function for " ++ str ast_typ ++ str " twice")
+
+(* Adds a possible existing interpretation function *)
+let overwriting_interp_add (ast_typ,interp_fun) =
+ if Hashtbl.mem interp_tab ast_typ then
+ begin
+ Hashtbl.remove interp_tab ast_typ;
+ warning ("Overwriting definition of tactic interpreter command " ^ ast_typ)
+ end;
+ Hashtbl.add interp_tab ast_typ interp_fun
+
+(* Finds the interpretation function corresponding to a given ast type *)
+let look_for_interp = Hashtbl.find interp_tab
+
+(* Globalizes the identifier *)
+
+let find_reference ist qid =
+ (* We first look for a variable of the current proof *)
+ match Nametab.repr_qualid qid, ist.goalopt with
+ | (d,id),Some gl when repr_dirpath d = [] & List.mem id (pf_ids_of_hyps gl)
+ -> VarRef id
+ | _ -> Nametab.locate qid
+
+let coerce_to_reference ist = function
+ | VConstr c ->
+ (try reference_of_constr c
+ with Not_found -> invalid_arg_loc (loc, "Not a reference"))
+(* | VIdentifier id -> VarRef id*)
+ | v -> errorlabstrm "coerce_to_reference"
+ (str "The value" ++ spc () ++ pr_value ist.env v ++
+ str "cannot be coerced to a reference")
+
+(* turns a value into an evaluable reference *)
+let error_not_evaluable s =
+ errorlabstrm "evalref_of_ref"
+ (str "Cannot coerce" ++ spc () ++ s ++ spc () ++
+ str "to an evaluable reference")
+
+let coerce_to_evaluable_ref env c =
+ let ev = match c with
+ | VConstr c when isConst c -> EvalConstRef (destConst c)
+ | VConstr c when isVar c -> EvalVarRef (destVar c)
+(* | VIdentifier id -> EvalVarRef id*)
+ | _ -> error_not_evaluable (pr_value env c)
+ in
+ if not (Tacred.is_evaluable env ev) then
+ error_not_evaluable (pr_value env c);
+ ev
+
+let coerce_to_inductive = function
+ | VConstr c when isInd c -> destInd c
+ | x ->
+ try
+ let r = match x with
+ | VConstr c -> reference_of_constr c
+ | _ -> failwith "" in
+ errorlabstrm "coerce_to_inductive"
+ (Printer.pr_global r ++ str " is not an inductive type")
+ with _ ->
+ errorlabstrm "coerce_to_inductive"
+ (str "Found an argument which should be an inductive type")
+
+(* Summary and Object declaration *)
+let mactab = ref Gmap.empty
+
+let lookup qid = Gmap.find (locate_tactic qid) !mactab
+
+let _ =
+ let init () = mactab := Gmap.empty in
+ let freeze () = !mactab in
+ let unfreeze fs = mactab := fs in
+ Summary.declare_summary "tactic-definition"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init;
+ Summary.survive_section = false }
+
+(* Interpretation of extra generic arguments *)
+type genarg_interp_type =
+ interp_sign -> raw_generic_argument -> closed_generic_argument
+let extragenargtab = ref (Gmap.empty : (string,genarg_interp_type) Gmap.t)
+let add_genarg_interp id f = extragenargtab := Gmap.add id f !extragenargtab
+let lookup_genarg_interp id =
+ try Gmap.find id !extragenargtab
+ with Not_found -> failwith ("No interpretation function found for entry "^id)
+
+
+(* Unboxes VRec *)
+let unrec = function
+ | VRec v -> !v
+ | a -> a
+
+(************* GLOBALIZE ************)
+
+(* We have identifier <| global_reference <| constr *)
+
+(* Globalize a name which can be fresh *)
+let glob_ident l ist x =
+ (* We use identifier both for variables and new names; thus nothing to do *)
+ if List.mem x (fst ist) then () else l:=x::!l;
+ x
+
+let glob_name l ist = function
+ | Anonymous -> Anonymous
+ | Name id -> Name (glob_ident l ist id)
+
+(* Globalize a name which must be bound -- actually just check it is bound *)
+let glob_hyp (lfun,_) (loc,id) =
+ if List.mem id lfun then id
+ else
+(*
+ try let _ = lookup (make_short_qualid id) in id
+ with Not_found ->
+*)
+ Pretype_errors.error_var_not_found_loc loc id
+
+let glob_lochyp ist (loc,_ as locid) = (loc,glob_hyp ist locid)
+
+let error_unbound_metanum loc n =
+ user_err_loc
+ (loc,"glob_qualid_or_metanum", str "?" ++ int n ++ str " is unbound")
+
+let glob_metanum ist loc n =
+ if List.mem n (snd ist) then n else error_unbound_metanum loc n
+
+let glob_hyp_or_metanum ist = function
+ | AN (loc,id) -> AN (loc,glob_hyp ist (loc,id))
+ | MetaNum (loc,n) -> MetaNum (loc,glob_metanum ist loc n)
+
+let glob_qualid_or_metanum ist = function
+ | AN (loc,qid) -> AN (loc,qualid_of_sp (sp_of_global (Global.env())(Nametab.global (loc,qid))))
+ | MetaNum (loc,n) -> MetaNum (loc,glob_metanum ist loc n)
+
+let glob_reference ist (_,qid as locqid) =
+ let dir, id = repr_qualid qid in
+ try
+ if dir = empty_dirpath && List.mem id (fst ist) then qid
+ else raise Not_found
+ with Not_found ->
+ qualid_of_sp (sp_of_global (Global.env()) (Nametab.global locqid))
+
+let glob_ltac_qualid ist (loc,qid as locqid) =
+ try qualid_of_sp (locate_tactic qid)
+ with Not_found -> glob_reference ist locqid
+
+let glob_ltac_reference ist = function
+ | RIdent (loc,id) ->
+ if List.mem id (fst ist) then RIdent (loc,id)
+ else RQualid (loc,glob_ltac_qualid ist (loc,make_short_qualid id))
+ | RQualid qid -> RQualid (loc,glob_ltac_qualid ist qid)
+
+let rec glob_intro_pattern lf ist = function
+ | IntroOrAndPattern l ->
+ IntroOrAndPattern (List.map (List.map (glob_intro_pattern lf ist)) l)
+ | IntroWildcard ->
+ IntroWildcard
+ | IntroIdentifier id ->
+ IntroIdentifier (glob_ident lf ist id)
+
+let glob_quantified_hypothesis ist x =
+ (* We use identifier both for variables and quantified hyps (no way to
+ statically check the existence of a quantified hyp); thus nothing to do *)
+ x
+
+let glob_constr ist c =
+ let _ = Astterm.interp_rawconstr_gen Evd.empty (Global.env()) [] false (fst ist) c in
+ c
+
+(* Globalize bindings *)
+let glob_binding ist (b,c) =
+ (glob_quantified_hypothesis ist b,glob_constr ist c)
+
+let glob_bindings ist = function
+ | NoBindings -> NoBindings
+ | ImplicitBindings l -> ImplicitBindings (List.map (glob_constr ist) l)
+ | ExplicitBindings l -> ExplicitBindings (List.map (glob_binding ist) l)
+
+let glob_constr_with_bindings ist (c,bl) =
+ (glob_constr ist c, glob_bindings ist bl)
+
+let glob_clause_pattern ist (l,occl) =
+ let rec check = function
+ | (hyp,l) :: rest ->
+ let (loc,_ as id) = skip_metaid hyp in
+ (AI(loc,glob_hyp ist id),l)::(check rest)
+ | [] -> []
+ in (l,check occl)
+
+let glob_induction_arg ist = function
+ | ElimOnConstr c -> ElimOnConstr (glob_constr ist c)
+ | ElimOnAnonHyp n as x -> x
+ | ElimOnIdent (loc,id) as x -> x
+
+(* Globalize a reduction expression *)
+let glob_evaluable_or_metanum ist = function
+ | AN (loc,qid) -> AN (loc,glob_reference ist (loc,qid))
+ | MetaNum (loc,n) -> MetaNum (loc,glob_metanum ist loc n)
+
+let glob_unfold ist (l,qid) = (l,glob_evaluable_or_metanum ist qid)
+
+let glob_flag ist red =
+ { red with rConst = List.map (glob_evaluable_or_metanum ist) red.rConst }
+
+let glob_pattern ist (l,c) = (l,glob_constr ist c)
+
+let glob_redexp ist = function
+ | Unfold l -> Unfold (List.map (glob_unfold ist) l)
+ | Fold l -> Fold (List.map (glob_constr ist) l)
+ | Cbv f -> Cbv (glob_flag ist f)
+ | Lazy f -> Lazy (glob_flag ist f)
+ | Pattern l -> Pattern (List.map (glob_pattern ist) l)
+ | (Red _ | Simpl | Hnf as r) -> r
+ | ExtraRedExpr (s,l) -> ExtraRedExpr (s, List.map (glob_constr ist) l)
+
+(* Interprets an hypothesis name *)
+let glob_hyp_location ist = function
+ | InHyp id ->
+ let (loc,_ as id) = skip_metaid id in
+ InHyp (AI(loc,glob_hyp ist id))
+ | InHypType id ->
+ let (loc,_ as id) = skip_metaid id in
+ InHypType (AI(loc,glob_hyp ist id))
+
+(* Reads a pattern *)
+let glob_pattern evc env lfun = function
+ | Subterm (ido,pc) ->
+ let lfun = List.map (fun id -> (id, mkVar id)) lfun in
+ let (metas,_) = interp_constrpattern_gen evc env lfun pc in
+ metas, Subterm (ido,pc)
+ | Term pc ->
+ let lfun = List.map (fun id -> (id, mkVar id)) lfun in
+ let (metas,_) = interp_constrpattern_gen evc env lfun pc in
+ metas, Term pc
+
+let glob_constr_may_eval ist = function
+ | ConstrEval (r,c) -> ConstrEval (glob_redexp ist r,glob_constr ist c)
+ | ConstrContext (locid,c) ->
+ ConstrContext ((loc,glob_hyp ist locid),glob_constr ist c)
+ | ConstrTypeOf c -> ConstrTypeOf (glob_constr ist c)
+ | ConstrTerm c -> ConstrTerm (glob_constr ist c)
+
+(* Reads the hypotheses of a Match Context rule *)
+let rec glob_match_context_hyps evc env lfun = function
+ | (NoHypId mp)::tl ->
+ let metas1, pat = glob_pattern evc env lfun mp in
+ let lfun, metas2, hyps = glob_match_context_hyps evc env lfun tl in
+ lfun, metas1@metas2, (NoHypId pat)::hyps
+ | (Hyp ((_,s) as locs,mp))::tl ->
+ let metas1, pat = glob_pattern evc env lfun mp in
+ let lfun, metas2, hyps = glob_match_context_hyps evc env lfun tl in
+ s::lfun, metas1@metas2, Hyp (locs,pat)::hyps
+ | [] -> lfun, [], []
+
+(* Utilities *)
+let rec filter_some = function
+ | None :: l -> filter_some l
+ | Some a :: l -> a :: filter_some l
+ | [] -> []
+
+let extract_names lrc =
+ List.fold_right
+ (fun ((loc,name),_) l ->
+ if List.mem name l then
+ user_err_loc
+ (loc, "glob_tactic", str "This variable is bound several times");
+ name::l)
+ lrc []
+
+let extract_let_names lrc =
+ List.fold_right
+ (fun ((loc,name),_,_) l ->
+ if List.mem name l then
+ user_err_loc
+ (loc, "glob_tactic", str "This variable is bound several times");
+ name::l)
+ lrc []
+
+(* Globalizes tactics *)
+let rec glob_atomic lf ist = function
+ (* Basic tactics *)
+ | TacIntroPattern l -> TacIntroPattern (List.map (glob_intro_pattern lf ist) l)
+ | TacIntrosUntil hyp -> TacIntrosUntil (glob_quantified_hypothesis ist hyp)
+ | TacIntroMove (ido,ido') ->
+ TacIntroMove (option_app (glob_ident lf ist) ido,
+ option_app (fun (loc,_ as x) -> (loc,glob_hyp ist x)) ido')
+ | TacAssumption -> TacAssumption
+ | TacExact c -> TacExact (glob_constr ist c)
+ | TacApply cb -> TacApply (glob_constr_with_bindings ist cb)
+ | TacElim (cb,cbo) ->
+ TacElim (glob_constr_with_bindings ist cb,
+ option_app (glob_constr_with_bindings ist) cbo)
+ | TacElimType c -> TacElimType (glob_constr ist c)
+ | TacCase cb -> TacCase (glob_constr_with_bindings ist cb)
+ | TacCaseType c -> TacCaseType (glob_constr ist c)
+ | TacFix (idopt,n) -> TacFix (option_app (glob_ident lf ist) idopt,n)
+ | TacMutualFix (id,n,l) ->
+ let f (id,n,c) = (glob_ident lf ist id,n,glob_constr ist c) in
+ TacMutualFix (glob_ident lf ist id, n, List.map f l)
+ | TacCofix idopt -> TacCofix (option_app (glob_ident lf ist) idopt)
+ | TacMutualCofix (id,l) ->
+ let f (id,c) = (glob_ident lf ist id,glob_constr ist c) in
+ TacMutualCofix (glob_ident lf ist id, List.map f l)
+ | TacCut c -> TacCut (glob_constr ist c)
+ | TacTrueCut (ido,c) ->
+ TacTrueCut (option_app (glob_ident lf ist) ido, glob_constr ist c)
+ | TacForward (b,na,c) -> TacForward (b,glob_name lf ist na,glob_constr ist c)
+ | TacGeneralize cl -> TacGeneralize (List.map (glob_constr ist) cl)
+ | TacGeneralizeDep c -> TacGeneralizeDep (glob_constr ist c)
+ | TacLetTac (id,c,clp) ->
+ TacLetTac (id,glob_constr ist c,glob_clause_pattern ist clp)
+ | TacInstantiate (n,c) -> TacInstantiate (n,glob_constr ist c)
+
+ (* Automation tactics *)
+ | TacTrivial l -> TacTrivial l
+ | TacAuto (n,l) -> TacAuto (n,l)
+ | TacAutoTDB n -> TacAutoTDB n
+ | TacDestructHyp (b,(loc,_ as id)) -> TacDestructHyp(b,(loc,glob_hyp ist id))
+ | TacDestructConcl -> TacDestructConcl
+ | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
+ | TacDAuto (n,p) -> TacDAuto (n,p)
+
+ (* Derived basic tactics *)
+ | TacOldInduction h -> TacOldInduction (glob_quantified_hypothesis ist h)
+ | TacNewInduction c -> TacNewInduction (glob_induction_arg ist c)
+ | TacOldDestruct h -> TacOldDestruct (glob_quantified_hypothesis ist h)
+ | TacNewDestruct c -> TacNewDestruct (glob_induction_arg ist c)
+ | TacDoubleInduction (h1,h2) ->
+ let h1 = glob_quantified_hypothesis ist h1 in
+ let h2 = glob_quantified_hypothesis ist h2 in
+ TacDoubleInduction (h1,h2)
+ | TacDecomposeAnd c -> TacDecomposeAnd (glob_constr ist c)
+ | TacDecomposeOr c -> TacDecomposeOr (glob_constr ist c)
+ | TacDecompose (l,c) ->
+ let l = List.map (glob_qualid_or_metanum ist) l in
+ TacDecompose (l,glob_constr ist c)
+ | TacSpecialize (n,l) -> TacSpecialize (n,glob_constr_with_bindings ist l)
+ | TacLApply c -> TacLApply (glob_constr ist c)
+
+ (* Context management *)
+ | TacClear l -> TacClear (List.map (glob_hyp_or_metanum ist) l)
+ | TacClearBody l -> TacClearBody (List.map (glob_hyp_or_metanum ist) l)
+ | TacMove (dep,id1,id2) -> TacMove (dep,glob_lochyp ist id1,glob_lochyp ist id2)
+ | TacRename (id1,id2) -> TacRename (glob_lochyp ist id1, glob_lochyp ist id2)
+
+ (* Constructors *)
+ | TacLeft bl -> TacLeft (glob_bindings ist bl)
+ | TacRight bl -> TacRight (glob_bindings ist bl)
+ | TacSplit bl -> TacSplit (glob_bindings ist bl)
+ | TacAnyConstructor t -> TacAnyConstructor (option_app (glob_tactic ist) t)
+ | TacConstructor (n,bl) -> TacConstructor (n, glob_bindings ist bl)
+
+ (* Conversion *)
+ | TacReduce (r,cl) ->
+ TacReduce (glob_redexp ist r, List.map (glob_hyp_location ist) cl)
+ | TacChange (c,cl) ->
+ TacChange (glob_constr ist c, List.map (glob_hyp_location ist) cl)
+
+ (* Equivalence relations *)
+ | TacReflexivity -> TacReflexivity
+ | TacSymmetry -> TacSymmetry
+ | TacTransitivity c -> TacTransitivity (glob_constr ist c)
+
+ (* For extensions *)
+ | TacExtend (opn,l) ->
+ let _ = lookup_tactic opn in
+ TacExtend (opn,List.map (glob_genarg ist) l)
+ | TacAlias (_,l,body) -> failwith "TODO"
+
+and glob_tactic ist tac = snd (glob_tactic_seq ist tac)
+
+and glob_tactic_seq (lfun,lmeta as ist) = function
+ | TacAtom (loc,t) ->
+ let lf = ref lfun in
+ let t = glob_atomic lf ist t in
+ !lf, TacAtom (loc, t)
+ | TacFun tacfun -> lfun, TacFun (glob_tactic_fun ist tacfun)
+ | TacFunRec (name,tacfun) ->
+ lfun, TacFunRec (name,glob_tactic_fun ((snd name)::lfun,lmeta) tacfun)
+ | TacLetRecIn (lrc,u) ->
+ let names = extract_names lrc in
+ let ist = (names@lfun,lmeta) in
+ let lrc = List.map (fun (n,b) -> (n,glob_tactic_fun ist b)) lrc in
+ lfun, TacLetRecIn (lrc,glob_tactic ist u)
+ | TacLetIn (l,u) ->
+ let l = List.map (fun (n,c,b) -> (n,option_app (glob_constr_may_eval ist) c,glob_tacarg ist b)) l in
+ let ist' = ((extract_let_names l)@lfun,lmeta) in
+ lfun, TacLetIn (l,glob_tactic ist' u)
+ | TacLetCut l ->
+ let f (n,c,t) = (n,glob_constr_may_eval ist c,glob_tacarg ist t) in
+ lfun, TacLetCut (List.map f l)
+ | TacMatchContext (lr,lmr) ->
+ lfun, TacMatchContext(lr, glob_match_rule ist lmr)
+ | TacMatch (c,lmr) ->
+ lfun, TacMatch (glob_constr_may_eval ist c,glob_match_rule ist lmr)
+ | TacId -> lfun, TacId
+ | TacFail n as x -> lfun, x
+ | TacProgress tac -> lfun, TacProgress (glob_tactic ist tac)
+ | TacAbstract (tac,s) -> lfun, TacAbstract (glob_tactic ist tac,s)
+ | TacThen (t1,t2) ->
+ let lfun', t1 = glob_tactic_seq ist t1 in
+ let lfun'', t2 = glob_tactic_seq (lfun',lmeta) t2 in
+ lfun'', TacThen (t1,t2)
+ | TacThens (t,tl) ->
+ let lfun', t = glob_tactic_seq ist t in
+ (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
+ lfun', TacThens (t, List.map (glob_tactic (lfun',lmeta)) tl)
+ | TacDo (n,tac) -> lfun, TacDo (n,glob_tactic ist tac)
+ | TacTry tac -> lfun, TacTry (glob_tactic ist tac)
+ | TacInfo tac -> lfun, TacInfo (glob_tactic ist tac)
+ | TacRepeat tac -> lfun, TacRepeat (glob_tactic ist tac)
+ | TacOrelse (tac1,tac2) ->
+ lfun, TacOrelse (glob_tactic ist tac1,glob_tactic ist tac2)
+ | TacFirst l -> lfun, TacFirst (List.map (glob_tactic ist) l)
+ | TacSolve l -> lfun, TacSolve (List.map (glob_tactic ist) l)
+ | TacArg a -> lfun, TacArg (glob_tacarg ist a)
+
+and glob_tactic_fun (lfun,lmeta) (var,body) =
+ let lfun' = List.rev_append (filter_some var) lfun in
+ (var,glob_tactic (lfun',lmeta) body)
+
+and glob_tacarg ist = function
+ | TacVoid -> TacVoid
+ | Reference r -> Reference (glob_ltac_reference ist r)
+ | Integer n -> Integer n
+ | ConstrMayEval c -> ConstrMayEval (glob_constr_may_eval ist c)
+ | MetaNumArg (loc,n) -> MetaNumArg (loc,glob_metanum ist loc n)
+ | MetaIdArg (loc,_) -> error_syntactic_metavariables_not_allowed loc
+ | TacCall (loc,f,l) ->
+ TacCall (loc,glob_tacarg ist f,List.map (glob_tacarg ist) l)
+ | Tacexp t -> Tacexp (glob_tactic ist t)
+ | TacDynamic(_,t) as x ->
+ (match tag t with
+ | "tactic"|"value"|"constr" -> x
+ | s -> anomaly_loc (loc, "Tacinterp.val_interp",
+ str "Unknown dynamic: <" ++ str s ++ str ">"))
+
+(* Reads the rules of a Match Context or a Match *)
+and glob_match_rule (lfun,lmeta as ist) = function
+ | (All tc)::tl ->
+ (All (glob_tactic ist tc))::(glob_match_rule ist tl)
+ | (Pat (rl,mp,tc))::tl ->
+ let env = Global.env() in
+ let lfun',metas1,hyps = glob_match_context_hyps Evd.empty env lfun rl in
+ let metas2,pat = glob_pattern Evd.empty env lfun mp in
+ let metas = list_uniquize (metas1@metas2@lmeta) in
+ (Pat (hyps,pat,glob_tactic (lfun',metas) tc))::(glob_match_rule ist tl)
+ | [] -> []
+
+and glob_genarg ist x =
+ match genarg_tag x with
+ | BoolArgType -> in_gen rawwit_bool (out_gen rawwit_bool x)
+ | IntArgType -> in_gen rawwit_int (out_gen rawwit_int x)
+ | IntOrVarArgType ->
+ let f = function
+ | ArgVar (loc,id) -> ArgVar (loc,glob_hyp ist (loc,id))
+ | ArgArg n as x -> x in
+ in_gen rawwit_int_or_var (f (out_gen rawwit_int_or_var x))
+ | StringArgType ->
+ in_gen rawwit_string (out_gen rawwit_string x)
+ | PreIdentArgType ->
+ in_gen rawwit_pre_ident (out_gen rawwit_pre_ident x)
+ | IdentArgType ->
+ in_gen rawwit_ident (glob_hyp ist (dummy_loc,out_gen rawwit_ident x))
+ | QualidArgType ->
+ let (loc,qid) = out_gen rawwit_qualid x in
+ in_gen rawwit_qualid (loc,glob_ltac_qualid ist (loc,qid))
+ | ConstrArgType ->
+ in_gen rawwit_constr (glob_constr ist (out_gen rawwit_constr x))
+ | ConstrMayEvalArgType ->
+ in_gen rawwit_constr_may_eval (glob_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
+ | QuantHypArgType ->
+ in_gen rawwit_quant_hyp
+ (glob_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
+ | RedExprArgType ->
+ in_gen rawwit_red_expr (glob_redexp ist (out_gen rawwit_red_expr x))
+ | TacticArgType ->
+ in_gen rawwit_tactic (glob_tactic ist (out_gen rawwit_tactic x))
+ | CastedOpenConstrArgType ->
+ in_gen rawwit_casted_open_constr
+ (glob_constr ist (out_gen rawwit_casted_open_constr x))
+ | ConstrWithBindingsArgType ->
+ in_gen rawwit_constr_with_bindings
+ (glob_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
+ | List0ArgType _ -> app_list0 (glob_genarg ist) x
+ | List1ArgType _ -> app_list1 (glob_genarg ist) x
+ | OptArgType _ -> app_opt (glob_genarg ist) x
+ | PairArgType _ -> app_pair (glob_genarg ist) (glob_genarg ist) x
+ | ExtraArgType s -> x
+
+
+(************* END GLOBALIZE ************)
+
+(* Reads the head of Fun *)
+let read_fun ast =
+ let rec read_fun_rec = function
+ | Node(_,"VOID",[])::tl -> None::(read_fun_rec tl)
+ | Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl)
+ | [] -> []
+ | _ ->
+ anomalylabstrm "Tacinterp.read_fun_rec" (str "Fun not well formed")
+ in
+ match ast with
+ | Node(_,"FUNVAR",l) -> read_fun_rec l
+ | _ ->
+ anomalylabstrm "Tacinterp.read_fun" (str "Fun not well formed")
+
+(* Reads the clauses of a Rec *)
+let rec read_rec_clauses = function
+ | [] -> []
+ | Node(_,"RECCLAUSE",[Nvar(_,name);it;body])::tl ->
+ (name,it,body)::(read_rec_clauses tl)
+ |_ ->
+ anomalylabstrm "Tacinterp.read_rec_clauses"
+ (str "Rec not well formed")
+
+(* Associates variables with values and gives the remaining variables and
+ values *)
+let head_with_value (lvar,lval) =
+ let rec head_with_value_rec lacc = function
+ | ([],[]) -> (lacc,[],[])
+ | (vr::tvr,ve::tve) ->
+ (match vr with
+ | None -> head_with_value_rec lacc (tvr,tve)
+ | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
+ | (vr,[]) -> (lacc,vr,[])
+ | ([],ve) -> (lacc,[],ve)
+ in
+ head_with_value_rec [] (lvar,lval)
+
+(* Gives a context couple if there is a context identifier *)
+let give_context ctxt = function
+ | None -> []
+ | Some id -> [id,VConstr_context ctxt]
+
+(* Reads a pattern *)
+let read_pattern evc env lfun = function
+ | Subterm (ido,pc) ->
+ Subterm (ido,snd (interp_constrpattern_gen evc env lfun pc))
+ | Term pc ->
+ Term (snd (interp_constrpattern_gen evc env lfun pc))
+
+(* Reads the hypotheses of a Match Context rule *)
+let rec read_match_context_hyps evc env lfun lidh = function
+ | (NoHypId mp)::tl ->
+ (NoHypId (read_pattern evc env lfun mp))::
+ (read_match_context_hyps evc env lfun lidh tl)
+ | (Hyp ((loc,id) as locid,mp))::tl ->
+ if List.mem id lidh then
+ user_err_loc (loc,"Tacinterp.read_match_context_hyps",
+ str ("Hypothesis pattern-matching variable "^(string_of_id id)^
+ " used twice in the same pattern"))
+ else
+ (Hyp (locid,read_pattern evc env lfun mp))::
+ (read_match_context_hyps evc env lfun (id::lidh) tl)
+ | [] -> []
+
+(* Reads the rules of a Match Context or a Match *)
+let rec read_match_rule evc env lfun = function
+ | (All tc)::tl -> (All tc)::(read_match_rule evc env lfun tl)
+ | (Pat (rl,mp,tc))::tl ->
+ (Pat (read_match_context_hyps evc env lfun [] rl,
+ read_pattern evc env lfun mp,tc))
+ ::(read_match_rule evc env lfun tl)
+ | [] -> []
+
+(* For Match Context and Match *)
+exception No_match
+exception Not_coherent_metas
+
+let is_match_catchable = function
+ | No_match | FailError _ -> true
+ | e -> Logic.catchable_exception e
+
+(* Verifies if the matched list is coherent with respect to lcm *)
+let rec verify_metas_coherence ist lcm = function
+ | (num,csr)::tl ->
+ if (List.for_all
+ (fun (a,b) ->
+ if a=num then
+ Reductionops.is_conv ist.env ist.evc b csr
+ else
+ true) lcm) then
+ (num,csr)::(verify_metas_coherence ist lcm tl)
+ else
+ raise Not_coherent_metas
+ | [] -> []
+
+(* Tries to match a pattern and a constr *)
+let apply_matching pat csr =
+ try
+ (Pattern.matches pat csr)
+ with
+ PatternMatchingFailure -> raise No_match
+
+(* Tries to match one hypothesis pattern with a list of hypotheses *)
+let apply_one_mhyp_context ist lmatch mhyp lhyps noccopt =
+ let get_pattern = function
+ | Hyp (_,pat) -> pat
+ | NoHypId pat -> pat
+ and get_id_couple id = function
+ | Hyp((_,idpat),_) -> [idpat,VIdentifier id]
+ | NoHypId _ -> [] in
+ let rec apply_one_mhyp_context_rec mhyp lhyps_acc nocc = function
+ | (id,hyp)::tl ->
+ (match (get_pattern mhyp) with
+ | Term t ->
+ (try
+ let lmeta =
+ verify_metas_coherence ist lmatch (Pattern.matches t hyp) in
+ (get_id_couple id mhyp,[],lmeta,tl,(id,hyp),None)
+ with | PatternMatchingFailure | Not_coherent_metas ->
+ apply_one_mhyp_context_rec mhyp (lhyps_acc@[id,hyp]) 0 tl)
+ | Subterm (ic,t) ->
+ (try
+ let (lm,ctxt) = sub_match nocc t hyp in
+ let lmeta = verify_metas_coherence ist lmatch lm in
+ (get_id_couple id mhyp,give_context ctxt
+ ic,lmeta,tl,(id,hyp),Some nocc)
+ with
+ | NextOccurrence _ ->
+ apply_one_mhyp_context_rec mhyp (lhyps_acc@[id,hyp]) 0 tl
+ | Not_coherent_metas ->
+ apply_one_mhyp_context_rec mhyp lhyps_acc (nocc + 1) ((id,hyp)::tl)))
+ | [] -> raise No_match in
+ let nocc =
+ match noccopt with
+ | None -> 0
+ | Some n -> n in
+ apply_one_mhyp_context_rec mhyp [] nocc lhyps
+
+(*
+let coerce_to_qualid loc = function
+ | Constr c when isVar c -> make_short_qualid (destVar c)
+ | Constr c ->
+ (try qualid_of_sp (sp_of_global (Global.env()) (reference_of_constr c))
+ with Not_found -> invalid_arg_loc (loc, "Not a reference"))
+ | Identifier id -> make_short_qualid id
+ | Qualid qid -> qid
+ | _ -> invalid_arg_loc (loc, "Not a reference")
+*)
+
+let constr_to_id loc c =
+ if isVar c then destVar c
+ else invalid_arg_loc (loc, "Not an identifier")
+
+let constr_to_qid loc c =
+ try qualid_of_sp (sp_of_global (Global.env ()) (reference_of_constr c))
+ with _ -> invalid_arg_loc (loc, "Not a global reference")
+
+(* Check for LetTac *)
+let check_clause_pattern ist (l,occl) =
+ match ist.goalopt with
+ | Some gl ->
+ let sign = pf_hyps gl in
+ let rec check acc = function
+ | (hyp,l) :: rest ->
+ let _,hyp = skip_metaid hyp in
+ if List.mem hyp acc then
+ error ("Hypothesis "^(string_of_id hyp)^" occurs twice");
+ if not (mem_named_context hyp sign) then
+ error ("No such hypothesis: " ^ (string_of_id hyp));
+ (hyp,l)::(check (hyp::acc) rest)
+ | [] -> []
+ in (l,check [] occl)
+ | None -> error "No goal"
+
+(* Debug reference *)
+let debug = ref DebugOff
+
+(* Sets the debugger mode *)
+let set_debug pos = debug := pos
+
+(* Gives the state of debug *)
+let get_debug () = !debug
+
+(* Interprets an identifier *)
+let eval_ident ist id =
+ try (unrec (List.assoc id ist.lfun))
+ with | Not_found ->
+(*
+ try (vcontext_interp ist (lookup (make_short_qualid id)))
+ with | Not_found ->
+*)
+VIdentifier id
+
+(* Gives the identifier corresponding to an Identifier tactic_arg *)
+let id_of_Identifier = function
+ | VConstr c when isVar c -> destVar c
+ | VIdentifier id -> id
+ | _ ->
+ anomalylabstrm "id_of_Identifier" (str "Not an IDENTIFIER tactic_arg")
+
+let coerce_to_hypothesis ist = function
+ | VConstr c when isVar c -> destVar c
+ | VIdentifier id -> id
+ | v -> errorlabstrm "coerce_to_hypothesis"
+ (str "Cannot coerce" ++ spc () ++ pr_value ist.env v ++ spc () ++
+ str "to an existing hypothesis")
+
+let ident_interp ist id =
+ id_of_Identifier (eval_ident ist id)
+
+let hyp_interp ist (loc,id) =
+ coerce_to_hypothesis ist (eval_ident ist id)
+
+let name_interp ist = function
+ | Anonymous -> Anonymous
+ | Name id -> Name (ident_interp ist id)
+
+let hyp_or_metanum_interp ist = function
+ | AN (loc,id) -> ident_interp ist id
+ | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lmatch)
+
+(* To avoid to move to much simple functions in the big recursive block *)
+let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented")
+
+let interp_pure_qualid ist (loc,qid) =
+ try (!forward_vcontext_interp ist (lookup qid))
+ with | Not_found ->
+ try VConstr (constr_of_reference (find_reference ist qid))
+ with Not_found ->
+ let (dir,id) = repr_qualid qid in
+ if dir = empty_dirpath then VIdentifier id
+ else user_err_loc (loc,"interp_pure_qualid",str "Unknown reference")
+
+let interp_ltac_reference ist = function
+ | RIdent (loc,id) ->
+ (try unrec (List.assoc id ist.lfun)
+ with | Not_found -> interp_pure_qualid ist (loc,make_short_qualid id))
+ | RQualid qid -> interp_pure_qualid ist qid
+
+(* Interprets a qualified name *)
+let eval_qualid ist (loc,qid as locqid) =
+ let dir, id = repr_qualid qid in
+ try
+ if dir = empty_dirpath then unrec (List.assoc id ist.lfun)
+ else raise Not_found
+ with | Not_found ->
+ interp_pure_qualid ist locqid
+
+let qualid_interp ist qid =
+ let v = eval_qualid ist qid in
+ coerce_to_reference ist v
+
+(* Interprets a qualified name. This can be a metavariable to be injected *)
+let qualid_or_metanum_interp ist = function
+ | AN (loc,qid) -> qid
+ | MetaNum (loc,n) -> constr_to_qid loc (List.assoc n ist.lmatch)
+
+let eval_ref_or_metanum ist = function
+ | AN (loc,qid) -> eval_qualid ist (loc,qid)
+ | MetaNum (loc,n) -> VConstr (List.assoc n ist.lmatch)
+
+let interp_evaluable_or_metanum ist c =
+ let c = eval_ref_or_metanum ist c in
+ coerce_to_evaluable_ref ist.env c
+
+let interp_inductive_or_metanum ist c =
+ let c = eval_ref_or_metanum ist c in
+ coerce_to_inductive c
+
+(* Interprets an hypothesis name *)
+let interp_hyp_location ist = function
+ | InHyp id -> InHyp (hyp_interp ist (skip_metaid id))
+ | InHypType id -> InHypType (hyp_interp ist (skip_metaid id))
+
+let id_opt_interp ist = option_app (ident_interp ist)
+
+(* Interpretation of constructions *)
+
+ (* Extracted the constr list from lfun *)
+let rec constr_list_aux ist = function
+ | (id,VConstr c)::tl -> (id,c)::(constr_list_aux ist tl)
+ | (id0,VIdentifier id)::tl ->
+ (try (id0,(constr_of_id ist id))::(constr_list_aux ist tl)
+ with | Not_found -> (constr_list_aux ist tl))
+ | _::tl -> constr_list_aux ist tl
+ | [] -> []
+
+let constr_list ist = constr_list_aux ist ist.lfun
+let interp_constr ocl ist c =
+ interp_constr_gen ist.evc ist.env (constr_list ist) ist.lmatch c ocl
+
+let interp_openconstr ist c ocl =
+ interp_openconstr_gen ist.evc ist.env (constr_list ist) ist.lmatch c ocl
+
+(* Interprets a constr expression *)
+let constr_interp ist c =
+ let csr = interp_constr None ist c in
+ begin
+ db_constr ist.debug ist.env csr;
+ csr
+ end
+
+(* Interprets a constr expression casted by the current goal *)
+let cast_constr_interp ist c =
+ match ist.goalopt with
+ | Some gl ->
+ let csr = interp_constr (Some (pf_concl gl)) ist c in
+ begin
+ db_constr ist.debug ist.env csr;
+ csr
+ end
+
+ | None ->
+ errorlabstrm "cast_constr_interp"
+ (str "Cannot cast a constr without goal")
+
+(* Interprets an open constr expression casted by the current goal *)
+let cast_openconstr_interp ist c =
+ match ist.goalopt with
+ | Some gl -> interp_openconstr ist c (Some (pf_concl gl))
+ | None ->
+ errorlabstrm "cast_openconstr_interp"
+ (str "Cannot cast a constr without goal")
+
+(* Interprets a reduction expression *)
+let unfold_interp ist (l,qid) = (l,interp_evaluable_or_metanum ist qid)
+
+let flag_interp ist red =
+ { red with rConst = List.map (interp_evaluable_or_metanum ist) red.rConst }
+
+let pattern_interp ist (l,c) = (l,constr_interp ist c)
+
+let redexp_interp ist = function
+ | Unfold l -> Unfold (List.map (unfold_interp ist) l)
+ | Fold l -> Fold (List.map (constr_interp ist) l)
+ | Cbv f -> Cbv (flag_interp ist f)
+ | Lazy f -> Lazy (flag_interp ist f)
+ | Pattern l -> Pattern (List.map (pattern_interp ist) l)
+ | (Red _ | Simpl | Hnf as r) -> r
+ | ExtraRedExpr (s,l) -> ExtraRedExpr (s,List.map (constr_interp ist) l)
+
+let interp_may_eval f ist = function
+ | ConstrEval (r,c) ->
+ let redexp = redexp_interp ist r in
+ (reduction_of_redexp redexp) ist.env ist.evc (f ist c)
+ | ConstrContext ((loc,s),c) ->
+ (try
+ let ic = f ist c
+ and ctxt = constr_of_VConstr_context (List.assoc s ist.lfun) in
+ subst_meta [-1,ic] ctxt
+ with
+ | Not_found ->
+ user_err_loc (loc, "constr_interp",
+ str "Unbound context identifier" ++ pr_id s))
+ | ConstrTypeOf c -> type_of ist.env ist.evc (f ist c)
+ | ConstrTerm c -> f ist c
+
+(* Interprets a constr expression possibly to first evaluate *)
+let constr_interp_may_eval ist c =
+ let csr = interp_may_eval (interp_constr None) ist c in
+ begin
+ db_constr ist.debug ist.env csr;
+ csr
+ end
+
+let rec interp_intro_pattern ist = function
+ | IntroOrAndPattern l ->
+ IntroOrAndPattern (List.map (List.map (interp_intro_pattern ist)) l)
+ | IntroWildcard ->
+ IntroWildcard
+ | IntroIdentifier id ->
+ IntroIdentifier (ident_interp ist id)
+
+let interp_quantified_hypothesis ist = function
+ | AnonHyp n -> AnonHyp n
+ | NamedHyp id ->
+ match eval_ident ist id with
+ | VIdentifier id -> NamedHyp id
+ | VInteger n -> AnonHyp n
+ | _ -> invalid_arg_loc
+ (loc, "Not a reference to an hypothesis: "^(string_of_id id))
+
+
+let interp_induction_arg ist = function
+ | ElimOnConstr c -> ElimOnConstr (constr_interp ist c)
+ | ElimOnAnonHyp n as x -> x
+ | ElimOnIdent (loc,id) ->
+ match ist.goalopt with
+ | None -> error "No goal"
+ | Some gl ->
+ if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+ else ElimOnConstr
+ (constr_interp ist (Termast.ast_of_qualid (make_short_qualid id)))
+
+let binding_interp ist (b,c) =
+ (interp_quantified_hypothesis ist b,constr_interp ist c)
+
+let bindings_interp ist = function
+ | NoBindings -> NoBindings
+ | ImplicitBindings l -> ImplicitBindings (List.map (constr_interp ist) l)
+ | ExplicitBindings l -> ExplicitBindings (List.map (binding_interp ist) l)
+
+let interp_constr_with_bindings ist (c,bl) =
+ (constr_interp ist c, bindings_interp ist bl)
+
+(* Interprets a tactic expression *)
+let rec val_interp ist ast =
+
+ let value_interp ist =
+ match ast with
+ (* Immediate evaluation *)
+ | TacFun (it,body) -> VFun (ist.lfun,it,body)
+ | TacFunRec rc -> funrec_interp ist rc
+ | TacLetRecIn (lrc,u) -> letrec_interp ist lrc u
+ | TacLetIn (l,u) ->
+ let addlfun=letin_interp ist l in
+ val_interp { ist with lfun=addlfun@ist.lfun } u
+ | TacMatchContext (lr,lmr) ->
+ (match ist.goalopt with
+ | None -> VContext (ist,lr,lmr)
+ | Some g -> match_context_interp ist lr lmr g)
+ | TacMatch (c,lmr) -> match_interp ist c lmr
+ | TacArg a -> tacarg_interp ist a
+ (* Delayed evaluation *)
+ | t -> VClosure (ist,t)
+ in
+ if ist.debug = DebugOn then
+ match debug_prompt ist.goalopt ast with
+ | Exit -> VClosure (ist,TacId)
+ | v -> value_interp {ist with debug=v}
+ else
+ value_interp ist
+
+and eval_tactic ist = function
+ | TacAtom (loc,t) ->
+ (try interp_atomic ist t
+ with e -> Stdpp.raise_with_loc loc e)
+ | TacFun (it,body) -> assert false
+ | TacFunRec rc -> assert false
+ | TacLetRecIn (lrc,u) -> assert false
+ | TacLetIn (l,u) -> assert false
+ | TacLetCut l -> letcut_interp ist l
+ | TacMatchContext _ -> assert false
+ | TacMatch (c,lmr) -> assert false
+ | TacId -> tclIDTAC
+ | TacFail n -> tclFAIL n
+ | TacProgress tac -> tclPROGRESS (tactic_interp ist tac)
+ | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (tactic_interp ist tac)
+ | TacThen (t1,t2) -> tclTHEN (tactic_interp ist t1) (tactic_interp ist t2)
+ | TacThens (t,tl) ->
+ tclTHENS (tactic_interp ist t) (List.map (tactic_interp ist) tl)
+ | TacDo (n,tac) -> tclDO n (tactic_interp ist tac)
+ | TacTry tac -> tclTRY (tactic_interp ist tac)
+ | TacInfo tac -> tclINFO (tactic_interp ist tac)
+ | TacRepeat tac -> tclREPEAT (tactic_interp ist tac)
+ | TacOrelse (tac1,tac2) ->
+ tclORELSE (tactic_interp ist tac1) (tactic_interp ist tac2)
+ | TacFirst l -> tclFIRST (List.map (tactic_interp ist) l)
+ | TacSolve l -> tclSOLVE (List.map (tactic_interp ist) l)
+(* Obsolete ??
+ | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
+ (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))
+ | Node(_,"PRIMTACTIC",[Node(loc,opn,[])]) ->
+ VFTactic ([],(interp_atomic opn))
+*)
+ | TacArg a -> assert false
+
+and tacarg_interp ist = function
+ | TacVoid -> VVoid
+ | Reference r -> interp_ltac_reference ist r
+ | Integer n -> VInteger n
+ | ConstrMayEval c -> VConstr (constr_interp_may_eval ist c)
+ | MetaNumArg (_,n) -> VConstr (List.assoc n ist.lmatch)
+ | MetaIdArg (loc,_) -> error_syntactic_metavariables_not_allowed loc
+(*
+ | Tacexp t -> VArg (Tacexp ((*tactic_interp ist t,*)t))
+*)
+ | TacCall (loc,f,l) ->
+ let fv = tacarg_interp ist f
+ and largs = List.map (tacarg_interp ist) l in
+ app_interp ist fv largs loc
+ | Tacexp t -> val_interp ist t
+(*
+ | Node(loc,s,l) ->
+ let fv = val_interp ist (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
+ and largs = List.map (val_interp ist) l in
+ app_interp ist fv largs ast
+*)
+ | TacDynamic(_,t) ->
+ let tg = (tag t) in
+ if tg = "tactic" then
+ let f = (tactic_out t) in val_interp ist (f ist)
+ else if tg = "value" then
+ value_out t
+ else if tg = "constr" then
+ VConstr (Pretyping.constr_out t)
+ else
+ anomaly_loc (loc, "Tacinterp.val_interp",
+ (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
+
+(* Interprets an application node *)
+and app_interp ist fv largs loc =
+ match fv with
+ | VFTactic(l,f) -> VFTactic(l@largs,f)
+ | VFun(olfun,var,body) ->
+ let (newlfun,lvar,lval)=head_with_value (var,largs) in
+ if lvar=[] then
+ if lval=[] then
+ val_interp { ist with lfun=newlfun@olfun } body
+ else
+ app_interp ist
+ (val_interp {ist with lfun=newlfun@olfun } body) lval loc
+ else
+ VFun(newlfun@olfun,lvar,body)
+ | _ ->
+ user_err_loc (loc, "Tacinterp.app_interp",
+ (str"Illegal tactic application"))
+
+(* Gives the tactic corresponding to the tactic value *)
+and tactic_of_value vle g =
+ match vle with
+ | VClosure (ist,tac) -> eval_tactic ist tac g
+ | VFTactic (largs,f) -> (f largs g)
+ | VRTactic res -> res
+ | VTactic tac -> tac g
+ | _ -> raise NotTactic
+
+(* Evaluation with FailError catching *)
+and eval_with_fail interp ast goal =
+ try
+ (match interp ast with
+ | VClosure (ist,tac) -> VRTactic (eval_tactic ist tac goal)
+ | VFTactic (largs,f) -> VRTactic (f largs goal)
+ | VTactic tac -> VRTactic (tac goal)
+ | a -> a)
+ with | FailError lvl ->
+ if lvl = 0 then
+ raise No_match
+ else
+ raise (FailError (lvl - 1))
+
+(* Interprets recursive expressions *)
+and funrec_interp ist ((loc,name),(var,body)) =
+ let ve = ref VVoid in
+ let newve = VFun((name,VRec ve)::ist.lfun,var,body) in
+ begin
+ ve:=newve;
+ !ve
+ end
+
+and letrec_interp ist lrc u =
+ let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in
+ let lenv = List.fold_right2 (fun ((loc,name),_) vref l -> (name,VRec vref)::l)
+ lrc lref [] in
+ let lve = List.map (fun ((loc,name),(var,body)) ->
+ (name,VFun(lenv@ist.lfun,var,body))) lrc in
+ begin
+ List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
+ val_interp { ist with lfun=lve@ist.lfun } u
+ end
+
+(* Interprets the clauses of a LetCutIn *)
+and letin_interp ist = function
+ | [] -> []
+ | ((loc,id),None,t)::tl -> (id,tacarg_interp ist t):: (letin_interp ist tl)
+ | ((loc,id),Some com,tce)::tl ->
+ let typ = interp_may_eval (interp_constr None) ist com
+ and tac = tacarg_interp ist tce in
+ match tac with
+ | VConstr csr ->
+ (id,VConstr (mkCast (csr,typ)))::(letin_interp ist tl)
+ | VIdentifier id ->
+ (try
+ (id,VConstr (mkCast (constr_of_id ist id,typ)))::
+ (letin_interp ist tl)
+ with | Not_found ->
+ errorlabstrm "Tacinterp.letin_interp"
+ (str "Term or tactic expected"))
+ | _ ->
+ (try
+ let t = tactic_of_value tac in
+ let ndc =
+ (match ist.goalopt with
+ | None -> Global.named_context ()
+ | Some g -> pf_hyps g) in
+ start_proof id (true,NeverDischarge) ndc typ (fun _ _ -> ());
+ by t;
+ let (_,({const_entry_body = pft; const_entry_type = _},_,_)) =
+ cook_proof () in
+ delete_proof id;
+ (id,VConstr (mkCast (pft,typ)))::(letin_interp ist tl)
+ with | NotTactic ->
+ delete_proof id;
+ errorlabstrm "Tacinterp.letin_interp"
+ (str "Term or tactic expected"))
+
+(* Interprets the clauses of a LetCut *)
+and letcut_interp ist = function
+ | [] -> tclIDTAC
+ | (id,com,tce)::tl ->
+ let typ = constr_interp_may_eval ist com
+ and tac = tacarg_interp ist tce
+ and (ndc,ccl) =
+ match ist.goalopt with
+ | None ->
+ errorlabstrm "Tacinterp.letcut_interp" (str
+ "Do not use Let for toplevel definitions, use Lemma, ... instead")
+ | Some g -> (pf_hyps g,pf_concl g) in
+ (match tac with
+ | VConstr csr ->
+ let cutt = h_cut typ
+ and exat = h_exact csr in
+ tclTHENSV cutt [|tclTHEN (introduction id)
+ (letcut_interp ist tl);exat|]
+
+(* let lic = mkLetIn (Name id,csr,typ,ccl) in
+ let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in
+ tclTHEN ntac (tclTHEN (introduction id)
+ (letcut_interp ist tl))*)
+
+ | VIdentifier ir ->
+ (try
+ let cutt = h_cut typ
+ and exat = h_exact (constr_of_id ist ir) in
+ tclTHENSV cutt [| tclTHEN (introduction id)
+ (letcut_interp ist tl); exat |]
+ with | Not_found ->
+ errorlabstrm "Tacinterp.letin_interp"
+ (str "Term or tactic expected"))
+ | _ ->
+ (try
+ let t = tactic_of_value tac in
+ start_proof id (false,NeverDischarge) ndc typ (fun _ _ -> ());
+ by t;
+ let (_,({const_entry_body = pft; const_entry_type = _},_,_)) =
+ cook_proof () in
+ delete_proof id;
+ let cutt = h_cut typ
+ and exat = h_exact pft in
+ tclTHENSV cutt [|tclTHEN (introduction id)
+ (letcut_interp ist tl);exat|]
+
+(* let lic = mkLetIn (Name id,pft,typ,ccl) in
+ let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in
+ tclTHEN ntac (tclTHEN (introduction id)
+ (letcut_interp ist tl))*)
+ with | NotTactic ->
+ delete_proof id;
+ errorlabstrm "Tacinterp.letcut_interp"
+ (str "Term or tactic expected")))
+
+(* Interprets the Match Context expressions *)
+and match_context_interp ist lr lmr g =
+(* let goal =
+ (match goalopt with
+ | None ->
+ errorlabstrm "Tacinterp.apply_match_context" (str
+ "No goal available")
+ | Some g -> g) in*)
+ let rec apply_goal_sub ist goal nocc (id,c) csr mt mhyps hyps =
+ try
+ let (lgoal,ctxt) = sub_match nocc c csr in
+ let lctxt = give_context ctxt id in
+ if mhyps = [] then
+ eval_with_fail
+ (val_interp
+ { ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch;
+ goalopt=Some goal})
+ mt goal
+ else
+ apply_hyps_context {ist with goalopt=Some goal} mt lgoal mhyps hyps
+ with
+ | (FailError _) as e -> raise e
+ | NextOccurrence _ -> raise No_match
+ | No_match | _ ->
+ apply_goal_sub ist goal (nocc + 1) (id,c) csr mt mhyps hyps in
+ let rec apply_match_context ist goal = function
+ | (All t)::tl ->
+ (try
+ eval_with_fail (val_interp {ist with goalopt=Some goal }) t
+ goal
+ with No_match | FailError _ -> apply_match_context ist goal tl
+ | e when Logic.catchable_exception e -> apply_match_context ist goal tl)
+ | (Pat (mhyps,mgoal,mt))::tl ->
+ let hyps = make_hyps (pf_hyps goal) in
+ let hyps = if lr then List.rev hyps else hyps in
+ let concl = pf_concl goal in
+ (match mgoal with
+ | Term mg ->
+ (try
+ (let lgoal = apply_matching mg concl in
+ begin
+ db_matched_concl ist.debug ist.env concl;
+ if mhyps = [] then
+ eval_with_fail (val_interp
+ {ist with lmatch=lgoal@ist.lmatch; goalopt=Some goal}) mt goal
+ else
+ apply_hyps_context { ist with goalopt=Some goal} mt lgoal mhyps
+ hyps
+ end)
+ with e when is_match_catchable e -> apply_match_context ist goal tl)
+ | Subterm (id,mg) ->
+ (try
+ apply_goal_sub ist goal 0 (id,mg) concl mt mhyps hyps
+ with e when is_match_catchable e ->
+ apply_match_context ist goal tl))
+ | _ ->
+ errorlabstrm "Tacinterp.apply_match_context" (str
+ "No matching clauses for Match Context")
+
+ in
+ apply_match_context ist g
+ (read_match_rule ist.evc ist.env (constr_list ist) lmr)
+
+(* Interprets a VContext value *)
+and vcontext_interp ist = function
+ | (VContext (ist',lr,lmr)) as v ->
+ (match ist.goalopt with
+ | None -> v
+ | Some g -> (* Relaunch *) match_context_interp ist' lr lmr g)
+ | v -> v
+
+(* Tries to match the hypotheses in a Match Context *)
+and apply_hyps_context ist mt lgmatch mhyps hyps =
+ let rec apply_hyps_context_rec ist mt lfun lmatch mhyps lhyps_mhyp
+ lhyps_rest noccopt =
+ let goal = match ist.goalopt with Some g -> g | _ -> assert false in
+ match mhyps with
+ | hd::tl ->
+ let (lid,lc,lm,newlhyps,hyp_match,noccopt) =
+ apply_one_mhyp_context ist lmatch hd lhyps_mhyp noccopt in
+ begin
+ db_matched_hyp ist.debug ist.env hyp_match;
+ (try
+ if tl = [] then
+ eval_with_fail
+ (val_interp {ist with lfun=lfun@lid@lc@ist.lfun;
+ lmatch=lmatch@lm@ist.lmatch;
+ goalopt=Some goal})
+ mt goal
+ else
+ let nextlhyps =
+ List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) []
+ lhyps_rest in
+ apply_hyps_context_rec ist mt
+ (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
+ with
+ | (FailError _) as e -> raise e
+ | e when is_match_catchable e ->
+ (match noccopt with
+ | None ->
+ apply_hyps_context_rec ist mt lfun
+ lmatch mhyps newlhyps lhyps_rest None
+ | Some nocc ->
+ apply_hyps_context_rec ist mt ist.lfun ist.lmatch mhyps
+ (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1))))
+ end
+ | [] ->
+ anomalylabstrm "apply_hyps_context_rec" (str
+ "Empty list should not occur") in
+ apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None
+
+ (* Interprets extended tactic generic arguments *)
+and genarg_interp ist x =
+ match genarg_tag x with
+ | BoolArgType -> in_gen wit_bool (out_gen rawwit_bool x)
+ | IntArgType -> in_gen wit_int (out_gen rawwit_int x)
+ | IntOrVarArgType ->
+ let f = function
+ | ArgVar (loc,id) ->
+ (match eval_ident ist id with
+ | VInteger n -> ArgArg n
+ | _ ->
+ user_err_loc
+ (loc,"genarg_interp",str "should be bound to an integer"))
+ | ArgArg n as x -> x in
+ in_gen wit_int_or_var (f (out_gen rawwit_int_or_var x))
+ | StringArgType ->
+ in_gen wit_string (out_gen rawwit_string x)
+ | PreIdentArgType ->
+ in_gen wit_pre_ident (out_gen rawwit_pre_ident x)
+ | IdentArgType ->
+ in_gen wit_ident (ident_interp ist (out_gen rawwit_ident x))
+ | QualidArgType ->
+ in_gen wit_qualid (qualid_interp ist (out_gen rawwit_qualid x))
+ | ConstrArgType ->
+ in_gen wit_constr (constr_interp ist (out_gen rawwit_constr x))
+ | ConstrMayEvalArgType ->
+ in_gen wit_constr_may_eval (constr_interp_may_eval ist (out_gen rawwit_constr_may_eval x))
+ | QuantHypArgType ->
+ in_gen wit_quant_hyp
+ (interp_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
+ | RedExprArgType ->
+ in_gen wit_red_expr (redexp_interp ist (out_gen rawwit_red_expr x))
+ | TacticArgType ->
+ in_gen wit_tactic ((*tactic_interp ist*) (out_gen rawwit_tactic x))
+ | CastedOpenConstrArgType ->
+ in_gen wit_casted_open_constr
+ (cast_openconstr_interp ist (out_gen rawwit_casted_open_constr x))
+ | ConstrWithBindingsArgType ->
+ in_gen wit_constr_with_bindings
+ (interp_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
+ | List0ArgType _ -> app_list0 (genarg_interp ist) x
+ | List1ArgType _ -> app_list1 (genarg_interp ist) x
+ | OptArgType _ -> app_opt (genarg_interp ist) x
+ | PairArgType _ -> app_pair (genarg_interp ist) (genarg_interp ist) x
+ | ExtraArgType s -> lookup_genarg_interp s ist x
+
+(* Interprets the Match expressions *)
+and match_interp ist constr lmr =
+ let rec apply_sub_match ist nocc (id,c) csr
+ mt =
+ match ist.goalopt with
+ | None ->
+ (try
+ let (lm,ctxt) = sub_match nocc c csr in
+ let lctxt = give_context ctxt id in
+ val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch} mt
+ with | NextOccurrence _ -> raise No_match)
+ | Some g ->
+ (try
+ let (lm,ctxt) = sub_match nocc c csr in
+ let lctxt = give_context ctxt id in
+ eval_with_fail (val_interp { ist with lfun=lctxt@ist.lfun;
+ lmatch=lm@ist.lmatch})
+ mt g
+ with
+ | NextOccurrence n -> raise No_match
+ | (FailError _) as e -> raise e
+ | e when is_match_catchable e ->
+ apply_sub_match ist (nocc + 1) (id,c) csr mt)
+ in
+ let rec apply_match ist csr = function
+ | (All t)::_ ->
+ (match ist.goalopt with
+ | None ->
+ (try val_interp ist t
+ with e when is_match_catchable e -> apply_match ist csr [])
+ | Some g ->
+ (try
+ eval_with_fail (val_interp ist) t g
+ with
+ | (FailError _) as e -> raise e
+ | e when is_match_catchable e ->
+ apply_match ist csr []))
+ | (Pat ([],mp,mt))::tl ->
+ (match mp with
+ | Term c ->
+ (match ist.goalopt with
+ | None ->
+ (try
+ val_interp
+ { ist with lmatch=(apply_matching c csr)@ist.lmatch } mt
+ with e when is_match_catchable e -> apply_match ist csr tl)
+ | Some g ->
+ (try
+ eval_with_fail (val_interp
+ { ist with lmatch=(apply_matching c csr)@ist.lmatch }) mt g
+ with
+ | (FailError _) as e -> raise e
+ | e when is_match_catchable e ->
+ apply_match ist csr tl))
+ | Subterm (id,c) ->
+ (try
+ apply_sub_match ist 0 (id,c) csr mt
+ with | No_match ->
+ apply_match ist csr tl))
+ | _ ->
+ errorlabstrm "Tacinterp.apply_match" (str
+ "No matching clauses for Match") in
+ let csr = constr_interp_may_eval ist constr
+ and ilr = read_match_rule ist.evc ist.env (constr_list ist) lmr in
+ apply_match ist csr ilr
+
+and tactic_interp ist (ast:raw_tactic_expr) g =
+ tac_interp ist.lfun ist.lmatch ist.debug ast g
+
+(* Interprets tactic expressions *)
+and tac_interp lfun lmatch debug ast g =
+ let evc = project g
+ and env = pf_env g in
+ let ist = { evc=evc; env=env; lfun=lfun; lmatch=lmatch;
+ goalopt=Some g; debug=debug } in
+ try tactic_of_value (val_interp ist ast) g
+ with | NotTactic ->
+ errorlabstrm "Tacinterp.tac_interp" (str
+ "Must be a command or must give a tactic value")
+
+(* errorlabstrm "Tacinterp.tac_interp" (str
+ "Interpretation gives a non-tactic value") *)
+
+(* match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with
+ | VClosure tac -> (tac g)
+ | VFTactic (largs,f) -> (f largs g)
+ | VRTactic res -> res
+ | _ ->
+ errorlabstrm "Tacinterp.tac_interp" (str
+ "Interpretation gives a non-tactic value")*)
+
+(* Interprets a primitive tactic *)
+and interp_atomic ist = function
+ (* Basic tactics *)
+ | TacIntroPattern l ->
+ Elim.h_intro_patterns (List.map (interp_intro_pattern ist) l)
+ | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp)
+ | TacIntroMove (ido,ido') ->
+ h_intro_move (option_app (ident_interp ist) ido)
+ (option_app (fun x -> ident_interp ist (snd x)) ido')
+ | TacAssumption -> h_assumption
+ | TacExact c -> h_exact (cast_constr_interp ist c)
+ | TacApply cb -> h_apply (interp_constr_with_bindings ist cb)
+ | TacElim (cb,cbo) ->
+ h_elim (interp_constr_with_bindings ist cb)
+ (option_app (interp_constr_with_bindings ist) cbo)
+ | TacElimType c -> h_elim_type (constr_interp ist c)
+ | TacCase cb -> h_case (interp_constr_with_bindings ist cb)
+ | TacCaseType c -> h_case_type (constr_interp ist c)
+ | TacFix (idopt,n) -> h_fix (id_opt_interp ist idopt) n
+ | TacMutualFix (id,n,l) ->
+ let f (id,n,c) = (ident_interp ist id,n,constr_interp ist c) in
+ h_mutual_fix (ident_interp ist id) n (List.map f l)
+ | TacCofix idopt -> h_cofix (id_opt_interp ist idopt)
+ | TacMutualCofix (id,l) ->
+ let f (id,c) = (ident_interp ist id,constr_interp ist c) in
+ h_mutual_cofix (ident_interp ist id) (List.map f l)
+ | TacCut c -> h_cut (constr_interp ist c)
+ | TacTrueCut (ido,c) -> h_true_cut (id_opt_interp ist ido) (constr_interp ist c)
+ | TacForward (b,na,c) -> h_forward b (name_interp ist na) (constr_interp ist c)
+ | TacGeneralize cl -> h_generalize (List.map (constr_interp ist) cl)
+ | TacGeneralizeDep c -> h_generalize_dep (constr_interp ist c)
+ | TacLetTac (id,c,clp) ->
+ let clp = check_clause_pattern ist clp in
+ h_let_tac (ident_interp ist id) (constr_interp ist c) clp
+ | TacInstantiate (n,c) -> h_instantiate n (constr_interp ist c)
+
+ (* Automation tactics *)
+ | TacTrivial l -> Auto.h_trivial l
+ | TacAuto (n, l) -> Auto.h_auto n l
+ | TacAutoTDB n -> Dhyp.h_auto_tdb n
+ | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (hyp_interp ist id)
+ | TacDestructConcl -> Dhyp.h_destructConcl
+ | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
+ | TacDAuto (n,p) -> Auto.h_dauto (n,p)
+
+ (* Derived basic tactics *)
+ | TacOldInduction h -> h_old_induction (interp_quantified_hypothesis ist h)
+ | TacNewInduction c -> h_new_induction (interp_induction_arg ist c)
+ | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist h)
+ | TacNewDestruct c -> h_new_destruct (interp_induction_arg ist c)
+ | TacDoubleInduction (h1,h2) ->
+ let h1 = interp_quantified_hypothesis ist h1 in
+ let h2 = interp_quantified_hypothesis ist h2 in
+ Elim.h_double_induction h1 h2
+ | TacDecomposeAnd c -> Elim.h_decompose_and (constr_interp ist c)
+ | TacDecomposeOr c -> Elim.h_decompose_or (constr_interp ist c)
+ | TacDecompose (l,c) ->
+ let l = List.map (interp_inductive_or_metanum ist) l in
+ Elim.h_decompose l (constr_interp ist c)
+ | TacSpecialize (n,l) -> h_specialize n (interp_constr_with_bindings ist l)
+ | TacLApply c -> h_lapply (constr_interp ist c)
+
+ (* Context management *)
+ | TacClear l -> h_clear (List.map (hyp_or_metanum_interp ist) l)
+ | TacClearBody l -> h_clear_body (List.map (hyp_or_metanum_interp ist) l)
+ | TacMove (dep,id1,id2) ->
+ h_move dep (hyp_interp ist id1) (hyp_interp ist id2)
+ | TacRename (id1,id2) ->
+ h_rename (hyp_interp ist id1) (hyp_interp ist id2)
+
+ (* Constructors *)
+ | TacLeft bl -> h_left (bindings_interp ist bl)
+ | TacRight bl -> h_right (bindings_interp ist bl)
+ | TacSplit bl -> h_split (bindings_interp ist bl)
+ | TacAnyConstructor t ->
+ abstract_tactic (TacAnyConstructor t)
+ (Tactics.any_constructor (option_app (tactic_interp ist) t))
+ | TacConstructor (n,bl) ->
+ h_constructor (skip_metaid n) (bindings_interp ist bl)
+
+ (* Conversion *)
+ | TacReduce (r,cl) ->
+ h_reduce (redexp_interp ist r) (List.map (interp_hyp_location ist) cl)
+ | TacChange (c,cl) ->
+ h_change (constr_interp ist c) (List.map (interp_hyp_location ist) cl)
+
+ (* Equivalence relations *)
+ | TacReflexivity -> h_reflexivity
+ | TacSymmetry -> h_symmetry
+ | TacTransitivity c -> h_transitivity (constr_interp ist c)
+
+ (* For extensions *)
+ | TacExtend (opn,l) -> vernac_tactic (opn,List.map (genarg_interp ist) l)
+ | TacAlias (_,l,body) ->
+ let f x = match genarg_tag x with
+ | IdentArgType -> VIdentifier (ident_interp ist (out_gen rawwit_ident x))
+ | QualidArgType -> VConstr (constr_of_reference (qualid_interp ist (out_gen rawwit_qualid x)))
+ | ConstrArgType -> VConstr (constr_interp ist (out_gen rawwit_constr x))
+ | ConstrMayEvalArgType ->
+ VConstr (constr_interp_may_eval ist (out_gen rawwit_constr_may_eval x))
+ | _ -> failwith "This generic type is not supported in alias" in
+
+ tactic_of_value (val_interp { ist with lfun=(List.map (fun (x,c) -> (id_of_string x,f c)) l)@ist.lfun } body)
+
+let _ = forward_vcontext_interp := vcontext_interp
+
+(* Interprets tactic arguments *)
+let interp_tacarg sign ast = (*unvarg*) (val_interp sign ast)
+
+(* Initial call for interpretation *)
+let interp = fun ast -> tac_interp [] [] !debug ast
+
+(* Hides interpretation for pretty-print *)
+let hide_interp t = abstract_tactic_expr (TacArg (Tacexp t)) (interp t)
+
+(* For bad tactic calls *)
+let bad_tactic_args s =
+ anomalylabstrm s
+ (str "Tactic " ++ str s ++ str " called with bad arguments")
+
+(* Declaration of the TAC-DEFINITION object *)
+let add (sp,td) = mactab := Gmap.add sp td !mactab
+
+let register_tacdef (sp,td) =
+ let ve = val_interp
+ {evc=Evd.empty;env=Global.env ();lfun=[];
+ lmatch=[]; goalopt=None; debug=get_debug ()}
+ td in
+ sp,ve
+
+let cache_md (_,defs) =
+ (* Needs a rollback if something goes wrong *)
+ List.iter (fun (sp,_) -> Nametab.push_tactic_path sp) defs;
+ List.iter add (List.map register_tacdef defs)
+
+let (inMD,outMD) =
+ declare_object ("TAC-DEFINITION",
+ {cache_function = cache_md;
+ load_function = (fun _ -> ());
+ open_function = cache_md;
+ export_function = (fun x -> Some x)})
+
+(* Adds a definition for tactics in the table *)
+let make_absolute_name (loc,id) =
+ let sp = Lib.make_path id in
+ if Gmap.mem sp !mactab then
+ errorlabstrm "Tacinterp.add_tacdef"
+ (str "There is already a Meta Definition or a Tactic Definition named "
+ ++ pr_sp sp);
+ sp
+
+let add_tacdef tacl =
+ let lfun = List.map (fun ((loc,id),_) -> id) tacl in
+ let tacl = List.map (fun (id,tac) -> (make_absolute_name id,tac)) tacl in
+ List.iter (fun (_,def) -> let _ = glob_tactic (lfun,[]) def in ()) tacl;
+ let _ = Lib.add_leaf (List.hd lfun) (inMD tacl) in
+ List.iter
+ (fun id -> Options.if_verbose msgnl (pr_id id ++ str " is defined")) lfun
+
+let interp_redexp env evc r =
+ let ist =
+ { evc=evc; env=env; lfun=[]; lmatch=[]; goalopt=None; debug=get_debug ()}
+ in
+ redexp_interp ist r
+
+let _ = Auto.set_extern_interp (fun l -> tac_interp [] l (get_debug()))
+let _ = Dhyp.set_extern_interp interp
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
new file mode 100644
index 0000000000..c4017fc889
--- /dev/null
+++ b/tactics/tacinterp.mli
@@ -0,0 +1,115 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Dyn
+open Pp
+open Names
+open Proof_type
+open Tacmach
+open Tactic_debug
+open Term
+open Tacexpr
+open Genarg
+(*i*)
+
+(* Values for interpretation *)
+type value =
+ | VClosure of interp_sign * raw_tactic_expr
+ | VTactic of tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *)
+ | VFTactic of value list * (value list->tactic)
+ | VRTactic of (goal list sigma * validation)
+ | VContext of interp_sign * direction_flag
+ * (pattern_ast,raw_tactic_expr) match_rule list
+ | VFun of (identifier * value) list * identifier option list *raw_tactic_expr
+ | VVoid
+ | VInteger of int
+ | VIdentifier of identifier
+ | VConstr of constr
+ | VConstr_context of constr
+ | VRec of value ref
+
+(* Signature for interpretation: val\_interp and interpretation functions *)
+and interp_sign =
+ { evc : Evd.evar_map;
+ env : Environ.env;
+ lfun : (identifier * value) list;
+ lmatch : (int * constr) list;
+ goalopt : goal sigma option;
+ debug : debug_info }
+
+(* Gives the identifier corresponding to an Identifier [tactic_arg] *)
+val id_of_Identifier : value -> identifier
+
+(* Gives the constr corresponding to a Constr [value] *)
+val constr_of_VConstr : value -> constr
+
+(* Transforms an id into a constr if possible *)
+val constr_of_id : interp_sign -> identifier -> constr
+
+(* To embed several objects in Coqast.t *)
+val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
+val tacticOut : raw_tactic_expr -> (interp_sign -> raw_tactic_expr)
+val valueIn : value -> raw_tactic_arg
+val valueOut: raw_tactic_arg -> value
+val constrIn : constr -> Coqast.t
+val constrOut : Coqast.t -> constr
+val loc : Coqast.loc
+
+(* Sets the debugger mode *)
+val set_debug : debug_info -> unit
+
+(* Gives the state of debug *)
+val get_debug : unit -> debug_info
+
+(* Adds a definition for tactics in the table *)
+val add_tacdef : (identifier Util.located * raw_tactic_expr) list -> unit
+
+(* Adds an interpretation function for extra generic arguments *)
+val add_genarg_interp :
+ string ->
+ (interp_sign -> raw_generic_argument -> closed_generic_argument) -> unit
+
+val genarg_interp :
+ interp_sign -> raw_generic_argument -> closed_generic_argument
+
+(* Interprets any expression *)
+val val_interp : interp_sign -> raw_tactic_expr -> value
+
+(*
+(* Interprets tactic arguments *)
+val interp_tacarg : interp_sign -> raw_tactic_expr -> value
+*)
+
+(* Interprets redexp arguments *)
+val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr
+ -> Tacred.red_expr
+
+(* Interprets tactic expressions *)
+val tac_interp : (identifier * value) list -> (int * constr) list ->
+ debug_info -> raw_tactic_expr -> tactic
+
+(* Interprets constr expressions *)
+val constr_interp : interp_sign -> constr_ast -> constr
+
+(* Initial call for interpretation *)
+val interp : raw_tactic_expr -> tactic
+
+(* Hides interpretation for pretty-print *)
+val hide_interp : raw_tactic_expr -> tactic
+
+(* Adds an interpretation function *)
+val interp_add : string * (interp_sign -> Coqast.t -> value) -> unit
+
+(* Adds a possible existing interpretation function *)
+val overwriting_interp_add : string * (interp_sign -> Coqast.t -> value) ->
+ unit
+
+
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2285850c00..f154ef3723 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -24,16 +24,19 @@ open Declare
open Evd
open Pfedit
open Tacred
+open Rawterm
open Tacmach
open Proof_trees
open Proof_type
open Logic
open Evar_refiner
open Clenv
+open Refiner
open Tacticals
open Hipattern
open Coqlib
open Nametab
+open Tacexpr
exception Bound
@@ -54,12 +57,14 @@ let rec nb_prod x =
(* General functions *)
(****************************************)
+(*
let get_pairs_from_bindings =
let pair_from_binding = function
| [(Bindings binds)] -> binds
| _ -> error "not a binding list!"
in
List.map pair_from_binding
+*)
let string_of_inductive c =
try match kind_of_term c with
@@ -85,8 +90,10 @@ let rec head_constr_bound t l =
let head_constr c =
try head_constr_bound c [] with Bound -> error "Bound head variable"
+(*
let bad_tactic_args s l =
raise (RefinerError (BadTacticArgs (s,l)))
+*)
(******************************************)
(* Primitive tactics *)
@@ -100,54 +107,27 @@ let refine = Tacmach.refine
let convert_concl = Tacmach.convert_concl
let convert_hyp = Tacmach.convert_hyp
let thin = Tacmach.thin
-let thin_body = Tacmach.thin_body
-let move_hyp = Tacmach.move_hyp
+let thin_body = Tacmach.thin_body
+
+(* Moving hypotheses *)
+let move_hyp = Tacmach.move_hyp
+
+(* Renaming hypotheses *)
let rename_hyp = Tacmach.rename_hyp
-let mutual_fix = Tacmach.mutual_fix
-let fix f n = mutual_fix f n []
-
-let fix_noname n =
- let id = Pfedit.get_current_proof_name () in
- fix id n
-
-let dyn_mutual_fix argsl gl =
- match argsl with
- | [Integer n] -> fix_noname n gl
- | [Identifier id;Integer n] -> fix id n gl
- | ((Identifier id)::(Integer n)::lfix) ->
- let rec decomp lar = function
- | (Fixexp (id,n,ar)::rest) ->
- decomp ((id,n,pf_interp_constr gl ar)::lar) rest
- | [] -> (List.rev lar)
- | _ -> bad_tactic_args "mutual_fix" argsl
- in
- let lar = decomp [] lfix in
- mutual_fix id n lar gl
- | l -> bad_tactic_args "mutual_fix" l
+(* Refine as a fixpoint *)
+let mutual_fix = Tacmach.mutual_fix
+let fix ido n = match ido with
+ | None -> mutual_fix (Pfedit.get_current_proof_name ()) n []
+ | Some id -> mutual_fix id n []
+
+(* Refine as a cofixpoint *)
let mutual_cofix = Tacmach.mutual_cofix
-let cofix f = mutual_cofix f []
-
-let cofix_noname n =
- let id = Pfedit.get_current_proof_name () in
- cofix id n
-
-let dyn_mutual_cofix argsl gl =
- match argsl with
- | [] -> cofix_noname gl
- | [(Identifier id)] -> cofix id gl
- | ((Identifier id)::lcofix) ->
- let rec decomp lar = function
- | (Cofixexp (id,ar)::rest) ->
- decomp ((id,pf_interp_constr gl ar)::lar) rest
- | [] -> List.rev lar
- | _ -> bad_tactic_args "mutual_cofix" argsl
- in
- let lar = decomp [] lcofix in
- mutual_cofix id lar gl
- | l -> bad_tactic_args "mutual_cofix" l
+let cofix = function
+ | None -> mutual_cofix (Pfedit.get_current_proof_name ()) []
+ | Some id -> mutual_cofix id []
(**************************************************************)
(* Reduction and conversion tactics *)
@@ -213,7 +193,7 @@ let change_option t = function
| Some id -> reduct_in_hyp (change_hyp_and_check t) id
| None -> reduct_in_concl (change_concl_and_check t)
-(* Pour usage interne (le niveau User est pris en compte par dyn_reduce) *)
+(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl red_product
let red_in_hyp = reduct_in_hyp red_product
let red_option = reduct_option red_product
@@ -231,12 +211,7 @@ let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
let unfold_option loccname = reduct_option (unfoldn loccname)
let pattern_option l = reduct_option (pattern_occs l)
-let dyn_change = function
- | [Constr c; Clause cl] ->
- (fun goal ->
-(* let c = Astterm.interp_type (project goal) (pf_env goal) com in*)
- in_combinator (change_in_concl c) (change_in_hyp c) cl goal)
- | l -> bad_tactic_args "change" l
+let change c = in_combinator (change_in_concl c) (change_in_hyp c)
(* A function which reduces accordingly to a reduction expression,
as the command Eval does. *)
@@ -244,10 +219,6 @@ let dyn_change = function
let reduce redexp cl goal =
redin_combinator (reduction_of_redexp redexp) cl goal
-let dyn_reduce = function
- | [Redexp redexp; Clause cl] -> (fun goal -> reduce redexp cl goal)
- | l -> bad_tactic_args "reduce" l
-
(* Unfolding occurrences of a constant *)
let unfold_constr = function
@@ -360,93 +331,59 @@ let intros_replacing ids gls =
(* User-level introduction tactics *)
-let dyn_intro = function
- | [] -> intro_gen (IntroAvoid []) None true
- | [Identifier id] -> intro_gen (IntroMustBe id) None true
- | l -> bad_tactic_args "intro" l
-
-let dyn_intro_move = function
- | [Identifier id2] -> intro_gen (IntroAvoid []) (Some id2) true
- | [Identifier id; Identifier id2] ->
- intro_gen (IntroMustBe id) (Some id2) true
- | l -> bad_tactic_args "intro_move" l
-
-let rec intros_until s g =
- match pf_lookup_name_as_renamed (pf_env g) (pf_concl g) s with
- | Some depth -> tclDO depth intro g
- | None ->
- try
- ((tclTHEN (reduce (Red true) []) (intros_until s)) g)
- with Redelimination ->
- errorlabstrm "Intros"
- (str ("No hypothesis "^(string_of_id s)^" in current goal") ++
- str " even after head-reduction")
-
-let rec intros_until_n_gen red n g =
- match pf_lookup_index_as_renamed (pf_env g) (pf_concl g) n with
- | Some depth -> tclDO depth intro g
+let intro_move idopt idopt' = match idopt with
+ | None -> intro_gen (IntroAvoid []) idopt' true
+ | Some id -> intro_gen (IntroMustBe id) idopt' true
+
+let pf_lookup_hypothesis_as_renamed env ccl = function
+ | AnonHyp n -> pf_lookup_index_as_renamed env ccl n
+ | NamedHyp id -> pf_lookup_name_as_renamed env ccl id
+
+let pf_lookup_hypothesis_as_renamed_gen red h gl =
+ let env = pf_env gl in
+ let rec aux ccl =
+ match pf_lookup_hypothesis_as_renamed env ccl h with
+ | None when red -> aux (reduction_of_redexp (Red true) env Evd.empty ccl)
+ | x -> x
+ in
+ try aux (pf_concl gl)
+ with Redelimination -> None
+
+let is_quantified_hypothesis id g =
+ match pf_lookup_hypothesis_as_renamed_gen true (NamedHyp id) g with
+ | Some _ -> true
+ | None -> false
+
+let msg_quantified_hypothesis = function
+ | NamedHyp id ->
+ str "hypothesis " ++ pr_id id
+ | AnonHyp n ->
+ int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
+ str " non dependent hypothesis"
+
+let depth_of_quantified_hypothesis red h gl =
+ match pf_lookup_hypothesis_as_renamed_gen red h gl with
+ | Some depth -> depth
| None ->
- if red then
- try
- ((tclTHEN (reduce (Red true) []) (intros_until_n_gen red n)) g)
- with Redelimination ->
- errorlabstrm "Intros"
- (str ("No "^(string_of_int n)) ++
- str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
- str " non dependent hypothesis in current goal" ++
- str " even after head-reduction")
- else
- errorlabstrm "Intros" (str "No such hypothesis in current goal")
+ errorlabstrm "lookup_quantified_hypothesis"
+ (str "No " ++ msg_quantified_hypothesis h ++
+ str " in current goal" ++
+ if red then str " even after head-reduction" else mt ())
+
+let intros_until_gen red h g =
+ tclDO (depth_of_quantified_hypothesis red h g) intro g
+let intros_until_id id = intros_until_gen true (NamedHyp id)
+let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
+
+let intros_until = intros_until_gen true
let intros_until_n = intros_until_n_gen true
let intros_until_n_wored = intros_until_n_gen false
-let dyn_intros_until = function
- | [Identifier id] -> intros_until id
- | [Integer n] -> intros_until_n n
- | l -> bad_tactic_args "Intros until" l
-
-let tactic_try_intros_until tac = function
- | Identifier id ->
- tclTHEN (tclTRY (intros_until id)) (tac id)
- | Integer n ->
- tclTHEN (intros_until_n n)
- (fun gl -> let id,_,_ = pf_last_hyp gl in tac id gl)
- | c -> bad_tactic_args "tactic_try_intros_until" [c]
-
-let hide_ident_or_numarg_tactic s tac =
- let tacfun = function
- | [Identifier id] -> tclTHEN (tclTRY (intros_until id)) (tac id)
- | [Integer n] ->
- tclTHEN (intros_until_n n)
- (fun gl -> let id,_,_ = pf_last_hyp gl in tac id gl)
- | _ -> assert false in
- add_tactic s tacfun;
- fun id -> vernac_tactic(s,[Identifier id])
-
-
-(* Obsolete, remplace par intros_unitl_n ?
-let intros_do n g =
- let depth =
- let rec lookup all nodep c = match kind_of_term c with
- | Prod (name,_,c') ->
- (match name with
- | Name(s') ->
- if dependent (mkRel 1) c' then
- lookup (all+1) nodep c'
- else if nodep = n then
- all
- else
- lookup (all+1) (nodep+1) c'
- | Anonymous ->
- if nodep=n then all else lookup (all+1) (nodep+1) c')
- | Cast (c,_) -> lookup all nodep c
- | _ -> error "No such hypothesis in current goal"
- in
- lookup 1 1 (pf_concl g)
- in
- tclDO depth intro g
-*)
+let try_intros_until tac = function
+ | NamedHyp id -> tclTHEN (tclTRY (intros_until_id id)) (tac id)
+ | AnonHyp n -> tclTHEN (intros_until_n n) (onLastHyp tac)
+
let rec intros_move = function
| [] -> tclIDTAC
| (hyp,destopt) :: rest ->
@@ -508,8 +445,7 @@ let bring_hyps hyps =
(* Resolution with missing arguments *)
-
-let apply_with_bindings (c,lbind) gl =
+let apply_with_bindings (c,lbind) gl =
let apply =
match kind_of_term c with
| Lambda _ -> res_pf_cast
@@ -539,11 +475,11 @@ let apply_with_bindings (c,lbind) gl =
apply kONT clause gl
-let apply c = apply_with_bindings (c,[])
-let apply_com = tactic_com (fun c -> apply_with_bindings (c,[]))
+let apply c = apply_with_bindings (c,NoBindings)
+let apply_com = tactic_com (fun c -> apply_with_bindings (c,NoBindings))
let apply_list = function
- | c::l -> apply_with_bindings (c,List.map (fun com ->(Com,com)) l)
+ | c::l -> apply_with_bindings (c,ImplicitBindings l)
| _ -> assert false
(* Resolution with no reduction on the type *)
@@ -557,85 +493,68 @@ let apply_without_reduce_com = tactic_com apply_without_reduce
let refinew_scheme kONT clause gl = res_pf kONT clause gl
-let dyn_apply l =
- match l with
- | [Command com; Bindings binds] ->
- tactic_com_bind_list apply_with_bindings (com,binds)
- | [Constr c; Cbindings binds] ->
- apply_with_bindings (c,binds)
- | l ->
- bad_tactic_args "apply" l
+(* A useful resolution tactic which, if c:A->B, transforms |- C into
+ |- B -> C and |- A (which is realized by Cut B;[Idtac|Apply c]
-(* A useful resolution tactic, equivalent to Cut type_of_c;[Idtac|Apply c] *)
+ -------------------
+ Gamma |- c : A -> B Gamma |- ?2 : A
+ ----------------------------------------
+ Gamma |- B Gamma |- ?1 : B -> C
+ -----------------------------------------------------
+ Gamma |- ? : C
+ *)
let cut_and_apply c gl =
let goal_constr = pf_concl gl in
match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
| Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
- tclTHENS
- (apply_type (mkProd (Anonymous,c2,goal_constr))
- [mkMeta (new_meta())])
- [tclIDTAC;apply_term c [mkMeta (new_meta())]] gl
+ tclTHENLAST
+ (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
+ (apply_term c [mkMeta (new_meta())]) gl
| _ -> error "Imp_elim needs a non-dependent product"
-let dyn_cut_and_apply = function
- | [Command com] -> tactic_com cut_and_apply com
- | [Constr c] -> cut_and_apply c
- | l -> bad_tactic_args "cut_and_apply" l
-
(**************************)
(* Cut tactics *)
(**************************)
-let true_cut id c gl =
- match kind_of_term (hnf_type_of gl c) with
- | Sort _ -> internal_cut id c gl
- | _ -> error "Not a proposition or a type"
-
-let true_cut_anon c gl =
+let true_cut idopt c gl =
match kind_of_term (hnf_type_of gl c) with
| Sort s ->
- let d = match s with Prop _ -> "H" | Type _ -> "X" in
- let id = next_name_away_with_default d Anonymous (pf_ids_of_hyps gl) in
- internal_cut id c gl
+ let id =
+ match idopt with
+ | None ->
+ let d = match s with Prop _ -> "H" | Type _ -> "X" in
+ next_name_away_with_default d Anonymous (pf_ids_of_hyps gl)
+ | Some id -> id
+ in
+ internal_cut id c gl
| _ -> error "Not a proposition or a type"
-let dyn_true_cut = function
- | [Command com] -> tactic_com_sort true_cut_anon com
- | [Constr c] -> true_cut_anon c
- | [Command com; Identifier id] -> tactic_com_sort (true_cut id) com
- | [Constr c; Identifier id] -> true_cut id c
- | l -> bad_tactic_args "true_cut" l
-
let cut c gl =
match kind_of_term (hnf_type_of gl c) with
| Sort _ ->
let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
let t = mkProd (Anonymous, c, pf_concl gl) in
- tclTHENS
+ tclTHENFIRST
(internal_cut_rev id c)
- [tclTHEN (apply_type t [mkVar id]) (thin [id]);
- tclIDTAC] gl
+ (tclTHEN (apply_type t [mkVar id]) (thin [id]))
+ gl
| _ -> error "Not a proposition or a type"
-let dyn_cut = function
- | [Command com] -> tactic_com_sort cut com
- | [Constr c] -> cut c
- | l -> bad_tactic_args "cut" l
-
-let cut_intro t = (tclTHENS (cut t) [intro;tclIDTAC])
+let cut_intro t = tclTHENFIRST (cut t) intro
let cut_replacing id t =
- (tclTHENS (cut t)
- [(tclORELSE (intro_replacing id)
- (tclORELSE (intro_erasing id)
- (intro_using id)));
- tclIDTAC])
+ tclTHENFIRST
+ (cut t)
+ (tclORELSE
+ (intro_replacing id)
+ (tclORELSE (intro_erasing id)
+ (intro_using id)))
let cut_in_parallel l =
let rec prec = function
| [] -> tclIDTAC
- | h::t -> (tclTHENS (cut h) ([prec t;tclIDTAC]))
+ | h::t -> tclTHENFIRST (cut h) (prec t)
in
prec (List.rev l)
@@ -693,13 +612,6 @@ let generalize lconstr gl =
let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in
apply_type newcl lconstr gl
-let dyn_generalize =
- fun argsl -> generalize (List.map Tacinterp.constr_of_Constr argsl)
-
-let dyn_generalize_dep = function
- | [Constr csr] -> generalize_dep csr
- | l -> bad_tactic_args "dyn_generalize_dep" l
-
(* Faudra-t-il une version avec plusieurs args de generalize_dep ?
Cela peut-être troublant de faire "Generalize Dependent H n" dans
"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
@@ -736,21 +648,35 @@ let quantify lconstr =
the left of each x1, ...).
*)
-let letin_abstract id c (occ_ccl,occ_hyps) gl =
- let everywhere = (occ_ccl = None) & (occ_hyps = []) in
+let occurrences_of_hyp id = function
+ | None, [] -> (* Everywhere *) Some []
+ | _, occ_hyps -> try Some (List.assoc id occ_hyps) with Not_found -> None
+
+let occurrences_of_goal = function
+ | None, [] -> (* Everywhere *) Some []
+ | Some gocc as x, _ -> x
+ | None, _ -> None
+
+let everywhere (occ_ccl,occ_hyps) = (occ_ccl = None) & (occ_hyps = [])
+
+let letin_abstract id c occs gl =
let env = pf_env gl in
let compute_dependency _ (hyp,_,_ as d) ctxt =
let d' =
try
- let occ = if everywhere then [] else List.assoc hyp occ_hyps in
- let newdecl = subst_term_occ_decl env occ c d in
- if d = newdecl then
- if not everywhere then raise (RefinerError (DoesNotOccurIn (c,hyp)))
- else raise Not_found
- else
- (subst1_decl (mkVar id) newdecl, true)
- with Not_found ->
- (d,List.exists (fun((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt)
+ match occurrences_of_hyp hyp occs with
+ | None -> raise Not_found
+ | Some occ ->
+ let newdecl = subst_term_occ_decl env occ c d in
+ if d = newdecl then
+ if not (everywhere occs)
+ then raise (RefinerError (DoesNotOccurIn (c,hyp)))
+ else raise Not_found
+ else
+ (subst1_decl (mkVar id) newdecl, true)
+ with Not_found ->
+ (d,List.exists
+ (fun ((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt)
in d'::ctxt
in
let ctxt' = fold_named_context compute_dependency env ~init:[] in
@@ -758,27 +684,7 @@ let letin_abstract id c (occ_ccl,occ_hyps) gl =
if b then ((d::depdecls,(hyp,lhyp)::marks), lhyp)
else (accu, Some hyp) in
let (depdecls,marks),_ = List.fold_left compute_marks (([],[]),None) ctxt' in
-(*
- let abstract ((depdecls,marks as accu),lhyp) (hyp,_,_ as d) =
- try
- let occ = if everywhere then [] else List.assoc hyp occ_hyps in
- let newdecl = subst_term_occ_decl env occ c d in
- if d = newdecl then
- if not everywhere then raise (RefinerError (DoesNotOccurIn (c,hyp)))
- else
- if List.exists (fun (id,_,_) -> occur_var id d)
- (accu, Some hyp)
- else
- let newdecl = subst1_decl (mkVar id) newdecl in
- ((newdecl::depdecls,(hyp,lhyp)::marks), lhyp)
- with Not_found ->
- (accu, Some hyp)
- in
- let (depdecls,marks),_ =
- fold_named_context_reverse abstract ~init:(([],[]),None) env in(* *)
-*)
- let occ_ccl = if everywhere then Some [] else occ_ccl in
- let ccl = match occ_ccl with
+ let ccl = match occurrences_of_goal occs with
| None -> pf_concl gl
| Some occ -> subst1 (mkVar id) (subst_term_occ env occ c (pf_concl gl))
in
@@ -810,7 +716,7 @@ let letin_tac with_eq name c occs gl =
if with_eq then tclIDTAC else thin_body [id];
intros_move marks ] gl
-let check_hypotheses_occurrences_list env occl =
+let check_hypotheses_occurrences_list env (_,occl) =
let rec check acc = function
| (hyp,_) :: rest ->
if List.mem hyp acc then
@@ -821,27 +727,9 @@ let check_hypotheses_occurrences_list env occl =
| [] -> ()
in check [] occl
-let dyn_lettac args gl = match args with
- | [Identifier id; Command com; Letpatterns (o,l)] ->
- check_hypotheses_occurrences_list (pf_env gl) l;
- letin_tac true (Name id) (pf_interp_constr gl com) (o,l) gl
- | [Identifier id; Constr c; Letpatterns (o,l)] ->
- check_hypotheses_occurrences_list (pf_env gl) l;
- letin_tac true (Name id) c (o,l) gl
- | l -> bad_tactic_args "letin" l
-
let nowhere = (Some [],[])
-let dyn_forward args gl = match args with
- | [Quoted_string s; Command com; Identifier id] ->
- letin_tac (s="KeepBody") (Name id) (pf_interp_constr gl com) nowhere gl
- | [Quoted_string s; Constr c; Identifier id] ->
- letin_tac (s="KeepBody") (Name id) c nowhere gl
- | [Quoted_string s; Constr c] ->
- letin_tac (s="KeepBody") Anonymous c nowhere gl
- | [Quoted_string s; Command c] ->
- letin_tac (s="KeepBody") Anonymous (pf_interp_constr gl c) nowhere gl
- | l -> bad_tactic_args "forward" l
+let forward b na c = letin_tac b na c nowhere
(********************************************************************)
(* Exact tactics *)
@@ -857,23 +745,10 @@ let exact_check c gl =
let exact_no_check = refine
-let dyn_exact_no_check cc gl = match cc with
- | [Constr c] -> exact_no_check c gl
- | [Command com] ->
- let evc = (project gl) in
- let concl = (pf_concl gl) in
- let c = Astterm.interp_casted_constr evc (pf_env gl) com concl in
- refine c gl
- | l -> bad_tactic_args "exact_no_check" l
-
-let dyn_exact_check cc gl = match cc with
- | [Constr c] -> exact_check c gl
- | [Command com] ->
- let evc = (project gl) in
- let concl = (pf_concl gl) in
- let c = Astterm.interp_casted_constr evc (pf_env gl) com concl in
- refine c gl
- | l -> bad_tactic_args "exact_check" l
+let exact_proof c gl =
+ (* on experimente la synthese d'ise dans exact *)
+ let c = Astterm.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
+ in refine c gl
let (assumption : tactic) = fun gl ->
let concl = pf_concl gl in
@@ -885,11 +760,6 @@ let (assumption : tactic) = fun gl ->
in
arec (pf_hyps gl)
-let dyn_assumption = function
- | [] -> assumption
- | l -> bad_tactic_args "assumption" l
-
-
(*****************************************************************)
(* Modification of a local context *)
(*****************************************************************)
@@ -899,22 +769,10 @@ let dyn_assumption = function
* subsequently used in other hypotheses or in the conclusion of the
* goal. *)
-let clear ids gl = thin ids gl
-let dyn_clear = function
- | [Clause ids] ->
- if ids=[] then tclIDTAC
- else
- let out = function InHyp id -> id | _ -> assert false in
- clear (List.map out ids)
- | l -> bad_tactic_args "clear" l
+let clear ids gl = (* avant seul dyn_clear n'echouait pas en [] *)
+ if ids=[] then tclIDTAC gl else thin ids gl
let clear_body = thin_body
-let dyn_clear_body = function
- | [Clause ids] ->
- let out = function InHyp id -> id | _ -> assert false in
- clear_body (List.map out ids)
- | l -> bad_tactic_args "clear_body" l
-
(* Takes a list of booleans, and introduces all the variables
* quantified in the goal which are associated with a value
@@ -940,44 +798,10 @@ let new_hyp mopt c lbind g =
| Some m -> if m < nargs then list_firstn m tstack else tstack
| None -> tstack)
in
- (tclTHENL (tclTHEN (kONT clause.hook)
+ (tclTHENLAST (tclTHEN (kONT clause.hook)
(cut (pf_type_of g cut_pf)))
((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
-let dyn_new_hyp argsl gl =
- match argsl with
- | [Integer n; Command com; Bindings binds] ->
- tactic_bind_list
- (new_hyp (Some n)
- (pf_interp_constr gl com))
- binds gl
- | [Command com; Bindings binds] ->
- tactic_bind_list
- (new_hyp None
- (pf_interp_constr gl com))
- binds gl
- | [Integer n; Constr c; Cbindings binds] ->
- new_hyp (Some n) c binds gl
- | [Constr c; Cbindings binds] ->
- new_hyp None c binds gl
- | l -> bad_tactic_args "new_hyp" l
-
-(* Moving hypotheses *)
-
-let dyn_move = function
- | [Identifier idfrom; Identifier idto] -> move_hyp false idfrom idto
- | l -> bad_tactic_args "move" l
-
-let dyn_move_dep = function
- | [Identifier idfrom; Identifier idto] -> move_hyp true idfrom idto
- | l -> bad_tactic_args "move_dep" l
-
-(* Renaming hypotheses *)
-
-let dyn_rename = function
- | [Identifier idfrom; Identifier idto] -> rename_hyp idfrom idto
- | l -> bad_tactic_args "rename" l
-
(************************)
(* Introduction tactics *)
(************************)
@@ -1002,63 +826,28 @@ let constructor_tac boundopt i lbind gl =
let one_constructor i = constructor_tac None i
-let any_constructor gl =
- let cl = pf_concl gl in
- let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in
- let nconstr =
- Array.length (snd (Global.lookup_inductive mind)).mind_consnames
- and sigma = project gl in
- if nconstr = 0 then error "The type has no constructors";
- tclFIRST (List.map (fun i -> one_constructor i [])
- (interval 1 nconstr)) gl
-
(* Try to apply the constructor of the inductive definition followed by
a tactic t given as an argument.
Should be generalize in Constructor (Fun c : I -> tactic)
*)
-let tclConstrThen t gl =
- let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl))
- in let lconstr =
- (snd (Global.lookup_inductive mind)).mind_consnames
- in let nconstr = Array.length lconstr
- in
+let any_constructor tacopt gl =
+ let t = match tacopt with None -> tclIDTAC | Some t -> t in
+ let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
+ let nconstr =
+ Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
if nconstr = 0 then error "The type has no constructors";
- tclFIRST (List.map (fun i -> (tclTHEN (one_constructor i []) t))
+ tclFIRST (List.map (fun i -> tclTHEN (one_constructor i NoBindings) t)
(interval 1 nconstr)) gl
-let dyn_constructor = function
- | [Integer i; Bindings binds] -> tactic_bind_list (one_constructor i) binds
- | [Integer i; Cbindings binds] -> (one_constructor i) binds
- | [Tac (tac,_)] -> tclConstrThen tac
- | [] -> any_constructor
- | l -> bad_tactic_args "constructor" l
-
-
let left = constructor_tac (Some 2) 1
-let simplest_left = left []
-
-let dyn_left = function
- | [Cbindings binds] -> left binds
- | [Bindings binds] -> tactic_bind_list left binds
- | l -> bad_tactic_args "left" l
+let simplest_left = left NoBindings
let right = constructor_tac (Some 2) 2
-let simplest_right = right []
-
-let dyn_right = function
- | [Cbindings binds] -> right binds
- | [Bindings binds] -> tactic_bind_list right binds
- | l -> bad_tactic_args "right" l
-
+let simplest_right = right NoBindings
let split = constructor_tac (Some 1) 1
-let simplest_split = split []
-
-let dyn_split = function
- | [Cbindings binds] -> split binds
- | [Bindings binds] -> tactic_bind_list split binds
- | l -> bad_tactic_args "split" l
+let simplest_split = split NoBindings
(********************************************)
(* Elimination tactics *)
@@ -1112,17 +901,33 @@ let general_elim (c,lbindc) (elimc,lbindelimc) gl =
(* Elimination tactic with bindings but using the default elimination
* constant associated with the type. *)
-let default_elim (c,lbindc) gl =
+let find_eliminator c gl =
let env = pf_env gl in
let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in
let s = elimination_sort_of_goal gl in
- let elimc = Indrec.lookup_eliminator ind s in
- general_elim (c,lbindc) (elimc,[]) gl
-
+ try Indrec.lookup_eliminator ind s
+ with Not_found ->
+ let dir, base = repr_path (path_of_inductive env ind) in
+ let id = Indrec.make_elimination_ident base s in
+ errorlabstrm "default_elim"
+ (str "Cannot find the elimination combinator :" ++
+ pr_id id ++ spc () ++
+ str "The elimination of the inductive definition :" ++
+ pr_id base ++ spc () ++ str "on sort " ++
+ spc () ++ print_sort (new_sort_in_family s) ++
+ str " is probably not allowed")
+
+let default_elim (c,lbindc) gl =
+ general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl
+
+let elim (c,lbindc) elim gl =
+ match elim with
+ | Some (elimc,lbindelimc) -> general_elim (c,lbindc) (elimc,lbindelimc) gl
+ | None -> general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl
(* The simplest elimination tactic, with no substitutions at all. *)
-let simplest_elim c = default_elim (c,[])
+let simplest_elim c = default_elim (c,NoBindings)
(* Elimination in hypothesis *)
@@ -1383,11 +1188,6 @@ let find_atomic_param_of_ind mind indtyp =
Others solutions are welcome *)
-(*
-type hyp_status =
-let hyps_map
-*)
-
exception Shunt of identifier option
let cook_sign hyp0 indvars env =
@@ -1438,44 +1238,12 @@ let cook_sign hyp0 indvars env =
let statuslists = (!lstatus,List.rev !rstatus) in
(statuslists, lhyp0, !indhyps, !decldeps)
-
-(* Vieille version en une seule passe grace à l'ordre supérieur mais
- trop difficile à comprendre
-
-let cook_sign hyp0 indvars sign =
- let finaldeps = ref ([],[]) in
- let indhyps = ref [] in
- let hyp0succ = ref None in
- let cook_init (hdeps,tdeps) rhyp before =
- finaldeps := (List.rev hdeps, List.rev tdeps);
- (None, []) in
- let cook_hyp compute_rhyp hyp typ ((hdeps,tdeps) as deps) =
- fun rhyp before ->
- match () with
- _ when (List.mem hyp indvars)
- -> let result = compute_rhyp deps rhyp before in
- indhyps := hyp::!indhyps; result
- | _ when hyp = hyp0
- -> let (lhyp,statl) = compute_rhyp deps rhyp true in
- hyp0succ := lhyp; (None (* fake value *),statl)
- | _ when (List.exists (fun id -> occur_var id typ) (hyp0::indvars)
- or List.exists (fun id -> occur_var id typ) hdeps)
- -> let deps' = (hyp::hdeps, typ::tdeps) in
- let (lhyp,statl) = compute_rhyp deps' rhyp before in
- let hyp = if before then lhyp else rhyp in
- (lhyp,(DEPENDENT (before,hyp,hyp))::statl)
- | _ ->
- let (_,statl) = compute_rhyp deps (Some hyp) before
- in (Some hyp, statl)
- in let (_,statuslist) = it_sign cook_hyp cook_init sign ([],[]) None false in
- (statuslist, !hyp0succ, !indhyps, !finaldeps)
-*)
-
-let induction_tac varname typ (elimc,elimt) gl =
+let induction_tac varname typ (elimc,elimt,lbindelimc) gl =
let c = mkVar varname in
let (wc,kONT) = startWalk gl in
- let indclause = make_clenv_binding wc (c,typ) [] in
- let elimclause = make_clenv_binding wc (mkCast (elimc,elimt),elimt) [] in
+ let indclause = make_clenv_binding wc (c,typ) NoBindings in
+ let elimclause =
+ make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in
elimination_clause_scheme kONT elimclause indclause gl
let is_indhyp p n t =
@@ -1510,9 +1278,9 @@ let compute_elim_signature_and_roughly_check elimt mind =
| Prod (_,t,c) -> (check_branch n t lra.(n)) :: (check_elim c (n+1))
| _ -> error "Not an eliminator: some constructor case is lacking" in
let _,elimt3 = decompose_prod_n npred elimt2 in
- check_elim elimt3 0
+ Array.of_list (check_elim elimt3 0)
-let induction_from_context isrec style hyp0 gl =
+let induction_from_context isrec style elim hyp0 gl =
(*test suivant sans doute inutile car refait par le letin_tac*)
if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
errorlabstrm "induction"
@@ -1520,12 +1288,17 @@ let induction_from_context isrec style hyp0 gl =
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
let env = pf_env gl in
let (mind,typ0) = pf_reduce_to_quantified_ind gl tmptyp0 in
- let indvars = find_atomic_param_of_ind mind (snd (decompose_prod typ0)) in
- let elimc =
- if isrec then Indrec.lookup_eliminator mind (elimination_sort_of_goal gl)
- else Indrec.make_case_gen env (project gl) mind (elimination_sort_of_goal gl)
- in
+ let elimc,lbindelimc = match elim with
+ | None ->
+ let s = elimination_sort_of_goal gl in
+ (if isrec then Indrec.lookup_eliminator mind s
+ else Indrec.make_case_gen env (project gl) mind s),
+ NoBindings
+ | Some elim ->
+ (* Not really robust: no control on the form of the combinator *)
+ elim in
let elimt = pf_type_of gl elimc in
+ let indvars = find_atomic_param_of_ind mind (snd (decompose_prod typ0)) in
let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
let lr = compute_elim_signature_and_roughly_check elimt mind in
@@ -1538,32 +1311,35 @@ let induction_from_context isrec style hyp0 gl =
eux qui ouvrent de nouveaux buts arrivent en premier dans la
liste des sous-buts du fait qu'ils sont le plus à gauche dans le
combinateur engendré par make_case_gen (un "Cases (hyp0 ?) of
- ...") et on ne peut plus appliquer tclTHENST après; en revanche,
+ ...") et on ne peut plus appliquer tclTHENSI après; en revanche,
comme lookup_eliminator renvoie un combinateur de la forme
"ind_rec ... (hyp0 ?)", les buts correspondant à des arguments de
- hyp0 sont maintenant à la fin et tclTHENS marche !!! *)
+ hyp0 sont maintenant à la fin et tclTHENSI marche !!! *)
+(*
if not isrec && nb_prod typ0 <> 0 && lr <> [] (* passe-droit *) then
error "Cases analysis on a functional term not implemented";
-
+*)
tclTHENLIST
[ apply_type tmpcl args;
thin dephyps;
- tclTHENST
+ (if isrec then tclTHENFIRSTn else tclTHENLASTn)
(tclTHEN
- (induction_tac hyp0 typ0 (elimc,elimt))
+ (induction_tac hyp0 typ0 (elimc,elimt,lbindelimc))
(thin (hyp0::indhyps)))
- (List.map
+ (Array.map
(induct_discharge style mind statlists hyp0 lhyp0
(List.rev dephyps)) lr)
- tclIDTAC ]
+ ]
gl
let induction_with_atomization_of_ind_arg isrec hyp0 =
tclTHEN
(atomize_param_of_ind hyp0)
- (induction_from_context isrec false hyp0)
+ (induction_from_context isrec false None hyp0)
-let new_induct isrec c gl =
+(* This is Induction since V7 ("natural" induction both in quantified
+ premisses and introduced ones) *)
+let new_induct_gen isrec c gl =
match kind_of_term c with
| Var id when not (mem_named_context id (Global.named_context())) ->
induction_with_atomization_of_ind_arg isrec id gl
@@ -1575,60 +1351,34 @@ let new_induct isrec c gl =
(letin_tac true (Name id) c (None,[]))
(induction_with_atomization_of_ind_arg isrec id) gl
-(*
-let new_induct_nodep isrec n =
- tclTHEN (intros_until_n n) (induction_with_atomization_of_ind_arg isrec None)
-*)
+let new_induct_destruct isrec = function
+ | ElimOnConstr c -> new_induct_gen isrec c
+ | ElimOnAnonHyp n ->
+ tclTHEN (intros_until_n n) (tclLAST_HYP (new_induct_gen isrec))
+ (* Identifier apart because id can be quantified in goal and not typable *)
+ | ElimOnIdent (_,id) ->
+ tclTHEN (tclTRY (intros_until_id id)) (new_induct_gen isrec (mkVar id))
+
+let new_induct = new_induct_destruct true
+let new_destruct = new_induct_destruct false
(* The registered tactic, which calls the default elimination
* if no elimination constant is provided. *)
-
-let dyn_elim = function
- | [Constr mp; Cbindings mpbinds] ->
- default_elim (mp,mpbinds)
- | [Command mp; Bindings mpbinds] ->
- tactic_com_bind_list default_elim (mp,mpbinds)
- | [Command mp; Bindings mpbinds; Command elimc; Bindings elimcbinds] ->
- let funpair2funlist f = (function [x;y] -> f x y | _ -> assert false) in
- tactic_com_bind_list_list
- (funpair2funlist general_elim)
- [(mp,mpbinds);(elimc,elimcbinds)]
- | [Constr mp; Cbindings mpbinds; Constr elimc; Cbindings elimcbinds] ->
- general_elim (mp,mpbinds) (elimc,elimcbinds)
- | l -> bad_tactic_args "elim" l
(* Induction tactics *)
(* This was Induction before 6.3 (induction only in quantified premisses) *)
-let raw_induct s = tclTHEN (intros_until s) (tclLAST_HYP simplest_elim)
+let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim)
let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
(* This was Induction in 6.3 (hybrid form) *)
-let old_induct s =tclORELSE (raw_induct s) (induction_from_context true true s)
+let old_induct_id s =
+ tclORELSE (raw_induct s) (induction_from_context true true None s)
let old_induct_nodep = raw_induct_nodep
-(* This is Induction since V7 ("natural" induction both in quantified
- premisses and introduced ones) *)
-let dyn_new_induct = function
- | [(Command c)] -> tactic_com (new_induct true) c
- | [(Constr x)] -> new_induct true x
- (* Identifier apart because id can be quantified in goal and not typable *)
- | [Integer _ | Identifier _ as arg] ->
- tactic_try_intros_until (fun id -> new_induct true (mkVar id)) arg
- | l -> bad_tactic_args "induct" l
-
-(* This was Induction before 6.3 (induction only in quantified premisses)
-let dyn_raw_induct = function
- | [Identifier x] -> raw_induct x
- | [Integer n] -> raw_induct_nodep n
- | l -> bad_tactic_args "raw_induct" l
-*)
-
-(* This was Induction in 6.3 (hybrid form) *)
-let dyn_old_induct = function
- | [(Identifier n)] -> old_induct n
- | [Integer n] -> raw_induct_nodep n
- | l -> bad_tactic_args "raw_induct" l
+let old_induct = function
+ | NamedHyp id -> old_induct_id id
+ | AnonHyp n -> old_induct_nodep n
(* Case analysis tactics *)
@@ -1640,37 +1390,20 @@ let general_case_analysis (c,lbindc) gl =
let case = if occur_term c (pf_concl gl) then Indrec.make_case_dep
else Indrec.make_case_gen in
let elim = case env sigma mind sort in
- general_elim (c,lbindc) (elim,[]) gl
+ general_elim (c,lbindc) (elim,NoBindings) gl
-let simplest_case c = general_case_analysis (c,[])
-
-let dyn_case =function
- | [Constr mp; Cbindings mpbinds] ->
- general_case_analysis (mp,mpbinds)
- | [Command mp; Bindings mpbinds] ->
- tactic_com_bind_list general_case_analysis (mp,mpbinds)
- | l -> bad_tactic_args "case" l
-
+let simplest_case c = general_case_analysis (c,NoBindings)
(* Destruction tactics *)
-let destruct s = (tclTHEN (intros_until s) (tclLAST_HYP simplest_case))
-let destruct_nodep n = (tclTHEN (intros_until_n n) (tclLAST_HYP simplest_case))
+let old_destruct_id s =
+ (tclTHEN (intros_until_id s) (tclLAST_HYP simplest_case))
+let old_destruct_nodep n =
+ (tclTHEN (intros_until_n n) (tclLAST_HYP simplest_case))
-let dyn_new_destruct = function
- | [(Command c)] -> tactic_com (new_induct false) c
- | [(Constr x)] -> new_induct false x
- (* Identifier apart because id can be quantified in goal and not typable *)
- | [Integer _ | Identifier _ as arg] ->
- tactic_try_intros_until (fun id -> new_induct false (mkVar id)) arg
- | l -> bad_tactic_args "induct" l
-
-let dyn_old_destruct = function
- | [Identifier x] -> destruct x
- | [Integer n] -> destruct_nodep n
- | l -> bad_tactic_args "destruct" l
-
-let dyn_destruct = dyn_old_destruct
+let old_destruct = function
+ | NamedHyp id -> old_destruct_id id
+ | AnonHyp n -> old_destruct_nodep n
(*
* Eliminations giving the type instead of the proof.
@@ -1695,22 +1428,12 @@ let elim_type t gl =
let elimc = Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
elim_scheme_type elimc t gl
-let dyn_elim_type = function
- | [Constr c] -> elim_type c
- | [Command com] -> tactic_com_sort elim_type com
- | l -> bad_tactic_args "elim_type" l
-
let case_type t gl =
let (ind,t) = pf_reduce_to_atomic_ind gl t in
let env = pf_env gl in
let elimc = Indrec.make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in
elim_scheme_type elimc t gl
-let dyn_case_type = function
- | [Constr c] -> case_type c
- | [Command com] -> tactic_com case_type com
- | l -> bad_tactic_args "case_type" l
-
(* Some eliminations frequently used *)
@@ -1750,14 +1473,15 @@ let orE id gl =
let dorE b cls gl =
match cls with
| (Some id) -> orE id gl
- | None -> (if b then right else left) [] gl
+ | None -> (if b then right else left) NoBindings gl
let impE id gl =
let t = pf_get_hyp_typ gl id in
if is_imp_term (pf_hnf_constr gl t) then
let (dom, _, rng) = destProd (pf_hnf_constr gl t) in
- (tclTHENS (cut_intro rng)
- [tclIDTAC;apply_term (mkVar id) [mkMeta (new_meta())]]) gl
+ tclTHENLAST
+ (cut_intro rng)
+ (apply_term (mkVar id) [mkMeta (new_meta())]) gl
else
errorlabstrm "impE"
(str("Tactic impE expects "^(string_of_id id)^
@@ -1772,55 +1496,15 @@ let dImp cls gl =
(* Tactics related with logic connectives *)
(************************************************)
-(* Contradiction *)
-
-let contradiction_on_hyp id gl =
- let hyp = pf_get_hyp_typ gl id in
- if is_empty_type hyp then
- simplest_elim (mkVar id) gl
- else
- error "Not a contradiction"
-
-(* Absurd *)
-let absurd c gls =
- (tclTHENS
- (tclTHEN (elim_type (build_coq_False ())) (cut c))
- ([(tclTHENS
- (cut (applist(build_coq_not (),[c])))
- ([(tclTHEN intros
- ((fun gl ->
- let ida = pf_nth_hyp_id gl 1
- and idna = pf_nth_hyp_id gl 2 in
- exact_no_check (applist(mkVar idna,[mkVar ida])) gl)));
- tclIDTAC]));
- tclIDTAC])) gls
-
-let dyn_absurd = function
- | [Constr c] -> absurd c
- | [Command com] -> tactic_com_sort absurd com
- | l -> bad_tactic_args "absurd" l
-
-let contradiction gls =
- tclTHENLIST [ intros; elim_type (build_coq_False ()); assumption ] gls
-
-let dyn_contradiction = function
- | [] -> contradiction
- | l -> bad_tactic_args "contradiction" l
-
-(* Relfexivity tactics *)
+(* Reflexivity tactics *)
let reflexivity gl =
match match_with_equation (pf_concl gl) with
| None -> error "The conclusion is not a substitutive equation"
- | Some (hdcncl,args) -> one_constructor 1 [] gl
+ | Some (hdcncl,args) -> one_constructor 1 NoBindings gl
let intros_reflexivity = (tclTHEN intros reflexivity)
-let dyn_reflexivity = function
- | [] -> intros_reflexivity
- | _ -> errorlabstrm "Tactics.reflexivity"
- (str "Tactic applied to bad arguments!")
-
(* Symmetry tactics *)
(* This tactic first tries to apply a constant named sym_eq, where eq
@@ -1842,19 +1526,16 @@ let symmetry gl =
| [c1;c2] -> mkApp (hdcncl, [| c2; c1 |])
| _ -> assert false
in
- (tclTHENS (cut symc)
- [ tclTHENLIST [ intro;
- tclLAST_HYP simplest_case;
- one_constructor 1 [] ];
- tclIDTAC ]) gl
+ tclTHENLAST (cut symc)
+ (tclTHENLIST
+ [ intro;
+ tclLAST_HYP simplest_case;
+ one_constructor 1 NoBindings ])
+ gl
end
let intros_symmetry = (tclTHEN intros symmetry)
-let dyn_symmetry = function
- | [] -> intros_symmetry
- | l -> bad_tactic_args "symmetry" l
-
(* Transitivity tactics *)
(* This tactic first tries to apply a constant named trans_eq, where eq
@@ -1886,22 +1567,16 @@ let transitivity t gl =
| [c1;c2] -> mkApp (hdcncl, [| t; c2 |])
| _ -> assert false
in
- (tclTHENS (cut eq2)
- [tclTHENS (cut eq1)
- [ tclTHENLIST [ tclDO 2 intro;
- tclLAST_HYP simplest_case;
- assumption ];
- tclIDTAC];
- tclIDTAC])gl
+ tclTHENFIRST (cut eq2)
+ (tclTHENFIRST (cut eq1)
+ (tclTHENLIST
+ [ tclDO 2 intro;
+ tclLAST_HYP simplest_case;
+ assumption ])) gl
end
let intros_transitivity n = tclTHEN intros (transitivity n)
-let dyn_transitivity = function
- | [Constr n] -> intros_transitivity n
- | [Command n] -> tactic_com intros_transitivity n
- | l -> bad_tactic_args "transitivity" l
-
(* tactical to save as name a subproof such that the generalisation of
the current goal, abstracted with respect to the local signature,
is solved by tac *)
@@ -1922,8 +1597,8 @@ let abstract_subproof name tac gls =
in
if occur_existential concl then error "Abstract cannot handle existentials";
let lemme =
- start_proof na NeverDischarge current_sign concl;
- let _,(const,strength) =
+ start_proof na (false,Nametab.NeverDischarge) current_sign concl (fun _ _ -> ());
+ let _,(const,(_,strength),_) =
try
by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac));
let r = cook_proof () in
@@ -1947,15 +1622,3 @@ let tclABSTRACT name_op tac gls =
| None -> add_suffix (get_current_proof_name ()) "_subproof"
in
abstract_subproof s tac gls
-
-let dyn_tclABSTRACT =
- hide_tactic "ABSTRACT"
- (function
- | [Tac (tac,_)] ->
- tclABSTRACT None tac
- | [Identifier s; Tac (tac,_)] ->
- tclABSTRACT (Some s) tac
- | _ -> invalid_arg "tclABSTRACT")
-
-
-
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 76a21ba833..14d4793625 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -21,8 +21,9 @@ open Evar_refiner
open Clenv
open Tacred
open Tacticals
+open Tacexpr
open Nametab
-(*i*)
+open Rawterm
(* Main tactics. *)
@@ -34,7 +35,7 @@ val type_clenv_binding : named_context sigma ->
val string_of_inductive : constr -> string
val head_constr : constr -> constr list
val head_constr_bound : constr -> constr list -> constr list
-val bad_tactic_args : string -> tactic_arg list -> 'a
+val is_quantified_hypothesis : identifier -> goal sigma -> bool
exception Bound
@@ -47,12 +48,9 @@ val convert_hyp : named_declaration -> tactic
val thin : identifier list -> tactic
val mutual_fix :
identifier -> int -> (identifier * int * constr) list -> tactic
-val fix : identifier -> int -> tactic
+val fix : identifier option -> int -> tactic
val mutual_cofix : identifier -> (identifier * constr) list -> tactic
-val cofix : identifier -> tactic
-
-val dyn_mutual_fix : tactic_arg list -> tactic
-val dyn_mutual_cofix : tactic_arg list -> tactic
+val cofix : identifier option -> tactic
(*s Introduction tactics. *)
@@ -62,9 +60,7 @@ val fresh_id : identifier list -> identifier -> goal sigma -> identifier
val intro : tactic
val introf : tactic
val intro_force : bool -> tactic
-val dyn_intro : tactic_arg list -> tactic
-
-val dyn_intro_move : tactic_arg list -> tactic
+val intro_move : identifier option -> identifier option -> tactic
val intro_replacing : identifier -> tactic
val intro_using : identifier -> tactic
@@ -75,42 +71,31 @@ val intros_replacing : identifier list -> tactic
val intros : tactic
-(*i Obsolete, subsumed by Elim.dyn_intro_pattern
-val dyn_intros_using : tactic_arg list -> tactic
-i*)
+(* [depth_of_quantified_hypothesis b h g] returns the index of [h] in
+ the conclusion of goal [g], up to head-reduction if [b] is [true] *)
+val depth_of_quantified_hypothesis :
+ bool -> quantified_hypothesis -> goal sigma -> int
-val intros_until : identifier -> tactic
-val intros_until_n : int -> tactic
val intros_until_n_wored : int -> tactic
-val dyn_intros_until : tactic_arg list -> tactic
+val intros_until : quantified_hypothesis -> tactic
val intros_clearing : bool list -> tactic
(* Assuming a tactic [tac] depending on an hypothesis identifier,
- [tactic_try_intros_until tac arg] first assumes that arg denotes a
+ [try_intros_until tac arg] first assumes that arg denotes a
quantified hypothesis (denoted by name or by index) and try to
introduce it in context before to apply [tac], otherwise assume the
hypothesis is already in context and directly apply [tac] *)
-val tactic_try_intros_until : (identifier,tactic_arg) parse_combinator
-
-(* Assuming a tactic [tac] depending on an hypothesis identifier,
- [hide_ident_or_numarg_tactic str tac] registers a tactic which
- compose [tac] with "Intros Until" and returns a tactic which
- behaves as [tac] (without implicit "Intros until") but hiding the
- implementation under the name [str] *)
-val hide_ident_or_numarg_tactic : identifier hide_combinator
+val try_intros_until :
+ (identifier -> tactic) -> quantified_hypothesis -> tactic
(*s Exact tactics. *)
val assumption : tactic
-val dyn_assumption : tactic_arg list -> tactic
-
val exact_no_check : constr -> tactic
-val dyn_exact_no_check : tactic_arg list -> tactic
-
val exact_check : constr -> tactic
-val dyn_exact_check : tactic_arg list -> tactic
+val exact_proof : Coqast.t -> tactic
(*s Reduction tactics. *)
@@ -143,28 +128,21 @@ val unfold_option :
(int list * Closure.evaluable_global_reference) list -> hyp_location option
-> tactic
val reduce : red_expr -> hyp_location list -> tactic
-val dyn_reduce : tactic_arg list -> tactic
-val dyn_change : tactic_arg list -> tactic
+val change : constr -> hyp_location list -> tactic
val unfold_constr : global_reference -> tactic
-val pattern_option :
- (int list * constr * constr) list -> hyp_location option -> tactic
+val pattern_option : (int list * constr) list -> hyp_location option -> tactic
(*s Modification of the local context. *)
val clear : identifier list -> tactic
-val dyn_clear : tactic_arg list -> tactic
val clear_body : identifier list -> tactic
-val dyn_clear_body : tactic_arg list -> tactic
val new_hyp : int option ->constr -> constr substitution -> tactic
-val dyn_new_hyp : tactic_arg list -> tactic
-
-val dyn_move : tactic_arg list -> tactic
-val dyn_move_dep : tactic_arg list -> tactic
-val dyn_rename : tactic_arg list -> tactic
+val move_hyp : bool -> identifier -> identifier -> tactic
+val rename_hyp : identifier -> identifier -> tactic
(*s Resolution tactics. *)
@@ -175,47 +153,37 @@ val bring_hyps : named_context -> tactic
val apply : constr -> tactic
val apply_without_reduce : constr -> tactic
val apply_list : constr list -> tactic
-val apply_with_bindings : (constr * constr substitution) -> tactic
-val dyn_apply : tactic_arg list -> tactic
+val apply_with_bindings : constr with_bindings -> tactic
val cut_and_apply : constr -> tactic
-val dyn_cut_and_apply : tactic_arg list -> tactic
(*s Elimination tactics. *)
-val general_elim : constr * constr substitution ->
- constr * constr substitution -> tactic
-val default_elim : constr * constr substitution -> tactic
-val simplest_elim : constr -> tactic
-val dyn_elim : tactic_arg list -> tactic
+val general_elim : constr with_bindings -> constr with_bindings -> tactic
+val default_elim : constr with_bindings -> tactic
+val simplest_elim : constr -> tactic
+val elim : constr with_bindings -> constr with_bindings option -> tactic
+val general_elim_in : identifier -> constr * constr substitution ->
+ constr * constr substitution -> tactic
+val old_induct : quantified_hypothesis -> tactic
val general_elim_in : identifier -> constr * constr substitution ->
constr * constr substitution -> tactic
-val old_induct : identifier -> tactic
-val old_induct_nodep : int -> tactic
-val dyn_old_induct : tactic_arg list -> tactic
-val dyn_new_induct : tactic_arg list -> tactic
+val new_induct : constr induction_arg -> tactic
(*s Case analysis tactics. *)
-val general_case_analysis : constr * constr substitution -> tactic
+val general_case_analysis : constr with_bindings -> tactic
val simplest_case : constr -> tactic
-val dyn_case : tactic_arg list -> tactic
-val destruct : identifier -> tactic
-val destruct_nodep : int -> tactic
-val dyn_destruct : tactic_arg list -> tactic
-val dyn_new_destruct : tactic_arg list -> tactic
+val old_destruct : quantified_hypothesis -> tactic
+val new_destruct : constr induction_arg -> tactic
(*s Eliminations giving the type instead of the proof. *)
val case_type : constr -> tactic
-val dyn_case_type : tactic_arg list -> tactic
-
val elim_type : constr -> tactic
-val dyn_elim_type : tactic_arg list -> tactic
-
(*s Some eliminations which are frequently used. *)
@@ -232,8 +200,7 @@ val dorE : bool -> clause ->tactic
val constructor_tac : int option -> int ->
constr substitution -> tactic
val one_constructor : int -> constr substitution -> tactic
-val any_constructor : tactic
-val tclConstrThen : tactic -> tactic
+val any_constructor : tactic option -> tactic
val left : constr substitution -> tactic
val simplest_left : tactic
val right : constr substitution -> tactic
@@ -241,45 +208,27 @@ val simplest_right : tactic
val split : constr substitution -> tactic
val simplest_split : tactic
-val dyn_constructor : tactic_arg list -> tactic
-val dyn_left : tactic_arg list -> tactic
-val dyn_right : tactic_arg list -> tactic
-val dyn_split : tactic_arg list -> tactic
-
(*s Logical connective tactics. *)
-val absurd : constr -> tactic
-val dyn_absurd : tactic_arg list -> tactic
-
-val contradiction_on_hyp : identifier -> tactic
-val contradiction : tactic
-val dyn_contradiction : tactic_arg list -> tactic
-
-val reflexivity : tactic
+val reflexivity : tactic
val intros_reflexivity : tactic
-val dyn_reflexivity : tactic_arg list -> tactic
-
+
val symmetry : tactic
val intros_symmetry : tactic
-val dyn_symmetry : tactic_arg list -> tactic
val transitivity : constr -> tactic
val intros_transitivity : constr -> tactic
-val dyn_transitivity : tactic_arg list -> tactic
val cut : constr -> tactic
val cut_intro : constr -> tactic
val cut_replacing : identifier -> constr -> tactic
val cut_in_parallel : constr list -> tactic
-val true_cut : identifier -> constr -> tactic
-val true_cut_anon : constr -> tactic
-val dyn_cut : tactic_arg list -> tactic
-val dyn_true_cut : tactic_arg list -> tactic
-val dyn_lettac : tactic_arg list -> tactic
-val dyn_forward : tactic_arg list -> tactic
+val true_cut : identifier option -> constr -> tactic
+val letin_tac : bool -> name -> constr ->
+ identifier clause_pattern -> tactic
+val forward : bool -> name -> constr -> tactic
val generalize : constr list -> tactic
-val dyn_generalize : tactic_arg list -> tactic
-val dyn_generalize_dep : tactic_arg list -> tactic
+val generalize_dep : constr -> tactic
val tclABSTRACT : identifier option -> tactic -> tactic
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 007a3aa997..78f3890c5f 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -18,6 +18,7 @@ open Sign
open Reductionops
open Environ
open Logic
+open Refiner
open Tacmach
open Evd
open Proof_trees
@@ -99,10 +100,12 @@ let clenv_constrain_with_bindings bl clause =
matchrec clause bl
(* What follows is part of the contents of the former file tactics3.ml *)
-
+(* 2/2002: replaced THEN_i by THENSLAST to solve a bug in
+ Tacticals.general_elim when the eliminator has missing bindings *)
+
let elim_res_pf_THEN_i kONT clenv tac gls =
let clenv' = (clenv_unique_resolver true clenv gls) in
- tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
+ tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
let rec build_args acc ce p_0 p_1 =
match kind_of_term p_0, p_1 with
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 26c46e89a5..45b9553265 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -45,6 +45,6 @@ val add_prods_sign :
**i*)
val elim_res_pf_THEN_i :
- (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
+ (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
val applyUsing : constr -> tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 01:16:33 +0000