package dedukti

  1. Overview
  2. Docs
On This Page
  1. Terms
  2. Contexts

Lambda terms

Terms

type term = private
  1. | Kind
    (*

    Kind

    *)
  2. | Type of Basic.loc
    (*

    Type

    *)
  3. | DB of Basic.loc * Basic.ident * int
    (*

    deBruijn indices

    *)
  4. | Const of Basic.loc * Basic.name
    (*

    Global variable

    *)
  5. | App of term * term * term list
    (*

    f a1 a2 ; ... ; an , f not an App

    *)
  6. | Lam of Basic.loc * Basic.ident * term option * term
    (*

    Lambda abstraction

    *)
  7. | 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 =
  1. | Free
  2. | AC
  3. | 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.