agda/examples/outdated-and-incorrect/Alonzo/Records.hs

{-# OPTIONS -fglasgow-exts #-}

-- Generated by Alonzo

module Records where
import RTS
import qualified RTP
import qualified Nat
import qualified Bool
name1 = "Point"

data T1 a b = C1 a b
d1 = ()
name2 = "x"
d2 = d2_1
  where d2_1 (Records.C1 v0 _) = cast v0
name3 = "y"
d3 = d3_1
  where d3_1 (Records.C1 _ v0) = cast v0
name4 = "Point'"

data T4 a b = C7 a b
d4 = ()
name7 = "mkPoint"
name8 = "origin"
d8 = d8_1
  where d8_1
          = cast
              (Records.C1 (cast (RTP._primIntToNat (0 :: Prelude.Int)))
                 (cast (RTP._primIntToNat (0 :: Prelude.Int))))
name9 = "origin'"
d9 = d9_1
  where d9_1
          = cast
              (Records.C7 (cast (RTP._primIntToNat (0 :: Prelude.Int)))
                 (cast (RTP._primIntToNat (0 :: Prelude.Int))))
name10 = "getX"
d10 = d10_1
  where d10_1 = cast Records.d2
name11 = "sum"
d11 = d11_1
  where d11_1 v0
          = cast
              (Nat.d4 (cast (Records.d16 (cast v0)))
                 (cast (Records.d17 (cast v0))))
name16 = "x"
d16 = d16_1
  where d16_1 v0 = cast (Records.d2 (cast v0))
name17 = "y"
d17 = d17_1
  where d17_1 v0 = cast (Records.d3 (cast v0))
name20 = "_==_"

data T20 = C23
d20 v2 v1 = ()
name23 = "refl"
name25 = "\951-Point"
d25 = d25_1
  where d25_1 _ = cast Records.C23
name27 = "True"

data T27 = C27
d27 = ()
name28 = "tt"
d28 = d28_1
  where d28_1 = cast Records.C27
name29 = "False"

data T29 = C29
d29 = ()
name30 = "NonZero"
d30 = d30_1
  where d30_1 (Nat.C2) = cast Records.d29
        d30_1 a = cast d30_2 a
        d30_2 (Nat.C3 _) = cast Records.d27
name34 = "_/_"
d34 = d34_1
  where d34_1 _ (Nat.C2) _ = undefined
        d34_1 a b c = cast d34_2 a b c
        d34_2 (Nat.C2) (Nat.C3 _) v0 = cast Nat.C2
        d34_2 a b c = cast d34_3 a b c
        d34_3 (Nat.C3 v0) (Nat.C3 v1) v2
          = cast
              (Records.d41 (cast v0) (cast v1) (cast v2)
                 (cast (Nat.C3 (cast v0)))
                 (cast (Nat.C3 (cast v1)))
                 (cast v1))
name41 = "div"
d41 = d41_1
  where d41_1 v0 v1 v2 (Nat.C2) (Nat.C2) _
          = cast (Nat.C3 (cast Nat.C2))
        d41_1 a b c d e f = cast d41_2 a b c d e f
        d41_2 v0 v1 v2 (Nat.C2) (Nat.C3 _) v3 = cast Nat.C2
        d41_2 a b c d e f = cast d41_3 a b c d e f
        d41_3 v0 v1 v2 (Nat.C3 v3) (Nat.C2) v4
          = cast
              (Nat.C3
                 (cast
                    (Records.d41 (cast v0) (cast v1) (cast v2) (cast v3) (cast v4)
                       (cast v4))))
        d41_3 a b c d e f = cast d41_4 a b c d e f
        d41_4 v0 v1 v2 (Nat.C3 v3) (Nat.C3 v4) v5
          = cast
              (Records.d41 (cast v0) (cast v1) (cast v2) (cast v3) (cast v4)
                 (cast v5))
name50 = "five"
d50 = d50_1
  where d50_1
          = cast
              (Records.d34 (cast (RTP._primIntToNat (17 :: Prelude.Int)))
                 (cast (RTP._primIntToNat (3 :: Prelude.Int)))
                 (cast Records.C27))
name53 = "\8707"

data T53 a b = C53 a b
d53 = ()
name56 = "witness"
d56 = d56_1
  where d56_1 _ _ (Records.C53 v0 _) = cast v0
name57 = "proof"
d57 = d57_1
  where d57_1 _ _ (Records.C53 _ v0) = cast v0