From 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Nov 2015 09:54:42 +0100 Subject: Moving three related small half-general half-ad-hoc utility functions next to each other, waiting for possible integration into a more uniform API. --- engine/termops.mli | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 6c680005db..5d812131ed 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -174,6 +174,16 @@ val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst val decompose_prod_letin : constr -> int * rel_context * constr val align_prod_letin : constr -> constr -> rel_context * constr +(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction + gives {% $ %}n{% $ %} (casts are ignored) *) +val nb_lam : constr -> int + +(** Similar to [nb_lam], but gives the number of products instead *) +val nb_prod : constr -> int + +(** Similar to [nb_prod], but zeta-contracts let-in on the way *) +val nb_prod_modulo_zeta : constr -> int + (** Get the last arg of a constr intended to be an application *) val last_arg : constr -> constr -- cgit v1.2.3 From ade2363e357db3ac3f258e645fe6bba988e7e7dd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 19 Nov 2015 22:49:25 +0100 Subject: About building of substitutions from instances. Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev. --- engine/termops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 5d812131ed..94c485a261 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -219,7 +219,7 @@ val assums_of_rel_context : rel_context -> (Name.t * constr) list val lift_rel_context : int -> rel_context -> rel_context val substl_rel_context : constr list -> rel_context -> rel_context val smash_rel_context : rel_context -> rel_context (** expand lets in context *) -val adjust_subst_to_rel_context : rel_context -> constr list -> constr list + val map_rel_context_in_env : (env -> constr -> constr) -> env -> rel_context -> rel_context val map_rel_context_with_binders : -- cgit v1.2.3 From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:17:21 +0100 Subject: Moving extended_rel_vect/extended_rel_list to the kernel. It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. --- engine/termops.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 94c485a261..87f74f7435 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -37,13 +37,9 @@ val lookup_rel_id : Id.t -> rel_context -> int * constr option * types (** Functions that build argument lists matching a block of binders or a context. [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|] - [extended_rel_vect n ctx] extends the [ctx] context of length [m] - with [n] elements. *) val rel_vect : int -> int -> constr array val rel_list : int -> int -> constr list -val extended_rel_list : int -> rel_context -> constr list -val extended_rel_vect : int -> rel_context -> constr array (** iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types -- cgit v1.2.3 From a582737fc27da2c03c8c57c773fc4854c1e88d7a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Dec 2015 14:03:12 +0100 Subject: API: documenting context_chop and removing a duplicate. --- engine/termops.mli | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 87f74f7435..6083f1ab59 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -202,7 +202,14 @@ val ids_of_named_context : named_context -> Id.t list val ids_of_context : env -> Id.t list val names_of_rel_context : env -> names_context +(* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has + [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, + starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) val context_chop : int -> rel_context -> rel_context * rel_context + +(* [env_rel_context_chop n env] extracts out the [n] top declarations + of the rel_context part of [env], counting both local definitions and + hypotheses *) val env_rel_context_chop : int -> env -> env * rel_context (** Set of local names *) -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- engine/termops.mli | 77 +++++++++++++++++++++++++++--------------------------- 1 file changed, 38 insertions(+), 39 deletions(-) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 6083f1ab59..0fbd1ee82e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -9,7 +9,6 @@ open Pp open Names open Term -open Context open Environ (** printers *) @@ -22,7 +21,7 @@ val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds val print_constr_env : env -> constr -> std_ppcmds val print_named_context : env -> std_ppcmds -val pr_rel_decl : env -> rel_declaration -> std_ppcmds +val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds @@ -31,7 +30,7 @@ val push_rel_assum : Name.t * types -> env -> env val push_rels_assum : (Name.t * types) list -> env -> env val push_named_rec_types : Name.t array * types array * 'a -> env -> env -val lookup_rel_id : Id.t -> rel_context -> int * constr option * types +val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types (** Associates the contents of an identifier in a [rel_context]. Raise [Not_found] if there is no such identifier. *) @@ -42,20 +41,20 @@ val rel_vect : int -> int -> constr array val rel_list : int -> int -> constr list (** iterators/destructors on terms *) -val mkProd_or_LetIn : rel_declaration -> types -> types -val mkProd_wo_LetIn : rel_declaration -> types -> types +val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types +val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types val it_mkProd : types -> (Name.t * types) list -> types val it_mkLambda : constr -> (Name.t * types) list -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types -val it_mkProd_wo_LetIn : types -> rel_context -> types -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkNamedProd_or_LetIn : types -> named_context -> types -val it_mkNamedProd_wo_LetIn : types -> named_context -> types -val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr +val it_mkProd_or_LetIn : types -> Context.Rel.t -> types +val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr +val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types +val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types +val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr +val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr (** {6 Generic iterators on constr} *) @@ -63,11 +62,11 @@ val map_constr_with_named_binders : (Name.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_binders_left_to_right : - (rel_declaration -> 'a -> 'a) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate @@ -81,11 +80,11 @@ val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b val fold_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b val iter_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit (**********************************************************************) @@ -110,7 +109,7 @@ val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool val dependent_univs : constr -> constr -> bool val dependent_univs_no_evar : constr -> constr -> bool -val dependent_in_decl : constr -> named_declaration -> bool +val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool val count_occurrences : constr -> constr -> int val collect_metas : constr -> int list val collect_vars : constr -> Id.Set.t (** for visible vars only *) @@ -164,11 +163,11 @@ exception CannotFilter (context,term), or raises [CannotFilter]. Warning: Outer-kernel sort subtyping are taken into account: c1 has to be smaller than c2 wrt. sorts. *) -type subst = (rel_context*constr) Evar.Map.t -val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst +type subst = (Context.Rel.t * constr) Evar.Map.t +val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst -val decompose_prod_letin : constr -> int * rel_context * constr -val align_prod_letin : constr -> constr -> rel_context * constr +val decompose_prod_letin : constr -> int * Context.Rel.t * constr +val align_prod_letin : constr -> constr -> Context.Rel.t * constr (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) @@ -197,51 +196,51 @@ val add_name : Name.t -> names_context -> names_context val lookup_name_of_rel : int -> names_context -> Name.t val lookup_rel_of_name : Id.t -> names_context -> int val empty_names_context : names_context -val ids_of_rel_context : rel_context -> Id.t list -val ids_of_named_context : named_context -> Id.t list +val ids_of_rel_context : Context.Rel.t -> Id.t list +val ids_of_named_context : Context.Named.t -> Id.t list val ids_of_context : env -> Id.t list val names_of_rel_context : env -> names_context (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) -val context_chop : int -> rel_context -> rel_context * rel_context +val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t (* [env_rel_context_chop n env] extracts out the [n] top declarations of the rel_context part of [env], counting both local definitions and hypotheses *) -val env_rel_context_chop : int -> env -> env * rel_context +val env_rel_context_chop : int -> env -> env * Context.Rel.t (** Set of local names *) val vars_of_env: env -> Id.Set.t val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) -val process_rel_context : (rel_declaration -> env -> env) -> env -> env -val assums_of_rel_context : rel_context -> (Name.t * constr) list -val lift_rel_context : int -> rel_context -> rel_context -val substl_rel_context : constr list -> rel_context -> rel_context -val smash_rel_context : rel_context -> rel_context (** expand lets in context *) +val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env +val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list +val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t +val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t +val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *) val map_rel_context_in_env : - (env -> constr -> constr) -> env -> rel_context -> rel_context + (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t val map_rel_context_with_binders : - (int -> constr -> constr) -> rel_context -> rel_context + (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t val fold_named_context_both_sides : - ('a -> named_declaration -> named_declaration list -> 'a) -> - named_context -> init:'a -> 'a -val mem_named_context : Id.t -> named_context -> bool -val compact_named_context : named_context -> named_list_context -val compact_named_context_reverse : named_context -> named_list_context + ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> + Context.Named.t -> init:'a -> 'a +val mem_named_context : Id.t -> Context.Named.t -> bool +val compact_named_context : Context.Named.t -> Context.NamedList.t +val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t val clear_named_body : Id.t -> env -> env val global_vars : env -> constr -> Id.t list -val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t +val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) -val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list +val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -- cgit v1.2.3 From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: CLEANUP: Context.{Rel,Named}.Declaration.t Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- engine/termops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 720ed3bd67..c2a4f33235 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -101,7 +101,7 @@ val occur_evar : existential_key -> types -> bool val occur_var : env -> Id.t -> types -> bool val occur_var_in_decl : env -> - Id.t -> 'a * types option * types -> bool + Id.t -> Context.Named.Declaration.t -> bool val free_rels : constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) -- cgit v1.2.3