From 5f8ce72b29f4a4620ce46895f2e563b2fd85f24b Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 22 Oct 2013 20:11:20 +0000 Subject: Removing some generic equalities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/context.ml | 3 ++- kernel/context.mli | 2 +- kernel/conv_oracle.ml | 7 +++++-- kernel/environ.ml | 4 ++-- kernel/environ.mli | 2 +- lib/flags.ml | 12 +++++++++++- library/globnames.ml | 8 +++++++- parsing/tok.ml | 14 +++++++++++++- pretyping/evarsolve.ml | 2 +- pretyping/evarutil.ml | 2 +- pretyping/termops.ml | 2 +- 11 files changed, 45 insertions(+), 13 deletions(-) diff --git a/kernel/context.ml b/kernel/context.ml index 930ab7508..bdc4c067a 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -90,7 +90,8 @@ let rec lookup_named id = function let named_context_length = List.length let named_context_equal = List.equal eq_named_declaration -let vars_of_named_context = List.map (fun (id,_,_) -> id) +let vars_of_named_context ctx = + List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx let instance_from_named_context sign = let filter = function diff --git a/kernel/context.mli b/kernel/context.mli index ad6d645cd..048edef95 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -56,7 +56,7 @@ type rel_context = rel_declaration list val empty_named_context : named_context val add_named_decl : named_declaration -> named_context -> named_context -val vars_of_named_context : named_context -> Id.t list +val vars_of_named_context : named_context -> Id.Set.t val lookup_named : Id.t -> named_context -> named_declaration diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 0a96821a3..65efb4fd0 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -18,6 +18,9 @@ open Names *) type level = Expand | Level of int | Opaque let default = Level 0 +let is_default = function +| Level 0 -> true +| _ -> false let transparent = default let is_transparent = function | Level 0 -> true @@ -45,11 +48,11 @@ let set_strategy k l = match k with | VarKey id -> var_opacity := - if l=default then Id.Map.remove id !var_opacity + if is_default l then Id.Map.remove id !var_opacity else Id.Map.add id l !var_opacity | ConstKey c -> cst_opacity := - if l=default then Cmap.remove c !cst_opacity + if is_default l then Cmap.remove c !cst_opacity else Cmap.add c l !cst_opacity | RelKey _ -> Errors.error "set_strategy: RelKey" diff --git a/kernel/environ.ml b/kernel/environ.ml index 9b18db78e..ae6817a76 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -228,7 +228,7 @@ let lookup_constructor_variables (ind,_) env = let vars_of_global env constr = match kind_of_term constr with - Var id -> [id] + Var id -> Id.Set.singleton id | Const kn -> lookup_constant_variables kn env | Ind ind -> lookup_inductive_variables ind env | Construct cstr -> lookup_constructor_variables cstr env @@ -239,7 +239,7 @@ let global_vars_set env constr = let acc = match kind_of_term c with | Var _ | Const _ | Ind _ | Construct _ -> - List.fold_right Id.Set.add (vars_of_global env c) acc + Id.Set.union (vars_of_global env c) acc | _ -> acc in fold_constr filtrec acc c diff --git a/kernel/environ.mli b/kernel/environ.mli index 54e88f646..d378501a0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -165,7 +165,7 @@ val set_engagement : engagement -> env -> env val global_vars_set : env -> constr -> Id.Set.t (** the constr must be a global reference *) -val vars_of_global : env -> constr -> Id.t list +val vars_of_global : env -> constr -> Id.Set.t val keep_hyps : env -> Id.Set.t -> section_context diff --git a/lib/flags.ml b/lib/flags.ml index 4e3da3d8c..cde45a81f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -79,8 +79,18 @@ let we_are_parsing = ref false For correct comparisons, this constructor should remain the last one. *) type compat_version = V8_2 | V8_3 | V8_4 | Current + let compat_version = ref Current -let version_strictly_greater v = !compat_version > v + +let version_strictly_greater v = match !compat_version, v with +| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false +| V8_3, (V8_3 | V8_4 | Current) -> false +| V8_4, (V8_4 | Current) -> false +| Current, Current -> false +| V8_3, V8_2 -> true +| V8_4, (V8_2 | V8_3) -> true +| Current, (V8_2 | V8_3 | V8_4) -> true + let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function diff --git a/library/globnames.ml b/library/globnames.ml index e80197030..af4ebde7f 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -82,7 +82,13 @@ let global_ord_gen ord_cst ord_ind ord_cons x y = match x, y with | IndRef indx, IndRef indy -> ord_ind indx indy | ConstructRef consx, ConstructRef consy -> ord_cons consx consy | VarRef v1, VarRef v2 -> Id.compare v1 v2 - | _, _ -> Pervasives.compare x y + + | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1 + | ConstRef _, VarRef _ -> 1 + | ConstRef _, (IndRef _ | ConstructRef _) -> -1 + | IndRef _, (VarRef _ | ConstRef _) -> 1 + | IndRef _, ConstructRef _ -> -1 + | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1 let global_ord_can = global_ord_gen con_ord ind_ord constructor_ord diff --git a/parsing/tok.ml b/parsing/tok.ml index 4cb94e38b..0ff94d395 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -19,6 +19,18 @@ type t = | LEFTQMARK | EOI +let equal t1 t2 = match t1, t2 with +| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2 +| METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2 +| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2 +| IDENT s1, IDENT s2 -> CString.equal s1 s2 +| FIELD s1, FIELD s2 -> CString.equal s1 s2 +| INT s1, INT s2 -> CString.equal s1 s2 +| STRING s1, STRING s2 -> CString.equal s1 s2 +| LEFTQMARK, LEFTQMARK -> true +| EOI, EOI -> true +| _ -> false + let extract_string = function | KEYWORD s -> s | IDENT s -> s @@ -89,4 +101,4 @@ let match_pattern = | "EOI", "" -> (function EOI -> "" | _ -> err ()) | pat -> let tok = of_pattern pat in - function tok' -> if tok = tok' then snd pat else err () + function tok' -> if equal tok tok' then snd pat else err () diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a4fc330c6..fc5fc0d2c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -273,7 +273,7 @@ let free_vars_and_rels_up_alias_expansion aliases c = | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1 | _ -> frec (aliases,depth) c end | Const _ | Ind _ | Construct _ -> - acc2 := List.fold_right Id.Set.add (vars_of_global (Global.env()) c) !acc2 + acc2 := Id.Set.union (vars_of_global (Global.env()) c) !acc2 | _ -> iter_constr_with_full_binders (fun d (aliases,depth) -> (extend_alias d aliases,depth+1)) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index de394e660..d2f53e953 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -390,7 +390,7 @@ let rec check_and_clear_in_constr evdref err ids c = | ( Const _ | Ind _ | Construct _ ) -> let vars = Environ.vars_of_global (Global.env()) c in - List.iter check vars; c + Id.Set.iter check vars; c | Evar (evk,l as ev) -> if Evd.is_defined !evdref evk then diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 66a656ad7..908010428 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -523,7 +523,7 @@ let occur_evar n c = let occur_in_global env id constr = let vars = vars_of_global env constr in - if List.mem id vars then raise Occur + if Id.Set.mem id vars then raise Occur let occur_var env id c = let rec occur_rec c = -- cgit v1.2.3