Module Kernel.TermSource

Lambda terms

Terms

Sourcetype 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

    *)
Sourceval get_loc : term -> Basic.loc
Sourceval mk_Kind : term
Sourceval mk_Type : Basic.loc -> term
Sourceval mk_DB : Basic.loc -> Basic.ident -> int -> term
Sourceval mk_Const : Basic.loc -> Basic.name -> term
Sourceval mk_Lam : Basic.loc -> Basic.ident -> term option -> term -> term
Sourceval mk_App : term -> term -> term list -> term
Sourceval mk_App2 : term -> term list -> term
Sourceval mk_Pi : Basic.loc -> Basic.ident -> term -> term -> term
Sourceval mk_Arrow : Basic.loc -> term -> term -> term
Sourceval 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.

Sourceval term_eq : term -> term -> bool

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

Sourcetype position = int list

Position in a term

Sourceexception InvalidSubterm of term * int
Sourceval 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.

Sourcetype 'a comparator = 'a -> 'a -> int

Type for comparison functions

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')

Sourcetype algebra =
  1. | Free
  2. | AC
  3. | ACU of term
    (*

    Symbols' algebra

    *)
Sourceval is_AC : algebra -> bool

Return true iff given algebra is AC or ACU.

Sourcetype cstr = int * term * term

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

Contexts

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

General context: variables have abstract annotations

Sourcetype partially_typed_context = term option context

Partially annotated context: as generated at rule parsing

Sourcetype typed_context = term context

Fully type annotated context: as generated by type checking

Sourcetype arity_context = int context

Arity annotated context: used for rewriting in untyped setting

Sourceval pp_untyped_context : 'a context Basic.printer
Sourceval pp_typed_context : typed_context Basic.printer
Sourceval pp_part_typed_context : partially_typed_context Basic.printer
Sourceval rename_vars_with_typed_context : typed_context -> term -> term
Sourcetype 'a depthed = int * 'a

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