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

4 files changed, 70 insertions, 49 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1cd140ed64..0ee8c7aec1 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -85,20 +85,20 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >>
       | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
 
-(* Tactic Definition *)
+(* Meta Definition *)
 
-      |IDENT "Tactic"; "Definition"; name=identarg; ":="; body=Tactic.tactic;
-        "." -> <:ast<(TACDEF $name (AST $body))>>
-      |IDENT "Tactic"; "Definition"; name=identarg; largs=LIST1 input_fun;
+      |IDENT "Meta"; "Definition"; name=identarg; ":="; body=Tactic.tactic;
+        "." -> <:ast<(METADEF $name (AST $body))>>
+      |IDENT "Meta"; "Definition"; name=identarg; largs=LIST1 input_fun;
         ":="; body=Tactic.tactic; "." ->
-        <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
-      |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause ; "." ->
+        <:ast<(METADEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
+      |IDENT "Recursive"; IDENT "Meta"; "Definition"; vc=vrec_clause ; "." ->
         (match vc with
             Coqast.Node(_,"RECCLAUSE",nme::tl) ->
-              <:ast<(TACDEF $nme (AST (REC $vc)))>>
+              <:ast<(METADEF $nme (AST (REC $vc)))>>
            |_ ->
              anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
-      |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause;
+      |IDENT "Recursive"; IDENT "Meta"; "Definition"; vc=vrec_clause;
         IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." ->
         let nvcl=
           List.fold_right
@@ -109,7 +109,7 @@ GEXTEND Gram
                  anomalylabstrm "Gram.vernac" [<'sTR
                    "Not a correct RECCLAUSE">]) (vc::vcl) []
         in
-          <:ast<(TACDEF ($LIST $nvcl))>>
+          <:ast<(METADEF ($LIST $nvcl))>>
 
 (* Hints for Auto and EAuto *)
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index dd0199c0f0..5d7c46a792 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 a23f953e6c..67bd209e30 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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9ad4fa0121..361cf3d20c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1342,16 +1342,16 @@ let _ =
        | _ -> bad_vernac_args "SYNTAX")
     
 let _ =
-  add "TACDEF"
-    (let rec tacdef_fun lacc=function
+  add "METADEF"
+    (let rec metadef_fun lacc=function
         (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl ->
-          tacdef_fun ((string_of_id name,tacexp)::lacc) tl
+          metadef_fun ((string_of_id name,tacexp)::lacc) tl
        |[] ->
          fun () ->
-           List.iter (fun (name,ve) -> Tacinterp.add_tacdef name ve) lacc
-       |_ -> bad_vernac_args "TACDEF"
+           List.iter (fun (name,ve) -> Tacinterp.add_metadef name ve) lacc
+       |_ -> bad_vernac_args "METADEF"
      in
-       tacdef_fun [])
+       metadef_fun [])
 
 let _ =
   add "INFIX"