aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof_trees.ml26
-rw-r--r--proofs/tacinterp.ml47
-rw-r--r--proofs/tacinterp.mli12
3 files changed, 40 insertions, 45 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 8bfa53842c..222b8277a2 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -342,13 +342,12 @@ open Termast
let ast_of_cvt_bind f = function
| (NoDep n,c) -> ope ("BINDING", [(num n); ope ("COMMAND",[(f c)])])
- | (Dep id,c) -> ope ("BINDING", [nvar (string_of_id id);
- ope ("COMMAND",[(f c)])])
+ | (Dep id,c) -> ope ("BINDING", [nvar id; ope ("COMMAND",[(f c)])])
| (Com,c) -> ope ("BINDING", [ope ("COMMAND",[(f c)])])
let rec ast_of_cvt_intro_pattern = function
| WildPat -> ope ("WILDCAR",[])
- | IdPat id -> nvar (string_of_id id)
+ | IdPat id -> nvar id
| DisjPat l -> ope ("DISJPATTERN", (List.map ast_of_cvt_intro_pattern l))
| ConjPat l -> ope ("CONJPATTERN", (List.map ast_of_cvt_intro_pattern l))
| ListPat l -> ope ("LISTPATTERN", (List.map ast_of_cvt_intro_pattern l))
@@ -363,7 +362,7 @@ let last_of_cvt_flags (_,red) =
let lqid =
List.map
(function
- | EvalVarRef id -> nvar (string_of_id id)
+ | EvalVarRef id -> nvar id
| EvalConstRef sp ->
ast_of_qualid (Global.qualid_of_global (ConstRef sp)))
lconst in
@@ -383,7 +382,7 @@ let ast_of_cvt_redexp = function
| Unfold l ->
ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
[match sp with
- | EvalVarRef id -> nvar (string_of_id id)
+ | EvalVarRef id -> nvar id
| EvalConstRef sp ->
ast_of_qualid (Global.qualid_of_global (ConstRef sp))]
@(List.map num locc))) l)
@@ -397,8 +396,8 @@ let ast_of_cvt_redexp = function
(* Gives the ast corresponding to a tactic argument *)
let ast_of_cvt_arg = function
- | Identifier id -> nvar (string_of_id id)
- | Qualid qid -> nvar (Nametab.string_of_qualid qid)
+ | Identifier id -> nvar id
+ | Qualid qid -> ast_of_qualid qid
| Quoted_string s -> str s
| Integer n -> num n
| Command c -> ope ("COMMAND",[c])
@@ -411,8 +410,8 @@ let ast_of_cvt_arg = function
"Constr_context argument could not be used">]
| Clause idl ->
let transl = function
- | InHyp id -> ope ("INHYP", [nvar (string_of_id id)])
- | InHypType id -> ope ("INHYPTYPE", [nvar (string_of_id id)]) in
+ | InHyp id -> ope ("INHYP", [nvar id])
+ | InHypType id -> ope ("INHYPTYPE", [nvar id]) in
ope ("CLAUSE", List.map transl idl)
| Bindings bl -> ope ("BINDINGS",
List.map (ast_of_cvt_bind (fun x -> x)) bl)
@@ -424,17 +423,14 @@ let ast_of_cvt_arg = function
| Tacexp ast -> ope ("TACTIC",[ast])
| Tac (tac,ast) -> ast
| Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red])
- | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id));
- (num n);
- ope ("COMMAND",[c])])
- | Cofixexp (id,c) -> ope ("COFIXEXP",[(nvar (string_of_id id));
- (ope ("COMMAND",[c]))])
+ | Fixexp (id,n,c) -> ope ("FIXEXP",[nvar id; num n; ope ("COMMAND",[c])])
+ | Cofixexp (id,c) -> ope ("COFIXEXP",[nvar id; ope ("COMMAND",[c])])
| Intropattern p -> ast_of_cvt_intro_pattern p
| Letpatterns (gl_occ_opt,hyp_occ_list) ->
let hyps_pats =
List.map
(fun (id,l) ->
- ope ("HYPPATTERN", nvar (string_of_id id) :: (List.map num l)))
+ ope ("HYPPATTERN", nvar id :: (List.map num l)))
hyp_occ_list in
let all_pats =
match gl_occ_opt with
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index ede93699af..846344210c 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -29,6 +29,7 @@ open Tactic_debug
open Coqast
open Ast
open Term
+open Declare
let err_msg_tactic_not_found macro_loc macro =
user_err_loc
@@ -42,13 +43,13 @@ type value =
| VRTactic of (goal list sigma * validation)
| VContext of (goal sigma -> value)
| VArg of tactic_arg
- | VFun of (string * value) list * string option list * Coqast.t
+ | VFun of (identifier * value) list * identifier option list * Coqast.t
| VVoid
| VRec of value ref
(* Signature for interpretation: val_interp and interpretation functions *)
and interp_sign =
- enamed_declarations * Environ.env * (string * value) list *
+ enamed_declarations * Environ.env * (identifier * value) list *
(int * constr) list * goal sigma option * debug_info
(* For tactic_of_value *)
@@ -124,9 +125,9 @@ let constr_of_id id = function
(* Extracted the constr list from lfun *)
let rec constr_list goalopt = function
- | (str,VArg(Constr c))::tl -> (id_of_string str,c)::(constr_list goalopt tl)
- | (str,VArg(Identifier id))::tl ->
- (try (id_of_string str,(constr_of_id id goalopt))::(constr_list goalopt tl)
+ | (id,VArg(Constr c))::tl -> (id,c)::(constr_list goalopt tl)
+ | (id0,VArg(Identifier id))::tl ->
+ (try (id0,(constr_of_id id goalopt))::(constr_list goalopt tl)
with | Not_found -> (constr_list goalopt tl))
| _::tl -> constr_list goalopt tl
| [] -> []
@@ -278,12 +279,12 @@ let head_with_value (lvar,lval) =
(* Type of patterns *)
type match_pattern =
| Term of constr_pattern
- | Subterm of string option * constr_pattern
+ | Subterm of identifier option * constr_pattern
(* Type of hypotheses for a Match Context rule *)
type match_context_hyps =
| NoHypId of match_pattern
- | Hyp of string * match_pattern
+ | Hyp of identifier * match_pattern
(* Type of a Match rule for Match Context and Match *)
type match_rule=
@@ -503,7 +504,7 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
(try (unrec (List.assoc s lfun))
with | Not_found ->
(try (vcontext_interp goalopt (lookup s))
- with | Not_found -> VArg (Identifier (id_of_string s))))
+ with | Not_found -> VArg (Identifier s)))
| Node(_,"QUALIDARG",[Nvar(_,s)]) ->
(try (make_qid (unrec (List.assoc s lfun)))
with | Not_found ->
@@ -531,9 +532,9 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
VArg (Tac ((tac_interp lfun lmatch debug ast),ast))
(*Remains to treat*)
| Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
- VArg ((Fixexp (id_of_string s,n,c)))
+ VArg ((Fixexp (s,n,c)))
| Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) ->
- VArg ((Cofixexp (id_of_string s,c)))
+ VArg ((Cofixexp (s,c)))
(*End of Remains to treat*)
| Node(_,"INTROPATTERN", [ast]) ->
VArg ((Intropattern (cvt_intro_pattern
@@ -621,19 +622,18 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
| Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
(id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t)::
(letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
- | Node(_,"LETCUTCLAUSE",[Nvar(_,s);com;tce])::tl ->
- let id = id_of_string s
- and typ =
+ | Node(_,"LETCUTCLAUSE",[Nvar(_,id);com;tce])::tl ->
+ let typ =
constr_of_Constr (unvarg
(val_interp (evc,env,lfun,lmatch,goalopt,debug) com))
and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce in
(match tac with
| VArg (Constr csr) ->
- (s,VArg (Constr (mkCast (csr,typ))))::
+ (id,VArg (Constr (mkCast (csr,typ))))::
(letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
| VArg (Identifier id) ->
(try
- (s,VArg (Constr (mkCast (constr_of_id id goalopt,typ))))::
+ (id,VArg (Constr (mkCast (constr_of_id id goalopt,typ))))::
(letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
with | Not_found ->
errorlabstrm "Tacinterp.letin_interp"
@@ -645,12 +645,12 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
(match goalopt with
| None -> Global.named_context ()
| Some g -> pf_hyps g) in
- start_proof id Declare.NeverDischarge ndc typ;
+ start_proof id NeverDischarge ndc typ;
by t;
let (_,({const_entry_body = pft; const_entry_type = _},_)) =
cook_proof () in
delete_proof id;
- (s,VArg (Constr (mkCast (pft,typ))))::
+ (id,VArg (Constr (mkCast (pft,typ))))::
(letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
with | NotTactic ->
delete_proof id;
@@ -663,9 +663,8 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
(* Interprets the clauses of a LetCut *)
and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
| [] -> tclIDTAC
- | Node(_,"LETCUTCLAUSE",[Nvar(_,s);com;tce])::tl ->
- let id = id_of_string s
- and typ =
+ | Node(_,"LETCUTCLAUSE",[Nvar(_,id);com;tce])::tl ->
+ let typ =
constr_of_Constr (unvarg
(val_interp (evc,env,lfun,lmatch,goalopt,debug) com))
and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce
@@ -699,7 +698,7 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
| _ ->
(try
let t = tactic_of_value tac in
- start_proof id Declare.NeverDischarge ndc typ;
+ start_proof id NeverDischarge ndc typ;
by t;
let (_,({const_entry_body = pft; const_entry_type = _},_)) =
cook_proof () in
@@ -1216,7 +1215,7 @@ let add_tacdef na vbody =
errorlabstrm "Tacinterp.add_tacdef"
[< 'sTR
"There is already a Meta Definition or a Tactic Definition named ";
- 'sTR na>];
- let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
- Options.if_verbose mSGNL [< 'sTR (na ^ " is defined") >]
+ pr_id na>];
+ let _ = Lib.add_leaf na OBJ (inMD (na,vbody)) in
+ Options.if_verbose mSGNL [< pr_id na; 'sTR " is defined" >]
end
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 971cb88df8..f6be508697 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -25,13 +25,13 @@ type value =
| VRTactic of (goal list sigma * validation)
| VContext of (goal sigma -> value)
| VArg of tactic_arg
- | VFun of (string * value) list * string option list * Coqast.t
+ | VFun of (identifier * value) list * identifier option list * Coqast.t
| VVoid
| VRec of value ref
(* Signature for interpretation: val\_interp and interpretation functions *)
and interp_sign =
- enamed_declarations * Environ.env * (string * value) list *
+ enamed_declarations * Environ.env * (identifier * value) list *
(int * constr) list * goal sigma option * debug_info
(* Gives the constr corresponding to a CONSTR [tactic_arg] *)
@@ -45,7 +45,7 @@ val tacticIn : (unit -> Coqast.t) -> Coqast.t
initialized with dummy values *)
val r_evc : enamed_declarations ref
val r_env : Environ.env ref
-val r_lfun : (string * value) list ref
+val r_lfun : (identifier * value) list ref
val r_lmatch : (int * constr) list ref
val r_goalopt : goal sigma option ref
val r_debug : debug_info ref
@@ -57,7 +57,7 @@ val set_debug : debug_info -> unit
val get_debug : unit -> debug_info
(* Adds a definition for tactics in the table *)
-val add_tacdef : string -> Coqast.t -> unit
+val add_tacdef : identifier -> Coqast.t -> unit
(* Interprets any expression *)
val val_interp : interp_sign -> Coqast.t -> value
@@ -66,8 +66,8 @@ val val_interp : interp_sign -> Coqast.t -> value
val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg
(* Interprets tactic expressions *)
-val tac_interp : (string * value) list -> (int * constr) list -> debug_info ->
- Coqast.t -> tactic
+val tac_interp : (identifier * value) list -> (int * constr) list ->
+ debug_info -> Coqast.t -> tactic
(* Initial call for interpretation *)
val interp : Coqast.t -> tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 15:46:24 +0000