diff options
Diffstat (limited to 'kernel/term.mli')
-rw-r--r-- | kernel/term.mli | 62 |
1 files changed, 39 insertions, 23 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 72ba6f511..9019fa091 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -59,10 +59,9 @@ type constr = sorts oper term type flat_arity = (name * constr) list * sorts -type 'a judge = { body : constr; typ : 'a } +(*type 'a judge = { body : constr; typ : 'a }*) type typed_type -type typed_term = typed_type judge val make_typed : constr -> sorts -> typed_type val make_typed_lazy : constr -> (constr -> sorts) -> typed_type @@ -78,6 +77,9 @@ val incast_type : typed_type -> constr val outcast_type : constr -> typed_type +type var_declaration = identifier * constr option * typed_type +type rel_declaration = name * constr option * typed_type + (**********************************************************************) type binder_kind = BProd | BLambda @@ -96,7 +98,10 @@ type 'ctxt reference = manipulation of terms. Some of these functions may be overlapped with previous ones. *) -(* Concrete type for making pattern-matching. *) +(* Concrete type for making pattern-matching. *) + +(* [constr array] is an instance matching definitional var_context in + the same order (i.e. last argument first) *) type existential = int * constr array type constant = section_path * constr array type constructor = constructor_path * constr array @@ -169,18 +174,30 @@ val implicit_sort : sorts type $t_2$ (that means t2 is declared as the type of t1). *) val mkCast : constr -> constr -> constr -(* Constructs the product $(x:t_1)t_2$. $x$ may be anonymous. *) +(* Constructs the product $(x:t_1)t_2$ *) val mkProd : name -> constr -> constr -> constr - -(* [mkProd_string s t c] constructs the product $(s:t)c$ *) +val mkNamedProd : identifier -> constr -> constr -> constr val mkProd_string : string -> constr -> constr -> constr +(* Constructs the product $(x:t_1)t_2$ *) +val mkLetIn : name -> constr -> constr -> constr -> constr +val mkNamedLetIn : identifier -> constr -> constr -> constr -> constr + +(* Constructs either [(x:t)c] or [[x=b:t]c] *) +val mkProd_or_LetIn : rel_declaration -> constr -> constr +val mkNamedProd_or_LetIn : var_declaration -> constr -> constr + +(* Constructs either [[x:t]c] or [[x=b:t]c] *) +val mkLambda_or_LetIn : rel_declaration -> constr -> constr +val mkNamedLambda_or_LetIn : var_declaration -> constr -> constr + +(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) +val mkProd_wo_LetIn : rel_declaration -> constr -> constr +val mkNamedProd_wo_LetIn : var_declaration -> constr -> constr + (* non-dependant product $t_1 \rightarrow t_2$ *) val mkArrow : constr -> constr -> constr -(* named product *) -val mkNamedProd : identifier -> constr -> constr -> constr - (* Constructs the abstraction $[x:t_1]t_2$ *) val mkLambda : name -> constr -> constr -> constr val mkNamedLambda : identifier -> constr -> constr -> constr @@ -198,7 +215,7 @@ val mkAppList : constr -> constr list -> constr val mkConst : constant -> constr (* Constructs an existential variable *) -val mkEvar : int -> constr array -> constr +val mkEvar : existential -> constr (* Constructs an abstract object *) val mkAbst : section_path -> constr array -> constr @@ -360,13 +377,6 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint -(* Provisoire, le temps de maitriser les cast *) -val destUntypedFix : - constr -> int array * int * constr array * Names.name list * constr array -val destUntypedCoFix : - constr -> int * constr array * Names.name list * constr array - - (*s Other term constructors. *) val abs_implicit : constr -> constr @@ -410,7 +420,8 @@ val prod_applist : constr -> constr list -> constr (*s Other term destructors. *) (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair - $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product. *) + $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product. + It includes also local definitions *) val decompose_prod : constr -> (name*constr) list * constr (* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ into the pair @@ -420,11 +431,11 @@ val decompose_lam : constr -> (name*constr) list * constr (* Given a positive integer n, transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair $([(xn,Tn);...;(x1,T1)],T)$. *) -val decompose_prod_n : int -> constr -> (name*constr) list * constr +val decompose_prod_n : int -> constr -> (name * constr) list * constr (* Given a positive integer $n$, transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *) -val decompose_lam_n : int -> constr -> (name*constr) list * constr +val decompose_lam_n : int -> constr -> (name * constr) list * constr (* [nb_lam] $[x_1:T_1]...[x_n:T_n]c$ where $c$ is not an abstraction gives $n$ (casts are ignored) *) @@ -565,11 +576,16 @@ val rename_bound_var : identifier list -> constr -> constr val eta_reduce_head : constr -> constr val eq_constr : constr -> constr -> bool val eta_eq_constr : constr -> constr -> bool -val subst_term : constr -> constr -> constr -val subst_term_eta_eq : constr -> constr -> constr + +(*s The following functions substitutes [what] by [Rel 1] in [where] *) +val subst_term : what:constr -> where:constr -> constr +val subst_term_eta_eq : what:constr -> where:constr -> constr +val subst_term_occ : occs:int list -> what:constr -> where:constr -> constr +val subst_term_occ_decl : occs:int list -> what:constr -> + where:var_declaration -> var_declaration + val replace_consts : (section_path * (identifier list * constr) option) list -> constr -> constr -val subst_term_occ : int list -> constr -> constr -> constr (* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] for each binding $(i,c_i)$ in [bl], |