Clean up language specifications

Specificaties/ExEff.txt

-import (Operations)
-namespace TermVar : Value , ValueType
-namespace SkelTypeVar : SkeletonType
-namespace DirtVar : Dirt
-namespace TypeVar : ValueType , SkeletonType
-namespace CoVar : Coercion , SimpleCoercionType
-
-sort Value
-    inh ctx  TermVar
-    inh tctx  TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-    inh coctx CoVar
- | TmVar (x@ctx)
- | TmFun (x:Computation) (t:ValueType) [z:TermVar]
-            x.ctx = lhs.ctx,z
- | TmTSkellAbs (t1 : Value) [T:SkelTypeVar]
-        t1.skelctx = lhs.skelctx, T
- |  TmTSkelApp (t1 : Value) (ty : SkeletonType)
- | TmValueTypeAbs (t:Value) (ty:SkeletonType) [Z:TypeVar]
-            t.tctx=lhs.tctx,Z
- | TmValueTypeApp (t:Value) (ty:ValueType)
- | TmDirtAbs (t:Value) [Z:DirtVar]
-            t.dctx=lhs.dctx,Z
- | TmDirtApp (t:Value) (ty:Dirt)
- |TmCoAbs (t:Value) (coty:SimpleCoercionType) [Z:CoVar]
-    t.coctx=lhs.coctx,Z
- | TmCoApp (t:Value) (Co:Coercion)
- | TmCast (val:Value) (Co:Coercion)
- |TmUnit
- |TmHandler (h:Handler)
-
-sort OperationCompTuple
-    inh ctx  TermVar
-    inh tctx  TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-    inh coctx CoVar
-    |OpAndComp (comp:Computation)  {Op} [k:TermVar]
-            comp.ctx=lhs.ctx,k
-sort Handler
-    inh ctx  TermVar
-    inh tctx  TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-    inh coctx CoVar
-    |ReturnHandler (opsc:[OperationCompTuple]) (ty:ValueType) (cr:Computation) [x:TermVar]
-                cr.ctx=lhs.ctx,x
-                opsc.ctx=lhs.ctx,x
-
-sort Computation
-    inh ctx  TermVar
-    inh tctx  TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-    inh coctx CoVar
-    |ReturnComp (v:Value)
-    |HandleComp (comp:Computation) (v:Value)
-    |ComputationApp (t1 : Value) (t2 : Value)
-    |LetComp (v:Value) (comp:Computation) [x:TermVar]
-               comp.ctx=lhs.ctx,x
-    |DoComp (c1:Computation) (c2:Computation) [x:TermVar]
-                c2.ctx= lhs.ctx,x
-    |CastComp (comp:Computation) (gamma:Coercion)
-    |OpComp (v:Value) (ty:ValueType) (co:Computation) {Op}[y:TermVar]
-            co.ctx=lhs.ctx,y
-
-sort ValueType
-    inh tctx TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-    |ValTyVar (x@tctx)
-    |ValTUnit
-    |ValTyArr (ty:ValueType) (comp:ComputationType)
-    |ValTyHandler (c1:ComputationType) (c2:ComputationType)
-    |ValTyAllSkel (t:ValueType)  [Z:SkelTypeVar]
-            t.skelctx=lhs.skelctx,Z
-    |ValTyAll (t:ValueType) (ty:SkeletonType) [Z:TypeVar]
-            t.tctx=lhs.tctx,Z
-    |ValTyAllDirt  (t:ValueType) [Z:DirtVar]
-        t.dctx=lhs.dctx,Z
-    |ValTyCoArr (pi:SimpleCoercionType) (T:ValueType)
-sort CoercionType
-    inh tctx  TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-    | CoSimple (co: SimpleCoercionType)
-    |CoComp (v1:ComputationType) (v2: ComputationType)
-
-sort SimpleCoercionType
-    inh tctx  TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-   | DirtCoTypes (d1:Dirt) (d2:Dirt)
-   | ValTypes (d1:ValueType) (d2:ValueType)
-
-sort SkeletonType
-    inh skelctx SkelTypeVar
-    |SkelTUnit
-    |SkellAllType (t:SkeletonType) [T:SkelTypeVar]
-            t.skelctx= lhs.skelctx,T
-    |SkelVar (d@skelctx)
-    |SkelArr (t1:SkeletonType) (t2:SkeletonType)
-sort Dirt
-    inh dctx DirtVar
-    |DirtVariable (d@dctx)
-    |EmptyDirt
-    |UnionDirt (d:Dirt) {Op}
-
-sort ComputationType
-    inh tctx  TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-    | ComputationTy (t:ValueType) (d:Dirt)
-sort Coercion rewrite
-    inh coctx CoVar
-    inh tctx TypeVar
-    inh skelctx SkelTypeVar
-    inh dctx DirtVar
-    |CoercionVar(x@coctx)
-    |CoUnit
-    |CoTypeVar (valty:ValueType)
-    |CoDirt (d:Dirt)
-    |CoArrow (co1:Coercion) (co2:Coercion)
-    |CoHandler (co1:Coercion) (co2:Coercion)
-    |CoEmptyDirt
-    |UnionOp (Co:Coercion) {Op}
-    |CoskeletonAll (co:Coercion) [Z:SkelTypeVar]
-            co.skelctx=lhs.skelctx,Z
-    |CoTypeAll (co:Coercion) (t:SkeletonType) [Z:TypeVar]
-                co.tctx=lhs.tctx,Z
-    |CodirtAll (co: Coercion )  [Z:DirtVar]
-            co.dctx=lhs.dctx,Z
-    |CoCoArrow  (pi: SimpleCoercionType) (Co:Coercion)
-    |CoComputation (co1:Coercion) (co2:Coercion)
-
-
-HaskellCode
-
--- You need to delete the "b" binder parameters if using De Bruijn indices
-
-rewriteTypeToCoercion:: ValueType ->Coercion
-rewriteTypeToCoercion (ValTyVar hnat) = CoTypeVar (ValTyVar hnat)
-rewriteTypeToCoercion (ValTUnit) = CoUnit
-rewriteTypeToCoercion  (ValTyArr ty1 (ComputationTy ty2 dirt))= CoArrow (rewriteTypeToCoercion ty1) (CoComputation (rewriteTypeToCoercion ty2)  (CoDirt dirt))
-rewriteTypeToCoercion  (ValTyHandler (ComputationTy ty1 dirt1) (ComputationTy ty2 dirt2)) =  CoHandler (CoComputation (rewriteTypeToCoercion ty1)  (CoDirt dirt1)) (CoComputation (rewriteTypeToCoercion ty2)  (CoDirt dirt2))
-rewriteTypeToCoercion  (ValTyAllSkel b ty) = CoskeletonAll b (rewriteTypeToCoercion ty)
-rewriteTypeToCoercion  (ValTyAll b valty skel)= CoTypeAll b (rewriteTypeToCoercion valty) skel
-rewriteTypeToCoercion  (ValTyAllDirt b valty)=CodirtAll b (rewriteTypeToCoercion valty )
-rewriteTypeToCoercion  (ValTyCoArr pi ty)= CoCoArrow pi (rewriteTypeToCoercion ty)
-
-
-rewriteCoercion :: Coercion->Coercion
-rewriteCoercion (CoTypeVar ty) = rewriteTypeToCoercion ty
-rewriteCoercion  (CoArrow co1 co2) = CoArrow (rewriteCoercion co1) (rewriteCoercion co2)
-rewriteCoercion (CoHandler co1 co2) = CoHandler  (rewriteCoercion co1) (rewriteCoercion co2)
-rewriteCoercion (UnionOp co1 op) = UnionOp (rewriteCoercion co1) op
-rewriteCoercion (CoskeletonAll b co) = CoskeletonAll b (rewriteCoercion co)
-rewriteCoercion (CoTypeAll b co skel) = CoTypeAll b (rewriteCoercion co ) skel
-rewriteCoercion (CoCoArrow pi co) = CoCoArrow pi (rewriteCoercion co )
-rewriteCoercion (CoComputation co1 co2) = CoComputation (rewriteCoercion co1) (rewriteCoercion co2)
-rewriteCoercion co = co

Specificaties/FCo.txt

-namespace TermVar : Term , Type
-namespace TypeVar : Type 
-sort Term
-    inh ctx  TermVar 
-    inh tctx  TypeVar 
- | TmVar (x@ctx)
- | TmAbs (x:Term) (t:Type) [z:TermVar]
-            x.ctx = lhs.ctx,z
- | TmApp (t1 : Term) (t2 : Term)
- | TmTApp (t1 : Term) (T : Type)           
- | TmTAbs (t1 : Term) [T:TypeVar]
-        t1.ctx= lhs.ctx
-        t1.tctx = lhs.tctx, T 
- |TmTop
- |TmTuple (e1:Term) (e2:Term)
- |TmInt {Int}
- |TmCast (co:Coercion) (e:Term)
-
-sort Type 
-    inh tyctx TypeVar
-    | TyVar (t@tyctx)
-    | TyArr (t1 : Type) (t2 : Type)
-    | TyAll (t1:Type) [T:TypeVar]
-                    t1.tyctx = lhs.tyctx ,T
-    |TyInt
-    |TyTop
-    |TyProd (t1:Type) (t2:Type)
-       
-sort Coercion
-    inh tycoctx TypeVar
-    | CoId
-    |CoTrans (co1:Coercion) (co2:Coercion)
-    |CoTop (ty:Type)
-    |CoBot (ty:Type)
-    |CoArrow (co1:Coercion) (co2:Coercion)
-    |CoTuple (co1:Coercion) (co2:Coercion)
-    |CoProj1 (ty2:Type)
-    |CoProj2 (ty1:Type)
-    |CoAll (co1:Coercion)
-    |CoDistArrow
-    |CoTopArrow
-    |CoTopAll
-    |CoDistAll
\ No newline at end of file

Specificaties/Fi+.txt

-namespace TermVar : FiTerm,FiType
-namespace TypeVar : FiType,FiType
-
-sort FiTerm
-    inh ctx TermVar
-    inh tyctx TypeVar
-    |TmVar (x@ctx)
-    |TmInt {Int}
-    |TmTop
-    |TmAbs (t:FiTerm) (ty:FiType) [x:TermVar]
-            t.ctx=lhs.ctx,x 
-    |TmApp (t1:FiTerm) (t2:FiTerm)
-    |TmMerge (t1:FiTerm) (t2:FiTerm)
-    |TmAnn (t:FiTerm) (ty:FiType)
-    |TmRecord (t:FiTerm) {String}
-    |TmProj (t:FiTerm) {String}
-    |TmAll (ty:FiType) (t:FiTerm) [alpha:TypeVar]
-            t.tyctx=lhs.tyctx,alpha
-    |TypeApp (t:FiTerm) (ty:FiType)
-
-sort FiType 
-    inh tyctx TypeVar
-    |TyTop
-    |TyBot
-    |TyInt
-    |TyArr (ty1:FiType) (ty2:FiType)
-    |TyAnd (ty1:FiType) (ty2:FiType)    
-    |TyRecord (ty:FiType) {String}
-    |TyVar(x@tyctx)
-    |TyAll (tyStar:FiType) (ty:FiType) [alpha:TypeVar]
-                ty.tyctx= lhs.tyctx,alpha
-    
-    
\ No newline at end of file

Specificaties/systemF.txt

-namespace TermVar : Term ,Type
-namespace TypeVar : Type 
-sort Term
-    inh ctx  TermVar 
-    inh tctx  TypeVar 
- | TmVar (x@ctx)
- | TmAbs (x:Term) (t:Type) [z:TermVar]
-            x.tctx = lhs.tctx
-            x.ctx = lhs.ctx,z
-            t.tyctx = lhs.tctx
- | TmApp (t1 : Term) (t2 : Term)
- | TmTApp (t1 : Term) (T : Type)           
- | TmTAbs (t1 : Term) [T:TypeVar]
-        t1.ctx= lhs.ctx
-        t1.tctx = lhs.tctx, T 
-
-sort Type 
-    inh tyctx TypeVar
-    | TyVar (t@tyctx)
-    | TyArr (t1 : Type) (t2 : Type)
-            t1.tyctx = lhs.tyctx 
-             t2.tyctx = lhs.tyctx 
-    | TyAll (t1:Type) [T:TypeVar]
-                    t1.tyctx = lhs.tyctx ,T
-    |TyBase
-      
\ No newline at end of file

Specifications/ExEff.txt

+import (Operations)
+
+namespace TermVar: Value, ValueType
+namespace SkelTypeVar: SkeletonType
+namespace DirtVar: Dirt
+namespace TypeVar: ValueType, SkeletonType
+namespace CoVar: Coercion, SimpleCoercionType
+
+sort Value
+    inh ctx TermVar
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+    inh coctx CoVar
+    | TmVar (x@ctx)
+    | TmFun (x: Computation) (t: ValueType) [z: TermVar]
+        x.ctx = lhs.ctx, z
+    | TmTSkellAbs (t1: Value) [T: SkelTypeVar]
+        t1.skelctx = lhs.skelctx, T
+    | TmTSkelApp (t1: Value) (ty: SkeletonType)
+    | TmValueTypeAbs (t: Value) (ty: SkeletonType) [Z: TypeVar]
+        t.tctx = lhs.tctx, Z
+    | TmValueTypeApp (t: Value) (ty: ValueType)
+    | TmDirtAbs (t: Value) [Z: DirtVar]
+        t.dctx = lhs.dctx, Z
+    | TmDirtApp (t: Value) (ty: Dirt)
+    | TmCoAbs (t: Value) (coty: SimpleCoercionType) [Z: CoVar]
+        t.coctx = lhs.coctx, Z
+    | TmCoApp (t: Value) (Co: Coercion)
+    | TmCast (val: Value) (Co: Coercion)
+    | TmUnit
+    | TmHandler (h: Handler)
+
+sort OperationCompTuple
+    inh ctx TermVar
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+    inh coctx CoVar
+    | OpAndComp (comp: Computation) {Op} [k: TermVar]
+        comp.ctx = lhs.ctx, k
+
+sort Handler
+    inh ctx TermVar
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+    inh coctx CoVar
+    | ReturnHandler (opsc: [OperationCompTuple]) (ty: ValueType) (cr: Computation) [x: TermVar]
+        cr.ctx = lhs.ctx, x
+        opsc.ctx = lhs.ctx, x
+
+sort Computation
+    inh ctx TermVar
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+    inh coctx CoVar
+    | ReturnComp (v: Value)
+    | HandleComp (comp: Computation) (v: Value)
+    | ComputationApp (t1: Value) (t2: Value)
+    | LetComp (v: Value) (comp: Computation) [x: TermVar]
+        comp.ctx = lhs.ctx, x
+    | DoComp (c1: Computation) (c2: Computation) [x: TermVar]
+        c2.ctx = lhs.ctx, x
+    | CastComp (comp: Computation) (gamma: Coercion)
+    | OpComp (v: Value) (ty: ValueType) (co: Computation) {Op} [y: TermVar]
+        co.ctx = lhs.ctx, y
+
+sort ValueType
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+    | ValTyVar (x@tctx)
+    | ValTUnit
+    | ValTyArr (ty: ValueType) (comp: ComputationType)
+    | ValTyHandler (c1: ComputationType) (c2: ComputationType)
+    | ValTyAllSkel (t: ValueType) [Z: SkelTypeVar]
+        t.skelctx = lhs.skelctx, Z
+    | ValTyAll (t: ValueType) (ty: SkeletonType) [Z: TypeVar]
+        t.tctx = lhs.tctx, Z
+    | ValTyAllDirt (t: ValueType) [Z: DirtVar]
+        t.dctx = lhs.dctx, Z
+    | ValTyCoArr (pi: SimpleCoercionType) (T: ValueType)
+
+sort CoercionType
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+    | CoSimple (co: SimpleCoercionType)
+    | CoComp (v1: ComputationType) (v2: ComputationType)
+
+sort SimpleCoercionType
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+   | DirtCoTypes (d1: Dirt) (d2: Dirt)
+   | ValTypes (d1: ValueType) (d2: ValueType)
+
+sort SkeletonType
+    inh skelctx SkelTypeVar
+    | SkelTUnit
+    | SkellAllType (t: SkeletonType) [T: SkelTypeVar]
+        t.skelctx = lhs.skelctx, T
+    | SkelVar (d@skelctx)
+    | SkelArr (t1: SkeletonType) (t2: SkeletonType)
+
+sort Dirt
+    inh dctx DirtVar
+    | DirtVariable (d@dctx)
+    | EmptyDirt
+    | UnionDirt (d: Dirt) {Op}
+
+sort ComputationType
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+    | ComputationTy (t: ValueType) (d: Dirt)
+
+sort Coercion rewrite
+    inh coctx CoVar
+    inh tctx TypeVar
+    inh skelctx SkelTypeVar
+    inh dctx DirtVar
+    | CoercionVar (x@coctx)
+    | CoUnit
+    | CoTypeVar (valty: ValueType)
+    | CoDirt (d: Dirt)
+    | CoArrow (co1: Coercion) (co2: Coercion)
+    | CoHandler (co1: Coercion) (co2: Coercion)
+    | CoEmptyDirt
+    | UnionOp (Co: Coercion) {Op}
+    | CoskeletonAll (co: Coercion) [Z: SkelTypeVar]
+        co.skelctx = lhs.skelctx, Z
+    | CoTypeAll (co: Coercion) (t: SkeletonType) [Z: TypeVar]
+        co.tctx = lhs.tctx, Z
+    | CodirtAll (co: Coercion) [Z: DirtVar]
+        co.dctx = lhs.dctx, Z
+    | CoCoArrow (pi: SimpleCoercionType) (Co: Coercion)
+    | CoComputation (co1: Coercion) (co2: Coercion)
+
+HaskellCode
+
+-- You need to delete the "b" binder parameters if using De Bruijn indices
+
+rewriteTypeToCoercion :: ValueType -> Coercion
+rewriteTypeToCoercion (ValTyVar hnat) = CoTypeVar (ValTyVar hnat)
+rewriteTypeToCoercion (ValTUnit) = CoUnit
+rewriteTypeToCoercion (ValTyArr ty1 (ComputationTy ty2 dirt)) = CoArrow (rewriteTypeToCoercion ty1) (CoComputation (rewriteTypeToCoercion ty2) (CoDirt dirt))
+rewriteTypeToCoercion (ValTyHandler (ComputationTy ty1 dirt1) (ComputationTy ty2 dirt2)) = CoHandler (CoComputation (rewriteTypeToCoercion ty1) (CoDirt dirt1)) (CoComputation (rewriteTypeToCoercion ty2) (CoDirt dirt2))
+rewriteTypeToCoercion (ValTyAllSkel b ty) = CoskeletonAll b (rewriteTypeToCoercion ty)
+rewriteTypeToCoercion (ValTyAll b valty skel) = CoTypeAll b (rewriteTypeToCoercion valty) skel
+rewriteTypeToCoercion (ValTyAllDirt b valty) = CodirtAll b (rewriteTypeToCoercion valty)
+rewriteTypeToCoercion (ValTyCoArr pi ty) = CoCoArrow pi (rewriteTypeToCoercion ty)
+
+rewriteCoercion :: Coercion -> Coercion
+rewriteCoercion (CoTypeVar ty) = rewriteTypeToCoercion ty
+rewriteCoercion (CoArrow co1 co2) = CoArrow (rewriteCoercion co1) (rewriteCoercion co2)
+rewriteCoercion (CoHandler co1 co2) = CoHandler (rewriteCoercion co1) (rewriteCoercion co2)
+rewriteCoercion (UnionOp co1 op) = UnionOp (rewriteCoercion co1) op
+rewriteCoercion (CoskeletonAll b co) = CoskeletonAll b (rewriteCoercion co)
+rewriteCoercion (CoTypeAll b co skel) = CoTypeAll b (rewriteCoercion co) skel
+rewriteCoercion (CoCoArrow pi co) = CoCoArrow pi (rewriteCoercion co)
+rewriteCoercion (CoComputation co1 co2) = CoComputation (rewriteCoercion co1) (rewriteCoercion co2)
+rewriteCoercion co = co

Specifications/FCo.txt

+namespace TermVar: Term, Type
+namespace TypeVar: Type
+
+sort Term
+    inh ctx  TermVar
+    inh tctx TypeVar
+    | TmVar (x@ctx)
+    | TmAbs (x: Term) (t: Type) [z: TermVar]
+        x.ctx = lhs.ctx, z
+    | TmApp (t1: Term) (t2: Term)
+    | TmTApp (t1: Term) (t: Type)
+    | TmTAbs (t1: Term) [t: TypeVar]
+        t1.ctx = lhs.ctx
+        t1.tctx = lhs.tctx, t
+    | TmTop
+    | TmTuple (e1: Term) (e2: Term)
+    | TmInt {Int}
+    | TmCast (co: Coercion) (e: Term)
+
+sort Type
+    inh tyctx TypeVar
+    | TyVar (t@tyctx)
+    | TyArr (t1: Type) (t2: Type)
+    | TyAll (t1: Type) [t: TypeVar]
+        t1.tyctx = lhs.tyctx, t
+    | TyInt
+    | TyTop
+    | TyProd (t1: Type) (t2: Type)
+
+sort Coercion
+    inh tycoctx TypeVar
+    | CoId
+    | CoTrans (co1: Coercion) (co2: Coercion)
+    | CoTop (ty: Type)
+    | CoBot (ty: Type)
+    | CoArrow (co1: Coercion) (co2: Coercion)
+    | CoTuple (co1: Coercion) (co2: Coercion)
+    | CoProj1 (ty2: Type)
+    | CoProj2 (ty1: Type)
+    | CoAll (co1: Coercion)
+    | CoDistArrow
+    | CoTopArrow
+    | CoTopAll
+    | CoDistAll

Specifications/Fi+.txt

+namespace TermVar: FiTerm, FiType
+namespace TypeVar: FiType, FiType
+
+sort FiTerm
+    inh ctx   TermVar
+    inh tyctx TypeVar
+    | TmVar (x@ctx)
+    | TmInt {Int}
+    | TmTop
+    | TmAbs (t: FiTerm) (ty: FiType) [x: TermVar]
+        t.ctx = lhs.ctx, x
+    | TmApp (t1: FiTerm) (t2: FiTerm)
+    | TmMerge (t1: FiTerm) (t2: FiTerm)
+    | TmAnn (t: FiTerm) (ty: FiType)
+    | TmRecord (t: FiTerm) {String}
+    | TmProj (t: FiTerm) {String}
+    | TmAll (ty: FiType) (t: FiTerm) [alpha: TypeVar]
+        t.tyctx = lhs.tyctx, alpha
+    | TypeApp (t: FiTerm) (ty: FiType)
+
+sort FiType
+    inh tyctx TypeVar
+    | TyTop
+    | TyBot
+    | TyInt
+    | TyArr (ty1: FiType) (ty2: FiType)
+    | TyAnd (ty1: FiType) (ty2: FiType)
+    | TyRecord (ty: FiType) {String}
+    | TyVar(x@tyctx)
+    | TyAll (tyStar: FiType) (ty: FiType) [alpha: TypeVar]
+        ty.tyctx = lhs.tyctx, alpha

Specifications/systemF.txt

+namespace TermVar: Term, Type
+namespace TypeVar: Type
+
+sort Term
+    inh ctx  TermVar
+    inh tctx TypeVar
+    | TmVar (x@ctx)
+    | TmAbs (x: Term) (t: Type) [z: TermVar]
+        x.tctx = lhs.tctx
+        x.ctx = lhs.ctx, z
+        t.tyctx = lhs.tctx
+    | TmApp (t1: Term) (t2: Term)
+    | TmTApp (t1: Term) (t: Type)
+    | TmTAbs (t1: Term) [t: TypeVar]
+        t1.ctx = lhs.ctx
+        t1.tctx = lhs.tctx, t
+
+sort Type
+    inh tyctx TypeVar
+    | TyVar (t@tyctx)
+    | TyArr (t1: Type) (t2: Type)
+        t1.tyctx = lhs.tyctx
+        t2.tyctx = lhs.tyctx
+    | TyAll (t1: Type) [t: TypeVar]
+        t1.tyctx = lhs.tyctx, t
+    | TyBase