dedukti 2.7 · OCaml Package

Lambda terms

Terms

type term = private

| Kind
(*
Kind
*)
| Type of Basic.loc
(*
Type
*)
| DB of Basic.loc * Basic.ident * int
(*
deBruijn indices
*)
| Const of Basic.loc * Basic.name
(*
Global variable
*)
| App of term * term * term list
(*
f a1 a2 ; ... ; an , f not an App
*)
| Lam of Basic.loc * Basic.ident * term option * term
(*
Lambda abstraction
*)
| Pi of Basic.loc * Basic.ident * term * term
(*
Pi abstraction
*)

val pp_term : term Basic.printer

val get_loc : term -> Basic.loc

val mk_Kind : term

val mk_Type : Basic.loc -> term

val mk_DB : Basic.loc -> Basic.ident -> int -> term

val mk_Const : Basic.loc -> Basic.name -> term

val mk_Lam : Basic.loc -> Basic.ident -> term option -> term -> term

val mk_App : term -> term -> term list -> term

val mk_App2 : term -> term list -> term

val mk_Pi : Basic.loc -> Basic.ident -> term -> term -> term

val mk_Arrow : Basic.loc -> term -> term -> term

val add_n_lambdas : int -> term -> term

add_n_lambdas n t returns the term t with n (extra) anonymous lambda abstraction. Doesn't shift free variables of t.

val term_eq : term -> term -> bool

term_eq t t' is true if t = t' (up to alpha equivalence)

type position = int list

Position in a term

exception InvalidSubterm of term * int

val subterm : term -> position -> term

subterm t p returns the subterm of t at position p. Raises InvalidSubterm in case of invalid position in given term.

type 'a comparator = 'a -> 'a -> int

Type for comparison functions

val compare_term : Basic.name comparator -> term comparator

compare_term id_comp t t' compares both terms (up to alpha equivalence). * The order relation goes : * Kind < Type < Const < DB < App < Lam < Pi * Besides * Const m v < Const m' v' iif (m,v) < (m',v') * DB n < DB n' iif n < n' * App f a args < App f' a' args' iif (f,a,args) < (f',a',args') * Lam x ty t < Lam x' ty' t' iif t < t' * Pi x a b < Pi x' a' b' iif (a,b) < (a',b')

type algebra =

| Free
| AC
| ACU of term
(*
Symbols' algebra
*)

val is_AC : algebra -> bool

Return true iff given algebra is AC or ACU.

type cstr = int * term * term

Constraints (n,t,u) are t=u under n lambdas

val pp_cstr : cstr Basic.printer

Contexts

type 'a context = (Basic.loc * Basic.ident * 'a) list

General context: variables have abstract annotations

type partially_typed_context = term option context

Partially annotated context: as generated at rule parsing

type typed_context = term context

Fully type annotated context: as generated by type checking

type arity_context = int context

Arity annotated context: used for rewriting in untyped setting

val pp_untyped_context : 'a context Basic.printer

val pp_typed_context : typed_context Basic.printer

val pp_part_typed_context : partially_typed_context Basic.printer

val rename_vars_with_typed_context : typed_context -> term -> term

type 'a depthed = int * 'a

(n, t) represents the term represented by t * (whichever its representation) under n lambda abstractions.

package dedukti

Terms

Contexts