diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.ml | 11 | ||||
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 3 | ||||
| -rw-r--r-- | library/keys.ml | 162 | ||||
| -rw-r--r-- | library/keys.mli | 23 | ||||
| -rw-r--r-- | library/lib.ml | 59 | ||||
| -rw-r--r-- | library/lib.mli | 10 | ||||
| -rw-r--r-- | library/library.mllib | 2 |
8 files changed, 38 insertions, 235 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml deleted file mode 100644 index 17746645ee..0000000000 --- a/library/decl_kinds.ml +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type binding_kind = Explicit | Implicit diff --git a/library/global.ml b/library/global.ml index ca774dbd74..0fc9e11364 100644 --- a/library/global.ml +++ b/library/global.ml @@ -89,6 +89,9 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c) +let set_check_positive c = globalize0 (Safe_typing.set_check_positive c) +let set_check_universes c = globalize0 (Safe_typing.set_check_universes c) let typing_flags () = Environ.typing_flags (env ()) let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) diff --git a/library/global.mli b/library/global.mli index d034bc4208..b089b7dd80 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,6 +31,9 @@ val named_context : unit -> Constr.named_context val set_engagement : Declarations.engagement -> unit val set_indices_matter : bool -> unit val set_typing_flags : Declarations.typing_flags -> unit +val set_check_guarded : bool -> unit +val set_check_positive : bool -> unit +val set_check_universes : bool -> unit val typing_flags : unit -> Declarations.typing_flags val make_sprop_cumulative : unit -> unit val set_allow_sprop : bool -> unit diff --git a/library/keys.ml b/library/keys.ml deleted file mode 100644 index 9964992433..0000000000 --- a/library/keys.ml +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Keys for unification and indexing *) - -open Names -open Constr -open Libobject -open Globnames - -type key = - | KGlob of GlobRef.t - | KLam - | KLet - | KProd - | KSort - | KCase - | KFix - | KCoFix - | KRel - | KInt - -module KeyOrdered = struct - type t = key - - let hash gr = - match gr with - | KGlob gr -> 9 + GlobRef.Ordered.hash gr - | KLam -> 0 - | KLet -> 1 - | KProd -> 2 - | KSort -> 3 - | KCase -> 4 - | KFix -> 5 - | KCoFix -> 6 - | KRel -> 7 - | KInt -> 8 - - let compare gr1 gr2 = - match gr1, gr2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2 - | _, KGlob _ -> -1 - | KGlob _, _ -> 1 - | k, k' -> Int.compare (hash k) (hash k') - - let equal k1 k2 = - match k1, k2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2 - | _, KGlob _ -> false - | KGlob _, _ -> false - | k, k' -> k == k' -end - -module Keymap = HMap.Make(KeyOrdered) -module Keyset = Keymap.Set - -(* Mapping structure for references to be considered equivalent *) - -let keys = Summary.ref Keymap.empty ~name:"Keys_decl" - -let add_kv k v m = - try Keymap.modify k (fun k' vs -> Keyset.add v vs) m - with Not_found -> Keymap.add k (Keyset.singleton v) m - -let add_keys k v = - keys := add_kv k v (add_kv v k !keys) - -let equiv_keys k k' = - k == k' || KeyOrdered.equal k k' || - try Keyset.mem k' (Keymap.find k !keys) - with Not_found -> false - -(** Registration of keys as an object *) - -let load_keys _ (_,(ref,ref')) = - add_keys ref ref' - -let cache_keys o = - load_keys 1 o - -let subst_key subst k = - match k with - | KGlob gr -> KGlob (subst_global_reference subst gr) - | _ -> k - -let subst_keys (subst,(k,k')) = - (subst_key subst k, subst_key subst k') - -let discharge_key = function - | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None - | x -> Some x - -let discharge_keys (_,(k,k')) = - match discharge_key k, discharge_key k' with - | Some x, Some y -> Some (x, y) - | _ -> None - -type key_obj = key * key - -let inKeys : key_obj -> obj = - declare_object @@ superglobal_object "KEYS" - ~cache:cache_keys - ~subst:(Some subst_keys) - ~discharge:discharge_keys - -let declare_equiv_keys ref ref' = - Lib.add_anonymous_leaf (inKeys (ref,ref')) - -let constr_key kind c = - try - let rec aux k = - match kind k with - | Const (c, _) -> KGlob (GlobRef.ConstRef c) - | Ind (i, u) -> KGlob (GlobRef.IndRef i) - | Construct (c,u) -> KGlob (GlobRef.ConstructRef c) - | Var id -> KGlob (GlobRef.VarRef id) - | App (f, _) -> aux f - | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p)) - | Cast (p, _, _) -> aux p - | Lambda _ -> KLam - | Prod _ -> KProd - | Case _ -> KCase - | Fix _ -> KFix - | CoFix _ -> KCoFix - | Rel _ -> KRel - | Meta _ -> raise Not_found - | Evar _ -> raise Not_found - | Sort _ -> KSort - | LetIn _ -> KLet - | Int _ -> KInt - in Some (aux c) - with Not_found -> None - -open Pp - -let pr_key pr_global = function - | KGlob gr -> pr_global gr - | KLam -> str"Lambda" - | KLet -> str"Let" - | KProd -> str"Product" - | KSort -> str"Sort" - | KCase -> str"Case" - | KFix -> str"Fix" - | KCoFix -> str"CoFix" - | KRel -> str"Rel" - | KInt -> str"Int" - -let pr_keyset pr_global v = - prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) - -let pr_mapping pr_global k v = - pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v - -let pr_keys pr_global = - Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt()) diff --git a/library/keys.mli b/library/keys.mli deleted file mode 100644 index a7adf7791b..0000000000 --- a/library/keys.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type key - -val declare_equiv_keys : key -> key -> unit -(** Declare two keys as being equivalent. *) - -val equiv_keys : key -> key -> bool -(** Check equivalence of keys. *) - -val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option -(** Compute the head key of a term. *) - -val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t -(** Pretty-print the mapping *) diff --git a/library/lib.ml b/library/lib.ml index 59b55cc16b..3f51826315 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -413,11 +413,8 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Constr.named_declaration * Decl_kinds.binding_kind - -type variable_context = variable_info list type abstr_info = { - abstr_ctx : variable_context; + abstr_ctx : Constr.named_context; abstr_subst : Univ.Instance.t; abstr_uctx : Univ.AUContext.t; } @@ -426,21 +423,17 @@ type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = | Variable of { id:Names.Id.t; - kind:Decl_kinds.binding_kind; - univs:Univ.ContextSet.t; } | Context of Univ.ContextSet.t type section_data = { sec_entry : secentry list; - sec_workl : Opaqueproof.work_list; sec_abstr : abstr_list; sec_poly : bool; } let empty_section_data ~poly = { sec_entry = []; - sec_workl = (Names.Cmap.empty,Names.Mindmap.empty); sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty); sec_poly = poly; } @@ -456,12 +449,12 @@ let add_section ~poly () = List.iter (fun tab -> check_same_poly poly tab) !sectab; sectab := empty_section_data ~poly :: !sectab -let add_section_variable ~name ~kind ~poly univs = +let add_section_variable ~name ~poly = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | s :: sl -> List.iter (fun tab -> check_same_poly poly tab) !sectab; - let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in + let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in sectab := s :: sl let add_section_context ctx = @@ -472,38 +465,45 @@ let add_section_context ctx = let s = { s with sec_entry = Context ctx :: s.sec_entry } in sectab := s :: sl -exception PolyFound of bool (* make this a let exception once possible *) +exception PolyFound (* make this a let exception once possible *) let is_polymorphic_univ u = try let open Univ in List.iter (fun s -> let vars = s.sec_entry in List.iter (function - | Variable {univs=(univs,_)} -> - if LSet.mem u univs then raise (PolyFound s.sec_poly) + | Variable _ -> () | Context (univs,_) -> - if LSet.mem u univs then raise (PolyFound true) + if LSet.mem u univs then raise PolyFound ) vars ) !sectab; false - with PolyFound b -> b + with PolyFound -> true let extract_hyps poly (secs,ohyps) = let rec aux = function - | (Variable {id;kind;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> + | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in - (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r - | (Variable {univs}::idl,hyps) -> + decl :: l, r + | (Variable _::idl,hyps) -> let l, r = aux (idl,hyps) in - l, if poly then Univ.ContextSet.union r univs else r + l, r | (Context ctx :: idl, hyps) -> + let () = assert poly in let l, r = aux (idl, hyps) in l, Univ.ContextSet.union r ctx | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) let instance_from_variable_context = - List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list + List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list + +let extract_worklist info = + let args = instance_from_variable_context info.abstr_ctx in + info.abstr_subst, args + +let make_worklist (cmap, mmap) = + Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap let name_instance inst = (* FIXME: this should probably be done at an upper level, by storing the @@ -522,37 +522,34 @@ let name_instance inst = in Array.map map (Univ.Instance.to_array inst) -let add_section_replacement f g poly hyps = +let add_section_replacement g poly hyps = match !sectab with | [] -> () | s :: sl -> let () = check_same_poly poly s in let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in let ctx = Univ.ContextSet.to_context ctx in - let inst = Univ.UContext.instance ctx in - let nas = name_instance inst in + let nas = name_instance (Univ.UContext.instance ctx) in let subst, ctx = Univ.abstract_universes nas ctx in - let args = instance_from_variable_context (List.rev sechyps) in let info = { abstr_ctx = sechyps; abstr_subst = subst; abstr_uctx = ctx; } in let s = { s with - sec_workl = f (inst, args) s.sec_workl; sec_abstr = g info s.sec_abstr; } in sectab := s :: sl let add_section_kn ~poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f poly + add_section_replacement f poly let add_section_constant ~poly kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f poly + add_section_replacement f poly -let replacement_context () = (List.hd !sectab).sec_workl +let replacement_context () = make_worklist (List.hd !sectab).sec_abstr let section_segment_of_constant con = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) @@ -585,9 +582,11 @@ let section_instance = let open GlobRef in function then Univ.Instance.empty, [||] else raise Not_found | ConstRef con -> - Names.Cmap.find con (fst (List.hd !sectab).sec_workl) + let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in + extract_worklist data | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - Names.Mindmap.find kn (snd (List.hd !sectab).sec_workl) + let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in + extract_worklist data let is_in_section ref = try ignore (section_instance ref); true with Not_found -> false diff --git a/library/lib.mli b/library/lib.mli index fe6bf69ec4..9ffa69ef93 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -163,10 +163,8 @@ val drop_objects : frozen -> frozen val init : unit -> unit (** {6 Section management for discharge } *) -type variable_info = Constr.named_declaration * Decl_kinds.binding_kind -type variable_context = variable_info list type abstr_info = private { - abstr_ctx : variable_context; + abstr_ctx : Constr.named_context; (** Section variables of this prefix *) abstr_subst : Univ.Instance.t; (** Actual names of the abstracted variables *) @@ -174,18 +172,16 @@ type abstr_info = private { (** Universe quantification, same length as the substitution *) } -val instance_from_variable_context : variable_context -> Id.t array - val section_segment_of_constant : Constant.t -> abstr_info val section_segment_of_mutual_inductive: MutInd.t -> abstr_info val section_segment_of_reference : GlobRef.t -> abstr_info -val variable_section_segment_of_reference : GlobRef.t -> variable_context +val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit +val add_section_variable : name:Id.t -> poly:bool -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit diff --git a/library/library.mllib b/library/library.mllib index 35af5fa43b..3b75438ccd 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,4 +1,3 @@ -Decl_kinds Libnames Globnames Libobject @@ -11,5 +10,4 @@ Library States Kindops Goptions -Keys Coqlib |