{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Untyped.Relation.Binary.Core where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.Untyped

-- Untyped.Relation.Binary.Core.Relation
d_Relation_8 :: ()
d_Relation_8 :: ()
d_Relation_8 = ()
forall a. a
erased
-- Untyped.Relation.Binary.Core.Relation*
d_Relation'42'_12 :: ()
d_Relation'42'_12 :: ()
d_Relation'42'_12 = ()
forall a. a
erased
-- Untyped.Relation.Binary.Core.Pointwise
d_Pointwise_20 :: p -> p -> p -> p -> ()
d_Pointwise_20 p
a0 p
a1 p
a2 p
a3 = ()
data T_Pointwise_20
  = C_'91''93'_26 | C__'8759'__36 AgdaAny T_Pointwise_20
-- Untyped.Relation.Binary.Core.DecidableRel
d_DecidableRel_38 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_DecidableRel_38 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_DecidableRel_38 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Core.pointwise?
d_pointwise'63'_56 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  Integer ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_pointwise'63'_56 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Dec_20
d_pointwise'63'_56 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v0 Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
v1 Integer
v2 [T__'8866'_14]
v3 [T__'8866'_14]
v4
  = (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Integer -> [T__'8866'_14] -> [T__'8866'_14] -> T_Dec_20
du_pointwise'63'_56 Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
v1 Integer
v2 [T__'8866'_14]
v3 [T__'8866'_14]
v4
du_pointwise'63'_56 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  Integer ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_pointwise'63'_56 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Integer -> [T__'8866'_14] -> [T__'8866'_14] -> T_Dec_20
du_pointwise'63'_56 Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
v0 Integer
v1 [T__'8866'_14]
v2 [T__'8866'_14]
v3
  = case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v2 of
      []
        -> case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v3 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
                       Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                       (T_Pointwise_20 -> Any
forall a b. a -> b
coe T_Pointwise_20
C_'91''93'_26))
             (:) Any
v4 [Any]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             [Any]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) Any
v4 [Any]
v5
        -> case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v3 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             (:) Any
v6 [Any]
v7
               -> let v8 :: Any
v8
                        = (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                            T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84
                            ((Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Integer -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
v0 Integer
v1 Any
v4 Any
v6)
                            (((Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
 -> Integer -> [T__'8866'_14] -> [T__'8866'_14] -> T_Dec_20)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Integer -> [T__'8866'_14] -> [T__'8866'_14] -> T_Dec_20
du_pointwise'63'_56 ((Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20) -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v5) ([Any] -> Any
forall a b. a -> b
coe [Any]
v7)) in
                  Any -> T_Dec_20
forall a b. a -> b
coe
                    (case Any -> T_Dec_20
forall a b. a -> b
coe Any
v8 of
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
                         -> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
                              then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v10 of
                                     MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v11
                                       -> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v11 of
                                            MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v12 Any
v13
                                              -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                   Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                   (Bool -> Any
forall a b. a -> b
coe Bool
v9)
                                                   ((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
                                                      Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                                                      ((Any -> T_Pointwise_20 -> T_Pointwise_20) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> T_Pointwise_20 -> T_Pointwise_20
C__'8759'__36 Any
v12 Any
v13))
                                            T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                              else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                     Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v10)
                                     ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                        Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                        (Bool -> Any
forall a b. a -> b
coe Bool
v9)
                                        (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
                       T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [Any]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      [Any]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError