Module Ast

Abstract syntax tree. Definition of the internal representation of SubML's types, terms and syntactic ordinals in an abstract syntax tree (AST).

Main types for the AST

type occur =
| Non(*

The variable does not occur.

*)
| Pos of bool(*

The variable occurs only positively.

*)
| Neg of bool(*

The variable occurs only negatively.

*)
| All(*

The variable occurs both positively and negatively.

*)
| Reg of int * occur array(*

Special constructor for constructing the variance of definitions.

*)

Occurence markers for variables.

type kind =
| KVari of kind LibTools.Bindlib.var(*

Free type variable.

*)
| KFunc of kind * kind(*

Arrow type.

*)
| KProd of (string * kind) list * bool(*

if true: the record is extensible

*)
| KDSum of (string * kind) list(*

Sum (of Variant) type.

*)
| KKAll of kkbinder(*

Universal quantifier over a type.

*)
| KKExi of kkbinder(*

Corresponding existential quantifier.

*)
| KOAll of okbinder(*

Universal quantifier over an ordinal.

*)
| KOExi of okbinder(*

Corresponding existential quantifier.

*)
| KFixM of ordi * kkbinder(*

Least fixpoint with ordinal size.

*)
| KFixN of ordi * kkbinder(*

Greatest fixpoint with ordinal size.

*)
| KDefi of kdefi(*

User-defined type with its arguments.

*)
| KUCst of term * kkbinder * bool(*

Universal witness.

*)
| KECst of term * kkbinder * bool(*

Existential witness.

*)
| KUVar of kuvar * ordi array(*

Unification variable.

*)
| KMRec of ordi Subset.set * kind(*

Ordinal conjunction. FIXME wrong name

*)
| KNRec of ordi Subset.set * kind(*

Ordinal disjunction. FIXME wrong name

*)
| KPrnt of kprint(*

Special pretty-printing constructor.

*)

Ast of kinds (or types).

and okbinder = (ordi, kind) LibTools.Bindlib.binder

Bindlib binder for an ordinal in a kind.

and kkbinder = (kind, kind) LibTools.Bindlib.binder

Bindlib binder for a kind in a kind.

and kdefi = kdef * ordi array * kind array

Fully applied type definition with its ordinal and kind arguments.

and kprint =
| FreeVr of string(*

Used to print a variable.

*)
| DotPrj of string * string(*

Used to print a dot projection.

*)

Pretty-printing markers for free variables and dot-projection.

and kdef = {
tdef_name : string;(*

Name of the type constructor.

*)
tdef_tex_name : string;(*

LateX Name of the type constructor.

*)
tdef_oarity : int;(*

Number of ordinal parameters.

*)
tdef_karity : int;(*

Number of type parameters.

*)
tdef_ovariance : occur array;(*

Variance of the ordinal parameters

*)
tdef_kvariance : occur array;(*

Variance of the type parameters

*)
tdef_value : okmkbinder;(*

Definition of the constructor.

*)
}

User-defined type with ordinal and kind parameters.

and okmkbinder = kind from_kinds from_ordis

Bindlib type for a kind parametrised by ordinals and kinds.

and okmtbinder = term from_kinds from_ordis

Bindlib type for a term parametrised by ordinals and kinds.

and 'a from_ordis = (ordi, 'a) LibTools.Bindlib.mbinder

General Bindlib types for 'a parametrised by ordinals.

and 'a from_kinds = (kind, 'a) LibTools.Bindlib.mbinder

General Bindlib types for 'a parametrised by kinds.

and ('a, 'b) uvar = {
uvar_key : int;(*

Unique key (or UID).

*)
uvar_state : ('a, 'b) uvar_state Stdlib.ref;
uvar_arity : int;(*

Arity of the variable.

*)
}

Unification variable type managed using a union-find algorithm.

and ('a, 'b) uvar_state =
| Set of 'a from_ordis
| Unset of 'b
and kuvar = (kind, kuvar_state) uvar

Unification variable for a kind.

and kuvar_state =
| Free(*

No constraint.

*)
| DSum of (string * kind from_ordis) list(*

Has the given constructors.

*)
| Prod of (string * kind from_ordis) list(*

Has the given fields.

*)

State of a unification variable for kinds, useful for the inference of sum types and product types.

and ordi =
| OVari of ordi LibTools.Bindlib.var(*

Free ordinal variable.

*)
| OConv(*

ordinal that makes fixpoints converge.

*)
| OMaxi(*

OConv + omega, ordinal defining the model. only appears in OLess

*)
| OSucc of ordi(*

Succesor of an ordinal.

*)
| OLess of ordi * ord_wit(*

Ordinal witness.

*)
| OUVar of ouvar * ordi array(*

Unification variables for ordinals.

*)
| OVars of string(*

for printing only

*)

Abstract syntax tree for ordinals.

and ouvar = (ordi, ordi from_ordis option * ordi from_ordis option) uvar

Unification variable for an ordinal.

and ord_wit =
| In of term * (ordi, kind) LibTools.Bindlib.binder(*

OLess(o',In(t,f)) refers to an ordinal o smaller than o' and such that t has type Bindlib.subst f o.

*)
| NotIn of term * (ordi, kind) LibTools.Bindlib.binder(*

OLess(o',NotIn(t,f)) refers to an ordinal o smaller than o' and such that t does not have type Bindlib.subst f o.

*)
| Gen of int * schema(*

the i-th member of a counter example to e schema

*)

Ordinal constraints carried by ordinal witnesses.

and term = term' Pos.loc

Abstract syntax tree for terms, with a source code position.

and sugar =
| SgNop
| SgNil
| SgCns
| SgRec of string list
| SgTpl of int

syntactic sugar from parsing

and term' =
| TVari of term' LibTools.Bindlib.var(*

Free λ-variable.

*)
| TAbst of kind option * (term', term) LibTools.Bindlib.binder * sugar(*

λ-abstraction.

*)
| TAppl of term * term(*

Application.

*)
| TReco of (string * term) list(*

Record.

*)
| TProj of term * string(*

Projection.

*)
| TCons of string * term(*

Variant.

*)
| TCase of term * (string * term) list * term option(*

Case analysis.

*)
| TDefi of tdef(*

Defined term.

*)
| TFixY of bool option * int * (term', term) LibTools.Bindlib.binder(*

Fixpoint combinator. the integer is an indications for the termination checker. It indicates the number of unrolling to build the induction hypothesis. The boolean indicates if contravariant Conv must not be replaced by ordinal parameters

*)
| TAbrt(*

Error.

*)
| TCoer of term * kind(*

Type coercion.

*)
| TMLet of okmkbinder * term option * okmtbinder(*

Matching over a type to access the typing environment.

*)
| TCnst of (term', term) LibTools.Bindlib.binder * kind * kind(*

Witness (a.k.a. epsilon). Cnst(f,a,b) denotes a term u of type a such that Bindlib.subst f u does not have type b.

*)
| TPrnt of string(*

Print a message on the screen. Note that this operation performs is a side-effect.

*)
| TVars of string(*

Special pretty printing constructor

*)

Abstract syntax tree for terms.

and tdef = {
name : string;(*

Name of the term.

*)
tex_name : string;(*

Latex name of the term.

*)
value : term;(*

Evaluated term.

*)
orig_value : term;(*

Original term (not evaluated).

*)
ttype : kind;(*

Type of the term.

*)
proof : typ_prf;(*

Typing proof.

*)
calls_graph : Sct.t;(*

SCT instance.

*)
}

Term definition (user defined term)

and schema = {
sch_index : Sct.index;(*

index of the schema in the sct call graph

*)
sch_posit : int list;(*

the index of positive ordinals

*)
sch_relat : (int * int) list;(*

relation between ordinals

*)
sch_judge : (ordi, term_or_kind * kind) LibTools.Bindlib.mbinder;(*

judgement

*)
}

the type of a general typing judgement, i.e. with quantified ordinals

and term_or_kind =
| SchTerm of (term', term) LibTools.Bindlib.binder
| SchKind of kind

Representation of proof trees

and sub_rule =
| Sub_Delay of sub_prf Stdlib.ref
| Sub_Lower
| Sub_Func of sub_prf * sub_prf
| Sub_Prod of (string * sub_prf) list
| Sub_DSum of (string * sub_prf) list
| Sub_KAll_r of sub_prf
| Sub_KAll_l of sub_prf
| Sub_KExi_l of sub_prf
| Sub_KExi_r of sub_prf
| Sub_OAll_r of sub_prf
| Sub_OAll_l of sub_prf
| Sub_OExi_l of sub_prf
| Sub_OExi_r of sub_prf
| Sub_FixM_r of sub_prf
| Sub_FixN_l of sub_prf
| Sub_FixM_l of sub_prf
| Sub_FixN_r of sub_prf
| Sub_And_l of sub_prf
| Sub_And_r of sub_prf
| Sub_Or_l of sub_prf
| Sub_Or_r of sub_prf
| Sub_Gen of schema * (ordi * ordi) list * sub_prf
| Sub_Ind of schema
| Sub_Error of string

Subtyping proof

and sub_prf = ordi list * term * kind * kind * sub_rule

the integer is referenced by induction hyp (Sub_Ind)

and typ_rule =
| Typ_Coer of sub_prf * typ_prf
| Typ_Nope of typ_prf
| Typ_Defi of sub_prf
| Typ_Prnt of sub_prf
| Typ_Cnst of sub_prf
| Typ_Func_i of sub_prf * typ_prf
| Typ_Func_e of typ_prf * typ_prf
| Typ_Prod_i of sub_prf * typ_prf list
| Typ_Prod_e of typ_prf
| Typ_DSum_i of sub_prf * typ_prf
| Typ_DSum_e of typ_prf * typ_prf list * typ_prf option
| Typ_YGen of typ_gen Stdlib.ref
| Typ_Yufl of typ_prf
| Typ_Abrt
| Typ_Error of string

Typing proof

and typ_prf = ordi list * term * kind * typ_rule
and typ_gen =
| Todo
| Induction of schema * sub_prf
| Unroll of schema * (ordi * ordi) list * typ_prf
val eq_uvar : ('a, 'b) uvar -> ('c, 'd) uvar -> bool

Equality on variables

val tdummy : term'
val pdummy : term' Pos.loc
val kdummy : kind
val odummy : ordi

Unfolding unification variables indirections and definitions. Also perform mu/nu contractions

val contract_mu : bool Stdlib.ref

This flags controls the merging of consecutive mu and nu (true by default disables by --no-contr)

val is_set : ('a, 'b) uvar -> bool

Main shared function

val is_unset : ('a, 'b) uvar -> bool
val uvar_state : ('a, 'b) uvar -> 'b
val is_mu : bool -> kkbinder -> bool
val is_nu : bool -> kkbinder -> bool
val full_repr : kind -> kind

The main function: unfold type variables indirections and definitions

val repr : kind -> kind

The main function: unfold type variables indirections only

val orepr : ordi -> ordi

Unfold ordinal variables indirections

Pointer to printing function from "print.ml", to use in debugging

val fprint_term : (bool -> Stdlib.Format.formatter -> term -> unit) Stdlib.ref
val fprint_kind : (bool -> Stdlib.Format.formatter -> kind -> unit) Stdlib.ref
val fprint_ordi : (bool -> Stdlib.Format.formatter -> ordi -> unit) Stdlib.ref

Frequently used types and functions

type val_env = (string, tdef) Stdlib.Hashtbl.t

Value and type environments.

type typ_env = (string, kdef) Stdlib.Hashtbl.t
val typ_env : typ_env
val val_env : val_env
val verbose : bool Stdlib.ref

Bindbox type shortcuts

val mk_free_k : kind LibTools.Bindlib.var -> kind

Kind variable management.

val new_kvari : string -> kind LibTools.Bindlib.var
val mk_free_t : term' LibTools.Bindlib.var -> term'

Term variable management.

val new_tvari : string -> term' LibTools.Bindlib.var
val mk_free_o : ovar -> ordi

Ordinal variable management.

val new_ovari : string -> ovar

Smart constructors for ordinals

val oadd : ordi -> int -> ordi
val ouvar : ouvar -> obox array -> obox

Smart constructors for kinds

val kvari : string -> kbox
val kfunc : kbox -> kbox -> kbox
val kprod : bool -> (string * kbox) list -> kbox
val sprod : (string * kbox) list -> kbox
val eprod : (string * kbox) list -> kbox
val kunit : kind
val kdsum : (string * kbox) list -> kbox
val kkall : string -> (kvar -> kbox) -> kbox
val kkexi : string -> (kvar -> kbox) -> kbox
val koall : string -> (ovar -> kbox) -> kbox
val koexi : string -> (ovar -> kbox) -> kbox
val kdefi : kdef -> obox array -> kbox array -> kbox
val kfixn : string -> obox -> (kvar -> kbox) -> kbox
val kfixm : string -> obox -> (kvar -> kbox) -> kbox
val kuvar : kuvar -> obox array -> kbox
val kucst : string -> tbox -> (kvar -> kbox) -> kbox
val kecst : string -> tbox -> (kvar -> kbox) -> kbox
val new_kuvar : ?state:kuvar_state -> unit -> kind

Unification variable management. Useful for typing.

val new_kuvara : ?state:kuvar_state -> int -> kuvar

Unification variable management. Useful for typing.

val reset_all : unit -> unit

Unification variable management. Useful for typing.

val new_ouvara : ?lower:ordi from_ordis -> ?upper:ordi from_ordis -> int -> ouvar

Unification variable management. Useful for typing.

val new_ouvar : ?lower:ordi from_ordis -> ?upper:ordi from_ordis -> unit -> ordi

Unification variable management. Useful for typing.

Smart constructors for terms

val tcoer : Pos.popt -> tbox -> kbox -> tbox
val tabst : Pos.popt -> kbox option -> Pos.strloc -> sugar -> (tvar -> tbox) -> tbox
val tappl : Pos.popt -> tbox -> tbox -> tbox
val treco : Pos.popt -> (string * tbox) list -> tbox
val tunit : term' Pos.loc
val tproj : Pos.popt -> tbox -> string -> tbox
val tcase : Pos.popt -> tbox -> (string * tbox) list -> tbox option -> tbox
val tcons : Pos.popt -> string -> tbox -> tbox
val tdefi : Pos.popt -> tdef -> tbox
val tprnt : Pos.popt -> string -> tbox
val tabrt : Pos.popt -> tbox
val tfixy : Pos.popt -> int -> Pos.strloc -> (tvar -> tbox) -> tbox
val tmlet : Pos.popt -> string array -> string array -> (ovar array -> kvar array -> kbox) -> tbox option -> (ovar array -> kvar array -> tbox) -> tbox
val tcnst : (term', term) LibTools.Bindlib.binder -> kbox -> kbox -> tbox

Definition of common types and terms

val bot : kind
val top : kind
val idt : tbox
val generic_tcnst : kbox -> kbox -> tbox

Syntactic sugars

val do_dot_proj : term -> kind -> string -> kind

dot projection: computing the witness

val dot_proj : tbox -> string -> kbox

dot projection: we compute the projection if t is an epsilon or a definition. We also deal with a special case for printing !)

val with_clause : kbox -> string -> kbox -> kbox

with clause

Variance function

val combine : occur -> occur -> occur
val compose : occur -> occur -> occur
val compose2 : occur -> occur -> occur
val neg : occur -> occur
val sPos : occur
val sNeg : occur
val isPos : occur -> bool
val isNeg : occur -> bool