Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 628 insertions, 0 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
new file mode 100755
index 00000000..d5236a7a
--- /dev/null
+++ b/contrib/interface/blast.ml
@@ -0,0 +1,628 @@
+(* Une tactique qui tente de démontrer toute seule le but courant,
+   interruptible par pcoq (si dans le fichier C:\WINDOWS\free il y a un A)
+*)
+open Ctast;;
+open Termops;;
+open Nameops;;
+open Auto;;
+open Clenv;;
+open Command;;
+open Ctast;;
+open Declarations;;
+open Declare;;
+open Eauto;;
+open Environ;;
+open Equality;;
+open Evd;;
+open Hipattern;;
+open Inductive;;
+open Names;;
+open Pattern;;
+open Pbp;;
+open Pfedit;;
+open Pp;;
+open Printer
+open Proof_trees;;
+open Proof_type;;
+open Rawterm;;
+open Reduction;;
+open Refiner;;
+open Sign;;
+open String;;
+open Tacmach;;
+open Tacred;;
+open Tacticals;;
+open Tactics;;
+open Term;;
+open Typing;;
+open Util;;
+open Vernacentries;;
+open Vernacinterp;;
+open Evar_refiner;;
+
+
+let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
+let parse_tac  t =
+    try (Pcoq.parse_string Pcoq.Tactic.tactic t)
+    with _ -> (msgnl (hov 0 (str"pas parsé: " ++ str t));
+	       failwith "tactic")
+;;
+
+let is_free () =
+   let st =open_in_bin ((Sys.getenv "HOME")^"/.free") in
+   let c=input_char st in
+   close_in st;
+   c = 'A'
+;;
+
+(* marche pas *)
+(*
+let is_free () =
+   msgnl (hov 0 [< 'str"Isfree========= "; 'fNL >]);
+   let s = Stream.of_channel stdin in
+   msgnl (hov 0 [< 'str"Isfree s "; 'fNL >]);
+   try (Stream.empty s;
+        msgnl (hov 0 [< 'str"Isfree empty "; 'fNL >]);
+        true)
+   with _ -> (msgnl (hov 0 [< 'str"Isfree not empty "; 'fNL >]);
+              false)
+;;
+*)
+let free_try tac g =
+    if is_free()
+    then (tac g)
+    else (failwith "not free")
+;;
+let adrel (x,t) e =
+    match x with 
+      Name(xid) -> Environ.push_rel (x,None,t) e
+    | Anonymous -> Environ.push_rel (x,None,t) e
+(* les constantes ayant une définition apparaissant dans x *)
+let rec def_const_in_term_rec vl x = 
+     match (kind_of_term x) with
+     Prod(n,t,c)->
+        let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
+   | Lambda(n,t,c) ->
+        let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
+   | App(f,args) -> def_const_in_term_rec vl f
+   | Sort(Prop(Null)) -> Prop(Null)
+   | Sort(c) -> c
+   | Ind(ind) ->
+          let (mib, mip) = Global.lookup_inductive ind in
+          mip.mind_sort
+   | Construct(c) ->
+          def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
+   | Case(_,x,t,a) 
+        -> def_const_in_term_rec vl x
+   | Cast(x,t)-> def_const_in_term_rec vl t
+   | Const(c)  -> def_const_in_term_rec vl (lookup_constant c vl).const_type
+   | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
+;;
+let def_const_in_term_ x =
+    def_const_in_term_rec  (Global.env()) (strip_outer_cast x)
+;;
+(*************************************************************************
+ recopiés de refiner.ml, car print_subscript pas exportée dans refiner.mli 
+ modif de print_info_script avec pr_bar
+*)
+
+let pr_bar () = str "|"
+
+let rec print_info_script sigma osign pf =
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+  match pf.ref with
+    | None -> (mt ())
+    | Some(r,spfl) ->
+        pr_rule r ++
+           match spfl with
+             | [] ->
+		   (str " " ++ fnl())
+             | [pf1] ->
+                 if pf1.ref = None then 
+		   (str " " ++ fnl())
+                 else 
+		   (str";" ++ brk(1,3) ++
+		      print_info_script sigma sign pf1)
+             | _ -> ( str";[" ++ fnl() ++
+                       prlist_with_sep pr_bar
+                         (print_info_script sigma sign) spfl ++
+                       str"]")
+
+let format_print_info_script sigma osign pf = 
+  hov 0 (print_info_script sigma osign pf)
+    
+let print_subscript sigma sign pf = 
+ (* if is_tactic_proof pf then 
+    format_print_info_script sigma sign (subproof_of_proof pf)
+  else *)
+    format_print_info_script sigma sign pf
+(****************)
+
+let pp_string x =
+   msgnl_with Format.str_formatter x;
+   Format.flush_str_formatter ()
+;;
+
+(***********************************************************************
+   copié de tactics/eauto.ml
+*)
+
+(***************************************************************************)
+(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
+(***************************************************************************)
+
+let unify_e_resolve  (c,clenv) gls = 
+  let (wc,kONT) = startWalk gls in
+  let clenv' = connect_clenv wc clenv in
+  let _ = clenv_unique_resolver false clenv' gls in
+  vernac_e_resolve_constr c gls
+
+let rec e_trivial_fail_db db_list local_db goal =
+  let tacl = 
+    registered_e_assumption ::
+    (tclTHEN Tactics.intro 
+       (function g'->
+	  let d = pf_last_hyp g' in
+	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
+          (e_trivial_fail_db db_list
+	     (Hint_db.add_list hintl local_db) g'))) ::
+    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
+  in 
+  tclFIRST (List.map tclCOMPLETE tacl) goal 
+
+and e_my_find_search db_list local_db hdc concl = 
+  let hdc = head_of_constr_reference hdc in
+  let hintl =
+    if occur_existential concl then 
+      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
+    else 
+      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
+  in 
+  let tac_of_hint = 
+    fun ({pri=b; pat = p; code=t} as patac) -> 
+      (b, 
+       let tac =
+	 match t with
+	   | Res_pf (term,cl) -> unify_resolve (term,cl)
+	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+	   | Give_exact (c) -> e_give_exact_constr c
+	   | Res_pf_THEN_trivial_fail (term,cl) ->
+               tclTHEN (unify_e_resolve (term,cl)) 
+		 (e_trivial_fail_db db_list local_db)
+	   | Unfold_nth c -> unfold_constr c
+	   | Extern tacast -> Auto.conclPattern concl 
+	       (out_some p) tacast
+       in 
+       (free_try tac,fmt_autotactic t))
+       (*i
+	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
+                     try tac gls
+		     with e when Logic.catchable_exception(e) -> 
+                            (Format.print_string "Fail\n"; 
+			     Format.print_flush (); 
+			     raise e)
+       i*)
+  in 
+  List.map tac_of_hint hintl
+    
+and e_trivial_resolve db_list local_db gl = 
+  try 
+    Auto.priority 
+      (e_my_find_search db_list local_db 
+	 (List.hd (head_constr_bound gl [])) gl)
+  with Bound | Not_found -> []
+
+let e_possible_resolve db_list local_db gl =
+  try List.map snd (e_my_find_search db_list local_db 
+		      (List.hd (head_constr_bound gl [])) gl)
+  with Bound | Not_found -> []
+
+let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
+
+let find_first_goal gls = 
+  try first_goal gls with UserError _ -> assert false
+
+(*s The following module [SearchProblem] is used to instantiate the generic
+    exploration functor [Explore.Make]. *)
+      
+module MySearchProblem = struct
+
+  type state = { 
+    depth : int; (*r depth of search before failing *)
+    tacres : goal list sigma * validation;
+    last_tactic : std_ppcmds;
+    dblist : Auto.Hint_db.t list;
+    localdb :  Auto.Hint_db.t list }
+		 
+  let success s = (sig_it (fst s.tacres)) = []
+
+  let rec filter_tactics (glls,v) = function
+    | [] -> []
+    | (tac,pptac) :: tacl -> 
+	try 
+	  let (lgls,ptl) = apply_tac_list tac glls in 
+	  let v' p = v (ptl p) in
+	  ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
+	with e when Logic.catchable_exception e ->
+	  filter_tactics (glls,v) tacl
+
+  let rec list_addn n x l = 
+    if n = 0 then l else x :: (list_addn (pred n) x l)
+
+  (* Ordering of states is lexicographic on depth (greatest first) then
+     number of remaining goals. *)
+  let compare s s' =
+    let d = s'.depth - s.depth in
+    let nbgoals s = List.length (sig_it (fst s.tacres)) in
+    if d <> 0 then d else nbgoals s - nbgoals s'
+
+  let branching s = 
+    if s.depth = 0 then 
+      []
+    else      
+      let lg = fst s.tacres in
+      let nbgl = List.length (sig_it lg) in
+      assert (nbgl > 0);
+      let g = find_first_goal lg in
+      let assumption_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (List.map 
+	       (fun id -> (e_give_exact_constr (mkVar id),
+			   (str "Exact" ++ spc()++ pr_id id)))
+	       (pf_ids_of_hyps g))
+	in
+	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
+				    last_tactic = pp; dblist = s.dblist;
+				    localdb = List.tl s.localdb }) l
+      in
+      let intro_tac = 
+	List.map 
+	  (fun ((lgls,_) as res,pp) -> 
+	     let g' = first_goal lgls in 
+	     let hintl = 
+	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	     in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
+	     { depth = s.depth; tacres = res; 
+	       last_tactic = pp; dblist = s.dblist;
+	       localdb = ldb :: List.tl s.localdb })
+	  (filter_tactics s.tacres [Tactics.intro,(str "Intro" )])
+      in
+      let rec_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+	in
+	List.map 
+	  (fun ((lgls,_) as res, pp) -> 
+	     let nbgl' = List.length (sig_it lgls) in
+	     if nbgl' < nbgl then
+	       { depth = s.depth; tacres = res; last_tactic = pp;
+		 dblist = s.dblist; localdb = List.tl s.localdb }
+	     else 
+	       { depth = pred s.depth; tacres = res; 
+		 dblist = s.dblist; last_tactic = pp;
+		 localdb = 
+		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
+	  l
+      in
+      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
+
+  let pp s = 
+    msg (hov 0 (str " depth="++ int s.depth ++ spc() ++
+		  s.last_tactic ++ str "\n"))
+
+end
+
+module MySearch = Explore.Make(MySearchProblem)
+
+let make_initial_state n gl dblist localdb =
+  { MySearchProblem.depth = n;
+    MySearchProblem.tacres = tclIDTAC gl;
+    MySearchProblem.last_tactic = (mt ());
+    MySearchProblem.dblist = dblist;
+    MySearchProblem.localdb = [localdb] }
+
+let e_depth_search debug p db_list local_db gl =
+  try
+    let tac = if debug then MySearch.debug_depth_first else MySearch.depth_first in
+    let s = tac (make_initial_state p gl db_list local_db) in
+    s.MySearchProblem.tacres
+  with Not_found -> error "EAuto: depth first search failed"
+
+let e_breadth_search debug n db_list local_db gl =
+  try
+    let tac = 
+      if debug then MySearch.debug_breadth_first else MySearch.breadth_first 
+    in
+    let s = tac (make_initial_state n gl db_list local_db) in
+    s.MySearchProblem.tacres
+  with Not_found -> error "EAuto: breadth first search failed"
+
+let e_search_auto debug (n,p) db_list gl = 
+  let local_db = make_local_hint_db gl in 
+  if n = 0 then 
+    e_depth_search debug p db_list local_db gl
+  else 
+    e_breadth_search debug n db_list local_db gl
+
+let eauto debug np dbnames = 
+  let db_list =
+    List.map
+      (fun x -> 
+	 try Stringmap.find x !searchtable
+	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+      ("core"::dbnames) 
+  in
+  tclTRY (e_search_auto debug np db_list)
+
+let full_eauto debug n gl = 
+  let dbnames = stringmap_dom !searchtable in
+  let dbnames =  list_subtract dbnames ["v62"] in
+  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
+  let local_db = make_local_hint_db gl in
+  tclTRY (e_search_auto debug n db_list) gl
+
+let my_full_eauto n gl = full_eauto false (n,0) gl
+
+(**********************************************************************
+   copié de tactics/auto.ml on a juste modifié search_gen
+*)
+let searchtable_map name = 
+  Stringmap.find name !searchtable
+
+(* local_db is a Hint database containing the hypotheses of current goal *)
+(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
+  de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
+
+let rec trivial_fail_db db_list local_db gl =
+  let intro_tac = 
+    tclTHEN intro 
+      (fun g'->
+	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
+  in
+  tclFIRST 
+    (assumption::intro_tac::
+     (List.map tclCOMPLETE 
+	(trivial_resolve db_list local_db (pf_concl gl)))) gl
+
+and my_find_search db_list local_db hdc concl =
+  let tacl = 
+    if occur_existential concl then 
+      list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list)
+    else 
+      list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db)
+      	(local_db::db_list)
+  in
+  List.map 
+    (fun ({pri=b; pat=p; code=t} as patac) -> 
+       (b,
+	match t with
+	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
+	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
+	  | Give_exact c  -> exact_check c
+	  | Res_pf_THEN_trivial_fail (term,cl) -> 
+	      tclTHEN 
+		(unify_resolve (term,cl)) 
+		(trivial_fail_db db_list local_db)
+	  | Unfold_nth c -> unfold_constr c
+	  | Extern tacast -> 
+	      conclPattern concl (out_some p) tacast))
+    tacl
+
+and trivial_resolve db_list local_db cl = 
+  try 
+    let hdconstr = List.hd (head_constr_bound cl []) in
+    priority 
+      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
+  with Bound | Not_found -> 
+    []
+
+(**************************************************************************)
+(*                       The classical Auto tactic                        *)
+(**************************************************************************)
+
+let possible_resolve db_list local_db cl =
+  try 
+    let hdconstr = List.hd (head_constr_bound cl []) in
+    List.map snd 
+      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
+  with Bound | Not_found -> 
+    []
+
+let decomp_unary_term c gls = 
+  let typc = pf_type_of gls c in 
+  let hd = List.hd (head_constr typc) in 
+  if Hipattern.is_conjunction hd then 
+    simplest_case c gls 
+  else 
+    errorlabstrm "Auto.decomp_unary_term" (str "not a unary type")
+
+let decomp_empty_term c gls = 
+  let typc = pf_type_of gls c in 
+  let (hd,_) = decompose_app typc in 
+  if Hipattern.is_empty_type hd then 
+    simplest_case c gls 
+  else 
+    errorlabstrm "Auto.decomp_empty_term" (str "not an empty type")
+
+
+(* decomp is an natural number giving an indication on decomposition 
+   of conjunction in hypotheses, 0 corresponds to no decomposition *)
+(* n is the max depth of search *)
+(* local_db contains the local Hypotheses *)
+
+let rec search_gen decomp n db_list local_db extra_sign goal =
+  if n=0 then error "BOUND 2";
+  let decomp_tacs = match decomp with 
+    | 0 -> [] 
+    | p -> 
+	(tclTRY_sign decomp_empty_term extra_sign)
+	::
+	(List.map 
+	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
+		(tclTHEN 
+		   (clear [id])
+		   (free_try (search_gen decomp p db_list local_db []))))
+	   (pf_ids_of_hyps goal)) 
+  in
+  let intro_tac = 
+    tclTHEN intro 
+      (fun g' -> 
+	 let (hid,_,htyp as d) = pf_last_hyp g' in
+	 let hintl = 
+	   try 
+	     [make_apply_entry (pf_env g') (project g')
+		(true,false) 
+		hid (mkVar hid,body_of_type htyp)]
+	   with Failure _ -> [] 
+	 in
+         (free_try
+	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
+	  g'))
+  in
+  let rec_tacs = 
+    List.map 
+      (fun ntac -> 
+	 tclTHEN ntac
+	   (free_try
+	    (search_gen decomp (n-1) db_list local_db empty_named_context)))
+      (possible_resolve db_list local_db (pf_concl goal))
+  in 
+  tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
+
+
+let search = search_gen 0
+
+let default_search_depth = ref 5
+			     
+let full_auto n gl = 
+  let dbnames = stringmap_dom !searchtable in
+  let dbnames = list_subtract dbnames ["v62"] in
+  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+  let hyps = pf_hyps gl in
+  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+  
+let default_full_auto gl = full_auto !default_search_depth gl
+(************************************************************************)
+
+let blast_tactic = ref (free_try default_full_auto)
+;;
+
+let blast_auto = (free_try default_full_auto)
+(*                  (tclTHEN (free_try default_full_auto)
+			  (free_try (my_full_eauto 2)))
+*)
+;;
+let blast_simpl = (free_try (reduce (Simpl None) onConcl))
+;;
+let blast_induction1 = 
+    (free_try (tclTHEN (tclTRY intro)
+		       (tclTRY (tclLAST_HYP simplest_elim))))
+;;
+let blast_induction2 = 
+    (free_try (tclTHEN (tclTRY (tclTHEN intro intro))
+		       (tclTRY (tclLAST_HYP simplest_elim))))
+;;
+let blast_induction3 = 
+    (free_try (tclTHEN (tclTRY (tclTHEN intro (tclTHEN intro intro)))
+		       (tclTRY (tclLAST_HYP simplest_elim))))
+;;
+
+blast_tactic :=
+  (tclORELSE (tclCOMPLETE blast_auto)
+  (tclORELSE (tclCOMPLETE (tclTHEN blast_simpl blast_auto))
+  (tclORELSE (tclCOMPLETE (tclTHEN blast_induction1
+                          (tclTHEN blast_simpl blast_auto)))
+  (tclORELSE (tclCOMPLETE (tclTHEN blast_induction2
+                          (tclTHEN blast_simpl blast_auto)))
+             (tclCOMPLETE (tclTHEN blast_induction3
+                          (tclTHEN blast_simpl blast_auto)))))))
+;;
+(*
+blast_tactic := (tclTHEN (free_try default_full_auto)
+			 (free_try (my_full_eauto 4)))
+;;
+*)
+
+let vire_extvar s =
+   let interro = ref false in
+   let interro_pos = ref 0 in
+   for i=0 to (length s)-1 do
+     if get s i = '?'
+     then (interro := true;
+           interro_pos := i)
+     else if (!interro && 
+              (List.mem (get s i)
+			['0';'1';'2';'3';'4';'5';'6';'7';'8';'9']))
+     then set s i ' '
+     else interro:=false
+   done;
+   s
+;;
+
+let blast gls =
+   let leaf g = {
+      open_subgoals = 1;
+      goal = g;
+      ref = None } in
+     try (let (sgl,v) as res = !blast_tactic gls in
+	  let {it=lg} = sgl in
+          if lg = [] 
+          then (let pf = v (List.map leaf (sig_it sgl)) in
+                let sign = (sig_it gls).evar_hyps in
+                let x = print_subscript 
+                     (sig_sig gls) sign pf in
+		msgnl (hov 0 (str"Blast ==> " ++ x));
+                let x = print_subscript 
+                     (sig_sig gls) sign pf in
+                let tac_string =
+                pp_string  (hov 0 x ) in
+    (* on remplace les ?1 ?2 ... de refine par ? *)
+		parse_tac ((vire_extvar tac_string)
+			   ^ ".")
+	  )
+	  else (msgnl (hov 0 (str"Blast failed to prove the goal..."));
+		failwith "echec de blast"))
+     with _ -> failwith "echec de blast"
+;;
+
+let blast_tac display_function = function 
+          | (n::_) as l -> 
+                 (function g ->
+                    let exp_ast = (blast g) in
+                     (display_function exp_ast;
+                       tclIDTAC g))
+          |  _ -> failwith "expecting other arguments";;
+
+let blast_tac_txt = 
+  blast_tac
+    (function x -> msgnl(Pptactic.pr_glob_tactic (Tacinterp.glob_tactic x)));;
+
+(* Obsolète ?
+overwriting_add_tactic "Blast1" blast_tac_txt;;
+*)
+
+(*
+Grammar tactic ne_numarg_list : list :=
+  ne_numarg_single [numarg($n)] ->[$n]
+| ne_numarg_cons [numarg($n) ne_numarg_list($ns)] -> [ $n ($LIST $ns) ].
+Grammar tactic simple_tactic : ast :=
+  blast1 [ "Blast1" ne_numarg_list($ns) ] ->
+         [ (Blast1 ($LIST $ns)) ].
+
+
+
+PATH=/usr/local/bin:/usr/bin:$PATH
+COQTOP=d:/Tools/coq-7.0-3mai
+CAMLLIB=/usr/local/lib/ocaml
+CAMLP4LIB=/usr/local/lib/camlp4
+export CAMLLIB
+export COQTOP
+export CAMLP4LIB 
+d:/Tools/coq-7.0-3mai/bin/coqtop.byte.exe 
+Drop.
+#use "/cygdrive/D/Tools/coq-7.0-3mai/dev/base_include";;
+*)