diff options
Diffstat (limited to 'contrib/first-order')
| -rw-r--r-- | contrib/first-order/ground.ml4 | 4 | ||||
| -rw-r--r-- | contrib/first-order/instances.ml | 178 | ||||
| -rw-r--r-- | contrib/first-order/instances.mli | 40 | ||||
| -rw-r--r-- | contrib/first-order/rules.ml | 60 | ||||
| -rw-r--r-- | contrib/first-order/rules.mli | 32 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 12 | ||||
| -rw-r--r-- | contrib/first-order/sequent.mli | 8 | ||||
| -rw-r--r-- | contrib/first-order/unify.ml | 110 | ||||
| -rw-r--r-- | contrib/first-order/unify.mli | 15 |
9 files changed, 267 insertions, 192 deletions
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4 index f0cd3afa6..b8f684977 100644 --- a/contrib/first-order/ground.ml4 +++ b/contrib/first-order/ground.ml4 @@ -13,6 +13,7 @@ open Formula open Sequent open Rules +open Instances open Term open Tacmach open Tactics @@ -79,7 +80,8 @@ let ground_tac solver startseq gl= cont_tac gl else (match - Unify.give_right_instances i dom triv atoms seq with + Instances.give_right_instances i dom triv atoms seq + with Some l -> tclORELSE (exists_tac l toptac (re_add seq)) cont_tac gl | None -> diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml new file mode 100644 index 000000000..8625c988d --- /dev/null +++ b/contrib/first-order/instances.ml @@ -0,0 +1,178 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \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 Tacmach +open Tactics +open Tacticals +open Termops +open Reductionops +open Declarations +open Formula +open Sequent +open Libnames + +let rev_rels n t= (* requires n = max (free_rels t) *) + let l=list_tabulate (fun i->mkRel (n-i)) n in + substl l t + +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 + +(* ordre lexico: + nombre de metas dans terme; + profondeur de matching; + le reste +*) + +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 n2 n1 c1 c2 + | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1 + | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 + +module OrderedRightInstance= +struct + type t = instance + let compare = compare_instance +end + +module OrderedLeftInstance= +struct + type t=instance * Libnames.global_reference + let compare (inst1,id1) (inst2,id2)= + (compare_instance =? Pervasives.compare) inst1 inst2 id1 id2 + (* we want a __decreasing__ total order *) +end + +module RIS=Set.Make(OrderedRightInstance) +module LIS=Set.Make(OrderedLeftInstance) + +let make_goal_atoms seq= + match seq.gl with + Atomic t->{negative=[];positive=[t]} + | Complex (_,_,l)->l + +let make_left_atoms seq= + {negative=seq.latoms;positive=[]} + +let do_sequent setref triv add mkelt 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:=add (mkelt c) !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_left_atoms seq); + do_atoms atoms (make_goal_atoms seq); + !flag && !phref + +let give_right_instances i dom triv atoms seq= + let setref=ref RIS.empty in + let inj inst=inst in + if do_sequent setref triv RIS.add inj seq i dom atoms then + None + else + Some (RIS.elements !setref) + +let match_one_forall_hyp setref seq lf= + match lf.pat with + Lforall(i,dom,triv)-> + let inj x=(x,lf.id) in + if do_sequent setref triv LIS.add inj seq i dom lf.atoms then + setref:=LIS.add ((Phantom dom),lf.id) !setref + | _ ->anomaly "can't happen" + +let give_left_instances lfh seq= + let setref=ref LIS.empty in + List.iter (match_one_forall_hyp setref seq) lfh; + LIS.elements !setref + +(*tactics*) + + +let rec collect_forall seq= + if is_empty_left seq then ([],seq) + else + let hd,seq1=take_left seq in + (match hd.pat with + Lforall(_,_,_)-> + let (q,seq2)=collect_forall seq1 in + ((hd::q),seq2) + | _->[],seq) + +let left_instance_tac (inst,id) tacrec seq= + match inst with + Phantom dom-> + if lookup (id,None) seq then + tclFAIL 0 "already done" + else + tclTHENS (cut dom) + [tclTHENLIST + [intro; + (fun gls->generalize + [mkApp(constr_of_reference id, + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); + intro; + tclSOLVE [wrap 1 false tacrec + (deepen (record (id,None) seq))]]; + tclTRY assumption] + | Real((m,t) as c,_)-> + if lookup (id,Some c) seq || m>0 then + tclFAIL 0 "already done" + else + tclTHENLIST + [generalize [mkApp(constr_of_reference id,[|t|])]; + intro; + tclSOLVE + [wrap 1 false tacrec + (deepen (record (id,Some c) seq))]] + +let left_forall_tac lfp tacrec seq gl= + let insts=give_left_instances lfp seq in + tclFIRST (List.map (fun inst->left_instance_tac inst tacrec seq) insts) gl + +let dummy_exists_tac dom tacrec seq= + tclTHENS (cut dom) + [tclTHENLIST + [intro; + (fun gls-> + split (Rawterm.ImplicitBindings + [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + tclSOLVE [wrap 0 false tacrec (deepen seq)]]; + tclTRY assumption] + +let right_instance_tac inst tacrec seq= + match inst with + Phantom _ ->anomaly "can't happen" + | Real ((m,t),_) -> + if m>0 then tclFAIL 0 "not implemented ... yes" + else + tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclSOLVE [wrap 0 true tacrec (deepen seq)]) + +let exists_tac insts tacrec seq gl= + tclFIRST + (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl + diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli new file mode 100644 index 000000000..b1d88280b --- /dev/null +++ b/contrib/first-order/instances.mli @@ -0,0 +1,40 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \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 give_right_instances : metavariable -> constr -> bool -> Formula.atoms -> + Sequent.t -> Unify.instance list option + +val give_left_instances : Formula.left_formula list-> Sequent.t -> + (Unify.instance*global_reference) list + +val collect_forall : Sequent.t -> Formula.left_formula list * Sequent.t + +val left_instance_tac : Unify.instance * global_reference -> seqtac + +val left_forall_tac : Formula.left_formula list -> seqtac + +val dummy_exists_tac : constr -> seqtac + +val right_instance_tac : Unify.instance -> seqtac + +val exists_tac : Unify.instance list -> seqtac + + + + + + + diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index 01ae688ad..c5c7319e8 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -19,7 +19,6 @@ open Reductionops open Declarations open Formula open Sequent -open Unify open Libnames type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -193,64 +192,7 @@ let ll_forall_tac prod id tacrec seq= (* complicated stuff for instantiation with unification *) -let rec collect_forall seq= - if is_empty_left seq then ([],seq) - else - let hd,seq1=take_left seq in - (match hd.pat with - Lforall(_,_,_)-> - let (q,seq2)=collect_forall seq1 in - ((hd::q),seq2) - | _->[],seq) - -let left_instance_tac (inst,id) tacrec seq= - match inst with - Phantom dom-> - if lookup id None seq then - tclFAIL 0 "already done" - else - tclTHENS (cut dom) - [tclTHENLIST - [intro; - (fun gls->generalize - [mkApp(constr_of_reference id, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); - intro; - tclSOLVE [wrap 1 false tacrec - (deepen (record id None seq))]]; - tclTRY assumption] - | Real(t,_)-> - if lookup id (Some t) seq then - tclFAIL 0 "already done" - else - tclTHENLIST - [generalize [mkApp(constr_of_reference id,[|t|])]; - intro; - tclSOLVE - [wrap 1 false tacrec - (deepen (record id (Some t) seq))]] - -let left_forall_tac lfp tacrec seq gl= - let insts=give_left_instances lfp seq in - tclFIRST (List.map (fun inst->left_instance_tac inst tacrec seq) insts) gl - -let dummy_exists_tac dom tacrec seq= - tclTHENS (cut dom) - [tclTHENLIST - [intro; - (fun gls-> - split (Rawterm.ImplicitBindings - [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); - tclSOLVE [wrap 0 false tacrec (deepen seq)]]; - tclTRY assumption] - -let right_instance_tac (t,_) tacrec seq= - tclTHEN (split (Rawterm.ImplicitBindings [t])) - (tclSOLVE [wrap 0 true tacrec (deepen seq)]) - -let exists_tac insts tacrec seq gl= - tclFIRST - (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl +(* moved to instances.ml *) (* special for compatibility with old Intuition *) diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli index 045316263..10ffe863d 100644 --- a/contrib/first-order/rules.mli +++ b/contrib/first-order/rules.mli @@ -19,47 +19,37 @@ type lseqtac= global_reference -> seqtac 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 + val evaluable_tac : evaluable_global_reference -> seqtac val left_evaluable_tac : evaluable_global_reference -> lseqtac val and_tac : seqtac -val left_and_tac : inductive -> lseqtac - val or_tac : seqtac -val left_or_tac : inductive -> lseqtac - -val forall_tac : seqtac - -val collect_forall : Sequent.t -> Formula.left_formula list * Sequent.t - -val left_instance_tac : Unify.instance * global_reference -> seqtac - -val left_forall_tac : Formula.left_formula list -> seqtac - val arrow_tac : seqtac -val dummy_exists_tac : constr -> seqtac +val left_and_tac : inductive -> lseqtac -val right_instance_tac : constr * int -> seqtac +val left_or_tac : inductive -> lseqtac -val exists_tac : (constr * int) list -> seqtac - -val left_exists_tac : inductive -> lseqtac +val left_false_tac : global_reference -> tactic -val ll_arrow_tac : constr -> constr -> constr -> lseqtac +val ll_ind_tac : inductive -> constr list -> lseqtac -val ll_atom_tac : constr -> lseqtac +val ll_arrow_tac : constr -> constr -> constr -> lseqtac -val left_false_tac : global_reference -> tactic +val forall_tac : seqtac -val ll_ind_tac : inductive -> constr list -> lseqtac +val left_exists_tac : inductive -> lseqtac val ll_forall_tac : types -> lseqtac diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 4ece7c8c5..91a8f1ddd 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -11,6 +11,7 @@ open Term open Util open Formula +open Unify open Tacmach open Names open Libnames @@ -120,14 +121,17 @@ struct let compare=compare_constr end +type h_item = global_reference * (int*constr) option + module Hitem= struct - type t=(global_reference * constr option) + type t = h_item let compare (id1,co1) (id2,co2)= (Pervasives.compare =? (fun oc1 oc2 -> match oc1,oc2 with - Some c1,Some c2 -> OrderedConstr.compare c1 c2 + Some (m1,c1),Some (m2,c2) -> + ((-) =? OrderedConstr.compare) m1 m2 c1 c2 | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2 end @@ -163,9 +167,9 @@ type t= let deepen seq={seq with depth=seq.depth-1} -let record id topt seq={seq with history=History.add (id,topt) seq.history} +let record item seq={seq with history=History.add item seq.history} -let lookup id topt seq=History.mem (id,topt) seq.history +let lookup item seq=History.mem item seq.history let add_left (nam,t) seq internal gl= match build_left_entry nam t internal gl seq.cnt with diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli index 851396d45..79cf0d1ed 100644 --- a/contrib/first-order/sequent.mli +++ b/contrib/first-order/sequent.mli @@ -23,7 +23,9 @@ module OrderedConstr: Set.OrderedType with type t=constr module CM: Map.S with type key=constr -module History: Set.S with type elt = global_reference * constr option +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 @@ -43,9 +45,9 @@ type t = {redexes:HP.t; val deepen: t -> t -val record: global_reference -> constr option -> t -> t +val record: h_item -> t -> t -val lookup: global_reference -> constr option -> t -> bool +val lookup: h_item -> t -> bool val add_left : global_reference * constr -> t -> bool -> Proof_type.goal sigma -> t diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml index b9c3a1a42..30ff1c811 100644 --- a/contrib/first-order/unify.ml +++ b/contrib/first-order/unify.ml @@ -10,17 +10,22 @@ open Util open Formula -open Sequent open Tacmach open Term open Names open Termops -open Pattern open Reductionops exception UFAIL of constr*constr -let unif t1 t2= (* Martelli-Montanari style *) +(* + 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= @@ -83,9 +88,6 @@ let unif t1 t2= (* Martelli-Montanari style *) (* this place is unreachable but needed for the sake of typing *) with Queue.Empty-> !sigma -(* collect tries finds ground instantiations for Meta i*) -let is_ground t=(Clenv.collect_metas t)=[] - let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false let value i t= @@ -100,7 +102,7 @@ let value i t= vaux t type instance= - Real of (constr*int) (* instance*valeur heuristique*) + Real of (int*constr)*int (* nb trous*terme*valeur heuristique *) | Phantom of constr (* domaine de quantification *) let mk_rel_inst t= @@ -118,97 +120,15 @@ let mk_rel_inst t= 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 nt=renum_rec 0 t in (!new_rel - 1,nt) + let unif_atoms i dom t1 t2= - if is_head_meta t1 || is_head_meta t2 then None else + if is_head_meta t1 || is_head_meta t2 then None else try let t=List.assoc i (unif t1 t2) in - if is_ground t then Some (Real(t,value i t1)) - else if is_head_meta t then Some (Phantom dom) - else None + if is_head_meta t then Some (Phantom dom) + else Some (Real(mk_rel_inst t,value i t1)) with UFAIL(_,_) ->None | Not_found ->Some (Phantom dom) - -(* ordre lexico: - nombre de metas dans terme; - profondeur de matching; - le reste -*) - - -let compare_instance inst1 inst2= - match inst1,inst2 with - Phantom(d1),Phantom(d2)-> - (OrderedConstr.compare d1 d2) - | Real(c1,n1),Real(c2,n2)-> - ((-) =? OrderedConstr.compare) n2 n1 c1 c2 - | Phantom(_),_-> 1 - | _,_-> -1 - -module OrderedRightInstance= -struct - type t = constr*int - let compare (c1,n1) (c2,n2) = ((-) =? OrderedConstr.compare) n2 n1 c1 c2 -end - -module OrderedLeftInstance= -struct - type t=instance * Libnames.global_reference - let compare (inst1,id1) (inst2,id2)= - (compare_instance =? Pervasives.compare) inst1 inst2 id1 id2 - (* we want a __decreasing__ total order *) -end - -module RIS=Set.Make(OrderedRightInstance) -module LIS=Set.Make(OrderedLeftInstance) - -let make_goal_atoms seq= - match seq.gl with - Atomic t->{negative=[];positive=[t]} - | Complex (_,_,l)->l - -let make_left_atoms seq= - {negative=seq.latoms;positive=[]} - -let do_sequent setref triv add mkelt 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:=add (mkelt c) !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_left_atoms seq); - do_atoms atoms (make_goal_atoms seq); - !flag && !phref - -let give_right_instances i dom triv atoms seq= - let setref=ref RIS.empty in - let inj=function - Real c->c - | _->anomaly "can't happen" in - if do_sequent setref triv RIS.add inj seq i dom atoms then - None - else - Some (RIS.elements !setref) - -let match_one_forall_hyp setref seq lf= - match lf.pat with - Lforall(i,dom,triv)-> - let inj x=(x,lf.id) in - if do_sequent setref triv LIS.add inj seq i dom lf.atoms then - setref:=LIS.add ((Phantom dom),lf.id) !setref - | _ ->anomaly "can't happen" - -let give_left_instances lfh seq= - let setref=ref LIS.empty in - List.iter (match_one_forall_hyp setref seq) lfh; - LIS.elements !setref - + diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli index 7effac207..013fc73cd 100644 --- a/contrib/first-order/unify.mli +++ b/contrib/first-order/unify.mli @@ -8,17 +8,14 @@ (* $Id$ *) -open Libnames open Term +exception UFAIL of constr*constr + +val unif : constr -> constr -> (int*constr) list + type instance= - Real of (constr*int) (* instance*valeur heuristique*) - | Phantom of constr (* domaine de quantification *) + 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 give_right_instances : metavariable -> constr -> bool -> Formula.atoms -> - Sequent.t -> (constr*int) list option - -val give_left_instances : Formula.left_formula list-> Sequent.t -> - (instance*global_reference) list |