diff options
Diffstat (limited to 'checker/term.mli')
| -rw-r--r-- | checker/term.mli | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/checker/term.mli b/checker/term.mli new file mode 100644 index 00000000..30a2c03a --- /dev/null +++ b/checker/term.mli @@ -0,0 +1,111 @@ +open Names + +type existential_key = int +type metavariable = int +type case_style = + LetStyle + | IfStyle + | LetPatternStyle + | MatchStyle + | RegularStyle +type case_printing = { ind_nargs : int; style : case_style; } +type case_info = { + ci_ind : inductive; + ci_npar : int; + ci_cstr_nargs : int array; + ci_pp_info : case_printing; +} +type contents = Pos | Null +type sorts = Prop of contents | Type of Univ.universe +type sorts_family = InProp | InSet | InType +val family_of_sort : sorts -> sorts_family +type 'a pexistential = existential_key * 'a array +type 'a prec_declaration = name array * 'a array * 'a array +type 'a pfixpoint = (int array * int) * 'a prec_declaration +type 'a pcofixpoint = int * 'a prec_declaration +type cast_kind = VMcast | DEFAULTcast +type constr = + Rel of int + | Var of identifier + | Meta of metavariable + | Evar of constr pexistential + | Sort of sorts + | Cast of constr * cast_kind * constr + | Prod of name * constr * constr + | Lambda of name * constr * constr + | LetIn of name * constr * constr * constr + | App of constr * constr array + | Const of constant + | Ind of inductive + | Construct of constructor + | Case of case_info * constr * constr * constr array + | Fix of constr pfixpoint + | CoFix of constr pcofixpoint +type existential = constr pexistential +type rec_declaration = constr prec_declaration +type fixpoint = constr pfixpoint +type cofixpoint = constr pcofixpoint +val strip_outer_cast : constr -> constr +val collapse_appl : constr -> constr +val decompose_app : constr -> constr * constr list +val applist : constr * constr list -> constr +val iter_constr_with_binders : + ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +exception LocalOccur +val closedn : int -> constr -> bool +val closed0 : constr -> bool +val noccurn : int -> constr -> bool +val noccur_between : int -> int -> constr -> bool +val noccur_with_meta : int -> int -> constr -> bool +val map_constr_with_binders : + ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr +val exliftn : Esubst.lift -> constr -> constr +val liftn : int -> int -> constr -> constr +val lift : int -> constr -> constr +type info = Closed | Open | Unknown +type 'a substituend = { mutable sinfo : info; sit : 'a; } +val lift_substituend : int -> constr substituend -> constr +val make_substituend : 'a -> 'a substituend +val substn_many : constr substituend array -> int -> constr -> constr +val substnl : constr list -> int -> constr -> constr +val substl : constr list -> constr -> constr +val subst1 : constr -> constr -> constr + +type named_declaration = identifier * constr option * constr +type rel_declaration = name * constr option * constr +val map_named_declaration : + (constr -> constr) -> named_declaration -> named_declaration +val map_rel_declaration : + (constr -> constr) -> rel_declaration -> rel_declaration +val fold_named_declaration : + (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a +val fold_rel_declaration : + (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a +type named_context = named_declaration list +val empty_named_context : named_context +val fold_named_context : + (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a +type section_context = named_context +type rel_context = rel_declaration list +val empty_rel_context : rel_context +val rel_context_length : rel_context -> int +val rel_context_nhyps : rel_context -> int +val fold_rel_context : + (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a +val map_context : (constr -> constr) -> named_context -> named_context +val map_rel_context : (constr -> constr) -> rel_context -> rel_context +val extended_rel_list : int -> rel_context -> constr list +val compose_lam : (name * constr) list -> constr -> constr +val decompose_lam : constr -> (name * constr) list * constr +val decompose_lam_n_assum : int -> constr -> rel_context * constr +val mkProd_or_LetIn : name * constr option * constr -> constr -> constr +val it_mkProd_or_LetIn : constr -> rel_context -> constr +val decompose_prod_assum : constr -> rel_context * constr +val decompose_prod_n_assum : int -> constr -> rel_context * constr + +type arity = rel_context * sorts +val mkArity : arity -> constr +val destArity : constr -> arity +val isArity : constr -> bool +val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool +val eq_constr : constr -> constr -> bool |