package acgtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type kind =
  1. | Type
  2. | Depend of stype * kind
and stype =
  1. | Atom of int
  2. | DAtom of int
  3. | LFun of stype * stype
  4. | Fun of stype * stype
  5. | Dprod of string * stype * stype
  6. | Record of int * stype list
  7. | Variant of int * stype list
  8. | TAbs of string * stype
  9. | TApp of stype * term
and term =
  1. | Var of int
  2. | LVar of int
  3. | Const of int
  4. | DConst of int
  5. | Abs of string * term
  6. | LAbs of string * term
  7. | App of term * term
  8. | Rcons of int * term list
  9. | Proj of int * int * term
  10. | Vcons of int * int * term
  11. | Case of int * term * (string * term) list
  12. | 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.