1 files changed, 758 insertions, 0 deletions

diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
new file mode 100644
index 00000000..e0f88ba6
--- /dev/null
+++ b/contrib/interface/pbp.ml
@@ -0,0 +1,758 @@
+(* A proof by pointing algorithm. *)
+open Util;;
+open Names;;
+open Term;;
+open Tactics;;
+open Tacticals;;
+open Hipattern;;
+open Pattern;;
+open Matching;;
+open Reduction;;
+open Rawterm;;
+open Environ;;
+
+open Proof_trees;;
+open Proof_type;;
+open Tacmach;;
+open Tacexpr;;
+open Typing;;
+open Pp;;
+open Libnames;;
+open Genarg;;
+open Topconstr;;
+open Termops;;
+
+let zz = Util.dummy_loc;;
+
+let hyp_radix = id_of_string "H";;
+
+let next_global_ident = next_global_ident_away true
+
+(* get_hyp_by_name : goal sigma -> string -> constr,
+   looks up for an hypothesis (or a global constant), from its name *)
+let get_hyp_by_name g name =
+  let evd = project g in
+  let env = pf_env g in
+  try (let judgment = 
+         Pretyping.understand_judgment 
+          evd env (RVar(zz, name)) in
+       ("hyp",judgment.uj_type))
+(* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
+   Loïc *)
+  with _ -> (let c = Nametab.global (Ident (zz,name)) in
+             ("cste",type_of (Global.env()) Evd.empty (constr_of_reference c)))
+;;
+
+type pbp_atom =
+  | PbpTryAssumption of identifier option
+  | PbpTryClear of identifier list
+  | PbpGeneralize of identifier * identifier list
+  | PbpLApply of identifier (* = CutAndApply *)
+  | PbpIntros of intro_pattern_expr list
+  | PbpSplit
+  (* Existential *)
+  | PbpExists of identifier
+  (* Or *)
+  | PbpLeft
+  | PbpRight
+  (* Head *)
+  | PbpApply of identifier
+  | PbpElim of identifier * identifier list;;
+
+(* Invariant: In PbpThens ([a1;...;an],[t1;...;tp]), all tactics
+   [a1]..[an-1] are atomic (or try of an atomic) tactic and produce
+   exactly one goal, and [an] produces exactly p subgoals
+
+   In [PbpThen [a1;..an]], all tactics are (try of) atomic tactics and
+   produces exactly one subgoal, except the last one which may complete the
+   goal
+
+   Convention: [PbpThen []] is Idtac and [PbpThen t] is a coercion
+   from atomic to composed tactic
+*)
+
+type pbp_sequence =
+  | PbpThens of pbp_atom list * pbp_sequence list
+  | PbpThen of pbp_atom list
+
+(* This flattens sequences of tactics producing just one subgoal *)
+let chain_tactics tl1 = function
+  | PbpThens (tl2, tl3) -> PbpThens (tl1@tl2, tl3)
+  | PbpThen tl2 -> PbpThen (tl1@tl2)
+
+type pbp_rule = (identifier list *
+                    identifier list *
+                    bool *
+                    identifier option *
+                    (types, constr) kind_of_term *
+                    int list *
+                    (identifier list ->
+                     identifier list ->
+                     bool ->
+                       identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) ->
+                    pbp_sequence option;;
+
+
+let make_named_intro id = PbpIntros [IntroIdentifier id];;
+
+let make_clears str_list = PbpThen [PbpTryClear str_list]
+
+let add_clear_names_if_necessary tactic clear_names =
+    match clear_names with
+      [] -> tactic
+    | l -> chain_tactics [PbpTryClear l] tactic;;
+
+let make_final_cmd f optname clear_names constr path =
+    add_clear_names_if_necessary (f optname constr path) clear_names;;
+
+let (rem_cast:pbp_rule) = function
+    (a,c,cf,o, Cast(f,_), p, func) ->
+      Some(func a c cf o (kind_of_term f) p)
+  | _ -> None;;
+
+let (forall_intro: pbp_rule) = function
+  (avoid,
+   clear_names,
+   clear_flag,
+   None,
+   Prod(Name x, _, body),
+   (2::path),
+   f) ->
+     let x' = next_global_ident x avoid in
+      Some(chain_tactics [make_named_intro x']
+	      (f (x'::avoid)
+		clear_names clear_flag None (kind_of_term body) path))
+| _ -> None;;
+
+let (imply_intro2: pbp_rule) = function
+  avoid, clear_names,
+  clear_flag, None, Prod(Anonymous, _, body), 2::path, f ->
+   let h' = next_global_ident hyp_radix avoid in
+     Some(chain_tactics [make_named_intro h']
+          (f (h'::avoid) clear_names clear_flag None (kind_of_term body) path))
+  | _ -> None;;
+
+      
+(*
+let (imply_intro1: pbp_rule) = function
+  avoid, clear_names,
+  clear_flag, None, Prod(Anonymous, prem, body), 1::path, f ->
+   let h' = next_global_ident hyp_radix avoid in
+   let str_h' = h' in
+     Some(chain_tactics [make_named_intro str_h']
+            (f (h'::avoid) clear_names clear_flag (Some str_h') 
+		(kind_of_term prem) path))
+  | _ -> None;;
+*)
+
+let make_var id = CRef (Ident(zz, id))
+
+let make_app f l = CApp (zz,(None,f),List.map (fun x -> (x,None)) l)
+
+let make_pbp_pattern x =
+  make_app (make_var (id_of_string "PBP_META"))
+     [make_var (id_of_string ("Value_for_" ^ (string_of_id x)))]
+
+let rec make_then = function
+  | [] -> TacId ""
+  | [t] -> t
+  | t1::t2::l -> make_then (TacThen (t1,t2)::l)
+
+let make_pbp_atomic_tactic = function
+  | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption))
+  | PbpTryAssumption (Some a) ->
+      TacTry (TacAtom (zz, TacExact (make_var a)))
+  | PbpExists x -> 
+      TacAtom (zz, TacSplit (true,ImplicitBindings [make_pbp_pattern x]))
+  | PbpGeneralize (h,args) ->
+      let l = List.map make_pbp_pattern args in
+      TacAtom (zz, TacGeneralize [make_app (make_var h) l])
+  | PbpLeft -> TacAtom (zz, TacLeft NoBindings)
+  | PbpRight -> TacAtom (zz, TacRight NoBindings)
+  | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
+  | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
+  | PbpApply h -> TacAtom (zz, TacApply (make_var h,NoBindings))
+  | PbpElim (hyp_name, names) ->
+      let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
+      TacAtom
+	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
+  | PbpTryClear l -> 
+      TacTry (TacAtom (zz, TacClear (List.map (fun s -> AI (zz,s)) l)))
+  | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
+
+let rec make_pbp_tactic = function
+  | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl)
+  | PbpThens (l,tl) ->
+      TacThens
+        (make_then (List.map make_pbp_atomic_tactic l),
+	 List.map make_pbp_tactic tl)
+
+let (forall_elim: pbp_rule) = function
+  avoid, clear_names, clear_flag, 
+  Some h, Prod(Name x, _, body), 2::path, f ->
+  let h' = next_global_ident hyp_radix avoid in
+  let clear_names' = if clear_flag then h::clear_names else clear_names in
+    Some
+     (chain_tactics [PbpGeneralize (h,[x]); make_named_intro h']
+        (f (h'::avoid) clear_names' true (Some h') (kind_of_term body) path))
+  | _ -> None;;
+
+
+let (imply_elim1: pbp_rule) = function
+  avoid, clear_names, clear_flag,
+  Some h, Prod(Anonymous, prem, body), 1::path, f ->
+  let clear_names' = if clear_flag then h::clear_names else clear_names in
+  let h' = next_global_ident hyp_radix avoid in
+  let str_h' = (string_of_id h') in
+  Some(PbpThens
+	  ([PbpLApply h],
+	   [chain_tactics [make_named_intro h'] (make_clears (h::clear_names));
+	    f avoid clear_names' false None (kind_of_term prem) path]))
+  | _ -> None;;
+
+
+let (imply_elim2: pbp_rule) = function
+  avoid, clear_names, clear_flag,
+  Some h, Prod(Anonymous, prem, body), 2::path, f ->
+  let clear_names' = if clear_flag then h::clear_names else clear_names in
+  let h' = next_global_ident hyp_radix avoid in
+  Some(PbpThens
+	 ([PbpLApply h],
+          [chain_tactics [make_named_intro h']
+              (f (h'::avoid) clear_names' false (Some h') 
+		      (kind_of_term body) path);
+           make_clears clear_names]))
+  | _ -> None;;
+
+let reference dir s = Coqlib.gen_reference "Pbp" ("Init"::dir) s
+
+let constant dir s =  Coqlib.gen_constant "Pbp" ("Init"::dir) s
+
+let andconstr: unit -> constr = Coqlib.build_coq_and;;
+let prodconstr () = constant ["Datatypes"] "prod";;
+let exconstr = Coqlib.build_coq_ex;;
+let sigconstr () = constant ["Specif"] "sig";;
+let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ;;
+let orconstr = Coqlib.build_coq_or;;
+let sumboolconstr = Coqlib.build_coq_sumbool;;
+let sumconstr() = constant ["Datatypes"] "sum";;
+let notconstr = Coqlib.build_coq_not;;
+let notTconstr () = constant ["Logic_Type"] "notT";;
+
+let is_matching_local a b = is_matching (pattern_of_constr a) b;;
+
+let rec (or_and_tree_to_intro_pattern: identifier list -> 
+	   constr -> int list -> 
+	     intro_pattern_expr * identifier list * identifier *constr
+	     * int list * int * int) =
+fun avoid c path -> match kind_of_term c, path with
+  | (App(oper, [|c1; c2|]), 2::a::path)
+    when ((is_matching_local (andconstr()) oper) or
+	  (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
+      let id2 = next_global_ident hyp_radix avoid in
+      let cont_expr = if a = 1 then c1 else c2 in
+      let cont_patt, avoid_names, id, c, path, rank, total_branches = 
+	or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in
+      let patt_list = 
+	if a = 1 then
+	  [cont_patt; IntroIdentifier id2]
+	else
+	  [IntroIdentifier id2; cont_patt] in
+      	(IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank, 
+	 total_branches)
+  | (App(oper, [|c1; c2|]), 2::3::path)
+    when ((is_matching_local (exconstr()) oper) or
+	  (is_matching_local (sigconstr()) oper)) ->
+      (match (kind_of_term c2) with 
+	   Lambda (Name x, _, body) ->
+	     let id1 = next_global_ident x avoid in
+	     let cont_patt, avoid_names, id, c, path, rank, total_branches =
+	       or_and_tree_to_intro_pattern (id1::avoid) body path in
+	     (IntroOrAndPattern[[IntroIdentifier id1; cont_patt]],
+	      avoid_names, id, c, path, rank, total_branches)
+	 | _ -> assert false)
+  | (App(oper, [|c1; c2|]), 2::a::path)
+      when ((is_matching_local (orconstr ()) oper) or
+            (is_matching_local (sumboolconstr ()) oper) or
+	    (is_matching_local (sumconstr ()) oper)) & (a = 1 or a = 2) ->
+      let id2 = next_global_ident hyp_radix avoid in
+      let cont_expr = if a = 1 then c1 else c2 in
+      let cont_patt, avoid_names, id, c, path, rank, total_branches =
+ 	or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in
+      let new_rank = if a = 1 then rank else rank+1 in
+      let patt_list =
+	if a = 1 then
+	  [[cont_patt];[IntroIdentifier id2]]
+	else
+	  [[IntroIdentifier id2];[cont_patt]] in
+	(IntroOrAndPattern patt_list, 
+	 avoid_names, id, c, path, new_rank, total_branches+1)
+  | (_, path) -> let id = next_global_ident hyp_radix avoid in
+      (IntroIdentifier id, (id::avoid), id, c, path, 1, 1);;
+
+let auxiliary_goals clear_names clear_flag this_name n_aux others =
+  let clear_cmd = 
+    make_clears (if clear_flag then (this_name ::clear_names) else clear_names) in
+  let rec clear_list = function
+      0 -> others
+    | n -> clear_cmd::(clear_list (n - 1)) in
+  clear_list n_aux;;
+
+
+let (imply_intro3: pbp_rule) = function
+    avoid, clear_names, clear_flag, None, Prod(Anonymous, prem, body),
+    1::path, f ->
+      let intro_patt, avoid_names, id, c, p, rank, total_branches =
+	or_and_tree_to_intro_pattern avoid prem path in
+	if total_branches = 1 then
+	  Some(chain_tactics [PbpIntros [intro_patt]]
+		 (f avoid_names clear_names clear_flag (Some id)
+		    (kind_of_term c) path))
+	else
+	  Some
+	    (PbpThens
+	       ([PbpIntros [intro_patt]],
+	    	auxiliary_goals clear_names clear_flag id
+		  (rank - 1)
+		  ((f avoid_names clear_names clear_flag (Some id)
+		      (kind_of_term c) path)::
+		     auxiliary_goals clear_names clear_flag id 
+		     (total_branches - rank) [])))
+  | _ -> None;;
+		 
+
+
+let (and_intro: pbp_rule) = function
+    avoid, clear_names, clear_flag,
+    None, App(and_oper, [|c1; c2|]), 2::a::path, f 
+      ->
+      if ((is_matching_local (andconstr()) and_oper) or
+          (is_matching_local (prodconstr ()) and_oper)) & (a = 1 or a = 2) then
+      	let cont_term = if a = 1 then c1 else c2 in
+      	let cont_cmd = f avoid clear_names false None 
+			 (kind_of_term cont_term) path in
+      	let clear_cmd = make_clears clear_names in
+      	let cmds =
+            (if a = 1 
+	    then [cont_cmd;clear_cmd] 
+	    else [clear_cmd;cont_cmd]) in
+      	Some (PbpThens ([PbpSplit],cmds))
+      else None
+  | _ -> None;;
+
+let exists_from_lambda avoid clear_names clear_flag c2 path f =
+  match kind_of_term c2 with
+    Lambda(Name x, _, body) -> 
+      Some (PbpThens ([PbpExists x],
+		      [f avoid clear_names false None (kind_of_term body) path]))
+  | _ -> None;;
+
+
+let (ex_intro: pbp_rule) = function
+    avoid, clear_names, clear_flag, None,
+    App(oper, [| c1; c2|]), 2::3::path, f
+      when (is_matching_local (exconstr ()) oper)
+ 	or (is_matching_local (sigconstr ()) oper) ->
+	  exists_from_lambda avoid clear_names clear_flag c2 path f
+  | _ -> None;;
+
+let (exT_intro : pbp_rule) = function
+    avoid, clear_names, clear_flag, None,
+    App(oper, [| c1; c2|]), 2::2::2::path, f
+      when (is_matching_local (sigTconstr ()) oper) ->
+	exists_from_lambda avoid clear_names clear_flag c2 path f
+  | _ -> None;;
+
+let (or_intro: pbp_rule) = function
+    avoid, clear_names, clear_flag, None,
+    App(or_oper, [|c1; c2 |]), 2::a::path, f ->
+      if ((is_matching_local (orconstr ()) or_oper) or
+        (is_matching_local (sumboolconstr ()) or_oper) or 
+	(is_matching_local (sumconstr ()) or_oper))
+	  & (a = 1 or a = 2) then
+	let cont_term = if a = 1 then c1 else c2 in
+	let fst_cmd = if a = 1 then PbpLeft else PbpRight in
+	let cont_cmd = f avoid clear_names false None 
+			 (kind_of_term cont_term) path in
+	Some(chain_tactics [fst_cmd] cont_cmd)
+      else
+	None
+  | _ -> None;;
+	
+let dummy_id = id_of_string "Dummy";;
+
+let (not_intro: pbp_rule) = function
+    avoid, clear_names, clear_flag, None,
+    App(not_oper, [|c1|]), 2::1::path, f ->
+      if(is_matching_local (notconstr ()) not_oper) or 
+	(is_matching_local (notTconstr ()) not_oper) then
+	let h' = next_global_ident hyp_radix avoid in
+	Some(chain_tactics [make_named_intro h']
+	       (f (h'::avoid) clear_names false (Some h') 
+		  (kind_of_term c1) path))
+      else
+ 	None
+  | _ -> None;;
+
+
+
+
+let elim_with_bindings hyp_name names =
+  PbpElim (hyp_name, names);;
+
+(* This function is used to follow down a path, while staying on the spine of
+   successive products (universal quantifications or implications).
+   Arguments are the current observed constr object and the path that remains
+   to be followed, and an integer indicating how many products have already been
+   crossed.
+   Result is:
+     - a list of string indicating the names of universally quantified variables.
+     - a list of integers indicating the positions of the successive 
+       universally quantified variables.
+     - an integer indicating the number of non-dependent products.
+     - the last constr object encountered during the walk down, and
+     - the remaining path.
+
+   For instance the following session should happen:
+  let tt = raw_constr_of_com (Evd.mt_evd())(gLOB(initial_sign()))
+     (parse_com "(P:nat->Prop)(x:nat)(P x)->(P x)") in
+     down_prods (tt, [2;2;2], 0)
+  ---> ["P","x"],[0;1], 1, <<(P x)>>, []
+*)
+
+
+let rec down_prods: (types, constr) kind_of_term * (int list) * int -> 
+           identifier list * (int list) * int * (types, constr) kind_of_term *
+  (int list) = 
+   function
+     Prod(Name x, _, body), 2::path, k ->
+	let res_sl, res_il, res_i, res_cstr, res_p 
+	    = down_prods (kind_of_term body, path, k+1) in
+	x::res_sl, (k::res_il), res_i, res_cstr, res_p
+   | Prod(Anonymous, _, body), 2::path, k ->
+        let res_sl, res_il, res_i, res_cstr, res_p 
+	    = down_prods (kind_of_term body, path, k+1) in
+	res_sl, res_il, res_i+1, res_cstr, res_p
+   | cstr, path, _ -> [], [], 0, cstr, path;;
+
+exception Pbp_internal of int list;;
+
+(* This function should be usable to check that a type can be used by the
+   Apply command.  Basically, c is supposed to be the head of some
+   type, where l gives the ranks of all universally quantified variables.
+   It check that these universally quantified variables occur in the head.
+
+   The knowledge I have on constr structures is incomplete.
+*)
+let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) = 
+   function c -> function l ->
+   let rec delete n = function
+     | [] -> []
+     | p::tl -> if n = p then tl else p::(delete n tl) in
+   let rec check_rec l = function
+   | App(f, array) ->
+       Array.fold_left (fun l c -> check_rec l (kind_of_term c))
+	 (check_rec l (kind_of_term f)) array
+   | Const _ -> l
+   | Ind _ -> l
+   | Construct _ -> l
+   | Var _ -> l
+   | Rel p ->
+       let result = delete p l in
+       if result = [] then
+	 raise (Pbp_internal [])
+       else
+	 result
+   | _ -> raise (Pbp_internal l) in
+   try 
+     (check_rec l c) = []
+   with Pbp_internal l -> l = [];;
+
+let (mk_db_indices: int list -> int -> int list) =
+  function int_list -> function nprems ->
+   let total = (List.length int_list) + nprems  in
+   let rec mk_db_aux = function
+     [] -> []
+   | a::l -> (total - a)::(mk_db_aux l) in
+   mk_db_aux int_list;;
+     
+
+(* This proof-by-pointing rule is quite complicated, as it attempts to foresee
+   usages of head tactics.  A first operation is to follow the path as far
+   as possible while staying on the spine of products (function down_prods)
+   and then to check whether the next step will be an elim step.  If the 
+   answer is true, then the built command takes advantage of the power of
+   head tactics.  *)
+
+let (head_tactic_patt: pbp_rule) = function
+    avoid, clear_names, clear_flag, Some h, cstr, path, f ->
+    (match down_prods (cstr, path, 0) with
+    | (str_list, _, nprems, App(oper,[|c1; c2|]), b::a::path)
+      when (((is_matching_local (exconstr ()) oper) (* or
+	      (is_matching_local (sigconstr ()) oper) *))  && a = 3) ->
+		   (match (kind_of_term c2) with
+		     Lambda(Name x, _,body) ->
+		       Some(PbpThens
+		    		 ([elim_with_bindings h str_list],
+				   let x' = next_global_ident x avoid in
+				   let cont_body =
+				     Prod(Name x', c1,
+					    mkProd(Anonymous, body, 
+						   mkVar(dummy_id))) in
+				   let cont_tac 
+				       = f avoid (h::clear_names) false None
+				       cont_body (2::1::path) in
+				   cont_tac::(auxiliary_goals
+						       clear_names clear_flag
+						       h nprems [])))
+		     | _ -> None)
+    | (str_list, _, nprems, 
+       App(oper,[|c1|]), 2::1::path) 
+      	when
+ 	  (is_matching_local (notconstr ()) oper) or
+ 	  (is_matching_local (notTconstr ()) oper) ->
+	 Some(chain_tactics [elim_with_bindings h str_list]
+		 (f avoid clear_names false None (kind_of_term c1) path))
+    | (str_list, _, nprems, 
+       App(oper, [|c1; c2|]), 2::a::path) 
+      when ((is_matching_local (andconstr()) oper) or
+	    (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
+	let h1 = next_global_ident hyp_radix avoid in
+	let h2 = next_global_ident hyp_radix (h1::avoid) in
+	Some(PbpThens
+                  ([elim_with_bindings h str_list],
+		    let cont_body = 
+		      if a = 1 then c1 else c2 in
+		    let cont_tac = 
+		      f (h2::h1::avoid) (h::clear_names) 
+                        false (Some (if 1 = a then h1 else h2))
+                        (kind_of_term cont_body) path in
+		      (chain_tactics 
+			 [make_named_intro h1; make_named_intro h2]
+			 cont_tac)::
+	       (auxiliary_goals clear_names clear_flag h nprems [])))
+    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
+      when ((is_matching_local (sigTconstr()) oper)) & a = 2 ->
+		   (match (kind_of_term c2),path with
+		     Lambda(Name x, _,body), (2::path) ->
+		       Some(PbpThens
+		    		 ([elim_with_bindings h str_list],
+				   let x' = next_global_ident x avoid in
+				   let cont_body =
+				     Prod(Name x', c1,
+					    mkProd(Anonymous, body, 
+						   mkVar(dummy_id))) in
+				   let cont_tac 
+				       = f avoid (h::clear_names) false None
+				       cont_body (2::1::path) in
+				   cont_tac::(auxiliary_goals
+						       clear_names clear_flag
+						       h nprems [])))
+		     | _ -> None)
+    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
+	when ((is_matching_local (orconstr ()) oper) or
+              (is_matching_local (sumboolconstr ()) oper) or
+	      (is_matching_local (sumconstr ()) oper)) &
+                (a = 1 or a = 2) ->
+	  Some(PbpThens
+		    ([elim_with_bindings h str_list],
+		      let cont_body =
+			if a = 1 then c1 else c2 in
+                      (* h' is the name for the new intro *)
+		      let h' = next_global_ident hyp_radix avoid in
+		      let cont_tac =
+                        chain_tactics 
+			  [make_named_intro h']
+			  (f 
+			     (* h' should not be used again *)
+			     (h'::avoid)
+			     (* the disjunct itself can be discarded *)
+			     (h::clear_names) false (Some h')
+                             (kind_of_term cont_body) path) in
+		      let snd_tac = 
+			chain_tactics
+			   [make_named_intro h']
+			   (make_clears (h::clear_names)) in
+		      let tacs1 = 
+			if a = 1 then
+			  [cont_tac; snd_tac]
+		      	else
+			  [snd_tac; cont_tac] in
+		      tacs1@(auxiliary_goals (h::clear_names)
+				   false dummy_id nprems [])))
+    | (str_list, int_list, nprems, c, []) 
+        when  (check_apply c (mk_db_indices int_list nprems)) &
+              (match c with Prod(_,_,_) -> false
+              |  _ -> true) &
+              (List.length int_list) + nprems > 0 ->
+          Some(add_clear_names_if_necessary (PbpThen [PbpApply h]) clear_names)
+    | _ -> None)
+  | _ -> None;;
+      
+
+let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2;
+                      forall_elim; imply_intro3; imply_elim1; imply_elim2;
+		      and_intro; or_intro; not_intro; ex_intro; exT_intro];;
+
+
+let try_trace = ref true;;
+
+let traced_try (f1:tactic) g =
+    try (try_trace := true; tclPROGRESS f1 g)
+    with e when Logic.catchable_exception e ->
+      (try_trace := false; tclIDTAC g);;
+
+let traced_try_entry = function
+     [Tacexp t] ->
+           traced_try (Tacinterp.interp t)
+  |  _ -> failwith "traced_try_entry received wrong arguments";;
+
+
+(* When the recursive descent along the path is over, one includes the
+   command requested by the point-and-shoot strategy.  Default is
+   Try Assumption--Try Exact.  *)
+
+
+let default_ast optname constr path = PbpThen [PbpTryAssumption optname]
+
+(* This is the main proof by pointing function. *)
+(* avoid: les noms a ne pas utiliser *)
+(* final_cmd: la fonction appelee par defaut *)
+(* opt_name: eventuellement le nom de l'hypothese sur laquelle on agit *)
+
+let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path =
+  let rec try_all_rules rl =
+      match rl with 
+         f::tl ->
+           (match f (avoid, clear_names, clear_flag,
+                     opt_name, constr, path, pbpt final_cmd) with
+              Some(ast) -> ast
+            | None -> try_all_rules tl)
+      |	 [] -> make_final_cmd final_cmd opt_name clear_names constr path
+  in try_all_rules (!pbp_rules);;
+
+(* these are the optimisation functions. *)
+(* This function takes care of flattening successive then commands. *)
+
+
+(* Invariant: in [flatten_sequence t], occurrences of [PbpThenCont(l,t)] enjoy
+    that t is some [PbpAtom t] *)
+
+(* This optimization function takes care of compacting successive Intro commands
+   together. *)
+
+let rec group_intros names = function
+    [] -> (match names with
+        [] -> []
+      | l -> [PbpIntros l])
+  | (PbpIntros ids)::others -> group_intros (names@ids) others
+  | t1::others ->
+      (match names with
+	  [] -> t1::(group_intros [] others)
+	| l -> (PbpIntros l)::t1::(group_intros [] others))
+
+let rec optim2 = function
+  | PbpThens (tl1,tl2) -> PbpThens (group_intros [] tl1, List.map optim2 tl2)
+  | PbpThen tl -> PbpThen (group_intros [] tl)
+
+
+let rec cleanup_clears str_list = function
+    [] -> []
+  | x::tail ->
+      if List.mem x str_list then cleanup_clears str_list tail
+      else x::(cleanup_clears str_list tail);;
+
+(* This function takes care of compacting instanciations of universal
+   quantifications. *)
+
+let rec optim3_aux str_list = function
+    (PbpGeneralize (h,l1))::
+    (PbpIntros [IntroIdentifier s])::(PbpGeneralize (h',l2))::others
+      when s=h' ->
+      optim3_aux (s::str_list) (PbpGeneralize (h,l1@l2)::others)
+  | (PbpTryClear names)::other ->
+      (match cleanup_clears str_list names with
+	  [] -> other
+	| l -> (PbpTryClear l)::other)
+  | a::l -> a::(optim3_aux str_list l) 
+  | [] -> [];;
+
+let rec optim3 str_list = function
+    PbpThens (tl1, tl2) ->
+      PbpThens (optim3_aux str_list tl1, List.map (optim3 str_list) tl2)
+  | PbpThen tl -> PbpThen (optim3_aux str_list tl)
+
+let optim x = make_pbp_tactic (optim3 [] (optim2 x));;
+
+(* TODO
+add_tactic "Traced_Try" traced_try_entry;;
+*)
+
+let rec tactic_args_to_ints = function
+    [] -> []
+  | (Integer n)::l -> n::(tactic_args_to_ints l)
+  | _ -> failwith "expecting only numbers";;
+
+(*
+let pbp_tac display_function = function 
+            (Identifier a)::l -> 
+                 (function g ->
+                    let str = (string_of_id a) in
+		    let (ou,tstr) = (get_hyp_by_name g str) in
+		    let exp_ast =
+		      pbpt default_ast
+		        (match ou with
+			       "hyp" ->(pf_ids_of_hyps g)
+			       |_ -> (a::(pf_ids_of_hyps g)))
+                        []
+			false
+			(Some str)
+			(kind_of_term tstr)
+                        (tactic_args_to_ints l) in
+                    (display_function (optim exp_ast);
+                        tclIDTAC g))
+          | ((Integer n)::_) as l -> 
+                 (function g ->
+                    let exp_ast =
+                       (pbpt default_ast (pf_ids_of_hyps g) [] false
+                          None (kind_of_term (pf_concl g))
+			  (tactic_args_to_ints l)) in
+                     (display_function (optim exp_ast);
+                       tclIDTAC g))
+          | [] -> (function g ->
+                     (display_function (default_ast None (pf_concl g) []);
+                      tclIDTAC g))
+          |  _ -> failwith "expecting other arguments";;
+
+
+*)
+let pbp_tac display_function idopt nl =
+  match idopt with
+    | Some str ->
+        (function g ->
+	  let (ou,tstr) = (get_hyp_by_name g str) in
+	  let exp_ast =
+	    pbpt default_ast
+	      (match ou with
+		  "hyp" ->(pf_ids_of_hyps g)
+		|_ -> (str::(pf_ids_of_hyps g)))
+              []
+	      false
+	      (Some str)
+	      (kind_of_term tstr)
+              nl in
+              (display_function (optim exp_ast); tclIDTAC g))
+    | None ->
+	if nl <> [] then
+          (function g ->
+            let exp_ast =
+              (pbpt default_ast (pf_ids_of_hyps g) [] false
+		None (kind_of_term (pf_concl g)) nl) in
+            (display_function (optim exp_ast); tclIDTAC g))
+	else
+          (function g ->
+            (display_function
+	       (make_pbp_tactic (default_ast None (pf_concl g) []));
+            tclIDTAC g));;
+
+