testFullSimple :: SpecWith ()
testFullSimple = test s "FullSimple" input output
  where
    s :: Syntactic '[TmApp, TyArr, TmCase, TmRecord, TmFloat, TmLet, TmFix, TmString, TmLam2, TmBool, TmNat, TmArith, TmAscribe, TyVariant, TmTag, TmUnit, TyUnit, TyBool, TyNat, 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",
      "\\a:Unit.fix (\\x:T.x)"]
    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",
      "\\a:Unit.fix (\\x:T.x)"]
testFullSimple :: SpecWith ()
testFullSimple = test s "FullSimple" input output
  where
    s :: Syntactic '[TmApp, TyArr, TmCase, TmRecord, TmFloat, TmLet, TmFix, TmString, TmLam2, TmBool, TmNat, TmArith, TmAscribe, TyVariant, TmTag, TmUnit, TyUnit, TyBool, TyNat, 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",
      "\\a:Unit.fix (\\x:T.x)"]
    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",
      "\\a:Unit.fix (\\x:T.x)"]
testFullSimple = test s "FullSimple" input output
  where
    s :: Syntactic '[TmApp, TyArr, TmCase, TmRecord, TmFloat, TmLet, TmFix, TmString, TmLam2, TmBool, TmNat, TmArith, TmAscribe, TyVariant, TmTag, TmUnit, TyUnit, TyBool, TyNat, 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",
      "\\a:Unit.fix (\\x:T.x)"]
    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",
      "\\a:Unit.fix (\\x:T.x)"]