Retablissement de interp_tab + injection id -> constr sans goal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2527 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 59 insertions, 22 deletions

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index e58d951c42..dfefece60d 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -118,8 +118,9 @@ let make_qid = function
 let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ))
 
 (* Transforms an id into a constr if possible *)
-let constr_of_id id = function
-  | None -> raise Not_found
+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
@@ -131,21 +132,21 @@ let constr_of_id id = function
       | _ -> csr)
 
 (* Extracted the constr list from lfun *)
-let rec constr_list goalopt = function
-  | (id,VArg(Constr c))::tl -> (id,c)::(constr_list goalopt tl)
+let rec constr_list_aux ist = function
+  | (id,VArg(Constr c))::tl -> (id,c)::(constr_list_aux ist 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
+    (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 ist c ocl =
-  interp_constr_gen ist.evc ist.env
-    (constr_list ist.goalopt ist.lfun) ist.lmatch c ocl
+  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.goalopt ist.lfun) ist.lmatch c ocl
+  interp_openconstr_gen ist.evc ist.env (constr_list ist) ist.lmatch c ocl
 
 (* To embed several objects in Coqast.t *)
 let ((tactic_in : (interp_sign -> Coqast.t) -> Dyn.t),
@@ -181,6 +182,32 @@ 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 glob_const_nvar loc env qid =
   try
@@ -614,7 +641,7 @@ and letin_interp ist ast = function
       (id,VArg (Constr (mkCast (csr,typ))))::(letin_interp ist ast tl)
     | VArg (Identifier id) ->
       (try
-         (id,VArg (Constr (mkCast (constr_of_id id ist.goalopt,typ))))::
+         (id,VArg (Constr (mkCast (constr_of_id ist id,typ))))::
          (letin_interp ist ast tl)
        with | Not_found ->
          errorlabstrm "Tacinterp.letin_interp"
@@ -668,7 +695,7 @@ and letcut_interp ist ast = function
       (try
          let cutt = interp_atomic "Cut" [Constr typ]
          and exat =
-           interp_atomic "Exact" [Constr (constr_of_id ir ist.goalopt)] in
+           interp_atomic "Exact" [Constr (constr_of_id ist ir)] in
          tclTHENS cutt [tclTHEN (introduction id)
          (letcut_interp ist ast tl);exat]
        with | Not_found ->
@@ -762,26 +789,24 @@ and match_context_interp ist ast lmr =
   let app_wo_goal = 
     (fun ist goal ->
        apply_match_context ist goal
-         (read_match_context_rule ist.evc ist.env
-           (constr_list ist.goalopt ist.lfun) lmr)) in
+         (read_match_context_rule ist.evc ist.env (constr_list ist) lmr)) in
 
 (*    (fun goal ->
        let evc = project goal
        and env = pf_env goal in
        apply_match_context ist goal
-         (read_match_context_rule ist.evc ist.env
-           (constr_list ist.goalopt ist.lfun) lmr)) in*)
+         (read_match_context_rule ist.evc ist.env (constr_list ist) lmr)) in*)
 
 (*    (fun ist goal ->
      apply_match_context ist goal
-     (read_match_context_rule evc env (constr_list goalopt lfun) lmr)) in*)
+     (read_match_context_rule evc env (constr_list ist) lmr)) in*)
 
  (match ist.goalopt with
     | None -> VContext app_wo_goal
     | Some g -> app_wo_goal ist g)
 
-(*  apply_match_context evc env lfun lmatch goal (read_match_context_rule evc env
-    (constr_list goalopt lfun) lmr)*)
+(*  apply_match_context evc env lfun lmatch goal (read_match_context_rule evc
+      env (constr_list ist) lmr)*)
 
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist mt lgmatch mhyps hyps =
@@ -892,8 +917,7 @@ and match_interp ist ast lmr =
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for Match") in
   let csr = constr_of_Constr (unvarg (val_interp ist (List.hd lmr)))
-  and ilr = read_match_rule ist.evc ist.env (constr_list ist.goalopt ist.lfun)
-    (List.tl lmr) in
+  and ilr = read_match_rule ist.evc ist.env (constr_list ist) (List.tl lmr) in
   apply_match ist csr ilr
 
 and tactic_interp ist ast g =
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 631d7e0af2..0c82af6bbd 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -38,9 +38,15 @@ and interp_sign =
     goalopt : goal sigma option;
     debug : debug_info }
 
+(* Gives the identifier corresponding to an Identifier [tactic_arg] *)
+val id_of_Identifier : tactic_arg -> identifier
+
 (* Gives the constr corresponding to a Constr [tactic_arg] *)
 val constr_of_Constr : tactic_arg -> 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 -> Coqast.t) -> Coqast.t
 val tacticOut : Coqast.t -> (interp_sign -> Coqast.t)
@@ -75,5 +81,12 @@ val interp : Coqast.t -> tactic
 (* Hides interpretation for pretty-print *)
 val hide_interp : Coqast.t -> 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
+
 (* For bad tactic calls *)
 val bad_tactic_args : string -> 'a