module Tactics (debut)

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

9 files changed, 94 insertions, 51 deletions

diff --git a/.depend b/.depend
index e8107997ea..f215a33d94 100644
--- a/.depend
+++ b/.depend
@@ -38,6 +38,8 @@ library/global.cmi: kernel/constant.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/typing.cmi kernel/univ.cmi 
 library/impargs.cmi: kernel/names.cmi 
+library/indrec.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
+    kernel/names.cmi kernel/term.cmi 
 library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi 
 library/libobject.cmi: kernel/names.cmi 
 library/library.cmi: lib/pp.cmi 
@@ -87,6 +89,9 @@ tactics/stock.cmi: kernel/names.cmi
 tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi tactics/pattern.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
     proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi 
+tactics/tactics.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \
+    proofs/proof_trees.cmi kernel/reduction.cmi proofs/tacmach.cmi \
+    proofs/tacred.cmi tactics/tacticals.cmi kernel/term.cmi 
 tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi 
 tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \
     proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
@@ -235,8 +240,12 @@ library/declare.cmx: kernel/constant.cmx kernel/generic.cmx \
     library/lib.cmx library/libobject.cmx kernel/names.cmx \
     library/nametab.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
     library/declare.cmi 
-library/global.cmo: library/summary.cmi kernel/typing.cmi library/global.cmi 
-library/global.cmx: library/summary.cmx kernel/typing.cmx library/global.cmi 
+library/global.cmo: kernel/generic.cmi kernel/inductive.cmi \
+    kernel/instantiate.cmi kernel/sign.cmi library/summary.cmi \
+    kernel/term.cmi kernel/typing.cmi lib/util.cmi library/global.cmi 
+library/global.cmx: kernel/generic.cmx kernel/inductive.cmx \
+    kernel/instantiate.cmx kernel/sign.cmx library/summary.cmx \
+    kernel/term.cmx kernel/typing.cmx lib/util.cmx library/global.cmi 
 library/impargs.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi kernel/inductive.cmi kernel/names.cmi \
     kernel/reduction.cmi library/summary.cmi kernel/term.cmi \
@@ -245,6 +254,12 @@ library/impargs.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
     library/global.cmx kernel/inductive.cmx kernel/names.cmx \
     kernel/reduction.cmx library/summary.cmx kernel/term.cmx \
     kernel/typing.cmx library/impargs.cmi 
+library/indrec.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
+    kernel/term.cmi kernel/typing.cmi lib/util.cmi library/indrec.cmi 
+library/indrec.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+    kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
+    kernel/term.cmx kernel/typing.cmx lib/util.cmx library/indrec.cmi 
 library/lib.cmo: library/libobject.cmi kernel/names.cmi library/summary.cmi \
     lib/util.cmi library/lib.cmi 
 library/lib.cmx: library/libobject.cmx kernel/names.cmx library/summary.cmx \
@@ -405,16 +420,30 @@ tactics/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \
     kernel/names.cmx lib/pp.cmx lib/util.cmx tactics/stock.cmi 
 tactics/tacticals.cmo: proofs/clenv.cmi library/declare.cmi \
     kernel/environ.cmi kernel/generic.cmi library/global.cmi \
-    kernel/inductive.cmi kernel/names.cmi tactics/pattern.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi tactics/wcclausenv.cmi \
-    tactics/tacticals.cmi 
+    library/indrec.cmi kernel/inductive.cmi kernel/names.cmi \
+    tactics/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
+    lib/util.cmi tactics/wcclausenv.cmi tactics/tacticals.cmi 
 tactics/tacticals.cmx: proofs/clenv.cmx library/declare.cmx \
     kernel/environ.cmx kernel/generic.cmx library/global.cmx \
-    kernel/inductive.cmx kernel/names.cmx tactics/pattern.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi \
-    tactics/tacticals.cmi 
+    library/indrec.cmx kernel/inductive.cmx kernel/names.cmx \
+    tactics/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
+    lib/util.cmx tactics/wcclausenv.cmi tactics/tacticals.cmi 
+tactics/tactics.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \
+    kernel/evd.cmi kernel/generic.cmi library/global.cmi library/indrec.cmi \
+    kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi \
+    tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi kernel/sign.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi proofs/tacred.cmi tactics/tacticals.cmi \
+    kernel/term.cmi lib/util.cmi tactics/tactics.cmi 
+tactics/tactics.cmx: proofs/clenv.cmx library/declare.cmx kernel/environ.cmx \
+    kernel/evd.cmx kernel/generic.cmx library/global.cmx library/indrec.cmx \
+    kernel/inductive.cmx proofs/logic.cmx kernel/names.cmx \
+    tactics/pattern.cmx proofs/pfedit.cmi lib/pp.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx kernel/sign.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx proofs/tacred.cmx tactics/tacticals.cmx \
+    kernel/term.cmx lib/util.cmx tactics/tactics.cmi 
 tactics/termdn.cmo: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi \
     lib/util.cmi tactics/termdn.cmi 
 tactics/termdn.cmx: tactics/dn.cmx kernel/generic.cmx kernel/term.cmx \
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a0294029a6..429d626f1f 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -48,6 +48,7 @@ let mis_kelim mis = mis.mis_mip.mind_kelim
 let mis_recargs mis =
   Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
 let mis_recarg mis = mis.mis_mip.mind_listrec
+let mis_typename mis = mis.mis_mip.mind_typename
 
 let mind_nth_type_packet mib n = mib.mind_packets.(n)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 51df826044..46c781eea0 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -55,6 +55,7 @@ val mis_nparams : mind_specif -> int
 val mis_kelim : mind_specif -> sorts list
 val mis_recargs : mind_specif -> (recarg list) array array
 val mis_recarg : mind_specif -> (recarg list) array
+val mis_typename : mind_specif -> identifier
 
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
diff --git a/library/declare.ml b/library/declare.ml
index 2220632c66..ff006625a1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -172,6 +172,13 @@ let global_reference kind id =
   let ids =  ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
 
+let is_global id =
+  try 
+    let osp = Nametab.sp_of_id CCI id in
+    prefix_of (dirpath osp) (Lib.cwd())
+  with Not_found -> 
+    false
+
 let mind_path = function
   | DOPN(MutInd (sp,0),_) -> sp
   | DOPN(MutInd (sp,tyi),_) -> 
diff --git a/library/declare.mli b/library/declare.mli
index 3a1e7884fb..c2944c330a 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -36,4 +36,6 @@ val declare_mind : mutual_inductive_entry -> unit
 
 val global_reference : path_kind -> identifier -> constr
 
+val is_global : identifier -> bool
+
 val mind_path : constr -> section_path
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 7056dadf17..e619c70b00 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -21,6 +21,7 @@ type refiner_error =
   | OccurMeta of constr
   | CannotApply of constr * constr
   | CannotUnify of constr * constr
+  | BadTacticArgs of string * tactic_arg list
 
 exception RefinerError of refiner_error
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index cbd94b52b1..d8c71f7605 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -28,5 +28,8 @@ type refiner_error =
   | OccurMeta of constr
   | CannotApply of constr * constr
   | CannotUnify of constr * constr
+  | BadTacticArgs of string * tactic_arg list
+
+exception RefinerError of refiner_error
 
 val error_cannot_unify : path_kind -> constr * constr -> 'a
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f3054b3cc7..8bb6fba486 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -271,14 +271,14 @@ let overwrite_hidden_tactic s tac  =
   overwriting_add_tactic s tac;
   (fun args -> vernac_tactic(s,args))
 
-
+(*** 
 let tactic_com = 
   fun tac t x -> tac (pf_constr_of_com x t) x
       
 let tactic_com_sort = 
   fun tac t x -> tac (pf_constr_of_com_sort x t) x
       
-let tactic_com_list =
+let tactic_com_list =    
   fun tac tl x -> 
     let translate = pf_constr_of_com x in 
     tac (List.map translate tl) x
@@ -301,7 +301,6 @@ let tactic_com_bind_list_list =
     in 
     tac (List.map translate args) gl
 
-
 (* Some useful combinators for hiding tactic implementations *)
 
 type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic)
@@ -317,106 +316,107 @@ let overwrite_hidden_atomic_tactic s tac =
 
 let hide_constr_comarg_tactic s tac =
   let tacfun = function 
-    | [CONSTR c]    -> tac c
-    | [COMMAND com] -> tactic_com tac com
+    | [Constr c]    -> tac c
+    | [Command com] -> tactic_com tac com
     | _ -> anomaly "hide_constr_comarg_tactic : neither CONSTR nor COMMAND"
   in 
   add_tactic s tacfun;
-  (fun c   -> vernac_tactic(s,[(CONSTR c)])), 
-  fun com -> vernac_tactic(s,[(COMMAND com)])
+  (fun c -> vernac_tactic(s,[Constr c]),
+   fun com -> vernac_tactic(s,[Command com]))
  
 let overwrite_hidden_constr_comarg_tactic s tac =
   let tacfun = function 
-    | [CONSTR c] -> tac c
-    | [COMMAND com] -> 
+    | [Constr c] -> tac c
+    | [Command com] -> 
         (fun gls -> tac (pf_constr_of_com gls com) gls)
     | _ -> 
 	anomaly 
 	  "overwrite_hidden_constr_comarg_tactic : neither CONSTR nor COMMAND"
   in 
   overwriting_tactic s tacfun;
-  (fun c -> vernac_tactic(s,[(CONSTR c)]), 
-   fun c -> vernac_tactic(s,[(COMMAND c)]))
+  (fun c -> vernac_tactic(s,[(Constr c)]), 
+   fun c -> vernac_tactic(s,[(Command c)]))
 
 let hide_constr_tactic s tac =
   let tacfun = function 
-    | [CONSTR c]    -> tac c
-    | [COMMAND com] -> tactic_com tac com
+    | [Constr c]    -> tac c
+    | [Command com] -> tactic_com tac com
     | _ -> anomaly "hide_constr_tactic : neither CONSTR nor COMMAND"
   in 
   add_tactic s tacfun;
-  (fun c  -> vernac_tactic(s,[(CONSTR c)]))
+  (fun c  -> vernac_tactic(s,[(Constr c)]))
 
 let hide_numarg_tactic s tac =
-  let tacfun = (function [INTEGER n] -> tac n | _ -> assert false) in 
+  let tacfun = (function [Integer n] -> tac n | _ -> assert false) in 
   add_tactic s tacfun;
-  fun n -> vernac_tactic(s,[INTEGER n])
+  fun n -> vernac_tactic(s,[Integer n])
 
 let hide_ident_tactic s tac =
-  let tacfun = (function [IDENTIFIER id] -> tac id | _ -> assert false) in
+  let tacfun = (function [Identifier id] -> tac id | _ -> assert false) in
   add_tactic s tacfun;
-  fun id -> vernac_tactic(s,[IDENTIFIER id])
+  fun id -> vernac_tactic(s,[Identifier id])
       
 let hide_string_tactic s tac =
-  let tacfun = (function [QUOTED_STRING str] -> tac str | _ -> assert false) in
+  let tacfun = (function [Quoted_string str] -> tac str | _ -> assert false) in
   add_tactic s tacfun;
-  fun str -> vernac_tactic(s,[QUOTED_STRING str])
+  fun str -> vernac_tactic(s,[Quoted_string str])
 
 let hide_identl_tactic s tac =
-  let tacfun = (function [CLAUSE idl] -> tac idl | _ -> assert false) in 
+  let tacfun = (function [Clause idl] -> tac idl | _ -> assert false) in 
   add_tactic s tacfun;
-  fun idl -> vernac_tactic(s,[CLAUSE idl])
+  fun idl -> vernac_tactic(s,[Clause idl])
 
 let hide_constrl_tactic s tac = 
   let tacfun = function 
-    | ((COMMAND com)::_) as al -> 
+    | ((Command com)::_) as al -> 
       	tactic_com_list tac 
-          (List.map (function (COMMAND com) -> com | _ -> assert false) al)
-    | ((CONSTR com)::_) as al ->
-      	tac (List.map (function (CONSTR c) -> c | _ -> assert false) al)
+          (List.map (function (Command com) -> com | _ -> assert false) al)
+    | ((Constr com)::_) as al ->
+      	tac (List.map (function (Constr c) -> c | _ -> assert false) al)
     | _ -> anomaly "hide_constrl_tactic : neither CONSTR nor COMMAND"
   in 
   add_tactic s tacfun;
-  fun ids -> vernac_tactic(s,(List.map (fun id -> CONSTR id) ids))
+  fun ids -> vernac_tactic(s,(List.map (fun id -> Constr id) ids))
 
 let hide_bindl_tactic s tac = 
   let tacfun = function  
-    | [(BINDINGS  al)] -> tactic_bind_list tac al
-    | [(CBINDINGS al)] -> tac al
+    | [Bindings  al] -> tactic_bind_list tac al
+    | [Cbindings al] -> tac al
     | _ -> anomaly "hide_bindl_tactic : neither BINDINGS nor CBINDINGS"
   in 
   add_tactic s tacfun;
-  fun bindl -> vernac_tactic(s,[(CBINDINGS bindl)])
+  fun bindl -> vernac_tactic(s,[Cbindings bindl])
       
 let hide_cbindl_tactic s tac = 
   let tacfun = function 
-    | [(COMMAND com);(BINDINGS al)] -> tactic_com_bind_list tac (com,al)
-    | [(CONSTR  c);(CBINDINGS al)]  -> tac (c,al)
+    | [Command com; Bindings al] -> tactic_com_bind_list tac (com,al)
+    | [Constr c; Cbindings al]  -> tac (c,al)
     | _ -> anomaly "hide_cbindl_tactic : neither CONSTR nor COMMAND"
   in 
   add_tactic s tacfun;
-  fun (c,bindl) -> vernac_tactic(s,[(CONSTR c);(CBINDINGS bindl)])
+  fun (c,bindl) -> vernac_tactic(s,[Constr c; Cbindings bindl])
       
 let hide_cbindll_tactic s tac = 
   let rec getcombinds = function 
-    | ((COMMAND com)::(BINDINGS al)::l) -> (com,al)::(getcombinds l)
+    | ((Command com)::(Bindings al)::l) -> (com,al)::(getcombinds l)
     | []                                ->  [] 
     | _ -> anomaly "hide_cbindll_tactic : not the expected form" 
   in  
   let rec getconstrbinds = function
-    | ((CONSTR c)::(CBINDINGS al)::l) -> (c,al)::(getconstrbinds l)
-    |  []                             ->  [] 
+    | ((Constr c)::(Cbindings al)::l) -> (c,al)::(getconstrbinds l)
+    | []                              ->  [] 
     | _ -> anomaly "hide_cbindll_tactic : not the expected form" 
   in  
   let rec putconstrbinds = function 
-    | (c,binds)::l -> (CONSTR c)::(CBINDINGS binds)::(putconstrbinds l)
+    | (c,binds)::l -> (Constr c)::(Cbindings binds)::(putconstrbinds l)
     |  []          -> [] 
   in
   let tacfun = function 
-    | ((COMMAND com)::_) as args -> 
+    | ((Command com)::_) as args -> 
       	tactic_com_bind_list_list tac (getcombinds args)
-    | ((CONSTR com)::_) as args -> tac (getconstrbinds args)
+    | ((Constr com)::_) as args -> tac (getconstrbinds args)
     | _ -> anomaly "hide_cbindll_tactic : neither CONSTR nor COMMAND"
   in 
   add_tactic s tacfun;
   fun l -> vernac_tactic(s,putconstrbinds l)
+***)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a3480cc18d..863023b79a 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -45,8 +45,7 @@ val pf_get_hyp             : goal sigma -> identifier -> constr
 
 val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
 
-val pf_reduce : (evar_declarations -> constr -> constr) 
-                -> goal sigma -> constr -> constr
+val pf_reduce : 'a reduction_function -> goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
 val pf_whd_betadeltaiota_stack : goal sigma -> 'a stack_reduction_function