summaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/README20
-rw-r--r--plugins/cc/cc_plugin.mllib5
-rw-r--r--plugins/cc/ccalgo.ml884
-rw-r--r--plugins/cc/ccalgo.mli222
-rw-r--r--plugins/cc/ccproof.ml153
-rw-r--r--plugins/cc/ccproof.mli31
-rw-r--r--plugins/cc/cctac.ml465
-rw-r--r--plugins/cc/cctac.mli22
-rw-r--r--plugins/cc/g_congruence.ml429
9 files changed, 1831 insertions, 0 deletions
diff --git a/plugins/cc/README b/plugins/cc/README
new file mode 100644
index 00000000..073b140e
--- /dev/null
+++ b/plugins/cc/README
@@ -0,0 +1,20 @@
+
+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/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mllib
new file mode 100644
index 00000000..1bcfc537
--- /dev/null
+++ b/plugins/cc/cc_plugin.mllib
@@ -0,0 +1,5 @@
+Ccalgo
+Ccproof
+Cctac
+G_congruence
+Cc_plugin_mod
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
new file mode 100644
index 00000000..9cc6f9de
--- /dev/null
+++ b/plugins/cc/ccalgo.ml
@@ -0,0 +1,884 @@
+(************************************************************************)
+(* 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$ *)
+
+(* 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=["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/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
new file mode 100644
index 00000000..5f56c7e6
--- /dev/null
+++ b/plugins/cc/ccalgo.mli
@@ -0,0 +1,222 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Util
+open 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/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
new file mode 100644
index 00000000..2a019ebf
--- /dev/null
+++ b/plugins/cc/ccproof.ml
@@ -0,0 +1,153 @@
+(************************************************************************)
+(* 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$ *)
+
+(* 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/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
new file mode 100644
index 00000000..2a0ca688
--- /dev/null
+++ b/plugins/cc/ccproof.mli
@@ -0,0 +1,31 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open 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/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
new file mode 100644
index 00000000..4e6ea802
--- /dev/null
+++ b/plugins/cc/cctac.ml
@@ -0,0 +1,465 @@
+(************************************************************************)
+(* 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$ *)
+
+(* 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 (sort_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 (decompose_prod_assum ti) in
+ let head=
+ if i=ci then special else default in
+ 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/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
new file mode 100644
index 00000000..7ed077bd
--- /dev/null
+++ b/plugins/cc/cctac.mli
@@ -0,0 +1,22 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Term
+open 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/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
new file mode 100644
index 00000000..d9db927a
--- /dev/null
+++ b/plugins/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$ *)
+
+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
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-04 02:53:17 +0000