summaryrefslogtreecommitdiff
path: root/contrib/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/firstorder')
-rw-r--r--contrib/firstorder/formula.ml270
-rw-r--r--contrib/firstorder/formula.mli77
-rw-r--r--contrib/firstorder/g_ground.ml4128
-rw-r--r--contrib/firstorder/ground.ml152
-rw-r--r--contrib/firstorder/ground.mli13
-rw-r--r--contrib/firstorder/instances.ml206
-rw-r--r--contrib/firstorder/instances.mli26
-rw-r--r--contrib/firstorder/rules.ml216
-rw-r--r--contrib/firstorder/rules.mli54
-rw-r--r--contrib/firstorder/sequent.ml303
-rw-r--r--contrib/firstorder/sequent.mli66
-rw-r--r--contrib/firstorder/unify.ml143
-rw-r--r--contrib/firstorder/unify.mli23
13 files changed, 1677 insertions, 0 deletions
diff --git a/contrib/firstorder/formula.ml b/contrib/firstorder/formula.ml
new file mode 100644
index 00000000..3e49cd9c
--- /dev/null
+++ b/contrib/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: formula.ml 10785 2008-04-13 21:41:54Z herbelin $ *)
+
+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 (Sign.decompose_prod_n_assum nevar t1) in
+ fst (Sign.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/contrib/firstorder/formula.mli b/contrib/firstorder/formula.mli
new file mode 100644
index 00000000..8703045c
--- /dev/null
+++ b/contrib/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: formula.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
+
+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 -> Sign.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/contrib/firstorder/g_ground.ml4 b/contrib/firstorder/g_ground.ml4
new file mode 100644
index 00000000..f7b0a546
--- /dev/null
+++ b/contrib/firstorder/g_ground.ml4
@@ -0,0 +1,128 @@
+(************************************************************************)
+(* 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: g_ground.ml4 10346 2007-12-05 21:11:19Z aspiwack $ *)
+
+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=SecondaryTable("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=SecondaryTable("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")
+
+type external_env=
+ Ids of global_reference list
+ | Bases of Auto.hint_db_name list
+ | Void
+
+let gen_ground_tac flag taco ext gl=
+ let backup= !qflag in
+ try
+ qflag:=flag;
+ let solver=
+ match taco with
+ Some tac-> tac
+ | None-> default_solver in
+ let startseq=
+ match ext with
+ Void -> (fun gl -> empty_seq !ground_depth)
+ | Ids l-> create_with_ref_list l !ground_depth
+ | Bases l-> create_with_auto_hints l !ground_depth 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=
+ onAllClauses
+ (function
+ None->unfold_in_concl (Lazy.force defined_connectives)
+ | Some id->
+ unfold_in_hyp (Lazy.force defined_connectives)
+ (Tacexpr.InHypType id)) *)
+
+TACTIC EXTEND firstorder
+ [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] ->
+ [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ]
+| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
+ [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ]
+| [ "firstorder" tactic_opt(t) ] ->
+ [ gen_ground_tac true (Option.map eval_tactic t) Void ]
+END
+
+TACTIC EXTEND gintuition
+ [ "gintuition" tactic_opt(t) ] ->
+ [ gen_ground_tac false (Option.map eval_tactic t) Void ]
+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 [])))
+ Void) gls
+
+
+
+let () =
+ Decl_proof_instr.register_automation_tac default_declarative_automation
+
diff --git a/contrib/firstorder/ground.ml b/contrib/firstorder/ground.ml
new file mode 100644
index 00000000..f4661869
--- /dev/null
+++ b/contrib/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: ground.ml 9549 2007-01-28 23:30:12Z corbinea $ *)
+
+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/contrib/firstorder/ground.mli b/contrib/firstorder/ground.mli
new file mode 100644
index 00000000..621f99db
--- /dev/null
+++ b/contrib/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: ground.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
+
+val ground_tac: Tacmach.tactic ->
+ (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
+
diff --git a/contrib/firstorder/instances.ml b/contrib/firstorder/instances.ml
new file mode 100644
index 00000000..1432207d
--- /dev/null
+++ b/contrib/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: instances.ml 10410 2007-12-31 13:11:55Z msozeau $ 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
+ Sign.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/contrib/firstorder/instances.mli b/contrib/firstorder/instances.mli
new file mode 100644
index 00000000..7667c89f
--- /dev/null
+++ b/contrib/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: instances.mli 5920 2004-07-16 20:01:26Z herbelin $ 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/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml
new file mode 100644
index 00000000..b8b56548
--- /dev/null
+++ b/contrib/firstorder/rules.ml
@@ -0,0 +1,216 @@
+(************************************************************************)
+(* 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: rules.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+
+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 id_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
+ Sign.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=
+ onAllClauses
+ (function
+ None->unfold_in_concl (Lazy.force defined_connectives)
+ | Some ((_,id),_)->
+ unfold_in_hyp (Lazy.force defined_connectives)
+ ((Rawterm.all_occurrences_expr,id),Tacexpr.InHypTypeOnly))
diff --git a/contrib/firstorder/rules.mli b/contrib/firstorder/rules.mli
new file mode 100644
index 00000000..3798d8d4
--- /dev/null
+++ b/contrib/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: rules.mli 6141 2004-09-27 14:55:34Z corbinea $ *)
+
+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 id_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/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml
new file mode 100644
index 00000000..c832d30f
--- /dev/null
+++ b/contrib/firstorder/sequent.ml
@@ -0,0 +1,303 @@
+(************************************************************************)
+(* 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 10824 2008-04-21 13:57:03Z msozeau $ *)
+
+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 (snd 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/contrib/firstorder/sequent.mli b/contrib/firstorder/sequent.mli
new file mode 100644
index 00000000..47fb74c7
--- /dev/null
+++ b/contrib/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: sequent.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
+
+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 create_with_ref_list : global_reference list ->
+ int -> Proof_type.goal sigma -> t
+
+val create_with_auto_hints : Auto.hint_db_name list ->
+ int -> Proof_type.goal sigma -> t
+
+val print_cmap: global_reference list CM.t -> unit
diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml
new file mode 100644
index 00000000..1dd13cbe
--- /dev/null
+++ b/contrib/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: unify.ml 7639 2005-12-02 10:01:15Z gregoire $ 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 t1)
+ and nt2=head_reduce (whd_betaiotazeta 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/contrib/firstorder/unify.mli b/contrib/firstorder/unify.mli
new file mode 100644
index 00000000..9fbe3dda
--- /dev/null
+++ b/contrib/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: unify.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
+
+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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 15:20:01 +0000