testFullRef :: SpecWith ()
testFullRef = test s "FullRef" input output
  where
    s :: Syntactic '[TmApp, TmAssign, TyArr, TmLet, TmLam2, TmRef, TmBool, TmDeref, TyRef, TySink, TySource, TmNat, TyNat, TyUnit, TmVar]
    s = crep
    input = [
      "\\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))",
      "\\x:Top.x",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit"]
    output = [
      "\\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))",
      "\\x:Top.x",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit"]
testFullRef :: SpecWith ()
testFullRef = test s "FullRef" input output
  where
    s :: Syntactic '[TmApp, TmAssign, TyArr, TmLet, TmLam2, TmRef, TmBool, TmDeref, TyRef, TySink, TySource, TmNat, TyNat, TyUnit, TmVar]
    s = crep
    input = [
      "\\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))",
      "\\x:Top.x",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit"]
    output = [
      "\\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))",
      "\\x:Top.x",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit"]
testFullRef = test s "FullRef" input output
  where
    s :: Syntactic '[TmApp, TmAssign, TyArr, TmLet, TmLam2, TmRef, TmBool, TmDeref, TyRef, TySink, TySource, TmNat, TyNat, TyUnit, TmVar]
    s = crep
    input = [
      "\\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))",
      "\\x:Top.x",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit"]
    output = [
      "\\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))",
      "\\x:Top.x",
      "let t = Source Nat in \\x:t.unit",
      "\\x:Sink t.unit"]