Add test

Implementation of quoted pattern matching formalization.

Additions:
 * `T-Abs`, `T-Pat-Var` and `T-Pat-Abs` require a context that does not already define their name
 * `Fix` and required renaming

Author: nicolasstucki

tests/run/quoted-sematics-1.check

@@ -0,0 +1,106 @@
+Input: Nat(1)
+ Type: NatType
+Result: Nat(1)
+
+Failed to type Nat(-1) at level 0 with enviroment Set()
+Failed to typechecks: Nat(-1)
+
+Input: Box(Nat(2))
+ Type: BoxType(NatType)
+Result: Box(Nat(2))
+
+Input: Lift(Nat(3))
+ Type: BoxType(NatType)
+Step: Box(Nat(3))
+Result: Box(Nat(3))
+
+Input: Lambda(x,NatType,Ref(x))
+ Type: LambdaType(NatType,NatType)
+Result: Lambda(x,NatType,Ref(x))
+
+Input: App(Lambda(x,NatType,Ref(x)),Nat(4))
+ Type: NatType
+Step: Nat(4)
+Result: Nat(4)
+
+Input: Box(Splice(Box(Nat(1))))
+ Type: BoxType(NatType)
+Step: Box(Nat(1))
+Result: Box(Nat(1))
+
+Input: Box(Splice(Lift(Nat(1))))
+ Type: BoxType(NatType)
+Step: Box(Splice(Box(Nat(1))))
+Step: Box(Nat(1))
+Result: Box(Nat(1))
+
+Input: Box(Splice(Box(App(Lambda(x,NatType,Ref(x)),Splice(Lift(Nat(4)))))))
+ Type: BoxType(NatType)
+Step: Box(Splice(Box(App(Lambda(x,NatType,Ref(x)),Splice(Box(Nat(4)))))))
+Step: Box(Splice(Box(App(Lambda(x,NatType,Ref(x)),Nat(4)))))
+Step: Box(App(Lambda(x,NatType,Ref(x)),Nat(4)))
+Result: Box(App(Lambda(x,NatType,Ref(x)),Nat(4)))
+
+Input: Match(Box(Nat(2)),PNat(2),Nat(0),Nat(1))
+ Type: NatType
+Step: Nat(0)
+Result: Nat(0)
+
+Input: Match(Box(Nat(2)),PNat(3),Nat(1),Nat(0))
+ Type: NatType
+Step: Nat(0)
+Result: Nat(0)
+
+Input: Match(Box(Nat(2)),PLit(x),Ref(x),Nat(0))
+ Type: NatType
+Step: Nat(2)
+Result: Nat(2)
+
+Input: Match(Box(Nat(2)),PBind(x),Ref(x),Box(Nat(0)))
+ Type: BoxType(NatType)
+Step: Box(Nat(2))
+Result: Box(Nat(2))
+
+Input: Match(Box(Lambda(y,NatType,Ref(y))),PBind(x),Ref(x),Box(Lambda(y2,NatType,Nat(2))))
+ Type: BoxType(LambdaType(NatType,NatType))
+Step: Box(Lambda(x1,NatType,Ref(x1)))
+Result: Box(Lambda(x1,NatType,Ref(x1)))
+
+Input: Match(Box(App(Lambda(y,NatType,Ref(y)),Nat(4))),PApp(PFun(f),PBind(x)),App(Ref(f),Ref(x)),Box(Nat(3)))
+ Type: BoxType(NatType)
+Step: App(Lambda(x4,BoxType(NatType),Box(Splice(Ref(x4)))),Box(Nat(4)))
+Step: Box(Splice(Box(Nat(4))))
+Step: Box(Nat(4))
+Result: Box(Nat(4))
+
+Failed to type Lambda(x,NatType,Ref(x)) at level 1 with enviroment Set(EnvVar(x,1,NatType))
+Failed to type Lambda(x,NatType,Lambda(x,NatType,Ref(x))) at level 1 with enviroment Set()
+Failed to type Box(Lambda(x,NatType,Lambda(x,NatType,Ref(x)))) at level 0 with enviroment Set()
+Failed to typechecks: Box(Lambda(x,NatType,Lambda(x,NatType,Ref(x))))
+
+Input: Fix(Lambda(x,NatType,Nat(1)))
+ Type: NatType
+Step: Nat(1)
+Result: Nat(1)
+
+Input: App(Fix(Lambda(f,LambdaType(NatType,NatType),Lambda(n,NatType,Match(Lift(Ref(n)),PNat(0),Nat(1),App(Lambda(a,NatType,App(Ref(f),Ref(a))),Nat(0)))))),Nat(1))
+ Type: NatType
+Step: App(Lambda(n,NatType,Match(Lift(Ref(n)),PNat(0),Nat(1),App(Lambda(a,NatType,App(Fix(Lambda(x6,LambdaType(NatType,NatType),Lambda(x7,NatType,Match(Lift(Ref(x7)),PNat(0),Nat(1),App(Lambda(x8,NatType,App(Ref(x6),Ref(x8))),Nat(0)))))),Ref(a))),Nat(0)))),Nat(1))
+Step: Match(Lift(Nat(1)),PNat(0),Nat(1),App(Lambda(a,NatType,App(Fix(Lambda(x6,LambdaType(NatType,NatType),Lambda(x7,NatType,Match(Lift(Ref(x7)),PNat(0),Nat(1),App(Lambda(x8,NatType,App(Ref(x6),Ref(x8))),Nat(0)))))),Ref(a))),Nat(0)))
+Step: Match(Box(Nat(1)),PNat(0),Nat(1),App(Lambda(a,NatType,App(Fix(Lambda(x6,LambdaType(NatType,NatType),Lambda(x7,NatType,Match(Lift(Ref(x7)),PNat(0),Nat(1),App(Lambda(x8,NatType,App(Ref(x6),Ref(x8))),Nat(0)))))),Ref(a))),Nat(0)))
+Step: App(Lambda(a,NatType,App(Fix(Lambda(x6,LambdaType(NatType,NatType),Lambda(x7,NatType,Match(Lift(Ref(x7)),PNat(0),Nat(1),App(Lambda(x8,NatType,App(Ref(x6),Ref(x8))),Nat(0)))))),Ref(a))),Nat(0))
+Step: App(Fix(Lambda(x6,LambdaType(NatType,NatType),Lambda(x7,NatType,Match(Lift(Ref(x7)),PNat(0),Nat(1),App(Lambda(x8,NatType,App(Ref(x6),Ref(x8))),Nat(0)))))),Nat(0))
+Step: App(Lambda(x7,NatType,Match(Lift(Ref(x7)),PNat(0),Nat(1),App(Lambda(x8,NatType,App(Fix(Lambda(x9,LambdaType(NatType,NatType),Lambda(x10,NatType,Match(Lift(Ref(x10)),PNat(0),Nat(1),App(Lambda(x11,NatType,App(Ref(x9),Ref(x11))),Nat(0)))))),Ref(x8))),Nat(0)))),Nat(0))
+Step: Match(Lift(Nat(0)),PNat(0),Nat(1),App(Lambda(x8,NatType,App(Fix(Lambda(x9,LambdaType(NatType,NatType),Lambda(x10,NatType,Match(Lift(Ref(x10)),PNat(0),Nat(1),App(Lambda(x11,NatType,App(Ref(x9),Ref(x11))),Nat(0)))))),Ref(x8))),Nat(0)))
+Step: Match(Box(Nat(0)),PNat(0),Nat(1),App(Lambda(x8,NatType,App(Fix(Lambda(x9,LambdaType(NatType,NatType),Lambda(x10,NatType,Match(Lift(Ref(x10)),PNat(0),Nat(1),App(Lambda(x11,NatType,App(Ref(x9),Ref(x11))),Nat(0)))))),Ref(x8))),Nat(0)))
+Step: Nat(1)
+Result: Nat(1)
+
+Input: App(Lambda(x,BoxType(NatType),Match(Ref(x),PApp(PFun(f),PBind(x2)),App(Ref(f),Ref(x)),Box(Nat(4)))),Box(App(Lambda(a,NatType,App(Lambda(b,NatType,Ref(b)),Ref(a))),Nat(2))))
+ Type: BoxType(NatType)
+Step: Match(Box(App(Lambda(x13,NatType,App(Lambda(x14,NatType,Ref(x14)),Ref(x13))),Nat(2))),PApp(PFun(f),PBind(x2)),App(Ref(f),Box(App(Lambda(x13,NatType,App(Lambda(x14,NatType,Ref(x14)),Ref(x13))),Nat(2)))),Box(Nat(4)))
+Step: App(Lambda(x17,BoxType(NatType),Box(App(Lambda(x18,NatType,Ref(x18)),Splice(Ref(x17))))),Box(App(Lambda(x13,NatType,App(Lambda(x14,NatType,Ref(x14)),Ref(x13))),Nat(2))))
+Step: Box(App(Lambda(x18,NatType,Ref(x18)),Splice(Box(App(Lambda(x19,NatType,App(Lambda(x20,NatType,Ref(x20)),Ref(x19))),Nat(2))))))
+Step: Box(App(Lambda(x18,NatType,Ref(x18)),App(Lambda(x19,NatType,App(Lambda(x20,NatType,Ref(x20)),Ref(x19))),Nat(2))))
+Result: Box(App(Lambda(x18,NatType,Ref(x18)),App(Lambda(x19,NatType,App(Lambda(x20,NatType,Ref(x20)),Ref(x19))),Nat(2))))
+