package acgtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Lambda.LambdaSource

Sourcetype kind =
  1. | Type
  2. | Depend of stype * kind
Sourceand 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
Sourceand 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
Sourcetype env = (int * string) list
Sourceval env_to_string : env -> string
Sourceval generate_var_name : string -> (env * env) -> string
Sourceval unfold_labs : env -> int -> (env * env) -> term -> env * int * term
Sourceval unfold_abs : env -> int -> (env * env) -> term -> env * int * term
Sourceval unfold_app : term list -> term -> term list * term
Sourceval is_binder : int -> consts -> bool
Sourceval is_infix : int -> consts -> bool
Sourceval is_prefix : int -> consts -> bool
Sourceval 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
Sourceval kind_to_string : kind -> consts -> string
Sourceval type_to_string : stype -> consts -> string
Sourceval term_to_string : term -> consts -> string
Sourceval kind_to_formatted_string : Format.formatter -> kind -> consts -> unit
Sourceval type_to_formatted_string : Format.formatter -> stype -> consts -> unit
Sourceval term_to_formatted_string : Format.formatter -> term -> consts -> unit
Sourceval raw_to_string : term -> string
Sourceval raw_type_to_string : stype -> string
Sourceval raw_to_caml : term -> string
Sourceval raw_type_to_caml : stype -> string
Sourceval normalize : ?id_to_term:(int -> term) -> term -> term
Sourceval unlinearize_term : term -> term
Sourceval unlinearize_type : stype -> stype
Sourceval 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.

Sourceval 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.

OCaml

Innovation. Community. Security.