diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 158 |
1 files changed, 55 insertions, 103 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 81b23d7e..9f3efd72 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -1,30 +1,22 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Pp open Names open Term -open Sign +open Context open Environ - -(** Universes *) -val new_univ_level : unit -> Univ.universe_level -val new_univ : unit -> Univ.universe -val new_sort_in_family : sorts_family -> sorts -val new_Type : unit -> types -val new_Type_sort : unit -> sorts -val refresh_universes : types -> types -val refresh_universes_strict : types -> types +open Locus (** printers *) val print_sort : sorts -> std_ppcmds val pr_sort_family : sorts_family -> std_ppcmds +val pr_fix : (constr -> std_ppcmds) -> fixpoint -> std_ppcmds (** debug printer: do not use to display terms to the casual user... *) val set_print_constr : (env -> constr -> std_ppcmds) -> unit @@ -36,12 +28,19 @@ val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds (** about contexts *) -val push_rel_assum : name * types -> env -> env -val push_rels_assum : (name * types) list -> env -> env -val push_named_rec_types : name array * types array * 'a -> env -> env -val lookup_rel_id : identifier -> rel_context -> int * constr option * types - -(** builds argument lists matching a block of binders or a context *) +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 +(** Associates the contents of an identifier in a [rel_context]. Raise + [Not_found] if there is no such identifier. *) + +(** 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 @@ -50,8 +49,8 @@ val extended_rel_vect : int -> rel_context -> constr array (** iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkProd_wo_LetIn : rel_declaration -> types -> types -val it_mkProd : types -> (name * types) list -> types -val it_mkLambda : constr -> (name * types) list -> constr +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 @@ -59,13 +58,14 @@ 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_named_context_quantifier : - (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a +(* 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 (** {6 Generic iterators on constr} *) val map_constr_with_named_binders : - (name -> 'a -> 'a) -> + (Name.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_binders_left_to_right : (rel_declaration -> 'a -> 'a) -> @@ -99,18 +99,22 @@ exception Occur val occur_meta : types -> bool val occur_existential : types -> bool val occur_meta_or_existential : types -> bool -val occur_const : constant -> types -> bool val occur_evar : existential_key -> types -> bool -val occur_var : env -> identifier -> types -> bool +val occur_var : env -> Id.t -> types -> bool val occur_var_in_decl : env -> - identifier -> 'a * types option * types -> bool -val free_rels : constr -> Intset.t + Id.t -> 'a * types option * types -> bool +val free_rels : constr -> Int.Set.t + +(** [dependent m t] tests whether [m] is a subterm of [t] *) 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 count_occurrences : constr -> constr -> int val collect_metas : constr -> int list -val collect_vars : constr -> Idset.t (** for visible vars only *) +val collect_vars : constr -> Id.Set.t (** for visible vars only *) val occur_term : constr -> constr -> bool (** Synonymous of dependent Substitution of metavariables *) @@ -144,68 +148,14 @@ val subst_term : constr -> constr -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : constr -> constr -> constr -> constr -(** In occurrences sets, false = everywhere except and true = nowhere except *) -type occurrences = bool * int list -val all_occurrences : occurrences -val no_occurrences_in_set : occurrences - -(** [subst_closed_term_occ_gen occl n c d] replaces occurrences of closed [c] at - positions [occl], counting from [n], by [Rel 1] in [d] *) -val subst_closed_term_occ_gen : - occurrences -> int -> constr -> types -> int * types - -(** [subst_closed_term_occ_modulo] looks for subterm modulo a - testing function returning a substitution of type ['a] (or failing - with NotUnifiable); a function for merging substitution (possibly - failing with NotUnifiable) and an initial substitution are - required too *) - -type hyp_location_flag = (** To distinguish body and type of local defs *) - | InHyp - | InHypTypeOnly - | InHypValueOnly - -type 'a testing_function = { - match_fun : constr -> 'a; - merge_fun : 'a -> 'a -> 'a; - mutable testing_state : 'a; - mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option -} - -val make_eq_test : constr -> unit testing_function - -exception NotUnifiable - -val subst_closed_term_occ_modulo : - occurrences -> 'a testing_function -> (identifier * hyp_location_flag) option - -> constr -> types - -(** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at - positions [occl] by [Rel 1] in [d] (see also Note OCC) *) -val subst_closed_term_occ : occurrences -> constr -> constr -> constr - -(** [subst_closed_term_occ_decl occl c decl] replaces occurrences of closed [c] - at positions [occl] by [Rel 1] in [decl] *) - -val subst_closed_term_occ_decl : - occurrences * hyp_location_flag -> constr -> named_declaration -> - named_declaration - -val subst_closed_term_occ_decl_modulo : - occurrences * hyp_location_flag -> 'a testing_function -> - named_declaration -> named_declaration - -val error_invalid_occurrence : int list -> 'a - (** Alternative term equalities *) val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) -> Reduction.conv_pb -> constr -> constr -> bool val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool -val eq_constr : constr -> constr -> bool +val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*) val eta_reduce_head : constr -> constr -val eta_eq_constr : constr -> constr -> bool exception CannotFilter @@ -215,7 +165,7 @@ 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) Intmap.t +type subst = (rel_context*constr) Evar.Map.t val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst val decompose_prod_letin : constr -> int * rel_context * constr @@ -233,26 +183,26 @@ val adjust_app_array_size : constr -> constr array -> constr -> constr array -> (constr * constr array * constr * constr array) (** name contexts *) -type names_context = name list -val add_name : name -> names_context -> names_context -val lookup_name_of_rel : int -> names_context -> name -val lookup_rel_of_name : identifier -> names_context -> int +type names_context = Name.t list +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 -> identifier list -val ids_of_named_context : named_context -> identifier list -val ids_of_context : env -> identifier list +val ids_of_rel_context : rel_context -> Id.t list +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 val context_chop : int -> rel_context -> rel_context * rel_context val env_rel_context_chop : int -> env -> env * rel_context (** Set of local names *) -val vars_of_env: env -> Idset.t -val add_vname : Idset.t -> name -> Idset.t +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 * constr) list +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 *) @@ -264,23 +214,25 @@ val map_rel_context_with_binders : val fold_named_context_both_sides : ('a -> named_declaration -> named_declaration list -> 'a) -> named_context -> init:'a -> 'a -val mem_named_context : identifier -> named_context -> bool +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 -val clear_named_body : identifier -> env -> env +val clear_named_body : Id.t -> env -> env -val global_vars : env -> constr -> identifier list -val global_vars_set_of_decl : env -> named_declaration -> Idset.t +val global_vars : env -> constr -> Id.t list +val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) -val dependency_closure : env -> named_context -> Idset.t -> identifier list +val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list (** Test if an identifier is the basename of a global reference *) -val is_section_variable : identifier -> bool +val is_section_variable : Id.t -> bool val isGlobalRef : constr -> bool -val has_polymorphic_type : constant -> bool +val is_template_polymorphic : env -> constr -> bool (** Combinators on judgments *) @@ -289,5 +241,5 @@ val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment (** {6 Functions to deal with impossible cases } *) -val set_impossible_default_clause : constr * types -> unit -val coq_unit_judge : unit -> unsafe_judgment +val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit +val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set |