diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 147 |
1 files changed, 94 insertions, 53 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 91c76564..5448d97c 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: termops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Util open Pp open Names @@ -15,7 +13,8 @@ open Term open Sign open Environ -(* Universes *) +(** 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 @@ -23,10 +22,11 @@ val new_Type_sort : unit -> sorts val refresh_universes : types -> types val refresh_universes_strict : types -> types -(* printers *) +(** printers *) val print_sort : sorts -> std_ppcmds val pr_sort_family : sorts_family -> std_ppcmds -(* debug printer: do not use to display terms to the casual user... *) + +(** debug printer: do not use to display terms to the casual user... *) val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds val print_constr_env : env -> constr -> std_ppcmds @@ -35,35 +35,34 @@ val pr_rel_decl : env -> rel_declaration -> std_ppcmds val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds -(* about contexts *) +(** 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 *) +(** builds argument lists matching a block of binders or a context *) 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 *) +(** iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkProd_wo_LetIn : rel_declaration -> types -> types -val it_mkProd : init:types -> (name * types) list -> types -val it_mkLambda : init:constr -> (name * types) list -> constr -val it_mkProd_or_LetIn : init:types -> rel_context -> types -val it_mkProd_wo_LetIn : init:types -> rel_context -> types -val it_mkLambda_or_LetIn : init:constr -> rel_context -> constr -val it_mkNamedProd_or_LetIn : init:types -> named_context -> types -val it_mkNamedProd_wo_LetIn : init:types -> named_context -> types -val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr +val it_mkProd : types -> (name * types) list -> types +val it_mkLambda : constr -> (name * 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_named_context_quantifier : (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a -(**********************************************************************) -(* Generic iterators on constr *) +(** {6 Generic iterators on constr} *) val map_constr_with_named_binders : (name -> 'a -> 'a) -> @@ -76,7 +75,7 @@ val map_constr_with_full_binders : (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr -(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate +(** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to right according to the usual representation of the constructions as [fold_constr] but it carries an extra data [n] (typically a lift @@ -93,8 +92,9 @@ val iter_constr_with_full_binders : (**********************************************************************) val strip_head_cast : constr -> constr +val drop_extra_implicit_args : constr -> constr -(* occur checks *) +(** occur checks *) exception Occur val occur_meta : types -> bool val occur_existential : types -> bool @@ -108,68 +108,96 @@ val occur_var_in_decl : val free_rels : constr -> Intset.t val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool +val count_occurrences : constr -> constr -> int val collect_metas : constr -> int list -val occur_term : constr -> constr -> bool (* Synonymous - of dependent *) -(* Substitution of metavariables *) +val collect_vars : constr -> Idset.t (** for visible vars only *) +val occur_term : constr -> constr -> bool (** Synonymous + of dependent + Substitution of metavariables *) type meta_value_map = (metavariable * constr) list val subst_meta : meta_value_map -> constr -> constr -(* Type assignment for metavariables *) +(** Type assignment for metavariables *) type meta_type_map = (metavariable * types) list -(* [pop c] lifts by -1 the positive indexes in [c] *) +(** [pop c] lifts by -1 the positive indexes in [c] *) val pop : constr -> constr -(*s Substitution of an arbitrary large term. Uses equality modulo +(** {6 ... } *) +(** Substitution of an arbitrary large term. Uses equality modulo reduction of let *) -(* [subst_term_gen eq d c] replaces [Rel 1] by [d] in [c] using [eq] +(** [subst_term_gen eq d c] replaces [Rel 1] by [d] in [c] using [eq] as equality *) val subst_term_gen : (constr -> constr -> bool) -> constr -> constr -> constr -(* [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] +(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] as equality *) val replace_term_gen : (constr -> constr -> bool) -> constr -> constr -> constr -> constr -(* [subst_term d c] replaces [Rel 1] by [d] in [c] *) +(** [subst_term d c] replaces [Rel 1] by [d] in [c] *) val subst_term : constr -> constr -> constr -(* [replace_term d e c] replaces [d] by [e] in [c] *) +(** [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 *) +(** 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_term_occ_gen occl n c d] replaces occurrences of [c] at +(** [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_term_occ_gen : +val subst_closed_term_occ_gen : occurrences -> int -> constr -> types -> int * types -(* [subst_term_occ occl c d] replaces occurrences of [c] at - positions [occl] by [Rel 1] in [d] (see also Note OCC) *) -val subst_term_occ : occurrences -> constr -> constr -> constr - -(* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at - positions [occl] by [Rel 1] in [decl] *) +(** [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 *) +type hyp_location_flag = (** To distinguish body and type of local defs *) | InHyp | InHypTypeOnly | InHypValueOnly -val subst_term_occ_decl : +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 *) +(** 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 @@ -181,7 +209,7 @@ val eta_eq_constr : constr -> constr -> bool exception CannotFilter -(* Lightweight first-order filtering procedure. Unification +(** Lightweight first-order filtering procedure. Unification variables ar represented by (untyped) Evars. [filtering c1 c2] returns the substitution n'th evar -> (context,term), or raises [CannotFilter]. @@ -193,10 +221,18 @@ 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 -(* Get the last arg of a constr intended to be an application *) +(** Get the last arg of a constr intended to be an application *) val last_arg : constr -> constr -(* name contexts *) +(** Force the decomposition of a term as an applicative one *) +val decompose_app_vect : constr -> constr * constr array + +val adjust_app_list_size : constr -> constr list -> constr -> constr list -> + (constr * constr list * constr * constr list) +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 @@ -207,18 +243,19 @@ val ids_of_named_context : named_context -> identifier list val ids_of_context : env -> identifier list val names_of_rel_context : env -> names_context -val context_chop : int -> rel_context -> (rel_context*rel_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 *) +(** Set of local names *) val vars_of_env: env -> Idset.t val add_vname : Idset.t -> name -> Idset.t -(* other signature iterators *) +(** other signature iterators *) val process_rel_context : (rel_declaration -> env -> env) -> env -> env val assums_of_rel_context : rel_context -> (name * 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 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 @@ -234,19 +271,23 @@ val clear_named_body : identifier -> env -> env val global_vars : env -> constr -> identifier list val global_vars_set_of_decl : env -> named_declaration -> Idset.t -(* Gives an ordered list of hypotheses, closed by dependencies, +(** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) val dependency_closure : env -> named_context -> Idset.t -> identifier list -(* Test if an identifier is the basename of a global reference *) +(** Test if an identifier is the basename of a global reference *) val is_section_variable : identifier -> bool val isGlobalRef : constr -> bool val has_polymorphic_type : constant -> bool -(* Combinators on judgments *) +(** Combinators on judgments *) val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment 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 |