diff options
Diffstat (limited to 'contrib/cc')
| -rw-r--r-- | contrib/cc/ccalgo.ml | 698 | ||||
| -rw-r--r-- | contrib/cc/ccalgo.mli | 104 | ||||
| -rw-r--r-- | contrib/cc/ccproof.ml | 89 | ||||
| -rw-r--r-- | contrib/cc/ccproof.mli | 25 | ||||
| -rw-r--r-- | contrib/cc/cctac.ml | 336 | ||||
| -rw-r--r-- | contrib/cc/cctac.ml4 | 247 | ||||
| -rw-r--r-- | contrib/cc/cctac.mli (renamed from contrib/cc/CCSolve.v) | 20 | ||||
| -rw-r--r-- | contrib/cc/g_congruence.ml4 | 29 |
8 files changed, 929 insertions, 619 deletions
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml index e73a6221..3e2d11a2 100644 --- a/contrib/cc/ccalgo.ml +++ b/contrib/cc/ccalgo.ml @@ -6,45 +6,33 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccalgo.ml,v 1.6.2.1 2004/07/16 19:29:58 herbelin Exp $ *) +(* $Id: ccalgo.ml 7298 2005-08-17 12:56:38Z corbinea $ *) (* This file implements the basic congruence-closure algorithm by *) (* Downey,Sethi and Tarjan. *) open Util +open Pp +open Goptions open Names open Term -let init_size=251 +let init_size=5 -type pa_constructor= - {head_constr: int; - arity:int; - nhyps:int; - args:int list; - term_head:int} - - -module PacMap=Map.Make(struct type t=int*int let compare=compare end) - -type term= - Symb of constr - | Appli of term*term - | Constructor of constructor*int*int (* constructor arity+ nhyps *) +let cc_verbose=ref false -type rule= - Congruence - | Axiom of identifier - | Injection of int*int*int*int (* terms+head+arg position *) +let debug msg (stdpp:std_ppcmds) = + if !cc_verbose then msg stdpp -type equality = {lhs:int;rhs:int;rule:rule} - -let swap eq= - let swap_rule=match eq.rule with - Congruence -> Congruence - | Injection (i,j,c,a) -> Injection (j,i,c,a) - | Axiom id -> anomaly "no symmetry for axioms" - in {lhs=eq.rhs;rhs=eq.lhs;rule=swap_rule} +let _= + let gdopt= + { optsync=true; + optname="Congruence Verbose"; + optkey=SecondaryTable("Congruence","Verbose"); + optread=(fun ()-> !cc_verbose); + optwrite=(fun b -> cc_verbose := b)} + in + declare_bool_option gdopt (* Signature table *) @@ -68,290 +56,452 @@ module ST=struct let query sign st=Hashtbl.find st.toterm sign - let delete t st= + let delete st t= try let sign=Hashtbl.find st.tosign t in Hashtbl.remove st.toterm sign; Hashtbl.remove st.tosign t with Not_found -> () - let rec delete_list l st= - match l with - []->() - | t::q -> delete t st;delete_list q st + let rec delete_set st s = Intset.iter (delete st) s end - -(* Basic Union-Find algo w/o path compression *) - -module UF = struct -module IndMap=Map.Make(struct type t=inductive let compare=compare end) +type pa_constructor= + { cnode : int; + arity : int; + args : int list} - type representative= - {mutable nfathers:int; - mutable fathers:int list; - mutable constructors:pa_constructor PacMap.t; - mutable inductives:(int * int) IndMap.t} +module PacMap=Map.Make(struct + type t=pa_constructor + let compare=Pervasives.compare end) - type cl = Rep of representative| Eqto of int*equality +type cinfo= + {ci_constr: constructor; (* inductive type *) + ci_arity: int; (* # args *) + ci_nhyps: int} (* # projectable args *) - type vertex = Leaf| Node of (int*int) +type term= + Symb of constr + | Eps + | Appli of term*term + | Constructor of cinfo (* constructor arity + nhyps *) - type node = - {clas:cl; - vertex:vertex; - term:term; - mutable node_constr: int PacMap.t} +type rule= + Congruence + | Axiom of identifier * bool + | Injection of int * pa_constructor * int * pa_constructor * int - type t={mutable size:int; - map:(int,node) Hashtbl.t; - syms:(term,int) Hashtbl.t; - sigtable:ST.t} +type from= + Goal + | Hyp of identifier + | HeqG of identifier + | HeqnH of identifier * identifier - let empty ():t={size=0; - map=Hashtbl.create init_size; - syms=Hashtbl.create init_size; - sigtable=ST.empty ()} +type 'a eq = {lhs:int;rhs:int;rule:'a} - let rec find uf i= - match (Hashtbl.find uf.map i).clas with - Rep _ -> i - | Eqto (j,_) ->find uf j - - let get_representative uf i= - let node=Hashtbl.find uf.map i in - match node.clas with - Rep r ->r - | _ -> anomaly "get_representative: not a representative" +type equality = rule eq + +type disequality = from eq - let get_constructor uf i= - match (Hashtbl.find uf.map i).term with - Constructor (cstr,_,_)->cstr - | _ -> anomaly "get_constructor: not a constructor" +let swap eq : equality = + let swap_rule=match eq.rule with + Congruence -> Congruence + | Injection (i,pi,j,pj,k) -> Injection (j,pj,i,pi,k) + | Axiom (id,reversed) -> Axiom (id,not reversed) + in {lhs=eq.rhs;rhs=eq.lhs;rule=swap_rule} + +type inductive_status = + Unknown + | Partial of pa_constructor + | Partial_applied + | Total of (int * pa_constructor) + +type representative= + {mutable nfathers:int; + mutable lfathers:Intset.t; + mutable fathers:Intset.t; + mutable inductive_status: inductive_status; + mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *) + +type cl = Rep of representative| Eqto of int*equality + +type vertex = Leaf| Node of (int*int) + +type node = + {mutable clas:cl; + mutable cpath: int; + vertex:vertex; + term:term} + +type forest= + {mutable max_size:int; + mutable size:int; + mutable map: node array; + axioms: (identifier,term*term) Hashtbl.t; + mutable epsilons: pa_constructor list; + syms:(term,int) Hashtbl.t} + +type state = + {uf: forest; + sigtable:ST.t; + mutable terms: Intset.t; + combine: equality Queue.t; + marks: (int * pa_constructor) Queue.t; + mutable diseq: disequality list; + mutable pa_classes: Intset.t} + +let dummy_node = + {clas=Eqto(min_int,{lhs=min_int;rhs=min_int;rule=Congruence}); + cpath=min_int; + vertex=Leaf; + term=Symb (mkRel min_int)} + +let empty ():state = + {uf= + {max_size=init_size; + size=0; + map=Array.create init_size dummy_node; + epsilons=[]; + axioms=Hashtbl.create init_size; + syms=Hashtbl.create init_size}; + terms=Intset.empty; + combine=Queue.create (); + marks=Queue.create (); + sigtable=ST.empty (); + diseq=[]; + pa_classes=Intset.empty} + +let forest state = state.uf + +let compress_path uf i j = uf.map.(j).cpath<-i + +let rec find_aux uf visited i= + let j = uf.map.(i).cpath in + if j<0 then let _ = List.iter (compress_path uf i) visited in i else + find_aux uf (i::visited) j + +let find uf i= find_aux uf [] i + +let get_representative uf i= + match uf.map.(i).clas with + Rep r -> r + | _ -> anomaly "get_representative: not a representative" + +let find_pac uf i pac = + PacMap.find pac (get_representative uf i).constructors + +let get_constructor_info uf i= + match uf.map.(i).term with + Constructor cinfo->cinfo + | _ -> anomaly "get_constructor: not a constructor" + +let size uf i= + (get_representative uf i).nfathers +let axioms uf = uf.axioms - let fathers uf i= - (get_representative uf i).fathers - - let size uf i= - (get_representative uf i).nfathers +let epsilons uf = uf.epsilons - let add_father uf i t= - let r=get_representative uf i in - r.nfathers<-r.nfathers+1; - r.fathers<-t::r.fathers +let add_lfather uf i t= + let r=get_representative uf i in + r.nfathers<-r.nfathers+1; + r.lfathers<-Intset.add t r.lfathers; + r.fathers <-Intset.add t r.fathers - let pac_map uf i= - (get_representative uf i).constructors +let add_rfather uf i t= + let r=get_representative uf i in + r.nfathers<-r.nfathers+1; + r.fathers <-Intset.add t r.fathers - let pac_arity uf i sg= - (PacMap.find sg (get_representative uf i).constructors).arity +exception Discriminable of int * pa_constructor * int * pa_constructor - let add_node_pac uf i sg j= - let node=Hashtbl.find uf.map i in - if not (PacMap.mem sg node.node_constr) then - node.node_constr<-PacMap.add sg j node.node_constr - - let mem_node_pac uf i sg= - PacMap.find sg (Hashtbl.find uf.map i).node_constr - - exception Discriminable of int * int * int * int * t - - let add_pacs uf i pacs = - let rep=get_representative uf i in - let pending=ref [] and combine=ref [] in - let add_pac sg pac= - try - let opac=PacMap.find sg rep.constructors in - if (snd sg)>0 then () else - let tk=pac.term_head - and tl=opac.term_head in - let rec f n lk ll q= - if n > 0 then match (lk,ll) with - k::qk,l::ql-> - let eq= - {lhs=k;rhs=l;rule=Injection(tk,tl,pac.head_constr,n)} - in f (n-1) qk ql (eq::q) - | _-> anomaly - "add_pacs : weird error in injection subterms merge" - else q in - combine:=f pac.nhyps pac.args opac.args !combine - with Not_found -> (* Still Unknown Constructor *) - rep.constructors <- PacMap.add sg pac rep.constructors; - pending:= - (fathers uf (find uf pac.term_head)) @rep.fathers@ !pending; - let (c,a)=sg in - if a=0 then - let (ind,_)=get_constructor uf c in - try - let th2,hc2=IndMap.find ind rep.inductives in - raise (Discriminable (pac.term_head,c,th2,hc2,uf)) - with Not_found -> - rep.inductives<- - IndMap.add ind (pac.term_head,c) rep.inductives in - PacMap.iter add_pac pacs; - !pending,!combine +let append_pac t p = + {p with arity=pred p.arity;args=t::p.args} + +let tail_pac p= + {p with arity=succ p.arity;args=List.tl p.args} + +let add_pac rep pac t = + if not (PacMap.mem pac rep.constructors) then + rep.constructors<-PacMap.add pac t rep.constructors + +let term uf i=uf.map.(i).term + +let subterms uf i= + match uf.map.(i).vertex with + Node(j,k) -> (j,k) + | _ -> anomaly "subterms: not a node" - let term uf i=(Hashtbl.find uf.map i).term - - let subterms uf i= - match (Hashtbl.find uf.map i).vertex with - Node(j,k) -> (j,k) - | _ -> anomaly "subterms: not a node" - - let signature uf i= - let j,k=subterms uf i in (find uf j,find uf k) - - let nodes uf= (* cherche les noeuds binaires *) - Hashtbl.fold - (fun i node l-> - match node.vertex with - Node (_,_)->i::l - | _ ->l) uf.map [] - - let next uf= - let n=uf.size in uf.size<-n+1; n +let signature uf i= + let j,k=subterms uf i in (find uf j,find uf k) + +let next uf= + let size=uf.size in + let nsize= succ size in + if nsize=uf.max_size then + let newmax=uf.max_size * 3 / 2 + 1 in + let newmap=Array.create newmax dummy_node in + begin + uf.max_size<-newmax; + Array.blit uf.map 0 newmap 0 size; + uf.map<-newmap + end + else (); + uf.size<-nsize; + size - let new_representative pm im= - {nfathers=0; - fathers=[]; - constructors=pm; - inductives=im} - - let rec add uf t= +let new_representative ()= + {nfathers=0; + lfathers=Intset.empty; + fathers=Intset.empty; + inductive_status=Unknown; + constructors=PacMap.empty} + +let rec add_term state t= + let uf=state.uf in try Hashtbl.find uf.syms t with Not_found -> let b=next uf in let new_node= match t with - Symb s -> - {clas=Rep (new_representative PacMap.empty IndMap.empty); - vertex=Leaf;term=t;node_constr=PacMap.empty} + Symb _ | Eps -> + {clas= Rep (new_representative ()); + cpath= -1; + vertex= Leaf; + term= t} | Appli (t1,t2) -> - let i1=add uf t1 and i2=add uf t2 in - add_father uf (find uf i1) b; - add_father uf (find uf i2) b; - {clas=Rep (new_representative PacMap.empty IndMap.empty); - vertex=Node(i1,i2);term=t;node_constr=PacMap.empty} - | Constructor (c,a,n) -> - let pacs= - PacMap.add (b,a) - {head_constr=b;arity=a;nhyps=n;args=[];term_head=b} - PacMap.empty in - let inds= - if a=0 then - let (ind,_)=c in - IndMap.add ind (b,b) IndMap.empty - else IndMap.empty in - {clas=Rep (new_representative pacs inds); - vertex=Leaf;term=t;node_constr=PacMap.empty} + let i1=add_term state t1 and i2=add_term state t2 in + add_lfather uf (find uf i1) b; + add_rfather uf (find uf i2) b; + state.terms<-Intset.add b state.terms; + {clas= Rep (new_representative ()); + cpath= -1; + vertex= Node(i1,i2); + term= t} + | Constructor cinfo -> + let pac = + {cnode= b; + arity= cinfo.ci_arity; + args=[]} in + Queue.add (b,pac) state.marks; + {clas=Rep (new_representative ()); + cpath= -1; + vertex=Leaf; + term=t} in - Hashtbl.add uf.map b new_node; + uf.map.(b)<-new_node; Hashtbl.add uf.syms t b; b - let link uf i j eq= (* links i -> j *) - let node=Hashtbl.find uf.map i in - Hashtbl.replace uf.map i {node with clas=Eqto (j,eq)} - - let union uf i1 i2 eq= - let r1= get_representative uf i1 - and r2= get_representative uf i2 in - link uf i1 i2 eq; - r2.nfathers<-r1.nfathers+r2.nfathers; - r2.fathers<-r1.fathers@r2.fathers; - add_pacs uf i2 r1.constructors +let add_equality state id s t= + let i = add_term state s in + let j = add_term state t in + Queue.add {lhs=i;rhs=j;rule=Axiom(id,false)} state.combine; + Hashtbl.add state.uf.axioms id (s,t) + +let add_disequality state from s t = + let i = add_term state s in + let j = add_term state t in + state.diseq<-{lhs=i;rhs=j;rule=from}::state.diseq + +let link uf i j eq = (* links i -> j *) + let node=uf.map.(i) in + node.clas<-Eqto (j,eq); + node.cpath<-j - let rec down_path uf i l= - match (Hashtbl.find uf.map i).clas with - Eqto(j,t)->down_path uf j (((i,j),t)::l) - | Rep _ ->l - - let rec min_path=function - ([],l2)->([],l2) - | (l1,[])->(l1,[]) - | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2) - | cpl -> cpl +let rec down_path uf i l= + match uf.map.(i).clas with + Eqto(j,t)->down_path uf j (((i,j),t)::l) + | Rep _ ->l - let join_path uf i j= - assert (find uf i=find uf j); - min_path (down_path uf i [],down_path uf j []) +let rec min_path=function + ([],l2)->([],l2) + | (l1,[])->(l1,[]) + | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2) + | cpl -> cpl -end - -let rec combine_rec uf=function - []->[] - | t::pending-> - let combine=combine_rec uf pending in - let s=UF.signature uf t in - let u=snd (UF.subterms uf t) in - let f (c,a) pac pacs= - if a=0 then pacs else - let sg=(c,a-1) in - UF.add_node_pac uf t sg pac.term_head; - PacMap.add sg {pac with args=u::pac.args;term_head=t} pacs - in - let pacs=PacMap.fold f (UF.pac_map uf (fst s)) PacMap.empty in - let i=UF.find uf t in - let (p,c)=UF.add_pacs uf i pacs in - let combine2=(combine_rec uf p)@c@combine in - try {lhs=t;rhs=ST.query s uf.UF.sigtable;rule=Congruence}::combine2 with - Not_found-> - ST.enter t s uf.UF.sigtable;combine2 - -let rec process_rec uf=function - []->[] - | eq::combine-> - let pending=process_rec uf combine in - let i=UF.find uf eq.lhs - and j=UF.find uf eq.rhs in - if i=j then - pending +let join_path uf i j= + assert (find uf i=find uf j); + min_path (down_path uf i [],down_path uf j []) + +let union state i1 i2 eq= + debug msgnl (str "Linking " ++ int i1 ++ str " and " ++ int i2 ++ str "."); + let r1= get_representative state.uf i1 + and r2= get_representative state.uf i2 in + link state.uf i1 i2 eq; + let f= Intset.union r1.fathers r2.fathers in + r2.nfathers<-Intset.cardinal f; + r2.fathers<-f; + r2.lfathers<-Intset.union r1.lfathers r2.lfathers; + ST.delete_set state.sigtable r1.fathers; + state.terms<-Intset.union state.terms r1.fathers; + PacMap.iter (fun pac b -> Queue.add (b,pac) state.marks) r1.constructors; + match r1.inductive_status,r2.inductive_status with + Unknown,_ -> () + | Partial pac,Unknown -> + r2.inductive_status<-Partial pac; + state.pa_classes<-Intset.remove i1 state.pa_classes; + state.pa_classes<-Intset.add i2 state.pa_classes + | Partial _ ,(Partial _ |Partial_applied) -> + state.pa_classes<-Intset.remove i1 state.pa_classes + | Partial_applied,Unknown -> + r2.inductive_status<-Partial_applied + | Partial_applied,Partial _ -> + state.pa_classes<-Intset.remove i2 state.pa_classes; + r2.inductive_status<-Partial_applied + | Total cpl,Unknown -> r2.inductive_status<-Total cpl; + | Total cpl,Total _ -> Queue.add cpl state.marks + | _,_ -> () + +let merge eq state = (* merge and no-merge *) + debug msgnl + (str "Merging " ++ int eq.lhs ++ str " and " ++ int eq.rhs ++ str "."); + let uf=state.uf in + let i=find uf eq.lhs + and j=find uf eq.rhs in + if i<>j then + if (size uf i)<(size uf j) then + union state i j eq else - if (UF.size uf i)<(UF.size uf j) then - let l=UF.fathers uf i in - let (p,c)=UF.union uf i j eq in - let _ =ST.delete_list l uf.UF.sigtable in - let inj_pending=process_rec uf c in - inj_pending@p@l@pending + union state j i (swap eq) + +let update t state = (* update 1 and 2 *) + debug msgnl + (str "Updating term " ++ int t ++ str "."); + let (i,j) as sign = signature state.uf t in + let (u,v) = subterms state.uf t in + let rep = get_representative state.uf i in + begin + match rep.inductive_status with + Partial _ -> + rep.inductive_status <- Partial_applied; + state.pa_classes <- Intset.remove i state.pa_classes + | _ -> () + end; + PacMap.iter + (fun pac _ -> Queue.add (t,append_pac v pac) state.marks) + rep.constructors; + try + let s = ST.query sign state.sigtable in + Queue.add {lhs=t;rhs=s;rule=Congruence} state.combine + with + Not_found -> ST.enter t sign state.sigtable + +let process_mark t pac state = + debug msgnl + (str "Processing mark for term " ++ int t ++ str "."); + let i=find state.uf t in + let rep=get_representative state.uf i in + match rep.inductive_status with + Total (s,opac) -> + if pac.cnode <> opac.cnode then (* Conflict *) + raise (Discriminable (s,opac,t,pac)) + else (* Match *) + let cinfo = get_constructor_info state.uf pac.cnode in + let rec f n oargs args= + if n > 0 then + match (oargs,args) with + s1::q1,s2::q2-> + Queue.add + {lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)} + state.combine; + f (n-1) q1 q2 + | _-> anomaly + "add_pacs : weird error in injection subterms merge" + in f cinfo.ci_nhyps opac.args pac.args + | Partial_applied | Partial _ -> + add_pac rep pac t; + state.terms<-Intset.union rep.lfathers state.terms + | Unknown -> + if pac.arity = 0 then + rep.inductive_status <- Total (t,pac) + else + begin + add_pac rep pac t; + state.terms<-Intset.union rep.lfathers state.terms; + rep.inductive_status <- Partial pac; + state.pa_classes<- Intset.add i state.pa_classes + end + +type explanation = + Discrimination of (int*pa_constructor*int*pa_constructor) + | Contradiction of disequality + | Incomplete + +let check_disequalities state = + let uf=state.uf in + let rec check_aux = function + dis::q -> + debug msg + (str "Checking if " ++ int dis.lhs ++ str " = " ++ + int dis.rhs ++ str " ... "); + if find uf dis.lhs=find uf dis.rhs then + begin debug msgnl (str "Yes");Some dis end else - let l=UF.fathers uf j in - let (p,c)=UF.union uf j i (swap eq) in - let _ =ST.delete_list l uf.UF.sigtable in - let inj_pending=process_rec uf c in - inj_pending@p@l@pending - -let rec cc_rec uf=function - []->() - | pending-> - let combine=combine_rec uf pending in - let pending0=process_rec uf combine in - cc_rec uf pending0 - -let cc uf=cc_rec uf (UF.nodes uf) - -let rec make_uf=function - []->UF.empty () - | (ax,(t1,t2))::q-> - let uf=make_uf q in - let i1=UF.add uf t1 in - let i2=UF.add uf t2 in - let j1=UF.find uf i1 and j2=UF.find uf i2 in - if j1=j2 then uf else - let (_,inj_combine)= - UF.union uf j1 j2 {lhs=i1;rhs=i2;rule=Axiom ax} in - let _ = process_rec uf inj_combine in uf - -let add_one_diseq uf (t1,t2)=(UF.add uf t1,UF.add uf t2) - -let add_disaxioms uf disaxioms= - let f (id,cpl)=(id,add_one_diseq uf cpl) in - List.map f disaxioms - -let check_equal uf (i1,i2) = UF.find uf i1 = UF.find uf i2 - -let find_contradiction uf diseq = - List.find (fun (id,cpl) -> check_equal uf cpl) diseq - + begin debug msgnl (str "No");check_aux q end + | [] -> None + in + check_aux state.diseq + +let one_step state = + try + let eq = Queue.take state.combine in + merge eq state + with Queue.Empty -> + try + let (t,m) = Queue.take state.marks in + process_mark t m state + with Queue.Empty -> + let t = Intset.choose state.terms in + state.terms<-Intset.remove t state.terms; + update t state + +let complete_one_class state i= + match (get_representative state.uf i).inductive_status with + Partial pac -> + let rec app t n = + if n<=0 then t else + app (Appli(t,Eps)) (n-1) in + state.uf.epsilons <- pac :: state.uf.epsilons; + ignore (add_term state (app (term state.uf i) pac.arity)) + | _ -> anomaly "wrong incomplete class" + +let complete state = + Intset.iter (complete_one_class state) state.pa_classes + +let rec execute first_run state = + debug msgnl (str "Executing ... "); + try + while true do + one_step state + done; + anomaly "keep out of here" + with + Discriminable(s,spac,t,tpac) -> + Some + begin + if first_run then + Discrimination (s,spac,t,tpac) + else + Incomplete + end + | Not_found -> + match check_disequalities state with + None -> + if not(Intset.is_empty state.pa_classes) then + begin + debug msgnl + (str "First run was incomplete, completing ... "); + complete state; + execute false state + end + else None + | Some dis -> Some + begin + if first_run then + Contradiction dis + else + Incomplete + end diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli index 47cdb3ea..74132811 100644 --- a/contrib/cc/ccalgo.mli +++ b/contrib/cc/ccalgo.mli @@ -6,15 +6,109 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccalgo.mli,v 1.6.2.1 2004/07/16 19:29:58 herbelin Exp $ *) +(* $Id: ccalgo.mli 7298 2005-08-17 12:56:38Z corbinea $ *) -type pa_constructor - (*{head: int; arity: int; args: (int * int) list}*) +open Util +open Term +open Names -module PacMap:Map.S with type key=int * int +type cinfo = + {ci_constr: constructor; (* inductive type *) + ci_arity: int; (* # args *) + ci_nhyps: int} (* # projectable args *) + +type term = + Symb of constr + | Eps + | Appli of term*term + | Constructor of cinfo (* constructor arity + nhyps *) + +type pa_constructor = + { cnode : int; + arity : int; + args : int list} + +module PacMap : Map.S with type key = pa_constructor + +type forest + +type state + +type rule= + Congruence + | Axiom of identifier * bool + | Injection of int * pa_constructor * int * pa_constructor * int + +type from= + Goal + | Hyp of identifier + | HeqG of identifier + | HeqnH of identifier * identifier + +type 'a eq = {lhs:int;rhs:int;rule:'a} + +type equality = rule eq + +type disequality = from eq + +type explanation = + Discrimination of (int*pa_constructor*int*pa_constructor) + | Contradiction of disequality + | Incomplete + +val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit + +val forest : state -> forest + +val axioms : forest -> (identifier, term * term) Hashtbl.t + +val epsilons : forest -> pa_constructor list + +val empty : unit -> state + +val add_term : state -> term -> int + +val add_equality : state -> identifier -> term -> term -> unit + +val add_disequality : state -> from -> term -> term -> unit + +val tail_pac : pa_constructor -> pa_constructor + +val find : forest -> int -> int + +val find_pac : forest -> int -> pa_constructor -> int + +val term : forest -> int -> term + +val get_constructor_info : forest -> int -> cinfo + +val subterms : forest -> int -> int * int + +val join_path : forest -> int -> int -> + ((int * int) * equality) list * ((int * int) * equality) list + +val execute : bool -> state -> explanation option + + + + + + + + + + + + + +(*type pa_constructor + + +module PacMap:Map.S with type key=pa_constructor type term = Symb of Term.constr + | Eps | Appli of term * term | Constructor of Names.constructor*int*int @@ -79,6 +173,6 @@ val check_equal : UF.t -> int * int -> bool val find_contradiction : UF.t -> (Names.identifier * (int * int)) list -> (Names.identifier * (int * int)) - +*) diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml index fa525e65..1200dc2e 100644 --- a/contrib/cc/ccproof.ml +++ b/contrib/cc/ccproof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.ml,v 1.8.2.1 2004/07/16 19:29:58 herbelin Exp $ *) +(* $Id: ccproof.ml 7298 2005-08-17 12:56:38Z corbinea $ *) (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) @@ -51,8 +51,8 @@ let pcongr=function let build_proof uf= let rec equal_proof i j= - if i=j then Refl (UF.term uf i) else - let (li,lj)=UF.join_path uf i j in + if i=j then Refl (term uf i) else + let (li,lj)=join_path uf i j in ptrans (path_proof i li,psym (path_proof j lj)) and edge_proof ((i,j),eq)= @@ -60,45 +60,44 @@ let build_proof uf= let pj=psym (equal_proof j eq.rhs) in let pij= match eq.rule with - Axiom s->Ax s + Axiom (s,reversed)->if reversed then SymAx s else Ax s | Congruence ->congr_proof eq.lhs eq.rhs - | Injection (ti,tj,c,a) -> - let p=equal_proof ti tj in - let p1=constr_proof ti ti c 0 - and p2=constr_proof tj tj c 0 in - match UF.term uf c with - Constructor (cstr,nargs,nhyps) -> - Inject(ptrans(psym p1,ptrans(p,p2)),cstr,nhyps,a) - | _ -> anomaly "injection on non-constructor terms" + | Injection (ti,ipac,tj,jpac,k) -> + let p=ind_proof ti ipac tj jpac in + let cinfo= get_constructor_info uf ipac.cnode in + Inject(p,cinfo.ci_constr,cinfo.ci_nhyps,k) in ptrans(ptrans (pi,pij),pj) - and constr_proof i j c n= - try - let nj=UF.mem_node_pac uf j (c,n) in - let (ni,arg)=UF.subterms uf j in - let p=constr_proof ni nj c (n+1) in - let targ=UF.term uf arg in - ptrans (equal_proof i j, pcongr (p,Refl targ)) - with Not_found->equal_proof i j + and constr_proof i t ipac= + if ipac.args=[] then + equal_proof i t + else + let npac=tail_pac ipac in + let (j,arg)=subterms uf t in + let targ=term uf arg in + let rj=find uf j in + let u=find_pac uf rj npac in + let p=constr_proof j u npac in + ptrans (equal_proof i t, pcongr (p,Refl targ)) and path_proof i=function - [] -> Refl (UF.term uf i) + [] -> Refl (term uf i) | x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x) and congr_proof i j= - let (i1,i2) = UF.subterms uf i - and (j1,j2) = UF.subterms uf j in + let (i1,i2) = subterms uf i + and (j1,j2) = subterms uf j in pcongr (equal_proof i1 j1, equal_proof i2 j2) - and discr_proof i ci j cj= + and ind_proof i ipac j jpac= let p=equal_proof i j - and p1=constr_proof i i ci 0 - and p2=constr_proof j j cj 0 in + and p1=constr_proof i i ipac + and p2=constr_proof j j jpac in ptrans(psym p1,ptrans(p,p2)) in function - `Prove_goal (i,j) | `Refute_hyp (i,j) -> equal_proof i j - | `Discriminate (i,ci,j,cj)-> discr_proof i ci j cj + `Prove (i,j) -> equal_proof i j + | `Discr (i,ci,j,cj)-> ind_proof i ci j cj let rec nth_arg t n= match t with @@ -110,8 +109,8 @@ let rec nth_arg t n= let rec type_proof axioms p= match p with - Ax s->List.assoc s axioms - | SymAx s-> let (t1,t2)=List.assoc s axioms in (t2,t1) + Ax s->Hashtbl.find axioms s + | SymAx s-> let (t1,t2)=Hashtbl.find axioms s in (t2,t1) | Refl t-> t,t | Trans (p1,p2)-> let (s1,t1)=type_proof axioms p1 @@ -125,33 +124,3 @@ let rec type_proof axioms p= let (ti,tj)=type_proof axioms p in nth_arg ti (n-a),nth_arg tj (n-a) -let by_contradiction uf diseq axioms disaxioms= - try - let id,cpl=find_contradiction uf diseq in - let prf=build_proof uf (`Refute_hyp cpl) in - if List.assoc id disaxioms=type_proof axioms prf then - `Refute_hyp (id,prf) - else - anomaly "wrong proof generated" - with Not_found -> - errorlabstrm "Congruence" (Pp.str "I couldn't solve goal") - -let cc_proof axioms disaxioms glo= - try - let uf=make_uf axioms in - let diseq=add_disaxioms uf disaxioms in - match glo with - Some cpl -> - let goal=add_one_diseq uf cpl in cc uf; - if check_equal uf goal then - let prf=build_proof uf (`Prove_goal goal) in - if cpl=type_proof axioms prf then - `Prove_goal prf - else anomaly "wrong proof generated" - else by_contradiction uf diseq axioms disaxioms - | None -> cc uf; by_contradiction uf diseq axioms disaxioms - with UF.Discriminable (i,ci,j,cj,uf) -> - let prf=build_proof uf (`Discriminate (i,ci,j,cj)) in - `Discriminate (UF.get_constructor uf ci,prf) - - diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli index 887ed070..18c745bf 100644 --- a/contrib/cc/ccproof.mli +++ b/contrib/cc/ccproof.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.mli,v 1.6.2.1 2004/07/16 19:29:59 herbelin Exp $ *) +(* $Id: ccproof.mli 7298 2005-08-17 12:56:38Z corbinea $ *) open Ccalgo open Names @@ -19,27 +19,12 @@ type proof = | Congr of proof * proof | Inject of proof * constructor * int * int -val pcongr : proof * proof -> proof -val ptrans : proof * proof -> proof -val psym : proof -> proof -val pcongr : proof * proof -> proof - val build_proof : - UF.t -> - [ `Discriminate of int * int * int * int - | `Prove_goal of int * int - | `Refute_hyp of int * int ] - -> proof + forest -> + [ `Discr of int * pa_constructor * int * pa_constructor + | `Prove of int * int ] -> proof val type_proof : - (identifier * (term * term)) list -> proof -> term * term - -val cc_proof : - (identifier * (term * term)) list -> - (identifier * (term * term)) list -> - (term * term) option -> - [ `Discriminate of constructor * proof - | `Prove_goal of proof - | `Refute_hyp of identifier * proof ] + (identifier, (term * term)) Hashtbl.t -> proof -> term * term diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml new file mode 100644 index 00000000..4a719f38 --- /dev/null +++ b/contrib/cc/cctac.ml @@ -0,0 +1,336 @@ +(************************************************************************) +(* 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: cctac.ml 7909 2006-01-21 11:09:18Z herbelin $ *) + +(* This file is the interface between the c-c algorithm and Coq *) + +open Evd +open Proof_type +open Names +open Libnames +open Nameops +open Inductiveops +open Declarations +open Term +open Termops +open Tacmach +open Tactics +open Tacticals +open Ccalgo +open Tacinterp +open Ccproof +open Pp +open Util +open Format + +let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) + +let _f_equal = constant ["Init";"Logic"] "f_equal" + +let _eq_rect = constant ["Init";"Logic"] "eq_rect" + +let _eq = constant ["Init";"Logic"] "eq" + +let _False = constant ["Init";"Logic"] "False" + +(* decompose member of equality in an applicative format *) + +let whd env= + let infos=Closure.create_clos_infos Closure.betaiotazeta env in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let whd_delta env= + let infos=Closure.create_clos_infos Closure.betadeltaiota env in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let rec decompose_term env t= + match kind_of_term (whd env t) with + App (f,args)-> + let tf=decompose_term env f in + let targs=Array.map (decompose_term env) args in + Array.fold_left (fun s t->Appli (s,t)) tf targs + | Construct c-> + let (oib,_)=Global.lookup_inductive (fst c) in + let nargs=mis_constructor_nargs_env env c in + Constructor {ci_constr=c; + ci_arity=nargs; + ci_nhyps=nargs-oib.mind_nparams} + | _ ->(Symb t) + +(* decompose equality in members and type *) + +let atom_of_constr env term = + let wh = (whd_delta env term) in + let kot = kind_of_term wh in + match kot with + App (f,args)-> + if eq_constr f (Lazy.force _eq) && (Array.length args)=3 + then `Eq (args.(0), + decompose_term env args.(1), + decompose_term env args.(2)) + else `Other (decompose_term env term) + | _ -> `Other (decompose_term env term) + +let rec litteral_of_constr env term= + match kind_of_term (whd_delta env term) with + Prod (_,atom,ff) -> + if eq_constr ff (Lazy.force _False) then + match (atom_of_constr env atom) with + `Eq(t,a,b) -> `Neq(t,a,b) + | `Other(p) -> `Nother(p) + else + `Other (decompose_term env term) + | _ -> atom_of_constr env term + +(* rebuild a term from applicative format *) + +let rec make_term = function + Symb s->s + | Eps -> anomaly "epsilon constant has no value" + | Constructor cinfo -> mkConstruct cinfo.ci_constr + | Appli (s1,s2)-> + make_app [(make_term s2)] s1 +and make_app l=function + Appli (s1,s2)->make_app ((make_term s2)::l) s1 + | other -> applistc (make_term other) l + +(* store all equalities from the context *) + +let rec make_prb gls additionnal_terms = + let env=pf_env gls in + let state = empty () in + let pos_hyps = ref [] in + let neg_hyps =ref [] in + List.iter + (fun c -> + let t = decompose_term env c in + ignore (add_term state t)) additionnal_terms; + List.iter + (fun (id,_,e) -> + begin + match litteral_of_constr env e with + `Eq (t,a,b) -> add_equality state id a b + | `Neq (t,a,b) -> add_disequality state (Hyp id) a b + | `Other ph -> + List.iter + (fun (idn,nh) -> + add_disequality state (HeqnH (id,idn)) ph nh) + !neg_hyps; + pos_hyps:=(id,ph):: !pos_hyps + | `Nother nh -> + List.iter + (fun (idp,ph) -> + add_disequality state (HeqnH (idp,id)) ph nh) + !pos_hyps; + neg_hyps:=(id,nh):: !neg_hyps + end) (Environ.named_context_of_val gls.it.evar_hyps); + begin + match atom_of_constr env gls.it.evar_concl with + `Eq (t,a,b) -> add_disequality state Goal a b + | `Other g -> + List.iter + (fun (idp,ph) -> + add_disequality state (HeqG idp) ph g) !pos_hyps + end; + state + +(* indhyps builds the array of arrays of constructor hyps for (ind largs) *) + +let build_projection intype outtype (cstr:constructor) special default gls= + let env=pf_env gls in + let (h,argv) = + try destApp intype with + Invalid_argument _ -> (intype,[||]) in + let ind=destInd h in + let types=Inductiveops.arities_of_constructors env ind in + let lp=Array.length types in + let ci=(snd cstr)-1 in + let branch i= + let ti=Term.prod_appvect types.(i) argv in + let rc=fst (Sign.decompose_prod_assum ti) in + let head= + if i=ci then special else default in + Sign.it_mkLambda_or_LetIn head rc in + let branches=Array.init lp branch in + let casee=mkRel 1 in + let pred=mkLambda(Anonymous,intype,outtype) in + let case_info=make_default_case_info (pf_env gls) RegularStyle ind in + let body= mkCase(case_info, pred, casee, branches) in + let id=pf_get_new_id (id_of_string "t") gls in + mkLambda(Name id,intype,body) + +(* generate an adhoc tactic following the proof tree *) + +let rec proof_tac axioms=function + Ax id->exact_check (mkVar id) + | SymAx id->tclTHEN symmetry (exact_check (mkVar id)) + | Refl t->reflexivity + | Trans (p1,p2)->let t=(make_term (snd (type_proof axioms p1))) in + (tclTHENS (transitivity t) + [(proof_tac axioms p1);(proof_tac axioms p2)]) + | Congr (p1,p2)-> + fun gls-> + let (f1,f2)=(type_proof axioms p1) + and (x1,x2)=(type_proof axioms p2) in + let tf1=make_term f1 and tx1=make_term x1 + and tf2=make_term f2 and tx2=make_term x2 in + let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1 + and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in + let id=pf_get_new_id (id_of_string "f") gls in + let appx1=mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in + let lemma1= + mkApp(Lazy.force _f_equal,[|typf;typfx;appx1;tf1;tf2|]) + and lemma2= + mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2|]) in + (tclTHENS (transitivity (mkApp(tf2,[|tx1|]))) + [tclTHEN (apply lemma1) (proof_tac axioms p1); + tclFIRST + [tclTHEN (apply lemma2) (proof_tac axioms p2); + reflexivity; + fun gls -> + errorlabstrm "Congruence" + (Pp.str + "I don't know how to handle dependent equality")]] + gls) + | Inject (prf,cstr,nargs,argind) as gprf-> + (fun gls -> + let ti,tj=type_proof axioms prf in + let ai,aj=type_proof axioms gprf in + let cti=make_term ti in + let ctj=make_term tj in + let cai=make_term ai in + let intype=pf_type_of gls cti in + let outtype=pf_type_of gls cai in + let special=mkRel (1+nargs-argind) in + let default=make_term ai in + let proj=build_projection intype outtype cstr special default gls in + let injt= + mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in + tclTHEN (apply injt) (proof_tac axioms prf) gls) + +let refute_tac axioms id t1 t2 p gls = + let tt1=make_term t1 and tt2=make_term t2 in + let intype=pf_type_of gls tt1 in + let neweq= + mkApp(Lazy.force _eq, + [|intype;tt1;tt2|]) in + let hid=pf_get_new_id (id_of_string "Heq") gls in + let false_t=mkApp (mkVar id,[|mkVar hid|]) in + tclTHENS (true_cut (Name hid) neweq) + [proof_tac axioms p; simplest_elim false_t] gls + +let convert_to_goal_tac axioms id t1 t2 p gls = + let tt1=make_term t1 and tt2=make_term t2 in + let sort=pf_type_of gls tt2 in + let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in + let e=pf_get_new_id (id_of_string "e") gls in + let x=pf_get_new_id (id_of_string "X") gls in + let identity=mkLambda (Name x,sort,mkRel 1) in + let endt=mkApp (Lazy.force _eq_rect, + [|sort;tt1;identity;mkVar id;tt2;mkVar e|]) in + tclTHENS (true_cut (Name e) neweq) + [proof_tac axioms p;exact_check endt] gls + +let convert_to_hyp_tac axioms id1 t1 id2 t2 p gls = + let tt2=make_term t2 in + let h=pf_get_new_id (id_of_string "H") gls in + let false_t=mkApp (mkVar id2,[|mkVar h|]) in + tclTHENS (true_cut (Name h) tt2) + [convert_to_goal_tac axioms id1 t1 t2 p; + simplest_elim false_t] gls + +let discriminate_tac axioms cstr p gls = + let t1,t2=type_proof axioms p in + let tt1=make_term t1 and tt2=make_term t2 in + let intype=pf_type_of gls tt1 in + let concl=pf_concl gls in + let outsort=mkType (new_univ ()) in + let xid=pf_get_new_id (id_of_string "X") gls in + let tid=pf_get_new_id (id_of_string "t") gls in + let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in + let trivial=pf_type_of gls identity in + let outtype=mkType (new_univ ()) in + let pred=mkLambda(Name xid,outtype,mkRel 1) in + let hid=pf_get_new_id (id_of_string "Heq") gls in + let proj=build_projection intype outtype cstr trivial concl gls in + let injt=mkApp (Lazy.force _f_equal, + [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in + let endt=mkApp (Lazy.force _eq_rect, + [|outtype;trivial;pred;identity;concl;injt|]) in + let neweq=mkApp(Lazy.force _eq,[|intype;tt1;tt2|]) in + tclTHENS (true_cut (Name hid) neweq) + [proof_tac axioms p;exact_check endt] gls + +(* wrap everything *) + +let build_term_to_complete uf meta pac = + let cinfo = get_constructor_info uf pac.cnode in + let real_args = List.map (fun i -> make_term (term uf i)) pac.args in + let dummy_args = List.rev (list_tabulate meta pac.arity) in + let all_args = List.rev_append real_args dummy_args in + applistc (mkConstruct cinfo.ci_constr) all_args + +let cc_tactic additionnal_terms gls= + Coqlib.check_required_library ["Coq";"Init";"Logic"]; + let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in + let state = make_prb gls additionnal_terms in + let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in + let sol = execute true state in + let _ = debug Pp.msgnl (Pp.str "Computation completed.") in + let uf=forest state in + match sol with + None -> tclFAIL 0 (str "congruence failed") gls + | Some reason -> + debug Pp.msgnl (Pp.str "Goal solved, generating proof ..."); + match reason with + Discrimination (i,ipac,j,jpac) -> + let p=build_proof uf (`Discr (i,ipac,j,jpac)) in + let cstr=(get_constructor_info uf ipac.cnode).ci_constr in + discriminate_tac (axioms uf) cstr p gls + | Incomplete -> + let metacnt = ref 0 in + let newmeta _ = incr metacnt; mkMeta !metacnt in + let terms_to_complete = + List.map + (build_term_to_complete uf newmeta) + (epsilons uf) in + Pp.msgnl + (Pp.str "Goal is solvable by congruence but \ + some arguments are missing."); + Pp.msgnl + (Pp.str " Try " ++ + hov 8 + begin + str "\"congruence with (" ++ + prlist_with_sep + (fun () -> str ")" ++ pr_spc () ++ str "(") + (print_constr_env (pf_env gls)) + terms_to_complete ++ + str ")\"," + end); + Pp.msgnl + (Pp.str " replacing metavariables by arbitrary terms."); + tclFAIL 0 (str "Incomplete") gls + | Contradiction dis -> + let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in + let ta=term uf dis.lhs and tb=term uf dis.rhs in + let axioms = axioms uf in + match dis.rule with + Goal -> proof_tac axioms p gls + | Hyp id -> refute_tac axioms id ta tb p gls + | HeqG id -> + convert_to_goal_tac axioms id ta tb p gls + | HeqnH (ida,idb) -> + convert_to_hyp_tac axioms ida ta idb tb p gls + + +let cc_fail gls = + errorlabstrm "Congruence" (Pp.str "congruence failed.") diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4 deleted file mode 100644 index 49fe46fe..00000000 --- a/contrib/cc/cctac.ml4 +++ /dev/null @@ -1,247 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -(* $Id: cctac.ml4,v 1.13.2.1 2004/07/16 19:29:59 herbelin Exp $ *) - -(* This file is the interface between the c-c algorithm and Coq *) - -open Evd -open Proof_type -open Names -open Libnames -open Nameops -open Inductiveops -open Declarations -open Term -open Termops -open Tacmach -open Tactics -open Tacticals -open Ccalgo -open Tacinterp -open Ccproof -open Pp -open Util -open Format - -exception Not_an_eq - -let fail()=raise Not_an_eq - -let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) - -let f_equal_theo = constant ["Init";"Logic"] "f_equal" - -let eq_rect_theo = constant ["Init";"Logic"] "eq_rect" - -(* decompose member of equality in an applicative format *) - -let rec decompose_term env t= - match kind_of_term t with - App (f,args)-> - let tf=decompose_term env f in - let targs=Array.map (decompose_term env) args in - Array.fold_left (fun s t->Appli (s,t)) tf targs - | Construct c-> - let (_,oib)=Global.lookup_inductive (fst c) in - let nargs=mis_constructor_nargs_env env c in - Constructor (c,nargs,nargs-oib.mind_nparams) - | _ ->(Symb t) - -(* decompose equality in members and type *) - -let rec eq_type_of_term term= - match kind_of_term term with - App (f,args)-> - (try - let ref = reference_of_constr f in - if ref=Coqlib.glob_eq && (Array.length args)=3 - then (true,args.(0),args.(1),args.(2)) - else - if ref=(Lazy.force Coqlib.coq_not_ref) && - (Array.length args)=1 then - let (pol,t,a,b)=eq_type_of_term args.(0) in - if pol then (false,t,a,b) else fail () - else fail () - with Not_found -> fail ()) - | Prod (_,eq,ff) -> - (try - let ref = reference_of_constr ff in - if ref=(Lazy.force Coqlib.coq_False_ref) then - let (pol,t,a,b)=eq_type_of_term eq in - if pol then (false,t,a,b) else fail () - else fail () - with Not_found -> fail ()) - | _ -> fail () - -(* read an equality *) - -let read_eq env term= - let (pol,_,t1,t2)=eq_type_of_term term in - (pol,(decompose_term env t1,decompose_term env t2)) - -(* rebuild a term from applicative format *) - -let rec make_term=function - Symb s->s - | Constructor(c,_,_)->mkConstruct c - | Appli (s1,s2)-> - make_app [(make_term s2)] s1 -and make_app l=function - Symb s->applistc s l - | Constructor(c,_,_)->applistc (mkConstruct c) l - | Appli (s1,s2)->make_app ((make_term s2)::l) s1 - -(* store all equalities from the context *) - -let rec read_hyps env=function - []->[],[] - | (id,_,e)::hyps->let eq,diseq=read_hyps env hyps in - try let pol,cpl=read_eq env e in - if pol then - ((id,cpl)::eq),diseq - else - eq,((id,cpl)::diseq) - with Not_an_eq -> eq,diseq - -(* build a problem ( i.e. read the goal as an equality ) *) - -let make_prb gl= - let env=pf_env gl in - let eq,diseq=read_hyps env gl.it.evar_hyps in - try - let pol,cpl=read_eq env gl.it.evar_concl in - if pol then (eq,diseq,Some cpl) else assert false with - Not_an_eq -> (eq,diseq,None) - -(* indhyps builds the array of arrays of constructor hyps for (ind largs) *) - -let build_projection intype outtype (cstr:constructor) special default gls= - let env=pf_env gls in - let (h,argv) = - try destApplication intype with - Invalid_argument _ -> (intype,[||]) in - let ind=destInd h in - let types=Inductive.arities_of_constructors env ind in - let lp=Array.length types in - let ci=(snd cstr)-1 in - let branch i= - let ti=Term.prod_appvect types.(i) argv in - let rc=fst (Sign.decompose_prod_assum ti) in - let head= - if i=ci then special else default in - Sign.it_mkLambda_or_LetIn head rc in - let branches=Array.init lp branch in - let casee=mkRel 1 in - let pred=mkLambda(Anonymous,intype,outtype) in - let case_info=make_default_case_info (pf_env gls) RegularStyle ind in - let body= mkCase(case_info, pred, casee, branches) in - let id=pf_get_new_id (id_of_string "t") gls in - mkLambda(Name id,intype,body) - -(* generate an adhoc tactic following the proof tree *) - -let rec proof_tac axioms=function - Ax id->exact_check (mkVar id) - | SymAx id->tclTHEN symmetry (exact_check (mkVar id)) - | Refl t->reflexivity - | Trans (p1,p2)->let t=(make_term (snd (type_proof axioms p1))) in - (tclTHENS (transitivity t) - [(proof_tac axioms p1);(proof_tac axioms p2)]) - | Congr (p1,p2)-> - fun gls-> - let (f1,f2)=(type_proof axioms p1) - and (x1,x2)=(type_proof axioms p2) in - let tf1=make_term f1 and tx1=make_term x1 - and tf2=make_term f2 and tx2=make_term x2 in - let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1 - and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in - let id=pf_get_new_id (id_of_string "f") gls in - let appx1=mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1= - mkApp(Lazy.force f_equal_theo,[|typf;typfx;appx1;tf1;tf2|]) - and lemma2= - mkApp(Lazy.force f_equal_theo,[|typx;typfx;tf2;tx1;tx2|]) in - (tclTHENS (transitivity (mkApp(tf2,[|tx1|]))) - [tclTHEN (apply lemma1) (proof_tac axioms p1); - tclFIRST - [tclTHEN (apply lemma2) (proof_tac axioms p2); - reflexivity; - fun gls -> - errorlabstrm "Congruence" - (Pp.str - "I don't know how to handle dependent equality")]] - gls) - | Inject (prf,cstr,nargs,argind) as gprf-> - (fun gls -> - let ti,tj=type_proof axioms prf in - let ai,aj=type_proof axioms gprf in - let cti=make_term ti in - let ctj=make_term tj in - let cai=make_term ai in - let intype=pf_type_of gls cti in - let outtype=pf_type_of gls cai in - let special=mkRel (1+nargs-argind) in - let default=make_term ai in - let proj=build_projection intype outtype cstr special default gls in - let injt= - mkApp (Lazy.force f_equal_theo,[|intype;outtype;proj;cti;ctj|]) in - tclTHEN (apply injt) (proof_tac axioms prf) gls) - -let refute_tac axioms disaxioms id p gls = - let t1,t2=List.assoc id disaxioms in - let tt1=make_term t1 and tt2=make_term t2 in - let intype=pf_type_of gls tt1 in - let neweq= - mkApp(constr_of_reference Coqlib.glob_eq, - [|intype;tt1;tt2|]) in - let hid=pf_get_new_id (id_of_string "Heq") gls in - let false_t=mkApp (mkVar id,[|mkVar hid|]) in - tclTHENS (true_cut (Name hid) neweq) - [proof_tac axioms p; simplest_elim false_t] gls - -let discriminate_tac axioms cstr p gls = - let t1,t2=type_proof axioms p in - let tt1=make_term t1 and tt2=make_term t2 in - let intype=pf_type_of gls tt1 in - let concl=pf_concl gls in - let outsort=mkType (new_univ ()) in - let xid=pf_get_new_id (id_of_string "X") gls in - let tid=pf_get_new_id (id_of_string "t") gls in - let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in - let trivial=pf_type_of gls identity in - let outtype=mkType (new_univ ()) in - let pred=mkLambda(Name xid,outtype,mkRel 1) in - let hid=pf_get_new_id (id_of_string "Heq") gls in - let proj=build_projection intype outtype cstr trivial concl gls in - let injt=mkApp (Lazy.force f_equal_theo, - [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in - let endt=mkApp (Lazy.force eq_rect_theo, - [|outtype;trivial;pred;identity;concl;injt|]) in - let neweq=mkApp(constr_of_reference Coqlib.glob_eq,[|intype;tt1;tt2|]) in - tclTHENS (true_cut (Name hid) neweq) - [proof_tac axioms p;exact_check endt] gls - -(* wrap everything *) - -let cc_tactic gls= - Library.check_required_library ["Coq";"Init";"Logic"]; - let (axioms,disaxioms,glo)=make_prb gls in - match (cc_proof axioms disaxioms glo) with - `Prove_goal p -> proof_tac axioms p gls - | `Refute_hyp (id,p) -> refute_tac axioms disaxioms id p gls - | `Discriminate (cstr,p) -> discriminate_tac axioms cstr p gls - -(* Tactic registration *) - -TACTIC EXTEND CC - [ "Congruence" ] -> [ tclSOLVE [tclTHEN (tclREPEAT introf) cc_tactic] ] -END - diff --git a/contrib/cc/CCSolve.v b/contrib/cc/cctac.mli index fab6f775..6082beb6 100644 --- a/contrib/cc/CCSolve.v +++ b/contrib/cc/cctac.mli @@ -6,17 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: CCSolve.v,v 1.4.2.1 2004/07/16 19:29:58 herbelin Exp $ *) +(* $Id: cctac.mli 7298 2005-08-17 12:56:38Z corbinea $ *) -Ltac CCsolve := - repeat - match goal with - | H:?X1 |- ?X2 => - let Heq := fresh "Heq" in - (assert (Heq : X2 = X1); [ congruence | rewrite Heq; exact H ]) - | H:?X1,G:(?X2 -> ?X3) |- _ => - let Heq := fresh "Heq" in - (assert (Heq : X2 = X1); - [ congruence - | rewrite Heq in G; generalize (G H); clear G; intro G ]) - end. +open Term +open Proof_type + +val cc_tactic : constr list -> tactic + +val cc_fail : tactic diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4 new file mode 100644 index 00000000..0bdf7608 --- /dev/null +++ b/contrib/cc/g_congruence.ml4 @@ -0,0 +1,29 @@ +(************************************************************************) +(* 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_congruence.ml4 7734 2005-12-26 14:06:51Z herbelin $ *) + +open Cctac +open Tactics +open Tacticals + +(* Tactic registration *) + +TACTIC EXTEND cc + [ "congruence" ] -> [ tclORELSE + (tclTHEN (tclREPEAT introf) (cc_tactic [])) + cc_fail ] +END + +TACTIC EXTEND cc_with + [ "congruence" "with" ne_constr_list(l) ] -> [ tclORELSE + (tclTHEN (tclREPEAT introf) (cc_tactic l)) + cc_fail] +END |