Imported Upstream snapshot 8.3~beta0+13298

14 files changed, 1713 insertions, 0 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
new file mode 100644
index 00000000..45365cb2
--- /dev/null
+++ b/plugins/firstorder/formula.ml
@@ -0,0 +1,270 @@
+(************************************************************************)
+(*  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$ *)
+
+open Hipattern
+open Names
+open Term
+open Termops
+open Reductionops
+open Tacmach
+open Util
+open Declarations
+open Libnames
+open Inductiveops
+
+let qflag=ref true
+
+let red_flags=ref Closure.betaiotazeta
+
+let (=?) f g i1 i2 j1 j2=
+  let c=f i1 i2 in
+    if c=0 then g j1 j2 else c
+
+let (==?) fg h i1 i2 j1 j2 k1 k2=
+  let c=fg i1 i2 j1 j2 in
+    if c=0 then h k1 k2 else c
+
+type ('a,'b) sum = Left of 'a | Right of 'b
+
+type counter = bool -> metavariable
+
+exception Is_atom of constr
+
+let meta_succ m = m+1
+
+let rec nb_prod_after n c=
+  match kind_of_term c with
+    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
+	1+(nb_prod_after 0 b)
+    | _ -> 0
+
+let construct_nhyps ind gls =
+  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
+  let hyp = nb_prod_after nparams in
+    Array.map hyp constr_types
+
+(* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
+let ind_hyps nevar ind largs gls=
+  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
+  let lp=Array.length types in
+  let myhyps i=
+    let t1=Term.prod_applist types.(i) largs in
+    let t2=snd (decompose_prod_n_assum nevar t1) in
+      fst (decompose_prod_assum t2) in
+    Array.init lp myhyps
+
+let special_nf gl=
+  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> Closure.norm_val infos (Closure.inject t))
+
+let special_whd gl=
+  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+type kind_of_formula=
+    Arrow of constr*constr
+  | False of inductive*constr list
+  | And of inductive*constr list*bool
+  | Or of inductive*constr list*bool
+  | Exists of inductive*constr list
+  | Forall of constr*constr
+  | Atom of constr
+
+let rec kind_of_formula gl term =
+  let normalize=special_nf gl in
+  let cciterm=special_whd gl term in
+    match match_with_imp_term cciterm with
+	Some (a,b)-> Arrow(a,(pop b))
+      |_->
+	 match match_with_forall_term cciterm with
+	     Some (_,a,b)-> Forall(a,b)
+	   |_->
+	      match match_with_nodep_ind cciterm with
+		  Some (i,l,n)->
+		    let ind=destInd i in
+		    let (mib,mip) = Global.lookup_inductive ind in
+		    let nconstr=Array.length mip.mind_consnames in
+		      if nconstr=0 then
+			False(ind,l)
+		      else
+			let has_realargs=(n>0) in
+			let is_trivial=
+			  let is_constant c =
+			    nb_prod c = mib.mind_nparams in
+			    array_exists is_constant mip.mind_nf_lc in
+			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
+			    (has_realargs && not is_trivial)
+			  then
+			    Atom cciterm
+			  else
+			    if nconstr=1 then
+			      And(ind,l,is_trivial)
+			    else
+			      Or(ind,l,is_trivial)
+		| _ ->
+		    match match_with_sigma_type cciterm with
+			Some (i,l)-> Exists((destInd i),l)
+		      |_-> Atom (normalize cciterm)
+
+type atoms = {positive:constr list;negative:constr list}
+
+type side = Hyp | Concl | Hint
+
+let no_atoms = (false,{positive=[];negative=[]})
+
+let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *)
+
+let build_atoms gl metagen side cciterm =
+  let trivial =ref false
+  and positive=ref []
+  and negative=ref [] in
+  let normalize=special_nf gl in
+  let rec build_rec env polarity cciterm=
+    match kind_of_formula gl cciterm with
+	False(_,_)->if not polarity then trivial:=true
+      | Arrow (a,b)->
+	  build_rec env (not polarity) a;
+	  build_rec env polarity b
+      | And(i,l,b) | Or(i,l,b)->
+	  if b then
+	    begin
+	      let unsigned=normalize (substnl env 0 cciterm) in
+		if polarity then
+		  positive:= unsigned :: !positive
+		else
+		  negative:= unsigned :: !negative
+	    end;
+	  let v = ind_hyps 0 i l gl in
+	  let g i _ (_,_,t) =
+	    build_rec env polarity (lift i t) in
+	  let f l =
+	    list_fold_left_i g (1-(List.length l)) () l in
+	    if polarity && (* we have a constant constructor *)
+	      array_exists (function []->true|_->false) v
+	    then trivial:=true;
+	    Array.iter f v
+      | Exists(i,l)->
+	  let var=mkMeta (metagen true) in
+	  let v =(ind_hyps 1 i l gl).(0) in
+	  let g i _ (_,_,t) =
+	    build_rec (var::env) polarity (lift i t) in
+	    list_fold_left_i g (2-(List.length l)) () v
+      | Forall(_,b)->
+	  let var=mkMeta (metagen true) in
+	    build_rec (var::env) polarity b
+      | Atom t->
+	  let unsigned=substnl env 0 t in
+	    if not (isMeta unsigned) then (* discarding wildcard atoms *)
+	      if polarity then
+		positive:= unsigned :: !positive
+	      else
+		negative:= unsigned :: !negative in
+    begin
+      match side with
+	  Concl    -> build_rec [] true cciterm
+	| Hyp      -> build_rec [] false cciterm
+	| Hint     ->
+	    let rels,head=decompose_prod cciterm in
+	    let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in
+	      build_rec env false head;trivial:=false (* special for hints *)
+    end;
+    (!trivial,
+     {positive= !positive;
+      negative= !negative})
+
+type right_pattern =
+    Rarrow
+  | Rand
+  | Ror
+  | Rfalse
+  | Rforall
+  | Rexists of metavariable*constr*bool
+
+type left_arrow_pattern=
+    LLatom
+  | LLfalse of inductive*constr list
+  | LLand of inductive*constr list
+  | LLor of inductive*constr list
+  | LLforall of constr
+  | LLexists of inductive*constr list
+  | LLarrow of constr*constr*constr
+
+type left_pattern=
+    Lfalse
+  | Land of inductive
+  | Lor of inductive
+  | Lforall of metavariable*constr*bool
+  | Lexists of inductive
+  | LA of constr*left_arrow_pattern
+
+type t={id:global_reference;
+	constr:constr;
+	pat:(left_pattern,right_pattern) sum;
+	atoms:atoms}
+
+let build_formula side nam typ gl metagen=
+  let normalize = special_nf gl in
+    try
+      let m=meta_succ(metagen false) in
+      let trivial,atoms=
+	if !qflag then
+	  build_atoms gl metagen side typ
+	else no_atoms in
+      let pattern=
+	match side with
+	    Concl ->
+	      let pat=
+		match kind_of_formula gl typ with
+		    False(_,_)        -> Rfalse
+		  | Atom a       -> raise (Is_atom a)
+		  | And(_,_,_)        -> Rand
+		  | Or(_,_,_)         -> Ror
+		  | Exists (i,l) ->
+		      let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in
+			Rexists(m,d,trivial)
+		  | Forall (_,a) -> Rforall
+		  | Arrow (a,b) -> Rarrow in
+		Right pat
+	  | _ ->
+	      let pat=
+		match kind_of_formula gl typ with
+		    False(i,_)        ->  Lfalse
+		  | Atom a       ->  raise (Is_atom a)
+		  | And(i,_,b)         ->
+		      if b then
+			let nftyp=normalize typ in raise (Is_atom nftyp)
+		      else Land i
+		  | Or(i,_,b)          ->
+		      if b then
+			let nftyp=normalize typ in raise (Is_atom nftyp)
+		      else Lor i
+		  | Exists (ind,_) ->  Lexists ind
+		  | Forall (d,_) ->
+		      Lforall(m,d,trivial)
+		  | Arrow (a,b) ->
+		      let nfa=normalize a in
+			LA (nfa,
+			    match kind_of_formula gl a with
+				False(i,l)-> LLfalse(i,l)
+			      | Atom t->     LLatom
+			      | And(i,l,_)-> LLand(i,l)
+			      | Or(i,l,_)->  LLor(i,l)
+			      | Arrow(a,c)-> LLarrow(a,c,b)
+			      | Exists(i,l)->LLexists(i,l)
+			      | Forall(_,_)->LLforall a) in
+		Left pat
+      in
+	Left {id=nam;
+	      constr=normalize typ;
+	      pat=pattern;
+	      atoms=atoms}
+    with Is_atom a-> Right a (* already in nf *)
+
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
new file mode 100644
index 00000000..2e89ddb0
--- /dev/null
+++ b/plugins/firstorder/formula.mli
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  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$ *)
+
+open Term
+open Names
+open Libnames
+
+val qflag : bool ref
+
+val red_flags: Closure.RedFlags.reds ref
+
+val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
+  'a -> 'a -> 'b -> 'b -> int
+
+val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) ->
+  'a -> 'a -> 'b -> 'b -> 'c ->'c -> int
+
+type ('a,'b) sum = Left of 'a | Right of 'b
+
+type counter = bool -> metavariable
+
+val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
+
+val ind_hyps : int -> inductive -> constr list ->
+  Proof_type.goal Tacmach.sigma -> rel_context array
+
+type atoms = {positive:constr list;negative:constr list}
+
+type side = Hyp | Concl | Hint
+
+val dummy_id: global_reference
+
+val build_atoms : Proof_type.goal Tacmach.sigma -> counter ->
+  side -> constr -> bool * atoms
+
+type right_pattern =
+    Rarrow
+  | Rand
+  | Ror
+  | Rfalse
+  | Rforall
+  | Rexists of metavariable*constr*bool
+
+type left_arrow_pattern=
+    LLatom
+  | LLfalse of inductive*constr list
+  | LLand of inductive*constr list
+  | LLor of inductive*constr list
+  | LLforall of constr
+  | LLexists of inductive*constr list
+  | LLarrow of constr*constr*constr
+
+type left_pattern=
+    Lfalse
+  | Land of inductive
+  | Lor of inductive
+  | Lforall of metavariable*constr*bool
+  | Lexists of inductive
+  | LA of constr*left_arrow_pattern
+
+type t={id: global_reference;
+	constr: constr;
+	pat: (left_pattern,right_pattern) sum;
+	atoms: atoms}
+
+(*exception Is_atom of constr*)
+
+val build_formula : side -> global_reference -> types ->
+  Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum
+
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
new file mode 100644
index 00000000..9080e7db
--- /dev/null
+++ b/plugins/firstorder/g_ground.ml4
@@ -0,0 +1,148 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma"  i*)
+
+(* $Id$ *)
+
+open Formula
+open Sequent
+open Ground
+open Goptions
+open Tactics
+open Tacticals
+open Tacinterp
+open Term
+open Names
+open Util
+open Libnames
+
+(* declaring search depth as a global option *)
+
+let ground_depth=ref 3
+
+let _=
+  let gdopt=
+    { optsync=true;
+      optname="Firstorder Depth";
+      optkey=["Firstorder";"Depth"];
+      optread=(fun ()->Some !ground_depth);
+      optwrite=
+   (function
+	None->ground_depth:=3
+      |	Some i->ground_depth:=(max i 0))}
+  in
+    declare_int_option gdopt
+
+let congruence_depth=ref 100
+
+let _=
+  let gdopt=
+    { optsync=true;
+      optname="Congruence Depth";
+      optkey=["Congruence";"Depth"];
+      optread=(fun ()->Some !congruence_depth);
+      optwrite=
+   (function
+	None->congruence_depth:=0
+      |	Some i->congruence_depth:=(max i 0))}
+  in
+    declare_int_option gdopt
+
+let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
+
+let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
+
+let gen_ground_tac flag taco ids bases gl=
+  let backup= !qflag in
+    try
+      qflag:=flag;
+      let solver=
+	match taco with
+	    Some tac-> tac
+	  | None-> default_solver in
+      let startseq gl=
+	let seq=empty_seq !ground_depth in
+	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
+      let result=ground_tac solver startseq gl in
+	qflag:=backup;result
+    with e ->qflag:=backup;raise e
+
+(* special for compatibility with Intuition
+
+let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+
+let defined_connectives=lazy
+  [[],EvalConstRef (destConst (constant "not"));
+   [],EvalConstRef (destConst (constant "iff"))]
+
+let normalize_evaluables=
+  onAllHypsAndConcl
+    (function
+	 None->unfold_in_concl (Lazy.force defined_connectives)
+       | Some id->
+	   unfold_in_hyp (Lazy.force defined_connectives)
+	   (Tacexpr.InHypType id)) *)
+
+open Genarg
+open Ppconstr
+open Printer
+let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference
+let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_located pr_global))
+let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global
+
+ARGUMENT EXTEND firstorder_using
+  TYPED AS reference_list
+  PRINTED BY pr_firstorder_using_typed
+  RAW_TYPED AS reference_list
+  RAW_PRINTED BY pr_firstorder_using_raw
+  GLOB_TYPED AS reference_list
+  GLOB_PRINTED BY pr_firstorder_using_glob
+| [ "using" reference(a) ] -> [ [a] ]
+| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
+| [ "using" reference(a) reference(b) reference_list(l) ] -> [
+    Flags.if_verbose
+      Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+    a::b::l
+  ]
+| [ ] -> [ [] ]
+END
+
+TACTIC EXTEND firstorder
+    [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
+      [ gen_ground_tac true (Option.map eval_tactic t) l [] ]
+|   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
+      [ gen_ground_tac true (Option.map eval_tactic t) [] l ]
+|   [ "firstorder" tactic_opt(t) firstorder_using(l)
+       "with" ne_preident_list(l') ] ->
+      [ gen_ground_tac true (Option.map eval_tactic t) l l' ]
+|   [ "firstorder" tactic_opt(t) ] ->
+      [ gen_ground_tac true (Option.map eval_tactic t) [] [] ]
+END
+
+TACTIC EXTEND gintuition
+  [ "gintuition" tactic_opt(t) ] ->
+     [ gen_ground_tac false (Option.map eval_tactic t) [] [] ]
+END
+
+
+let default_declarative_automation gls =
+  tclORELSE
+    (tclORELSE (Auto.h_trivial [] None)
+    (Cctac.congruence_tac !congruence_depth []))
+    (gen_ground_tac true
+       (Some (tclTHEN
+		default_solver
+		(Cctac.congruence_tac !congruence_depth [])))
+       [] []) gls
+
+
+
+let () =
+  Decl_proof_instr.register_automation_tac default_declarative_automation
+
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
new file mode 100644
index 00000000..8a0f02d2
--- /dev/null
+++ b/plugins/firstorder/ground.ml
@@ -0,0 +1,152 @@
+(************************************************************************)
+(*  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$ *)
+
+open Formula
+open Sequent
+open Rules
+open Instances
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Libnames
+
+(*
+let old_search=ref !Auto.searchtable
+
+(* I use this solution as a means to know whether hints have changed,
+but this prevents the GC from collecting the previous table,
+resulting in some limited space wasting*)
+
+let update_flags ()=
+  if not ( !Auto.searchtable == !old_search ) then
+    begin
+      old_search:=!Auto.searchtable;
+      let predref=ref Names.KNpred.empty in
+      let f p_a_t =
+	match p_a_t.Auto.code with
+	    Auto.Unfold_nth (ConstRef kn)->
+	      predref:=Names.KNpred.add kn !predref
+	  | _ ->() in
+      let g _ l=List.iter f l in
+      let h _ hdb=Auto.Hint_db.iter g hdb in
+	Util.Stringmap.iter h !Auto.searchtable;
+	red_flags:=
+	Closure.RedFlags.red_add_transparent
+	  Closure.betaiotazeta (Names.Idpred.full,!predref)
+    end
+*)
+
+let update_flags ()=
+  let predref=ref Names.Cpred.empty in
+  let f coe=
+    try
+      let kn=destConst (Classops.get_coercion_value coe) in
+	predref:=Names.Cpred.add kn !predref
+    with Invalid_argument "destConst"-> () in
+    List.iter f (Classops.coercions ());
+    red_flags:=
+    Closure.RedFlags.red_add_transparent
+      Closure.betaiotazeta
+      (Names.Idpred.full,Names.Cpred.complement !predref)
+
+let ground_tac solver startseq gl=
+  update_flags ();
+  let rec toptac skipped seq gl=
+    if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
+    then Pp.msgnl (Printer.pr_goal (sig_it gl));
+    tclORELSE (axiom_tac seq.gl seq)
+      begin
+	try
+	  let (hd,seq1)=take_formula seq
+	  and re_add s=re_add_formula_list skipped s in
+	  let continue=toptac []
+	  and backtrack gl=toptac (hd::skipped) seq1 gl in
+	    match hd.pat with
+		Right rpat->
+		  begin
+		    match rpat with
+			Rand->
+			  and_tac backtrack continue (re_add seq1)
+		      | Rforall->
+			  let backtrack1=
+			    if !qflag then
+			      tclFAIL 0 (Pp.str "reversible in 1st order mode")
+			    else
+			      backtrack in
+			    forall_tac backtrack1 continue (re_add seq1)
+		      | Rarrow->
+			  arrow_tac backtrack continue (re_add seq1)
+		      | Ror->
+			  or_tac  backtrack continue (re_add seq1)
+		      | Rfalse->backtrack
+		      | Rexists(i,dom,triv)->
+			  let (lfp,seq2)=collect_quantified seq in
+			  let backtrack2=toptac (lfp@skipped) seq2 in
+			    if  !qflag && seq.depth>0 then
+			      quantified_tac lfp backtrack2
+				continue (re_add seq)
+			    else
+			      backtrack2 (* need special backtracking *)
+		  end
+	      | Left lpat->
+		  begin
+		    match lpat with
+			Lfalse->
+			  left_false_tac hd.id
+		      | Land ind->
+			  left_and_tac ind backtrack
+			  hd.id continue (re_add seq1)
+		      | Lor ind->
+			  left_or_tac ind backtrack
+			  hd.id continue (re_add seq1)
+		      | Lforall (_,_,_)->
+			  let (lfp,seq2)=collect_quantified seq in
+			  let backtrack2=toptac (lfp@skipped) seq2 in
+			    if  !qflag && seq.depth>0 then
+			      quantified_tac lfp backtrack2
+				continue (re_add seq)
+			    else
+			      backtrack2 (* need special backtracking *)
+  		      | Lexists ind ->
+			  if !qflag then
+			    left_exists_tac ind backtrack hd.id
+			      continue (re_add seq1)
+			  else backtrack
+		      | LA (typ,lap)->
+			  let la_tac=
+			    begin
+			      match lap with
+				  LLatom -> backtrack
+				| LLand (ind,largs) | LLor(ind,largs)
+				| LLfalse (ind,largs)->
+				    (ll_ind_tac ind largs backtrack
+				       hd.id continue (re_add seq1))
+				| LLforall p ->
+				    if seq.depth>0 && !qflag then
+				      (ll_forall_tac p backtrack
+					 hd.id continue (re_add seq1))
+				    else backtrack
+				| LLexists (ind,l) ->
+				    if !qflag then
+				      ll_ind_tac ind l backtrack
+					hd.id continue (re_add seq1)
+				    else
+				      backtrack
+				| LLarrow (a,b,c) ->
+				    (ll_arrow_tac a b c backtrack
+				       hd.id continue (re_add seq1))
+			    end in
+			    ll_atom_tac typ la_tac hd.id continue (re_add seq1)
+		  end
+	    with Heap.EmptyHeap->solver
+      end gl in
+    wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
+
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
new file mode 100644
index 00000000..3c0e903f
--- /dev/null
+++ b/plugins/firstorder/ground.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  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$ *)
+
+val ground_tac:     Tacmach.tactic ->
+  (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
+
diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mllib
new file mode 100644
index 00000000..447a1fb5
--- /dev/null
+++ b/plugins/firstorder/ground_plugin.mllib
@@ -0,0 +1,8 @@
+Formula
+Unify
+Sequent
+Rules
+Instances
+Ground
+G_ground
+Ground_plugin_mod
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
new file mode 100644
index 00000000..810262a6
--- /dev/null
+++ b/plugins/firstorder/instances.ml
@@ -0,0 +1,206 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Formula
+open Sequent
+open Unify
+open Rules
+open Util
+open Term
+open Rawterm
+open Tacmach
+open Tactics
+open Tacticals
+open Termops
+open Reductionops
+open Declarations
+open Formula
+open Sequent
+open Names
+open Libnames
+
+let compare_instance inst1 inst2=
+	match inst1,inst2 with
+	    Phantom(d1),Phantom(d2)->
+	      (OrderedConstr.compare d1 d2)
+	  | Real((m1,c1),n1),Real((m2,c2),n2)->
+	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2
+	  | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
+	  | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
+
+let compare_gr id1 id2=
+  if id1==id2 then 0 else
+    if id1==dummy_id then 1
+    else if id2==dummy_id then -1
+    else Pervasives.compare id1 id2
+
+module OrderedInstance=
+struct
+  type t=instance * Libnames.global_reference
+  let compare (inst1,id1) (inst2,id2)=
+    (compare_instance =? compare_gr) inst2 inst1 id2 id1
+    (* we want a __decreasing__ total order *)
+end
+
+module IS=Set.Make(OrderedInstance)
+
+let make_simple_atoms seq=
+  let ratoms=
+    match seq.glatom with
+	Some t->[t]
+      | None->[]
+  in {negative=seq.latoms;positive=ratoms}
+
+let do_sequent setref triv id seq i dom atoms=
+  let flag=ref true in
+  let phref=ref triv in
+  let do_atoms a1 a2 =
+    let do_pair t1 t2 =
+      match unif_atoms i dom t1 t2 with
+	  None->()
+	| Some (Phantom _) ->phref:=true
+	| Some c ->flag:=false;setref:=IS.add (c,id) !setref in
+      List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
+      List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
+    HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
+    do_atoms atoms (make_simple_atoms seq);
+    !flag && !phref
+
+let match_one_quantified_hyp setref seq lf=
+  match lf.pat with
+      Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
+	if do_sequent setref triv lf.id seq i dom lf.atoms then
+	  setref:=IS.add ((Phantom dom),lf.id) !setref
+    | _ ->anomaly "can't happen"
+
+let give_instances lf seq=
+  let setref=ref IS.empty in
+    List.iter (match_one_quantified_hyp setref seq) lf;
+    IS.elements !setref
+
+(* collector for the engine *)
+
+let rec collect_quantified seq=
+  try
+    let hd,seq1=take_formula seq in
+      (match hd.pat with
+	   Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) ->
+	     let (q,seq2)=collect_quantified seq1 in
+	       ((hd::q),seq2)
+	 | _->[],seq)
+  with Heap.EmptyHeap -> [],seq
+
+(* open instances processor *)
+
+let dummy_constr=mkMeta (-1)
+
+let dummy_bvid=id_of_string "x"
+
+let mk_open_instance id gl m t=
+  let env=pf_env gl in
+  let evmap=Refiner.project gl in
+  let var_id=
+    if id==dummy_id then dummy_bvid else
+      let typ=pf_type_of gl (constr_of_global id) in
+	(* since we know we will get a product,
+	   reduction is not too expensive *)
+      let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
+	match nam with
+	    Name id -> id
+	  | Anonymous ->  dummy_bvid in
+  let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in
+  let rec aux n avoid=
+    if n=0 then [] else
+      let nid=(fresh_id avoid var_id gl) in
+	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
+  let nt=it_mkLambda_or_LetIn revt (aux m []) in
+  let rawt=Detyping.detype false [] [] nt in
+  let rec raux n t=
+    if n=0 then t else
+      match t with
+	  RLambda(loc,name,k,_,t0)->
+	    let t1=raux (n-1) t0 in
+	      RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1)
+	| _-> anomaly "can't happen" in
+  let ntt=try
+    Pretyping.Default.understand evmap env (raux m rawt)
+  with _ ->
+    error "Untypable instance, maybe higher-order non-prenex quantification" in
+    decompose_lam_n_assum m ntt
+
+(* tactics   *)
+
+let left_instance_tac (inst,id) continue seq=
+  match inst with
+      Phantom dom->
+	if lookup (id,None) seq then
+	  tclFAIL 0 (Pp.str "already done")
+	else
+	  tclTHENS (cut dom)
+	    [tclTHENLIST
+	       [introf;
+		(fun gls->generalize
+		   [mkApp(constr_of_global id,
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+		introf;
+		tclSOLVE [wrap 1 false continue
+			    (deepen (record (id,None) seq))]];
+	    tclTRY assumption]
+    | Real((m,t) as c,_)->
+	if lookup (id,Some c) seq then
+	  tclFAIL 0 (Pp.str "already done")
+	else
+	  let special_generalize=
+	    if m>0 then
+	      fun gl->
+		let (rc,ot)= mk_open_instance id gl m t in
+		let gt=
+		  it_mkLambda_or_LetIn
+		    (mkApp(constr_of_global id,[|ot|])) rc in
+		  generalize [gt] gl
+	    else
+	      generalize [mkApp(constr_of_global id,[|t|])]
+	  in
+	    tclTHENLIST
+	      [special_generalize;
+	       introf;
+	       tclSOLVE
+		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
+
+let right_instance_tac inst continue seq=
+  match inst with
+      Phantom dom ->
+	tclTHENS (cut dom)
+	[tclTHENLIST
+	   [introf;
+	    (fun gls->
+	       split (Rawterm.ImplicitBindings
+			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
+	    tclSOLVE [wrap 0 true continue (deepen seq)]];
+	 tclTRY assumption]
+    | Real ((0,t),_) ->
+	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
+    | Real ((m,t),_) ->
+	tclFAIL 0 (Pp.str "not implemented ... yet")
+
+let instance_tac inst=
+  if (snd inst)==dummy_id then
+    right_instance_tac (fst inst)
+  else
+    left_instance_tac inst
+
+let quantified_tac lf backtrack continue seq gl=
+  let insts=give_instances lf seq in
+    tclORELSE
+      (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
+      backtrack gl
+
+
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
new file mode 100644
index 00000000..95dd22ea
--- /dev/null
+++ b/plugins/firstorder/instances.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Term
+open Tacmach
+open Names
+open Libnames
+open Rules
+
+val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
+
+val give_instances : Formula.t list -> Sequent.t ->
+  (Unify.instance * global_reference) list
+
+val quantified_tac : Formula.t list -> seqtac with_backtracking
+
+
+
+
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
new file mode 100644
index 00000000..515efea7
--- /dev/null
+++ b/plugins/firstorder/rules.ml
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*  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$ *)
+
+open Util
+open Names
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Termops
+open Declarations
+open Formula
+open Sequent
+open Libnames
+
+type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
+
+type lseqtac= global_reference -> seqtac
+
+type 'a with_backtracking = tactic -> 'a
+
+let wrap n b continue seq gls=
+  check_for_interrupt ();
+  let nc=pf_hyps gls in
+  let env=pf_env gls in
+  let rec aux i nc ctx=
+    if i<=0 then seq else
+      match nc with
+	  []->anomaly "Not the expected number of hyps"
+	| ((id,_,typ) as nd)::q->
+	    if occur_var env id (pf_concl gls) ||
+	      List.exists (occur_var_in_decl env id) ctx then
+		(aux (i-1) q (nd::ctx))
+	    else
+	      add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
+  let seq1=aux n nc [] in
+  let seq2=if b then
+    add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
+    continue seq2 gls
+
+let basename_of_global=function
+    VarRef id->id
+  | _->assert false
+
+let clear_global=function
+    VarRef id->clear [id]
+  | _->tclIDTAC
+
+
+(* connection rules *)
+
+let axiom_tac t seq=
+  try exact_no_check (constr_of_global (find_left t seq))
+  with Not_found->tclFAIL 0 (Pp.str "No axiom link")
+
+let ll_atom_tac a backtrack id continue seq=
+  tclIFTHENELSE
+    (try
+      tclTHENLIST
+	[generalize [mkApp(constr_of_global id,
+			   [|constr_of_global (find_left a seq)|])];
+	 clear_global id;
+	 intro]
+    with Not_found->tclFAIL 0 (Pp.str "No link"))
+    (wrap 1 false continue seq) backtrack
+
+(* right connectives rules *)
+
+let and_tac backtrack continue seq=
+  tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
+
+let or_tac backtrack continue seq=
+  tclORELSE
+    (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
+    backtrack
+
+let arrow_tac backtrack continue seq=
+  tclIFTHENELSE intro (wrap 1 true continue seq)
+    (tclORELSE
+       (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
+       backtrack)
+(* left connectives rules *)
+
+let left_and_tac ind backtrack id continue seq gls=
+ let n=(construct_nhyps ind gls).(0) in
+   tclIFTHENELSE
+     (tclTHENLIST
+      [simplest_elim (constr_of_global id);
+       clear_global id;
+       tclDO n intro])
+     (wrap n false continue seq)
+     backtrack gls
+
+let left_or_tac ind backtrack id continue seq gls=
+  let v=construct_nhyps ind gls in
+  let f n=
+    tclTHENLIST
+      [clear_global id;
+       tclDO n intro;
+       wrap n false continue seq] in
+    tclIFTHENSVELSE
+      (simplest_elim (constr_of_global id))
+      (Array.map f v)
+      backtrack gls
+
+let left_false_tac id=
+  simplest_elim (constr_of_global id)
+
+(* left arrow connective rules *)
+
+(* We use this function for false, and, or, exists *)
+
+let ll_ind_tac ind largs backtrack id continue seq gl=
+     let rcs=ind_hyps 0 ind largs gl in
+     let vargs=Array.of_list largs in
+	     (* construire le terme  H->B, le generaliser etc *)
+     let myterm i=
+       let rc=rcs.(i) in
+       let p=List.length rc in
+       let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
+       let vars=Array.init p (fun j->mkRel (p-j)) in
+       let capply=mkApp ((lift p cstr),vars) in
+       let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
+	 it_mkLambda_or_LetIn head rc in
+       let lp=Array.length rcs in
+       let newhyps=list_tabulate myterm lp in
+	 tclIFTHENELSE
+	   (tclTHENLIST
+	      [generalize newhyps;
+	       clear_global id;
+	       tclDO lp intro])
+	   (wrap lp false continue seq) backtrack gl
+
+let ll_arrow_tac a b c backtrack id continue seq=
+  let cc=mkProd(Anonymous,a,(lift 1 b)) in
+  let d=mkLambda (Anonymous,b,
+		  mkApp ((constr_of_global id),
+			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+    tclORELSE
+      (tclTHENS (cut c)
+	 [tclTHENLIST
+	    [introf;
+	     clear_global id;
+	     wrap 1 false continue seq];
+	  tclTHENS (cut cc)
+            [exact_no_check (constr_of_global id);
+	     tclTHENLIST
+	       [generalize [d];
+		clear_global id;
+		introf;
+		introf;
+		tclCOMPLETE (wrap 2 true continue seq)]]])
+      backtrack
+
+(* quantifier rules (easy side) *)
+
+let forall_tac backtrack continue seq=
+  tclORELSE
+    (tclIFTHENELSE intro (wrap 0 true continue seq)
+       (tclORELSE
+	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
+	  backtrack))
+    (if !qflag then
+       tclFAIL 0 (Pp.str "reversible in 1st order mode")
+     else
+       backtrack)
+
+let left_exists_tac ind backtrack id continue seq gls=
+  let n=(construct_nhyps ind gls).(0) in
+    tclIFTHENELSE
+      (simplest_elim (constr_of_global id))
+      (tclTHENLIST [clear_global id;
+                    tclDO n intro;
+                    (wrap (n-1) false continue seq)])
+      backtrack
+      gls
+
+let ll_forall_tac prod backtrack id continue seq=
+  tclORELSE
+    (tclTHENS (cut prod)
+       [tclTHENLIST
+	  [intro;
+	   (fun gls->
+	      let id0=pf_nth_hyp_id gls 1 in
+	      let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
+		tclTHEN (generalize [term]) (clear [id0]) gls);
+	   clear_global id;
+	   intro;
+	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
+	tclCOMPLETE (wrap 0 true continue (deepen seq))])
+    backtrack
+
+(* rules for instantiation with unification moved to instances.ml *)
+
+(* special for compatibility with old Intuition *)
+
+let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+
+let defined_connectives=lazy
+  [all_occurrences,EvalConstRef (destConst (constant "not"));
+   all_occurrences,EvalConstRef (destConst (constant "iff"))]
+
+let normalize_evaluables=
+  onAllHypsAndConcl
+    (function
+	 None->unfold_in_concl (Lazy.force defined_connectives)
+       | Some id ->
+	   unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
new file mode 100644
index 00000000..fc32621c
--- /dev/null
+++ b/plugins/firstorder/rules.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  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$ *)
+
+open Term
+open Tacmach
+open Names
+open Libnames
+
+type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
+
+type lseqtac= global_reference -> seqtac
+
+type 'a with_backtracking = tactic -> 'a
+
+val wrap : int -> bool -> seqtac
+
+val basename_of_global: global_reference -> identifier
+
+val clear_global: global_reference -> tactic
+
+val axiom_tac : constr -> Sequent.t -> tactic
+
+val ll_atom_tac : constr -> lseqtac with_backtracking
+
+val and_tac : seqtac with_backtracking
+
+val or_tac : seqtac with_backtracking
+
+val arrow_tac : seqtac with_backtracking
+
+val left_and_tac : inductive -> lseqtac with_backtracking
+
+val left_or_tac : inductive -> lseqtac with_backtracking
+
+val left_false_tac : global_reference -> tactic
+
+val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking
+
+val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
+
+val forall_tac : seqtac with_backtracking
+
+val left_exists_tac : inductive -> lseqtac with_backtracking
+
+val ll_forall_tac : types -> lseqtac with_backtracking
+
+val normalize_evaluables : tactic
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
new file mode 100644
index 00000000..685d44a8
--- /dev/null
+++ b/plugins/firstorder/sequent.ml
@@ -0,0 +1,312 @@
+(************************************************************************)
+(*  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$ *)
+
+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 expand_constructor_hints =
+  list_map_append (function
+    | IndRef ind ->
+	list_tabulate (fun i -> ConstructRef (ind,i+1))
+	  (Inductiveops.nconstructors ind)
+    | gr ->
+	[gr])
+
+let extend_with_ref_list l seq gl=
+  let l = expand_constructor_hints l in
+  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 seq
+
+open Auto
+
+let extend_with_auto_hints l seq gl=
+  let seqref=ref seq 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 "-----"))
+
+
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
new file mode 100644
index 00000000..ce0eddcc
--- /dev/null
+++ b/plugins/firstorder/sequent.mli
@@ -0,0 +1,66 @@
+(************************************************************************)
+(*  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$ *)
+
+open Term
+open Util
+open Formula
+open Tacmach
+open Names
+open Libnames
+
+module OrderedConstr: Set.OrderedType with type t=constr
+
+module CM: Map.S with type key=constr
+
+type h_item = global_reference * (int*constr) option
+
+module History: Set.S with type elt = h_item
+
+val cm_add : constr -> global_reference -> global_reference list CM.t ->
+  global_reference list CM.t
+
+val cm_remove : constr -> global_reference -> global_reference list CM.t ->
+  global_reference list CM.t
+
+module HP: Heap.S with type elt=Formula.t
+
+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}
+
+val deepen: t -> t
+
+val record: h_item -> t -> t
+
+val lookup: h_item -> t -> bool
+
+val add_formula : side -> global_reference -> constr -> t ->
+  Proof_type.goal sigma -> t
+
+val re_add_formula_list : Formula.t list -> t -> t
+
+val find_left : constr -> t -> global_reference
+
+val take_formula : t -> Formula.t * t
+
+val empty_seq : int -> t
+
+val extend_with_ref_list : global_reference list ->
+  t -> Proof_type.goal sigma -> t
+
+val extend_with_auto_hints : Auto.hint_db_name list ->
+  t -> Proof_type.goal sigma -> t
+
+val print_cmap: global_reference list CM.t -> unit
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
new file mode 100644
index 00000000..e3a4c6a5
--- /dev/null
+++ b/plugins/firstorder/unify.ml
@@ -0,0 +1,143 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Util
+open Formula
+open Tacmach
+open Term
+open Names
+open Termops
+open Reductionops
+
+exception UFAIL of constr*constr
+
+(*
+   RIGID-only Martelli-Montanari style unification for CLOSED terms
+   I repeat : t1 and t2 must NOT have ANY free deBruijn
+   sigma is kept normal with respect to itself but is lazily applied
+   to the equation set. Raises UFAIL with a pair of  terms
+*)
+
+let unif t1 t2=
+  let bige=Queue.create ()
+  and sigma=ref [] in
+  let bind i t=
+    sigma:=(i,t)::
+      (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in
+  let rec head_reduce t=
+    (* forbids non-sigma-normal meta in head position*)
+    match kind_of_term t with
+	Meta i->
+	  (try
+	     head_reduce (List.assoc i !sigma)
+	   with Not_found->t)
+      | _->t in
+    Queue.add (t1,t2) bige;
+    try while true do
+      let t1,t2=Queue.take bige in
+      let nt1=head_reduce (whd_betaiotazeta Evd.empty t1)
+      and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
+	match (kind_of_term nt1),(kind_of_term nt2) with
+	    Meta i,Meta j->
+	      if i<>j then
+		if i<j then bind j nt1
+		else bind i nt2
+	  | Meta i,_ ->
+	      let t=subst_meta !sigma nt2 in
+		if Intset.is_empty (free_rels t) &&
+		  not (occur_term (mkMeta i) t) then
+		    bind i t else raise (UFAIL(nt1,nt2))
+	  | _,Meta i ->
+	      let t=subst_meta !sigma nt1 in
+		if Intset.is_empty (free_rels t) &&
+		  not (occur_term (mkMeta i) t) then
+		    bind i t else raise (UFAIL(nt1,nt2))
+	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
+ 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
+	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
+	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
+	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
+	      Queue.add (pa,pb) bige;
+	      Queue.add (ca,cb) bige;
+	      let l=Array.length va in
+		if l<>(Array.length vb) then
+		  raise (UFAIL (nt1,nt2))
+		else
+		  for i=0 to l-1 do
+		    Queue.add (va.(i),vb.(i)) bige
+		  done
+	  | App(ha,va),App(hb,vb)->
+	      Queue.add (ha,hb) bige;
+	      let l=Array.length va in
+		if l<>(Array.length vb) then
+		  raise (UFAIL (nt1,nt2))
+		else
+		  for i=0 to l-1 do
+		    Queue.add (va.(i),vb.(i)) bige
+		  done
+	  | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
+    done;
+      assert false
+	(* this place is unreachable but needed for the sake of typing *)
+    with Queue.Empty-> !sigma
+
+let value i t=
+  let add x y=
+    if x<0 then y else if y<0 then x else x+y in
+  let tref=mkMeta i in
+  let rec vaux term=
+    if term=tref then 0 else
+      let f v t=add v (vaux t) in
+      let vr=fold_constr f (-1) term in
+	if vr<0 then -1 else vr+1 in
+    vaux t
+
+type instance=
+    Real of (int*constr)*int
+  | Phantom of constr
+
+let mk_rel_inst t=
+  let new_rel=ref 1 in
+  let rel_env=ref [] in
+  let rec renum_rec d t=
+    match kind_of_term t with
+	Meta n->
+	  (try
+	     mkRel (d+(List.assoc n !rel_env))
+	   with Not_found->
+	     let m= !new_rel in
+	       incr new_rel;
+	       rel_env:=(n,m) :: !rel_env;
+	       mkRel (m+d))
+      | _ -> map_constr_with_binders succ renum_rec d t
+  in
+  let nt=renum_rec 0 t in (!new_rel - 1,nt)
+
+let unif_atoms i dom t1 t2=
+  try
+    let t=List.assoc i (unif t1 t2) in
+      if isMeta t then Some (Phantom dom)
+      else Some (Real(mk_rel_inst t,value i t1))
+  with
+      UFAIL(_,_) ->None
+    | Not_found ->Some (Phantom dom)
+
+let renum_metas_from k n t= (* requires n = max (free_rels t) *)
+  let l=list_tabulate (fun i->mkMeta (k+i)) n in
+    substl l t
+
+let more_general (m1,t1) (m2,t2)=
+  let mt1=renum_metas_from 0 m1 t1
+  and mt2=renum_metas_from m1 m2 t2 in
+    try
+      let sigma=unif mt1 mt2 in
+      let p (n,t)= n<m1 || isMeta t in
+	List.for_all p sigma
+    with UFAIL(_,_)->false
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
new file mode 100644
index 00000000..d6cb3a08
--- /dev/null
+++ b/plugins/firstorder/unify.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  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$ *)
+
+open Term
+
+exception UFAIL of constr*constr
+
+val unif : constr -> constr -> (int*constr) list
+
+type instance=
+    Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
+  | Phantom of constr        (* domaine de quantification *)
+
+val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
+
+val more_general : (int*constr) -> (int*constr) -> bool