diff options
Diffstat (limited to 'contrib/cc')
-rw-r--r-- | contrib/cc/README | 20 | ||||
-rw-r--r-- | contrib/cc/ccalgo.ml | 884 | ||||
-rw-r--r-- | contrib/cc/ccalgo.mli | 222 | ||||
-rw-r--r-- | contrib/cc/ccproof.ml | 153 | ||||
-rw-r--r-- | contrib/cc/ccproof.mli | 31 | ||||
-rw-r--r-- | contrib/cc/cctac.ml | 465 | ||||
-rw-r--r-- | contrib/cc/cctac.mli | 22 | ||||
-rw-r--r-- | contrib/cc/g_congruence.ml4 | 29 |
8 files changed, 0 insertions, 1826 deletions
diff --git a/contrib/cc/README b/contrib/cc/README deleted file mode 100644 index 073b140e..00000000 --- a/contrib/cc/README +++ /dev/null @@ -1,20 +0,0 @@ - -cctac: congruence-closure for coq - -author: Pierre Corbineau, - Stage de DEA au LSV, ENS Cachan - Thèse au LRI, Université Paris Sud XI - -Files : - -- ccalgo.ml : congruence closure algorithm -- ccproof.ml : proof generation code -- cctac.ml4 : the tactic itself -- CCSolve.v : a small Ltac tactic based on congruence - -Known Bugs : the congruence tactic can fail due to type dependencies. - -Related documents: - Peter J. Downey, Ravi Sethi, and Robert E. Tarjan. - Variations on the common subexpression problem. - JACM, 27(4):758-771, October 1980. diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml deleted file mode 100644 index e67797e4..00000000 --- a/contrib/cc/ccalgo.ml +++ /dev/null @@ -1,884 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: ccalgo.ml 10579 2008-02-21 13:54:00Z corbinea $ *) - -(* This file implements the basic congruence-closure algorithm by *) -(* Downey,Sethi and Tarjan. *) - -open Util -open Pp -open Goptions -open Names -open Term -open Tacmach -open Evd -open Proof_type - -let init_size=5 - -let cc_verbose=ref false - -let debug f x = - if !cc_verbose then f x - -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 *) - -module ST=struct - - (* l: sign -> term r: term -> sign *) - - type t = {toterm:(int*int,int) Hashtbl.t; - tosign:(int,int*int) Hashtbl.t} - - let empty ()= - {toterm=Hashtbl.create init_size; - tosign=Hashtbl.create init_size} - - let enter t sign st= - if Hashtbl.mem st.toterm sign then - anomaly "enter: signature already entered" - else - Hashtbl.replace st.toterm sign t; - Hashtbl.replace st.tosign t sign - - let query sign st=Hashtbl.find st.toterm sign - - let rev_query term st=Hashtbl.find st.tosign term - - 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_set st s = Intset.iter (delete st) s - -end - -type pa_constructor= - { cnode : int; - arity : int; - args : int list} - -type pa_fun= - {fsym:int; - fnargs:int} - -type pa_mark= - Fmark of pa_fun - | Cmark of pa_constructor - -module PacMap=Map.Make(struct - type t=pa_constructor - let compare=Pervasives.compare end) - -module PafMap=Map.Make(struct - type t=pa_fun - let compare=Pervasives.compare end) - -type cinfo= - {ci_constr: constructor; (* inductive type *) - ci_arity: int; (* # args *) - ci_nhyps: int} (* # projectable args *) - -type term= - Symb of constr - | Product of sorts_family * sorts_family - | Eps of identifier - | Appli of term*term - | Constructor of cinfo (* constructor arity + nhyps *) - -type ccpattern = - PApp of term * ccpattern list (* arguments are reversed *) - | PVar of int - -type rule= - Congruence - | Axiom of constr * bool - | Injection of int * pa_constructor * int * pa_constructor * int - -type from= - Goal - | Hyp of constr - | HeqG of constr - | HeqnH of constr * constr - -type 'a eq = {lhs:int;rhs:int;rule:'a} - -type equality = rule eq - -type disequality = from eq - -type patt_kind = - Normal - | Trivial of types - | Creates_variables - -type quant_eq = - {qe_hyp_id: identifier; - qe_pol: bool; - qe_nvars:int; - qe_lhs: ccpattern; - qe_lhs_valid:patt_kind; - qe_rhs: ccpattern; - qe_rhs_valid:patt_kind} - -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 weight:int; - mutable lfathers:Intset.t; - mutable fathers:Intset.t; - mutable inductive_status: inductive_status; - class_type : Term.types; - mutable functions: Intset.t PafMap.t; - 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: (constr,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_mark) Queue.t; - mutable diseq: disequality list; - mutable quant: quant_eq list; - mutable pa_classes: Intset.t; - q_history: (identifier,int array) Hashtbl.t; - mutable rew_depth:int; - mutable changed:bool; - by_type: (types,Intset.t) Hashtbl.t; - mutable gls:Proof_type.goal Tacmach.sigma} - -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 depth gls: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=[]; - quant=[]; - pa_classes=Intset.empty; - q_history=Hashtbl.create init_size; - rew_depth=depth; - by_type=Hashtbl.create init_size; - changed=false; - gls=gls} - -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).weight - -let axioms uf = uf.axioms - -let epsilons uf = uf.epsilons - -let add_lfather uf i t= - let r=get_representative uf i in - r.weight<-r.weight+1; - r.lfathers<-Intset.add t r.lfathers; - r.fathers <-Intset.add t r.fathers - -let add_rfather uf i t= - let r=get_representative uf i in - r.weight<-r.weight+1; - r.fathers <-Intset.add t r.fathers - -exception Discriminable of int * pa_constructor * int * pa_constructor - -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 fsucc paf = - {paf with fnargs=succ paf.fnargs} - -let add_pac rep pac t = - if not (PacMap.mem pac rep.constructors) then - rep.constructors<-PacMap.add pac t rep.constructors - -let add_paf rep paf t = - let already = - try PafMap.find paf rep.functions with Not_found -> Intset.empty in - rep.functions<- PafMap.add paf (Intset.add t already) rep.functions - -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 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 typ = - {weight=0; - lfathers=Intset.empty; - fathers=Intset.empty; - inductive_status=Unknown; - class_type=typ; - functions=PafMap.empty; - constructors=PacMap.empty} - -(* rebuild a constr from an applicative term *) - -let _A_ = Name (id_of_string "A") -let _B_ = Name (id_of_string "A") -let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2) - -let cc_product s1 s2 = - mkLambda(_A_,mkSort(Termops.new_sort_in_family s1), - mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_)) - -let rec constr_of_term = function - Symb s->s - | Product(s1,s2) -> cc_product s1 s2 - | Eps id -> mkVar id - | Constructor cinfo -> mkConstruct cinfo.ci_constr - | Appli (s1,s2)-> - make_app [(constr_of_term s2)] s1 -and make_app l=function - Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 - | other -> applistc (constr_of_term other) l - -(* rebuild a term from a pattern and a substitution *) - -let build_subst uf subst = - Array.map (fun i -> - try term uf i - with _ -> anomaly "incomplete matching") subst - -let rec inst_pattern subst = function - PVar i -> - subst.(pred i) - | PApp (t, args) -> - List.fold_right - (fun spat f -> Appli (f,inst_pattern subst spat)) - args t - -let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++ - Termops.print_constr (constr_of_term (term state.uf i)) ++ str "]" - -let pr_term t = str "[" ++ - Termops.print_constr (constr_of_term t) ++ str "]" - -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 typ = pf_type_of state.gls (constr_of_term t) in - let new_node= - match t with - Symb _ | Product (_,_) -> - let paf = - {fsym=b; - fnargs=0} in - Queue.add (b,Fmark paf) state.marks; - {clas= Rep (new_representative typ); - cpath= -1; - vertex= Leaf; - term= t} - | Eps id -> - {clas= Rep (new_representative typ); - cpath= -1; - vertex= Leaf; - term= t} - | Appli (t1,t2) -> - 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 typ); - cpath= -1; - vertex= Node(i1,i2); - term= t} - | Constructor cinfo -> - let paf = - {fsym=b; - fnargs=0} in - Queue.add (b,Fmark paf) state.marks; - let pac = - {cnode= b; - arity= cinfo.ci_arity; - args=[]} in - Queue.add (b,Cmark pac) state.marks; - {clas=Rep (new_representative typ); - cpath= -1; - vertex=Leaf; - term=t} - in - uf.map.(b)<-new_node; - Hashtbl.add uf.syms t b; - Hashtbl.replace state.by_type typ - (Intset.add b - (try Hashtbl.find state.by_type typ with - Not_found -> Intset.empty)); - b - -let add_equality state c s t= - let i = add_term state s in - let j = add_term state t in - Queue.add {lhs=i;rhs=j;rule=Axiom(c,false)} state.combine; - Hashtbl.add state.uf.axioms c (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 add_quant state id pol (nvars,valid1,patt1,valid2,patt2) = - state.quant<- - {qe_hyp_id= id; - qe_pol= pol; - qe_nvars=nvars; - qe_lhs= patt1; - qe_lhs_valid=valid1; - qe_rhs= patt2; - qe_rhs_valid=valid2}::state.quant - -let is_redundant state id args = - try - let norm_args = Array.map (find state.uf) args in - let prev_args = Hashtbl.find_all state.q_history id in - List.exists - (fun old_args -> - Util.array_for_all2 (fun i j -> i = find state.uf j) - norm_args old_args) - prev_args - with Not_found -> false - -let add_inst state (inst,int_subst) = - check_for_interrupt (); - if state.rew_depth > 0 then - if is_redundant state inst.qe_hyp_id int_subst then - debug msgnl (str "discarding redundant (dis)equality") - else - begin - Hashtbl.add state.q_history inst.qe_hyp_id int_subst; - let subst = build_subst (forest state) int_subst in - let prfhead= mkVar inst.qe_hyp_id in - let args = Array.map constr_of_term subst in - let _ = array_rev args in (* highest deBruijn index first *) - let prf= mkApp(prfhead,args) in - let s = inst_pattern subst inst.qe_lhs - and t = inst_pattern subst inst.qe_rhs in - state.changed<-true; - state.rew_depth<-pred state.rew_depth; - if inst.qe_pol then - begin - debug (fun () -> - msgnl - (str "Adding new equality, depth="++ int state.rew_depth); - msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++ - pr_term s ++ str " == " ++ pr_term t ++ str "]")) (); - add_equality state prf s t - end - else - begin - debug (fun () -> - msgnl - (str "Adding new disequality, depth="++ int state.rew_depth); - msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++ - pr_term s ++ str " <> " ++ pr_term t ++ str "]")) (); - add_disequality state (Hyp prf) s t - end - end - -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 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 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 (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++ - str " and " ++ pr_idx_term state i2 ++ str ".")) (); - let r1= get_representative state.uf i1 - and r2= get_representative state.uf i2 in - link state.uf i1 i2 eq; - Hashtbl.replace state.by_type r1.class_type - (Intset.remove i1 - (try Hashtbl.find state.by_type r1.class_type with - Not_found -> Intset.empty)); - let f= Intset.union r1.fathers r2.fathers in - r2.weight<-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,Cmark pac) state.marks) - r1.constructors; - PafMap.iter - (fun paf -> Intset.iter - (fun b -> Queue.add (b,Fmark paf) state.marks)) - r1.functions; - 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 (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks - | _,_ -> () - -let merge eq state = (* merge and no-merge *) - debug (fun () -> msgnl - (str "Merging " ++ pr_idx_term state eq.lhs ++ - str " and " ++ pr_idx_term state 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 - union state j i (swap eq) - -let update t state = (* update 1 and 2 *) - debug (fun () -> msgnl - (str "Updating term " ++ pr_idx_term state 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,Cmark (append_pac v pac)) state.marks) - rep.constructors; - PafMap.iter - (fun paf _ -> Queue.add (t,Fmark (fsucc paf)) state.marks) - rep.functions; - 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_function_mark t rep paf state = - add_paf rep paf t; - state.terms<-Intset.union rep.lfathers state.terms - -let process_constructor_mark t i rep pac state = - 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 - -let process_mark t m state = - debug (fun () -> msgnl - (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) (); - let i=find state.uf t in - let rep=get_representative state.uf i in - match m with - Fmark paf -> process_function_mark t rep paf state - | Cmark pac -> process_constructor_mark t i rep pac state - -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 (fun () -> msg - (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++ - pr_idx_term state dis.rhs ++ str " ... ")) (); - if find uf dis.lhs=find uf dis.rhs then - begin debug msgnl (str "Yes");Some dis end - else - 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; - true - with Queue.Empty -> - try - let (t,m) = Queue.take state.marks in - process_mark t m state; - true - with Queue.Empty -> - try - let t = Intset.choose state.terms in - state.terms<-Intset.remove t state.terms; - update t state; - true - with Not_found -> false - -let __eps__ = id_of_string "_eps_" - -let new_state_var typ state = - let id = pf_get_new_id __eps__ state.gls in - state.gls<- - {state.gls with it = - {state.gls.it with evar_hyps = - Environ.push_named_context_val (id,None,typ) - state.gls.it.evar_hyps}}; - id - -let complete_one_class state i= - match (get_representative state.uf i).inductive_status with - Partial pac -> - let rec app t typ n = - if n<=0 then t else - let _,etyp,rest= destProd typ in - let id = new_state_var etyp state in - app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = pf_type_of state.gls - (constr_of_term (term state.uf pac.cnode)) in - let _args = - List.map (fun i -> constr_of_term (term state.uf i)) - pac.args in - let typ = prod_applist _c (List.rev _args) in - let ct = app (term state.uf i) typ pac.arity in - state.uf.epsilons <- pac :: state.uf.epsilons; - ignore (add_term state ct) - | _ -> anomaly "wrong incomplete class" - -let complete state = - Intset.iter (complete_one_class state) state.pa_classes - -type matching_problem = -{mp_subst : int array; - mp_inst : quant_eq; - mp_stack : (ccpattern*int) list } - -let make_fun_table state = - let uf= state.uf in - let funtab=ref PafMap.empty in - Array.iteri - (fun i inode -> if i < uf.size then - match inode.clas with - Rep rep -> - PafMap.iter - (fun paf _ -> - let elem = - try PafMap.find paf !funtab - with Not_found -> Intset.empty in - funtab:= PafMap.add paf (Intset.add i elem) !funtab) - rep.functions - | _ -> ()) state.uf.map; - !funtab - - -let rec do_match state res pb_stack = - let mp=Stack.pop pb_stack in - match mp.mp_stack with - [] -> - res:= (mp.mp_inst,mp.mp_subst) :: !res - | (patt,cl)::remains -> - let uf=state.uf in - match patt with - PVar i -> - if mp.mp_subst.(pred i)<0 then - begin - mp.mp_subst.(pred i)<- cl; (* no aliasing problem here *) - Stack.push {mp with mp_stack=remains} pb_stack - end - else - if mp.mp_subst.(pred i) = cl then - Stack.push {mp with mp_stack=remains} pb_stack - else (* mismatch for non-linear variable in pattern *) () - | PApp (f,[]) -> - begin - try let j=Hashtbl.find uf.syms f in - if find uf j =cl then - Stack.push {mp with mp_stack=remains} pb_stack - with Not_found -> () - end - | PApp(f, ((last_arg::rem_args) as args)) -> - try - let j=Hashtbl.find uf.syms f in - let paf={fsym=j;fnargs=List.length args} in - let rep=get_representative uf cl in - let good_terms = PafMap.find paf rep.functions in - let aux i = - let (s,t) = signature state.uf i in - Stack.push - {mp with - mp_subst=Array.copy mp.mp_subst; - mp_stack= - (PApp(f,rem_args),s) :: - (last_arg,t) :: remains} pb_stack in - Intset.iter aux good_terms - with Not_found -> () - -let paf_of_patt syms = function - PVar _ -> invalid_arg "paf_of_patt: pattern is trivial" - | PApp (f,args) -> - {fsym=Hashtbl.find syms f; - fnargs=List.length args} - -let init_pb_stack state = - let syms= state.uf.syms in - let pb_stack = Stack.create () in - let funtab = make_fun_table state in - let aux inst = - begin - let good_classes = - match inst.qe_lhs_valid with - Creates_variables -> Intset.empty - | Normal -> - begin - try - let paf= paf_of_patt syms inst.qe_lhs in - PafMap.find paf funtab - with Not_found -> Intset.empty - end - | Trivial typ -> - begin - try - Hashtbl.find state.by_type typ - with Not_found -> Intset.empty - end in - Intset.iter (fun i -> - Stack.push - {mp_subst = Array.make inst.qe_nvars (-1); - mp_inst=inst; - mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes - end; - begin - let good_classes = - match inst.qe_rhs_valid with - Creates_variables -> Intset.empty - | Normal -> - begin - try - let paf= paf_of_patt syms inst.qe_rhs in - PafMap.find paf funtab - with Not_found -> Intset.empty - end - | Trivial typ -> - begin - try - Hashtbl.find state.by_type typ - with Not_found -> Intset.empty - end in - Intset.iter (fun i -> - Stack.push - {mp_subst = Array.make inst.qe_nvars (-1); - mp_inst=inst; - mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes - end in - List.iter aux state.quant; - pb_stack - -let find_instances state = - let pb_stack= init_pb_stack state in - let res =ref [] in - let _ = - debug msgnl (str "Running E-matching algorithm ... "); - try - while true do - check_for_interrupt (); - do_match state res pb_stack - done; - anomaly "get out of here !" - with Stack.Empty -> () in - !res - -let rec execute first_run state = - debug msgnl (str "Executing ... "); - try - while - check_for_interrupt (); - one_step state do () - done; - 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 - if state.rew_depth>0 then - let l=find_instances state in - List.iter (add_inst state) l; - if state.changed then - begin - state.changed <- false; - execute true state - end - else - begin - debug msgnl (str "Out of instances ... "); - None - end - else - begin - debug msgnl (str "Out of depth ... "); - None - end - | Some dis -> Some - begin - if first_run then Contradiction dis - else Incomplete - end - with Discriminable(s,spac,t,tpac) -> Some - begin - if first_run then Discrimination (s,spac,t,tpac) - else Incomplete - end - - diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli deleted file mode 100644 index cdc0065e..00000000 --- a/contrib/cc/ccalgo.mli +++ /dev/null @@ -1,222 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: ccalgo.mli 10579 2008-02-21 13:54:00Z corbinea $ *) - -open Util -open Term -open Names - -type cinfo = - {ci_constr: constructor; (* inductive type *) - ci_arity: int; (* # args *) - ci_nhyps: int} (* # projectable args *) - -type term = - Symb of constr - | Product of sorts_family * sorts_family - | Eps of identifier - | Appli of term*term - | Constructor of cinfo (* constructor arity + nhyps *) - -type patt_kind = - Normal - | Trivial of types - | Creates_variables - -type ccpattern = - PApp of term * ccpattern list - | PVar of int - -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 constr * bool - | Injection of int * pa_constructor * int * pa_constructor * int - -type from= - Goal - | Hyp of constr - | HeqG of constr - | HeqnH of constr*constr - -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 constr_of_term : term -> constr - -val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit - -val forest : state -> forest - -val axioms : forest -> (constr, term * term) Hashtbl.t - -val epsilons : forest -> pa_constructor list - -val empty : int -> Proof_type.goal Tacmach.sigma -> state - -val add_term : state -> term -> int - -val add_equality : state -> constr -> term -> term -> unit - -val add_disequality : state -> from -> term -> term -> unit - -val add_quant : state -> identifier -> bool -> - int * patt_kind * ccpattern * patt_kind * ccpattern -> 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 - -type quant_eq= - {qe_hyp_id: identifier; - qe_pol: bool; - qe_nvars:int; - qe_lhs: ccpattern; - qe_lhs_valid:patt_kind; - qe_rhs: ccpattern; - qe_rhs_valid:patt_kind} - - -type pa_fun= - {fsym:int; - fnargs:int} - -type matching_problem - -module PafMap: Map.S with type key = pa_fun - -val make_fun_table : state -> Intset.t PafMap.t - -val do_match : state -> - (quant_eq * int array) list ref -> matching_problem Stack.t -> unit - -val init_pb_stack : state -> matching_problem Stack.t - -val paf_of_patt : (term, int) Hashtbl.t -> ccpattern -> pa_fun - -val find_instances : state -> (quant_eq * int array) 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 - -type rule = - Congruence - | Axiom of Names.identifier - | Injection of int*int*int*int - -type equality = - {lhs : int; - rhs : int; - rule : rule} - -module ST : -sig - type t - val empty : unit -> t - val enter : int -> int * int -> t -> unit - val query : int * int -> t -> int - val delete : int -> t -> unit - val delete_list : int list -> t -> unit -end - -module UF : -sig - type t - exception Discriminable of int * int * int * int * t - val empty : unit -> t - val find : t -> int -> int - val size : t -> int -> int - val get_constructor : t -> int -> Names.constructor - val pac_arity : t -> int -> int * int -> int - val mem_node_pac : t -> int -> int * int -> int - val add_pacs : t -> int -> pa_constructor PacMap.t -> - int list * equality list - val term : t -> int -> term - val subterms : t -> int -> int * int - val add : t -> term -> int - val union : t -> int -> int -> equality -> int list * equality list - val join_path : t -> int -> int -> - ((int*int)*equality) list* - ((int*int)*equality) list -end - - -val combine_rec : UF.t -> int list -> equality list -val process_rec : UF.t -> equality list -> int list - -val cc : UF.t -> unit - -val make_uf : - (Names.identifier * (term * term)) list -> UF.t - -val add_one_diseq : UF.t -> (term * term) -> int * int - -val add_disaxioms : - UF.t -> (Names.identifier * (term * term)) list -> - (Names.identifier * (int * int)) list - -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 deleted file mode 100644 index a459b18f..00000000 --- a/contrib/cc/ccproof.ml +++ /dev/null @@ -1,153 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: ccproof.ml 9857 2007-05-24 14:21:08Z corbinea $ *) - -(* This file uses the (non-compressed) union-find structure to generate *) -(* proof-trees that will be transformed into proof-terms in cctac.ml4 *) - -open Util -open Names -open Term -open Ccalgo - -type rule= - Ax of constr - | SymAx of constr - | Refl of term - | Trans of proof*proof - | Congr of proof*proof - | Inject of proof*constructor*int*int -and proof = - {p_lhs:term;p_rhs:term;p_rule:rule} - -let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t} - -let pcongr p1 p2 = - match p1.p_rule,p2.p_rule with - Refl t1, Refl t2 -> prefl (Appli (t1,t2)) - | _, _ -> - {p_lhs=Appli (p1.p_lhs,p2.p_lhs); - p_rhs=Appli (p1.p_rhs,p2.p_rhs); - p_rule=Congr (p1,p2)} - -let rec ptrans p1 p3= - match p1.p_rule,p3.p_rule with - Refl _, _ ->p3 - | _, Refl _ ->p1 - | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3) - | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4) - | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) -> - ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5 - | _, _ -> - if p1.p_rhs = p3.p_lhs then - {p_lhs=p1.p_lhs; - p_rhs=p3.p_rhs; - p_rule=Trans (p1,p3)} - else anomaly "invalid cc transitivity" - -let rec psym p = - match p.p_rule with - Refl _ -> p - | SymAx s -> - {p_lhs=p.p_rhs; - p_rhs=p.p_lhs; - p_rule=Ax s} - | Ax s-> - {p_lhs=p.p_rhs; - p_rhs=p.p_lhs; - p_rule=SymAx s} - | Inject (p0,c,n,a)-> - {p_lhs=p.p_rhs; - p_rhs=p.p_lhs; - p_rule=Inject (psym p0,c,n,a)} - | Trans (p1,p2)-> ptrans (psym p2) (psym p1) - | Congr (p1,p2)-> pcongr (psym p1) (psym p2) - -let pax axioms s = - let l,r = Hashtbl.find axioms s in - {p_lhs=l; - p_rhs=r; - p_rule=Ax s} - -let psymax axioms s = - let l,r = Hashtbl.find axioms s in - {p_lhs=r; - p_rhs=l; - p_rule=SymAx s} - -let rec nth_arg t n= - match t with - Appli (t1,t2)-> - if n>0 then - nth_arg t1 (n-1) - else t2 - | _ -> anomaly "nth_arg: not enough args" - -let pinject p c n a = - {p_lhs=nth_arg p.p_lhs (n-a); - p_rhs=nth_arg p.p_rhs (n-a); - p_rule=Inject(p,c,n,a)} - -let build_proof uf= - - let axioms = axioms uf in - - let rec equal_proof i j= - if i=j then prefl (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)= - let pi=equal_proof i eq.lhs in - let pj=psym (equal_proof j eq.rhs) in - let pij= - match eq.rule with - Axiom (s,reversed)-> - if reversed then psymax axioms s - else pax axioms s - | Congruence ->congr_proof eq.lhs eq.rhs - | Injection (ti,ipac,tj,jpac,k) -> - let p=ind_proof ti ipac tj jpac in - let cinfo= get_constructor_info uf ipac.cnode in - pinject p cinfo.ci_constr cinfo.ci_nhyps k - in ptrans (ptrans pi pij) pj - - 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 (prefl targ)) - - and path_proof i=function - [] -> prefl (term uf i) - | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x) - - and congr_proof i j= - let (i1,i2) = subterms uf i - and (j1,j2) = subterms uf j in - pcongr (equal_proof i1 j1) (equal_proof i2 j2) - - and ind_proof i ipac j jpac= - let p=equal_proof i j - and p1=constr_proof i i ipac - and p2=constr_proof j j jpac in - ptrans (psym p1) (ptrans p p2) - in - function - `Prove (i,j) -> equal_proof i j - | `Discr (i,ci,j,cj)-> ind_proof i ci j cj - - - diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli deleted file mode 100644 index 0eb97efe..00000000 --- a/contrib/cc/ccproof.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: ccproof.mli 9857 2007-05-24 14:21:08Z corbinea $ *) - -open Ccalgo -open Names -open Term - -type rule= - Ax of constr - | SymAx of constr - | Refl of term - | Trans of proof*proof - | Congr of proof*proof - | Inject of proof*constructor*int*int -and proof = - private {p_lhs:term;p_rhs:term;p_rule:rule} - -val build_proof : - forest -> - [ `Discr of int * pa_constructor * int * pa_constructor - | `Prove of int * int ] -> proof - - - diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml deleted file mode 100644 index 00cbbeee..00000000 --- a/contrib/cc/cctac.ml +++ /dev/null @@ -1,465 +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.ml 11671 2008-12-12 12:43:03Z 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 Typing -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 _refl_equal = constant ["Init";"Logic"] "refl_equal" - -let _sym_eq = constant ["Init";"Logic"] "sym_eq" - -let _trans_eq = constant ["Init";"Logic"] "trans_eq" - -let _eq = constant ["Init";"Logic"] "eq" - -let _False = constant ["Init";"Logic"] "False" - -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)) - -(* decompose member of equality in an applicative format *) - -let sf_of env sigma c = family_of_sort (destSort (whd_delta env (type_of env sigma c))) - -let rec decompose_term env sigma t= - match kind_of_term (whd env t) with - App (f,args)-> - let tf=decompose_term env sigma f in - let targs=Array.map (decompose_term env sigma) args in - Array.fold_left (fun s t->Appli (s,t)) tf targs - | Prod (_,a,_b) when not (dependent (mkRel 1) _b) -> - let b = pop _b in - let sort_b = sf_of env sigma b in - let sort_a = sf_of env sigma a in - Appli(Appli(Product (sort_a,sort_b) , - decompose_term env sigma a), - decompose_term env sigma b) - | 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} - | _ ->if closed0 t then (Symb t) else raise Not_found - -(* decompose equality in members and type *) - -let atom_of_constr env sigma 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 sigma args.(1), - decompose_term env sigma args.(2)) - else `Other (decompose_term env sigma term) - | _ -> `Other (decompose_term env sigma term) - -let rec pattern_of_constr env sigma c = - match kind_of_term (whd env c) with - App (f,args)-> - let pf = decompose_term env sigma f in - let pargs,lrels = List.split - (array_map_to_list (pattern_of_constr env sigma) args) in - PApp (pf,List.rev pargs), - List.fold_left Intset.union Intset.empty lrels - | Prod (_,a,_b) when not (dependent (mkRel 1) _b) -> - let b =pop _b in - let pa,sa = pattern_of_constr env sigma a in - let pb,sb = pattern_of_constr env sigma (pop b) in - let sort_b = sf_of env sigma b in - let sort_a = sf_of env sigma a in - PApp(Product (sort_a,sort_b), - [pa;pb]),(Intset.union sa sb) - | Rel i -> PVar i,Intset.singleton i - | _ -> - let pf = decompose_term env sigma c in - PApp (pf,[]),Intset.empty - -let non_trivial = function - PVar _ -> false - | _ -> true - -let patterns_of_constr env sigma nrels term= - let f,args= - try destApp (whd_delta env term) with _ -> raise Not_found in - if eq_constr f (Lazy.force _eq) && (Array.length args)=3 - then - let patt1,rels1 = pattern_of_constr env sigma args.(1) - and patt2,rels2 = pattern_of_constr env sigma args.(2) in - let valid1 = - if Intset.cardinal rels1 <> nrels then Creates_variables - else if non_trivial patt1 then Normal - else Trivial args.(0) - and valid2 = - if Intset.cardinal rels2 <> nrels then Creates_variables - else if non_trivial patt2 then Normal - else Trivial args.(0) in - if valid1 <> Creates_variables - || valid2 <> Creates_variables then - nrels,valid1,patt1,valid2,patt2 - else raise Not_found - else raise Not_found - -let rec quantified_atom_of_constr env sigma nrels term = - match kind_of_term (whd_delta env term) with - Prod (_,atom,ff) -> - if eq_constr ff (Lazy.force _False) then - let patts=patterns_of_constr env sigma nrels atom in - `Nrule patts - else - quantified_atom_of_constr env sigma (succ nrels) ff - | _ -> - let patts=patterns_of_constr env sigma nrels term in - `Rule patts - -let litteral_of_constr env sigma 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 sigma atom) with - `Eq(t,a,b) -> `Neq(t,a,b) - | `Other(p) -> `Nother(p) - else - begin - try - quantified_atom_of_constr env sigma 1 ff - with Not_found -> - `Other (decompose_term env sigma term) - end - | _ -> - atom_of_constr env sigma term - - -(* store all equalities from the context *) - -let rec make_prb gls depth additionnal_terms = - let env=pf_env gls in - let sigma=sig_sig gls in - let state = empty depth gls in - let pos_hyps = ref [] in - let neg_hyps =ref [] in - List.iter - (fun c -> - let t = decompose_term env sigma c in - ignore (add_term state t)) additionnal_terms; - List.iter - (fun (id,_,e) -> - begin - let cid=mkVar id in - match litteral_of_constr env sigma e with - `Eq (t,a,b) -> add_equality state cid a b - | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b - | `Other ph -> - List.iter - (fun (cidn,nh) -> - add_disequality state (HeqnH (cid,cidn)) ph nh) - !neg_hyps; - pos_hyps:=(cid,ph):: !pos_hyps - | `Nother nh -> - List.iter - (fun (cidp,ph) -> - add_disequality state (HeqnH (cidp,cid)) ph nh) - !pos_hyps; - neg_hyps:=(cid,nh):: !neg_hyps - | `Rule patts -> add_quant state id true patts - | `Nrule patts -> add_quant state id false patts - end) (Environ.named_context_of_val gls.it.evar_hyps); - begin - match atom_of_constr env sigma 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=pred (snd cstr) 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_case_info (pf_env gls) ind RegularStyle 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 _M =mkMeta - -let rec proof_tac p gls = - match p.p_rule with - Ax c -> exact_check c gls - | SymAx c -> - let l=constr_of_term p.p_lhs and - r=constr_of_term p.p_rhs in - let typ = refresh_universes (pf_type_of gls l) in - exact_check - (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls - | Refl t -> - let lr = constr_of_term t in - let typ = refresh_universes (pf_type_of gls lr) in - exact_check - (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls - | Trans (p1,p2)-> - let t1 = constr_of_term p1.p_lhs and - t2 = constr_of_term p1.p_rhs and - t3 = constr_of_term p2.p_rhs in - let typ = refresh_universes (pf_type_of gls t2) in - let prf = - mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in - tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls - | Congr (p1,p2)-> - let tf1=constr_of_term p1.p_lhs - and tx1=constr_of_term p2.p_lhs - and tf2=constr_of_term p1.p_rhs - and tx2=constr_of_term p2.p_rhs in - let typf = refresh_universes (pf_type_of gls tf1) in - let typx = refresh_universes (pf_type_of gls tx1) in - let typfx = refresh_universes (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;_M 1|]) in - let lemma2= - mkApp(Lazy.force _f_equal, - [|typx;typfx;tf2;tx1;tx2;_M 1|]) in - let prf = - mkApp(Lazy.force _trans_eq, - [|typfx; - mkApp(tf1,[|tx1|]); - mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in - tclTHENS (refine prf) - [tclTHEN (refine lemma1) (proof_tac p1); - tclFIRST - [tclTHEN (refine lemma2) (proof_tac p2); - reflexivity; - fun gls -> - errorlabstrm "Congruence" - (Pp.str - "I don't know how to handle dependent equality")]] gls - | Inject (prf,cstr,nargs,argind) -> - let ti=constr_of_term prf.p_lhs in - let tj=constr_of_term prf.p_rhs in - let default=constr_of_term p.p_lhs in - let intype=refresh_universes (pf_type_of gls ti) in - let outtype=refresh_universes (pf_type_of gls default) in - let special=mkRel (1+nargs-argind) in - let proj=build_projection intype outtype cstr special default gls in - let injt= - mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in - tclTHEN (refine injt) (proof_tac prf) gls - -let refute_tac c t1 t2 p gls = - let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype=refresh_universes (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 (c,[|mkVar hid|]) in - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p; simplest_elim false_t] gls - -let convert_to_goal_tac c t1 t2 p gls = - let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let sort=refresh_universes (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;c;tt2;mkVar e|]) in - tclTHENS (assert_tac (Name e) neweq) - [proof_tac p;exact_check endt] gls - -let convert_to_hyp_tac c1 t1 c2 t2 p gls = - let tt2=constr_of_term t2 in - let h=pf_get_new_id (id_of_string "H") gls in - let false_t=mkApp (c2,[|mkVar h|]) in - tclTHENS (assert_tac (Name h) tt2) - [convert_to_goal_tac c1 t1 t2 p; - simplest_elim false_t] gls - -let discriminate_tac cstr p gls = - let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in - let intype=refresh_universes (pf_type_of gls t1) 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;t1;t2;mkVar hid|]) in - let endt=mkApp (Lazy.force _eq_rect, - [|outtype;trivial;pred;identity;concl;injt|]) in - let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac 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 -> constr_of_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 depth additionnal_terms gls= - Coqlib.check_required_library ["Coq";"Init";"Logic"]; - let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in - let state = make_prb gls depth 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 cstr p gls - | Incomplete -> - let metacnt = ref 0 in - let newmeta _ = incr metacnt; _M !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 - match dis.rule with - Goal -> proof_tac p gls - | Hyp id -> refute_tac id ta tb p gls - | HeqG id -> - convert_to_goal_tac id ta tb p gls - | HeqnH (ida,idb) -> - convert_to_hyp_tac ida ta idb tb p gls - - -let cc_fail gls = - errorlabstrm "Congruence" (Pp.str "congruence failed.") - -let congruence_tac depth l = - tclORELSE - (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) - cc_fail - -(* Beware: reflexivity = constructor 1 = apply refl_equal - might be slow now, let's rather do something equivalent - to a "simple apply refl_equal" *) - -let simple_reflexivity () = apply (Lazy.force _refl_equal) - -(* The [f_equal] tactic. - - It mimics the use of lemmas [f_equal], [f_equal2], etc. - This isn't particularly related with congruence, apart from - the fact that congruence is called internally. -*) - -let f_equal gl = - let cut_eq c1 c2 = - let ty = refresh_universes (pf_type_of gl c1) in - tclTHENTRY - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) - (simple_reflexivity ()) - in - try match kind_of_term (pf_concl gl) with - | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> - begin match kind_of_term t, kind_of_term t' with - | App (f,v), App (f',v') when Array.length v = Array.length v' -> - let rec cuts i = - if i < 0 then tclTRY (congruence_tac 1000 []) - else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1)) - in cuts (Array.length v - 1) gl - | _ -> tclIDTAC gl - end - | _ -> tclIDTAC gl - with Type_errors.TypeError _ -> tclIDTAC gl diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli deleted file mode 100644 index 57ad0558..00000000 --- a/contrib/cc/cctac.mli +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: cctac.mli 10637 2008-03-07 23:52:56Z letouzey $ *) - -open Term -open Proof_type - -val proof_tac: Ccproof.proof -> Proof_type.tactic - -val cc_tactic : int -> constr list -> tactic - -val cc_fail : tactic - -val congruence_tac : int -> constr list -> tactic - -val f_equal : tactic diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4 deleted file mode 100644 index 9877e6fc..00000000 --- a/contrib/cc/g_congruence.ml4 +++ /dev/null @@ -1,29 +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: g_congruence.ml4 10637 2008-03-07 23:52:56Z letouzey $ *) - -open Cctac -open Tactics -open Tacticals - -(* Tactic registration *) - -TACTIC EXTEND cc - [ "congruence" ] -> [ congruence_tac 1000 [] ] - |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] - |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] - |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> - [ congruence_tac n l ] -END - -TACTIC EXTEND f_equal - [ "f_equal" ] -> [ f_equal ] -END |