diff options
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 185 |
1 files changed, 91 insertions, 94 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 1699d600e..d7d9c743d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -12,6 +12,7 @@ open Pp open Names open Term +open EConstr open Environ (** printers *) @@ -20,59 +21,56 @@ val pr_sort_family : sorts_family -> std_ppcmds val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds (** 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 +val set_print_constr : (env -> Constr.constr -> std_ppcmds) -> unit +val print_constr : Constr.constr -> std_ppcmds +val print_constr_env : env -> Constr.constr -> std_ppcmds val print_named_context : env -> 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 (** about contexts *) -val push_rel_assum : Name.t * EConstr.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 push_rel_assum : Name.t * types -> env -> env +val push_rels_assum : (Name.t * Constr.types) list -> env -> env +val push_named_rec_types : Name.t array * Constr.types array * 'a -> env -> env -val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types +val lookup_rel_id : Id.t -> Context.Rel.t -> int * Constr.constr option * Constr.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)|] *) -val rel_vect : int -> int -> constr array -val rel_list : int -> int -> EConstr.constr list +val rel_vect : int -> int -> Constr.constr array +val rel_list : int -> int -> constr list (** iterators/destructors on terms *) val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types -val mkProd_wo_LetIn : Context.Rel.Declaration.t -> EConstr.types -> EConstr.types -val it_mkProd : EConstr.types -> (Name.t * EConstr.types) list -> EConstr.types -val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.constr +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 -> Context.Rel.t -> types -val it_mkProd_wo_LetIn : EConstr.types -> Context.Rel.t -> EConstr.types -val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr -val it_mkNamedProd_or_LetIn : EConstr.types -> Context.Named.t -> EConstr.types -val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types -val it_mkNamedLambda_or_LetIn : EConstr.constr -> Context.Named.t -> EConstr.constr +val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr +val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types +val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.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 -> Context.Rel.t -> constr +val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr (** {6 Generic iterators on constr} *) -val map_constr_with_named_binders : - (Name.t -> 'a -> 'a) -> - ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_binders_left_to_right : Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> EConstr.constr -> EConstr.constr) -> - 'a -> EConstr.constr -> EConstr.constr + ('a -> constr -> constr) -> + 'a -> constr -> constr val map_constr_with_full_binders : Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> EConstr.t -> EConstr.t) -> 'a -> EConstr.t -> EConstr.t + ('a -> constr -> constr) -> 'a -> constr -> constr (** [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 @@ -81,62 +79,61 @@ val map_constr_with_full_binders : index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -val fold_constr_with_binders : - Evd.evar_map -> ('a -> 'a) -> - ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b +val fold_constr_with_binders : Evd.evar_map -> + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val fold_constr_with_full_binders : - Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b +val fold_constr_with_full_binders : Evd.evar_map -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b val iter_constr_with_full_binders : - (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> - constr -> unit + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> Constr.constr -> unit) -> 'a -> + Constr.constr -> unit (**********************************************************************) -val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t -val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> EConstr.constr +val strip_head_cast : Evd.evar_map -> constr -> constr +val drop_extra_implicit_args : Evd.evar_map -> constr -> constr (** occur checks *) exception Occur -val occur_meta : Evd.evar_map -> EConstr.t -> bool -val occur_existential : Evd.evar_map -> EConstr.t -> bool -val occur_meta_or_existential : Evd.evar_map -> EConstr.t -> bool -val occur_evar : Evd.evar_map -> existential_key -> EConstr.t -> bool -val occur_var : env -> Evd.evar_map -> Id.t -> EConstr.t -> bool +val occur_meta : Evd.evar_map -> constr -> bool +val occur_existential : Evd.evar_map -> constr -> bool +val occur_meta_or_existential : Evd.evar_map -> constr -> bool +val occur_evar : Evd.evar_map -> existential_key -> constr -> bool +val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> Context.Named.Declaration.t -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) -val local_occur_var : Evd.evar_map -> Id.t -> EConstr.t -> bool +val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool -val free_rels : Evd.evar_map -> EConstr.t -> Int.Set.t +val free_rels : Evd.evar_map -> constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) -val dependent : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_univs : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_univs_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_in_decl : Evd.evar_map -> EConstr.t -> Context.Named.Declaration.t -> bool -val count_occurrences : Evd.evar_map -> EConstr.t -> EConstr.t -> int -val collect_metas : Evd.evar_map -> EConstr.t -> int list -val collect_vars : Evd.evar_map -> EConstr.t -> Id.Set.t (** for visible vars only *) +val dependent : Evd.evar_map -> constr -> constr -> bool +val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool +val dependent_univs : Evd.evar_map -> constr -> constr -> bool +val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool +val dependent_in_decl : Evd.evar_map -> constr -> Context.Named.Declaration.t -> bool +val count_occurrences : Evd.evar_map -> constr -> constr -> int +val collect_metas : Evd.evar_map -> constr -> int list +val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t -val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous of dependent *) +val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *) (* Substitution of metavariables *) -type meta_value_map = (metavariable * constr) list -val subst_meta : meta_value_map -> constr -> constr -val isMetaOf : Evd.evar_map -> metavariable -> EConstr.constr -> bool +type meta_value_map = (metavariable * Constr.constr) list +val subst_meta : meta_value_map -> Constr.constr -> Constr.constr +val isMetaOf : Evd.evar_map -> metavariable -> constr -> bool (** Type assignment for metavariables *) -type meta_type_map = (metavariable * types) list +type meta_type_map = (metavariable * Constr.types) list (** [pop c] lifts by -1 the positive indexes in [c] *) -val pop : EConstr.t -> constr +val pop : constr -> constr (** {6 ... } *) (** Substitution of an arbitrary large term. Uses equality modulo @@ -145,37 +142,37 @@ val pop : EConstr.t -> constr (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] as equality *) val subst_term_gen : Evd.evar_map -> - (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> EConstr.constr + (Evd.evar_map -> constr -> constr -> bool) -> constr -> constr -> constr (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] as equality *) val replace_term_gen : - Evd.evar_map -> (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> - EConstr.t -> EConstr.t -> EConstr.t -> constr + Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) -> + constr -> constr -> constr -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) -val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.constr +val subst_term : Evd.evar_map -> constr -> constr -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) -val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr +val replace_term : Evd.evar_map -> constr -> constr -> constr -> constr (** Alternative term equalities *) val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool -val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) -> - Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool -val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool -val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool (* FIXME rename: erases universes*) +val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> constr -> constr -> bool) -> + Reduction.conv_pb -> constr -> constr -> bool +val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> constr -> constr -> bool +val eq_constr : Evd.evar_map -> constr -> constr -> bool (* FIXME rename: erases universes*) -val eta_reduce_head : constr -> constr +val eta_reduce_head : Evd.evar_map -> constr -> constr (** Flattens application lists *) -val collapse_appl : Evd.evar_map -> EConstr.t -> constr +val collapse_appl : Evd.evar_map -> constr -> constr -val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t +val prod_applist : Evd.evar_map -> constr -> constr list -> constr (** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : Evd.evar_map -> EConstr.t -> EConstr.constr +val strip_outer_cast : Evd.evar_map -> constr -> constr exception CannotFilter @@ -185,32 +182,32 @@ 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 = (Context.Rel.t * constr) Evar.Map.t -val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst +type subst = (Context.Rel.t * Constr.constr) Evar.Map.t +val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> Constr.constr -> Constr.constr -> subst -val decompose_prod_letin : Evd.evar_map -> EConstr.t -> int * Context.Rel.t * constr -val align_prod_letin : Evd.evar_map -> EConstr.t -> EConstr.t -> Context.Rel.t * constr +val decompose_prod_letin : Evd.evar_map -> constr -> int * Context.Rel.t * constr +val align_prod_letin : Evd.evar_map -> 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) *) -val nb_lam : Evd.evar_map -> EConstr.t -> int +val nb_lam : Evd.evar_map -> constr -> int (** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : Evd.evar_map -> EConstr.t -> int +val nb_prod : Evd.evar_map -> constr -> int (** Similar to [nb_prod], but zeta-contracts let-in on the way *) -val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int +val nb_prod_modulo_zeta : Evd.evar_map -> constr -> int (** Get the last arg of a constr intended to be an application *) -val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr +val last_arg : Evd.evar_map -> constr -> constr (** Force the decomposition of a term as an applicative one *) -val decompose_app_vect : Evd.evar_map -> EConstr.t -> EConstr.constr * EConstr.constr array +val decompose_app_vect : Evd.evar_map -> constr -> constr * constr array -val adjust_app_list_size : EConstr.constr -> EConstr.constr list -> EConstr.constr -> EConstr.constr list -> - (EConstr.constr * EConstr.constr list * EConstr.constr * EConstr.constr list) -val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> - (EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.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.t list @@ -239,15 +236,15 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) 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 assums_of_rel_context : Context.Rel.t -> (Name.t * Constr.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 substl_rel_context : Constr.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 -> Context.Rel.t -> Context.Rel.t + (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t val map_rel_context_with_binders : - (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t + (int -> Constr.constr -> Constr.constr) -> Context.Rel.t -> Context.Rel.t val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a @@ -256,10 +253,10 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env -val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list -val global_vars_set : env -> Evd.evar_map -> EConstr.t -> Id.Set.t +val global_vars : env -> Evd.evar_map -> constr -> Id.t list +val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t -val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option +val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) @@ -268,15 +265,15 @@ val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> I (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses +val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses -val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool +val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool -val isGlobalRef : Evd.evar_map -> EConstr.t -> bool +val isGlobalRef : Evd.evar_map -> constr -> bool -val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool +val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool -val is_Prop : Evd.evar_map -> EConstr.t -> bool +val is_Prop : Evd.evar_map -> constr -> bool (** Combinators on judgments *) @@ -285,5 +282,5 @@ val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) puns val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment (** {6 Functions to deal with impossible cases } *) -val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit +val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set |