testFullSub :: SpecWith ()
testFullSub = test s "FullSub" input output
  where
    s :: Syntactic '[TmApp, TyArr, TmCase, TmRecord, TyRecord, TmFloat, TmLet, TmFix, TmString, TmLam2, TmBool, TmNat, TmArith, TmAscribe, TmAssign, TyVariant, TmTag, TmTry, TmError, TyRef, TmRef, TmDeref, TySource ,TySink, TmUnit, TyUnit, TyBool, TyNat, TyTop, TyBot, TyString, TyVar, TmVar]
    s = crep
    input = [
      "x",
      "if x then false else x",
      "\\x:A.x",
      "timesfloat 2.0 3.0",
      "\"hello\"",
      "0",
      "succ (pred 0)",
      "iszero (pred (succ (succ 0)))",
      "true",
      "if false then true else false",
      "if (x) then true else false",
      "Bool",
      "\\x:Bool.x",
      "Bool->Bool",
      "(\\x:Bool->Bool.x)",
      "(\\x:Bool->Bool.if x false then true else false) (\\x:Bool.if x then false else true)",
      "\\x:Nat.succ x",
      "(\\x:Nat. succ (succ x)) (succ 0)",
      "\\f:T. \\x:Nat. f (f x)",
      "let x=true in x",
      "{x=1.0}.t",
      "Unit",
      "unit",
      "unit as Unit",
      "<l=unit> as <l:Unit, r:Unit>",
      "case a of <phy=x> => x.first | <vir=y> => y.name",
      "\\x:Top.x",
      "(\\r:{x:Top->Top}. r.x r.x) {x=\\z:Top.z, y=\\z:Top.z}",
      "\\x:Bot. x x",
      "\\a:Ref (Nat->Nat).\\n:Nat.(!a n)",
      "\\a:Unit.ref (\\n:Nat.0)",
      "\\a:Ref (Nat->Nat).\\m:Nat.\\n:Nat.let oldf = !a in a := (\\n:Nat.if true then v else (oldf n))",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit",
      "\\x:Top.if error then (try x with true) else false",
      "error true",
      "(\\x:Bool.x) error"]
    output = [
      "x",
      "(if x then false else x)",
      "\\x:A.x",
      "timesfloat (2.0) (3.0)",
      "\"hello\"",
      "0",
      "succ (pred (0))",
      "iszero (pred (succ (succ (0))))",
      "true",
      "(if false then true else false)",
      "(if x then true else false)",
      "Bool",
      "\\x:Bool.x",
      "Bool->Bool",
      "\\x:Bool->Bool.x",
      "(\\x:Bool->Bool.(if (x false) then true else false) \\x:Bool.(if x then false else true))",
      "\\x:Nat.succ (x)",
      "(\\x:Nat.succ (succ (x)) succ (0))",
      "(\\f:T.\\x:Nat.f (f x))",
      "let x = true in x",
      "{x=1.0}.t",
      "Unit",
      "unit",
      "(unit as Unit)",
      "(<l=unit> as <l:Unit, r:Unit>)",
      "case a of <phy=x> => x.first | <vir=y> => y.name",
      "\\x:Top.x",
      "((\\r:{x:Top->Top}.r.x r.x) {x=\\z:Top.z, y=\\z:Top.z})",
      "(\\x:Bot.x x)",
      "\\a:Ref Nat->Nat.\\n:Nat.((!a) n)",
      "\\a:Unit.ref \\n:Nat.0",
      "\\a:Ref Nat->Nat.\\m:Nat.\\n:Nat.let oldf = (!a) in a := \\n:Nat.(if true then v else (oldf n))",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit",
      "\\x:Top.(if error then try x with true else false)",
      "(error true)",
      "(\\x:Bool.x error)"]
testFullSub :: SpecWith ()
testFullSub = test s "FullSub" input output
  where
    s :: Syntactic '[TmApp, TyArr, TmCase, TmRecord, TyRecord, TmFloat, TmLet, TmFix, TmString, TmLam2, TmBool, TmNat, TmArith, TmAscribe, TmAssign, TyVariant, TmTag, TmTry, TmError, TyRef, TmRef, TmDeref, TySource ,TySink, TmUnit, TyUnit, TyBool, TyNat, TyTop, TyBot, TyString, TyVar, TmVar]
    s = crep
    input = [
      "x",
      "if x then false else x",
      "\\x:A.x",
      "timesfloat 2.0 3.0",
      "\"hello\"",
      "0",
      "succ (pred 0)",
      "iszero (pred (succ (succ 0)))",
      "true",
      "if false then true else false",
      "if (x) then true else false",
      "Bool",
      "\\x:Bool.x",
      "Bool->Bool",
      "(\\x:Bool->Bool.x)",
      "(\\x:Bool->Bool.if x false then true else false) (\\x:Bool.if x then false else true)",
      "\\x:Nat.succ x",
      "(\\x:Nat. succ (succ x)) (succ 0)",
      "\\f:T. \\x:Nat. f (f x)",
      "let x=true in x",
      "{x=1.0}.t",
      "Unit",
      "unit",
      "unit as Unit",
      "<l=unit> as <l:Unit, r:Unit>",
      "case a of <phy=x> => x.first | <vir=y> => y.name",
      "\\x:Top.x",
      "(\\r:{x:Top->Top}. r.x r.x) {x=\\z:Top.z, y=\\z:Top.z}",
      "\\x:Bot. x x",
      "\\a:Ref (Nat->Nat).\\n:Nat.(!a n)",
      "\\a:Unit.ref (\\n:Nat.0)",
      "\\a:Ref (Nat->Nat).\\m:Nat.\\n:Nat.let oldf = !a in a := (\\n:Nat.if true then v else (oldf n))",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit",
      "\\x:Top.if error then (try x with true) else false",
      "error true",
      "(\\x:Bool.x) error"]
    output = [
      "x",
      "(if x then false else x)",
      "\\x:A.x",
      "timesfloat (2.0) (3.0)",
      "\"hello\"",
      "0",
      "succ (pred (0))",
      "iszero (pred (succ (succ (0))))",
      "true",
      "(if false then true else false)",
      "(if x then true else false)",
      "Bool",
      "\\x:Bool.x",
      "Bool->Bool",
      "\\x:Bool->Bool.x",
      "(\\x:Bool->Bool.(if (x false) then true else false) \\x:Bool.(if x then false else true))",
      "\\x:Nat.succ (x)",
      "(\\x:Nat.succ (succ (x)) succ (0))",
      "(\\f:T.\\x:Nat.f (f x))",
      "let x = true in x",
      "{x=1.0}.t",
      "Unit",
      "unit",
      "(unit as Unit)",
      "(<l=unit> as <l:Unit, r:Unit>)",
      "case a of <phy=x> => x.first | <vir=y> => y.name",
      "\\x:Top.x",
      "((\\r:{x:Top->Top}.r.x r.x) {x=\\z:Top.z, y=\\z:Top.z})",
      "(\\x:Bot.x x)",
      "\\a:Ref Nat->Nat.\\n:Nat.((!a) n)",
      "\\a:Unit.ref \\n:Nat.0",
      "\\a:Ref Nat->Nat.\\m:Nat.\\n:Nat.let oldf = (!a) in a := \\n:Nat.(if true then v else (oldf n))",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit",
      "\\x:Top.(if error then try x with true else false)",
      "(error true)",
      "(\\x:Bool.x error)"]
testFullSub = test s "FullSub" input output
  where
    s :: Syntactic '[TmApp, TyArr, TmCase, TmRecord, TyRecord, TmFloat, TmLet, TmFix, TmString, TmLam2, TmBool, TmNat, TmArith, TmAscribe, TmAssign, TyVariant, TmTag, TmTry, TmError, TyRef, TmRef, TmDeref, TySource ,TySink, TmUnit, TyUnit, TyBool, TyNat, TyTop, TyBot, TyString, TyVar, TmVar]
    s = crep
    input = [
      "x",
      "if x then false else x",
      "\\x:A.x",
      "timesfloat 2.0 3.0",
      "\"hello\"",
      "0",
      "succ (pred 0)",
      "iszero (pred (succ (succ 0)))",
      "true",
      "if false then true else false",
      "if (x) then true else false",
      "Bool",
      "\\x:Bool.x",
      "Bool->Bool",
      "(\\x:Bool->Bool.x)",
      "(\\x:Bool->Bool.if x false then true else false) (\\x:Bool.if x then false else true)",
      "\\x:Nat.succ x",
      "(\\x:Nat. succ (succ x)) (succ 0)",
      "\\f:T. \\x:Nat. f (f x)",
      "let x=true in x",
      "{x=1.0}.t",
      "Unit",
      "unit",
      "unit as Unit",
      "<l=unit> as <l:Unit, r:Unit>",
      "case a of <phy=x> => x.first | <vir=y> => y.name",
      "\\x:Top.x",
      "(\\r:{x:Top->Top}. r.x r.x) {x=\\z:Top.z, y=\\z:Top.z}",
      "\\x:Bot. x x",
      "\\a:Ref (Nat->Nat).\\n:Nat.(!a n)",
      "\\a:Unit.ref (\\n:Nat.0)",
      "\\a:Ref (Nat->Nat).\\m:Nat.\\n:Nat.let oldf = !a in a := (\\n:Nat.if true then v else (oldf n))",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit",
      "\\x:Top.if error then (try x with true) else false",
      "error true",
      "(\\x:Bool.x) error"]
    output = [
      "x",
      "(if x then false else x)",
      "\\x:A.x",
      "timesfloat (2.0) (3.0)",
      "\"hello\"",
      "0",
      "succ (pred (0))",
      "iszero (pred (succ (succ (0))))",
      "true",
      "(if false then true else false)",
      "(if x then true else false)",
      "Bool",
      "\\x:Bool.x",
      "Bool->Bool",
      "\\x:Bool->Bool.x",
      "(\\x:Bool->Bool.(if (x false) then true else false) \\x:Bool.(if x then false else true))",
      "\\x:Nat.succ (x)",
      "(\\x:Nat.succ (succ (x)) succ (0))",
      "(\\f:T.\\x:Nat.f (f x))",
      "let x = true in x",
      "{x=1.0}.t",
      "Unit",
      "unit",
      "(unit as Unit)",
      "(<l=unit> as <l:Unit, r:Unit>)",
      "case a of <phy=x> => x.first | <vir=y> => y.name",
      "\\x:Top.x",
      "((\\r:{x:Top->Top}.r.x r.x) {x=\\z:Top.z, y=\\z:Top.z})",
      "(\\x:Bot.x x)",
      "\\a:Ref Nat->Nat.\\n:Nat.((!a) n)",
      "\\a:Unit.ref \\n:Nat.0",
      "\\a:Ref Nat->Nat.\\m:Nat.\\n:Nat.let oldf = (!a) in a := \\n:Nat.(if true then v else (oldf n))",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit",
      "\\x:Top.(if error then try x with true else false)",
      "(error true)",
      "(\\x:Bool.x error)"]