Module Term

Terms of our language.

type t = {
desc : desc;
pos : Extlib.Pos.t;
}

An expression.

and desc =
| Coh of context * t(*

coherence

*)
| Var of string(*

variable

*)
| Abs of implicit * string * t * t(*

abstraction

*)
| App of implicit * t * t(*

application

*)
| Pi of implicit * string * t * t(*

Π-type

*)
| Hom of t * t(*

hom type

*)
| Prod of t * t(*

product type

*)
| One(*

terminal type

*)
| Id of t * t * t(*

identity type

*)
| Meta of meta(*

a variable to be unified

*)
| Obj(*

object type

*)
| Type(*

the type of types

*)
and implicit = [
| `Explicit
| `Implicit
]
and context = (string * t) list
and meta = {
id : int;
source_pos : Extlib.Pos.t option;(*

position in the source code (can be empty if the metavariable was created on the fly)

*)
mutable value : t option;
ty : t;
}
val to_string : ?pa:bool -> t -> string

String representation of an expression. This should mostly be useful for debugging (we want to print values).

val string_of_implicit : [< `Explicit | `Implicit ] -> string
val string_of_context : (string * t) list -> string
val mk : ?pos:Extlib.Pos.t -> desc -> t

Create an expression from its contents.

val repos : Extlib.Pos.t -> t -> t

Change the position.

val var : ?pos:Extlib.Pos.t -> string -> t
val meta_counter : int Stdlib.ref
val meta : ?pos:Extlib.Pos.t -> ?real:bool -> ?value:t -> t -> t
val hole : ?pos:Extlib.Pos.t -> ?real:bool -> unit -> t
val unmeta : t -> t

Replace metavariables at toplevel by their content.

val abs_coh : ?pos:Extlib.Pos.t -> (implicit * string * t) list -> t -> t

Create coherence with abstracted arguments.

type command =
| Let of string * t option * t(*

declare a value

*)
| Check of t(*

infer the type of an expression

*)
| NCoh of context * t(*

ensure that we are *not* coherent

*)

Commands a toplevel actions.

type prog = command list

A program.

val fresh_var_name : unit -> string
val fresh_var : unit -> t
val homs : ?pos:Extlib.Pos.t -> t list -> t -> t

Build multiple hom types.

val abss : ?pos:Extlib.Pos.t -> (implicit * string * t) list -> t -> t

Build multiple abstractions.

val pis : ?pos:Extlib.Pos.t -> (implicit * string * t) list -> t -> t

Build multiple pi types.

val prods : ?pos:Extlib.Pos.t -> t list -> t

Build multiple products.

val has_fv : string -> t -> bool
val is_var : t -> bool
val is_implicit_pi : t -> bool
val is_metavariable : t -> bool
val metavariables : t -> meta list

All metavariables of a term.

val has_metavariable : meta -> t -> bool
val eq_var : t -> t -> bool

Make sure that two variables are equal.

val compare_var : t -> t -> int
val failure : Extlib.Pos.t -> ('a, unit, string, 'b) Stdlib.format4 -> 'a