Module TermInner

module TermInner: sig .. end

Main View for terms

type id = ID.t

type 'a var = 'a Var.t

type 'a or_error = ('a, string) CCResult.t

type 'a printer = Format.formatter -> 'a -> unit

val fpf : Format.formatter -> ('a, Format.formatter, unit) Pervasives.format -> 'a

val print_undefined_id : bool Pervasives.ref

global option affecting printing: if true, undefined values will be displayed as "undefined_42" rather than "?__"

type prec =

`\|`	`P_bot`
`\|`	`P_app`
`\|`	`P_arrow`
`\|`	`P_eq`
`\|`	`P_not`
`\|`	`P_guard`
`\|`	`P_ite`
`\|`	`P_bind`
`\|`	`P_and`
`\|`	`P_or`
`\|`	`P_top`

module Binder: sig .. end

module TyBuiltin: sig .. end

module Builtin: sig .. end

type 'a case = 'a var list * 'a

A pattern match case for a given constructor vars, right-hand side The pattern must be linear (variable list does not contain duplicates)

type 'a cases = 'a case ID.Map.t

A list of cases (indexed by constructor)

val cases_to_list : 'a ID.Map.t -> (ID.Map.key * 'a) list

val cases_well_formed : ('a Var.t list * 'b) ID.Map.t -> bool

type 'a view =

`\|`	`Const of id`	`(*`	top-level symbol	`*)`
`\|`	`Var of 'a var`	`(*`	bound variable	`*)`
`\|`	`App of 'a * 'a list`
`\|`	`Builtin of 'a Builtin.t`	`(*`	built-in operation	`*)`
`\|`	`Bind of Binder.t * 'a var * 'a`
`\|`	`Let of 'a var * 'a * 'a`
`\|`	`Match of 'a * 'a cases`	`(*`	shallow pattern-match	`*)`
`\|`	`TyBuiltin of TyBuiltin.t`	`(*`	Builtin type	`*)`
`\|`	`TyArrow of 'a * 'a`	`(*`	Arrow type	`*)`
`\|`	`TyMeta of 'a MetaVar.t`

The main view of terms. Other representations will be refinements (read: restrictions) of this view that enforce additional restrictions, such as the absence of meta-variables or polymorphism

type 't repr = 't -> 't view

A concrete representation of terms by the type 't

type 't build = 't view -> 't

A builder for a concrete representation with type 't.

module type REPR = sig .. end

module type BUILD = sig .. end

module type S = sig .. end

module type PRINT = sig .. end

module Print (T : REPR) : sig .. end

type 'a print = (module TermInner.PRINT with type t = 'a)

module type UTIL_REPR = sig .. end

module UtilRepr (T : REPR) : sig .. end

Utils that only require a TermInner.REPR

exception Undefined of id

When a symbol is not defined

module type UTIL = sig .. end

module Util (T : S) : sig .. end

module Default: sig .. end

val default : (module TermInner.S)

module Convert (T1 : REPR)  (T2 : BUILD) : sig .. end