From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- plugins/cc/README | 2 +- plugins/cc/ccalgo.ml | 517 ++++++++++++++++++++++++++------------------ plugins/cc/ccalgo.mli | 132 ++++++----- plugins/cc/ccproof.ml | 123 ++++++----- plugins/cc/ccproof.mli | 38 +++- plugins/cc/cctac.ml | 463 +++++++++++++++++++++------------------ plugins/cc/cctac.mli | 11 +- plugins/cc/g_congruence.ml4 | 8 +- 8 files changed, 747 insertions(+), 547 deletions(-) (limited to 'plugins/cc') diff --git a/plugins/cc/README b/plugins/cc/README index 073b140e..c616b5da 100644 --- a/plugins/cc/README +++ b/plugins/cc/README @@ -3,7 +3,7 @@ cctac: congruence-closure for coq author: Pierre Corbineau, Stage de DEA au LSV, ENS Cachan - Thèse au LRI, Université Paris Sud XI + Thèse au LRI, Université Paris Sud XI Files : diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 056ae3a9..29bca862 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* term r: term -> sign *) - type t = {toterm:(int*int,int) Hashtbl.t; - tosign:(int,int*int) Hashtbl.t} + module IntTable = Hashtbl.Make(Int) + module IntPair = + struct + type t = int * int + let equal (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 + let hash (i, j) = Hashset.Combine.combine (Int.hash i) (Int.hash j) + end + module IntPairTable = Hashtbl.Make(IntPair) + + type t = {toterm: int IntPairTable.t; + tosign: (int * int) IntTable.t} let empty ()= - {toterm=Hashtbl.create init_size; - tosign=Hashtbl.create init_size} + {toterm=IntPairTable.create init_size; + tosign=IntTable.create init_size} let enter t sign st= - if Hashtbl.mem st.toterm sign then - anomaly "enter: signature already entered" + if IntPairTable.mem st.toterm sign then + anomaly ~label:"enter" (Pp.str "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 + IntPairTable.replace st.toterm sign t; + IntTable.replace st.tosign t sign - let rev_query term st=Hashtbl.find st.tosign term + let query sign st=IntPairTable.find st.toterm sign let delete st t= - try let sign=Hashtbl.find st.tosign t in - Hashtbl.remove st.toterm sign; - Hashtbl.remove st.tosign t + try let sign=IntTable.find st.tosign t in + IntPairTable.remove st.toterm sign; + IntTable.remove st.tosign t with Not_found -> () - let rec delete_set st s = Intset.iter (delete st) s + let delete_set st s = Int.Set.iter (delete st) s end @@ -84,45 +93,78 @@ 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 PacOrd = +struct + type t = pa_constructor + let compare { cnode = cnode0; arity = arity0; args = args0 } + { cnode = cnode1; arity = arity1; args = args1 } = + let cmp = Int.compare cnode0 cnode1 in + if cmp = 0 then + let cmp' = Int.compare arity0 arity1 in + if cmp' = 0 then + List.compare Int.compare args0 args1 + else + cmp' + else + cmp +end + +module PafOrd = +struct + type t = pa_fun + let compare { fsym = fsym0; fnargs = fnargs0 } { fsym = fsym1; fnargs = fnargs1 } = + let cmp = Int.compare fsym0 fsym1 in + if cmp = 0 then + Int.compare fnargs0 fnargs1 + else + cmp +end -module PafMap=Map.Make(struct - type t=pa_fun - let compare=Pervasives.compare end) +module PacMap=Map.Make(PacOrd) +module PafMap=Map.Make(PafOrd) type cinfo= - {ci_constr: constructor; (* inductive type *) + {ci_constr: pconstructor; (* inductive type *) ci_arity: int; (* # args *) ci_nhyps: int} (* # projectable args *) +let family_eq f1 f2 = match f1, f2 with +| InProp, InProp +| InSet, InSet +| InType, InType -> true +| _ -> false + type term= Symb of constr | Product of sorts_family * sorts_family - | Eps of identifier + | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) let rec term_equal t1 t2 = match t1, t2 with - | Symb c1, Symb c2 -> eq_constr c1 c2 - | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2 - | Eps i1, Eps i2 -> id_ord i1 i2 = 0 + | Symb c1, Symb c2 -> eq_constr_nounivs c1 c2 + | Product (s1, t1), Product (s2, t2) -> family_eq s1 s2 && family_eq t1 t2 + | Eps i1, Eps i2 -> Id.equal i1 i2 | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2 - | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1}, - Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} -> - i1 = i2 && j1 = j2 && eq_constructor c1 c2 - | _ -> t1 = t2 + | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1}, + Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} -> + Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *) + | _ -> false + +open Hashset.Combine -open Hashtbl_alt.Combine +let hash_sorts_family = function +| InProp -> 0 +| InSet -> 1 +| InType -> 2 let rec hash_term = function | Symb c -> combine 1 (hash_constr c) - | Product (s1, s2) -> combine3 2 (Hashtbl.hash s1) (Hashtbl.hash s2) - | Eps i -> combine 3 (Hashtbl.hash i) + | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2) + | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) - | Constructor {ci_constr=c; ci_arity=i; ci_nhyps=j} -> combine4 5 (Hashtbl.hash c) i j + | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j type ccpattern = PApp of term * ccpattern list (* arguments are reversed *) @@ -151,14 +193,16 @@ type patt_kind = | 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} - + { + qe_hyp_id: Id.t; + 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 @@ -174,12 +218,11 @@ type inductive_status = type representative= {mutable weight:int; - mutable lfathers:Intset.t; - mutable fathers:Intset.t; + mutable lfathers:Int.Set.t; + mutable fathers:Int.Set.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) *) + mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality @@ -188,12 +231,13 @@ type vertex = Leaf| Node of (int*int) type node = {mutable clas:cl; mutable cpath: int; + mutable constructors: int PacMap.t; vertex:vertex; term:term} module Constrhash = Hashtbl.Make (struct type t = constr - let equal = eq_constr + let equal = eq_constr_nounivs let hash = hash_constr end) module Typehash = Constrhash @@ -205,9 +249,9 @@ module Termhash = Hashtbl.Make end) module Identhash = Hashtbl.Make - (struct type t = identifier - let equal = Pervasives.(=) - let hash = Hashtbl.hash + (struct type t = Id.t + let equal = Id.equal + let hash = Id.hash end) type forest= @@ -221,45 +265,54 @@ type forest= type state = {uf: forest; sigtable:ST.t; - mutable terms: Intset.t; + mutable terms: Int.Set.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; + mutable pa_classes: Int.Set.t; q_history: (int array) Identhash.t; mutable rew_depth:int; mutable changed:bool; - by_type: Intset.t Typehash.t; + by_type: Int.Set.t Typehash.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)} - + { + clas=Eqto (min_int,{lhs=min_int;rhs=min_int;rule=Congruence}); + cpath=min_int; + constructors=PacMap.empty; + vertex=Leaf; + term=Symb (mkRel min_int) + } + +let empty_forest() = + { + max_size=init_size; + size=0; + map=Array.make init_size dummy_node; + epsilons=[]; + axioms=Constrhash.create init_size; + syms=Termhash.create init_size + } + let empty depth gls:state = - {uf= - {max_size=init_size; - size=0; - map=Array.create init_size dummy_node; - epsilons=[]; - axioms=Constrhash.create init_size; - syms=Termhash.create init_size}; - terms=Intset.empty; - combine=Queue.create (); - marks=Queue.create (); - sigtable=ST.empty (); - diseq=[]; - quant=[]; - pa_classes=Intset.empty; - q_history=Identhash.create init_size; - rew_depth=depth; - by_type=Constrhash.create init_size; - changed=false; - gls=gls} - + { + uf= empty_forest (); + terms=Int.Set.empty; + combine=Queue.create (); + marks=Queue.create (); + sigtable=ST.empty (); + diseq=[]; + quant=[]; + pa_classes=Int.Set.empty; + q_history=Identhash.create init_size; + rew_depth=depth; + by_type=Constrhash.create init_size; + changed=false; + gls=gls + } + let forest state = state.uf let compress_path uf i j = uf.map.(j).cpath<-i @@ -274,15 +327,25 @@ 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" + | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative") + +let get_constructors uf i= uf.map.(i).constructors let find_pac uf i pac = - PacMap.find pac (get_representative uf i).constructors + PacMap.find pac (get_constructors uf i) + +let rec find_oldest_pac uf i pac= + try PacMap.find pac (get_constructors uf i) with + Not_found -> + match uf.map.(i).clas with + Eqto (j,_) -> find_oldest_pac uf j pac + | Rep _ -> raise Not_found + let get_constructor_info uf i= match uf.map.(i).term with Constructor cinfo->cinfo - | _ -> anomaly "get_constructor: not a constructor" + | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor") let size uf i= (get_representative uf i).weight @@ -294,13 +357,13 @@ 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 + r.lfathers<-Int.Set.add t r.lfathers; + r.fathers <-Int.Set.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 + r.fathers <-Int.Set.add t r.fathers exception Discriminable of int * pa_constructor * int * pa_constructor @@ -313,21 +376,21 @@ let tail_pac p= 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_pac node pac t = + if not (PacMap.mem pac node.constructors) then + node.constructors<-PacMap.add pac t node.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 + try PafMap.find paf rep.functions with Not_found -> Int.Set.empty in + rep.functions<- PafMap.add paf (Int.Set.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" + | _ -> anomaly ~label:"subterms" (Pp.str "not a node") let signature uf i= let j,k=subterms uf i in (find uf j,find uf k) @@ -335,9 +398,9 @@ let signature uf i= let next uf= let size=uf.size in let nsize= succ size in - if nsize=uf.max_size then + if Int.equal nsize uf.max_size then let newmax=uf.max_size * 3 / 2 + 1 in - let newmap=Array.create newmax dummy_node in + let newmap=Array.make newmax dummy_node in begin uf.max_size<-newmax; Array.blit uf.map 0 newmap 0 size; @@ -349,46 +412,63 @@ let next uf= let new_representative typ = {weight=0; - lfathers=Intset.empty; - fathers=Intset.empty; + lfathers=Int.Set.empty; + fathers=Int.Set.empty; inductive_status=Unknown; class_type=typ; - functions=PafMap.empty; - constructors=PacMap.empty} + functions=PafMap.empty} (* rebuild a constr from an applicative term *) -let _A_ = Name (id_of_string "A") -let _B_ = Name (id_of_string "A") +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_)) + mkLambda(_A_,mkSort(Universes.new_sort_in_family s1), + mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_)) let rec constr_of_term = function - Symb s->s + Symb s-> applist_projection s [] | Product(s1,s2) -> cc_product s1 s2 | Eps id -> mkVar id - | Constructor cinfo -> mkConstruct cinfo.ci_constr + | Constructor cinfo -> mkConstructU 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 + | other -> + applist_proj other l +and applist_proj c l = + match c with + | Symb s -> applist_projection s l + | _ -> applistc (constr_of_term c) l +and applist_projection c l = + match kind_of_term c with + | Const c when Environ.is_projection (fst c) (Global.env()) -> + let p = Projection.make (fst c) false in + (match l with + | [] -> (* Expand the projection *) + let ty,_ = Typeops.type_of_constant (Global.env ()) c in + let pb = Environ.lookup_projection p (Global.env()) in + let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in + it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx + | hd :: tl -> + applistc (mkProj (p, hd)) tl) + | _ -> applistc c l let rec canonize_name c = let func = canonize_name in match kind_of_term c with - | Const kn -> + | Const (kn,u) -> let canon_const = constant_of_kn (canonical_con kn) in - (mkConst canon_const) - | Ind (kn,i) -> + (mkConstU (canon_const,u)) + | Ind ((kn,i),u) -> let canon_mind = mind_of_kn (canonical_mind kn) in - (mkInd (canon_mind,i)) - | Construct ((kn,i),j) -> + (mkIndU ((canon_mind,i),u)) + | Construct (((kn,i),j),u) -> let canon_mind = mind_of_kn (canonical_mind kn) in - mkConstruct ((canon_mind,i),j) + mkConstructU (((canon_mind,i),j),u) | Prod (na,t,ct) -> mkProd (na,func t, func ct) | Lambda (na,t,ct) -> @@ -396,16 +476,22 @@ let rec canonize_name c = | LetIn (na,b,t,ct) -> mkLetIn (na, func b,func t,func ct) | App (ct,l) -> - mkApp (func ct,array_smartmap func l) + mkApp (func ct,Array.smartmap func l) + | Proj(p,c) -> + let p' = Projection.map (fun kn -> + constant_of_kn (canonical_con kn)) p in + (mkProj (p', func c)) | _ -> c (* rebuild a term from a pattern and a substitution *) let build_subst uf subst = - Array.map (fun i -> - try term uf i - with e when Errors.noncritical e -> - anomaly "incomplete matching") subst + Array.map + (fun i -> + try term uf i + with e when Errors.noncritical e -> + anomaly (Pp.str "incomplete matching")) + subst let rec inst_pattern subst = function PVar i -> @@ -415,8 +501,8 @@ let rec inst_pattern subst = function (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_idx_term uf i = str "[" ++ int i ++ str ":=" ++ + Termops.print_constr (constr_of_term (term uf i)) ++ str "]" let pr_term t = str "[" ++ Termops.print_constr (constr_of_term t) ++ str "]" @@ -426,7 +512,8 @@ let rec add_term state t= try Termhash.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 trm = constr_of_term t in + let typ = pf_type_of state.gls trm in let typ = canonize_name typ in let new_node= match t with @@ -437,20 +524,23 @@ let rec add_term state t= Queue.add (b,Fmark paf) state.marks; {clas= Rep (new_representative typ); cpath= -1; + constructors=PacMap.empty; vertex= Leaf; term= t} | Eps id -> {clas= Rep (new_representative typ); cpath= -1; + constructors=PacMap.empty; 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; + state.terms<-Int.Set.add b state.terms; {clas= Rep (new_representative typ); cpath= -1; + constructors=PacMap.empty; vertex= Node(i1,i2); term= t} | Constructor cinfo -> @@ -465,15 +555,16 @@ let rec add_term state t= Queue.add (b,Cmark pac) state.marks; {clas=Rep (new_representative typ); cpath= -1; + constructors=PacMap.empty; vertex=Leaf; term=t} in uf.map.(b)<-new_node; Termhash.add uf.syms t b; Typehash.replace state.by_type typ - (Intset.add b + (Int.Set.add b (try Typehash.find state.by_type typ with - Not_found -> Intset.empty)); + Not_found -> Int.Set.empty)); b let add_equality state c s t= @@ -503,23 +594,23 @@ let is_redundant state id args = let prev_args = Identhash.find_all state.q_history id in List.exists (fun old_args -> - Util.array_for_all2 (fun i j -> i = find state.uf j) + Util.Array.for_all2 (fun i j -> Int.equal 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 (); + Control.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") + debug (str "discarding redundant (dis)equality") else begin Identhash.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 _ = 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 @@ -527,20 +618,18 @@ let add_inst state (inst,int_subst) = 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 "]")) (); + debug ( + (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ + (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 "]")) (); + debug ( + (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ + (str " [" ++ Termops.print_constr prf ++ str " : " ++ + pr_term s ++ str " <> " ++ pr_term t ++ str "]")); add_disequality state (Hyp prf) s t end end @@ -552,75 +641,77 @@ let link uf i j eq = (* links i -> 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) + Eqto (j,eq) ->down_path uf j (((i,j),eq)::l) | Rep _ ->l +let eq_pair (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 + let rec min_path=function ([],l2)->([],l2) | (l1,[])->(l1,[]) - | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2) + | (((c1,t1)::q1),((c2,t2)::q2)) when eq_pair c1 c2 -> min_path (q1,q2) | cpl -> cpl let join_path uf i j= - assert (find uf i=find uf j); + assert (Int.equal (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 ".")) (); + debug (str "Linking " ++ pr_idx_term state.uf i1 ++ + str " and " ++ pr_idx_term state.uf i2 ++ str "."); let r1= get_representative state.uf i1 and r2= get_representative state.uf i2 in link state.uf i1 i2 eq; Constrhash.replace state.by_type r1.class_type - (Intset.remove i1 + (Int.Set.remove i1 (try Constrhash.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; + Not_found -> Int.Set.empty)); + let f= Int.Set.union r1.fathers r2.fathers in + r2.weight<-Int.Set.cardinal f; r2.fathers<-f; - r2.lfathers<-Intset.union r1.lfathers r2.lfathers; + r2.lfathers<-Int.Set.union r1.lfathers r2.lfathers; ST.delete_set state.sigtable r1.fathers; - state.terms<-Intset.union state.terms r1.fathers; + state.terms<-Int.Set.union state.terms r1.fathers; PacMap.iter (fun pac b -> Queue.add (b,Cmark pac) state.marks) - r1.constructors; + state.uf.map.(i1).constructors; PafMap.iter - (fun paf -> Intset.iter + (fun paf -> Int.Set.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 + state.pa_classes<-Int.Set.remove i1 state.pa_classes; + state.pa_classes<-Int.Set.add i2 state.pa_classes | Partial _ ,(Partial _ |Partial_applied) -> - state.pa_classes<-Intset.remove i1 state.pa_classes + state.pa_classes<-Int.Set.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; + state.pa_classes<-Int.Set.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 ".")) (); + debug + (str "Merging " ++ pr_idx_term state.uf eq.lhs ++ + str " and " ++ pr_idx_term state.uf 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 not (Int.equal 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 ".")) (); + debug + (str "Updating term " ++ pr_idx_term state.uf 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 @@ -628,12 +719,12 @@ let update t state = (* update 1 and 2 *) match rep.inductive_status with Partial _ -> rep.inductive_status <- Partial_applied; - state.pa_classes <- Intset.remove i state.pa_classes + state.pa_classes <- Int.Set.remove i state.pa_classes | _ -> () end; PacMap.iter (fun pac _ -> Queue.add (t,Cmark (append_pac v pac)) state.marks) - rep.constructors; + (get_constructors state.uf i); PafMap.iter (fun paf _ -> Queue.add (t,Fmark (fsucc paf)) state.marks) rep.functions; @@ -645,12 +736,13 @@ let update t state = (* update 1 and 2 *) let process_function_mark t rep paf state = add_paf rep paf t; - state.terms<-Intset.union rep.lfathers state.terms + state.terms<-Int.Set.union rep.lfathers state.terms let process_constructor_mark t i rep pac state = - match rep.inductive_status with + add_pac state.uf.map.(i) pac t; + match rep.inductive_status with Total (s,opac) -> - if pac.cnode <> opac.cnode then (* Conflict *) + if not (Int.equal pac.cnode opac.cnode) then (* Conflict *) raise (Discriminable (s,opac,t,pac)) else (* Match *) let cinfo = get_constructor_info state.uf pac.cnode in @@ -662,26 +754,26 @@ let process_constructor_mark t i rep pac state = {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" + | _-> anomaly ~label:"add_pacs" + (Pp.str "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 +(* add_pac state.uf.map.(i) pac t; *) + state.terms<-Int.Set.union rep.lfathers state.terms | Unknown -> - if pac.arity = 0 then + if Int.equal 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; + (* add_pac state.uf.map.(i) pac t; *) + state.terms<-Int.Set.union rep.lfathers state.terms; rep.inductive_status <- Partial pac; - state.pa_classes<- Intset.add i state.pa_classes + state.pa_classes<- Int.Set.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 ".")) (); + debug + (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str "."); let i=find state.uf t in let rep=get_representative state.uf i in match m with @@ -696,14 +788,15 @@ type explanation = 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 + | dis::q -> + let (info, ans) = + if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis) + else (str "No", check_aux q) + in + let _ = debug + (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++ + pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in + ans | [] -> None in check_aux state.diseq @@ -720,13 +813,13 @@ let one_step state = true with Queue.Empty -> try - let t = Intset.choose state.terms in - state.terms<-Intset.remove t state.terms; + let t = Int.Set.choose state.terms in + state.terms<-Int.Set.remove t state.terms; update t state; true with Not_found -> false -let __eps__ = id_of_string "_eps_" +let __eps__ = Id.of_string "_eps_" let new_state_var typ state = let id = pf_get_new_id __eps__ state.gls in @@ -752,10 +845,10 @@ let complete_one_class state i= 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" + | _ -> anomaly (Pp.str "wrong incomplete class") let complete state = - Intset.iter (complete_one_class state) state.pa_classes + Int.Set.iter (complete_one_class state) state.pa_classes type matching_problem = {mp_subst : int array; @@ -773,14 +866,14 @@ let make_fun_table state = (fun paf _ -> let elem = try PafMap.find paf !funtab - with Not_found -> Intset.empty in - funtab:= PafMap.add paf (Intset.add i elem) !funtab) + with Not_found -> Int.Set.empty in + funtab:= PafMap.add paf (Int.Set.add i elem) !funtab) rep.functions | _ -> ()) state.uf.map; !funtab -let rec do_match state res pb_stack = +let do_match state res pb_stack = let mp=Stack.pop pb_stack in match mp.mp_stack with [] -> @@ -795,13 +888,13 @@ let rec do_match state res pb_stack = Stack.push {mp with mp_stack=remains} pb_stack end else - if mp.mp_subst.(pred i) = cl then + if Int.equal 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=Termhash.find uf.syms f in - if find uf j =cl then + if Int.equal (find uf j) cl then Stack.push {mp with mp_stack=remains} pb_stack with Not_found -> () end @@ -819,7 +912,7 @@ let rec do_match state res pb_stack = mp_stack= (PApp(f,rem_args),s) :: (last_arg,t) :: remains} pb_stack in - Intset.iter aux good_terms + Int.Set.iter aux good_terms with Not_found -> () let paf_of_patt syms = function @@ -836,21 +929,21 @@ let init_pb_stack state = begin let good_classes = match inst.qe_lhs_valid with - Creates_variables -> Intset.empty + Creates_variables -> Int.Set.empty | Normal -> begin try let paf= paf_of_patt syms inst.qe_lhs in PafMap.find paf funtab - with Not_found -> Intset.empty + with Not_found -> Int.Set.empty end | Trivial typ -> begin try Typehash.find state.by_type typ - with Not_found -> Intset.empty + with Not_found -> Int.Set.empty end in - Intset.iter (fun i -> + Int.Set.iter (fun i -> Stack.push {mp_subst = Array.make inst.qe_nvars (-1); mp_inst=inst; @@ -859,21 +952,21 @@ let init_pb_stack state = begin let good_classes = match inst.qe_rhs_valid with - Creates_variables -> Intset.empty + Creates_variables -> Int.Set.empty | Normal -> begin try let paf= paf_of_patt syms inst.qe_rhs in PafMap.find paf funtab - with Not_found -> Intset.empty + with Not_found -> Int.Set.empty end | Trivial typ -> begin try Typehash.find state.by_type typ - with Not_found -> Intset.empty + with Not_found -> Int.Set.empty end in - Intset.iter (fun i -> + Int.Set.iter (fun i -> Stack.push {mp_subst = Array.make inst.qe_nvars (-1); mp_inst=inst; @@ -886,28 +979,28 @@ let find_instances state = let pb_stack= init_pb_stack state in let res =ref [] in let _ = - debug msgnl (str "Running E-matching algorithm ... "); + debug (str "Running E-matching algorithm ... "); try while true do - check_for_interrupt (); + Control.check_for_interrupt (); do_match state res pb_stack done; - anomaly "get out of here !" + anomaly (Pp.str "get out of here !") with Stack.Empty -> () in !res let rec execute first_run state = - debug msgnl (str "Executing ... "); + debug (str "Executing ... "); try while - check_for_interrupt (); + Control.check_for_interrupt (); one_step state do () done; match check_disequalities state with None -> - if not(Intset.is_empty state.pa_classes) then + if not(Int.Set.is_empty state.pa_classes) then begin - debug msgnl (str "First run was incomplete, completing ... "); + debug (str "First run was incomplete, completing ... "); complete state; execute false state end @@ -922,12 +1015,12 @@ let rec execute first_run state = end else begin - debug msgnl (str "Out of instances ... "); + debug (str "Out of instances ... "); None end else begin - debug msgnl (str "Out of depth ... "); + debug (str "Out of depth ... "); None end | Some dis -> Some diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index e4713728..c72843d5 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* term -> bool +module Constrhash : Hashtbl.S with type key = constr +module Termhash : Hashtbl.S with type key = term -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 @@ -61,17 +60,67 @@ type equality = rule eq type disequality = from eq +type patt_kind = + Normal + | Trivial of types + | Creates_variables + +type quant_eq= + {qe_hyp_id: Id.t; + qe_pol: bool; + qe_nvars:int; + qe_lhs: ccpattern; + qe_lhs_valid:patt_kind; + qe_rhs: ccpattern; + qe_rhs_valid:patt_kind} + +type inductive_status = + Unknown + | Partial of pa_constructor + | Partial_applied + | Total of (int * pa_constructor) + +type representative= + {mutable weight:int; + mutable lfathers:Int.Set.t; + mutable fathers:Int.Set.t; + mutable inductive_status: inductive_status; + class_type : Term.types; + mutable functions: Int.Set.t PafMap.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; + mutable constructors: int PacMap.t; + vertex:vertex; + term:term} + +type forest= + {mutable max_size:int; + mutable size:int; + mutable map: node array; + axioms: (term*term) Constrhash.t; + mutable epsilons: pa_constructor list; + syms: int Termhash.t} + +type state + type explanation = Discrimination of (int*pa_constructor*int*pa_constructor) | Contradiction of disequality | Incomplete -module Constrhash : Hashtbl.S with type key = constr -module Termhash : Hashtbl.S with type key = term +type matching_problem + +val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit +val debug : Pp.std_ppcmds -> unit val forest : state -> forest @@ -87,7 +136,7 @@ val add_equality : state -> constr -> term -> term -> unit val add_disequality : state -> from -> term -> term -> unit -val add_quant : state -> identifier -> bool -> +val add_quant : state -> Id.t -> bool -> int * patt_kind * ccpattern * patt_kind * ccpattern -> unit val tail_pac : pa_constructor -> pa_constructor @@ -96,6 +145,8 @@ val find : forest -> int -> int val find_pac : forest -> int -> pa_constructor -> int +val find_oldest_pac : forest -> int -> pa_constructor -> int + val term : forest -> int -> term val get_constructor_info : forest -> int -> cinfo @@ -105,25 +156,7 @@ 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 make_fun_table : state -> Int.Set.t PafMap.t val do_match : state -> (quant_eq * int array) list ref -> matching_problem Stack.t -> unit @@ -136,8 +169,9 @@ val find_instances : state -> (quant_eq * int array) list val execute : bool -> state -> explanation option +val pr_idx_term : forest -> int -> Pp.std_ppcmds - +val empty_forest: unit -> forest @@ -161,7 +195,7 @@ type term = type rule = Congruence - | Axiom of Names.identifier + | Axiom of Names.Id.t | Injection of int*int*int*int type equality = @@ -207,19 +241,19 @@ val process_rec : UF.t -> equality list -> int list val cc : UF.t -> unit val make_uf : - (Names.identifier * (term * term)) list -> UF.t + (Names.Id.t * (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 + UF.t -> (Names.Id.t * (term * term)) list -> + (Names.Id.t * (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)) + (Names.Id.t * (int * int)) list -> + (Names.Id.t * (int * int)) *) diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 037e9f66..42c03234 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0 then nth_arg t1 (n-1) else t2 - | _ -> anomaly "nth_arg: not enough args" + | _ -> anomaly ~label:"nth_arg" (Pp.str "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 rec equal_proof uf i j= + debug (str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); + if i=j then prefl (term uf i) else + let (li,lj)=join_path uf i j in + ptrans (path_proof uf i li) (psym (path_proof uf j lj)) + +and edge_proof uf ((i,j),eq)= + debug (str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); + let pi=equal_proof uf i eq.lhs in + let pj=psym (equal_proof uf j eq.rhs) in + let pij= + match eq.rule with + Axiom (s,reversed)-> + if reversed then psymax (axioms uf) s + else pax (axioms uf) s + | Congruence ->congr_proof uf eq.lhs eq.rhs + | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *) + let p=ind_proof uf 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 uf i ipac= + debug (str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20)); + let t=find_oldest_pac uf i ipac in + let eq_it=equal_proof uf i t in + if ipac.args=[] then + eq_it + else + let fipac=tail_pac ipac in + let (fi,arg)=subterms uf t in + let targ=term uf arg in + let p=constr_proof uf fi fipac in + ptrans eq_it (pcongr p (prefl targ)) + +and path_proof uf i l= + debug (str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++ + (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}"); + match l with + | [] -> prefl (term uf i) + | x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x) + +and congr_proof uf i j= + debug (str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); + let (i1,i2) = subterms uf i + and (j1,j2) = subterms uf j in + pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2) + +and ind_proof uf i ipac j jpac= + debug (str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); + let p=equal_proof uf i j + and p1=constr_proof uf i ipac + and p2=constr_proof uf j jpac in + ptrans (psym p1) (ptrans p p2) - 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 +let build_proof uf= + function + | `Prove (i,j) -> equal_proof uf i j + | `Discr (i,ci,j,cj)-> ind_proof uf i ci j cj diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index d55d3ef7..0e0eb6d2 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* proof + +val pcongr: proof -> proof -> proof + +val ptrans: proof -> proof -> proof + +val psym: proof -> proof + +val pax : (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t -> + Ccalgo.Constrhash.key -> proof + +val psymax : (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t -> + Ccalgo.Constrhash.key -> proof + +val pinject : proof -> pconstructor -> int -> int -> proof + +(** Proof building functions *) + +val equal_proof : forest -> int -> int -> proof + +val edge_proof : forest -> (int*int)*equality -> proof + +val path_proof : forest -> int -> ((int*int)*equality) list -> proof + +val congr_proof : forest -> int -> int -> proof + +val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof + +(** Main proof building function *) + 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 index 60d42916..7110e5b2 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -1,49 +1,39 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let (mind,i_ind),i_con = c in + | Construct c -> + let (((mind,i_ind),i_con),u)= c in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in - let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in - Constructor {ci_constr= (canon_ind,i_con); + let nargs=constructor_nallargs_env env (canon_ind,i_con) in + Constructor {ci_constr= ((canon_ind,i_con),u); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} | Ind c -> - let mind,i_ind = c in + let (mind,i_ind),u = c in let canon_mind = mind_of_kn (canonical_mind mind) in - let canon_ind = canon_mind,i_ind in (Symb (mkInd canon_ind)) - | Const c -> + let canon_ind = canon_mind,i_ind in (Symb (mkIndU (canon_ind,u))) + | Const (c,u) -> let canon_const = constant_of_kn (canonical_con c) in - (Symb (mkConst canon_const)) + (Symb (mkConstU (canon_const,u))) + | Proj (p, c) -> + let canon_const kn = constant_of_kn (canonical_con kn) in + let p' = Projection.map canon_const p in + (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) | _ ->if closed0 t then (Symb t) else raise Not_found (* decompose equality in members and type *) +open Globnames 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 + if is_global _eq f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -107,9 +103,9 @@ let rec pattern_of_constr env sigma c = 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 + (Array.map_to_list (pattern_of_constr env sigma) args) in PApp (pf,List.rev pargs), - List.fold_left Intset.union Intset.empty lrels + List.fold_left Int.Set.union Int.Set.empty lrels | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> let b = Termops.pop _b in let pa,sa = pattern_of_constr env sigma a in @@ -117,11 +113,11 @@ let rec pattern_of_constr env sigma c = 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 + [pa;pb]),(Int.Set.union sa sb) + | Rel i -> PVar i,Int.Set.singleton i | _ -> let pf = decompose_term env sigma c in - PApp (pf,[]),Intset.empty + PApp (pf,[]),Int.Set.empty let non_trivial = function PVar _ -> false @@ -129,23 +125,21 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= - try destApp (whd_delta env term) - with e when Errors.noncritical e -> raise Not_found - in - if eq_constr f (Lazy.force _eq) && (Array.length args)=3 + try destApp (whd_delta env term) with DestKO -> raise Not_found in + if is_global _eq f && Int.equal (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 + if not (Int.equal (Int.Set.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 + if not (Int.equal (Int.Set.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 + if valid1 != Creates_variables + || valid2 != Creates_variables then nrels,valid1,patt1,valid2,patt2 else raise Not_found else raise Not_found @@ -153,7 +147,7 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match kind_of_term (whd_delta env term) with Prod (id,atom,ff) -> - if eq_constr ff (Lazy.force _False) then + if is_global _False ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else @@ -165,7 +159,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let litteral_of_constr env sigma term= match kind_of_term (whd_delta env term) with | Prod (id,atom,ff) -> - if eq_constr ff (Lazy.force _False) then + if is_global _False ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) @@ -182,7 +176,7 @@ let litteral_of_constr env sigma term= (* store all equalities from the context *) -let rec make_prb gls depth additionnal_terms = +let make_prb gls depth additionnal_terms = let env=pf_env gls in let sigma=sig_sig gls in let state = empty depth gls in @@ -213,9 +207,9 @@ let rec make_prb gls depth additionnal_terms = 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 (Goal.V82.hyps gls.sigma gls.it)); + end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it)); begin - match atom_of_constr env sigma (pf_concl gls) with + match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with `Eq (t,a,b) -> add_disequality state Goal a b | `Other g -> List.iter @@ -226,226 +220,256 @@ let rec make_prb gls depth additionnal_terms = (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) -let build_projection intype outtype (cstr:constructor) special default gls= +let build_projection intype outtype (cstr:pconstructor) 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 (h,argv) = try destApp intype with DestKO -> (intype,[||]) in + let ind,u=destInd h in + let types=Inductiveops.arities_of_constructors env (ind,u) in let lp=Array.length types in - let ci=pred (snd cstr) in + let ci=pred (snd(fst cstr)) in let branch i= - let ti=Term.prod_appvect types.(i) argv in + let ti= prod_appvect types.(i) argv in let rc=fst (decompose_prod_assum ti) in let head= - if i=ci then special else default in + if Int.equal 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 + 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 = +let app_global f args k = + Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + +let new_app_global f args k = + Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + +let new_refine c = Proofview.V82.tactic (refine c) + +let rec proof_tac p : unit Proofview.tactic = + Proofview.Goal.nf_enter begin fun gl -> + let type_of t = Tacmach.New.pf_type_of gl t in + try (* type_of can raise exceptions *) match p.p_rule with - Ax c -> exact_check c gls + Ax c -> exact_check c | SymAx c -> let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - let typ = Termops.refresh_universes (pf_type_of gls l) in - exact_check - (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls + let typ = (* Termops.refresh_universes *) type_of l in + new_app_global _sym_eq [|typ;r;l;c|] exact_check | Refl t -> let lr = constr_of_term t in - let typ = Termops.refresh_universes (pf_type_of gls lr) in - exact_check - (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls + let typ = (* Termops.refresh_universes *) type_of lr in + new_app_global _refl_equal [|typ;constr_of_term t|] exact_check | 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 = Termops.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 + let typ = (* Termops.refresh_universes *) (type_of t2) in + let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in + Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)] | 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 = Termops.refresh_universes (pf_type_of gls tf1) in - let typx = Termops.refresh_universes (pf_type_of gls tx1) in - let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in - let id = pf_get_new_id (id_of_string "f") gls in + let typf = (* Termops.refresh_universes *)(type_of tf1) in + let typx = (* Termops.refresh_universes *) (type_of tx1) in + let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in + let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl 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 + app_global _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 + app_global _f_equal + [|typx;typfx;tf2;tx1;tx2;_M 1|] in let prf = - mkApp(Lazy.force _trans_eq, + app_global _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); + mkApp(tf2,[|tx2|]);_M 2;_M 3|] in + Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine)) + [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1); + Tacticals.New.tclFIRST + [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); reflexivity; - fun gls -> - errorlabstrm "Congruence" + Proofview.tclZERO (UserError ("Congruence" , (Pp.str - "I don't know how to handle dependent equality")]] gls + "I don't know how to handle dependent equality")))]] | 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 = Termops.refresh_universes (pf_type_of gls ti) in - let outtype = Termops.refresh_universes (pf_type_of gls default) in + let intype = (* Termops.refresh_universes *) (type_of ti) in + let outtype = (* Termops.refresh_universes *) (type_of default) in let special=mkRel (1+nargs-argind) in - let proj=build_projection intype outtype cstr special default gls in + let proj = + Tacmach.New.of_old (build_projection intype outtype cstr special default) gl + in let injt= - mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in - tclTHEN (refine injt) (proof_tac prf) gls + app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in + Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end -let refute_tac c t1 t2 p gls = +let refute_tac c t1 t2 p = + Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype = Termops.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 intype = + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl + in + let neweq= new_app_global _eq [|intype;tt1;tt2|] in + let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let false_t=mkApp (c,[|mkVar hid|]) in - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p; simplest_elim false_t] gls + Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) + [proof_tac p; simplest_elim false_t] + end -let convert_to_goal_tac c t1 t2 p gls = +let refine_exact_check c gl = + let evm, _ = pf_apply e_type_of gl c in + Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl + +let convert_to_goal_tac c t1 t2 p = + Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let sort = Termops.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 sort = + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl + in + let neweq= new_app_global _eq [|sort;tt1;tt2|] in + let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in + let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl 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 endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + Tacticals.New.tclTHENS (neweq (assert_before (Name e))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + end -let convert_to_hyp_tac c1 t1 c2 t2 p gls = +let convert_to_hyp_tac c1 t1 c2 t2 p = + Proofview.Goal.nf_enter begin fun gl -> let tt2=constr_of_term t2 in - let h=pf_get_new_id (id_of_string "H") gls in + let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in let false_t=mkApp (c2,[|mkVar h|]) in - tclTHENS (assert_tac (Name h) tt2) + Tacticals.New.tclTHENS (assert_before (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 = Termops.refresh_universes (pf_type_of gls t1) in - let concl=pf_concl gls in - let outsort = mkType (Termops.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 (Termops.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 + simplest_elim false_t] + end + +let discriminate_tac (cstr,u as cstru) p = + Proofview.Goal.nf_enter begin fun gl -> + let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in + let intype = + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl + in + let concl = Proofview.Goal.concl gl in + (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) + (* let outsort = mkSort outsort in *) + let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) + (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) + let identity = Universes.constr_of_global _I in + (* let trivial=pf_type_of gls identity in *) + let trivial = Universes.constr_of_global _True in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in + let outtype = mkSort outtype in + let pred=mkLambda(Name xid,outtype,mkRel 1) in + let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in + let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in + let injt=app_global _f_equal + [|intype;outtype;proj;t1;t2;mkVar hid|] in + let endt k = + injt (fun injt -> + app_global _eq_rect + [|outtype;trivial;pred;identity;concl;injt|] k) in + let neweq=new_app_global _eq [|intype;t1;t2|] in + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) + (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) + end (* 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 dummy_args = List.rev (List.init pac.arity meta) 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 + applistc (mkConstructU cinfo.ci_constr) all_args + +let cc_tactic depth additionnal_terms = + Proofview.Goal.nf_enter begin fun gl -> + Coqlib.check_required_library Coqlib.logic_module_name; + let _ = debug (Pp.str "Reading subgoal ...") in + let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in + let _ = debug (Pp.str "Problem built, solving ...") in + let sol = execute true state in + let _ = debug (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 \ + None -> Tacticals.New.tclFAIL 0 (str "congruence failed") + | Some reason -> + debug (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 + | Incomplete -> + let env = Proofview.Goal.env gl in + 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.msg_info + (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 "(") - (Termops.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 - + Pp.msg_info + (Pp.str " Try " ++ + hov 8 + begin + str "\"congruence with (" ++ + prlist_with_sep + (fun () -> str ")" ++ spc () ++ str "(") + (Termops.print_constr_env env) + terms_to_complete ++ + str ")\"," + end ++ + Pp.str " replacing metavariables by arbitrary terms."); + Tacticals.New.tclFAIL 0 (str "Incomplete") + | 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 + | Hyp id -> refute_tac id ta tb p + | HeqG id -> + convert_to_goal_tac id ta tb p + | HeqnH (ida,idb) -> + convert_to_hyp_tac ida ta idb tb p + end 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 + Tacticals.New.tclORELSE + (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) + (Proofview.V82.tactic 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. @@ -453,22 +477,35 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal) the fact that congruence is called internally. *) -let f_equal gl = - let cut_eq c1 c2 = - let ty = Termops.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 f_equal = + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let type_of = Tacmach.New.pf_type_of gl in + let cut_eq c1 c2 = + try (* type_of can raise an exception *) + let ty = (* Termops.refresh_universes *) (type_of c1) in + if eq_constr_nounivs c1 c2 then Proofview.tclUNIT () + else + Tacticals.New.tclTRY (Tacticals.New.tclTHEN + ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + in + Proofview.tclORELSE + begin match kind_of_term concl with + | App (r,[|_;t;t'|]) when Globnames.is_global _eq r -> + begin match kind_of_term t, kind_of_term t' with + | App (f,v), App (f',v') when Int.equal (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 + if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 []) + else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1)) + in cuts (Array.length v - 1) + | _ -> Proofview.tclUNIT () + end + | _ -> Proofview.tclUNIT () + end + begin function (e, info) -> match e with + | Type_errors.TypeError _ -> Proofview.tclUNIT () + | e -> Proofview.tclZERO ~info e + end + end diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index 60a1b2ec..7c1d9f1c 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -1,6 +1,7 @@ + (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Proof_type.tactic +val proof_tac: Ccproof.proof -> unit Proofview.tactic -val cc_tactic : int -> constr list -> tactic +val cc_tactic : int -> constr list -> unit Proofview.tactic val cc_fail : tactic -val congruence_tac : int -> constr list -> tactic +val congruence_tac : int -> constr list -> unit Proofview.tactic -val f_equal : tactic +val f_equal : unit Proofview.tactic diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 8b3fe770..aa31c6f0 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -1,16 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*