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

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