diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 19:31:00 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 19:35:53 +0200 |
commit | 35ba593b4ecb805b4e69c01c56fb4b93dfafdf0b (patch) | |
tree | ffcf6a36e224f1a41996f7ede84d773753254209 | |
parent | 707bfd5719b76d131152a258d49740165fbafe03 (diff) |
Reverting 16 last commits, committed mistakenly using the wrong push command.
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
-rw-r--r-- | checker/univ.ml | 14 | ||||
-rw-r--r-- | ide/project_file.ml4 | 1 | ||||
-rw-r--r-- | kernel/constr.ml | 28 | ||||
-rw-r--r-- | kernel/cooking.ml | 12 | ||||
-rw-r--r-- | kernel/environ.ml | 2 | ||||
-rw-r--r-- | kernel/names.ml | 58 | ||||
-rw-r--r-- | kernel/names.mli | 26 | ||||
-rw-r--r-- | kernel/sorts.ml | 2 | ||||
-rw-r--r-- | kernel/univ.ml | 22 | ||||
-rw-r--r-- | lib/cSet.ml | 2 | ||||
-rw-r--r-- | lib/hashcons.ml | 12 | ||||
-rw-r--r-- | lib/hashcons.mli | 12 | ||||
-rw-r--r-- | lib/hashset.ml | 4 | ||||
-rw-r--r-- | lib/hashset.mli | 2 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 73 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
-rw-r--r-- | pretyping/reductionops.mli | 3 | ||||
-rw-r--r-- | proofs/pfedit.ml | 4 | ||||
-rw-r--r-- | proofs/pfedit.mli | 2 | ||||
-rw-r--r-- | tactics/elimschemes.ml | 20 | ||||
-rw-r--r-- | tactics/eqschemes.ml | 18 | ||||
-rw-r--r-- | test-suite/success/apply.v | 2 | ||||
-rw-r--r-- | theories/Init/Notations.v | 3 | ||||
-rw-r--r-- | theories/Init/Specif.v | 2 | ||||
-rw-r--r-- | toplevel/auto_ind_decl.ml | 42 | ||||
-rw-r--r-- | toplevel/ind_tables.ml | 32 | ||||
-rw-r--r-- | toplevel/ind_tables.mli | 15 |
27 files changed, 169 insertions, 248 deletions
diff --git a/checker/univ.ml b/checker/univ.ml index 912d20e0d..3bcb3bc95 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -33,7 +33,7 @@ module type Hashconsed = sig type t val hash : t -> int - val eq : t -> t -> bool + val equal : t -> t -> bool val hcons : t -> t end @@ -51,7 +51,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with + let equal l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -131,7 +131,7 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.eq x y then l + if H.equal x y then l else cons y (remove x l) end @@ -229,7 +229,7 @@ module Level = struct type _t = t type t = _t type u = unit - let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -319,7 +319,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let eq l1 l2 = + let equal l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -338,7 +338,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let eq x y = x == y || + let equal x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1079,7 +1079,7 @@ struct a end - let eq t1 t2 = + let equal t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 152f76cc0..f7279f9cf 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -28,7 +28,6 @@ let rec parse_string = parser and parse_string2 = parser | [< ''"' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise Parsing_error and parse_skip_comment = parser | [< ''\n'; s >] -> s | [< 'c; s >] -> parse_skip_comment s diff --git a/kernel/constr.ml b/kernel/constr.ml index 644f866b3..e2b1d3fd9 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -732,10 +732,12 @@ let hasheq t1 t2 = n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2 - | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 - | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 - | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 + | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> + sp1 == sp2 && Int.equal i1 i2 && u1 == u2 + | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) -> + sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 && u1 == u2 | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> @@ -755,10 +757,10 @@ let hasheq t1 t2 = once and for all the table we'll use for hash-consing all constr *) module HashsetTerm = - Hashset.Make(struct type t = constr let eq = hasheq end) + Hashset.Make(struct type t = constr let equal = hasheq end) module HashsetTermArray = - Hashset.Make(struct type t = constr array let eq = array_eqeq end) + Hashset.Make(struct type t = constr array let equal = array_eqeq end) let term_table = HashsetTerm.create 19991 (* The associative table to hashcons terms. *) @@ -813,19 +815,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Proj (p,c) -> let c, hc = sh_rec c in let p' = Projection.hcons p in - (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc)) + (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc)) | Const (c,u) -> let c' = sh_con c in let u', hu = sh_instance u in - (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) - | Ind (ind,u) -> + (Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu)) + | Ind ((kn,i) as ind,u) -> let u', hu = sh_instance u in (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_syntactic_hash ind) hu)) - | Construct (c,u) -> + combinesmall 10 (combine (ind_hash ind) hu)) + | Construct ((((kn,i),j) as c,u))-> let u', hu = sh_instance u in (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_syntactic_hash c) hu)) + combinesmall 11 (combine (constructor_hash c) hu)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in @@ -928,7 +930,7 @@ struct List.equal (==) info1.ind_tags info2.ind_tags && Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags && info1.style == info2.style - let eq ci ci' = + let equal ci ci' = ci.ci_ind == ci'.ci_ind && Int.equal ci.ci_npar ci'.ci_npar && Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) @@ -970,7 +972,7 @@ module Hsorts = let hashcons huniv = function Prop c -> Prop c | Type u -> Type (huniv u) - let eq s1 s2 = + let equal s1 s2 = s1 == s2 || match (s1,s2) with (Prop c1, Prop c2) -> c1 == c2 diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9849f156c..be71bd7b4 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -44,15 +44,15 @@ module RefHash = struct type t = my_global_reference let equal gr1 gr2 = match gr1, gr2 with - | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2 - | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2 - | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2 + | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2 + | IndRef i1, IndRef i2 -> eq_ind i1 i2 + | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2 | _ -> false open Hashset.Combine let hash = function - | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c) - | IndRef i -> combinesmall 2 (ind_syntactic_hash i) - | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) + | ConstRef c -> combinesmall 1 (Constant.hash c) + | IndRef i -> combinesmall 2 (ind_hash i) + | ConstructRef c -> combinesmall 3 (constructor_hash c) end module RefTable = Hashtbl.Make(RefHash) diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c..30b28177c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val let pop_rel_context n env = let ctxt = env.env_rel_context in { env with - env_rel_context = List.skipn n ctxt; + env_rel_context = List.firstn (List.length ctxt - n) ctxt; env_nb_rel = env.env_nb_rel - n } let fold_named_context f env ~init = diff --git a/kernel/names.ml b/kernel/names.ml index a99702d15..ae2b3b638 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -102,7 +102,7 @@ struct let hashcons hident = function | Name id -> Name (hident id) | n -> n - let eq n1 n2 = + let equal n1 n2 = n1 == n2 || match (n1,n2) with | (Name id1, Name id2) -> id1 == id2 @@ -236,7 +236,7 @@ struct type t = _t type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t) let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) - let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = + let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) let hash = hash @@ -327,7 +327,7 @@ module ModPath = struct | MPfile dir -> MPfile (hdir dir) | MPbound m -> MPbound (huniqid m) | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l) - let rec eq d1 d2 = + let rec equal d1 d2 = d1 == d2 || match d1,d2 with | MPfile dir1, MPfile dir2 -> dir1 == dir2 @@ -423,7 +423,7 @@ module KerName = struct let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } - let eq kn1 kn2 = + let equal kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel let hash = hash @@ -477,7 +477,7 @@ module KerPair = struct | Dual (kn,_) -> kn let same kn = Same kn - let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc) + let make knu knc = if knu == knc then Same knc else Dual (knu,knc) let make1 = same let make2 mp l = same (KerName.make2 mp l) @@ -524,23 +524,6 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end - module SyntacticOrd = struct - type t = kernel_pair - let compare x y = match x, y with - | Same knx, Same kny -> KerName.compare knx kny - | Dual (knux,kncx), Dual (knuy,kncy) -> - let c = KerName.compare knux knuy in - if not (Int.equal c 0) then c - else KerName.compare kncx kncy - | Same _, _ -> -1 - | Dual _, _ -> 1 - let equal x y = x == y || compare x y = 0 - let hash = function - | Same kn -> KerName.hash kn - | Dual (knu, knc) -> - Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) - end - (** Default (logical) comparison and hash is on the canonical part *) let equal = CanOrd.equal let hash = CanOrd.hash @@ -552,7 +535,7 @@ module KerPair = struct let hashcons hkn = function | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) - let eq x y = (* physical comparison on subterms *) + let equal x y = (* physical comparison on subterms *) x == y || match x,y with | Same x, Same y -> x == y @@ -607,8 +590,6 @@ let index_of_constructor (ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let eq_user_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 -let eq_syntactic_ind (m1, i1) (m2, i2) = - Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2 let ind_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in @@ -616,22 +597,15 @@ let ind_ord (m1, i1) (m2, i2) = let ind_user_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c -let ind_syntactic_ord (m1, i1) (m2, i2) = - let c = Int.compare i1 i2 in - if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c let ind_hash (m, i) = Hashset.Combine.combine (MutInd.hash m) (Int.hash i) let ind_user_hash (m, i) = Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) -let ind_syntactic_hash (m, i) = - Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i) let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 let eq_user_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_user_ind ind1 ind2 -let eq_syntactic_constructor (ind1, j1) (ind2, j2) = - Int.equal j1 j2 && eq_syntactic_ind ind1 ind2 let constructor_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in @@ -639,16 +613,11 @@ let constructor_ord (ind1, j1) (ind2, j2) = let constructor_user_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in if Int.equal c 0 then ind_user_ord ind1 ind2 else c -let constructor_syntactic_ord (ind1, j1) (ind2, j2) = - let c = Int.compare j1 j2 in - if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c let constructor_hash (ind, i) = Hashset.Combine.combine (ind_hash ind) (Int.hash i) let constructor_user_hash (ind, i) = Hashset.Combine.combine (ind_user_hash ind) (Int.hash i) -let constructor_syntactic_hash (ind, i) = - Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i) module InductiveOrdered = struct type t = inductive @@ -693,7 +662,7 @@ module Hind = Hashcons.Make( type t = inductive type u = MutInd.t -> MutInd.t let hashcons hmind (mind, i) = (hmind mind, i) - let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 + let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = ind_hash end) @@ -702,7 +671,7 @@ module Hconstruct = Hashcons.Make( type t = constructor type u = inductive -> inductive let hashcons hind (ind, j) = (hind ind, j) - let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 + let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 let hash = constructor_hash end) @@ -836,22 +805,13 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c - module SyntacticOrd = struct - type t = constant * bool - let compare (c, b) (c', b') = - if b = b' then Constant.SyntacticOrd.compare c c' else -1 - let equal (c, b as x) (c', b' as x') = - x == x' || b = b' && Constant.SyntacticOrd.equal c c' - let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c - end - module Self_Hashcons = struct type _t = t type t = _t type u = Constant.t -> Constant.t let hashcons hc (c,b) = (hc c,b) - let eq ((c,b) as x) ((c',b') as y) = + let equal ((c,b) as x) ((c',b') as y) = x == y || (c == c' && b == b') let hash = hash end diff --git a/kernel/names.mli b/kernel/names.mli index 9a8977c92..7cc444375 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -305,12 +305,6 @@ sig val hash : t -> int end - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) @@ -385,12 +379,6 @@ sig val hash : t -> int end - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) @@ -429,22 +417,16 @@ val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool val eq_user_ind : inductive -> inductive -> bool -val eq_syntactic_ind : inductive -> inductive -> bool val ind_ord : inductive -> inductive -> int val ind_hash : inductive -> int val ind_user_ord : inductive -> inductive -> int val ind_user_hash : inductive -> int -val ind_syntactic_ord : inductive -> inductive -> int -val ind_syntactic_hash : inductive -> int val eq_constructor : constructor -> constructor -> bool val eq_user_constructor : constructor -> constructor -> bool -val eq_syntactic_constructor : constructor -> constructor -> bool val constructor_ord : constructor -> constructor -> int -val constructor_hash : constructor -> int val constructor_user_ord : constructor -> constructor -> int +val constructor_hash : constructor -> int val constructor_user_hash : constructor -> int -val constructor_syntactic_ord : constructor -> constructor -> int -val constructor_syntactic_hash : constructor -> int (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = @@ -658,12 +640,6 @@ module Projection : sig val make : constant -> bool -> t - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val constant : t -> constant val unfolded : t -> bool val unfold : t -> t diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 2baf9b133..e2854abfd 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -98,7 +98,7 @@ module Hsorts = let u' = huniv u in if u' == u then c else Type u' | s -> s - let eq s1 s2 = match (s1,s2) with + let equal s1 s2 = match (s1,s2) with | (Prop c1, Prop c2) -> c1 == c2 | (Type u1, Type u2) -> u1 == u2 |_ -> false diff --git a/kernel/univ.ml b/kernel/univ.ml index 09a64d1b0..336cdb653 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -35,7 +35,7 @@ module type Hashconsed = sig type t val hash : t -> int - val eq : t -> t -> bool + val equal : t -> t -> bool val hcons : t -> t end @@ -53,7 +53,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with + let equal l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -135,12 +135,12 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.eq x y then l + if H.equal x y then l else cons y (remove x l) let rec mem x = function | Nil -> false - | Cons (y, _, l) -> H.eq x y || mem x l + | Cons (y, _, l) -> H.equal x y || mem x l let rec compare cmp l1 l2 = match l1, l2 with | Nil, Nil -> 0 @@ -251,7 +251,7 @@ module Level = struct type _t = t type t = _t type u = unit - let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -398,7 +398,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let eq l1 l2 = + let equal l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -417,7 +417,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let eq x y = x == y || + let equal x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1293,7 +1293,7 @@ module Hconstraint = type t = univ_constraint type u = universe_level -> universe_level let hashcons hul (l1,k,l2) = (hul l1, k, hul l2) - let eq (l1,k,l2) (l1',k',l2') = + let equal (l1,k,l2) (l1',k',l2') = l1 == l1' && k == k' && l2 == l2' let hash = Hashtbl.hash end) @@ -1305,7 +1305,7 @@ module Hconstraints = type u = univ_constraint -> univ_constraint let hashcons huc s = Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty - let eq s s' = + let equal s s' = List.for_all2eq (==) (Constraint.elements s) (Constraint.elements s') @@ -1676,7 +1676,7 @@ struct a end - let eq t1 t2 = + let equal t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = @@ -2043,7 +2043,7 @@ module Huniverse_set = type u = universe_level -> universe_level let hashcons huc s = LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty - let eq s s' = + let equal s s' = LSet.equal s s' let hash = Hashtbl.hash end) diff --git a/lib/cSet.ml b/lib/cSet.ml index 783165630..d7d5c70b3 100644 --- a/lib/cSet.ml +++ b/lib/cSet.ml @@ -57,7 +57,7 @@ struct open Hashset.Combine type t = set type u = M.t -> M.t - let eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) + let equal s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0 let hashcons = umap end diff --git a/lib/hashcons.ml b/lib/hashcons.ml index d368e20e6..46ba0b628 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -15,7 +15,7 @@ * of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...). * [hashcons u x] is a function that hash-cons the sub-structures of x using * the hash-consing functions u provides. - * [eq] is a comparison function. It is allowed to use physical equality + * [equal] is a comparison function. It is allowed to use physical equality * on the sub-terms hash-consed by the hashcons function. * [hash] is the hash function given to the Hashtbl.Make function * @@ -27,7 +27,7 @@ module type HashconsedType = type t type u val hashcons : u -> t -> t - val eq : t -> t -> bool + val equal : t -> t -> bool val hash : t -> int end @@ -53,7 +53,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) = (* We create the type of hashtables for t, with our comparison fun. * An invariant is that the table never contains two entries equals - * w.r.t (=), although the equality on keys is X.eq. This is + * w.r.t (=), although the equality on keys is X.equal. This is * granted since we hcons the subterms before looking up in the table. *) module Htbl = Hashset.Make(X) @@ -124,7 +124,7 @@ module Hlist (D:HashedType) = let hashcons (hrec,hdata) = function | x :: l -> hdata x :: hrec l | l -> l - let eq l1 l2 = + let equal l1 l2 = l1 == l2 || match l1, l2 with | [], [] -> true @@ -144,7 +144,7 @@ module Hstring = Make( type t = string type u = unit let hashcons () s =(* incr accesstr;*) s - external eq : string -> string -> bool = "caml_string_equal" "noalloc" + external equal : string -> string -> bool = "caml_string_equal" "noalloc" (** Copy from CString *) let rec hash len s i accu = if i = len then accu @@ -191,7 +191,7 @@ module Hobj = Make( type t = Obj.t type u = (Obj.t -> Obj.t) * unit let hashcons (hrec,_) = hash_obj hrec - let eq = comp_obj + let equal = comp_obj let hash = Hashtbl.hash end) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 93890c494..8d0adc3fd 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -14,9 +14,9 @@ module type HashconsedType = sig (** {6 Generic hashconsing signature} - Given an equivalence relation [eq], a hashconsing function is a + Given an equivalence relation [equal], a hashconsing function is a function that associates the same canonical element to two elements - related by [eq]. Usually, the element chosen is canonical w.r.t. + related by [equal]. Usually, the element chosen is canonical w.r.t. physical equality [(==)], so as to reduce memory consumption and enhance efficiency of equality tests. @@ -32,15 +32,15 @@ module type HashconsedType = Usually a tuple of functions. *) val hashcons : u -> t -> t (** The actual hashconsing function, using its fist argument to recursively - hashcons substructures. It should be compatible with [eq], that is - [eq x (hashcons f x) = true]. *) - val eq : t -> t -> bool + hashcons substructures. It should be compatible with [equal], that is + [equal x (hashcons f x) = true]. *) + val equal : t -> t -> bool (** A comparison function. It is allowed to use physical equality on the sub-terms hashconsed by the [hashcons] function, but it should be insensible to shallow copy of the compared object. *) val hash : t -> int (** A hash function passed to the underlying hashtable structure. [hash] - should be compatible with [eq], i.e. if [eq x y = true] then + should be compatible with [equal], i.e. if [equal x y = true] then [hash x = hash y]. *) end diff --git a/lib/hashset.ml b/lib/hashset.ml index 9454aef9b..1ca6cc641 100644 --- a/lib/hashset.ml +++ b/lib/hashset.ml @@ -16,7 +16,7 @@ module type EqType = sig type t - val eq : t -> t -> bool + val equal : t -> t -> bool end type statistics = { @@ -183,7 +183,7 @@ module Make (E : EqType) = if i >= sz then ifnotfound index else if h = hashes.(i) then begin match Weak.get bucket i with - | Some v when E.eq v d -> v + | Some v when E.equal v d -> v | _ -> loop (i + 1) end else loop (i + 1) in diff --git a/lib/hashset.mli b/lib/hashset.mli index 270484d8a..a455eec66 100644 --- a/lib/hashset.mli +++ b/lib/hashset.mli @@ -16,7 +16,7 @@ module type EqType = sig type t - val eq : t -> t -> bool + val equal : t -> t -> bool end type statistics = { diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b73ff2bc5..bb07bf056 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -380,26 +380,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in let consume_stack on_left (termF,skF) (termO,skO) evd = let switch f a b = if on_left then f a b else f b a in - let not_only_appO = Stack.not_purely_applicative skO in - match switch (ise_stack2 not_only_appO env evd (evar_conv_x ts)) skF skO with - |Some (lF,rO), Success i' when on_left && (not_only_appO || List.is_empty lF) -> - (* Case (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *) - (* or (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *) - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO)) - |Some (rO,lF), Success i' when not on_left && (not_only_appO || List.is_empty lF) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO)) + let not_only_app = Stack.not_purely_applicative skO in + match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with + |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> + switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) + |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> + switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) in - let eta env evd onleft (termR,skR) (termO,skO) = - assert (match skR with [] -> true | _ -> false); - let (na,c1,c'1) = destLambda termR in + let eta env evd onleft sk term sk' term' = + assert (match sk with [] -> true | _ -> false); + let (na,c1,c'1) = destLambda term in let c = nf_evar evd c1 in let env' = push_rel (na,None,c) env in let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip (termO, skO @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), + (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 @@ -419,7 +417,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> quick_fail evd + | None -> default_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left @@ -427,9 +425,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM else quick_fail i) ev lF tM i - and consume (termF,skF as apprF) (termM,skM as apprM) i = + and consume (termF,skF as apprF) (termM,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then - (* This tries first-order matching *) consume_stack on_left apprF apprM i else quick_fail i and delta i = @@ -468,32 +465,32 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let switch f a b = if on_left then f a b else f b a in let eta evd = match kind_of_term termR with - | Lambda _ -> eta env evd false apprR apprF - | Construct u -> eta_constructor ts env evd (u,skR) apprF + | Lambda _ -> eta env evd false skR termR skF termF + | Construct u -> eta_constructor ts env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in - let postpone tR lF evd = - (* Postpone the use of an heuristic *) - if not (occur_rigidly (fst ev) evd tR) then - let evd,tF = - if isRel tR || isVar tR then - (* Optimization so as to generate candidates *) - let evd,ev = evar_absorb_arguments env evd ev lF in - evd,mkEvar ev - else - evd,Stack.zip apprF in - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) evd)) - tF tR - else - UnifFailure (evd,OccurCheck (fst ev,tR)) - in match Stack.list_of_app_stack skF with | None -> ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> let tR = Stack.zip apprR in miller_pfenning on_left - (fun () -> ise_try evd [eta;postpone tR lF]) + (fun () -> + ise_try evd + [eta;(* Postpone the use of an heuristic *) + (fun i -> + if not (occur_rigidly (fst ev) i tR) then + let i,tF = + if isRel tR || isVar tR then + (* Optimization so as to generate candidates *) + let i,ev = evar_absorb_arguments env i ev lF in + i,mkEvar ev + else + i,Stack.zip apprF in + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) + tF tR + else + UnifFailure (evd,OccurCheck (fst ev,tR)))]) ev lF tR evd in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in @@ -712,10 +709,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Eta-expansion *) | Rigid, _ when isLambda term1 -> - eta env evd true appr1 appr2 + eta env evd true sk1 term1 sk2 term2 | _, Rigid when isLambda term2 -> - eta env evd false appr2 appr1 + eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin match kind_of_term term1, kind_of_term term2 with @@ -755,10 +752,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty rigids env evd sk1 term1 sk2 term2 | Construct u, _ -> - eta_constructor ts env evd (u,sk1) appr2 + eta_constructor ts env evd sk1 u sk2 term2 | _, Construct u -> - eta_constructor ts env evd (u,sk2) appr1 + eta_constructor ts env evd sk2 u sk1 term1 | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then @@ -854,7 +851,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fst (decompose_app_vect (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor ts env evd (((ind, i), u),sk1) (term2,sk2) = +and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2892de7c4..dc70f36cc 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -306,9 +306,7 @@ struct | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")" and pr pr_c l = let open Pp in - str "[" ++ - prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l ++ - str "]" + prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l and pr_cst_member pr_c c = let open Pp in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 51df07f28..1df2a73b2 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -90,9 +90,6 @@ module Stack : sig val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option val not_purely_applicative : 'a t -> bool - - (** @return the arguments in the stack if a purely applicative - stack, None otherwise *) val list_of_app_stack : constr t -> constr list option val assign : 'a t -> int -> 'a -> 'a t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index bde0a1c16..d024c01ba 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -145,12 +145,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic env ctx ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in - let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in + let ce = Term_typing.handle_entry_side_effects env ce in let (cb, ctx), se = Future.force ce.const_entry_body in assert(Declareops.side_effects_is_empty se); assert(Univ.ContextSet.is_empty ctx); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 4aa3c3bfd..5e0fb4dd3 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -153,7 +153,7 @@ val build_constant_by_tactic : types -> unit Proofview.tactic -> Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index dbaa60d61..749e0d2b5 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -21,7 +21,7 @@ open Ind_tables (* Induction/recursion schemes *) -let optimize_non_type_induction_scheme kind dep sort _ ind = +let optimize_non_type_induction_scheme kind dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in if check_scheme kind ind then @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f7d3ad5d0..8643fe10f 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -191,7 +191,7 @@ let build_sym_scheme env ind = let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" - (fun _ ind -> + (fun ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in (c, ctx), Declareops.no_seff) @@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind = let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" - (fun _ ind -> + (fun ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind) (**********************************************************************) @@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme (**********************************************************************) let rew_l2r_dep_scheme_kind = declare_individual_scheme_object "_rew_r_dep" - (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType) + (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Dependent rewrite from right-to-left in conclusion *) @@ -660,7 +660,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +670,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -693,7 +693,7 @@ let rew_l2r_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" - (fun _ ind -> fix_r2l_forward_rew_scheme + (fun ind -> fix_r2l_forward_rew_scheme (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) (**********************************************************************) @@ -704,7 +704,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) (* End of rewriting schemes *) @@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind = in c, Evd.evar_universe_context_of ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" - (fun _ ind -> + (fun ind -> (* May fail if equality is not defined *) build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 074004fa1..24d5cf8a9 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -371,7 +371,7 @@ Qed. Goal True. Fail eapply existT. -Set Universal Lemma Under Conjunction. +Set Trivial Tactic Unification Under Conjunction. eapply existT. Abort. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 07d7f9150..a7bdba90a 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -69,9 +69,6 @@ Reserved Notation "{ x }" (at level 0, x at level 99). Reserved Notation "{ x | P }" (at level 0, x at level 99). Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). -Reserved Notation "{ x & P }" (at level 0, x at level 99). -Reserved Notation "{ x & P & Q }" (at level 0, x at level 99). - Reserved Notation "{ x : A | P }" (at level 0, x at level 99). Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index ecdbef7f6..1384901b7 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -48,8 +48,6 @@ Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. -Notation "{ x & P }" := (sigT (fun x => P)) : type_scope. -Notation "{ x & P & Q }" := (sigT2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 118ffb3e8..d1452fca2 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -111,7 +111,7 @@ let check_bool_is_defined () = let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let build_beq_scheme mode kn = +let build_beq_scheme kn = check_bool_is_defined (); (* fetching global env *) let env = Global.env() in @@ -188,7 +188,7 @@ let build_beq_scheme mode kn = else begin try let eq, eff = - let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in + let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in mkConst c, eff in let eqa, eff = let eqa, effs = List.split (List.map aux a) in @@ -330,7 +330,7 @@ let destruct_ind c = so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) -let do_replace_lb mode lb_scheme_key aavoid narg p q = +let do_replace_lb lb_scheme_key aavoid narg p q = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -360,7 +360,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = let u,v = destruct_ind type_of_pq in let lb_type_of_p = try - let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in + let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in Proofview.tclUNIT (mkConst c, eff) with Not_found -> (* spiwack: the format of this error message should probably @@ -388,7 +388,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = end (* used in the bool -> leib side *) -let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = +let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -551,7 +551,7 @@ let compute_bl_goal ind lnamesparrec nparrec = (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) ))), eff -let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = +let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -608,7 +608,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). if eq_gr (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN - (do_replace_bl mode bl_scheme_key ind + (do_replace_bl bl_scheme_key ind (!avoid) nparrec (ca.(2)) (ca.(1))) @@ -625,12 +625,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let side_effect_of_mode = function - | Declare.KernelVerbose -> false - | Declare.KernelSilent -> true - | Declare.UserVerbose -> false - -let make_bl_scheme mode mind = +let make_bl_scheme mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -642,9 +637,8 @@ let make_bl_scheme mode mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in - let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal - (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal + (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -694,7 +688,7 @@ let compute_lb_goal ind lnamesparrec nparrec = (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) ))), eff -let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = +let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -738,7 +732,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = | App(c,ca) -> (match (kind_of_term ca.(1)) with | App(c',ca') -> let n = Array.length ca' in - do_replace_lb mode lb_scheme_key + do_replace_lb lb_scheme_key (!avoid) nparrec ca'.(n-2) ca'.(n-1) @@ -753,7 +747,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") -let make_lb_scheme mode mind = +let make_lb_scheme mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -765,9 +759,8 @@ let make_lb_scheme mode mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context in - let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal - (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal + (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx (* FIXME *)), eff @@ -926,7 +919,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ] end -let make_eq_decidability mode mind = +let make_eq_decidability mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then raise DecidabilityMutualNotSupported; @@ -937,8 +930,7 @@ let make_eq_decidability mode mind = let ctx = Evd.empty_evar_universe_context (* FIXME *)in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index b59d6fc8a..0d39466ed 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -28,10 +28,11 @@ open Pp (**********************************************************************) (* Registering schemes in the environment *) + type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects type 'a scheme_kind = string @@ -140,31 +141,32 @@ let define internal id c p univs = in kn -let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = - let (c, ctx), eff = f mode ind in +let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = + let (c, ctx), eff = f ind in let mib = Global.lookup_mind mind in let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define mode id c mib.mind_polymorphic ctx in + let const = define internal id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; const, Declareops.cons_side_effects (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff -let define_individual_scheme kind mode names (mind,i as ind) = +let define_individual_scheme kind internal names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with | _,MutualSchemeFunction f -> assert false | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode names ind + define_individual_scheme_base kind s f internal names ind -let define_mutual_scheme_base kind suff f mode names mind = - let (cl, ctx), eff = f mode mind in +let define_mutual_scheme_base kind suff f internal names mind = + let (cl, ctx), eff = f mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in + let consts = Array.map2 (fun id cl -> - define mode id cl mib.mind_polymorphic ctx) ids cl in + define internal id cl mib.mind_polymorphic ctx) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, @@ -173,11 +175,11 @@ let define_mutual_scheme_base kind suff f mode names mind = kind (Global.safe_env()) (Array.to_list schemes)) eff -let define_mutual_scheme kind mode names mind = +let define_mutual_scheme kind internal names mind = match Hashtbl.find scheme_object_table kind with | _,IndividualSchemeFunction _ -> assert false | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f mode names mind + define_mutual_scheme_base kind s f internal names mind let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in @@ -186,14 +188,14 @@ let find_scheme_on_env_too kind ind = kind (Global.safe_env()) [ind, s]) Declareops.no_seff -let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) = +let find_scheme kind (mind,i as ind) = try find_scheme_on_env_too kind ind with Not_found -> match Hashtbl.find scheme_object_table kind with | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode None ind + define_individual_scheme_base kind s f KernelSilent None ind | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f mode [] mind in + let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in ca.(i), eff let check_scheme kind ind = diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index d0844dd94..98eaac092 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -8,7 +8,6 @@ open Term open Names -open Declare (** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) @@ -20,9 +19,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects (** Main functions to register a scheme builder *) @@ -33,17 +32,21 @@ val declare_individual_scheme_object : string -> ?aux:string -> individual_scheme_object_function -> individual scheme_kind +(* +val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit +*) + (** Force generation of a (mutually) scheme with possibly user-level names *) val define_individual_scheme : individual scheme_kind -> - internal_flag (** internal *) -> + Declare.internal_flag (** internal *) -> Id.t option -> inductive -> constant * Declareops.side_effects -val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> +val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool |