diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-12 13:06:13 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-12 13:06:13 +0200 |
commit | 3bc69bf3d5a88a9ed948d14f9b069f9efd4cdce9 (patch) | |
tree | 6e44118d804b4d58eb0bb9243edc3e67cdf08210 | |
parent | 52c583660d3d7aa5eddf209632a46276ff9e4236 (diff) | |
parent | 0ca486fad19fc3da5160148ee4bce72b1e39ded3 (diff) |
Merge PR #7087: Congruence tactic engine update
-rw-r--r-- | plugins/cc/ccalgo.ml | 48 | ||||
-rw-r--r-- | proofs/goal.ml | 14 | ||||
-rw-r--r-- | proofs/goal.mli | 3 | ||||
-rw-r--r-- | test-suite/success/cc.v | 14 |
4 files changed, 29 insertions, 50 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 5a4818926..8e53a044d 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -9,7 +9,7 @@ (************************************************************************) (* This file implements the basic congruence-closure algorithm by *) -(* Downey,Sethi and Tarjan. *) +(* Downey, Sethi and Tarjan. *) (* Plus some e-matching and constructor handling by P. Corbineau *) open CErrors @@ -18,7 +18,6 @@ open Names open Sorts open Constr open Vars -open Evd open Goptions open Tacmach open Util @@ -272,7 +271,8 @@ type state = mutable rew_depth:int; mutable changed:bool; by_type: Int.Set.t Typehash.t; - mutable gls:Goal.goal Evd.sigma} + mutable env:Environ.env; + sigma:Evd.evar_map} let dummy_node = { @@ -307,7 +307,8 @@ let empty depth gls:state = rew_depth=depth; by_type=Constrhash.create init_size; changed=false; - gls=gls + env=pf_env gls; + sigma=project gls } let forest state = state.uf @@ -426,7 +427,7 @@ let cc_product s1 s2 = mkLambda(_B_,mkSort(s2),_body_)) let rec constr_of_term = function - Symb s-> applist_projection s [] + Symb s-> s | Product(s1,s2) -> cc_product s1 s2 | Eps id -> mkVar id | Constructor cinfo -> mkConstructU cinfo.ci_constr @@ -434,25 +435,7 @@ let rec constr_of_term = function make_app [(constr_of_term s2)] s1 and make_app l=function Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 - | other -> - applist_proj other l -and applist_proj c l = - match c with - | Symb s -> applist_projection s l - | _ -> Term.applistc (constr_of_term c) l -and applist_projection c l = - match Constr.kind 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_in (Global.env ()) c in (* FIXME constraints *) - let pb = Environ.lookup_projection p (Global.env()) in - let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx - | hd :: tl -> - Term.applistc (mkProj (p, hd)) tl) - | _ -> Term.applistc c l + | other -> Term.applist (constr_of_term other,l) let rec canonize_name sigma c = let c = EConstr.Unsafe.to_constr c in @@ -511,8 +494,8 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in - let typ = canonize_name (project state.gls) typ in + let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in + let typ = canonize_name state.sigma typ in let new_node= match t with Symb _ | Product (_,_) -> @@ -820,11 +803,10 @@ let one_step state = let __eps__ = Id.of_string "_eps_" let new_state_var typ state = - let id = pf_get_new_id __eps__ state.gls in - let {it=gl ; sigma=sigma} = state.gls in - let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in - state.gls<- gls; - id + let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in + let id = Namegen.next_ident_away __eps__ ids in + state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env; + id let complete_one_class state i= match (get_representative state.uf i).inductive_status with @@ -832,9 +814,9 @@ let complete_one_class state i= 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 + let id = new_state_var (EConstr.of_constr etyp) state in app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = pf_unsafe_type_of state.gls + let _c = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in let _c = EConstr.Unsafe.to_constr _c in let _args = diff --git a/proofs/goal.ml b/proofs/goal.ml index ba7e458f3..6912db364 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -117,20 +117,6 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl extra_hyps = - let evi = Evd.find sigma gl in - let hyps = evi.Evd.evar_hyps in - let new_hyps = - List.fold_right Environ.push_named_context_val extra_hyps hyps in - let filter = evi.Evd.evar_filter in - let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in - let new_evi = - { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in - let new_evi = Typeclasses.mark_unresolvable new_evi in - let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = sigma; } - (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = let evi = Evd.find sigma gl in diff --git a/proofs/goal.mli b/proofs/goal.mli index dc9863156..b8c979ad7 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -64,9 +64,6 @@ module V82 : sig (* Principal part of tclNOTSAMEGOAL *) val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool - (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma - (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index bbfe5ec42..49a8b9cf4 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -151,3 +151,17 @@ Section JLeivant. congruence. Qed. End JLeivant. + +(* An example with primitive projections *) + +Module PrimitiveProjections. +Set Primitive Projections. +Record t (A:Type) := { f : A }. +Goal forall g (a:t nat), @f nat = g -> f a = 0 -> g a = 0. +congruence. +Undo. +intros. +unfold f in H0. (* internally turn the projection to unfolded form *) +congruence. +Qed. +End PrimitiveProjections. |