diff options
Diffstat (limited to 'checker/term.mli')
| -rw-r--r-- | checker/term.mli | 66 |
1 files changed, 7 insertions, 59 deletions
diff --git a/checker/term.mli b/checker/term.mli index 0340c79b..ab488b2b 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -1,50 +1,9 @@ open Names +open Cic -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_ndecls : 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 family_equal : sorts_family -> sorts_family -> bool + val strip_outer_cast : constr -> constr val collapse_appl : constr -> constr val decompose_app : constr -> constr * constr list @@ -71,20 +30,11 @@ 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 -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 @@ -96,15 +46,13 @@ 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 -(* Validation *) -val val_sortfam : Validate.func -val val_sort : Validate.func -val val_constr : Validate.func -val val_rctxt : Validate.func -val val_nctxt : Validate.func +(** Instance substitution for polymorphism. *) +val subst_instance_constr : Univ.universe_instance -> constr -> constr +val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context |