acgtk

Abstract Categorial Grammar development toolkit
Library acgtkLib.logic
Module Logic . Lambda . Lambda
type kind =
| Type
| Depend of stype * kind
and stype =
| Atom of int
| DAtom of int
| LFun of stype * stype
| Fun of stype * stype
| Dprod of string * stype * stype
| Record of int * stype list
| Variant of int * stype list
| TAbs of string * stype
| TApp of stype * term
and term =
| Var of int
| LVar of int
| Const of int
| DConst of int
| Abs of string * term
| LAbs of string * term
| App of term * term
| Rcons of int * term list
| Proj of int * int * term
| Vcons of int * int * term
| Case of int * term * (string * term) list
| Unknown of int
type env = (int * string) list
val env_to_string : env -> string
val generate_var_name : string -> (env * env) -> string
val unfold_labs : env -> int -> (env * env) -> term -> env * int * term
val unfold_abs : env -> int -> (env * env) -> term -> env * int * term
val unfold_app : term list -> term -> term list * term
val is_binder : int -> consts -> bool
val is_infix : int -> consts -> bool
val is_prefix : int -> consts -> bool
val unfold_binder : int -> int -> int -> consts -> (int * (string * Abstract_syntax.Abstract_syntax.abstraction)) list -> (env * env) -> term -> (int * (string * Abstract_syntax.Abstract_syntax.abstraction)) list * int * int * term
val kind_to_string : kind -> consts -> string
val type_to_string : stype -> consts -> string
val term_to_string : term -> consts -> string
val kind_to_formatted_string : Format.formatter -> kind -> consts -> unit
val type_to_formatted_string : Format.formatter -> stype -> consts -> unit
val term_to_formatted_string : Format.formatter -> term -> consts -> unit
val raw_to_string : term -> string
val raw_type_to_string : stype -> string
val raw_to_caml : term -> string
val raw_type_to_caml : stype -> string
val normalize : ?id_to_term:( int -> term ) -> term -> term
val unlinearize_term : term -> term
val unlinearize_type : stype -> stype
val eta_long_form : term -> stype -> ( int -> stype ) -> term

eta_long_form t ty type_of_cst returns the eta-long form of t with respect of type ty. t is supposed to be in beta-normal form and all the definitions of t and ty should have been unfolded. type_of_cst i returns the type (with unfolded definitions) of the constant whose id is i. i is supposed to be an actual id of a constant.

val is_2nd_order : stype -> ( int -> stype ) -> bool

is_2nd_order ty type_definition returns true if ty is 2nd order. ty should have been unfolded and type_definition i is returns the unfolded type of a defined type (DAtom) whose id is i. i is supposed to be an actual id of such a defined type.