Module Term

Terms of our language.

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

An expression.

and desc =
  1. | Coh of string * (icit * string * t) list * t * substitution
    (*

    coherence

    *)
  2. | Var of string
    (*

    variable

    *)
  3. | Abs of icit * string * t * t
    (*

    abstraction

    *)
  4. | App of icit * t * t
    (*

    application

    *)
  5. | Pi of icit * string * t * t
    (*

    Π-type

    *)
  6. | Id of t * t * t
    (*

    identity type

    *)
  7. | Arr of t * t * t
    (*

    arrow type

    *)
  8. | Hom of t * t
    (*

    internal hom type

    *)
  9. | Prod of t * t
    (*

    product type

    *)
  10. | Op of t
    (*

    opposite of a type

    *)
  11. | One
    (*

    terminal type

    *)
  12. | Meta of meta
    (*

    a variable to be unified

    *)
  13. | Obj
    (*

    object type

    *)
  14. | Type
    (*

    the type of types

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

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

    *)
  3. mutable value : t option;
  4. ty : t;
}
val is_pi : t -> bool
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_icit : [< `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 -> string -> (icit * string * t) list -> t -> t

Create coherence with abstracted arguments.

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

    declare a value

    *)
  2. | NCoh of string * context * t
    (*

    ensure that we are *not* coherent

    *)
  3. | Include of string
    (*

    include another file

    *)
  4. | Setting of string
    (*

    change a setting

    *)

Commands a toplevel actions.

type prog = command list

A program.

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

Build multiple hom types.

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

Build multiple abstractions.

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

Build multiple pi types.

val pis_explicit : ?pos:Extlib.Pos.t -> (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_obj : 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 -> 'c
val dim : t -> int
val free_variable_names : t -> string list