Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 0 insertions, 303 deletions

diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
deleted file mode 100644
index 805700b0..00000000
--- a/contrib/first-order/sequent.ml
+++ /dev/null
@@ -1,303 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: sequent.ml 7925 2006-01-24 23:20:39Z herbelin $ *)
-
-open Term
-open Util
-open Formula
-open Unify
-open Tacmach
-open Names
-open Libnames
-open Pp
-
-let newcnt ()=
-  let cnt=ref (-1) in
-    fun b->if b then incr cnt;!cnt
-
-let priority = (* pure heuristics, <=0 for non reversible *)
-  function
-      Right rf->
-	begin
-	  match rf with
-	      Rarrow               -> 100
-	    | Rand                 ->  40 
-	    | Ror                  -> -15
-	    | Rfalse               -> -50
-	    | Rforall              -> 100
-	    | Rexists (_,_,_)      -> -29
-	end
-    | Left lf ->
-	match lf with
-	    Lfalse                 -> 999
-	  | Land _                 ->  90
-	  | Lor _                  ->  40
-	  | Lforall (_,_,_)        -> -30 
-	  | Lexists _              ->  60
-	  | LA(_,lap) ->
-	      match lap with
-		  LLatom           ->   0
-		| LLfalse (_,_)    -> 100
-		| LLand (_,_)      ->  80
-		| LLor (_,_)       ->  70
-		| LLforall _       -> -20
-		| LLexists (_,_)   ->  50
-		| LLarrow  (_,_,_) -> -10 
-
-let left_reversible lpat=(priority lpat)>0
-
-module OrderedFormula=
-struct
-  type t=Formula.t
-  let compare e1 e2=
-	(priority e1.pat) - (priority e2.pat)
-end
-
-(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed; Cast's,
-   application associativity, binders name and Cases annotations are
-   not taken into account *)
-
-let rec compare_list f l1 l2=
-  match l1,l2 with
-      [],[]-> 0
-    | [],_ -> -1
-    | _,[] -> 1
-    | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2
-
-let compare_array f v1 v2=  
-  let l=Array.length v1 in
-  let c=l - Array.length v2 in
-    if c=0 then
-      let rec comp_aux i=
-	if i<0 then 0 
-	else
-	  let ci=f v1.(i) v2.(i) in
-	    if ci=0 then 
-	      comp_aux (i-1)
-	    else ci
-      in comp_aux (l-1)
-    else c
-
-let compare_constr_int f t1 t2 =
-  match kind_of_term t1, kind_of_term t2 with
-    | Rel n1, Rel n2 -> n1 - n2
-    | Meta m1, Meta m2 -> m1 - m2
-    | Var id1, Var id2 -> Pervasives.compare id1 id2
-    | Sort s1, Sort s2 -> Pervasives.compare s1 s2
-    | Cast (c1,_,_), _ -> f c1 t2
-    | _, Cast (c2,_,_) -> f t1 c2
-    | Prod (_,t1,c1), Prod (_,t2,c2) 
-    | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
-	(f =? f) t1 t2 c1 c2 
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> 
-	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
-    | App (_,_), App (_,_) ->
-	let c1,l1=decompose_app t1 
-	and c2,l2=decompose_app t2 in
-	  (f =? (compare_list f)) c1 c2 l1 l2
-    | Evar (e1,l1), Evar (e2,l2) -> 
-	((-) =? (compare_array f)) e1 e2 l1 l2
-    | Const c1, Const c2 -> Pervasives.compare c1 c2
-    | Ind c1, Ind c2 -> Pervasives.compare c1 c2
-    | Construct c1, Construct c2 -> Pervasives.compare c1 c2
-    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-	((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2
-    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
-	ln1 ln2 tl1 tl2 bl1 bl2
-    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
-	ln1 ln2 tl1 tl2 bl1 bl2
-    | _ -> Pervasives.compare t1 t2
-
-let rec compare_constr m n=
-  compare_constr_int compare_constr m n
-    
-module OrderedConstr=
-struct
-  type t=constr
-  let compare=compare_constr
-end
-
-type h_item = global_reference * (int*constr) option
-
-module Hitem=
-struct 
-  type t = h_item
-  let compare (id1,co1) (id2,co2)=
-    (Pervasives.compare 
-     =? (fun oc1 oc2 ->
-	   match oc1,oc2 with 
-	       Some (m1,c1),Some (m2,c2) -> 
-		 ((-) =? OrderedConstr.compare) m1 m2 c1 c2
-	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
-end
-
-module CM=Map.Make(OrderedConstr)
-
-module History=Set.Make(Hitem)
-
-let cm_add typ nam cm=
-  try 
-    let l=CM.find typ cm in CM.add typ (nam::l) cm
-  with
-      Not_found->CM.add typ [nam] cm
-	
-let cm_remove typ nam cm=
-  try
-    let l=CM.find typ cm in 
-    let l0=List.filter (fun id->id<>nam) l in
-      match l0 with 
-	  []->CM.remove typ cm
-	| _ ->CM.add typ l0 cm
-      with Not_found ->cm
-
-module HP=Heap.Functional(OrderedFormula)
-
-type t=
-    {redexes:HP.t;
-     context:(global_reference list) CM.t;
-     latoms:constr list;
-     gl:types;
-     glatom:constr option;
-     cnt:counter;
-     history:History.t;
-     depth:int}
-
-let deepen seq={seq with depth=seq.depth-1}
- 
-let record item seq={seq with history=History.add item seq.history}
-
-let lookup item seq=
-  History.mem item seq.history ||
-  match item with
-      (_,None)->false
-    | (id,Some ((m,t) as c))->
-	let p (id2,o)=
-	  match o with
-	      None -> false
-	    | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
-	  History.exists p seq.history
-
-let rec add_formula side nam t seq gl=
-  match build_formula side nam t gl seq.cnt with
-      Left f->
-	begin
-	  match side with
-	      Concl ->
-		{seq with 
-		   redexes=HP.add f seq.redexes;
-		   gl=f.constr;
-		   glatom=None}
-	    | _ ->
-		{seq with 
-		   redexes=HP.add f seq.redexes;
-		   context=cm_add f.constr nam seq.context}
-	end
-    | Right t->
-	match side with
-	    Concl ->
-	      {seq with gl=t;glatom=Some t}
-	  | _ ->
-	      {seq with 
-		 context=cm_add t nam seq.context;
-		 latoms=t::seq.latoms}
-	      
-let re_add_formula_list lf seq=
-  let do_one f cm=
-    if f.id == dummy_id then cm
-    else cm_add f.constr f.id cm in
-  {seq with 
-     redexes=List.fold_right HP.add lf seq.redexes;
-     context=List.fold_right do_one lf seq.context}
-
-let find_left t seq=List.hd (CM.find t seq.context)
-
-(*let rev_left seq=
-  try
-    let lpat=(HP.maximum seq.redexes).pat in
-      left_reversible lpat
-  with Heap.EmptyHeap -> false
-*)
-let no_formula seq=
-  seq.redexes=HP.empty
-
-let rec take_formula seq=
-  let hd=HP.maximum seq.redexes
-  and hp=HP.remove seq.redexes in
-    if hd.id == dummy_id then
-      let nseq={seq with redexes=hp} in
-	if seq.gl==hd.constr then 
-	  hd,nseq
-	else
-	  take_formula nseq (* discarding deprecated goal *)
-    else
-      hd,{seq with 
-	    redexes=hp;
-	    context=cm_remove hd.constr hd.id seq.context}
-	
-let empty_seq depth=
-  {redexes=HP.empty;   
-   context=CM.empty;
-   latoms=[];
-   gl=(mkMeta 1);
-   glatom=None;
-   cnt=newcnt ();
-   history=History.empty;
-   depth=depth}
-
-let create_with_ref_list l depth gl=
-  let f gr seq=
-    let c=constr_of_global gr in    
-    let typ=(pf_type_of gl c) in
-      add_formula Hyp gr typ seq gl in
-    List.fold_right f l (empty_seq depth)
-
-open Auto
-
-let create_with_auto_hints l depth gl=
-  let seqref=ref (empty_seq depth) in
-  let f p_a_t =
-    match p_a_t.code with
-	Res_pf (c,_) | Give_exact c
-      | Res_pf_THEN_trivial_fail (c,_) ->
-	  (try 
-	     let gr=global_of_constr c in 
-	     let typ=(pf_type_of gl c) in
-	       seqref:=add_formula Hint gr typ !seqref gl
-	   with Not_found->())
-      | _-> () in
-  let g _ l=List.iter f l in
-  let h dbname=
-    let hdb=
-      try
-	searchtable_map dbname
-      with Not_found-> 
-	error ("Firstorder: "^dbname^" : No such Hint database") in
-      Hint_db.iter g hdb in
-    List.iter h l;
-    !seqref
-
-let print_cmap map=
-  let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) c in
-      str "| " ++ 
-      Util.prlist Printer.pr_global l ++ 
-      str " : " ++
-      Ppconstr.pr_constr_expr xc ++ 
-      cut () ++ 
-      s in
-    msgnl (v 0 
-	     (str "-----" ++ 
-	      cut () ++
-	      CM.fold print_entry map (mt ()) ++
-	      str "-----"))
-
-