LF (beluga.Synint.LF)

type 'a ctx =

| Empty
| Dec of 'a ctx * 'a

type svar_class =

| Ren
| Subst

type kind =

| Typ
| PiKind of typ_decl * Syncom.Depend.t * Syncom.Plicity.t * kind

and typ_decl =

| TypDecl of Syncom.Name.t * typ
| TypDeclOpt of Syncom.Name.t

and cltyp =

| MTyp of typ
| PTyp of typ
| STyp of svar_class * dctx

Right-hand side of the turnstile for meta-types

and ctyp =

| ClTyp of cltyp * dctx
| CTyp of Syncom.Id.cid_schema option

Meta-types

and ctyp_decl =

| Decl of {
1. name : Syncom.Name.t;
2. typ : ctyp;
3. plicity : Syncom.Plicity.t;
4. inductivity : Syncom.Inductivity.t;
}
| DeclOpt of {
1. name : Syncom.Name.t;
2. plicity : Syncom.Plicity.t;
}

and typ =

| Atom of Syncom.Location.t * Syncom.Id.cid_typ * spine
| PiTyp of typ_decl * Syncom.Depend.t * Syncom.Plicity.t * typ
| Sigma of typ_rec
| TClo of typ * sub

and normal =

| Lam of Syncom.Location.t * Syncom.Name.t * normal
| Root of Syncom.Location.t * head * spine * Syncom.Plicity.t
| LFHole of Syncom.Location.t * Syncom.HoleId.t * Syncom.HoleId.name
| Clo of normal * sub
| Tuple of Syncom.Location.t * tuple

and head =

| BVar of Syncom.Id.offset
| Const of Syncom.Id.cid_term
| MMVar of mm_var_inst
| MPVar of mm_var_inst
| MVar of cvar * sub
| PVar of Syncom.Id.offset * sub
| AnnH of head * typ
| Proj of head * int
| FVar of Syncom.Name.t
| FMVar of fvarsub
| FPVar of fvarsub
| HClo of Syncom.Id.offset * Syncom.Id.offset * sub
| HMClo of Syncom.Id.offset * mm_var_inst

and fvarsub = Syncom.Name.t * sub

and spine =

| Nil
| App of normal * spine
| SClo of spine * sub

and sub =

| Shift of Syncom.Id.offset
| SVar of Syncom.Id.offset * int * sub
| FSVar of Syncom.Id.offset * fvarsub
| Dot of front * sub
| MSVar of Syncom.Id.offset * mm_var_inst
| EmptySub
| Undefs

and front =

| Head of head
| Obj of normal
| Undef

and mfront =

| ClObj of dctx_hat * clobj
| CObj of dctx
| MV of Syncom.Id.offset
| MUndef

and clobj =

| MObj of normal
| PObj of head
| SObj of sub

and msub =

| MShift of int
| MDot of mfront * msub

and cvar =

| Offset of Syncom.Id.offset
| Inst of mm_var

and mm_var = {

name : Syncom.Name.t;
instantiation : iterm option Stdlib.ref;
cD : mctx;
mmvar_id : int;
typ : ctyp;
constraints : cnstr list Stdlib.ref;
plicity : Syncom.Plicity.t;
inductivity : Syncom.Inductivity.t;

}

and mm_var_inst' = mm_var * msub

and mm_var_inst = mm_var_inst' * sub

and iterm =

| INorm of normal
| IHead of head
| ISub of sub
| ICtx of dctx

and tvar =

| TInst of typ option Stdlib.ref * dctx * kind * cnstr list Stdlib.ref

and constrnt_id = int

and constrnt =

| Queued of constrnt_id
| Eqn of constrnt_id * mctx * dctx * iterm * iterm

and cnstr = constrnt Stdlib.ref

and dctx =

| Null
| CtxVar of ctx_var
| DDec of dctx * typ_decl

and ctx_var =

| CtxName of Syncom.Name.t
| CtxOffset of Syncom.Id.offset
| CInst of mm_var_inst'

and sch_elem =

| SchElem of typ_decl ctx * typ_rec

and schema =

| Schema of sch_elem list

and dctx_hat = ctx_var option * Syncom.Id.offset

and typ_rec =

| SigmaLast of Syncom.Name.t option * typ
| SigmaElem of Syncom.Name.t * typ * typ_rec

and tuple =

| Last of normal
| Cons of normal * tuple

and mctx = ctyp_decl ctx

val map_plicity : (Syncom.Plicity.t -> Syncom.Plicity.t) -> normal -> normal

val proj_maybe : head -> int option -> head

val tclo : typ -> sub -> typ

Helper for forming TClo LF types, which avoids doing so if the substitution is the identity.

val mm_var_inst : mm_var -> msub -> sub -> mm_var_inst

Forms an MMVar instantiation by attaching an LF substitution and a meta-substituation to the variable.

val is_mmvar_instantiated : mm_var -> bool

val type_of_mmvar_instantiated : mm_var -> ctyp

val rename_ctyp_decl : 
  (Syncom.Name.t -> Syncom.Name.t) ->
  ctyp_decl ->
  ctyp_decl

val head : head -> normal

Embeds a head into a normal by using an empty spine. Very useful for constructing variables as normals. Note that the normal will have a ghost location, as heads don't carry a location.

val mvar : cvar -> sub -> head

val mmvar : mm_var_inst -> head

val mpvar : mm_var_inst -> head

val require_decl : 
  ctyp_decl ->
  Syncom.Name.t * ctyp * Syncom.Plicity.t * Syncom.Inductivity.t

Assert that the contextual type declaration be a real Decl, and not a DeclOpt. Raises a violation if it is a DeclOpt.

val null_hat : dctx_hat

val loc_of_normal : normal -> Syncom.Location.t

type nclo = normal * sub

type sclo = spine * sub

type tclo = typ * sub

type trec_clo = typ_rec * sub

val blockLength : typ_rec -> int

val getType : head -> (typ_rec * sub) -> int -> typ * sub

val getIndex : typ_rec -> Syncom.Name.t -> int

val is_explicit : ctyp_decl -> bool

val name_of_ctyp_decl : ctyp_decl -> Syncom.Name.t

val variable_of_mfront : 
  mfront ->
  (Syncom.Id.offset * Syncom.Id.offset option) option

Decides whether the given mfront is a variable, viz. projection of a pattern variable, metavariable, or context variable. Returns the offset of the variable, and optionally the projection offset.

val get_constraint_id : constrnt -> constrnt_id

val drop_spine : int -> spine -> spine