From aa29c92dfa395e2f369e81bd72cef482cdf90c65 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 20 Sep 2016 09:11:09 +0200 Subject: Stylistic improvements in intf/decl_kinds.mli. We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic". --- library/decls.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'library/decls.ml') diff --git a/library/decls.ml b/library/decls.ml index 2952c258a..1e9afe968 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -19,18 +19,22 @@ module NamedDecl = Context.Named.Declaration (** Datas associated to section variables and local definitions *) type variable_data = - DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind + { dir_path : DirPath.t; + opaque : bool; + universe_context_set : Univ.universe_context_set; + polymorphic : bool; + kind : logical_kind } let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" let add_variable_data id o = vartab := Id.Map.add id o !vartab -let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p -let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq -let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k -let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx -let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p +let variable_path id = (Id.Map.find id !vartab).dir_path +let variable_opacity id = (Id.Map.find id !vartab).opaque +let variable_kind id = (Id.Map.find id !vartab).kind +let variable_context id = (Id.Map.find id !vartab).universe_context_set +let variable_polymorphic id = (Id.Map.find id !vartab).polymorphic let variable_secpath id = let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in -- cgit v1.2.3