From 663922262bc9bcc8876f7e12910f6294fc964753 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 24 Aug 2016 15:31:28 +0200 Subject: Changing the definition of the "Lib.variable.info" type to enable us to do more cleanups --- interp/notation.ml | 3 ++- kernel/names.ml | 3 +++ kernel/names.mli | 3 +++ library/impargs.ml | 9 +++------ library/lib.ml | 22 ++++++++-------------- library/lib.mli | 3 +-- pretyping/arguments_renaming.ml | 2 +- pretyping/typeclasses.ml | 10 ++++------ 8 files changed, 25 insertions(+), 30 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d..3e3523d76 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -686,7 +686,8 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = let n = try let vars = Lib.variable_section_segment_of_reference r in - List.length (List.filter (fun (_,_,b,_) -> b = None) vars) + let open Context.Named.Declaration in + vars |> List.map fst |> List.filter is_local_assum |> List.length with Not_found (* Not a ref defined in this section *) -> 0 in Some (req,Lib.discharge_global r,n,l,[]) diff --git a/kernel/names.ml b/kernel/names.ml index 9267a64d6..d673c91e8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -82,6 +82,9 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let mk_name id = + Name id + let is_anonymous = function | Anonymous -> true | Name _ -> false diff --git a/kernel/names.mli b/kernel/names.mli index feaedc775..0af1cde8f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -82,6 +82,9 @@ sig type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + val mk_name : Id.t -> t + (** constructor *) + val is_anonymous : t -> bool (** Return [true] iff a given name is [Anonymous]. *) diff --git a/library/impargs.ml b/library/impargs.ml index bce7a15cb..3ddef3a9a 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -515,14 +515,11 @@ let subst_implicits (subst,(req,l)) = (ImplLocal,List.smartmap (subst_implicits_decl subst) l) let impls_of_context ctx = - let map (id, impl, _, _) = match impl with - | Implicit -> Some (id, Manual, (true, true)) + let map (decl, impl) = match impl with + | Implicit -> Some (Context.Named.Declaration.get_id decl, Manual, (true, true)) | _ -> None in - let is_set (_, _, b, _) = match b with - | None -> true - | Some _ -> false - in + let is_set = Context.Named.Declaration.is_local_assum % fst in List.rev_map map (List.filter is_set ctx) let adjust_side_condition p = function diff --git a/library/lib.ml b/library/lib.ml index 8880a8b15..7fc3e0d9c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -388,7 +388,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -431,9 +431,8 @@ let extract_hyps (secs,ohyps) = let open Context.Named.Declaration in let rec aux = function | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) -> - let (id',b,t) = to_tuple decl in let l, r = aux (idl,hyps) in - (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r + (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r ctx else r @@ -443,17 +442,12 @@ let extract_hyps (secs,ohyps) = | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) -let instance_from_variable_context sign = - let rec inst_rec = function - | (id,b,None,_) :: sign -> id :: inst_rec sign - | _ :: sign -> inst_rec sign - | [] -> [] in - Array.of_list (inst_rec sign) - -let named_of_variable_context ctx = let open Context.Named.Declaration in - List.map (function id,_,None,t -> LocalAssum (id,t) - | id,_,Some b,t -> LocalDef (id,b,t)) - ctx +let instance_from_variable_context = + let open Context.Named.Declaration in + Array.of_list % List.map get_id % List.filter is_local_assum % List.map fst + +let named_of_variable_context = + List.map fst let add_section_replacement f g poly hyps = match !sectab with diff --git a/library/lib.mli b/library/lib.mli index 7080b5dba..092643c2d 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -162,8 +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 = Names.Id.t * Decl_kinds.binding_kind * - Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ca1d0b7fb..bf9063fdb 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -48,7 +48,7 @@ let discharge_rename_args = function (try let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in - let var_names = List.map (fun (id, _,_,_) -> Name id) vars in + let var_names = List.map (Name.mk_name % Context.Named.Declaration.get_id % fst) vars in let names' = List.map (fun l -> var_names @ l) names in Some (ReqGlobal (c', names), (c', names')) with Not_found -> Some req) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2c675b9ea..9fff64ae5 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -197,12 +197,10 @@ let subst_class (subst,cl) = let discharge_class (_,cl) = let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right - ( fun (n,_,b,t) (ctx', subst) -> - let decl = match b with - | None -> LocalAssum (Name n, substn_vars 1 subst t) - | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t) - in - (decl :: ctx', n :: subst) + ( fun (decl,_) (ctx', subst) -> + let open Context.Named.Declaration in + let decl' = decl |> map_constr (substn_vars 1 subst) |> to_rel in + (decl' :: ctx', Context.Named.Declaration.get_id decl :: subst) ) ctx ([], []) in let discharge_rel_context subst n rel = let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in -- cgit v1.2.3