debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes

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

6 files changed, 98 insertions, 70 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 2dc69c55bf..6358366b7b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -22,6 +22,7 @@ open Hiddentac
 open Libobject
 open Library
 open Vernacinterp
+open Printer
 
 (****************************************************************************)
 (*            The Type of Constructions Autotactic Hints                    *)
@@ -33,7 +34,7 @@ type auto_tactic =
   | Give_exact of constr                  
   | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
   | Unfold_nth of constr                 (* Hint Unfold *)
-  | Extern of CoqAst.t                   (* Hint Extern *) 
+  | Extern of Coqast.t                   (* Hint Extern *) 
 
 type pri_auto_tactic = { 
   hname : identifier;    (* name of the hint *)
@@ -120,9 +121,9 @@ end
 
 type frozen_hint_db_table = Hint_db.t Stringmap.t 
 
-type hint_db_table = Hint_db.t Stringmap.t
+type hint_db_table = Hint_db.t Stringmap.t ref
 
-let searchtable  = ref (Stringmap.empty : hint_db_table)
+let searchtable = (ref Stringmap.empty : hint_db_table)
 
 let searchtable_map name = 
   Stringmap.find name !searchtable
@@ -190,7 +191,7 @@ let make_exact_entry name (c,cty) =
 	 { hname=name; pri=0; pat=None; code=Give_exact c })
 
 let make_apply_entry (eapply,verbose) name (c,cty) =
-  match hnf_constr (Global.unsafe_env()) Evd.empty cty with
+  match hnf_constr (Global.env()) Evd.empty cty with
     | DOP2(Prod,_,_) as cty ->
         let hdconstr = (try  List.hd (head_constr_bound cty [])  
                         with Bound -> failwith "make_apply_entry") in
@@ -227,7 +228,7 @@ let make_resolves name eap (c,cty) =
       [make_exact_entry; make_apply_entry eap]
   in 
   if ents = [] then 
-    errorlabstrm "Hint" [< pTERM c; 'sPC; 'sTR "cannot be used as a hint" >];
+    errorlabstrm "Hint" [< prterm c; 'sPC; 'sTR "cannot be used as a hint" >];
   ents
 
 (* used to add an hypothesis to the local hint database *)
@@ -246,7 +247,7 @@ let add_resolves clist dbnames =
 	    (dbname,
      	     (List.flatten
 		(List.map (fun (name,c) -> 
-			     let env = Global.unsafe_env() in
+			     let env = Global.env() in
 			     let ty = type_of env Evd.empty c in
 			     make_resolves name (true,true) (c,ty)) clist))
 	    )))
@@ -284,21 +285,21 @@ let make_extern name pri pat tacast =
 let add_extern name pri pat tacast dbname =
   (* We check that all metas that appear in tacast have at least
      one occurence in the left pattern pat *)
-  let tacmetas = CoqAst.collect_metas tacast in 
+  let tacmetas = Coqast.collect_metas tacast in 
   let patmetas = Clenv.collect_metas pat in
-  match (subtract tacmetas patmetas) with
+  match (list_subtract tacmetas patmetas) with
     | i::_ ->
 	errorlabstrm "add_extern" 
 	  [< 'sTR "The meta-variable ?"; 'iNT i; 'sTR" is not bound" >]
     | []  ->
-	add_anonymous_object 
+	Lib.add_anonymous_leaf
 	  (inAutoHint(dbname, [make_extern name pri pat tacast]))
 
 let add_externs name pri pat tacast dbnames = 
   List.iter (add_extern name pri pat tacast) dbnames
 
 let make_trivial (name,c) =
-  let sigma = Evd.empty and env = Global.unsafe_env() in
+  let sigma = Evd.empty and env = Global.env() in
   let t = type_of env sigma c in
   let hdconstr = List.hd (head_constr t) in
   let ce = mk_clenv_from () (c,hnf_constr env sigma t) in
@@ -329,7 +330,7 @@ let _ =
     "HintResolve"
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] ->
-	   let c1 = Trad.constr_of_com (Evd.mt_evd()) (initial_sign()) c in
+	   let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 		      	 | _ -> bad_vernac_args "HintResolve") l in
@@ -341,7 +342,7 @@ let _ =
     "HintImmediate"
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] ->
-	   let c1 = Trad.constr_of_com (Evd.mt_evd()) (initial_sign()) c in
+	   let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 			 | _ -> bad_vernac_args "HintImmediate") l in
@@ -377,7 +378,7 @@ let _ =
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l;
 	  VARG_NUMBER pri; VARG_COMMAND patcom; VARG_TACTIC tacexp] ->
            let pat = Pattern.raw_sopattern_of_compattern 
-		       (initial_sign()) patcom in
+		       (Global.env()) patcom in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 		      	 | _ -> bad_vernac_args "HintConstructors") l in
@@ -507,7 +508,7 @@ let fmt_hint_term cl =
 		      'sTR " :"; 'fNL;
 		      fmt_hint_list hintlist >])
 	   valid_dbs >]
-  with BOUND | Match_failure _ | Failure _ -> 
+  with Bound | Match_failure _ | Failure _ -> 
     [<'sTR "No hint applicable for current goal" >]
 	  
 let print_hint_term cl = pPNL (fmt_hint_term cl)
@@ -542,29 +543,29 @@ let print_searchtable () =
     !searchtable
 
 let _ = 
-  vinterp_add("PrintHint",
-	      function 
-		| [] -> fun () -> print_searchtable()
-	        | _ -> assert false)
+  vinterp_add "PrintHint"
+    (function 
+       | [] -> fun () -> print_searchtable()
+       | _ -> bad_vernac_args "PrintHint")
 
 let _ = 
-  vinterp_add("PrintHintDb",
-	      function 
-	      	| [(VARG_IDENTIFIER id)] -> 
-		    fun () -> print_hint_db_by_name (string_of_id id)
-	      	| _ -> assert false)
+  vinterp_add "PrintHintDb"
+    (function 
+       | [(VARG_IDENTIFIER id)] -> 
+	   fun () -> print_hint_db_by_name (string_of_id id)
+       | _ -> bad_vernac_args "PrintHintDb")
 
 let _ = 
-  vinterp_add("PrintHintGoal",
-	      function 
-		| [] -> fun () -> print_applicable_hint()
-	        | _ -> assert false)
+  vinterp_add "PrintHintGoal"
+    (function 
+       | [] -> fun () -> print_applicable_hint()
+       | _ -> bad_vernac_args "PrintHintGoal")
     
 let _ = 
-  vinterp_add("PrintHintId",
-	      function 
-		| [(VARG_IDENTIFIER id)] -> fun () -> print_hint_id id
-	        | _ -> assert false)
+  vinterp_add "PrintHintId"
+    (function 
+       | [(VARG_IDENTIFIER id)] -> fun () -> print_hint_id id
+       | _ -> bad_vernac_args "PrintHintId")
 
 (**************************************************************************)
 (*                           Automatic tactics                            *)
@@ -635,7 +636,7 @@ and my_find_search db_list local_db hdc concl =
 		(trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> unfold_constr c
 	  | Extern tacast -> 
-	      conclPattern concl (outSOME p) tacast))
+	      conclPattern concl (out_some p) tacast))
     tacl
 
 and trivial_resolve db_list local_db cl = 
@@ -888,7 +889,7 @@ let search_superauto n ids argl g =
     ids,
     (List.map (fun id -> pf_type_of g (pf_global g id)) ids) in   
   let hyps = (concat_sign (pf_untyped_hyps g) sigma) in
-  super_search n [Fmavm.map searchtable "core"] (make_local_hint_db hyps)
+  super_search n [Stringmap.find "core" !searchtable] (make_local_hint_db hyps)
     argl g
 
 let superauto n ids_add argl  = 
@@ -907,13 +908,13 @@ let dyn_superauto l g =
   match l with
     | (Integer n)::(Clause ids_add)::l -> 
         superauto n ids_add 
-          (join_map_list 
+          (list_join_map
              (function 
 		| Quoted_string s -> (cvt_autoArgs s)
                 | _ -> assert false) l) g
     | _::(Clause ids_add)::l  -> 
         superauto !default_search_depth ids_add 
-          (join_map_list 
+          (list_join_map
              (function 
 		| Quoted_string s -> (cvt_autoArgs s)
                 | _ -> assert false) l) g
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 333aca1344..82a8ee792f 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -44,7 +44,7 @@ module Hint_db :
 
 type frozen_hint_db_table = Hint_db.t Stringmap.t
 
-type hint_db_table = Hint_db.t Stringmap.t
+type hint_db_table = Hint_db.t Stringmap.t ref
 
 val searchtable : hint_db_table
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index e4d79051c9..6efa9c686f 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -109,6 +109,7 @@ open Util
 open Names
 open Generic
 open Term
+open Environ
 open Reduction
 open Proof_trees
 open Tacmach
@@ -120,6 +121,9 @@ open Libobject
 open Library
 open Vernacinterp
 open Pattern
+open Coqast
+open Ast
+open Pcoq
 
 (* two patterns - one for the type, and one for the type of the type *)
 type destructor_pattern = {
@@ -200,28 +204,29 @@ let add_destructor_hint na pat pri code =
     (inDD (na,{ d_pat = pat; d_pri=pri; d_code=code }))
 
 let _ = 
-  vinterp_add
-    ("HintDestruct",
-     fun [VARG_IDENTIFIER na; VARG_AST location; VARG_COMMAND patcom;
+  vinterp_add "HintDestruct"
+    (function
+       | [VARG_IDENTIFIER na; VARG_AST location; VARG_COMMAND patcom;
           VARG_NUMBER pri; VARG_AST tacexp] ->
-       let loc =
-	 match location with
-           | Node(_,"CONCL",[]) -> CONCL()
-	   | Node(_,"DiscardableHYP",[]) -> HYP true
-	   | Node(_,"PreciousHYP",[]) -> HYP false 
-       in
-       fun () ->
-	 let pat = raw_sopattern_of_compattern (initial_sign()) patcom in
-	 let code = Ast.to_act_check_vars ["$0",ETast] ETast tacexp in
-	 add_destructor_hint na
-           (match loc with
-              | HYP b ->
-		  HYP(b,{d_typ=pat;d_sort=DOP0(Meta(newMETA()))},
-                      { d_typ=DOP0(Meta(newMETA()));
-		       	d_sort=DOP0(Meta(newMETA())) })
-              | CONCL () ->
-		  CONCL({d_typ=pat;d_sort=DOP0(Meta(newMETA()))}))
-           pri code)
+	   let loc = match location with
+             | Node(_,"CONCL",[]) -> Concl()
+	     | Node(_,"DiscardableHYP",[]) -> Hyp true
+	     | Node(_,"PreciousHYP",[]) -> Hyp false 
+	     | _ -> assert false
+	   in
+	   fun () ->
+	     let pat = raw_sopattern_of_compattern (Global.env()) patcom in
+	     let code = Ast.to_act_check_vars ["$0",ETast] ETast tacexp in
+	     add_destructor_hint na
+               (match loc with
+		  | Hyp b ->
+		      Hyp(b,{d_typ=pat;d_sort=DOP0(Meta(new_meta()))},
+			  { d_typ=DOP0(Meta(new_meta()));
+		       	    d_sort=DOP0(Meta(new_meta())) })
+		  | Concl () ->
+		      Concl({d_typ=pat;d_sort=DOP0(Meta(new_meta()))}))
+               pri code
+       | _ -> bad_vernac_args "HintDestruct")
 
 let match_dpat dp cls gls =
   let cltyp = clause_type cls gls in
@@ -242,12 +247,15 @@ let applyDestructor cls discard dd gls =
     | Some id -> ["$0", Vast (nvar (string_of_id id))]
     | None -> ["$0", Vast (nvar "$0")] in
   (* TODO: find the real location *)
-  let (Vast tcom) = Ast.eval_act dummy_loc astb dd.d_code in
+  let tcom = match Ast.eval_act dummy_loc astb dd.d_code with
+    | Vast tcom -> tcom
+    | _ -> assert false 
+  in
   let discard_0 =
     match (cls,dd.d_pat) with
-      | (Some id,HYP(discardable,_,_)) ->
+      | (Some id,Hyp(discardable,_,_)) ->
           if discard & discardable then thin [id] else tclIDTAC
-      | (None,CONCL _) -> tclIDTAC
+      | (None,Concl _) -> tclIDTAC
       | _ -> error "ApplyDestructor" 
   in
   (tclTHEN (Tacinterp.interp tcom) discard_0) gls
@@ -269,8 +277,17 @@ let dHyp id gls = destructHyp false id gls
 
 open Tacinterp
 
-let _ = tacinterp_add("DHyp",(fun [Identifier id] -> dHyp id))
-let _ = tacinterp_add("CDHyp",(fun [Identifier id] -> cDHyp id))
+let _ = 
+  tacinterp_add
+    ("DHyp",(function
+	       | [Identifier id] -> dHyp id
+	       | _ -> bad_tactic_args "DHyp"))
+
+let _ = 
+  tacinterp_add
+    ("CDHyp",(function
+		| [Identifier id] -> cDHyp id
+		| _ -> bad_tactic_args "CDHyp"))
 
 (* [DConcl gls]
 
@@ -283,9 +300,13 @@ let dConcl gls =
   let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
   tclFIRST (List.map (applyDestructor None false) sorted_ddl) gls
 
-let _ = tacinterp_add("DConcl",(fun [] -> dConcl))
+let _ = 
+  tacinterp_add
+    ("DConcl",(function
+		 | [] -> dConcl
+		 | _ -> bad_tactic_args "DConcl"))
 
-let to2Lists (table:t) = Nbtermdn.to2Lists table
+let to2Lists (table:t) = Nbtermdn.to2lists table
 
 let rec search n =
   if n=0 then error "Search has reached zero.";
@@ -306,5 +327,6 @@ let sarch_depth_tdb = ref(5)
 let dyn_auto_tdb = function 
   | [Integer n] -> auto_tdb n 
   | []          -> auto_tdb !sarch_depth_tdb
+  | _           -> bad_tactic_args "AutoTDB"
 
 let h_auto_tdb = hide_tactic "AutoTDB" dyn_auto_tdb
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index b59df6334b..de81cce919 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -1,5 +1,12 @@
 
 (* $Id$ *)
 
+(*i*)
+open Names
+open Tacmach
+(*i*)
+
 (* Programmable destruction of hypotheses and conclusions. *)
 
+val dHyp : identifier -> tactic
+val dConcl : tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ff5d324a31..bae9c87982 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -191,7 +191,7 @@ fois pour toutes : en particulier si Pattern.somatch produit une UserError
 Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
 si après Intros la conclusion matche le pattern.
 *)
-(***TODO
+
 let conclPattern concl pat tacast gl = 
   let constr_bindings = Pattern.somatch None pat concl in
   let ast_bindings = 
@@ -199,8 +199,7 @@ let conclPattern concl pat tacast gl =
       (fun (i,c) -> (i, Termast.bdize false (assumptions_for_print []) c))
       constr_bindings in 
   let tacast' = Coqast.subst_meta ast_bindings tacast in
-    Tacinterp.interp tacast' gl
-***)
+  Tacinterp.interp tacast' gl
 
 let clauseTacThen tac continuation =
   (fun cls -> (tclTHEN (tac cls) continuation))
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 298b5abd96..49acb49e44 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -77,9 +77,8 @@ val ifOnClause     :
    if the term concl matches the pattern pat, (in sense of 
    Pattern.somatches, then replace ?1 ?2 metavars in tacast by the
    right values to build a tactic *)
-(***
-val conclPattern : constr -> constr -> CoqAst.t -> tactic
-**i*)
+
+val conclPattern : constr -> constr -> Coqast.t -> tactic
 
 (*s Elimination tacticals. *)