aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-01-05 19:45:07 +0000
committerGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-01-05 19:45:07 +0000
commitbeed52ca495d7cceac9abba5722576a6d9f15ed2 (patch)
tree13ebe61c6a1f96ac72e6bc8d701d207c644af603 /proofs
parent6156db30ff25c13d9b2da8d5d591b4807e408040 (diff)
Arite cachee de Match Context + Meta Definition
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1236 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r--proofs/tacinterp.ml74
-rw-r--r--proofs/tacinterp.mli15
2 files changed, 55 insertions, 34 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index dd0199c0f..5d7c46a79 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -31,11 +31,17 @@ type value =
| VTactic of tactic
| VFTactic of tactic_arg list * (tactic_arg list->tactic)
| VRTactic of (goal list sigma * validation)
+ | VContext of (interp_sign -> goal sigma -> value)
| VArg of tactic_arg
| VFun of (string * value) list * string 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 *
+ (int * constr) list * goal sigma option * debug_info
+
(* For tactic_of_value *)
exception NotTactic
@@ -123,11 +129,6 @@ let rec constr_list goalopt = function
| _::tl -> constr_list goalopt tl
| [] -> []
-(* Signature for interpretation: val_interp and interpretation functions *)
-type interp_sign =
- enamed_declarations * Environ.env * (string * value) list *
- (int * constr) list * goal sigma option * debug_info
-
(* For user tactics *)
let ((ocamlIn : (unit -> Coqast.t) -> Dyn.t),
(ocamlOut : Dyn.t -> (unit -> Coqast.t))) = create "ocaml"
@@ -487,12 +488,12 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
| Nvar(_,s) ->
(try (unrec (List.assoc s lfun))
with | Not_found ->
- (try (lookup s)
+ (try (vcontext_interp (evc,env,lfun,lmatch,goalopt,debug) (lookup s))
with | Not_found -> VArg (Identifier (id_of_string s))))
| Node(_,"QUALID",[Nvar(_,s)]) ->
(try (unrec (List.assoc s lfun))
with | Not_found ->
- (try (lookup s)
+ (try (vcontext_interp (evc,env,lfun,lmatch,goalopt,debug) (lookup s))
with | Not_found -> VArg (Identifier (id_of_string s))))
| Str(_,s) -> VArg (Quoted_string s)
| Num(_,n) -> VArg (Integer n)
@@ -707,14 +708,14 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
(* Interprets the Match Context expressions *)
and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
- let goal =
+(* let goal =
(match goalopt with
| None ->
errorlabstrm "Tacinterp.apply_match_context" [< 'sTR
"No goal available" >]
- | Some g -> g) in
- let rec apply_goal_sub evc env lfun lmatch goal nocc (id,c) csr mt mhyps hyps
- =
+ | Some g -> g) in*)
+ let rec apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) 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
@@ -728,14 +729,16 @@ and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
| (FailError _) as e -> raise e
| NextOccurrence _ -> raise No_match
| No_match | _ ->
- apply_goal_sub evc env lfun lmatch goal (nocc + 1) (id,c) csr mt mhyps
- hyps in
- let rec apply_match_context evc env lfun lmatch goal = function
+ apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) goal (nocc + 1) (id,c)
+ csr mt mhyps hyps in
+ let rec apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal =
+ function
| (All t)::tl ->
(try
eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal,debug)) t
goal
- with No_match | _ -> apply_match_context evc env lfun lmatch goal tl)
+ with No_match | _ ->
+ apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl)
| (Pat (mhyps,mgoal,mt))::tl ->
let hyps = make_hyps (List.rev (pf_hyps goal))
and concl = pf_concl goal in
@@ -753,17 +756,27 @@ and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
hyps
end)
with | No_match | _ ->
- apply_match_context evc env lfun lmatch goal tl)
+ apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl)
| Subterm (id,mg) ->
(try
- apply_goal_sub evc env lfun lmatch goal 0 (id,mg) concl mt mhyps hyps
+ apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) goal 0 (id,mg)
+ concl mt mhyps hyps
with
- | No_match | _ -> apply_match_context evc env lfun lmatch goal tl))
+ | No_match | _ ->
+ apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl))
| _ ->
errorlabstrm "Tacinterp.apply_match_context" [<'sTR
"No matching clauses for Match Context">] in
- apply_match_context evc env lfun lmatch goal (read_match_context_rule evc env
- (constr_list goalopt lfun) lmr)
+ let app_wo_goal =
+ (fun (evc,env,lfun,lmatch,goalopt,debug) goal ->
+ apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal
+ (read_match_context_rule evc env (constr_list goalopt lfun) lmr)) in
+ (match goalopt with
+ | None -> VContext app_wo_goal
+ | Some g -> app_wo_goal (evc,env,lfun,lmatch,goalopt,debug) g)
+
+(* apply_match_context evc env lfun lmatch goal (read_match_context_rule evc env
+ (constr_list goalopt lfun) lmr)*)
(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context evc env lfun_glob lmatch_glob goal debug mt lgmatch
@@ -804,6 +817,14 @@ and apply_hyps_context evc env lfun_glob lmatch_glob goal debug mt lgmatch
apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch mhyps
hyps hyps None
+(* Interprets a VContext value *)
+and vcontext_interp (evc,env,lfun,lmatch,goalopt,debug) = function
+ | (VContext f) as v ->
+ (match goalopt with
+ | None -> v
+ | Some g -> f (evc,env,lfun,lmatch,goalopt,debug) g)
+ | v -> v
+
(* Interprets the Match expressions *)
and match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
let rec apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) nocc (id,c) csr
@@ -1096,25 +1117,24 @@ let bad_tactic_args s =
anomalylabstrm s
[<'sTR "Tactic "; 'sTR s; 'sTR " called with bad arguments">]
-(* Declaration of the TACTIC-DEFINITION object *)
+(* Declaration of the META-DEFINITION object *)
let (inMD,outMD) =
let add (na,td) = mactab := Gmap.add na td !mactab in
let cache_md (_,(na,td)) =
let ve=val_interp (Evd.empty,Environ.empty_env,[],[],None,get_debug ()) td
in add (na,ve) in
- declare_object ("TACTIC-DEFINITION",
+ declare_object ("META-DEFINITION",
{cache_function = cache_md;
load_function = (fun _ -> ());
open_function = cache_md;
export_function = (fun x -> Some x)})
-(* Adds a Tactic Definition in the table *)
-let add_tacdef na vbody =
+(* Adds a Meta Definition in the table *)
+let add_metadef na vbody =
begin
if Gmap.mem na !mactab then
- errorlabstrm "Tacdef.add_tacdef"
- [<'sTR "There is already a Tactic Definition named "; 'sTR na>];
+ errorlabstrm "Tacinterp.add_metadef"
+ [<'sTR "There is already a Meta Definition named "; 'sTR na>];
let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >]
end
-
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index a23f953e6..67bd209e3 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -16,19 +16,20 @@ type value =
| VTactic of tactic
| VFTactic of tactic_arg list * (tactic_arg list -> tactic)
| VRTactic of (goal list sigma * validation)
+ | VContext of (interp_sign -> goal sigma -> value)
| VArg of tactic_arg
| VFun of (string * value) list * string 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 *
+ (int * constr) list * goal sigma option * debug_info
+
(* Gives the constr corresponding to a CONSTR [tactic_arg] *)
val constr_of_Constr : tactic_arg -> constr
-(* Signature for interpretation: [val_interp] and interpretation functions *)
-type interp_sign =
- enamed_declarations * Environ.env * (string * value) list *
- (int * constr) list * goal sigma option * debug_info
-
(* To provide the tactic expressions *)
val loc : Coqast.loc
val tacticIn : (unit -> Coqast.t) -> Coqast.t
@@ -48,8 +49,8 @@ val set_debug : debug_info -> unit
(* Gives the state of debug *)
val get_debug : unit -> debug_info
-(* Adds a Tactic Definition in the table *)
-val add_tacdef : string -> Coqast.t -> unit
+(* Adds a Meta Definition in the table *)
+val add_metadef : string -> Coqast.t -> unit
(* Interprets any expression *)
val val_interp : interp_sign -> Coqast.t -> value