Previous  Up  Next

Module Lang

module Lang: sig .. end
Core part of the language.

Global options


val groupoid : bool Pervasives.ref
Do we want the theory of groupoids?
val unsafe_evars : bool Pervasives.ref
Do we allow unsafe uses of meta-variables?
val parametric_schemes : bool Pervasives.ref
Do we allow parametric pasting schemes?
val show_instances : bool Pervasives.ref
Do we show instance numbers in strings?

Data types


type var =
| VIdent of string
| VFresh of string * int
A variable.
type expr = {
   desc : desc;
   pos : Common.Pos.t;
}
An expression.
type desc =
| Var of var (*
type variable
*)
| EVar of (evar Pervasives.ref * subst) (*
meta-variable (expression, substition)
*)
| Type
| HomType (*
a type of hom set
*)
| Obj (*
type of 0-cells
*)
| Arr of expr * expr * expr (*
arrow type
*)
| Pi of var * expr * expr
| Abs of var * expr * expr
| App of expr * expr
| Coh of string * ps * expr (*
coherence (name, source, target)
*)
Contents of an expression.
type ps =
| PNil of (var * expr) (*
start
*)
| PCons of ps * (var * expr) * (var * expr) (*
extend
*)
| PDrop of ps (*
drop
*)
A pasting scheme.
type subst = (var * expr) list
A substitution.
type evar =
| ENone of int * expr (*
unknown variable with given number and type
*)
| ESome of expr (*
instantiated variable
*)
A meta-variable.
val mk : ?pos:Common.Pos.t -> desc -> expr
Create an expression from its contents.

String representation


val string_of_var : var -> string
String representation of a variable.
val to_string : ?pa:bool -> expr -> string
String representation of an expression.
val string_of_evar : ?pa:bool -> evar -> string
String representation of a meta-variable.
val string_of_ps : ps -> string
String representation of a pasting scheme.
val string_of_evarref : evar Pervasives.ref -> string
val string_of_expr : ?pa:bool -> expr -> string
module PS: sig .. end
Pasting schemes.

Variables


val fresh_var : var -> var
Generate a fresh variable name.
val fresh_inevar : ?t:expr -> unit -> evar Pervasives.ref
val fresh_evar : ?pos:Common.Pos.t -> ?t:expr -> unit -> expr
Generate a fresh meta-variable.
val occurs_evar : expr -> expr -> bool
Whether a meta-variable occurs in a term.
val subst : subst -> expr -> expr
Apply a parallel substitution.
val unevar : expr -> expr
Ensure that linked evars do not occur at toplevel.
val free_evar : expr -> evar Pervasives.ref list
Free meta-variables.
val instantiate : expr -> expr
Replace EVars by fresh ones.
val free_vars : expr -> var list
Free variables.
module Env: sig .. end
Typing environments.

Reduction and typing


val normalize : Env.t -> expr -> expr
Normalize a value.
val infer_type : Env.t -> expr -> expr
Type inference.
val check_type : Env.t -> expr -> expr -> unit
Check that an expression has given type.
val leq : Env.t -> expr -> expr -> bool
Subtype relation between expressions.

Programs


type cmd =
| Decl of var * expr (*
Declare a variable.
*)
| Axiom of var * expr (*
Declare an axiom of given type.
*)
| Check of expr (*
Check the type of an expression.
*)
| Eval of expr (*
Evaluate an expression.
*)
| Env (*
Display the environment.
*)
| Set of string * string (*
Set an option.
*)
A command.
val string_of_cmd : cmd -> string
String representation of a command.
type prog = cmd list
A program.
module Envs: sig .. end
Running environment. 
val exec_cmd : Envs.t -> cmd -> Envs.t
Execute a command.
val exec : Envs.t -> cmd list -> Envs.t
Execute a program.