From 17564e4922acda6b72bf39de7a8c23ed0c0178f6 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Sat, 23 Jul 2016 16:21:44 -0400 Subject: Imported Upstream version 8.5.1 --- .gitignore | 2 - AAC.v | 1 + CHANGELOG | 5 -- Caveats.v | 3 - Instances.v | 31 ++++---- Make | 21 ++++++ Makefile | 38 +++------- README | 55 ++++++++++++++ README.txt | 75 ------------------- Tutorial.v | 33 --------- aac.mlpack | 1 - coq.ml | 60 ++++++++------- coq.mli | 6 +- description | 15 ++++ evm_compute.ml | 221 -------------------------------------------------------- evm_compute.mli | 11 --- files.txt | 11 --- matcher.ml | 2 +- print.ml | 4 +- print.mli | 2 +- rewrite.ml4 | 95 +++++++----------------- rewrite.mli | 9 +++ theory.ml | 88 +++++++++++++++++----- theory.mli | 2 +- 24 files changed, 265 insertions(+), 526 deletions(-) delete mode 100644 .gitignore create mode 100644 Make create mode 100644 README delete mode 100644 README.txt mode change 100644 => 100755 coq.ml create mode 100644 description delete mode 100644 evm_compute.ml delete mode 100644 evm_compute.mli delete mode 100644 files.txt create mode 100644 rewrite.mli diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 50cfd07..0000000 --- a/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -doc -html diff --git a/AAC.v b/AAC.v index a16f1a0..f6f382f 100644 --- a/AAC.v +++ b/AAC.v @@ -33,6 +33,7 @@ Require Import RelationClasses Equality. Require Export Morphisms. Set Implicit Arguments. +Set Asymmetric Patterns. Local Open Scope signature_scope. diff --git a/CHANGELOG b/CHANGELOG index 13e9a02..84b2aae 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,8 +1,3 @@ - -AAC_tactics 0.3 : ------------------ -- New release for Coq 8.4 - AAC_tactics 0.2-pl2 : ----------------- diff --git a/Caveats.v b/Caveats.v index d0ec37a..a7967cc 100644 --- a/Caveats.v +++ b/Caveats.v @@ -13,7 +13,6 @@ with the path to the [aac_tactics] library *) -Add Rec LoadPath "." as AAC_tactics. Require Import AAC. Require Instances. @@ -371,5 +370,3 @@ to investigate on this in the future *) End Z. - - diff --git a/Instances.v b/Instances.v index 8ddf9e4..55dffbb 100644 --- a/Instances.v +++ b/Instances.v @@ -6,6 +6,11 @@ (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) +Require List. +Require Arith NArith Max Min. +Require ZArith Zminmax. +Require QArith Qminmax. +Require Relations. Require Export AAC. @@ -19,7 +24,7 @@ Proof. intros x y ->. reflexivity. Qed. (* At the moment, all the instances are exported even if they are packaged into modules. Even using LocalInstances in fact*) Module Peano. - Require Import Arith NArith Max Min. + Import Arith NArith Max Min. Instance aac_plus_Assoc : Associative eq plus := plus_assoc. Instance aac_plus_Comm : Commutative eq plus := plus_comm. @@ -38,14 +43,14 @@ Module Peano. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder le := Build_PreOrder _ _ le_refl le_trans. + Instance preorder_le : PreOrder le := Build_PreOrder _ le_refl le_trans. Instance lift_le_eq : AAC_lift le eq := Build_AAC_lift eq_equivalence _. End Peano. Module Z. - Require Import ZArith Zminmax. + Import ZArith Zminmax. Open Scope Z_scope. Instance aac_Zplus_Assoc : Associative eq Zplus := Zplus_assoc. Instance aac_Zplus_Comm : Commutative eq Zplus := Zplus_comm. @@ -63,13 +68,13 @@ Module Z. Instance aac_zero_Zplus : Unit eq Zplus 0 := Build_Unit eq Zplus 0 Zplus_0_l Zplus_0_r. (* We also provide liftings from le to eq *) - Instance preorder_Zle : PreOrder Zle := Build_PreOrder _ _ Zle_refl Zle_trans. + Instance preorder_Zle : PreOrder Zle := Build_PreOrder _ Zle_refl Zle_trans. Instance lift_le_eq : AAC_lift Zle eq := Build_AAC_lift eq_equivalence _. End Z. Module Lists. - Require Import List. + Import List. Instance aac_append_Assoc {A} : Associative eq (@app A) := @app_assoc A. Instance aac_nil_append {A} : @Unit (list A) eq (@app A) (@nil A) := Build_Unit _ (@app A) (@nil A) (@app_nil_l A) (@app_nil_r A). Instance aac_append_Proper {A} : Proper (eq ==> eq ==> eq) (@app A). @@ -82,7 +87,7 @@ End Lists. Module N. - Require Import NArith. + Import NArith. Open Scope N_scope. Instance aac_Nplus_Assoc : Associative eq Nplus := Nplus_assoc. Instance aac_Nplus_Comm : Commutative eq Nplus := Nplus_comm. @@ -101,13 +106,13 @@ Module N. Instance aac_zero_max : Unit eq Nmax 0 := Build_Unit eq Nmax 0 N.max_0_l N.max_0_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.le_refl N.le_trans. + Instance preorder_le : PreOrder Nle := Build_PreOrder Nle N.le_refl N.le_trans. Instance lift_le_eq : AAC_lift Nle eq := Build_AAC_lift eq_equivalence _. End N. Module P. - Require Import NArith. + Import NArith. Open Scope positive_scope. Instance aac_Pplus_Assoc : Associative eq Pplus := Pplus_assoc. Instance aac_Pplus_Comm : Commutative eq Pplus := Pplus_comm. @@ -126,12 +131,12 @@ Module P. Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 Pos.max_1_l Pos.max_1_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple Pos.le_refl Pos.le_trans. + Instance preorder_le : PreOrder Ple := Build_PreOrder Ple Pos.le_refl Pos.le_trans. Instance lift_le_eq : AAC_lift Ple eq := Build_AAC_lift eq_equivalence _. End P. Module Q. - Require Import QArith Qminmax. + Import QArith Qminmax. Instance aac_Qplus_Assoc : Associative Qeq Qplus := Qplus_assoc. Instance aac_Qplus_Comm : Commutative Qeq Qplus := Qplus_comm. @@ -148,7 +153,7 @@ Module Q. Instance aac_zero_Qplus : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Qle_refl Qle_trans. + Instance preorder_le : PreOrder Qle := Build_PreOrder Qle Qle_refl Qle_trans. Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _. End Q. @@ -162,7 +167,7 @@ Module Prop_ops. Instance aac_False : Unit iff and True. Proof. constructor; firstorder. Qed. Program Instance aac_not_compat : Proper (iff ==> iff) not. - Solve All Obligations using firstorder. + Solve All Obligations with firstorder. Instance lift_impl_iff : AAC_lift Basics.impl iff := Build_AAC_lift _ _. End Prop_ops. @@ -179,7 +184,7 @@ Module Bool. End Bool. Module Relations. - Require Import Relations. + Import Relations.Relations. Section defs. Variable T : Type. Variables R S: relation T. diff --git a/Make b/Make new file mode 100644 index 0000000..8caf805 --- /dev/null +++ b/Make @@ -0,0 +1,21 @@ +-I . +-R . AAC_tactics +coq.mli +helper.mli +search_monad.mli +matcher.mli +theory.mli +print.mli +rewrite.mli +coq.ml +helper.ml +search_monad.ml +matcher.ml +theory.ml +print.ml +rewrite.ml4 +aac.mlpack +AAC.v +Instances.v +Tutorial.v +Caveats.v diff --git a/Makefile b/Makefile index 03775bc..a9d5466 100644 --- a/Makefile +++ b/Makefile @@ -1,34 +1,14 @@ - - -FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli \ - evm_compute.mli evm_compute.ml \ - coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \ - aac.mlpack \ - AAC.v Instances.v Tutorial.v Caveats.v - -ARGS := -R . AAC_tactics - -.PHONY: coq clean doc - -world: all doc - all: Makefile.coq - $(MAKE) -f Makefile.coq all - -install: Makefile.coq - $(MAKE) -f Makefile.coq install - -coq: Makefile.coq - $(MAKE) -f Makefile.coq + +make -f Makefile.coq all -doc: Makefile.coq - $(MAKE) -f Makefile.coq html - $(MAKE) -f Makefile.coq mlihtml +clean: Makefile.coq + +make -f Makefile.coq clean + rm -f Makefile.coq -Makefile.coq: Makefile $(VS) - coq_makefile $(ARGS) $(FILES) -o Makefile.coq +Makefile.coq: Make + $(COQBIN)coq_makefile -f Make -o Makefile.coq -clean:: Makefile.coq - $(MAKE) -f Makefile.coq clean - rm -f Makefile.coq .depend +%: Makefile.coq + +make -f Makefile.coq $@ +.PHONY: all clean diff --git a/README b/README new file mode 100644 index 0000000..38fc514 --- /dev/null +++ b/README @@ -0,0 +1,55 @@ + + aac_tactics + =========== + + Thomas Braibant & Damien Pous + +Laboratoire d'Informatique de Grenoble (UMR 5217), INRIA, CNRS, France + + +FOREWORD +======== + +This plugin provides tactics for rewriting universally quantified +equations, modulo associativity and commutativity of some operators. + +INSTALLATION +============ + +opam repo add coq-released https://coq.inria.fr/opam/released +opam install coq-aac-tactics + +DOCUMENTATION +============= + +Please refer to Tutorial.v for a succinct introduction on how to use +this plugin. + +To understand the inner-working of the tactic, please refer to the +.mli files as the main source of information on each .ml +file. Alternatively, [make world] generates ocamldoc/coqdoc +documentation in directories doc/ and html/, respectively. + +File Instances.v defines several instances for frequent use-cases of +this plugin, that should allow you to use it out-of-the-shelf. Namely, +we have instances for: + +- Peano naturals (Import Instances.Peano) +- Z binary numbers (Import Instances.Z) +- N binary numbers (Import Instances.N) +- P binary numbers (Import Instances.P) +- Rationnal numbers (Import Instances.Q) +- Prop (Import Instances.Prop_ops) +- Booleans (Import Instances.Bool) +- Relations (Import Instances.Relations) +- All of the above (Import Instances.All) + + +ACKNOWLEDGEMENTS +================ + +We are grateful to Evelyne Contejean, Hugo Herbelin, Assia Mahboubi +and Matthieu Sozeau for highly instructive discussions. + +This plugin took inspiration from the plugin tutorial "constructors", +distributed under the LGPL 2.1, copyrighted by Matthieu Sozeau diff --git a/README.txt b/README.txt deleted file mode 100644 index d308f70..0000000 --- a/README.txt +++ /dev/null @@ -1,75 +0,0 @@ - - aac_tactics - =========== - - Thomas Braibant & Damien Pous - -Laboratoire d'Informatique de Grenoble (UMR 5217), INRIA, CNRS, France - -Webpage of the project: http://sardes.inrialpes.fr/~braibant/aac_tactics/ - - -FOREWORD -======== - -This plugin provides tactics for rewriting universally quantified -equations, modulo associativity and commutativity of some operators. - -INSTALLATION -============ - -This plugin should work with Coq v8.4 - -- running [make] in the top-level directory will generate a Makefile - (using coq_makefile), and will build the plugin and its documentation - -Option 1 --------- -To install the plugin in Coq's directory, as, e.g., omega or ring. - -- run [sudo make install CMXSFILES='aac_tactics.cmxs aac_tactics.cma'] - to copy the relevant files of the plugin - -Option 2 --------- - -If you chose not to use the previous option, you will need to add the -following lines to (all) your .v files to be able to use the plugin: - -Add Rec LoadPath "absolute_path_to_aac_tactics". -Add ML Path "absolute_path_to_aac_tactics". - -DOCUMENTATION -============= - -Please refer to Tutorial.v for a succinct introduction on how to use -this plugin. - -To understand the inner-working of the tactic, please refer to the -.mli files as the main source of information on each .ml -file. Alternatively, [make world] generates ocamldoc/coqdoc -documentation in directories doc/ and html/, respectively. - -File Instances.v defines several instances for frequent use-cases of -this plugin, that should allow you to use it out-of-the-shelf. Namely, -we have instances for: - -- Peano naturals (Import Instances.Peano) -- Z binary numbers (Import Instances.Z) -- N binary numbers (Import Instances.N) -- P binary numbers (Import Instances.P) -- Rationnal numbers (Import Instances.Q) -- Prop (Import Instances.Prop_ops) -- Booleans (Import Instances.Bool) -- Relations (Import Instances.Relations) -- All of the above (Import Instances.All) - - -ACKNOWLEDGEMENTS -================ - -We are grateful to Evelyne Contejean, Hugo Herbelin, Assia Mahboubi -and Matthieu Sozeau for highly instructive discussions. - -This plugin took inspiration from the plugin tutorial "constructors", -distributed under the LGPL 2.1, copyrighted by Matthieu Sozeau diff --git a/Tutorial.v b/Tutorial.v index 6356a10..76006ca 100644 --- a/Tutorial.v +++ b/Tutorial.v @@ -397,36 +397,3 @@ Section Examples. End Examples. -Section Match. - (* The following example is inspired by a question by Francois - Pottier, wokring in the context of separation logic. *) - - Variable T : Type. - Variable star : T -> T -> T. - Hypothesis P : T -> Prop. - - Context (starA : Associative eq star). - Context (starC : Commutative eq star). - - Hypothesis P_hereditary_left : forall a b, P (star a b) -> P a. - Hypothesis P_hereditary_right : forall a b, P (star a b) -> P b. - - Notation "a * b" := (star a b). - - Ltac crush := - match goal with - H: P ?R' |- P ?R => - let h := fresh in - aac_match (fun x => x * R) R' h; - rewrite <- h in H; - try eauto using P_hereditary_right - end. - - Goal forall a b c, P (c * a * c * b) -> P (b * a). - Proof. intros. crush. Qed. - - Goal forall a b c, exists d, P (d * a * c * b) -> P (b * d) /\ b = d. - Proof. intros. eexists. intros. split. crush. reflexivity. Qed. - -End Match. - diff --git a/aac.mlpack b/aac.mlpack index 60d5298..0c12567 100644 --- a/aac.mlpack +++ b/aac.mlpack @@ -4,5 +4,4 @@ Search_monad Matcher Theory Print -Evm_compute Rewrite diff --git a/coq.ml b/coq.ml old mode 100644 new mode 100755 index 132fbf7..97154e2 --- a/coq.ml +++ b/coq.ml @@ -19,17 +19,21 @@ let contrib_name = "aac_tactics" (* Getting constrs (primitive Coq terms) from existing Coq libraries. *) let find_constant contrib dir s = - Libnames.constr_of_global (Coqlib.find_reference contrib dir s) + Universes.constr_of_global (Coqlib.find_reference contrib dir s) let init_constant dir s = find_constant contrib_name dir s (* A clause specifying that the [let] should not try to fold anything in the goal *) let nowhere = - { Tacexpr.onhyps = Some []; - Tacexpr.concl_occs = Glob_term.no_occurrences_expr + { Locus.onhyps = Some []; + Locus.concl_occs = Locus.NoOccurrences } +let retype c gl = + let sigma, _ = Tacmach.pf_apply Typing.type_of gl c in + Refiner.tclEVARS sigma gl + let cps_mk_letin (name:string) (c: constr) @@ -38,20 +42,20 @@ let cps_mk_letin fun goal -> let name = (Names.id_of_string name) in let name = Tactics.fresh_id [] name goal in - let letin = (Tactics.letin_tac None (Name name) c None nowhere) in - Tacticals.tclTHEN letin (k (mkVar name)) goal + let letin = (Proofview.V82.of_tactic (Tactics.letin_tac None (Name name) c None nowhere)) in + Tacticals.tclTHENLIST [retype c; letin; (k (mkVar name))] goal (** {2 General functions} *) type goal_sigma = Proof_type.goal Tacmach.sigma let goal_update (goal : goal_sigma) evar_map : goal_sigma= let it = Tacmach.sig_it goal in - Tacmach.re_sig it evar_map + Tacmach.re_sig it evar_map let fresh_evar goal ty : constr * goal_sigma = let env = Tacmach.pf_env goal in let evar_map = Tacmach.project goal in - let (em,x) = Evarutil.new_evar evar_map env ty in + let (em,x) = Evarutil.new_evar env evar_map ty in x,( goal_update goal em) let resolve_one_typeclass goal ty : constr*goal_sigma= @@ -69,8 +73,8 @@ let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr -> Proof_type try Typeclasses.resolve_one_typeclass env em t with Not_found -> begin match error with - | None -> Util.anomaly "Cannot resolve a typeclass : please report" - | Some x -> Util.error x + | None -> Errors.anomaly (Pp.str "Cannot resolve a typeclass : please report") + | Some x -> Errors.error x end in Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal @@ -84,28 +88,28 @@ let nf_evar goal c : Term.constr= let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma = let env = Tacmach.pf_env gl in let evar_map = Tacmach.project gl in - let (em,x) = Evarutil.new_evar evar_map env x in + let (em,x) = Evarutil.new_evar env evar_map x in x,(goal_update gl em) let evar_binary (gl: goal_sigma) (x : constr) = let env = Tacmach.pf_env gl in let evar_map = Tacmach.project gl in let ty = mkArrow x (mkArrow x x) in - let (em,x) = Evarutil.new_evar evar_map env ty in + let (em,x) = Evarutil.new_evar env evar_map ty in x,( goal_update gl em) let evar_relation (gl: goal_sigma) (x: constr) = let env = Tacmach.pf_env gl in let evar_map = Tacmach.project gl in let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in - let (em,r) = Evarutil.new_evar evar_map env ty in + let (em,r) = Evarutil.new_evar env evar_map ty in r,( goal_update gl em) let cps_evar_relation (x: constr) k = fun goal -> Tacmach.pf_apply (fun env em -> let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in - let (em,r) = Evarutil.new_evar em env ty in + let (em,r) = Evarutil.new_evar env em ty in Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal ) goal @@ -148,8 +152,6 @@ module Leibniz = struct let path = ["Coq"; "Init"; "Logic"] let eq_refl = lazy (init_constant path "eq_refl") let eq_refl ty x = lapp eq_refl [| ty;x|] - let eq ty = Term.mkApp (init_constant path "eq", [| ty |]) - end module Option = struct @@ -319,7 +321,7 @@ end (**[ match_as_equation goal eqt] see [eqt] as an equation. An optionnal rel_context can be provided to ensure taht the term remains typable*) -let match_as_equation ?(context = Term.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option = +let match_as_equation ?(context = Context.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option = let env = Tacmach.pf_env goal in let env = Environ.push_rel_context context env in let evar_map = Tacmach.project goal in @@ -330,7 +332,7 @@ let match_as_equation ?(context = Term.empty_rel_context) goal equation : (const let left = ca.(n-2) in let right = ca.(n-1) in let r = (mkApp (c, Array.sub ca 0 (n - 2))) in - let carrier = Typing.type_of env evar_map left in + let carrier = Typing.unsafe_type_of env evar_map left in let rlt =Std.Relation.make carrier r in Some (left, right, rlt ) @@ -359,10 +361,10 @@ let tclPRINT tac = fun gl -> (* functions to handle the failures of our tactic. Some should be reported [anomaly], some are on behalf of the user [user_error]*) let anomaly msg = - Util.anomaly ("[aac_tactics] " ^ msg) + Errors.anomaly ~label:"[aac_tactics]" (Pp.str msg) let user_error msg = - Util.error ("[aac_tactics] " ^ msg) + Errors.error ("[aac_tactics] " ^ msg) let warning msg = Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg)) @@ -382,7 +384,7 @@ type hypinfo = { hyp : Term.constr; (** the actual constr corresponding to the hypothese *) hyptype : Term.constr; (** the type of the hypothesis *) - context : Term.rel_context; (** the quantifications of the hypothese *) + context : Context.rel_context; (** the quantifications of the hypothese *) body : Term.constr; (** the body of the type of the hypothesis*) rel : Std.Relation.t; (** the relation *) left : Term.constr; (** left hand side *) @@ -391,12 +393,12 @@ type hypinfo = } let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proof_type.tactic = fun goal -> - let ctype = Tacmach.pf_type_of goal c in + let ctype = Tacmach.pf_unsafe_type_of goal c in let (rel_context, body_type) = Term.decompose_prod_assum ctype in let rec check f e = match decomp_term e with | Term.Rel i -> - let name, constr_option, types = Term.lookup_rel i rel_context + let name, constr_option, types = Context.lookup_rel i rel_context in f types | _ -> Term.fold_constr (fun acc x -> acc && check f x) true e in @@ -441,7 +443,7 @@ let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proo (* Fresh evars for everyone (should be the good way to do this recompose in Coq v8.4) *) let recompose_prod - (context : Term.rel_context) + (context : Context.rel_context) (subst : (int * Term.constr) list) env em @@ -462,7 +464,7 @@ let recompose_prod let em,x = try em, List.assoc n subst with | Not_found -> - Evarutil.new_evar em env (Term.substl acc ty) + Evarutil.new_evar env em (Vars.substl acc ty) in (Environ.push_rel t env), em,x::acc else @@ -475,7 +477,7 @@ let recompose_prod application to handle non-instanciated variables. *) let recompose_prod' - (context : Term.rel_context) + (context : Context.rel_context) (subst : (int *Term.constr) list) c = @@ -506,7 +508,7 @@ let recompose_prod' | None :: sign, _ :: app -> None :: update sign (List.map (Termops.pop) app) | Some decl :: sign, _ :: app -> - Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app) + Some (Vars.substl_decl app decl)::update sign (List.map (Termops.pop) app) in let ctxt = update ctxt app in (* updates the rel accordingly, taking some care not to go to far @@ -576,13 +578,15 @@ let rewrite ?(abort=false)hypinfo subst k = (fun rew -> let tac = if not abort then + Proofview.V82.of_tactic begin Equality.general_rewrite_bindings hypinfo.l2r - Termops.all_occurrences + Locus.AllOccurrences true (* tell if existing evars must be frozen for instantiation *) false - (rew,Glob_term.NoBindings) + (rew,Misctypes.NoBindings) true + end else Tacticals.tclIDTAC in k tac diff --git a/coq.mli b/coq.mli index 53d42eb..1004d2c 100644 --- a/coq.mli +++ b/coq.mli @@ -40,6 +40,7 @@ val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Pro (** [cps_mk_letin name v] binds the constr [v] using a letin tactic *) val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val retype : Term.constr -> Proof_type.tactic val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term val lapp : Term.constr lazy_t -> Term.constr array -> Term.constr @@ -79,7 +80,6 @@ end module Leibniz : sig val eq_refl : Term.types -> Term.constr -> Term.constr - val eq : Term.types -> Term.constr end module Option : sig @@ -149,7 +149,7 @@ end (** [match_as_equation ?context goal c] try to decompose c as a relation applied to two terms. An optionnal rel_context can be provided to ensure that the term remains typable *) -val match_as_equation : ?context:Term.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option +val match_as_equation : ?context:Context.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option (** {2 Some tacticials} *) @@ -190,7 +190,7 @@ type hypinfo = { hyp : Term.constr; (** the actual constr corresponding to the hypothese *) hyptype : Term.constr; (** the type of the hypothesis *) - context : Term.rel_context; (** the quantifications of the hypothese *) + context : Context.rel_context; (** the quantifications of the hypothese *) body : Term.constr; (** the body of the hypothese*) rel : Relation.t; (** the relation *) left : Term.constr; (** left hand side *) diff --git a/description b/description new file mode 100644 index 0000000..7b7195d --- /dev/null +++ b/description @@ -0,0 +1,15 @@ +Name: AACTactics +Title: AAC tactics +Description: This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators: +Keywords: reflexive tactic, rewriting, rewriting modulo associativity and commutativity, rewriting modulo AC, reflexive decision procedure +Category: Miscellaneous/Coq Extensions +Author: Thomas Braibant +Email: thomas.braibant@gmail.com +Homepage: http://sardes.inrialpes.fr/~braibant/ +Institution: INRIA/UJF/Ens Lyon +Author: Damien Pous +Email: damien.pous@inria.fr +Homepage: http://sardes.inrialpes.fr/~pous/ +Institution: CNRS +Require: +License: LGPL diff --git a/evm_compute.ml b/evm_compute.ml deleted file mode 100644 index b10a9cd..0000000 --- a/evm_compute.ml +++ /dev/null @@ -1,221 +0,0 @@ -(*i camlp4deps: "parsing/grammar.cma" i*) -(*i camlp4use: "pa_extend.cmp" i*) - - -let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x) -let pp_list pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a; " pp x) l -let pp_list_nl pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a;\n" pp x) l -let pp_constrs fmt l = (pp_list pp_constr) fmt l - -type constr = Term.constr - -module Replace (X : sig val eq: Term.constr -> Term.constr -> bool - val subst : (Term.constr * Term.constr) list end) = - struct - - (* assumes that [c] and [t] have no outer casts, and all - applications have been flattened *) - let rec find l (t: constr) = - match l with - | [] -> None - | (c,c') :: q -> - begin - match Term.kind_of_term c, Term.kind_of_term t with - | Term.App (f1,args1), Term.App (f2, args2) -> - let l1 = Array.length args1 in - let l2 = Array.length args2 in - if l1 <= l2 && X.eq c (Term.mkApp (f2, Array.sub args2 0 l1)) - then - (* we must return the array of arguments, to make the - substitution in them too *) - Some (c',Array.sub args2 l1 (l2 - l1)) - else - find q t - | _, _ -> - if X.eq c t - then Some (c', [| |]) - else find q t - end - - - let replace_terms t = - let rec aux (k:int) t = - match find X.subst t with - | Some (t',v) -> - let v' = Array.map (Term.map_constr_with_binders (succ) aux k) v in - Term.mkApp (Term.lift k t', v') - | None -> - Term.map_constr_with_binders succ aux k t - in aux 0 t - - end - -let nowhere = - { Tacexpr.onhyps = Some []; - Tacexpr.concl_occs = Glob_term.no_occurrences_expr - } - -let mk_letin - (name:string) - (c: constr) - (k : Names .identifier -> Proof_type.tactic) -: Proof_type.tactic = - fun goal -> - let name = (Names.id_of_string name) in - let name = Tactics.fresh_id [] name goal in - let letin = (Tactics.letin_tac None (Names.Name name) c None nowhere) in - Tacticals.tclTHEN letin (k name) goal - -let assert_tac - (name:string) - (c: constr) - (by:Proof_type.tactic) - (k : Names.identifier -> Proof_type.tactic) -: Proof_type.tactic = - fun goal -> - let name = (Names.id_of_string name) in - let name = Tactics.fresh_id [] name goal in - let t = (Tactics.assert_tac (Names.Name name) c) in - Tacticals.tclTHENS t [by; (k name)] goal - - -(* The contrib name is used to locate errors when loading constrs *) -let contrib_name = "evm_compute" - -(* Getting constrs (primitive Coq terms) from existing Coq - libraries. *) -let find_constant contrib dir s = - Libnames.constr_of_global (Coqlib.find_reference contrib dir s) - -let init_constant dir s = find_constant contrib_name dir s - -module Leibniz = struct - let path = ["Coq"; "Init"; "Logic"] - - let eq_refl t x= - Term.mkApp (init_constant path "eq_refl", [| t; x|]) - - let eq t x y = - Term.mkApp (init_constant path "eq", [| t; x ; y|]) - - let eq_ind_r ty x p px y yx = - Term.mkApp (init_constant path "eq_ind_r", [|ty;x;p;px;y;yx|]) -end - -let mk_vm_cast t c = Term.mkCast (c,Term.VMcast,t) - -let mk_let - (name:Names.identifier) - (c: constr) - (t: constr) - (k : Names.identifier -> constr) = - Term.mkNamedLetIn name c t (Term.subst_vars [name] (k name)) - -let mk_fun - (name:Names.identifier) - (t: constr) - (k : Names.identifier -> constr) = - Term.mkNamedLambda name t (Term.subst_vars [name] (k name)) - -let rec has_evar x = - match Term.kind_of_term x with - | Term.Evar _ -> true - | Term.Rel _ | Term.Var _ | Term.Meta _ | Term.Sort _ | Term.Const _ | Term.Ind _ | Term.Construct _ -> - false - | Term.Cast (t1, _, t2) | Term.Prod (_, t1, t2) | Term.Lambda (_, t1, t2) -> - has_evar t1 || has_evar t2 - | Term.LetIn (_, t1, t2, t3) -> - has_evar t1 || has_evar t2 || has_evar t3 - | Term.App (t1, ts) -> - has_evar t1 || has_evar_array ts - | Term.Case (_, t1, t2, ts) -> - has_evar t1 || has_evar t2 || has_evar_array ts - | Term.Fix ((_, tr)) | Term.CoFix ((_, tr)) -> - has_evar_prec tr -and has_evar_array x = - Util.array_exists has_evar x -and has_evar_prec (_, ts1, ts2) = - Util.array_exists has_evar ts1 || Util.array_exists has_evar ts2 - -let evm_compute eq blacklist = fun gl -> - (* the type of the conclusion of the goal is [concl] *) - let concl = Tacmach.pf_concl gl in - - let extra = - List.fold_left (fun acc (id,body,ty) -> - match body with - | None -> acc - | Some body -> if has_evar body then (Term.mkVar id :: acc) else acc) - [] (Tacmach.pf_hyps gl) in - - (* the set of evars that appear in the goal *) - let evars = Evd.evar_list (Tacmach.project gl) concl in - - (* the arguments of the function are: the constr that are blacklisted, then the evars *) - let args = extra @ blacklist @ (List.map (fun x -> Term.mkEvar x) evars) in - - let argsv = Array.of_list args in - - let context = (Termops.rel_list 0 (List.length args)) in - - (* we associate to each argument the proper de bruijn index *) - let (subst: (Term.constr * Term.constr) list) = List.combine args context in - - let module R = Replace(struct let eq = eq let subst = subst end) in - - let t = R.replace_terms concl in - - (* we have to retype both the blacklist and the evars to know how to build the final product *) - let rel_context = List.map (fun x -> Names.Anonymous, None, Tacmach.pf_type_of gl x) args in - - (* the abstraction *) - let t = Term.it_mkLambda_or_LetIn t (List.rev rel_context) in - - let typeof_t = (Tacmach.pf_type_of gl t) in - - (* the normal form of the head function *) - let nft = Vnorm.cbv_vm (Tacmach.pf_env gl) t typeof_t in - - - let (!!) x = Tactics.fresh_id [] ((Names.id_of_string x)) gl in - - (* p = [fun x => x a_i] which corresponds to the type of the goal when applied to [t] *) - let p = mk_fun (!! "x") typeof_t (fun x -> Term.mkApp (Term.mkVar x,argsv)) in - - let proof_term pnft = begin - mk_let (!! "nft") nft typeof_t (fun nft -> let nft' = Term.mkVar nft in - mk_let (!! "t") t typeof_t (fun t -> let t' = Term.mkVar t in - mk_let (!! "H") (mk_vm_cast (Leibniz.eq typeof_t t' nft') (Leibniz.eq_refl typeof_t nft')) (Leibniz.eq typeof_t t' nft') - (fun h -> - (* typeof_t -> Prop *) - let body = Leibniz.eq_ind_r typeof_t - nft' p pnft t' (Term.mkVar h) - in - Term.mkCast (body, Term.DEFAULTcast, Term.mkApp (t', argsv)) - ))) - end in - - try - assert_tac "subgoal" (Term.mkApp (p,[| nft |])) - Tacticals.tclIDTAC - (fun subgoal -> - (* We use the tactic [exact_no_check]. It has two consequences: - - first, it means that in theory we could produce ill typed proof terms, that fail to type check at Qed; - - second, it means that we are able to use vm_compute and vm_compute casts, that will be checkable at Qed time when all evars have been instantiated. - *) - Tactics.exact_no_check (proof_term (Term.mkVar subgoal)) - ) gl - with - | e -> - Tacticals.tclFAIL 0 (Pp.str (Printf.sprintf "evm_compute failed with an exception %s" (Printexc.to_string e))) gl - -;; - -let evm_compute_in eq blacklist h = fun gl -> - let concl = Tacmach.pf_concl gl in - Tacticals.tclTHENLIST - [Tactics.revert [h]; - evm_compute eq (concl :: blacklist); - Tactics.introduction h - ] - gl diff --git a/evm_compute.mli b/evm_compute.mli deleted file mode 100644 index f50c0db..0000000 --- a/evm_compute.mli +++ /dev/null @@ -1,11 +0,0 @@ - - -(** [evm_compute eq blacklist] performs a vm_compute step with the - following provisos: evars can appear in the goal; terms that are - equal (modulo eq) to terms in the blacklist are abstracted - before-hand. *) -val evm_compute : (Term.constr -> Term.constr -> bool) -> Term.constr list -> Proof_type.tactic - - -(** [evm_compute eq blacklist h] performs an evm_compute step in the hypothesis h *) -val evm_compute_in : (Term.constr -> Term.constr -> bool) -> Term.constr list -> Names.identifier -> Proof_type.tactic diff --git a/files.txt b/files.txt deleted file mode 100644 index fb0b175..0000000 --- a/files.txt +++ /dev/null @@ -1,11 +0,0 @@ -AAC_coq.ml -AAC_helper.ml -AAC_search_monad.ml -AAC_matcher.ml -AAC_theory.ml -AAC_print.ml -AAC_rewrite.ml -AAC.v -Instances.v -Tutorial.v -Caveats.v diff --git a/matcher.ml b/matcher.ml index 55a64b7..2fd0517 100644 --- a/matcher.ml +++ b/matcher.ml @@ -455,7 +455,7 @@ end | Dot (s,l,r) -> Dot (s, aux l, aux r) | Var i -> begin match find t i with - | None -> Util.error "aac_tactics: instantiate failure" + | None -> Errors.error "aac_tactics: instantiate failure" | Some x -> t_of_term x end in aux x diff --git a/print.ml b/print.ml index 1ceb786..0305158 100644 --- a/print.ml +++ b/print.ml @@ -65,7 +65,7 @@ let pp_all pt : (int * Terms.t * named_env Search_monad.m) Search_monad.m -> Pp. rename the variables, and rebuilds raw Coq terms (for the context, and the terms in the environment). In order to do so, it requires the information gathered by the {!Theory.Trans} module.*) -let print rlt ir m (context : Term.rel_context) goal = +let print rlt ir m (context : Context.rel_context) goal = if Search_monad.count m = 0 then ( @@ -80,7 +80,7 @@ let print rlt ir m (context : Term.rel_context) goal = let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in let l = List.map (fun (v,t) -> - let (name,body,types) = Term.lookup_rel v context in + let (name,body,types) = Context.lookup_rel v context in (name,t) ) l in diff --git a/print.mli b/print.mli index 5b3dc15..7fab3be 100644 --- a/print.mli +++ b/print.mli @@ -18,6 +18,6 @@ val print : Coq.Relation.t -> Theory.Trans.ir -> (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m -> - Term.rel_context -> + Context.rel_context -> Proof_type.tactic diff --git a/rewrite.ml4 b/rewrite.ml4 index 383d706..b3e52e0 100644 --- a/rewrite.ml4 +++ b/rewrite.ml4 @@ -8,6 +8,7 @@ (** aac_rewrite -- rewriting modulo *) +DECLARE PLUGIN "aac" module Control = struct let debug = false @@ -26,16 +27,15 @@ let tac_or_exn tac exn msg = fun gl -> pr_constr "last goal" (Tacmach.pf_concl gl); exn msg e + +let retype = Coq.retype + (* helper to be used with the previous function: raise a new anomaly except if a another one was previously raised *) let push_anomaly msg = function - | Util.Anomaly _ as e -> raise e + | e when Errors.is_anomaly e -> raise e | _ -> Coq.anomaly msg - - - - module M = Matcher open Term @@ -184,14 +184,14 @@ let by_aac_reflexivity zero (* This convert is required to deal with evars in a proper way *) let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in - let convert = Tactics.convert_concl convert_to Term.VMcast in - let apply_tac = Tactics.apply decision_thm in + let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Term.VMcast) in + let apply_tac = Proofview.V82.of_tactic (Tactics.apply decision_thm) in (Tacticals.tclTHENLIST - [ + [ retype decision_thm; retype convert_to; convert ; tac_or_exn apply_tac Coq.user_error "unification failure"; tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) Coq.anomaly "vm_compute failure"; - Tacticals.tclORELSE Tactics.reflexivity + Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity) (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) ]) ) @@ -215,10 +215,10 @@ let by_aac_normalise zero lift ir t t' = (* This convert is required to deal with evars in a proper way *) let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in - let convert = Tactics.convert_concl convert_to Term.VMcast in - let apply_tac = Tactics.apply normalise_thm in + let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Term.VMcast) in + let apply_tac = Proofview.V82.of_tactic (Tactics.apply normalise_thm) in (Tacticals.tclTHENLIST - [ + [ retype normalise_thm; retype convert_to; convert ; apply_tac; ]) @@ -260,6 +260,7 @@ let aac_normalise = fun goal -> Tacticals.tclTHENLIST [ aac_conclude by_aac_normalise; + Proofview.V82.of_tactic begin Tacinterp.interp ( <:tactic< intro x; @@ -270,8 +271,8 @@ let aac_normalise = fun goal -> unfold y; compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl >> - ); - Tactics.keep ids + )end; + Proofview.V82.of_tactic (Tactics.keep ids) ] goal let aac_reflexivity = fun goal -> @@ -293,7 +294,8 @@ let aac_reflexivity = fun goal -> |]) in Tacticals.tclTHEN - (Tactics.apply lift_reflexivity) + + (Tacticals.tclTHEN (retype lift_reflexivity) (Proofview.V82.of_tactic (Tactics.apply lift_reflexivity))) (fun goal -> let concl = Tacmach.pf_concl goal in let _ = pr_constr "concl "concl in @@ -330,8 +332,8 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equ |]) in Tacticals.tclTHENLIST - [ - Tactics.apply lift_transitivity + [ retype lift_transitivity; + Proofview.V82.of_tactic (Tactics.apply lift_transitivity) ] goal @@ -439,41 +441,6 @@ let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ) goal -(** [aac_match eq (fun x1 ... xn => p) t H] match the term [t] against - the pattern, and introduces an hypothesis H of type p = t. (Note - that we have performed the substitution in p). -*) - -let aac_match ~eq pattern term h = fun gl -> - let env = Tacmach.pf_env gl in - let evar_map = Tacmach.project gl in - let carrier = Typing.type_of env evar_map term in - let rel = Coq.Relation.make carrier eq in - let equiv,gl = Coq.Equivalence.from_relation gl rel in - (* first, we decompose the pattern as an arity. *) - let x_args, pat = Term.decompose_lam pattern in - (* then, we reify the pattern and the term, using the provided equality *) - let envs = Theory.Trans.empty_envs () in - let left, right,gl = Theory.Trans.t_of_constr gl rel envs (pat,term) in - let gl,ir = Theory.Trans.ir_of_envs gl rel envs in - let solutions = Matcher.matcher (Theory.Trans.ir_to_units ir) left right in - (* then, we pick the first solution to the matching problem *) - let sigma = match Search_monad.choose solutions with - | None -> Coq.user_error "no solution to the matching problem" - | Some sigma -> sigma - in - let p_sigma = Matcher.Subst.instantiate sigma left in - let args = List.map (fun (x,t) -> x,Theory.Trans.raw_constr_of_t ir rel [] t) (Matcher.Subst.to_list sigma) in - (* Then, we have to assert the fact that p_sigma is equal to term *) - let equation = mkApp (eq, [| Theory.Trans.raw_constr_of_t ir rel [] p_sigma ; term |]) in - let evar_map = Tacmach.project gl in - Tacticals.tclTHENLIST - [ - Refiner.tclEVARS evar_map; - Tactics.assert_by h equation (by_aac_reflexivity term equiv ir p_sigma right); - ] gl - - open Coq.Rewrite open Tacmach open Tacticals @@ -525,47 +492,39 @@ PRINTED BY pr_constro END TACTIC EXTEND _aac_reflexivity_ -| [ "aac_reflexivity" ] -> [ aac_reflexivity ] +| [ "aac_reflexivity" ] -> [ Proofview.V82.tactic aac_reflexivity ] END TACTIC EXTEND _aac_normalise_ -| [ "aac_normalise" ] -> [ aac_normalise ] +| [ "aac_normalise" ] -> [ Proofview.V82.tactic aac_normalise ] END TACTIC EXTEND _aac_rewrite_ | [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl) ] END TACTIC EXTEND _aac_pattern_ | [ "aac_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl) ] END TACTIC EXTEND _aac_instances_ | [ "aac_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl) ] END TACTIC EXTEND _aacu_rewrite_ | [ "aacu_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl) ] END TACTIC EXTEND _aacu_pattern_ | [ "aacu_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl) ] END TACTIC EXTEND _aacu_instances_ | [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl ] -END - -TACTIC EXTEND _aac_match_ -| [ "aac_match" constr(p) constr(t) ident(h)] -> - [ fun gl -> - let ty = Tacmach.pf_type_of gl t in - let eq = Coq.Leibniz.eq ty in - aac_match ~eq p t (Names.Name h) gl] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl) ] END diff --git a/rewrite.mli b/rewrite.mli new file mode 100644 index 0000000..d195075 --- /dev/null +++ b/rewrite.mli @@ -0,0 +1,9 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Definition of the tactics, and corresponding Coq grammar entries.*) diff --git a/theory.ml b/theory.ml index 3fa35bf..a5229fa 100644 --- a/theory.ml +++ b/theory.ml @@ -13,6 +13,7 @@ be of little interest to most readers. *) open Term +open Context module Control = struct let printing = true @@ -26,15 +27,8 @@ open Debug (** {1 HMap : Specialized Hashtables based on constr} *) -module Hashed_constr = -struct - type t = constr - let equal = (=) - let hash = Hashtbl.hash -end - (* TODO module HMap = Hashtbl, du coup ? *) -module HMap = Hashtbl.Make(Hashed_constr) +module HMap = Hashtbl.Make(Constr) let ac_theory_path = ["AAC_tactics"; "AAC"] @@ -295,10 +289,10 @@ module Unit = struct end let anomaly msg = - Util.anomaly ("aac_tactics: " ^ msg) + Errors.anomaly ~label:"aac_tactics" (Pp.str msg) let user_error msg = - Util.error ("aac_tactics: " ^ msg) + Errors.error ("aac_tactics: " ^ msg) module Trans = struct @@ -329,6 +323,64 @@ module Trans = struct | Sym of Sym.pack | Unit of constr (* to avoid confusion in bloom *) + module PackHash = + struct + open Hashset.Combine + + type t = pack + + let eq_sym_pack p1 p2 = + let open Sym in + Constr.equal p1.ar p2.ar && + Constr.equal p1.value p2.value && + Constr.equal p1.morph p2.morph + + let hash_sym_pack p = + let open Sym in + combine3 (Constr.hash p.ar) (Constr.hash p.value) (Constr.hash p.morph) + + let eq_bin_pack p1 p2 = + let open Bin in + Constr.equal p1.value p2.value && + Constr.equal p1.compat p2.compat && + Constr.equal p1.assoc p2.assoc && + Option.equal Constr.equal p1.comm p2.comm + + let hash_bin_pack p = + let open Bin in + combine4 (Constr.hash p.value) (Constr.hash p.compat) + (Constr.hash p.assoc) (Option.hash Constr.hash p.comm) + + let eq_unit_of u1 u2 = + let open Unit in + Constr.equal u1.uf_u u2.uf_u && + Constr.equal u1.uf_idx u2.uf_idx && + Constr.equal u1.uf_desc u2.uf_desc + + let hash_unit_of u = + let open Unit in + combine3 (Constr.hash u.uf_u) (Constr.hash u.uf_idx) + (Constr.hash u.uf_desc) + + let equal p1 p2 = match p1, p2 with + | Bin (p1, o1), Bin (p2, o2) -> + eq_bin_pack p1 p2 && Option.equal eq_unit_of o1 o2 + | Sym p1, Sym p2 -> eq_sym_pack p1 p2 + | Unit c1, Unit c2 -> Constr.equal c1 c2 + | _ -> false + + let hash p = match p with + | Bin (p, o) -> + combinesmall 1 (combine (hash_bin_pack p) (Option.hash hash_unit_of o)) + | Sym p -> + combinesmall 2 (hash_sym_pack p) + | Unit c -> + combinesmall 3 (Constr.hash c) + + end + + module PackTable = Hashtbl.Make(PackHash) + (** discr is a map from {!Term.constr} to {!pack}. [None] means that it is not possible to instantiate this partial @@ -343,7 +395,7 @@ module Trans = struct type envs = { discr : (pack option) HMap.t ; - bloom : (pack, int ) Hashtbl.t; + bloom : int PackTable.t; bloom_back : (int, pack ) Hashtbl.t; bloom_next : int ref; } @@ -351,7 +403,7 @@ module Trans = struct let empty_envs () = { discr = HMap.create 17; - bloom = Hashtbl.create 17; + bloom = PackTable.create 17; bloom_back = Hashtbl.create 17; bloom_next = ref 1; } @@ -359,16 +411,16 @@ module Trans = struct let add_bloom envs pack = - if Hashtbl.mem envs.bloom pack + if PackTable.mem envs.bloom pack then () else let x = ! (envs.bloom_next) in - Hashtbl.add envs.bloom pack x; + PackTable.add envs.bloom pack x; Hashtbl.add envs.bloom_back x pack; incr (envs.bloom_next) let find_bloom envs pack = - try Hashtbl.find envs.bloom pack + try PackTable.find envs.bloom pack with Not_found -> assert false (********************************************) @@ -720,7 +772,7 @@ module Trans = struct match wu with | None -> acc | Some (unit_of) -> - let unit_n = Hashtbl.find envs.bloom + let unit_n = PackTable.find envs.bloom (Unit unit_of.Unit.uf_u) in ( n, unit_n)::unit_for, @@ -742,7 +794,7 @@ module Trans = struct match wu with | None -> acc | Some unit_of -> - if unit_of.Unit.uf_u = u + if Constr.equal (unit_of.Unit.uf_u) u then {unit_of with Unit.uf_idx = (Coq.Pos.of_int nop)} :: acc @@ -829,7 +881,7 @@ module Trans = struct (** cap rebuilds the products in front of the constr *) let rec cap c = function [] -> c | t::q -> - let i = Term.lookup_rel t context in + let i = Context.lookup_rel t context in cap (mkProd_or_LetIn i c) q in let t,indices = raw_constr_of_t_debruijn ir t in diff --git a/theory.mli b/theory.mli index cc9a617..1dae57b 100644 --- a/theory.mli +++ b/theory.mli @@ -160,7 +160,7 @@ module Trans : sig reconstruct the named products on top of it. In particular, this allow us to print the context put around the left (or right) hand side of a pattern. *) - val raw_constr_of_t : ir -> Coq.Relation.t -> (Term.rel_context) ->Matcher.Terms.t -> Term.constr + val raw_constr_of_t : ir -> Coq.Relation.t -> (Context.rel_context) ->Matcher.Terms.t -> Term.constr (** {2 Building reified terms} *) -- cgit v1.2.3