(* module Syntax: syntax trees and associated support functions *) open Support.Pervasive open Support.Error (* Data type definitions *) type ty = TyVar of int * int | TyRec of string * ty | TyFloat | TyId of string | TyArr of ty * ty | TyUnit | TyNat | TyRecord of (string * ty) list | TyVariant of (string * ty) list | TyString | TyBool type term = TmAscribe of info * term * ty | TmString of info * string | TmVar of info * int * int | TmTrue of info | TmFalse of info | TmIf of info * term * term * term | TmFloat of info * float | TmTimesfloat of info * term * term | TmLet of info * string * term * term | TmAbs of info * string * ty * term | TmApp of info * term * term | TmFix of info * term | TmUnit of info | TmRecord of info * (string * term) list | TmProj of info * term * string | TmZero of info | TmSucc of info * term | TmPred of info * term | TmIsZero of info * term | TmInert of info * ty | TmCase of info * term * (string * (string * term)) list | TmTag of info * string * term * ty type binding = NameBind | TyVarBind | TyAbbBind of ty | TmAbbBind of term * (ty option) | VarBind of ty type command = Import of string | Eval of info * term | Bind of info * string * binding (* Contexts *) type context val emptycontext : context val ctxlength : context -> int val addbinding : context -> string -> binding -> context val addname: context -> string -> context val index2name : info -> context -> int -> string val getbinding : info -> context -> int -> binding val name2index : info -> context -> string -> int val isnamebound : context -> string -> bool val getTypeFromContext : info -> context -> int -> ty (* Shifting and substitution *) val termShift: int -> term -> term val termSubstTop: term -> term -> term val typeShift : int -> ty -> ty val typeSubstTop: ty -> ty -> ty val tytermSubstTop: ty -> term -> term (* Printing *) val printtm: context -> term -> unit val printtm_ATerm: bool -> context -> term -> unit val printty : context -> ty -> unit val prbinding : context -> binding -> unit (* Misc *) val tmInfo: term -> info