- Changement de l'ordre de filtrage dans "Match Context"

- Protection des "Match Context" contre les exceptions non UserError ni Fail
- Remplacement des fermetures ML dans VTactic et VFTactic par des
  expressions de tactiques pour permettre l'intégration de Tactic
  Definition dans les états
- Changement en conséquence de Tauto


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

3 files changed, 90 insertions, 68 deletions

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 2343351c4e..967261d7b3 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -41,8 +41,8 @@ let err_msg_tactic_not_found macro_loc macro =
 
 (* Values for interpretation *)
 type value =
-  | VTactic of tactic
-  | VFTactic of tactic_arg list * (tactic_arg list->tactic)
+  | VTactic of interp_sign * Coqast.t
+  | VFTactic of tactic_arg list * string
   | VRTactic of (goal list sigma * validation)
   | VContext of (interp_sign -> goal sigma -> value)
   | VArg of tactic_arg
@@ -62,14 +62,6 @@ and interp_sign =
 (* For tactic_of_value *)
 exception NotTactic
 
-(* Gives the tactic corresponding to the tactic value *)
-let tactic_of_value vle g =
-  match vle with
-  | VTactic tac -> (tac g)
-  | VFTactic (largs,f) -> (f largs g) 
-  | VRTactic res -> res
-  | _ -> raise NotTactic
-
 (* Gives the identifier corresponding to an Identifier tactic_arg *)
 let id_of_Identifier = function
   | Identifier id -> id
@@ -394,18 +386,9 @@ let rec read_match_rule evc env lfun = function
 exception No_match
 exception Not_coherent_metas
 
-(* Evaluation with FailError catching *)
-let eval_with_fail interp ast goal =
-  try 
-    (match interp ast with
-    | VTactic tac -> VRTactic (tac goal)
-    | VFTactic (largs,f) -> VRTactic (f largs goal)
-    | a -> a)
-  with | FailError lvl ->
-    if lvl = 0 then
-      raise No_match
-    else
-      raise (FailError (lvl - 1))
+let is_match_catchable = function
+  | No_match | FailError _ -> true
+  | e -> Logic.catchable_exception e
 
 (* Verifies if the matched list is coherent with respect to lcm *)
 let rec verify_metas_coherence ist lcm = function
@@ -490,6 +473,7 @@ let rec val_interp ist ast =
 
   let value_interp ist =
   match ast with
+    (* Immediate evaluation *)
     | Node(_,"APP",l) ->
         let fv = val_interp ist (List.hd l)
         and largs = List.map (val_interp ist) (List.tl l) in
@@ -499,32 +483,11 @@ let rec val_interp ist ast =
     | Node(_,"LET",[Node(_,"LETDECL",l);u]) ->
         let addlfun=letin_interp ist ast l in
         val_interp { ist with lfun=addlfun@ist.lfun } u
-    | Node(_,"LETCUT",[Node(_,"LETDECL",l)]) ->
-        VTactic (letcut_interp ist ast l)
     | Node(_,"MATCHCONTEXT",lmr) -> match_context_interp ist ast lmr
     | Node(_,"MATCH",lmr) -> match_interp ist ast lmr
-    | Node(_,"IDTAC",[]) -> VTactic tclIDTAC
-    | Node(_,"FAIL",[]) -> VTactic (tclFAIL 0)
-    | Node(_,"FAIL",[n]) -> VTactic (tclFAIL (num_of_ast n))
-    | Node(_,"PROGRESS",[tac]) ->
-        VTactic (tclPROGRESS (tactic_interp ist tac))
-    | Node(_,"TACTICLIST",l) ->
-        VTactic (interp_semi_list tclIDTAC ist.lfun ist.lmatch ist.debug l)
-    | Node(_,"DO",[n;tac]) ->
-        VTactic (tclDO (num_of_ast n) (tactic_interp ist tac))
-    | Node(_,"TRY",[tac]) -> VTactic (tclTRY (tactic_interp ist tac))
-    | Node(_,"INFO",[tac]) -> VTactic (tclINFO (tactic_interp ist tac))
-    | Node(_,"REPEAT",[tac]) -> VTactic (tclREPEAT (tactic_interp ist tac))
-    | Node(_,"ORELSE",[tac1;tac2]) ->
-        VTactic (tclORELSE (tactic_interp ist tac1) (tactic_interp ist tac2))
-    | Node(_,"FIRST",l) -> VTactic (tclFIRST (List.map (tactic_interp ist) l))
-    | Node(_,"TCLSOLVE",l) ->
-        VTactic (tclSOLVE (List.map (tactic_interp ist) l))
-(*    | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
-        val_interp ist
-          (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))*)
-    | Node(_,"PRIMTACTIC",[Node(loc,opn,[])]) ->
-        VFTactic ([],(interp_atomic opn))
+    (* Delayed evaluation *)
+    | Node(loc,("LETCUT"|"IDTAC"|"FAIL"|"PROGRESS"|"TACTICLIST"|"DO"|"TRY"|"INFO"|"REPEAT"|"ORELSE"|"FIRST"|"TCLSOLVE"),_) -> VTactic (ist,ast)
+    (* Arguments and primitive tactics *)
     | Node(_,"VOID",[]) -> VVoid
     | Nvar(_,s) ->
         (try (unrec (List.assoc s ist.lfun))
@@ -561,17 +524,16 @@ let rec val_interp ist ast =
     | Node(_,"LETPATTERNS",astl) ->
         VArg (Letpatterns (List.fold_left (cvt_letpattern ist) (None,[]) astl))
     | Node(loc,s,[]) ->
-        VFTactic ([],(interp_atomic s))
+        VFTactic ([],s)
     | Node(loc,s,l) ->
         (try
           ((look_for_interp s) ist ast)
         with
            Not_found ->
              if l = [] then
-               VFTactic ([],(interp_atomic s))
+               VFTactic ([],s)
              else
-               let fv = val_interp ist
-                          (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
+               let fv = VFTactic ([],s)
                and largs = List.map (val_interp ist) l in
                app_interp ist fv largs ast)
     | Dynamic(_,t) ->
@@ -590,11 +552,36 @@ let rec val_interp ist ast =
           (str "Unrecognizable ast: " ++ print_ast ast)) in
   if ist.debug = DebugOn then
     match debug_prompt ist.goalopt ast with
-    | Exit -> VTactic tclIDTAC
+    | Exit -> VTactic (ist,Node(dummy_loc,"IDTAC",[]))
     | v -> value_interp {ist with debug=v}
   else
     value_interp ist
 
+and eval_tactic ist ast =
+  match ast with
+    | Node(_,"LETCUT",[Node(_,"LETDECL",l)]) -> letcut_interp ist ast l
+    | Node(_,"IDTAC",[]) -> tclIDTAC
+    | Node(_,"FAIL",[]) -> tclFAIL 0
+    | Node(_,"FAIL",[n]) -> tclFAIL (num_of_ast n)
+    | Node(_,"PROGRESS",[tac]) -> tclPROGRESS (tactic_interp ist tac)
+    | Node(_,"TACTICLIST",l) ->
+	interp_semi_list tclIDTAC ist.lfun ist.lmatch ist.debug l
+    | Node(_,"DO",[n;tac]) ->
+        tclDO (num_of_ast n) (tactic_interp ist tac)
+    | Node(_,"TRY",[tac]) -> tclTRY (tactic_interp ist tac)
+    | Node(_,"INFO",[tac]) -> tclINFO (tactic_interp ist tac)
+    | Node(_,"REPEAT",[tac]) -> tclREPEAT (tactic_interp ist tac)
+    | Node(_,"ORELSE",[tac1;tac2]) ->
+        tclORELSE (tactic_interp ist tac1) (tactic_interp ist tac2)
+    | Node(_,"FIRST",l) -> tclFIRST (List.map (tactic_interp ist) l)
+    | Node(_,"TCLSOLVE",l) -> tclSOLVE (List.map (tactic_interp ist) l)
+(*    | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
+        val_interp ist
+          (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))*)
+    | _ ->
+        anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",
+          (str "Unrecognizable ast: " ++ print_ast ast))
+
 (* Interprets an application node *)
 and app_interp ist fv largs ast =
   match fv with
@@ -613,6 +600,27 @@ and app_interp ist fv largs ast =
       user_err_loc (Ast.loc ast, "Tacinterp.app_interp",
                     (str"Illegal tactic application: " ++ print_ast ast))
 
+(* Gives the tactic corresponding to the tactic value *)
+and tactic_of_value vle g =
+  match vle with
+  | VTactic (ist,tac) -> eval_tactic ist tac g
+  | VFTactic (largs,f) -> (interp_atomic f largs g) 
+  | VRTactic res -> res
+  | _ -> raise NotTactic
+
+(* Evaluation with FailError catching *)
+and eval_with_fail interp ast goal =
+  try 
+    (match interp ast with
+    | VTactic (ist,tac) -> VRTactic (eval_tactic ist tac goal)
+    | VFTactic (largs,f) -> VRTactic (interp_atomic f largs goal)
+    | a -> a)
+  with | FailError lvl ->
+    if lvl = 0 then
+      raise No_match
+    else
+      raise (FailError (lvl - 1))
+
 (* Interprets recursive expressions *)
 and rec_interp ist ast = function
   | [Node(_,"RECCLAUSE",_)] as l ->
@@ -781,7 +789,7 @@ and match_context_interp ist ast lmr =
        with No_match | _ ->
          apply_match_context ist goal tl)
     | (Pat (mhyps,mgoal,mt))::tl ->
-      let hyps = make_hyps (List.rev (pf_hyps goal))
+      let hyps = make_hyps (pf_hyps goal)
       and concl = pf_concl goal in
       (match mgoal with
       |	Term mg ->
@@ -796,12 +804,11 @@ and match_context_interp ist ast lmr =
               apply_hyps_context { ist with goalopt=Some goal} mt lgoal mhyps
                 hyps
             end)
-         with | No_match | _ -> apply_match_context ist goal tl)
+         with e when is_match_catchable e -> apply_match_context ist goal tl)
       |	Subterm (id,mg) ->
         (try
           apply_goal_sub ist goal 0 (id,mg) concl mt mhyps hyps
-         with
-        | No_match | _ -> apply_match_context ist goal tl))
+         with e when is_match_catchable e -> apply_match_context ist goal tl))
     | _ ->
       errorlabstrm "Tacinterp.apply_match_context" (str
         "No matching clauses for Match Context") in
@@ -853,7 +860,7 @@ and apply_hyps_context ist mt lgmatch mhyps hyps =
             (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
          with
         | (FailError _) as e -> raise e
-        | _ ->
+	|  e when is_match_catchable e -> 
           (match noccopt with
           | None ->
             apply_hyps_context_rec ist mt lfun
@@ -896,20 +903,21 @@ and match_interp ist ast lmr =
        with
        | NextOccurrence n -> raise No_match
        | (FailError _) as e -> raise e
-       | _ -> apply_sub_match ist (nocc + 1) (id,c) csr mt)
+       | e when is_match_catchable e ->
+	   apply_sub_match ist (nocc + 1) (id,c) csr mt)
   in
   let rec apply_match ist csr = function
     | (All t)::_ ->
       (match ist.goalopt with
         | None ->
           (try val_interp ist t
-           with | No_match | _ -> apply_match ist csr [])
+           with e when is_match_catchable e -> apply_match ist csr [])
         | Some g ->
           (try
             eval_with_fail (val_interp ist) t g
            with
            | (FailError _) as e -> raise e
-           | _ -> apply_match ist csr []))
+           | e when is_match_catchable e -> apply_match ist csr []))
     | (Pat ([],mp,mt))::tl ->
       (match mp with
       |	Term c ->
@@ -918,7 +926,7 @@ and match_interp ist ast lmr =
           (try
              val_interp
                { ist with lmatch=(apply_matching c csr)@ist.lmatch } mt
-           with | No_match | _ ->
+           with | e when is_match_catchable e ->
              apply_match ist csr tl)
         | Some g ->
           (try
@@ -926,7 +934,7 @@ and match_interp ist ast lmr =
               { ist with lmatch=(apply_matching c csr)@ist.lmatch }) mt g
            with
            | (FailError _) as e -> raise e
-           | _ -> apply_match ist csr tl))
+           | e when is_match_catchable e -> apply_match ist csr tl))
       |	Subterm (id,c) ->
         (try
            apply_sub_match ist 0 (id,c) csr mt
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 0c82af6bbd..0f52803446 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -20,8 +20,8 @@ open Term
 
 (* Values for interpretation *)
 type value =
-  | VTactic of tactic
-  | VFTactic of tactic_arg list * (tactic_arg list -> tactic)
+  | VTactic of interp_sign * Coqast.t
+  | VFTactic of tactic_arg list * string
   | VRTactic of (goal list sigma * validation)
   | VContext of (interp_sign -> goal sigma -> value)
   | VArg of tactic_arg
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index eea887e727..56f7607235 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -25,25 +25,25 @@ let is_empty ist =
   if (is_empty_type (List.assoc 1 ist.lmatch)) then
     <:tactic<ElimType ?1;Assumption>>
   else
-    failwith "is_empty"
+    <:tactic<Fail>>
 
 let is_unit ist =
   if (is_unit_type (List.assoc 1 ist.lmatch)) then
     <:tactic<Idtac>>
   else
-    failwith "is_unit"
+    <:tactic<Fail>>
 
 let is_conj ist =
   if (is_conjunction (List.assoc 1 ist.lmatch)) then
      <:tactic<Idtac>>
   else
-    failwith "is_conj"
+    <:tactic<Fail>>
 
 let is_disj ist =
   if (is_disjunction (List.assoc 1 ist.lmatch)) then
      <:tactic<Idtac>>
   else
-    failwith "is_disj"
+    <:tactic<Fail>>
 
 let not_dep_intros ist =
   <:tactic<
@@ -109,6 +109,7 @@ let rec tauto_intuit t_reduce t_solver ist =
       $t_solver
    ) >>
 
+(*
 let unfold_not_iff = function
   | None -> interp <:tactic<Unfold not iff>>
   | Some id ->
@@ -118,12 +119,25 @@ let unfold_not_iff = function
 let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
 
 let t_reduction_not_iff = valueIn (VTactic reduction_not_iff)
+*)
+
+let reduction_not_iff ist =
+  match ist.goalopt with 
+    | None -> anomaly "reduction_not_iff"
+    | Some gl ->
+	List.fold_right
+	(fun id tac -> 
+	  let id = nvar id in <:tactic<Unfold not iff in $id; $tac>>)
+	(Tacmach.pf_ids_of_hyps gl)
+	<:tactic<Unfold not iff>>
+
+let t_reduction_not_iff = tacticIn reduction_not_iff
 
 let intuition_gen tac =
   interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
 
 let tauto g =
-  try intuition_gen <:tactic<Failtac>> g
+  try intuition_gen <:tactic<Fail>> g
   with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >]
 
 let default_intuition_tac = <:tactic< Auto with * >>