diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 19 | ||||
| -rw-r--r-- | library/heads.ml | 193 | ||||
| -rw-r--r-- | library/heads.mli | 28 | ||||
| -rw-r--r-- | library/lib.ml | 25 | ||||
| -rw-r--r-- | library/lib.mli | 5 | ||||
| -rw-r--r-- | library/library.mllib | 1 |
6 files changed, 27 insertions, 244 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index f14ad333e9..eafcb8fea6 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -318,26 +318,35 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v = | Some (name, depr, (read,write,append)) -> write locality (check_and_cast v (read ())) -let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") +let show_value_type = function + | BoolValue _ -> "bool" + | IntValue _ -> "int" + | StringValue _ -> "string" + | StringOptValue _ -> "string" + +let bad_type_error opt_value actual_type = + user_err Pp.(str "Bad type of value for this option:" ++ spc() ++ + str "expected " ++ str (show_value_type opt_value) ++ + str ", got " ++ str actual_type ++ str ".") let check_int_value v = function | IntValue _ -> IntValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "int" let check_bool_value v = function | BoolValue _ -> BoolValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "bool" let check_string_value v = function | StringValue _ -> StringValue v | StringOptValue _ -> StringOptValue (Some v) - | _ -> bad_type_error () + | optv -> bad_type_error optv "string" let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None | StringOptValue _ -> StringOptValue None - | _ -> bad_type_error () + | optv -> bad_type_error optv "nothing" (* Nota: For compatibility reasons, some errors are treated as warning. This allows a script to refer to an option that doesn't diff --git a/library/heads.ml b/library/heads.ml deleted file mode 100644 index d9d650ac07..0000000000 --- a/library/heads.ml +++ /dev/null @@ -1,193 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <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) *) -(************************************************************************) - -open Util -open Names -open Constr -open Vars -open Mod_subst -open Environ -open Globnames -open Libobject -open Lib -open Context.Named.Declaration - -(** Characterization of the head of a term *) - -(* We only compute an approximation to ensure the computation is not - arbitrary long (e.g. the head constant of [h] defined to be - [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch - the evaluation of [phi(0)] and the head of [h] is declared unknown). *) - -type rigid_head_kind = -| RigidParameter of Constant.t (* a Const without body *) -| RigidVar of variable (* a Var without body *) -| RigidType (* an inductive, a product or a sort *) - -type head_approximation = -| RigidHead of rigid_head_kind -| ConstructorHead -| FlexibleHead of int * int * int * bool (* [true] if a surrounding case *) -| NotImmediatelyComputableHead - -(** Registration as global tables and rollback. *) - -module Evalreford = struct - type t = evaluable_global_reference - let compare gr1 gr2 = match gr1, gr2 with - | EvalVarRef id1, EvalVarRef id2 -> Id.compare id1 id2 - | EvalVarRef _, EvalConstRef _ -> -1 - | EvalConstRef c1, EvalConstRef c2 -> - Constant.CanOrd.compare c1 c2 - | EvalConstRef _, EvalVarRef _ -> 1 -end - -module Evalrefmap = - Map.Make (Evalreford) - - -let head_map = Summary.ref Evalrefmap.empty ~name:"Head_decl" - -let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map -let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map - -let kind_of_head env t = - let rec aux k l t b = match kind (Reduction.whd_betaiotazeta env t) with - | Rel n when n > k -> NotImmediatelyComputableHead - | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) - | Var id -> - (try on_subterm k l b (variable_head id) - with Not_found -> - (* a goal variable *) - match lookup_named id env with - | LocalDef (_,c,_) -> aux k l c b - | LocalAssum _ -> NotImmediatelyComputableHead) - | Const (cst,_) -> - (try on_subterm k l b (constant_head cst) - with Not_found -> - CErrors.anomaly - Pp.(str "constant not found in kind_of_head: " ++ - Names.Constant.print cst ++ - str ".")) - | Construct _ | CoFix _ -> - if b then NotImmediatelyComputableHead else ConstructorHead - | Sort _ | Ind _ | Prod _ -> RigidHead RigidType - | Cast (c,_,_) -> aux k l c b - | Lambda (_,_,c) -> - begin match l with - | [] -> - let () = assert (not b) in - aux (k + 1) [] c b - | h :: l -> aux k l (subst1 h c) b - end - | LetIn _ -> assert false - | Meta _ | Evar _ -> NotImmediatelyComputableHead - | App (c,al) -> aux k (Array.to_list al @ l) c b - | Proj (p,c) -> - (try on_subterm k (c :: l) b (constant_head (Projection.constant p)) - with Not_found -> assert false) - - | Case (_,_,c,_) -> aux k [] c true - | Fix ((i,j),_) -> - let n = i.(j) in - try aux k [] (List.nth l n) true - with Failure _ -> FlexibleHead (k + n + 1, k + n + 1, 0, true) - and on_subterm k l with_case = function - | FlexibleHead (n,i,q,with_subcase) -> - let m = List.length l in - let k',rest,a = - if n > m then - (* eta-expansion *) - let a = - if i <= m then - (* we pick the head in the existing arguments *) - lift (n-m) (List.nth l (i-1)) - else - (* we pick the head in the added arguments *) - mkRel (n-i+1) in - k+n-m,[],a - else - (* enough arguments to [cst] *) - k,List.skipn n l,List.nth l (i-1) in - let l' = List.make q (mkMeta 0) @ rest in - aux k' l' a (with_subcase || with_case) - | ConstructorHead when with_case -> NotImmediatelyComputableHead - | x -> x - in aux 0 [] t false - -(* FIXME: maybe change interface here *) -let compute_head = function -| EvalConstRef cst -> - let env = Global.env() in - let cb = Environ.lookup_constant cst env in - let is_Def = function Declarations.Def _ -> true | _ -> false in - let body = - if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body - then Global.body_of_constant cst else None - in - (match body with - | None -> RigidHead (RigidParameter cst) - | Some (c, _) -> kind_of_head env c) -| EvalVarRef id -> - (match Global.lookup_named id with - | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> - kind_of_head (Global.env()) c - | _ -> - RigidHead (RigidVar id)) - -let is_rigid env t = - match kind_of_head env t with - | RigidHead _ | ConstructorHead -> true - | _ -> false - -(** Registration of heads as an object *) - -let load_head _ (_,(ref,(k:head_approximation))) = - head_map := Evalrefmap.add ref k !head_map - -let cache_head o = - load_head 1 o - -let subst_head_approximation subst = function - | RigidHead (RigidParameter cst) as k -> - let cst,c = subst_con_kn subst cst in - if isConst c && Constant.equal (fst (destConst c)) cst then - (* A change of the prefix of the constant *) - k - else - (* A substitution of the constant by a functor argument *) - kind_of_head (Global.env()) c - | x -> x - -let subst_head (subst,(ref,k)) = - (subst_evaluable_reference subst ref, subst_head_approximation subst k) - -let discharge_head (_,(ref,k)) = - match ref with - | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k) - | EvalVarRef id -> None - -let rebuild_head (ref,k) = - (ref, compute_head ref) - -type head_obj = evaluable_global_reference * head_approximation - -let inHead : head_obj -> obj = - declare_object {(default_object "HEAD") with - cache_function = cache_head; - load_function = load_head; - subst_function = subst_head; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_head; - rebuild_function = rebuild_head } - -let declare_head c = - let hd = compute_head c in - add_anonymous_leaf (inHead (c,hd)) diff --git a/library/heads.mli b/library/heads.mli deleted file mode 100644 index 421242996c..0000000000 --- a/library/heads.mli +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <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) *) -(************************************************************************) - -open Names -open Constr -open Environ - -(** This module is about the computation of an approximation of the - head symbol of defined constants and local definitions; it - provides the function to compute the head symbols and a table to - store the heads *) - -(** [declared_head] computes and registers the head symbol of a - possibly evaluable constant or variable *) - -val declare_head : evaluable_global_reference -> unit - -(** [is_rigid] tells if some term is known to ultimately reduce to a term - with a rigid head symbol *) - -val is_rigid : env -> constr -> bool diff --git a/library/lib.ml b/library/lib.ml index a20de55bf6..8ebe44890c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -26,13 +26,11 @@ type node = | Leaf of obj | CompilingLibrary of object_prefix | OpenedModule of is_type * export * object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_entry = object_name * node +type library_entry = object_name * node -and library_segment = library_entry list +type library_segment = library_entry list type lib_objects = (Names.Id.t * obj) list @@ -73,10 +71,6 @@ let classify_segment seg = clean ((id,o')::substl, keepl, anticipl) stk | Anticipate o' -> clean (substl, keepl, o'::anticipl) stk) - | (_,ClosedSection _) :: stk -> clean acc stk - (* LEM; TODO: Understand what this does and see if what I do is the - correct thing for ClosedMod(ule|type) *) - | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" @@ -307,7 +301,6 @@ let end_mod is_type = in let (after,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - add_entry oname (ClosedModule (List.rev (mark::after))); let prefix = !lib_state.path_prefix in recalc_path_prefix (); (oname, prefix, fs, after) @@ -555,7 +548,6 @@ let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -570,7 +562,6 @@ let close_section () = let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; pop_path_prefix (); - add_entry oname (ClosedSection (List.rev (mark::secdecls))); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls @@ -589,10 +580,8 @@ let freeze ~marshallable = | n, (CompilingLibrary _ as x) -> Some (n,x) | n, OpenedModule (it,e,op,_) -> Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) - | n, ClosedModule _ -> Some (n,ClosedModule []) | n, OpenedSection (op, _) -> - Some(n,OpenedSection(op,Summary.empty_frozen)) - | n, ClosedSection _ -> Some (n,ClosedSection [])) + Some(n,OpenedSection(op,Summary.empty_frozen))) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> @@ -656,6 +645,14 @@ let discharge_kn kn = let discharge_con cst = if con_defined_in_sec cst then Globnames.pop_con cst else cst +let discharge_proj_repr = + Projection.Repr.map_npars (fun mind npars -> + if not (defined_in_sec mind) then mind, npars + else + let modlist = replacement_context () in + let _, newpars = Mindmap.find mind (snd modlist) in + Globnames.pop_kn mind, npars + Array.length newpars) + let discharge_inductive (kn,i) = (discharge_kn kn,i) diff --git a/library/lib.mli b/library/lib.mli index 5abfccfc7d..9933b762ba 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -23,11 +23,9 @@ type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_segment = (Libnames.object_name * node) list +type library_segment = (Libnames.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list @@ -189,6 +187,7 @@ val replacement_context : unit -> Opaqueproof.work_list val discharge_kn : MutInd.t -> MutInd.t val discharge_con : Constant.t -> Constant.t +val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t val discharge_global : GlobRef.t -> GlobRef.t val discharge_inductive : inductive -> inductive val discharge_abstract_universe_context : diff --git a/library/library.mllib b/library/library.mllib index 2ac4266fc0..9cacaba4a7 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -14,6 +14,5 @@ Kindops Dischargedhypsmap Goptions Decls -Heads Keys Coqlib |