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/lib.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 749cc4ff3..954889fb6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -416,12 +416,12 @@ let check_same_poly p vars = if List.exists pred vars then error "Cannot mix universe polymorphic and monomorphic declarations in sections." -let add_section_variable id impl poly ctx = +let add_section_variable id impl ~polymorphic ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; - sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + List.iter (fun tab -> check_same_poly polymorphic (pi1 tab)) !sectab; + sectab := (Variable (id,impl,polymorphic,ctx)::vars,repl,abs)::sl let add_section_context ctx = match !sectab with @@ -450,11 +450,11 @@ let instance_from_variable_context = let named_of_variable_context = List.map fst -let add_section_replacement f g poly hyps = +let add_section_replacement f g ~polymorphic hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> - let () = check_same_poly poly vars in + let () = check_same_poly polymorphic vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in @@ -462,13 +462,13 @@ let add_section_replacement f g poly hyps = sectab := (vars,f (Univ.UContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl -let add_section_kn poly kn = +let add_section_kn ~polymorphic kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f poly + add_section_replacement f f ~polymorphic -let add_section_constant poly kn = +let add_section_constant ~polymorphic kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f poly + add_section_replacement f f ~polymorphic let replacement_context () = pi2 (List.hd !sectab) -- cgit v1.2.3 From 1bc1cba7a759a285131a3ed6ea8979716700b856 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 20 Sep 2016 17:13:27 +0200 Subject: Rename Decl_kinds.binding_kind into Decls_kind.implicit_status. The new name makes it more obvious what is meant here by "kind". We leave Decl_kinds.binding_kind as a deprecated alias for plugin compatibility. We also replace bool with implicit_status in a few places in the codebase. --- interp/constrexpr_ops.ml | 8 ++++---- interp/constrexpr_ops.mli | 4 ++-- interp/constrextern.ml | 4 ++-- interp/constrintern.ml | 2 +- interp/constrintern.mli | 2 +- interp/notation_ops.ml | 14 +++++++------- interp/notation_ops.mli | 2 +- intf/constrexpr.mli | 8 ++++---- intf/decl_kinds.mli | 5 ++++- intf/glob_term.mli | 6 +++--- library/declare.ml | 6 +++--- library/declare.mli | 2 +- library/lib.ml | 4 ++-- library/lib.mli | 4 ++-- stm/lemmas.ml | 2 +- toplevel/command.ml | 2 +- toplevel/command.mli | 2 +- 17 files changed, 40 insertions(+), 37 deletions(-) (limited to 'library/lib.ml') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 59c24900d..2644a56b3 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -17,7 +17,7 @@ open Decl_kinds (***********************) (* For binders parsing *) -let binding_kind_eq bk1 bk2 = match bk1, bk2 with +let implicit_status_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true | Implicit, Implicit -> true | _ -> false @@ -28,9 +28,9 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with | _ -> false let binder_kind_eq b1 b2 = match b1, b2 with -| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2 +| Default bk1, Default bk2 -> implicit_status_eq bk1 bk2 | Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) -> - binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 && + implicit_status_eq bk1 bk2 && implicit_status_eq ck1 ck2 && (if b1 then b2 else not b2) | _ -> false @@ -165,7 +165,7 @@ let rec constr_expr_eq e1 e2 = | CPrim(_,i1), CPrim(_,i2) -> prim_token_eq i1 i2 | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) -> - binding_kind_eq bk1 bk2 && + implicit_status_eq bk1 bk2 && Option.equal abstraction_kind_eq ak1 ak2 && constr_expr_eq e1 e2 | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index a92da035f..bfe546ba5 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -26,8 +26,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool val local_binder_eq : local_binder -> local_binder -> bool (** Equality on [local_binder]. Same properties as [constr_expr_eq]. *) -val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool -(** Equality on [binding_kind] *) +val implicit_status_eq : Decl_kinds.implicit_status -> Decl_kinds.implicit_status -> bool +(** Equality on [implicit_status] *) val binder_kind_eq : binder_kind -> binder_kind -> bool (** Equality on [binder_kind] *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f7fcbb4ee..62cb62f49 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -808,7 +808,7 @@ and factorize_prod scopes vars na bk aty c = let c = extern_typ scopes vars c in match na, c with | Name id, CProdN (loc,[nal,Default bk',ty],c) - when binding_kind_eq bk bk' && constr_expr_eq aty ty + when implicit_status_eq bk bk' && constr_expr_eq aty ty && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> @@ -818,7 +818,7 @@ and factorize_lambda inctx scopes vars na bk aty c = let c = sub_extern inctx scopes vars c in match c with | CLambdaN (loc,[nal,Default bk',ty],c) - when binding_kind_eq bk bk' && constr_expr_eq aty ty + when implicit_status_eq bk bk' && constr_expr_eq aty ty && not (occur_name na ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index fb11359e3..b9f5704d8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -65,7 +65,7 @@ type var_internalization_data = type internalization_env = (var_internalization_data) Id.Map.t -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) +type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr) type ltac_sign = { ltac_vars : Id.Set.t; diff --git a/interp/constrintern.mli b/interp/constrintern.mli index eea76aa31..718aa753e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -75,7 +75,7 @@ type ltac_sign = { val empty_ltac_sign : ltac_sign -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) +type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr) (** {6 Internalization performs interpretation of global names and notations } *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6b29b6d3d..c65d43db3 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -29,10 +29,10 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> + when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> + when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 @@ -772,18 +772,18 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in - let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in + let unify_implicit_status bk bk' = if bk == bk' then bk' else raise No_match in let unify_binder alp b b' = match b, b' with | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) -> let alp, na = unify_name alp na na' in - alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t') + alp, (Inl na, unify_implicit_status bk bk', None, unify_term alp t t') | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) -> let alp, na = unify_name alp na na' in - alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t') + alp, (Inl na, unify_implicit_status bk bk', Some (unify_term alp c c'), unify_term alp t t') | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) -> let alp, p = unify_pat alp p p' in - alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t') + alp, (Inr p, unify_implicit_status bk bk', None, unify_term alp t t') | _ -> raise No_match in let rec unify alp bl bl' = match bl, bl' with @@ -1122,7 +1122,7 @@ let term_of_binder = function | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) type glob_decl2 = - (name, cases_pattern) Util.union * Decl_kinds.binding_kind * + (name, cases_pattern) Util.union * Decl_kinds.implicit_status * glob_constr option * glob_constr let match_notation_constr u c (metas,pat) = diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 854e222e3..6428ccab6 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -48,7 +48,7 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr exception No_match type glob_decl2 = - (name, cases_pattern) Util.union * Decl_kinds.binding_kind * + (name, cases_pattern) Util.union * Decl_kinds.implicit_status * glob_constr option * glob_constr val match_notation_constr : bool -> glob_constr -> interpretation -> (glob_constr * subscopes) list * (glob_constr list * subscopes) list * diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 0cbb29575..e494b2f81 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -23,8 +23,8 @@ type explicitation = | ExplByName of Id.t type binder_kind = - | Default of binding_kind - | Generalized of binding_kind * binding_kind * bool + | Default of implicit_status + | Generalized of implicit_status * implicit_status * bool (** Inner binding, outer bindings, typeclass-specific flag for implicit generalization of superclasses *) @@ -95,7 +95,7 @@ and constr_expr = | CSort of Loc.t * glob_sort | CCast of Loc.t * constr_expr * constr_expr cast_type | CNotation of Loc.t * notation * constr_notation_substitution - | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr + | CGeneralization of Loc.t * implicit_status * abstraction_kind option * constr_expr | CPrim of Loc.t * prim_token | CDelimiters of Loc.t * string * constr_expr @@ -132,7 +132,7 @@ and constr_notation_substitution = constr_expr list list * (** for recursive notations *) local_binder list list (** for binders subexpressions *) -type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr +type typeclass_constraint = (Name.t located * Id.t located list option) * implicit_status * constr_expr and typeclass_context = typeclass_constraint list diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 29972f2f4..c117baf3f 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -10,7 +10,10 @@ type locality = Discharge | Local | Global -type binding_kind = Explicit | Implicit +type implicit_status = Explicit | Implicit + +type binding_kind = implicit_status +(** @deprecated Alias type *) type polymorphic = bool diff --git a/intf/glob_term.mli b/intf/glob_term.mli index b3159c860..178952fef 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -40,8 +40,8 @@ type glob_constr = | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list - | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr - | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GLambda of Loc.t * Name.t * implicit_status * glob_constr * glob_constr + | GProd of Loc.t * Name.t * implicit_status * glob_constr * glob_constr | GLetIn of Loc.t * Name.t * glob_constr * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) @@ -54,7 +54,7 @@ type glob_constr = | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option) | GCast of Loc.t * glob_constr * glob_constr cast_type -and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr +and glob_decl = Name.t * implicit_status * glob_constr option * glob_constr and fix_recursion_order = | GStructRec diff --git a/library/declare.ml b/library/declare.ml index 36a58629e..5c6543e28 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -46,7 +46,7 @@ type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; polymorphic : bool; - binding_kind : binding_kind } + implicit_status : implicit_status } type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -59,9 +59,9 @@ let cache_variable ((sp,_),o) = alreadydeclared (pr_id id ++ str " already exists"); let impl,opaque,polymorphic,ctx = match d with (* Fails if not well-typed *) - | SectionLocalAssum { type_context = (ty,ctx); polymorphic; binding_kind } -> + | SectionLocalAssum { type_context = (ty,ctx); polymorphic; implicit_status } -> let () = Global.push_named_assum ((id,ty,polymorphic),ctx) in - binding_kind, true, polymorphic, ctx + implicit_status, true, polymorphic, ctx | SectionLocalDef (de) -> let univs = Global.push_named_def (id,de) in Explicit, de.const_entry_opaque, diff --git a/library/declare.mli b/library/declare.mli index 760bf437b..a0ec26444 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -25,7 +25,7 @@ type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; polymorphic : bool; - binding_kind : binding_kind } + implicit_status : implicit_status } type variable_declaration = DirPath.t * section_variable_entry * logical_kind diff --git a/library/lib.ml b/library/lib.ml index 954889fb6..13921610d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -391,7 +391,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -399,7 +399,7 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = - | Variable of (Names.Id.t * Decl_kinds.binding_kind * + | Variable of (Names.Id.t * Decl_kinds.implicit_status * Decl_kinds.polymorphic * Univ.universe_context_set) | Context of Univ.universe_context_set diff --git a/library/lib.mli b/library/lib.mli index e905ee57e..51c74d395 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -162,7 +162,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -176,7 +176,7 @@ val variable_section_segment_of_reference : Globnames.global_reference -> variab val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> polymorphic:bool -> Univ.universe_context_set -> unit +val add_section_variable : Names.Id.t -> Decl_kinds.implicit_status -> polymorphic:bool -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit val add_section_constant : polymorphic:bool -> Names.constant -> Context.Named.t -> unit diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 004dd6801..b1b8aa288 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -241,7 +241,7 @@ let save_remaining_recthms { locality; polymorphic; object_kind } let k = IsAssumption Conjectural in let c = SectionLocalAssum { type_context = (t_i,ctx); polymorphic; - binding_kind = impl } + implicit_status = impl } in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) diff --git a/toplevel/command.ml b/toplevel/command.ml index 40c65b56f..7bb016d34 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -230,7 +230,7 @@ let declare_assumption is_coe assumption_kind (c,ctx) pl imps impl nl (_,ident) | Discharge when Lib.sections_are_opened () -> let entry = SectionLocalAssum { type_context = (c,ctx); polymorphic; - binding_kind = impl } + implicit_status = impl } in let decl = (Lib.cwd(), entry, IsAssumption kind) in let _ = declare_variable ident decl in diff --git a/toplevel/command.mli b/toplevel/command.mli index 2ae4cddd0..f0651a98c 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -55,7 +55,7 @@ val do_definition : Id.t -> definition_kind -> lident list option -> val declare_assumption : coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> Universes.universe_binders -> Impargs.manual_implicits -> - binding_kind -> Vernacexpr.inline -> variable Loc.located -> + implicit_status -> Vernacexpr.inline -> variable Loc.located -> global_reference * Univ.Instance.t * bool val do_assumptions : assumption_kind -> -- cgit v1.2.3