diff options
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 82 |
1 files changed, 53 insertions, 29 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 3b0c4bba64..eef8452e64 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -17,9 +17,10 @@ open Environ open EConstr (** printers *) -val print_sort : Sorts.t -> Pp.t val pr_sort_family : Sorts.family -> Pp.t +[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"] val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t +[@@ocaml.deprecated "Use [Constr.debug_print_fix]"] (** about contexts *) val push_rel_assum : Name.t * types -> env -> env @@ -43,14 +44,14 @@ 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.constr -> Context.Rel.t -> Constr.constr +val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr val it_mkNamedProd_or_LetIn : types -> named_context -> types -val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types +val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types val it_mkNamedLambda_or_LetIn : constr -> named_context -> 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.constr -> Context.Rel.t -> Constr.constr +val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr (** {6 Generic iterators on constr} *) @@ -63,6 +64,10 @@ val map_constr_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr +val map_constr_with_full_binders_user_view : + Evd.evar_map -> + (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 subterms of [c] starting from [acc] and proceeding from left to @@ -75,13 +80,15 @@ 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 -> constr -> 'b) -> - 'a -> 'b -> constr -> 'b + (rel_declaration -> 'a -> 'a) -> + ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b val iter_constr_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."] (**********************************************************************) @@ -94,6 +101,7 @@ exception Occur 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_metavariable : Evd.evar_map -> metavariable -> constr -> bool val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool val occur_var_in_decl : @@ -112,9 +120,9 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> 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 -> constr -> constr -> bool (** Synonymous of dependent *) -[@@ocaml.deprecated "alias of Termops.dependent"] + +val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t +[@@ocaml.deprecated "Use [Environ.vars_of_global]"] (* Substitution of metavariables *) type meta_value_map = (metavariable * Constr.constr) list @@ -225,7 +233,7 @@ 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 -> Context.Rel.t -> Context.Rel.t * Context.Rel.t +val context_chop : int -> Constr.rel_context -> Constr.rel_context * Constr.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 @@ -239,19 +247,19 @@ 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 : ('c, 't) Context.Rel.pt -> (Name.t * 't) list -val lift_rel_context : int -> 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 lift_rel_context : int -> Constr.rel_context -> Constr.rel_context +val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context +val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *) val map_rel_context_in_env : - (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t + (env -> Constr.constr -> Constr.constr) -> env -> Constr.rel_context -> Constr.rel_context val map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt val fold_named_context_both_sides : - ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> - Context.Named.t -> init:'a -> 'a + ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> + Constr.named_context -> init:'a -> 'a val mem_named_context_val : Id.t -> named_context_val -> bool -val compact_named_context : Context.Named.t -> Context.Compacted.t +val compact_named_context : Constr.named_context -> Constr.compacted_context val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt @@ -261,7 +269,7 @@ val clear_named_body : Id.t -> env -> env 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 -> named_declaration -> Id.Set.t -val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option +val global_app_of_constr : Evd.evar_map -> constr -> (GlobRef.t * EInstance.t) * constr option (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) @@ -270,19 +278,19 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id. (** 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 -> constr -> Globnames.global_reference * EInstance.t +val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t -val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool +val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool val isGlobalRef : Evd.evar_map -> constr -> bool -val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool +val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool val is_Type : Evd.evar_map -> constr -> bool -val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid (** Combinators on judgments *) @@ -298,21 +306,37 @@ val pr_existential_key : evar_map -> Evar.t -> Pp.t val pr_evar_suggested_name : Evar.t -> evar_map -> Id.t -val pr_evar_info : evar_info -> Pp.t +val pr_evar_info : env -> evar_map -> evar_info -> Pp.t val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t -val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t +val pr_evar_map : ?with_univs:bool -> int option -> env -> evar_map -> Pp.t val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> - evar_map -> Pp.t + env -> evar_map -> Pp.t val pr_metaset : Metaset.t -> Pp.t val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t -(** debug printer: do not use to display terms to the casual user... *) +module Internal : sig -val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit -val print_constr : constr -> Pp.t +(** NOTE: to print terms you always want to use functions in + Printer, not these ones which are for very special cases. *) + +(** debug printers: print raw form for terms, both with + evar-substitution and without. *) +val debug_print_constr : constr -> Pp.t +val debug_print_constr_env : env -> evar_map -> constr -> Pp.t + +(** Pretty-printer hook: [print_constr_env env sigma c] will pretty + print c if the pretty printing layer has been linked into the Coq + binary. *) val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t + +(** [set_print_constr f] sets f to be the pretty printer *) +val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit + +(** Printers for contexts *) val print_named_context : env -> Pp.t -val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t +val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t + +end |