removes all references to ctast.ml the Makefile has been updated accordingly.

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

1 files changed, 3 insertions, 291 deletions

diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index bc9f706c57..d4d134f647 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -7,7 +7,6 @@ open Tacticals;;
 open Hipattern;;
 open Pattern;;
 open Reduction;;
-open Ctast;;
 open Rawterm;;
 open Environ;;
 
@@ -88,34 +87,9 @@ type pbp_rule = (identifier list *
                        identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) ->
                     pbp_sequence option;;
 
-(*
-let make_named_intro s =
-    Node(zz, "Intros",
-          [Node(zz,"INTROPATTERN",
-            [Node(zz,"LISTPATTERN",
-              [Node(zz, "IDENTIFIER", 
-                [Nvar(zz, s)])])])]);;
-*)
+
 let make_named_intro id = PbpIntros [id]
 
-(*
-let get_name_from_intro = function
-    Node(a, "Intros",
-          [Node(b,"INTROPATTERN",
-            [Node(c,"LISTPATTERN",
-              [Node(d, "IDENTIFIER", 
-                [Nvar(e, s)])])])]) ->
-		  Some s
-  | _ -> None;;
-*)
-(*
-let make_clears =  function
-    [] -> Node(zz, "Idtac",[])
-  | str_list ->
-      Node(zz, "TRY", [Node(zz,"Clear",
-	   [Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)])
-	       ]);;
-*)
 let make_clears str_list = PbpThen [PbpTryClear str_list]
 
 let add_clear_names_if_necessary tactic clear_names =
@@ -124,7 +98,6 @@ let add_clear_names_if_necessary tactic clear_names =
     | l -> chain_tactics [PbpTryClear l] tactic;;
 
 let make_final_cmd f optname clear_names constr path =
-(*    let tactic = f optname constr path in*)
     add_clear_names_if_necessary (f optname constr path) clear_names;;
 
 let (rem_cast:pbp_rule) = function
@@ -336,23 +309,7 @@ let (not_intro: pbp_rule) = function
 
 
 
-(*
-let elim_with_bindings hyp_name names =
-  Node(zz,"Elim", 
-       [Node(zz, "COMMAND", [Nvar(zz,hyp_name)]);
-	 Node(zz,"BINDINGS", 
-	      List.map 
-		(function s -> 
-		  Node(zz,"BINDING",
-		       [Nvar(zz,s);
-			 Node
-			   (zz,"COMMAND",
-			    [Node
-				(zz,"APPLIST",
-				 [Nvar(zz,"PBP_META");
-				   Nvar(zz,
-					"value_for_" ^ s)])])])) names)]);;
-*)
+
 let elim_with_bindings hyp_name names =
   PbpElim (hyp_name, names);;
 
@@ -448,114 +405,6 @@ let (mk_db_indices: int list -> int -> int list) =
    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|]), 2::1::path) 
-      	when
- 	  (is_matching_local (notconstr ()) oper) or
- 	  (is_matching_local (notTconstr ()) oper) ->
-	 Some(Node(zz, "TACTICLIST",
-		   [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_away (id_of_string "H") avoid in
-	let str_h1 = (string_of_id h1) in
-	let h2 = next_global_ident_away (id_of_string "H") (h1::avoid) in
-	let str_h2 = (string_of_id h2) in
-	Some(Node(zz,"TACTICLIST",
-                  [elim_with_bindings h str_list;
-		    make_named_intro str_h1;
-		    make_named_intro str_h2;
-		    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 str_h1 else str_h2))
-                        (kind_of_term cont_body) path in
-		    if nprems = 0 then
-		      cont_tac
-		    else
-		      Node(zz,"TACLIST",
-			   cont_tac::(auxiliary_goals
-					clear_names clear_flag
-					h nprems))]))
-    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
-      when ((is_matching_local (exconstr ()) oper) or
-	    (is_matching_local (exTconstr ()) oper) or
-	    (is_matching_local (sigconstr ()) oper) or
-	    (is_matching_local (sigTconstr()) oper)) & a = 2 ->
-		   (match (kind_of_term c2),path with
-		     Lambda(Name x, _,body), (2::path) ->
-		       Some(Node(zz,"TACTICLIST",
-		    		 [elim_with_bindings h str_list;
-				   let x' = next_global_ident_away 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
-				   if nprems = 0 then
-				     cont_tac
-				   else
-				     Node(zz,"TACLIST",
-					  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(Node(zz, "TACTICLIST",
-		    [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_away (id_of_string "H") avoid in
-		      let str_h' = (string_of_id h') in
-		      let cont_tac =
-                        Node(zz,"TACTICLIST",
-			     [make_named_intro str_h';
-			       f 
-				 (* h' should not be used again *)
-				 (h'::avoid)
-				 (* the disjunct itself can be discarded *)
-				 (h::clear_names) false (Some str_h')
-                          (kind_of_term cont_body) path]) in
-		      let snd_tac = 
-			Node(zz, "TACTICLIST", 
-			     [make_named_intro str_h';
-			       make_clears (h::clear_names)]) in
-		      let tacs1 = 
-			if a = 1 then
-			  [cont_tac; snd_tac]
-		      	else
-			  [snd_tac; cont_tac] in
-		      Node(zz,"TACLIST",
-			   tacs1@(auxiliary_goals (h::clear_names)
-				   false "dummy" 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
-	     (Node(zz,"Apply", [Node(zz,"COMMAND",[Nvar(zz, h)]);
-			     Node(zz,"BINDINGS", [])]))
-             clear_names)
-    | _ -> None)
-  | _ -> None;;
-*)
-
 let (head_tactic_patt: pbp_rule) = function
     avoid, clear_names, clear_flag, Some h, cstr, path, f ->
     (match down_prods (cstr, path, 0) with
@@ -652,11 +501,6 @@ let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2;
 		      and_intro; or_intro; not_intro; ex_intro];;
 
 
-(* The tactic traced_try was intended to be used in tactics instead of
-   Try, with an argument  Node(zz, "TACTIC", [b]) where b is the tactic to
-   try.  However, the current design is not very robust to the fact that
-   Traced_Try may occur several times in the executed command! *)
-
 let try_trace = ref true;;
 
 let traced_try (f1:tactic) g =
@@ -670,24 +514,10 @@ let traced_try_entry = function
   |  _ -> failwith "traced_try_entry received wrong arguments";;
 
 
-let rec clean_trace flag =
-      function
-          Node(a,"Traced_Try", [Node(_,_,[b])]) ->
-             if flag then b else Node(zz,"Idtac",[])
-      	| Node(a,b,c) -> Node(a,b,List.map (clean_trace flag) c)
-        | t -> t;;
-
 (* 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 =
-      match optname with
-        None ->  Node(zz, "TRY", [Node(zz, "Assumption",[])])
-      | Some(a) -> Node(zz, "TRY", 
-                   [Node(zz, "Exact",[Node(zz,"COMMAND",[Nvar(zz,a)])])]);;
-*)
 
 let default_ast optname constr path = PbpThen [PbpTryAssumption optname]
 
@@ -710,100 +540,12 @@ let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path =
 (* these are the optimisation functions. *)
 (* This function takes care of flattening successive then commands. *)
 
-(*
-let rec optim1 =
-    function
-        Node(a,"TACTICLIST",b) ->
-          let tacs = List.map optim1 b in
-          let rec flatten = function
-            | [Node(a, "TACTICLIST", b')] ->
-                let rec last = function
-                    [] -> failwith "function last is called on an empty list"
-		  | [b] -> b
-		  | a::b -> last b in
-		(match last b' with
-		  Node(a, "TACLIST",_) -> [Node(a,"TACTICLIST", b')]
-		| _ -> flatten b')
-            | Node(a, "TACTICLIST", b')::others -> List.append (flatten b')
-                                                       (flatten others)
-            | Node(a, "Idtac",[])::others -> (flatten others)
-            | [Node(a, "TACLIST",tacs)] ->
-                 [Node(a, "TACLIST", List.map optim1 tacs)]
-            | t1::others -> t1::(flatten others)
-            | [] -> [] in
-          (match (flatten tacs) with
-            [] -> Node(zz,"Idtac", [])
-          | [t] -> t
-          | args -> Node(zz,"TACTICLIST", args))
-      |	t -> t;;
-*)
 
 (* Invariant: in [flatten_sequence t], occurrences of [PbpThenCont(l,t)] enjoy
     that t is some [PbpAtom t] *)
-(*
-let rec flatten_sequence =
-  function
-      PbpThens (tl1,tl2) -> PbpThens (tl1,List.map flatten_sequence tl2)
-    | PbpThen (tl1,t1) as x ->
-	(match flatten_sequence t1 with
-	  | PbpThenCont (tl2,t2) -> PbpThenCont (tl1@tl2,t2)
-	  | PbpThens (tl2,tl3) -> PbpThens (tl1@tl2,tl3)
-	  | PbpAtom _ -> x)
-    | PbpAtom t as x -> x;;
-*)
 
 (* This optimization function takes care of compacting successive Intro commands
    together. *)
-(*
-let rec optim2 =
-    function
-	Node(a,"TACTICLIST",b) ->
-         let get_ids = 
-           List.map (function Node(_,"IDENTIFIER", [Nvar(_,s)])->s
-             | Node(_,s,_) -> (failwith "unexpected node " ^ s)
-             |  _ -> failwith "get_ids expected an identifier") in
-         let put_ids ids =
-           Node(zz,"Intros",
-               	[Node(zz,"INTROPATTERN",
-		      [Node(zz,"LISTPATTERN", 
-			    List.map 
-			      (function s -> Node(zz,"IDENTIFIER",[Nvar(zz,s)]))
-			      ids)])]) in
-         let rec group_intros names = function
-             [] -> (match names with
-               [] -> []
-	     | l -> [put_ids l])
-           | Node(_,"Intros", 
-		  [Node(_,"INTROPATTERN",[Node(_,"LISTPATTERN", ids)])])::others ->
-		    group_intros (names@(get_ids ids)) others
-           | [Node(a,"TACLIST",b')] ->
-	       [Node(a,"TACLIST", List.map optim2 b')]
-           | t1::others -> 
-	       (match names with
-		 [] -> t1::(group_intros [] others)
-	       | l -> (put_ids l)::t1::(group_intros [] others)) in
-	 Node(a,"TACTICLIST",group_intros [] b)
-   | t -> t;;
-*)
-(*
-let rec optim2 = function
-  | TacThens (t,tl) -> TacThens (optim2 t, List.map optim2 tl)
-  | t ->
-      let get_ids = 
-	List.map (function IntroIdentifier _ as x -> x
-	  |  _ -> failwith "get_ids expected an identifier") in
-      let rec group_intros names = function
-	  [] -> (match names with
-              [] -> []
-	    | l -> [TacIntroPattern l])
-	| (TacIntroPattern ids)::others ->
-	    group_intros (names@(get_ids ids)) others
-	| t1::others -> 
-	    (match names with
-		[] -> t1::(group_intros [] others)
-	      | l -> (TacIntroPattern l)::t1::(group_intros [] others)) in
-      make_then (group_intros [] (flatten_sequence t))
-*)
 
 let rec group_intros names = function
     [] -> (match names with
@@ -819,37 +561,7 @@ let rec optim2 = function
   | PbpThens (tl1,tl2) -> PbpThens (group_intros [] tl1, List.map optim2 tl2)
   | PbpThen tl -> PbpThen (group_intros [] tl)
 
-(*
-let rec merge_ast_in_command com1 com2 =
-    let args1 =
-     (match com1 with
-	Node(_, "APPLIST", args) -> args
-     | _ -> failwith "unexpected com1 in merge_ast_in_command") in
-    let args2 =
-     (match com2 with
-        Node(_, "APPLIST", hyp::args) -> args
-     | _ -> failwith "unexpected com2 in merge_ast_in_command") in
-      Node(zz, "COMMAND", [Node(zz, "APPLIST", args1@args2)]);;
-*)
-(*
-let cleanup_clears empty_allowed names str_list other =
-  let rec clean_aux = function
-      [] -> []
-    | (Nvar(_,x) as fst_one)::tail ->
-      if List.mem x str_list then
-         clean_aux tail
-      else
-         fst_one::(clean_aux tail)
-    | _ -> failwith "unexpected argument in clean_aux" in
-  match clean_aux names with
-    [] -> (match other with 
-            [] -> 
-	      if empty_allowed then
-		[]
-	      else [Node(zz,"Idtac",[])]
-          | _ -> other)
-  | l -> Node(zz, "TRY", [Node(zz, "Clear", [Node(zz,"CLAUSE", l)])])::other;;
-*)
+
 let rec cleanup_clears str_list = function
     [] -> []
   | x::tail ->