Comments (38)
VictorCMiraldo
commented on August 22, 2024
1
from generics-mrsop.
arianvp
commented on August 22, 2024
https://github.com/VictorCMiraldo/generics-mrsop/tree/ghc-bug
GHC head doesn't work either :'(
from generics-mrsop.
arianvp
commented on August 22, 2024
To build against GHC head:
nix-shell --argstr compiler ghcHEAD
cabal build
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
I'll make a mutually recursive family smaller than the GoAST but bigger than what we've been doing and I'll check which phase experiences the leak. This should help us diagnose this issue.
from generics-mrsop.
arianvp
commented on August 22, 2024
I have just done that 5186843
You can turn data types into Empty Datatypes to vary the amount of memory used:
for example, turn data B = ... into just data B
Edit:
Woah, the first 8 values of the commit hash are numbers! Are we officially a PoW blockchain now?
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
@arianvp ,
Using your example and compiling the monster twice, once with the E type, the other without, I got the following numbers with -dshow-passes. I then made a CSV file for easier comparisson.
Edit: The data below is useless by itself. I'll run three times, each adding an additional datatype, so we
can compare the slowdowns. I believe that that's what we are looking for...
Edit2: removed the nonsense numbers
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
Ok,
I ran the Bug triggering code four times, once with types A, B, C, D, then I added E, then F and finally added G.
FWIW I plotted the numbers: https://imgur.com/a/tfyGQ
The simplifier is where the steepest increases both in memory and time are. I have all in a ods file if anyone is interested.
from generics-mrsop.
arianvp
commented on August 22, 2024
Next step, trigger the bug not with an AST + TH, but without TH? And then send it to the mailing list?
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
Ideally, we'd like to trigger the bug without any reference to our library. I can try a couple things tomorrow
But yes, if we can produce a minimal working example about this bug it would be awesome.
from generics-mrsop.
arianvp
commented on August 22, 2024
Is there also still any problem do that due to the paper still being in
review?
…On Wed, Mar 28, 2018, 18:11 Victor Cacciari Miraldo < ***@***.***> wrote:
Ideally, we'd like to trigger the bug without any reference to our
library. I can try a couple things tomorrow
But yes, if we can produce a minimal working example about this bug it
would be awesome.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#6 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAmWowHyQqEG0MZDjISN0BOkU7riUPxLks5ti7YVgaJpZM4S7Ngd>
.
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
There is the risk of a reviewer seeing this and thinking its a reason to reject the paper, which
I'd disagree with, but you know how these things go.
from generics-mrsop.
serras
commented on August 22, 2024
A bug ticket: https://ghc.haskell.org/trac/ghc/ticket/11195
And the rest of the tickets related to the new pattern matching: https://ghc.haskell.org/trac/ghc/wiki/PatternMatchCheck
from generics-mrsop.
serras
commented on August 22, 2024
Try with fmax-pmcheck-iterations=n with some number of n in the order of thousands?
from generics-mrsop.
arianvp
commented on August 22, 2024
Moving to base10 numbers instead of base1 seems to have solved it :) Memory usage is constant now :)) Because we compute the numbers during compile time with TH, writing them down in a Base10 format should not be an issue for us. We know all indices beforehand. This reduces the amount of steps to O(lg n) from O(n) for the Lkup type family
Here is an example where you can only have upto 9 constructors. using the Lkup'' type family. But it can easily be changed to use arbitrary base-10 numbers using the Lkup' type family.
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FunctionalDependencies #-}
module Minimal where
import GHC.TypeLits (TypeError, ErrorMessage (..))
import Data.Proxy
data Nat = S Nat | Z
deriving (Eq , Show)
data SNat :: Nat -> * where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
type family Lkup (n :: Nat) (ks :: [k]) :: k where
Lkup Z (k : ks) = k
Lkup (S n) (k : ks) = Lkup n ks
Lkup _ '[] = TypeError (Text "Lkup index too big")
data El :: [*] -> Digit -> * where
El :: {unEl :: Lkup'' ix fam} -> El fam ix
data NS :: (k -> *) -> [k] -> * where
T :: NS p xs -> NS p (x : xs)
H :: p x -> NS p (x : xs)
infixr 5 :*
data NP :: (k -> *) -> [k] -> * where
NP0 :: NP p '[]
(:*) :: p x -> NP p xs -> NP p (x : xs)
data Atom kon
= K kon
| I Digit
deriving (Eq, Show)
data NA :: (kon -> *) -> (Digit -> *) -> Atom kon -> * where
NA_I :: phi k -> NA ki phi (I k)
NA_K :: ki k -> NA ki phi (K k)
data Kon
= KInt
| KInteger
| KBool
| KFloat
| KChar
| KString
deriving (Eq , Show)
data Singl (kon :: Kon) :: * where
SInt :: Int -> Singl KInt
SInteger :: Integer -> Singl KInteger
SBool :: Bool -> Singl KBool
SFloat :: Float -> Singl KFloat
SChar :: Char -> Singl KChar
SString :: String -> Singl KString
deriving instance Show (Singl k)
deriving instance Eq (Singl k)
eqSingl :: Singl k -> Singl k -> Bool
eqSingl = (==)
class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]])
| fam -> ki codes , ki codes -> fam
where
sto' :: SDigit ix -> Rep ki (El fam) (Lkup'' ix codes) -> ()
newtype Rep (ki :: kon -> *) (phi :: Digit -> *) (code :: [[Atom kon]])
= Rep { unRep :: NS (PoA ki phi) code }
type PoA (ki :: kon -> *) (phi :: Digit -> *) = NP (NA ki phi)
data Digit = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 deriving (Eq, Show)
data SDigit :: Digit -> * where
SD0 :: SDigit D0
SD1 :: SDigit D1
SD2 :: SDigit D2
SD3 :: SDigit D3
SD4 :: SDigit D4
SD5 :: SDigit D5
SD6 :: SDigit D6
SD7 :: SDigit D7
SD8 :: SDigit D8
SD9 :: SDigit D9
-- special case because I'm too lazy to deal with recursion
type family Lkup'' (n :: Digit) (ks :: [k]) :: k where
Lkup'' D0 (k ': ks) = k
Lkup'' D1 (_ ': k ': ks) = k
Lkup'' D2 (_ ': _ ': k ': ks) = k
Lkup'' D3 (_ ': _ ': _ ': k ': ks) = k
Lkup'' D4 (_ ': _ ': _ ': _ ': k ': ks) = k
Lkup'' D5 (_ ':_ ': _ ': _ ': _ ': k ': ks) = k
Lkup'' D6 (_ ': _ ': _ ': _ ': _ ': _ ': k ': ks) = k
Lkup'' D7 (_ ': _ ': _ ': _ ': _ ': _ ': _ ': k ': ks) = k
Lkup'' D8 (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': k ': ks) = k
Lkup'' D9 (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': k ': ks) = k
-- logarithmic lookup function
type family Lkup' (n :: [Digit]) (ks :: [k]) :: k where
Lkup' '[] ks = TypeError (Text "Empty numeral")
Lkup' (D0 ': '[]) (k ': ks) = k
Lkup' (D1 ': '[]) (_ ': k ': ks) = k
Lkup' (D2 ': '[]) (_ ': _ ': k ': ks) = k
Lkup' (D3 ': '[]) (_ ': _ ': _ ': k ': ks) = k
Lkup' (D4 ': '[]) (_ ': _ ': _ ': _ ': k ': ks) = k
Lkup' (D5 ': '[]) (_ ':_ ': _ ': _ ': _ ': k ': ks) = k
Lkup' (D6 ': '[]) (_ ': _ ': _ ': _ ': _ ': _ ': k ': ks) = k
Lkup' (D7 ': '[]) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': k ': ks) = k
Lkup' (D8 ': '[]) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': k ': ks) = k
Lkup' (D9 ': '[]) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': k ': ks) = k
Lkup' (D1 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D1 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' (D2 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D2 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' (D3 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D3 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' (D4 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D4 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' (D5 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D5 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' (D6 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D6 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' (D7 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D7 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' (D8 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D8 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' (D9 ': ds) (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': ks) = Lkup' ds ks
Lkup' (D9 ': ds) _ = TypeError (Text "Out of bounds")
Lkup' _ '[] = TypeError (Text "Not found")
-- if recursion, we can skip 10 elements
type TestList200El = '[(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),(),()]
type TestIdx = D1 ': D0 ': D3 ': '[]
type Val = Lkup' TestIdx TestList200El
type FamA = '[(), (), (), (), (), (), ()]
type D0' = S Z
type D1' = S (S Z)
type D2' = S (S (S Z))
type D3' = S (S (S (S Z)))
type D4' = S (S (S (S (S Z))))
type D5' = S (S (S (S (S (S Z)))))
type D6' = S (S (S (S (S (S (S Z))))))
type D7' = S (S (S (S (S (S (S (S Z)))))))
type D8' = S (S (S (S (S (S (S (S (S Z))))))))
type D9' = S (S (S (S (S (S (S (S (S (S Z)))))))))
type LOL2 = '[I D0, I D1 , I D2 , I D3 , I D4 , I D5 , I D6]
type LOL = '[ LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2, LOL2 ]
type CodesA = '[ LOL, LOL, LOL, LOL, LOL, LOL, LOL]
instance Family Singl FamA CodesA where
sto'
= \case
SD0 -> \case
(Rep (H (NA_I (El y_aGws) :* (NA_I (El y_aGwt) :* (NA_I (El y_aGwu) :* (NA_I (El y_aGwv) :* (NA_I (El y_aGww) :* (NA_I (El y_aGwx) :* (NA_I (El y_aGwy) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGwH) :* (NA_I (El y_aGwI) :* (NA_I (El y_aGwK) :* (NA_I (El y_aGwL) :* (NA_I (El y_aGwM) :* (NA_I (El y_aGwN) :* (NA_I (El y_aGwO) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGwZ) :* (NA_I (El y_aGx0) :* (NA_I (El y_aGx1) :* (NA_I (El y_aGx2) :* (NA_I (El y_aGx3) :* (NA_I (El y_aGx4) :* (NA_I (El y_aGx5) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGx6) :* (NA_I (El y_aGx7) :* (NA_I (El y_aGx8) :* (NA_I (El y_aGx9) :* (NA_I (El y_aGxa) :* (NA_I (El y_aGxb) :* (NA_I (El y_aGxc) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGxd) :* (NA_I (El y_aGxe) :* (NA_I (El y_aGxg) :* (NA_I (El y_aGxh) :* (NA_I (El y_aGxi) :* (NA_I (El y_aGxj) :* (NA_I (El y_aGxk) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGxl) :* (NA_I (El y_aGxm) :* (NA_I (El y_aGxn) :* (NA_I (El y_aGxo) :* (NA_I (El y_aGxp) :* (NA_I (El y_aGxq) :* (NA_I (El y_aGxr) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGxs) :* (NA_I (El y_aGxt) :* (NA_I (El y_aGxu) :* (NA_I (El y_aGxv) :* (NA_I (El y_aGxw) :* (NA_I (El y_aGxx) :* (NA_I (El y_aGxy) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGxz) :* (NA_I (El y_aGxA) :* (NA_I (El y_aGxB) :* (NA_I (El y_aGxC) :* (NA_I (El y_aGxD) :* (NA_I (El y_aGxE) :* (NA_I (El y_aGxF) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxG) :* (NA_I (El y_aGxH) :* (NA_I (El y_aGxI) :* (NA_I (El y_aGxJ) :* (NA_I (El y_aGxK) :* (NA_I (El y_aGxL) :* (NA_I (El y_aGxM) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxN) :* (NA_I (El y_aGxO) :* (NA_I (El y_aGxP) :* (NA_I (El y_aGxQ) :* (NA_I (El y_aGxR) :* (NA_I (El y_aGxS) :* (NA_I (El y_aGxT) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxU) :* (NA_I (El y_aGxV) :* (NA_I (El y_aGxW) :* (NA_I (El y_aGxX) :* (NA_I (El y_aGxY) :* (NA_I (El y_aGxZ) :* (NA_I (El y_aGy0) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGy1) :* (NA_I (El y_aGy2) :* (NA_I (El y_aGy3) :* (NA_I (El y_aGy4) :* (NA_I (El y_aGy5) :* (NA_I (El y_aGy6) :* (NA_I (El y_aGy7) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGy8) :* (NA_I (El y_aGy9) :* (NA_I (El y_aGya) :* (NA_I (El y_aGyb) :* (NA_I (El y_aGyc) :* (NA_I (El y_aGyd) :* (NA_I (El y_aGye) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGyf) :* (NA_I (El y_aGyg) :* (NA_I (El y_aGyh) :* (NA_I (El y_aGyi) :* (NA_I (El y_aGyj) :* (NA_I (El y_aGyk) :* (NA_I (El y_aGyl) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGym) :* (NA_I (El y_aGyn) :* (NA_I (El y_aGyo) :* (NA_I (El y_aGyp) :* (NA_I (El y_aGyq) :* (NA_I (El y_aGyr) :* (NA_I (El y_aGys) :* NP0))))))))))))))))))))))) -> ()
SD1 -> \case
(Rep (H (NA_I (El y_aGyt) :* (NA_I (El y_aGyu) :* (NA_I (El y_aGyv) :* (NA_I (El y_aGyw) :* (NA_I (El y_aGyx) :* (NA_I (El y_aGyy) :* (NA_I (El y_aGyz) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGyA) :* (NA_I (El y_aGyB) :* (NA_I (El y_aGyC) :* (NA_I (El y_aGyD) :* (NA_I (El y_aGyE) :* (NA_I (El y_aGyF) :* (NA_I (El y_aGyG) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGyH) :* (NA_I (El y_aGyI) :* (NA_I (El y_aGyJ) :* (NA_I (El y_aGyK) :* (NA_I (El y_aGyL) :* (NA_I (El y_aGyM) :* (NA_I (El y_aGyN) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGyO) :* (NA_I (El y_aGyP) :* (NA_I (El y_aGyQ) :* (NA_I (El y_aGyR) :* (NA_I (El y_aGyS) :* (NA_I (El y_aGyT) :* (NA_I (El y_aGyU) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGyV) :* (NA_I (El y_aGyW) :* (NA_I (El y_aGyX) :* (NA_I (El y_aGyY) :* (NA_I (El y_aGyZ) :* (NA_I (El y_aGz0) :* (NA_I (El y_aGz1) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGz3) :* (NA_I (El y_aGz4) :* (NA_I (El y_aGz5) :* (NA_I (El y_aGz6) :* (NA_I (El y_aGz7) :* (NA_I (El y_aGz8) :* (NA_I (El y_aGz9) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGza) :* (NA_I (El y_aGzb) :* (NA_I (El y_aGzc) :* (NA_I (El y_aGzd) :* (NA_I (El y_aGze) :* (NA_I (El y_aGzg) :* (NA_I (El y_aGzh) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGzi) :* (NA_I (El y_aGzj) :* (NA_I (El y_aGzk) :* (NA_I (El y_aGzl) :* (NA_I (El y_aGzm) :* (NA_I (El y_aGzn) :* (NA_I (El y_aGzo) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzp) :* (NA_I (El y_aGzq) :* (NA_I (El y_aGzs) :* (NA_I (El y_aGzt) :* (NA_I (El y_aGzu) :* (NA_I (El y_aGzv) :* (NA_I (El y_aGzw) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzz) :* (NA_I (El y_aGzA) :* (NA_I (El y_aGzB) :* (NA_I (El y_aGzC) :* (NA_I (El y_aGzD) :* (NA_I (El y_aGzE) :* (NA_I (El y_aGzF) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzH) :* (NA_I (El y_aGzI) :* (NA_I (El y_aGzJ) :* (NA_I (El y_aGzM) :* (NA_I (El y_aGzN) :* (NA_I (El y_aGzO) :* (NA_I (El y_aGzP) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzQ) :* (NA_I (El y_aGzR) :* (NA_I (El y_aGzS) :* (NA_I (El y_aGzT) :* (NA_I (El y_aGzU) :* (NA_I (El y_aGzV) :* (NA_I (El y_aGzW) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzX) :* (NA_I (El y_aGzY) :* (NA_I (El y_aGzZ) :* (NA_I (El y_aGA0) :* (NA_I (El y_aGA1) :* (NA_I (El y_aGA2) :* (NA_I (El y_aGA3) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGA5) :* (NA_I (El y_aGA6) :* (NA_I (El y_aGA7) :* (NA_I (El y_aGA8) :* (NA_I (El y_aGA9) :* (NA_I (El y_aGAa) :* (NA_I (El y_aGAb) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGAc) :* (NA_I (El y_aGAd) :* (NA_I (El y_aGAe) :* (NA_I (El y_aGAf) :* (NA_I (El y_aGAg) :* (NA_I (El y_aGAh) :* (NA_I (El y_aGAi) :* NP0))))))))))))))))))))))) -> ()
SD2 -> \case
(Rep (H (NA_I (El y_aGAj) :* (NA_I (El y_aGAk) :* (NA_I (El y_aGAl) :* (NA_I (El y_aGAm) :* (NA_I (El y_aGAn) :* (NA_I (El y_aGAo) :* (NA_I (El y_aGAp) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGAq) :* (NA_I (El y_aGAr) :* (NA_I (El y_aGAs) :* (NA_I (El y_aGAt) :* (NA_I (El y_aGAu) :* (NA_I (El y_aGAv) :* (NA_I (El y_aGAw) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGAx) :* (NA_I (El y_aGAy) :* (NA_I (El y_aGAz) :* (NA_I (El y_aGAA) :* (NA_I (El y_aGAB) :* (NA_I (El y_aGAC) :* (NA_I (El y_aGAD) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGAE) :* (NA_I (El y_aGAF) :* (NA_I (El y_aGAG) :* (NA_I (El y_aGAH) :* (NA_I (El y_aGAI) :* (NA_I (El y_aGAJ) :* (NA_I (El y_aGAK) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGAL) :* (NA_I (El y_aGAM) :* (NA_I (El y_aGAN) :* (NA_I (El y_aGAO) :* (NA_I (El y_aGAP) :* (NA_I (El y_aGAQ) :* (NA_I (El y_aGAR) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGAS) :* (NA_I (El y_aGAT) :* (NA_I (El y_aGAU) :* (NA_I (El y_aGAV) :* (NA_I (El y_aGAW) :* (NA_I (El y_aGAX) :* (NA_I (El y_aGAY) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGAZ) :* (NA_I (El y_aGB0) :* (NA_I (El y_aGB1) :* (NA_I (El y_aGB2) :* (NA_I (El y_aGB3) :* (NA_I (El y_aGB4) :* (NA_I (El y_aGB5) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGB6) :* (NA_I (El y_aGB7) :* (NA_I (El y_aGB8) :* (NA_I (El y_aGB9) :* (NA_I (El y_aGBa) :* (NA_I (El y_aGBb) :* (NA_I (El y_aGBc) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBd) :* (NA_I (El y_aGBe) :* (NA_I (El y_aGBf) :* (NA_I (El y_aGBg) :* (NA_I (El y_aGBh) :* (NA_I (El y_aGBi) :* (NA_I (El y_aGBj) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBk) :* (NA_I (El y_aGBl) :* (NA_I (El y_aGBm) :* (NA_I (El y_aGBn) :* (NA_I (El y_aGBo) :* (NA_I (El y_aGBp) :* (NA_I (El y_aGBq) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBr) :* (NA_I (El y_aGBs) :* (NA_I (El y_aGBt) :* (NA_I (El y_aGBu) :* (NA_I (El y_aGBv) :* (NA_I (El y_aGBw) :* (NA_I (El y_aGBx) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBy) :* (NA_I (El y_aGBz) :* (NA_I (El y_aGBA) :* (NA_I (El y_aGBB) :* (NA_I (El y_aGBC) :* (NA_I (El y_aGBD) :* (NA_I (El y_aGBE) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBF) :* (NA_I (El y_aGBG) :* (NA_I (El y_aGBH) :* (NA_I (El y_aGBI) :* (NA_I (El y_aGBJ) :* (NA_I (El y_aGBK) :* (NA_I (El y_aGBL) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBM) :* (NA_I (El y_aGBN) :* (NA_I (El y_aGBO) :* (NA_I (El y_aGBP) :* (NA_I (El y_aGBQ) :* (NA_I (El y_aGBR) :* (NA_I (El y_aGBS) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBT) :* (NA_I (El y_aGBU) :* (NA_I (El y_aGBV) :* (NA_I (El y_aGBW) :* (NA_I (El y_aGBX) :* (NA_I (El y_aGBY) :* (NA_I (El y_aGBZ) :* NP0))))))))))))))))))))))) -> ()
SD3 -> \case
(Rep (H (NA_I (El y_aGC0) :* (NA_I (El y_aGC1) :* (NA_I (El y_aGC2) :* (NA_I (El y_aGC3) :* (NA_I (El y_aGC4) :* (NA_I (El y_aGC5) :* (NA_I (El y_aGC6) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGC7) :* (NA_I (El y_aGC8) :* (NA_I (El y_aGC9) :* (NA_I (El y_aGCa) :* (NA_I (El y_aGCb) :* (NA_I (El y_aGCc) :* (NA_I (El y_aGCd) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGCe) :* (NA_I (El y_aGCf) :* (NA_I (El y_aGCg) :* (NA_I (El y_aGCh) :* (NA_I (El y_aGCi) :* (NA_I (El y_aGCj) :* (NA_I (El y_aGCk) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGCl) :* (NA_I (El y_aGCm) :* (NA_I (El y_aGCn) :* (NA_I (El y_aGCo) :* (NA_I (El y_aGCp) :* (NA_I (El y_aGCq) :* (NA_I (El y_aGCr) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGCs) :* (NA_I (El y_aGCt) :* (NA_I (El y_aGCu) :* (NA_I (El y_aGCv) :* (NA_I (El y_aGCw) :* (NA_I (El y_aGCx) :* (NA_I (El y_aGCy) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGCz) :* (NA_I (El y_aGCA) :* (NA_I (El y_aGCB) :* (NA_I (El y_aGCC) :* (NA_I (El y_aGCD) :* (NA_I (El y_aGCE) :* (NA_I (El y_aGCF) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGCG) :* (NA_I (El y_aGCH) :* (NA_I (El y_aGCI) :* (NA_I (El y_aGCJ) :* (NA_I (El y_aGCK) :* (NA_I (El y_aGCL) :* (NA_I (El y_aGCM) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGCN) :* (NA_I (El y_aGCO) :* (NA_I (El y_aGCP) :* (NA_I (El y_aGCQ) :* (NA_I (El y_aGCR) :* (NA_I (El y_aGCS) :* (NA_I (El y_aGCT) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGCU) :* (NA_I (El y_aGCV) :* (NA_I (El y_aGCW) :* (NA_I (El y_aGCX) :* (NA_I (El y_aGCY) :* (NA_I (El y_aGCZ) :* (NA_I (El y_aGD0) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGD1) :* (NA_I (El y_aGD2) :* (NA_I (El y_aGD3) :* (NA_I (El y_aGD4) :* (NA_I (El y_aGD5) :* (NA_I (El y_aGD6) :* (NA_I (El y_aGD7) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGD8) :* (NA_I (El y_aGD9) :* (NA_I (El y_aGDa) :* (NA_I (El y_aGDb) :* (NA_I (El y_aGDc) :* (NA_I (El y_aGDd) :* (NA_I (El y_aGDe) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDf) :* (NA_I (El y_aGDg) :* (NA_I (El y_aGDh) :* (NA_I (El y_aGDi) :* (NA_I (El y_aGDj) :* (NA_I (El y_aGDk) :* (NA_I (El y_aGDl) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDm) :* (NA_I (El y_aGDn) :* (NA_I (El y_aGDo) :* (NA_I (El y_aGDp) :* (NA_I (El y_aGDq) :* (NA_I (El y_aGDr) :* (NA_I (El y_aGDs) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDt) :* (NA_I (El y_aGDu) :* (NA_I (El y_aGDv) :* (NA_I (El y_aGDw) :* (NA_I (El y_aGDx) :* (NA_I (El y_aGDy) :* (NA_I (El y_aGDz) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDA) :* (NA_I (El y_aGDB) :* (NA_I (El y_aGDC) :* (NA_I (El y_aGDD) :* (NA_I (El y_aGDE) :* (NA_I (El y_aGDF) :* (NA_I (El y_aGDG) :* NP0))))))))))))))))))))))) -> ()
SD4 -> \case
(Rep (H (NA_I (El y_aGDH) :* (NA_I (El y_aGDI) :* (NA_I (El y_aGDJ) :* (NA_I (El y_aGDK) :* (NA_I (El y_aGDL) :* (NA_I (El y_aGDM) :* (NA_I (El y_aGDN) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGDO) :* (NA_I (El y_aGDP) :* (NA_I (El y_aGDQ) :* (NA_I (El y_aGDR) :* (NA_I (El y_aGDS) :* (NA_I (El y_aGDT) :* (NA_I (El y_aGDU) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGDV) :* (NA_I (El y_aGDW) :* (NA_I (El y_aGDX) :* (NA_I (El y_aGDY) :* (NA_I (El y_aGDZ) :* (NA_I (El y_aGE0) :* (NA_I (El y_aGE1) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGE2) :* (NA_I (El y_aGE3) :* (NA_I (El y_aGE4) :* (NA_I (El y_aGE5) :* (NA_I (El y_aGE6) :* (NA_I (El y_aGE7) :* (NA_I (El y_aGE8) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGE9) :* (NA_I (El y_aGEa) :* (NA_I (El y_aGEb) :* (NA_I (El y_aGEc) :* (NA_I (El y_aGEd) :* (NA_I (El y_aGEe) :* (NA_I (El y_aGEf) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGEg) :* (NA_I (El y_aGEh) :* (NA_I (El y_aGEi) :* (NA_I (El y_aGEj) :* (NA_I (El y_aGEk) :* (NA_I (El y_aGEl) :* (NA_I (El y_aGEm) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGEv) :* (NA_I (El y_aGEw) :* (NA_I (El y_aGEx) :* (NA_I (El y_aGEy) :* (NA_I (El y_aGEz) :* (NA_I (El y_aGEA) :* (NA_I (El y_aGEB) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGEE) :* (NA_I (El y_aGEF) :* (NA_I (El y_aGEG) :* (NA_I (El y_aGEH) :* (NA_I (El y_aGEI) :* (NA_I (El y_aGEM) :* (NA_I (El y_aGEN) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGEO) :* (NA_I (El y_aGEP) :* (NA_I (El y_aGEQ) :* (NA_I (El y_aGER) :* (NA_I (El y_aGES) :* (NA_I (El y_aGET) :* (NA_I (El y_aGEU) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGEV) :* (NA_I (El y_aGEW) :* (NA_I (El y_aGEX) :* (NA_I (El y_aGEY) :* (NA_I (El y_aGEZ) :* (NA_I (El y_aGF0) :* (NA_I (El y_aGF1) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGF2) :* (NA_I (El y_aGF3) :* (NA_I (El y_aGF4) :* (NA_I (El y_aGF5) :* (NA_I (El y_aGF6) :* (NA_I (El y_aGF7) :* (NA_I (El y_aGF8) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGF9) :* (NA_I (El y_aGFa) :* (NA_I (El y_aGFb) :* (NA_I (El y_aGFc) :* (NA_I (El y_aGFd) :* (NA_I (El y_aGFe) :* (NA_I (El y_aGFf) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFg) :* (NA_I (El y_aGFh) :* (NA_I (El y_aGFi) :* (NA_I (El y_aGFj) :* (NA_I (El y_aGFk) :* (NA_I (El y_aGFl) :* (NA_I (El y_aGFm) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFn) :* (NA_I (El y_aGFo) :* (NA_I (El y_aGFp) :* (NA_I (El y_aGFq) :* (NA_I (El y_aGFr) :* (NA_I (El y_aGFs) :* (NA_I (El y_aGFt) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFC) :* (NA_I (El y_aGFD) :* (NA_I (El y_aGFE) :* (NA_I (El y_aGFF) :* (NA_I (El y_aGFG) :* (NA_I (El y_aGFH) :* (NA_I (El y_aGFI) :* NP0))))))))))))))))))))))) -> ()
SD5 -> \case
(Rep (H (NA_I (El y_aGFQ) :* (NA_I (El y_aGFR) :* (NA_I (El y_aGFS) :* (NA_I (El y_aGFT) :* (NA_I (El y_aGFU) :* (NA_I (El y_aGFW) :* (NA_I (El y_aGFX) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGG1) :* (NA_I (El y_aGG2) :* (NA_I (El y_aGG3) :* (NA_I (El y_aGG4) :* (NA_I (El y_aGG5) :* (NA_I (El y_aGG6) :* (NA_I (El y_aGG7) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGG8) :* (NA_I (El y_aGG9) :* (NA_I (El y_aGGa) :* (NA_I (El y_aGGb) :* (NA_I (El y_aGGc) :* (NA_I (El y_aGGd) :* (NA_I (El y_aGGe) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGGf) :* (NA_I (El y_aGGg) :* (NA_I (El y_aGGh) :* (NA_I (El y_aGGi) :* (NA_I (El y_aGGj) :* (NA_I (El y_aGGk) :* (NA_I (El y_aGGl) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGGm) :* (NA_I (El y_aGGn) :* (NA_I (El y_aGGo) :* (NA_I (El y_aGGp) :* (NA_I (El y_aGGq) :* (NA_I (El y_aGGr) :* (NA_I (El y_aGGs) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGGt) :* (NA_I (El y_aGGu) :* (NA_I (El y_aGGv) :* (NA_I (El y_aGGw) :* (NA_I (El y_aGGx) :* (NA_I (El y_aGGy) :* (NA_I (El y_aGGz) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGGA) :* (NA_I (El y_aGGB) :* (NA_I (El y_aGGC) :* (NA_I (El y_aGGD) :* (NA_I (El y_aGGE) :* (NA_I (El y_aGGF) :* (NA_I (El y_aGGG) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGGH) :* (NA_I (El y_aGGI) :* (NA_I (El y_aGGJ) :* (NA_I (El y_aGGK) :* (NA_I (El y_aGGL) :* (NA_I (El y_aGGQ) :* (NA_I (El y_aGGV) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGGZ) :* (NA_I (El y_aGH0) :* (NA_I (El y_aGH1) :* (NA_I (El y_aGH2) :* (NA_I (El y_aGH3) :* (NA_I (El y_aGH4) :* (NA_I (El y_aGH5) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHf) :* (NA_I (El y_aGHg) :* (NA_I (El y_aGHh) :* (NA_I (El y_aGHi) :* (NA_I (El y_aGHj) :* (NA_I (El y_aGHk) :* (NA_I (El y_aGHl) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHq) :* (NA_I (El y_aGHr) :* (NA_I (El y_aGHs) :* (NA_I (El y_aGHt) :* (NA_I (El y_aGHu) :* (NA_I (El y_aGHv) :* (NA_I (El y_aGHw) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHx) :* (NA_I (El y_aGHy) :* (NA_I (El y_aGHz) :* (NA_I (El y_aGHA) :* (NA_I (El y_aGHB) :* (NA_I (El y_aGHC) :* (NA_I (El y_aGHD) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHE) :* (NA_I (El y_aGHF) :* (NA_I (El y_aGHG) :* (NA_I (El y_aGHH) :* (NA_I (El y_aGHI) :* (NA_I (El y_aGHJ) :* (NA_I (El y_aGHK) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHL) :* (NA_I (El y_aGHM) :* (NA_I (El y_aGHN) :* (NA_I (El y_aGHO) :* (NA_I (El y_aGHP) :* (NA_I (El y_aGHQ) :* (NA_I (El y_aGHR) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHS) :* (NA_I (El y_aGHT) :* (NA_I (El y_aGHU) :* (NA_I (El y_aGHV) :* (NA_I (El y_aGHW) :* (NA_I (El y_aGHX) :* (NA_I (El y_aGHY) :* NP0))))))))))))))))))))))) -> ()
SD6 -> \case
(Rep (H (NA_I (El y_aGHZ) :* (NA_I (El y_aGI0) :* (NA_I (El y_aGI1) :* (NA_I (El y_aGI2) :* (NA_I (El y_aGI3) :* (NA_I (El y_aGI4) :* (NA_I (El y_aGI5) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGId) :* (NA_I (El y_aGIe) :* (NA_I (El y_aGIf) :* (NA_I (El y_aGIg) :* (NA_I (El y_aGIh) :* (NA_I (El y_aGIi) :* (NA_I (El y_aGIj) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGIk) :* (NA_I (El y_aGIl) :* (NA_I (El y_aGIm) :* (NA_I (El y_aGIn) :* (NA_I (El y_aGIo) :* (NA_I (El y_aGIp) :* (NA_I (El y_aGIr) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGIt) :* (NA_I (El y_aGIu) :* (NA_I (El y_aGIv) :* (NA_I (El y_aGIw) :* (NA_I (El y_aGIx) :* (NA_I (El y_aGIy) :* (NA_I (El y_aGIz) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGIA) :* (NA_I (El y_aGIB) :* (NA_I (El y_aGIC) :* (NA_I (El y_aGID) :* (NA_I (El y_aGIE) :* (NA_I (El y_aGIF) :* (NA_I (El y_aGIG) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGIH) :* (NA_I (El y_aGII) :* (NA_I (El y_aGIJ) :* (NA_I (El y_aGIK) :* (NA_I (El y_aGIL) :* (NA_I (El y_aGIM) :* (NA_I (El y_aGIN) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGIO) :* (NA_I (El y_aGIP) :* (NA_I (El y_aGIQ) :* (NA_I (El y_aGIR) :* (NA_I (El y_aGIS) :* (NA_I (El y_aGIT) :* (NA_I (El y_aGIU) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGIV) :* (NA_I (El y_aGIW) :* (NA_I (El y_aGIX) :* (NA_I (El y_aGIY) :* (NA_I (El y_aGIZ) :* (NA_I (El y_aGJ0) :* (NA_I (El y_aGJ1) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJc) :* (NA_I (El y_aGJm) :* (NA_I (El y_aGJo) :* (NA_I (El y_aGJp) :* (NA_I (El y_aGJq) :* (NA_I (El y_aGJr) :* (NA_I (El y_aGJs) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJt) :* (NA_I (El y_aGJv) :* (NA_I (El y_aGJw) :* (NA_I (El y_aGJy) :* (NA_I (El y_aGJz) :* (NA_I (El y_aGJD) :* (NA_I (El y_aGJE) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJF) :* (NA_I (El y_aGJG) :* (NA_I (El y_aGJH) :* (NA_I (El y_aGJI) :* (NA_I (El y_aGJJ) :* (NA_I (El y_aGJK) :* (NA_I (El y_aGJL) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJM) :* (NA_I (El y_aGJN) :* (NA_I (El y_aGJO) :* (NA_I (El y_aGJP) :* (NA_I (El y_aGJQ) :* (NA_I (El y_aGJR) :* (NA_I (El y_aGJS) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJT) :* (NA_I (El y_aGJU) :* (NA_I (El y_aGJV) :* (NA_I (El y_aGJW) :* (NA_I (El y_aGJY) :* (NA_I (El y_aGJZ) :* (NA_I (El y_aGK0) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGK3) :* (NA_I (El y_aGK4) :* (NA_I (El y_aGK5) :* (NA_I (El y_aGK6) :* (NA_I (El y_aGK7) :* (NA_I (El y_aGK8) :* (NA_I (El y_aGK9) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGKc) :* (NA_I (El y_aGKd) :* (NA_I (El y_aGKe) :* (NA_I (El y_aGKf) :* (NA_I (El y_aGKg) :* (NA_I (El y_aGKh) :* (NA_I (El y_aGKi) :* NP0))))))))))))))))))))))) -> ()
SD7 -> \case
(Rep (H (NA_I (El y_aGHZ) :* (NA_I (El y_aGI0) :* (NA_I (El y_aGI1) :* (NA_I (El y_aGI2) :* (NA_I (El y_aGI3) :* (NA_I (El y_aGI4) :* (NA_I (El y_aGI5) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGId) :* (NA_I (El y_aGIe) :* (NA_I (El y_aGIf) :* (NA_I (El y_aGIg) :* (NA_I (El y_aGIh) :* (NA_I (El y_aGIi) :* (NA_I (El y_aGIj) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGIk) :* (NA_I (El y_aGIl) :* (NA_I (El y_aGIm) :* (NA_I (El y_aGIn) :* (NA_I (El y_aGIo) :* (NA_I (El y_aGIp) :* (NA_I (El y_aGIr) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGIt) :* (NA_I (El y_aGIu) :* (NA_I (El y_aGIv) :* (NA_I (El y_aGIw) :* (NA_I (El y_aGIx) :* (NA_I (El y_aGIy) :* (NA_I (El y_aGIz) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGIA) :* (NA_I (El y_aGIB) :* (NA_I (El y_aGIC) :* (NA_I (El y_aGID) :* (NA_I (El y_aGIE) :* (NA_I (El y_aGIF) :* (NA_I (El y_aGIG) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGIH) :* (NA_I (El y_aGII) :* (NA_I (El y_aGIJ) :* (NA_I (El y_aGIK) :* (NA_I (El y_aGIL) :* (NA_I (El y_aGIM) :* (NA_I (El y_aGIN) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGIO) :* (NA_I (El y_aGIP) :* (NA_I (El y_aGIQ) :* (NA_I (El y_aGIR) :* (NA_I (El y_aGIS) :* (NA_I (El y_aGIT) :* (NA_I (El y_aGIU) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGIV) :* (NA_I (El y_aGIW) :* (NA_I (El y_aGIX) :* (NA_I (El y_aGIY) :* (NA_I (El y_aGIZ) :* (NA_I (El y_aGJ0) :* (NA_I (El y_aGJ1) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJc) :* (NA_I (El y_aGJm) :* (NA_I (El y_aGJo) :* (NA_I (El y_aGJp) :* (NA_I (El y_aGJq) :* (NA_I (El y_aGJr) :* (NA_I (El y_aGJs) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJt) :* (NA_I (El y_aGJv) :* (NA_I (El y_aGJw) :* (NA_I (El y_aGJy) :* (NA_I (El y_aGJz) :* (NA_I (El y_aGJD) :* (NA_I (El y_aGJE) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJF) :* (NA_I (El y_aGJG) :* (NA_I (El y_aGJH) :* (NA_I (El y_aGJI) :* (NA_I (El y_aGJJ) :* (NA_I (El y_aGJK) :* (NA_I (El y_aGJL) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJM) :* (NA_I (El y_aGJN) :* (NA_I (El y_aGJO) :* (NA_I (El y_aGJP) :* (NA_I (El y_aGJQ) :* (NA_I (El y_aGJR) :* (NA_I (El y_aGJS) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJT) :* (NA_I (El y_aGJU) :* (NA_I (El y_aGJV) :* (NA_I (El y_aGJW) :* (NA_I (El y_aGJY) :* (NA_I (El y_aGJZ) :* (NA_I (El y_aGK0) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGK3) :* (NA_I (El y_aGK4) :* (NA_I (El y_aGK5) :* (NA_I (El y_aGK6) :* (NA_I (El y_aGK7) :* (NA_I (El y_aGK8) :* (NA_I (El y_aGK9) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGKc) :* (NA_I (El y_aGKd) :* (NA_I (El y_aGKe) :* (NA_I (El y_aGKf) :* (NA_I (El y_aGKg) :* (NA_I (El y_aGKh) :* (NA_I (El y_aGKi) :* NP0))))))))))))))))))))))) -> ()
SD8 -> \case
(Rep (H (NA_I (El y_aGHZ) :* (NA_I (El y_aGI0) :* (NA_I (El y_aGI1) :* (NA_I (El y_aGI2) :* (NA_I (El y_aGI3) :* (NA_I (El y_aGI4) :* (NA_I (El y_aGI5) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGId) :* (NA_I (El y_aGIe) :* (NA_I (El y_aGIf) :* (NA_I (El y_aGIg) :* (NA_I (El y_aGIh) :* (NA_I (El y_aGIi) :* (NA_I (El y_aGIj) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGIk) :* (NA_I (El y_aGIl) :* (NA_I (El y_aGIm) :* (NA_I (El y_aGIn) :* (NA_I (El y_aGIo) :* (NA_I (El y_aGIp) :* (NA_I (El y_aGIr) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGIt) :* (NA_I (El y_aGIu) :* (NA_I (El y_aGIv) :* (NA_I (El y_aGIw) :* (NA_I (El y_aGIx) :* (NA_I (El y_aGIy) :* (NA_I (El y_aGIz) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGIA) :* (NA_I (El y_aGIB) :* (NA_I (El y_aGIC) :* (NA_I (El y_aGID) :* (NA_I (El y_aGIE) :* (NA_I (El y_aGIF) :* (NA_I (El y_aGIG) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGIH) :* (NA_I (El y_aGII) :* (NA_I (El y_aGIJ) :* (NA_I (El y_aGIK) :* (NA_I (El y_aGIL) :* (NA_I (El y_aGIM) :* (NA_I (El y_aGIN) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGIO) :* (NA_I (El y_aGIP) :* (NA_I (El y_aGIQ) :* (NA_I (El y_aGIR) :* (NA_I (El y_aGIS) :* (NA_I (El y_aGIT) :* (NA_I (El y_aGIU) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGIV) :* (NA_I (El y_aGIW) :* (NA_I (El y_aGIX) :* (NA_I (El y_aGIY) :* (NA_I (El y_aGIZ) :* (NA_I (El y_aGJ0) :* (NA_I (El y_aGJ1) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJc) :* (NA_I (El y_aGJm) :* (NA_I (El y_aGJo) :* (NA_I (El y_aGJp) :* (NA_I (El y_aGJq) :* (NA_I (El y_aGJr) :* (NA_I (El y_aGJs) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJt) :* (NA_I (El y_aGJv) :* (NA_I (El y_aGJw) :* (NA_I (El y_aGJy) :* (NA_I (El y_aGJz) :* (NA_I (El y_aGJD) :* (NA_I (El y_aGJE) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJF) :* (NA_I (El y_aGJG) :* (NA_I (El y_aGJH) :* (NA_I (El y_aGJI) :* (NA_I (El y_aGJJ) :* (NA_I (El y_aGJK) :* (NA_I (El y_aGJL) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJM) :* (NA_I (El y_aGJN) :* (NA_I (El y_aGJO) :* (NA_I (El y_aGJP) :* (NA_I (El y_aGJQ) :* (NA_I (El y_aGJR) :* (NA_I (El y_aGJS) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJT) :* (NA_I (El y_aGJU) :* (NA_I (El y_aGJV) :* (NA_I (El y_aGJW) :* (NA_I (El y_aGJY) :* (NA_I (El y_aGJZ) :* (NA_I (El y_aGK0) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGK3) :* (NA_I (El y_aGK4) :* (NA_I (El y_aGK5) :* (NA_I (El y_aGK6) :* (NA_I (El y_aGK7) :* (NA_I (El y_aGK8) :* (NA_I (El y_aGK9) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGKc) :* (NA_I (El y_aGKd) :* (NA_I (El y_aGKe) :* (NA_I (El y_aGKf) :* (NA_I (El y_aGKg) :* (NA_I (El y_aGKh) :* (NA_I (El y_aGKi) :* NP0))))))))))))))))))))))) -> ()
SD9 -> \case
(Rep (H (NA_I (El y_aGHZ) :* (NA_I (El y_aGI0) :* (NA_I (El y_aGI1) :* (NA_I (El y_aGI2) :* (NA_I (El y_aGI3) :* (NA_I (El y_aGI4) :* (NA_I (El y_aGI5) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGId) :* (NA_I (El y_aGIe) :* (NA_I (El y_aGIf) :* (NA_I (El y_aGIg) :* (NA_I (El y_aGIh) :* (NA_I (El y_aGIi) :* (NA_I (El y_aGIj) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGIk) :* (NA_I (El y_aGIl) :* (NA_I (El y_aGIm) :* (NA_I (El y_aGIn) :* (NA_I (El y_aGIo) :* (NA_I (El y_aGIp) :* (NA_I (El y_aGIr) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGIt) :* (NA_I (El y_aGIu) :* (NA_I (El y_aGIv) :* (NA_I (El y_aGIw) :* (NA_I (El y_aGIx) :* (NA_I (El y_aGIy) :* (NA_I (El y_aGIz) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGIA) :* (NA_I (El y_aGIB) :* (NA_I (El y_aGIC) :* (NA_I (El y_aGID) :* (NA_I (El y_aGIE) :* (NA_I (El y_aGIF) :* (NA_I (El y_aGIG) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGIH) :* (NA_I (El y_aGII) :* (NA_I (El y_aGIJ) :* (NA_I (El y_aGIK) :* (NA_I (El y_aGIL) :* (NA_I (El y_aGIM) :* (NA_I (El y_aGIN) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGIO) :* (NA_I (El y_aGIP) :* (NA_I (El y_aGIQ) :* (NA_I (El y_aGIR) :* (NA_I (El y_aGIS) :* (NA_I (El y_aGIT) :* (NA_I (El y_aGIU) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGIV) :* (NA_I (El y_aGIW) :* (NA_I (El y_aGIX) :* (NA_I (El y_aGIY) :* (NA_I (El y_aGIZ) :* (NA_I (El y_aGJ0) :* (NA_I (El y_aGJ1) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJc) :* (NA_I (El y_aGJm) :* (NA_I (El y_aGJo) :* (NA_I (El y_aGJp) :* (NA_I (El y_aGJq) :* (NA_I (El y_aGJr) :* (NA_I (El y_aGJs) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJt) :* (NA_I (El y_aGJv) :* (NA_I (El y_aGJw) :* (NA_I (El y_aGJy) :* (NA_I (El y_aGJz) :* (NA_I (El y_aGJD) :* (NA_I (El y_aGJE) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJF) :* (NA_I (El y_aGJG) :* (NA_I (El y_aGJH) :* (NA_I (El y_aGJI) :* (NA_I (El y_aGJJ) :* (NA_I (El y_aGJK) :* (NA_I (El y_aGJL) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJM) :* (NA_I (El y_aGJN) :* (NA_I (El y_aGJO) :* (NA_I (El y_aGJP) :* (NA_I (El y_aGJQ) :* (NA_I (El y_aGJR) :* (NA_I (El y_aGJS) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJT) :* (NA_I (El y_aGJU) :* (NA_I (El y_aGJV) :* (NA_I (El y_aGJW) :* (NA_I (El y_aGJY) :* (NA_I (El y_aGJZ) :* (NA_I (El y_aGK0) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGK3) :* (NA_I (El y_aGK4) :* (NA_I (El y_aGK5) :* (NA_I (El y_aGK6) :* (NA_I (El y_aGK7) :* (NA_I (El y_aGK8) :* (NA_I (El y_aGK9) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGKc) :* (NA_I (El y_aGKd) :* (NA_I (El y_aGKe) :* (NA_I (El y_aGKf) :* (NA_I (El y_aGKg) :* (NA_I (El y_aGKh) :* (NA_I (El y_aGKi) :* NP0))))))))))))))))))))))) -> ()
from generics-mrsop.
arianvp
commented on August 22, 2024
Another thing we could do is
instead of using [Digit] as a representation. Generate the Digit datatype with TH and dynamically and give it as many constructors as data constructors. adjust the Lkup type family with TH as well, and pass the Lkup type family as a paramter to the Family typeclass
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
That's great news! Great work @arianvp !!
We should talk on Thursday to evaluate the best solution here. Although we never really use Digit when programming, we need its declaration. Hence, generating with TH doesn't seem like a good idea.
Your sto function should instead have type: sto :: SNumber (ix :: '[ 'Digit]) -> ... though.
Otherwise, how do we handle more than 10 types?
I assume that writing the Idx type family now will be far from trivial, and will make us
lose our into function. Need to think a bit.
Thoughts?
from generics-mrsop.
arianvp
commented on August 22, 2024
Yes I agree it needs to be NP SDigit ix. To get that to work we use the Lkup' type family (which works for a list of digits) instead of the Lkup'' type family. I'm working on that change now
from generics-mrsop.
arianvp
commented on August 22, 2024
False alarm :( Bug.hs with just sto just doesn't use a lot of memory.. Also with Base-1 nats...
from generics-mrsop.
arianvp
commented on August 22, 2024
Interestingly, adding both sfrom' and sto' to the mix still doesn't trigger the bug for Bug.hs. This compiles just fine. I am very confused now :)
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
import GHC.TypeLits (TypeError, ErrorMessage (..))
import Data.Proxy
data Atom kon
= K kon
| I Nat
deriving (Eq, Show)
data Nat = S Nat | Z
deriving (Eq , Show)
data SNat :: Nat -> * where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
type family Lkup (n :: Nat) (ks :: [k]) :: k where
Lkup Z (k : ks) = k
Lkup (S n) (k : ks) = Lkup n ks
Lkup _ '[] = TypeError (Text "Lkup index too big")
data El :: [*] -> Nat -> * where
El :: {unEl :: Lkup ix fam} -> El fam ix
data NS :: (k -> *) -> [k] -> * where
T :: NS p xs -> NS p (x : xs)
H :: p x -> NS p (x : xs)
infixr 5 :*
data NP :: (k -> *) -> [k] -> * where
NP0 :: NP p '[]
(:*) :: p x -> NP p xs -> NP p (x : xs)
data NA :: (kon -> *) -> (nat -> *) -> Atom kon -> * where
NA_I :: phi k -> NA ki phi (I k)
NA_K :: ki k -> NA ki phi (K k)
data Kon
= KInt
| KInteger
| KBool
| KFloat
| KChar
| KString
deriving (Eq , Show)
newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])
= Rep { unRep :: NS (PoA ki phi) code }
type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]])
| fam -> ki codes , ki codes -> fam
where
sto' :: SNat ix -> Rep ki (El fam) (Lkup ix codes) -> ()
sfrom' :: SNat ix -> El fam ix -> ()
data A = A1 A B C D E F G | A2 A B C D E F G | A3 A B C D E F G | A4 A B C D E F G | A5 A B C D E F G | A6 A B C D E F G | A7 A B C D E F G | A8 A B C D E F G | A9 A B C D E F G | AA A B C D E F G | AB A B C D E F G | AC A B C D E F G | AD A B C D E F G | AE A B C D E F G | AF A B C D E F G
data B = B1 A B C D E F G | B2 A B C D E F G | B3 A B C D E F G | B4 A B C D E F G | B5 A B C D E F G | B6 A B C D E F G | B7 A B C D E F G | B8 A B C D E F G | B9 A B C D E F G | BA A B C D E F G | BB A B C D E F G | BC A B C D E F G | BD A B C D E F G | BE A B C D E F G | BF A B C D E F G
data C = C1 A B C D E F G | C2 A B C D E F G | C3 A B C D E F G | C4 A B C D E F G | C5 A B C D E F G | C6 A B C D E F G | C7 A B C D E F G | C8 A B C D E F G | C9 A B C D E F G | CA A B C D E F G | CB A B C D E F G | CC A B C D E F G | CD A B C D E F G | CE A B C D E F G | CF A B C D E F G
data D = D1 A B C D E F G | D2 A B C D E F G | D3 A B C D E F G | D4 A B C D E F G | D5 A B C D E F G | D6 A B C D E F G | D7 A B C D E F G | D8 A B C D E F G | D9 A B C D E F G | DA A B C D E F G | DB A B C D E F G | DC A B C D E F G | DD A B C D E F G | DE A B C D E F G | DF A B C D E F G
data E = E1 A B C D E F G | E2 A B C D E F G | E3 A B C D E F G | E4 A B C D E F G | E5 A B C D E F G | E6 A B C D E F G | E7 A B C D E F G | E8 A B C D E F G | E9 A B C D E F G | EA A B C D E F G | EB A B C D E F G | EC A B C D E F G | ED A B C D E F G | EE A B C D E F G | EF A B C D E F G
data F = F1 A B C D E F G | F2 A B C D E F G | F3 A B C D E F G | F4 A B C D E F G | F5 A B C D E F G | F6 A B C D E F G | F7 A B C D E F G | F8 A B C D E F G | F9 A B C D E F G | FA A B C D E F G | FB A B C D E F G | FC A B C D E F G | FD A B C D E F G | FE A B C D E F G | FF A B C D E F G
data G = G1 A B C D E F G | G2 A B C D E F G | G3 A B C D E F G | G4 A B C D E F G | G5 A B C D E F G | G6 A B C D E F G | G7 A B C D E F G | G8 A B C D E F G | G9 A B C D E F G | GA A B C D E F G | GB A B C D E F G | GC A B C D E F G | GD A B C D E F G | GE A B C D E F G | GF A B C D E F G
type A' = S Z
type B' = S (S Z)
type C' = S (S (S Z))
type D' = S (S (S (S Z)))
type E' = S (S (S (S (S Z))))
type F' = S (S (S (S (S (S Z)))))
type G' = S (S (S (S (S (S (S Z))))))
pattern SA' = SZ
pattern SB' = (SS SZ)
pattern SC' = (SS (SS SZ))
pattern SD' = (SS (SS (SS SZ)))
pattern SE' = (SS (SS (SS (SS SZ))))
pattern SF' = (SS (SS (SS (SS (SS SZ)))))
pattern SG' = (SS (SS (SS (SS (SS (SS SZ))))))
data Singl (kon :: Kon) :: * where
type FamA = '[A, B, C, D, E, F ,G]
type Prod = '[I A', I B', I C' , I D' , I E' , I F' , I G']
type Sum = '[Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod]
type CodesA = [Sum, Sum, Sum, Sum, Sum, Sum, Sum]
instance Family Singl FamA CodesA where
sto' = \case
SA' -> \case
(Rep (H (NA_I (El y_aGws) :* (NA_I (El y_aGwt) :* (NA_I (El y_aGwu) :* (NA_I (El y_aGwv) :* (NA_I (El y_aGww) :* (NA_I (El y_aGwx) :* (NA_I (El y_aGwy) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGwH) :* (NA_I (El y_aGwI) :* (NA_I (El y_aGwK) :* (NA_I (El y_aGwL) :* (NA_I (El y_aGwM) :* (NA_I (El y_aGwN) :* (NA_I (El y_aGwO) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGwZ) :* (NA_I (El y_aGx0) :* (NA_I (El y_aGx1) :* (NA_I (El y_aGx2) :* (NA_I (El y_aGx3) :* (NA_I (El y_aGx4) :* (NA_I (El y_aGx5) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGx6) :* (NA_I (El y_aGx7) :* (NA_I (El y_aGx8) :* (NA_I (El y_aGx9) :* (NA_I (El y_aGxa) :* (NA_I (El y_aGxb) :* (NA_I (El y_aGxc) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGxd) :* (NA_I (El y_aGxe) :* (NA_I (El y_aGxg) :* (NA_I (El y_aGxh) :* (NA_I (El y_aGxi) :* (NA_I (El y_aGxj) :* (NA_I (El y_aGxk) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGxl) :* (NA_I (El y_aGxm) :* (NA_I (El y_aGxn) :* (NA_I (El y_aGxo) :* (NA_I (El y_aGxp) :* (NA_I (El y_aGxq) :* (NA_I (El y_aGxr) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGxs) :* (NA_I (El y_aGxt) :* (NA_I (El y_aGxu) :* (NA_I (El y_aGxv) :* (NA_I (El y_aGxw) :* (NA_I (El y_aGxx) :* (NA_I (El y_aGxy) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGxz) :* (NA_I (El y_aGxA) :* (NA_I (El y_aGxB) :* (NA_I (El y_aGxC) :* (NA_I (El y_aGxD) :* (NA_I (El y_aGxE) :* (NA_I (El y_aGxF) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxG) :* (NA_I (El y_aGxH) :* (NA_I (El y_aGxI) :* (NA_I (El y_aGxJ) :* (NA_I (El y_aGxK) :* (NA_I (El y_aGxL) :* (NA_I (El y_aGxM) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxN) :* (NA_I (El y_aGxO) :* (NA_I (El y_aGxP) :* (NA_I (El y_aGxQ) :* (NA_I (El y_aGxR) :* (NA_I (El y_aGxS) :* (NA_I (El y_aGxT) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxU) :* (NA_I (El y_aGxV) :* (NA_I (El y_aGxW) :* (NA_I (El y_aGxX) :* (NA_I (El y_aGxY) :* (NA_I (El y_aGxZ) :* (NA_I (El y_aGy0) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGy1) :* (NA_I (El y_aGy2) :* (NA_I (El y_aGy3) :* (NA_I (El y_aGy4) :* (NA_I (El y_aGy5) :* (NA_I (El y_aGy6) :* (NA_I (El y_aGy7) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGy8) :* (NA_I (El y_aGy9) :* (NA_I (El y_aGya) :* (NA_I (El y_aGyb) :* (NA_I (El y_aGyc) :* (NA_I (El y_aGyd) :* (NA_I (El y_aGye) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGyf) :* (NA_I (El y_aGyg) :* (NA_I (El y_aGyh) :* (NA_I (El y_aGyi) :* (NA_I (El y_aGyj) :* (NA_I (El y_aGyk) :* (NA_I (El y_aGyl) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGym) :* (NA_I (El y_aGyn) :* (NA_I (El y_aGyo) :* (NA_I (El y_aGyp) :* (NA_I (El y_aGyq) :* (NA_I (El y_aGyr) :* (NA_I (El y_aGys) :* NP0))))))))))))))))))))))) -> ()
SB' -> \case
(Rep (H (NA_I (El y_aGyt) :* (NA_I (El y_aGyu) :* (NA_I (El y_aGyv) :* (NA_I (El y_aGyw) :* (NA_I (El y_aGyx) :* (NA_I (El y_aGyy) :* (NA_I (El y_aGyz) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGyA) :* (NA_I (El y_aGyB) :* (NA_I (El y_aGyC) :* (NA_I (El y_aGyD) :* (NA_I (El y_aGyE) :* (NA_I (El y_aGyF) :* (NA_I (El y_aGyG) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGyH) :* (NA_I (El y_aGyI) :* (NA_I (El y_aGyJ) :* (NA_I (El y_aGyK) :* (NA_I (El y_aGyL) :* (NA_I (El y_aGyM) :* (NA_I (El y_aGyN) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGyO) :* (NA_I (El y_aGyP) :* (NA_I (El y_aGyQ) :* (NA_I (El y_aGyR) :* (NA_I (El y_aGyS) :* (NA_I (El y_aGyT) :* (NA_I (El y_aGyU) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGyV) :* (NA_I (El y_aGyW) :* (NA_I (El y_aGyX) :* (NA_I (El y_aGyY) :* (NA_I (El y_aGyZ) :* (NA_I (El y_aGz0) :* (NA_I (El y_aGz1) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGz3) :* (NA_I (El y_aGz4) :* (NA_I (El y_aGz5) :* (NA_I (El y_aGz6) :* (NA_I (El y_aGz7) :* (NA_I (El y_aGz8) :* (NA_I (El y_aGz9) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGza) :* (NA_I (El y_aGzb) :* (NA_I (El y_aGzc) :* (NA_I (El y_aGzd) :* (NA_I (El y_aGze) :* (NA_I (El y_aGzg) :* (NA_I (El y_aGzh) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGzi) :* (NA_I (El y_aGzj) :* (NA_I (El y_aGzk) :* (NA_I (El y_aGzl) :* (NA_I (El y_aGzm) :* (NA_I (El y_aGzn) :* (NA_I (El y_aGzo) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzp) :* (NA_I (El y_aGzq) :* (NA_I (El y_aGzs) :* (NA_I (El y_aGzt) :* (NA_I (El y_aGzu) :* (NA_I (El y_aGzv) :* (NA_I (El y_aGzw) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzz) :* (NA_I (El y_aGzA) :* (NA_I (El y_aGzB) :* (NA_I (El y_aGzC) :* (NA_I (El y_aGzD) :* (NA_I (El y_aGzE) :* (NA_I (El y_aGzF) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzH) :* (NA_I (El y_aGzI) :* (NA_I (El y_aGzJ) :* (NA_I (El y_aGzM) :* (NA_I (El y_aGzN) :* (NA_I (El y_aGzO) :* (NA_I (El y_aGzP) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzQ) :* (NA_I (El y_aGzR) :* (NA_I (El y_aGzS) :* (NA_I (El y_aGzT) :* (NA_I (El y_aGzU) :* (NA_I (El y_aGzV) :* (NA_I (El y_aGzW) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzX) :* (NA_I (El y_aGzY) :* (NA_I (El y_aGzZ) :* (NA_I (El y_aGA0) :* (NA_I (El y_aGA1) :* (NA_I (El y_aGA2) :* (NA_I (El y_aGA3) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGA5) :* (NA_I (El y_aGA6) :* (NA_I (El y_aGA7) :* (NA_I (El y_aGA8) :* (NA_I (El y_aGA9) :* (NA_I (El y_aGAa) :* (NA_I (El y_aGAb) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGAc) :* (NA_I (El y_aGAd) :* (NA_I (El y_aGAe) :* (NA_I (El y_aGAf) :* (NA_I (El y_aGAg) :* (NA_I (El y_aGAh) :* (NA_I (El y_aGAi) :* NP0))))))))))))))))))))))) -> ()
SC' -> \case
(Rep (H (NA_I (El y_aGAj) :* (NA_I (El y_aGAk) :* (NA_I (El y_aGAl) :* (NA_I (El y_aGAm) :* (NA_I (El y_aGAn) :* (NA_I (El y_aGAo) :* (NA_I (El y_aGAp) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGAq) :* (NA_I (El y_aGAr) :* (NA_I (El y_aGAs) :* (NA_I (El y_aGAt) :* (NA_I (El y_aGAu) :* (NA_I (El y_aGAv) :* (NA_I (El y_aGAw) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGAx) :* (NA_I (El y_aGAy) :* (NA_I (El y_aGAz) :* (NA_I (El y_aGAA) :* (NA_I (El y_aGAB) :* (NA_I (El y_aGAC) :* (NA_I (El y_aGAD) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGAE) :* (NA_I (El y_aGAF) :* (NA_I (El y_aGAG) :* (NA_I (El y_aGAH) :* (NA_I (El y_aGAI) :* (NA_I (El y_aGAJ) :* (NA_I (El y_aGAK) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGAL) :* (NA_I (El y_aGAM) :* (NA_I (El y_aGAN) :* (NA_I (El y_aGAO) :* (NA_I (El y_aGAP) :* (NA_I (El y_aGAQ) :* (NA_I (El y_aGAR) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGAS) :* (NA_I (El y_aGAT) :* (NA_I (El y_aGAU) :* (NA_I (El y_aGAV) :* (NA_I (El y_aGAW) :* (NA_I (El y_aGAX) :* (NA_I (El y_aGAY) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGAZ) :* (NA_I (El y_aGB0) :* (NA_I (El y_aGB1) :* (NA_I (El y_aGB2) :* (NA_I (El y_aGB3) :* (NA_I (El y_aGB4) :* (NA_I (El y_aGB5) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGB6) :* (NA_I (El y_aGB7) :* (NA_I (El y_aGB8) :* (NA_I (El y_aGB9) :* (NA_I (El y_aGBa) :* (NA_I (El y_aGBb) :* (NA_I (El y_aGBc) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBd) :* (NA_I (El y_aGBe) :* (NA_I (El y_aGBf) :* (NA_I (El y_aGBg) :* (NA_I (El y_aGBh) :* (NA_I (El y_aGBi) :* (NA_I (El y_aGBj) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBk) :* (NA_I (El y_aGBl) :* (NA_I (El y_aGBm) :* (NA_I (El y_aGBn) :* (NA_I (El y_aGBo) :* (NA_I (El y_aGBp) :* (NA_I (El y_aGBq) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBr) :* (NA_I (El y_aGBs) :* (NA_I (El y_aGBt) :* (NA_I (El y_aGBu) :* (NA_I (El y_aGBv) :* (NA_I (El y_aGBw) :* (NA_I (El y_aGBx) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBy) :* (NA_I (El y_aGBz) :* (NA_I (El y_aGBA) :* (NA_I (El y_aGBB) :* (NA_I (El y_aGBC) :* (NA_I (El y_aGBD) :* (NA_I (El y_aGBE) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBF) :* (NA_I (El y_aGBG) :* (NA_I (El y_aGBH) :* (NA_I (El y_aGBI) :* (NA_I (El y_aGBJ) :* (NA_I (El y_aGBK) :* (NA_I (El y_aGBL) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBM) :* (NA_I (El y_aGBN) :* (NA_I (El y_aGBO) :* (NA_I (El y_aGBP) :* (NA_I (El y_aGBQ) :* (NA_I (El y_aGBR) :* (NA_I (El y_aGBS) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBT) :* (NA_I (El y_aGBU) :* (NA_I (El y_aGBV) :* (NA_I (El y_aGBW) :* (NA_I (El y_aGBX) :* (NA_I (El y_aGBY) :* (NA_I (El y_aGBZ) :* NP0))))))))))))))))))))))) -> ()
SD' -> \case
(Rep (H (NA_I (El y_aGC0) :* (NA_I (El y_aGC1) :* (NA_I (El y_aGC2) :* (NA_I (El y_aGC3) :* (NA_I (El y_aGC4) :* (NA_I (El y_aGC5) :* (NA_I (El y_aGC6) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGC7) :* (NA_I (El y_aGC8) :* (NA_I (El y_aGC9) :* (NA_I (El y_aGCa) :* (NA_I (El y_aGCb) :* (NA_I (El y_aGCc) :* (NA_I (El y_aGCd) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGCe) :* (NA_I (El y_aGCf) :* (NA_I (El y_aGCg) :* (NA_I (El y_aGCh) :* (NA_I (El y_aGCi) :* (NA_I (El y_aGCj) :* (NA_I (El y_aGCk) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGCl) :* (NA_I (El y_aGCm) :* (NA_I (El y_aGCn) :* (NA_I (El y_aGCo) :* (NA_I (El y_aGCp) :* (NA_I (El y_aGCq) :* (NA_I (El y_aGCr) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGCs) :* (NA_I (El y_aGCt) :* (NA_I (El y_aGCu) :* (NA_I (El y_aGCv) :* (NA_I (El y_aGCw) :* (NA_I (El y_aGCx) :* (NA_I (El y_aGCy) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGCz) :* (NA_I (El y_aGCA) :* (NA_I (El y_aGCB) :* (NA_I (El y_aGCC) :* (NA_I (El y_aGCD) :* (NA_I (El y_aGCE) :* (NA_I (El y_aGCF) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGCG) :* (NA_I (El y_aGCH) :* (NA_I (El y_aGCI) :* (NA_I (El y_aGCJ) :* (NA_I (El y_aGCK) :* (NA_I (El y_aGCL) :* (NA_I (El y_aGCM) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGCN) :* (NA_I (El y_aGCO) :* (NA_I (El y_aGCP) :* (NA_I (El y_aGCQ) :* (NA_I (El y_aGCR) :* (NA_I (El y_aGCS) :* (NA_I (El y_aGCT) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGCU) :* (NA_I (El y_aGCV) :* (NA_I (El y_aGCW) :* (NA_I (El y_aGCX) :* (NA_I (El y_aGCY) :* (NA_I (El y_aGCZ) :* (NA_I (El y_aGD0) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGD1) :* (NA_I (El y_aGD2) :* (NA_I (El y_aGD3) :* (NA_I (El y_aGD4) :* (NA_I (El y_aGD5) :* (NA_I (El y_aGD6) :* (NA_I (El y_aGD7) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGD8) :* (NA_I (El y_aGD9) :* (NA_I (El y_aGDa) :* (NA_I (El y_aGDb) :* (NA_I (El y_aGDc) :* (NA_I (El y_aGDd) :* (NA_I (El y_aGDe) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDf) :* (NA_I (El y_aGDg) :* (NA_I (El y_aGDh) :* (NA_I (El y_aGDi) :* (NA_I (El y_aGDj) :* (NA_I (El y_aGDk) :* (NA_I (El y_aGDl) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDm) :* (NA_I (El y_aGDn) :* (NA_I (El y_aGDo) :* (NA_I (El y_aGDp) :* (NA_I (El y_aGDq) :* (NA_I (El y_aGDr) :* (NA_I (El y_aGDs) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDt) :* (NA_I (El y_aGDu) :* (NA_I (El y_aGDv) :* (NA_I (El y_aGDw) :* (NA_I (El y_aGDx) :* (NA_I (El y_aGDy) :* (NA_I (El y_aGDz) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDA) :* (NA_I (El y_aGDB) :* (NA_I (El y_aGDC) :* (NA_I (El y_aGDD) :* (NA_I (El y_aGDE) :* (NA_I (El y_aGDF) :* (NA_I (El y_aGDG) :* NP0))))))))))))))))))))))) -> ()
SE' -> \case
(Rep (H (NA_I (El y_aGDH) :* (NA_I (El y_aGDI) :* (NA_I (El y_aGDJ) :* (NA_I (El y_aGDK) :* (NA_I (El y_aGDL) :* (NA_I (El y_aGDM) :* (NA_I (El y_aGDN) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGDO) :* (NA_I (El y_aGDP) :* (NA_I (El y_aGDQ) :* (NA_I (El y_aGDR) :* (NA_I (El y_aGDS) :* (NA_I (El y_aGDT) :* (NA_I (El y_aGDU) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGDV) :* (NA_I (El y_aGDW) :* (NA_I (El y_aGDX) :* (NA_I (El y_aGDY) :* (NA_I (El y_aGDZ) :* (NA_I (El y_aGE0) :* (NA_I (El y_aGE1) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGE2) :* (NA_I (El y_aGE3) :* (NA_I (El y_aGE4) :* (NA_I (El y_aGE5) :* (NA_I (El y_aGE6) :* (NA_I (El y_aGE7) :* (NA_I (El y_aGE8) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGE9) :* (NA_I (El y_aGEa) :* (NA_I (El y_aGEb) :* (NA_I (El y_aGEc) :* (NA_I (El y_aGEd) :* (NA_I (El y_aGEe) :* (NA_I (El y_aGEf) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGEg) :* (NA_I (El y_aGEh) :* (NA_I (El y_aGEi) :* (NA_I (El y_aGEj) :* (NA_I (El y_aGEk) :* (NA_I (El y_aGEl) :* (NA_I (El y_aGEm) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGEv) :* (NA_I (El y_aGEw) :* (NA_I (El y_aGEx) :* (NA_I (El y_aGEy) :* (NA_I (El y_aGEz) :* (NA_I (El y_aGEA) :* (NA_I (El y_aGEB) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGEE) :* (NA_I (El y_aGEF) :* (NA_I (El y_aGEG) :* (NA_I (El y_aGEH) :* (NA_I (El y_aGEI) :* (NA_I (El y_aGEM) :* (NA_I (El y_aGEN) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGEO) :* (NA_I (El y_aGEP) :* (NA_I (El y_aGEQ) :* (NA_I (El y_aGER) :* (NA_I (El y_aGES) :* (NA_I (El y_aGET) :* (NA_I (El y_aGEU) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGEV) :* (NA_I (El y_aGEW) :* (NA_I (El y_aGEX) :* (NA_I (El y_aGEY) :* (NA_I (El y_aGEZ) :* (NA_I (El y_aGF0) :* (NA_I (El y_aGF1) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGF2) :* (NA_I (El y_aGF3) :* (NA_I (El y_aGF4) :* (NA_I (El y_aGF5) :* (NA_I (El y_aGF6) :* (NA_I (El y_aGF7) :* (NA_I (El y_aGF8) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGF9) :* (NA_I (El y_aGFa) :* (NA_I (El y_aGFb) :* (NA_I (El y_aGFc) :* (NA_I (El y_aGFd) :* (NA_I (El y_aGFe) :* (NA_I (El y_aGFf) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFg) :* (NA_I (El y_aGFh) :* (NA_I (El y_aGFi) :* (NA_I (El y_aGFj) :* (NA_I (El y_aGFk) :* (NA_I (El y_aGFl) :* (NA_I (El y_aGFm) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFn) :* (NA_I (El y_aGFo) :* (NA_I (El y_aGFp) :* (NA_I (El y_aGFq) :* (NA_I (El y_aGFr) :* (NA_I (El y_aGFs) :* (NA_I (El y_aGFt) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFC) :* (NA_I (El y_aGFD) :* (NA_I (El y_aGFE) :* (NA_I (El y_aGFF) :* (NA_I (El y_aGFG) :* (NA_I (El y_aGFH) :* (NA_I (El y_aGFI) :* NP0))))))))))))))))))))))) -> ()
SF' -> \case
(Rep (H (NA_I (El y_aGFQ) :* (NA_I (El y_aGFR) :* (NA_I (El y_aGFS) :* (NA_I (El y_aGFT) :* (NA_I (El y_aGFU) :* (NA_I (El y_aGFW) :* (NA_I (El y_aGFX) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGG1) :* (NA_I (El y_aGG2) :* (NA_I (El y_aGG3) :* (NA_I (El y_aGG4) :* (NA_I (El y_aGG5) :* (NA_I (El y_aGG6) :* (NA_I (El y_aGG7) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGG8) :* (NA_I (El y_aGG9) :* (NA_I (El y_aGGa) :* (NA_I (El y_aGGb) :* (NA_I (El y_aGGc) :* (NA_I (El y_aGGd) :* (NA_I (El y_aGGe) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGGf) :* (NA_I (El y_aGGg) :* (NA_I (El y_aGGh) :* (NA_I (El y_aGGi) :* (NA_I (El y_aGGj) :* (NA_I (El y_aGGk) :* (NA_I (El y_aGGl) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGGm) :* (NA_I (El y_aGGn) :* (NA_I (El y_aGGo) :* (NA_I (El y_aGGp) :* (NA_I (El y_aGGq) :* (NA_I (El y_aGGr) :* (NA_I (El y_aGGs) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGGt) :* (NA_I (El y_aGGu) :* (NA_I (El y_aGGv) :* (NA_I (El y_aGGw) :* (NA_I (El y_aGGx) :* (NA_I (El y_aGGy) :* (NA_I (El y_aGGz) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGGA) :* (NA_I (El y_aGGB) :* (NA_I (El y_aGGC) :* (NA_I (El y_aGGD) :* (NA_I (El y_aGGE) :* (NA_I (El y_aGGF) :* (NA_I (El y_aGGG) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGGH) :* (NA_I (El y_aGGI) :* (NA_I (El y_aGGJ) :* (NA_I (El y_aGGK) :* (NA_I (El y_aGGL) :* (NA_I (El y_aGGQ) :* (NA_I (El y_aGGV) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGGZ) :* (NA_I (El y_aGH0) :* (NA_I (El y_aGH1) :* (NA_I (El y_aGH2) :* (NA_I (El y_aGH3) :* (NA_I (El y_aGH4) :* (NA_I (El y_aGH5) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHf) :* (NA_I (El y_aGHg) :* (NA_I (El y_aGHh) :* (NA_I (El y_aGHi) :* (NA_I (El y_aGHj) :* (NA_I (El y_aGHk) :* (NA_I (El y_aGHl) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHq) :* (NA_I (El y_aGHr) :* (NA_I (El y_aGHs) :* (NA_I (El y_aGHt) :* (NA_I (El y_aGHu) :* (NA_I (El y_aGHv) :* (NA_I (El y_aGHw) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHx) :* (NA_I (El y_aGHy) :* (NA_I (El y_aGHz) :* (NA_I (El y_aGHA) :* (NA_I (El y_aGHB) :* (NA_I (El y_aGHC) :* (NA_I (El y_aGHD) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHE) :* (NA_I (El y_aGHF) :* (NA_I (El y_aGHG) :* (NA_I (El y_aGHH) :* (NA_I (El y_aGHI) :* (NA_I (El y_aGHJ) :* (NA_I (El y_aGHK) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHL) :* (NA_I (El y_aGHM) :* (NA_I (El y_aGHN) :* (NA_I (El y_aGHO) :* (NA_I (El y_aGHP) :* (NA_I (El y_aGHQ) :* (NA_I (El y_aGHR) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHS) :* (NA_I (El y_aGHT) :* (NA_I (El y_aGHU) :* (NA_I (El y_aGHV) :* (NA_I (El y_aGHW) :* (NA_I (El y_aGHX) :* (NA_I (El y_aGHY) :* NP0))))))))))))))))))))))) -> ()
SG' -> \case
(Rep (H (NA_I (El y_aGHZ) :* (NA_I (El y_aGI0) :* (NA_I (El y_aGI1) :* (NA_I (El y_aGI2) :* (NA_I (El y_aGI3) :* (NA_I (El y_aGI4) :* (NA_I (El y_aGI5) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGId) :* (NA_I (El y_aGIe) :* (NA_I (El y_aGIf) :* (NA_I (El y_aGIg) :* (NA_I (El y_aGIh) :* (NA_I (El y_aGIi) :* (NA_I (El y_aGIj) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGIk) :* (NA_I (El y_aGIl) :* (NA_I (El y_aGIm) :* (NA_I (El y_aGIn) :* (NA_I (El y_aGIo) :* (NA_I (El y_aGIp) :* (NA_I (El y_aGIr) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGIt) :* (NA_I (El y_aGIu) :* (NA_I (El y_aGIv) :* (NA_I (El y_aGIw) :* (NA_I (El y_aGIx) :* (NA_I (El y_aGIy) :* (NA_I (El y_aGIz) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGIA) :* (NA_I (El y_aGIB) :* (NA_I (El y_aGIC) :* (NA_I (El y_aGID) :* (NA_I (El y_aGIE) :* (NA_I (El y_aGIF) :* (NA_I (El y_aGIG) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGIH) :* (NA_I (El y_aGII) :* (NA_I (El y_aGIJ) :* (NA_I (El y_aGIK) :* (NA_I (El y_aGIL) :* (NA_I (El y_aGIM) :* (NA_I (El y_aGIN) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGIO) :* (NA_I (El y_aGIP) :* (NA_I (El y_aGIQ) :* (NA_I (El y_aGIR) :* (NA_I (El y_aGIS) :* (NA_I (El y_aGIT) :* (NA_I (El y_aGIU) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGIV) :* (NA_I (El y_aGIW) :* (NA_I (El y_aGIX) :* (NA_I (El y_aGIY) :* (NA_I (El y_aGIZ) :* (NA_I (El y_aGJ0) :* (NA_I (El y_aGJ1) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJc) :* (NA_I (El y_aGJm) :* (NA_I (El y_aGJo) :* (NA_I (El y_aGJp) :* (NA_I (El y_aGJq) :* (NA_I (El y_aGJr) :* (NA_I (El y_aGJs) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJt) :* (NA_I (El y_aGJv) :* (NA_I (El y_aGJw) :* (NA_I (El y_aGJy) :* (NA_I (El y_aGJz) :* (NA_I (El y_aGJD) :* (NA_I (El y_aGJE) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJF) :* (NA_I (El y_aGJG) :* (NA_I (El y_aGJH) :* (NA_I (El y_aGJI) :* (NA_I (El y_aGJJ) :* (NA_I (El y_aGJK) :* (NA_I (El y_aGJL) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJM) :* (NA_I (El y_aGJN) :* (NA_I (El y_aGJO) :* (NA_I (El y_aGJP) :* (NA_I (El y_aGJQ) :* (NA_I (El y_aGJR) :* (NA_I (El y_aGJS) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJT) :* (NA_I (El y_aGJU) :* (NA_I (El y_aGJV) :* (NA_I (El y_aGJW) :* (NA_I (El y_aGJY) :* (NA_I (El y_aGJZ) :* (NA_I (El y_aGK0) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGK3) :* (NA_I (El y_aGK4) :* (NA_I (El y_aGK5) :* (NA_I (El y_aGK6) :* (NA_I (El y_aGK7) :* (NA_I (El y_aGK8) :* (NA_I (El y_aGK9) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGKc) :* (NA_I (El y_aGKd) :* (NA_I (El y_aGKe) :* (NA_I (El y_aGKf) :* (NA_I (El y_aGKg) :* (NA_I (El y_aGKh) :* (NA_I (El y_aGKi) :* NP0))))))))))))))))))))))) -> ()
sfrom' = \case
SA' -> \case
(El (A1 x_a7So x_a7Sp x_a7Sq x_a7Sr x_a7Ss x_a7St x_a7Su)) -> ()
(El (A2 x_a7Sv x_a7Sw x_a7Sx x_a7Sy x_a7Sz x_a7SA x_a7SB)) -> ()
(El (A3 x_a7SC x_a7SD x_a7SE x_a7SF x_a7SG x_a7SH x_a7SI)) -> ()
(El (A4 x_a7SJ x_a7SK x_a7SL x_a7SM x_a7SN x_a7SO x_a7SP)) -> ()
(El (A5 x_a7SQ x_a7SR x_a7SS x_a7ST x_a7SU x_a7SV x_a7SW)) -> ()
(El (A6 x_a7SX x_a7SY x_a7SZ x_a7T0 x_a7T1 x_a7T2 x_a7T3)) -> ()
(El (A7 x_a7T4 x_a7T5 x_a7T6 x_a7T7 x_a7T8 x_a7T9 x_a7Ta)) -> ()
(El (A8 x_a7Tb x_a7Tc x_a7Td x_a7Te x_a7Tf x_a7Tg x_a7Th)) -> ()
(El (A9 x_a7Ti x_a7Tj x_a7Tk x_a7Tl x_a7Tm x_a7Tn x_a7To)) -> ()
(El (AA x_a7Tp x_a7Tq x_a7Tr x_a7Ts x_a7Tt x_a7Tu x_a7Tv)) -> ()
(El (AB x_a7Tw x_a7Tx x_a7Ty x_a7Tz x_a7TA x_a7TB x_a7TC)) -> ()
(El (AC x_a7TD x_a7TE x_a7TF x_a7TG x_a7TH x_a7TI x_a7TJ)) -> ()
(El (AD x_a7TK x_a7TL x_a7TM x_a7TN x_a7TO x_a7TP x_a7TQ)) -> ()
(El (AE x_a7TR x_a7TS x_a7TT x_a7TU x_a7TV x_a7TW x_a7TX)) -> ()
(El (AF x_a7TY x_a7TZ x_a7U0 x_a7U1 x_a7U2 x_a7U3 x_a7U4)) -> ()
SB' -> \case
(El (B1 x_a7U5 x_a7U6 x_a7U7 x_a7U8 x_a7U9 x_a7Ua x_a7Ub)) -> ()
(El (B2 x_a7Uc x_a7Ud x_a7Ue x_a7Uf x_a7Ug x_a7Uh x_a7Ui)) -> ()
(El (B3 x_a7Uj x_a7Uk x_a7Ul x_a7Um x_a7Un x_a7Uo x_a7Up)) -> ()
(El (B4 x_a7Uq x_a7Ur x_a7Us x_a7Ut x_a7Uu x_a7Uv x_a7Uw)) -> ()
(El (B5 x_a7Ux x_a7Uy x_a7Uz x_a7UA x_a7UB x_a7UC x_a7UD)) -> ()
(El (B6 x_a7UE x_a7UF x_a7UG x_a7UH x_a7UI x_a7UJ x_a7UK)) -> ()
(El (B7 x_a7UL x_a7UM x_a7UN x_a7UO x_a7UP x_a7UQ x_a7UR)) -> ()
(El (B8 x_a7US x_a7UT x_a7UU x_a7UV x_a7UW x_a7UX x_a7UY)) -> ()
(El (B9 x_a7UZ x_a7V0 x_a7V1 x_a7V2 x_a7V3 x_a7V4 x_a7V5)) -> ()
(El (BA x_a7V6 x_a7V7 x_a7V8 x_a7V9 x_a7Va x_a7Vb x_a7Vc)) -> ()
(El (BB x_a7Vd x_a7Ve x_a7Vf x_a7Vg x_a7Vh x_a7Vi x_a7Vj)) -> ()
(El (BC x_a7Vk x_a7Vl x_a7Vm x_a7Vn x_a7Vo x_a7Vp x_a7Vq)) -> ()
(El (BD x_a7Vr x_a7Vs x_a7Vt x_a7Vu x_a7Vv x_a7Vw x_a7Vx)) -> ()
(El (BE x_a7Vy x_a7Vz x_a7VA x_a7VB x_a7VC x_a7VD x_a7VE)) -> ()
(El (BF x_a7VF x_a7VG x_a7VH x_a7VI x_a7VJ x_a7VK x_a7VL)) -> ()
SC' -> \case
(El (C1 x_a7VM x_a7VN x_a7VO x_a7VP x_a7VQ x_a7VR x_a7VS)) -> ()
(El (C2 x_a7VT x_a7VU x_a7VV x_a7VW x_a7VX x_a7VY x_a7VZ)) -> ()
(El (C3 x_a7W0 x_a7W1 x_a7W2 x_a7W3 x_a7W4 x_a7W5 x_a7W6)) -> ()
(El (C4 x_a7W7 x_a7W8 x_a7W9 x_a7Wa x_a7Wb x_a7Wc x_a7Wd)) -> ()
(El (C5 x_a7We x_a7Wf x_a7Wg x_a7Wh x_a7Wi x_a7Wj x_a7Wk)) -> ()
(El (C6 x_a7Wl x_a7Wm x_a7Wn x_a7Wo x_a7Wp x_a7Wq x_a7Wr)) -> ()
(El (C7 x_a7Ws x_a7Wt x_a7Wu x_a7Wv x_a7Ww x_a7Wx x_a7Wy)) -> ()
(El (C8 x_a7Wz x_a7WA x_a7WB x_a7WC x_a7WD x_a7WE x_a7WF)) -> ()
(El (C9 x_a7WG x_a7WH x_a7WI x_a7WJ x_a7WK x_a7WL x_a7WM)) -> ()
(El (CA x_a7WN x_a7WO x_a7WP x_a7WQ x_a7WR x_a7WS x_a7WT)) -> ()
(El (CB x_a7WU x_a7WV x_a7WW x_a7WX x_a7WY x_a7WZ x_a7X0)) -> ()
(El (CC x_a7X1 x_a7X2 x_a7X3 x_a7X4 x_a7X5 x_a7X6 x_a7X7)) -> ()
(El (CD x_a7X8 x_a7X9 x_a7Xa x_a7Xb x_a7Xc x_a7Xd x_a7Xe)) -> ()
(El (CE x_a7Xf x_a7Xg x_a7Xh x_a7Xi x_a7Xj x_a7Xk x_a7Xl)) -> ()
(El (CF x_a7Xm x_a7Xn x_a7Xo x_a7Xp x_a7Xq x_a7Xr x_a7Xs)) -> ()
SD' -> \case
(El (D1 x_a7Xt x_a7Xu x_a7Xv x_a7Xw x_a7Xx x_a7Xy x_a7Xz)) -> ()
(El (D2 x_a7XA x_a7XB x_a7XC x_a7XD x_a7XE x_a7XF x_a7XG)) -> ()
(El (D3 x_a7XH x_a7XI x_a7XJ x_a7XK x_a7XL x_a7XM x_a7XN)) -> ()
(El (D4 x_a7XO x_a7XP x_a7XQ x_a7XR x_a7XS x_a7XT x_a7XU)) -> ()
(El (D5 x_a7XV x_a7XW x_a7XX x_a7XY x_a7XZ x_a7Y0 x_a7Y1)) -> ()
(El (D6 x_a7Y2 x_a7Y3 x_a7Y4 x_a7Y5 x_a7Y6 x_a7Y7 x_a7Y8)) -> ()
(El (D7 x_a7Y9 x_a7Ya x_a7Yb x_a7Yc x_a7Yd x_a7Ye x_a7Yf)) -> ()
(El (D8 x_a7Yg x_a7Yh x_a7Yi x_a7Yj x_a7Yk x_a7Yl x_a7Ym)) -> ()
(El (D9 x_a7Yn x_a7Yo x_a7Yp x_a7Yq x_a7Yr x_a7Ys x_a7Yt)) -> ()
(El (DA x_a7Yu x_a7Yv x_a7Yw x_a7Yx x_a7Yy x_a7Yz x_a7YA)) -> ()
(El (DB x_a7YB x_a7YC x_a7YD x_a7YE x_a7YF x_a7YG x_a7YH)) -> ()
(El (DC x_a7YI x_a7YJ x_a7YK x_a7YL x_a7YM x_a7YN x_a7YO)) -> ()
(El (DD x_a7YP x_a7YQ x_a7YR x_a7YS x_a7YT x_a7YU x_a7YV)) -> ()
(El (DE x_a7YW x_a7YX x_a7YY x_a7YZ x_a7Z0 x_a7Z1 x_a7Z2)) -> ()
(El (DF x_a7Z3 x_a7Z4 x_a7Z5 x_a7Z6 x_a7Z7 x_a7Z8 x_a7Z9)) -> ()
SE' -> \case
(El (E1 x_a7Za x_a7Zb x_a7Zc x_a7Zd x_a7Ze x_a7Zf x_a7Zg)) -> ()
(El (E2 x_a7Zh x_a7Zi x_a7Zj x_a7Zk x_a7Zl x_a7Zm x_a7Zn)) -> ()
(El (E3 x_a7Zo x_a7Zp x_a7Zq x_a7Zr x_a7Zs x_a7Zt x_a7Zu)) -> ()
(El (E4 x_a7Zv x_a7Zw x_a7Zx x_a7Zy x_a7Zz x_a7ZA x_a7ZB)) -> ()
(El (E5 x_a7ZC x_a7ZD x_a7ZE x_a7ZF x_a7ZG x_a7ZH x_a7ZI)) -> ()
(El (E6 x_a7ZJ x_a7ZK x_a7ZL x_a7ZM x_a7ZN x_a7ZO x_a7ZP)) -> ()
(El (E7 x_a7ZQ x_a7ZR x_a7ZS x_a7ZT x_a7ZU x_a7ZV x_a7ZW)) -> ()
(El (E8 x_a7ZX x_a7ZY x_a7ZZ x_a800 x_a801 x_a802 x_a803)) -> ()
(El (E9 x_a804 x_a805 x_a806 x_a807 x_a808 x_a809 x_a80a)) -> ()
(El (EA x_a80b x_a80c x_a80d x_a80e x_a80f x_a80g x_a80h)) -> ()
(El (EB x_a80i x_a80j x_a80k x_a80l x_a80m x_a80n x_a80o)) -> ()
(El (EC x_a80p x_a80q x_a80r x_a80s x_a80t x_a80u x_a80v)) -> ()
(El (ED x_a80w x_a80x x_a80y x_a80z x_a80A x_a80B x_a80C)) -> ()
(El (EE x_a80D x_a80E x_a80F x_a80G x_a80H x_a80I x_a80J)) -> ()
(El (EF x_a80K x_a80L x_a80M x_a80N x_a80O x_a80P x_a80Q)) -> ()
SF' -> \case
(El (F1 x_a80R x_a80S x_a80T x_a80U x_a80V x_a80W x_a80X)) -> ()
(El (F2 x_a80Y x_a80Z x_a810 x_a811 x_a812 x_a813 x_a814)) -> ()
(El (F3 x_a815 x_a816 x_a817 x_a818 x_a819 x_a81a x_a81b)) -> ()
(El (F4 x_a81c x_a81d x_a81e x_a81f x_a81g x_a81h x_a81i)) -> ()
(El (F5 x_a81j x_a81k x_a81l x_a81m x_a81n x_a81o x_a81p)) -> ()
(El (F6 x_a81q x_a81r x_a81s x_a81t x_a81u x_a81v x_a81w)) -> ()
(El (F7 x_a81x x_a81y x_a81z x_a81A x_a81B x_a81C x_a81D)) -> ()
(El (F8 x_a81E x_a81F x_a81G x_a81H x_a81I x_a81J x_a81K)) -> ()
(El (F9 x_a81L x_a81M x_a81N x_a81O x_a81P x_a81Q x_a81R)) -> ()
(El (FA x_a81S x_a81T x_a81U x_a81V x_a81W x_a81X x_a81Y)) -> ()
(El (FB x_a81Z x_a820 x_a821 x_a822 x_a823 x_a824 x_a825)) -> ()
(El (FC x_a826 x_a827 x_a828 x_a829 x_a82a x_a82b x_a82c)) -> ()
(El (FD x_a82d x_a82e x_a82f x_a82g x_a82h x_a82i x_a82j)) -> ()
(El (FE x_a82k x_a82l x_a82m x_a82n x_a82o x_a82p x_a82q)) -> ()
(El (FF x_a82r x_a82s x_a82t x_a82u x_a82v x_a82w x_a82x)) -> ()
SG' -> \case
(El (G1 x_a82y x_a82z x_a82A x_a82B x_a82C x_a82D x_a82E)) -> ()
(El (G2 x_a82F x_a82G x_a82H x_a82I x_a82J x_a82K x_a82L)) -> ()
(El (G3 x_a82M x_a82N x_a82O x_a82P x_a82Q x_a82R x_a82S)) -> ()
(El (G4 x_a82T x_a82U x_a82V x_a82W x_a82X x_a82Y x_a82Z)) -> ()
(El (G5 x_a830 x_a831 x_a832 x_a833 x_a834 x_a835 x_a836)) -> ()
(El (G6 x_a837 x_a838 x_a839 x_a83a x_a83b x_a83c x_a83d)) -> ()
(El (G7 x_a83e x_a83f x_a83g x_a83h x_a83i x_a83j x_a83k)) -> ()
(El (G8 x_a83l x_a83m x_a83n x_a83o x_a83p x_a83q x_a83r)) -> ()
(El (G9 x_a83s x_a83t x_a83u x_a83v x_a83w x_a83x x_a83y)) -> ()
(El (GA x_a83z x_a83A x_a83B x_a83C x_a83D x_a83E x_a83F)) -> ()
(El (GB x_a83G x_a83H x_a83I x_a83J x_a83K x_a83L x_a83M)) -> ()
(El (GC x_a83N x_a83O x_a83P x_a83Q x_a83R x_a83S x_a83T)) -> ()
(El (GD x_a83U x_a83V x_a83W x_a83X x_a83Y x_a83Z x_a840)) -> ()
(El (GE x_a841 x_a842 x_a843 x_a844 x_a845 x_a846 x_a847)) -> ()
(El (GF x_a848 x_a849 x_a84a x_a84b x_a84c x_a84d x_a84e)) -> ()
main = undefinedfrom generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
That is weird, seriously weird!
…On Tue, Apr 3, 2018 at 1:36 PM, Arian van Putten ***@***.***> wrote:
Interestingly, adding *both* sfrom' and sto' to the mix still doesn't
trigger the bug for Bug.hs. This compiles just fine. I am very confused
now :)
```haskell {-# LANGUAGE CPP #-} {-# LANGUAGE TypeApplications #-} {-#
LANGUAGE RankNTypes #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE
FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE
PatternSynonyms #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE
ScopedTypeVariables #-} {-# LANGUAGE FunctionalDependencies #-} {-#
LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE
TypeFamilies #-}
import GHC.TypeLits (TypeError, ErrorMessage (..))
import Data.Proxy
data Atom kon
= K kon
| I Nat
deriving (Eq, Show)
data Nat = S Nat | Z
deriving (Eq , Show)
data SNat :: Nat -> * where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
type family Lkup (n :: Nat) (ks :: [k]) :: k where
Lkup Z (k : ks) = k
Lkup (S n) (k : ks) = Lkup n ks
Lkup _ '[] = TypeError (Text "Lkup index too big")
data El :: [*] -> Nat -> * where
El :: {unEl :: Lkup ix fam} -> El fam ix
data NS :: (k -> *) -> [k] -> * where
T :: NS p xs -> NS p (x : xs)
H :: p x -> NS p (x : xs)
infixr 5 :*
data NP :: (k ->
*) -> [k] -> * where NP0 :: NP p '[] (:*) :: p x -> NP p xs -> NP p (x :
xs)
data NA :: (kon -> *) -> (nat -> *) -> Atom kon -> * where
NA_I :: phi k -> NA ki phi (I k)
NA_K :: ki k -> NA ki phi (K k)
data Kon
= KInt
| KInteger
| KBool
| KFloat
| KChar
| KString
deriving (Eq , Show)
newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])
= Rep { unRep :: NS (PoA ki phi) code }
type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)
class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]])
| fam -> ki codes , ki codes -> fam
where
sto' :: SNat ix -> Rep ki (El fam) (Lkup ix codes) -> ()
sfrom' :: SNat ix -> El fam ix -> ()
data A = A1 A B C D E F G | A2 A B C D E F G | A3 A B C D E F G | A4 A B C
D E F G | A5 A B C D E F G | A6 A B C D E F G | A7 A B C D E F G | A8 A B C
D E F G | A9 A B C D E F G | AA A B C D E F G | AB A B C D E F G | AC A B C
D E F G | AD A B C D E F G | AE A B C D E F G | AF A B C D E F G
data B = B1 A B C D E F G | B2 A B C D E F G | B3 A B C D E F G | B4 A B C
D E F G | B5 A B C D E F G | B6 A B C D E F G | B7 A B C D E F G | B8 A B C
D E F G | B9 A B C D E F G | BA A B C D E F G | BB A B C D E F G | BC A B C
D E F G | BD A B C D E F G | BE A B C D E F G | BF A B C D E F G
data C = C1 A B C D E F G | C2 A B C D E F G | C3 A B C D E F G | C4 A B C
D E F G | C5 A B C D E F G | C6 A B C D E F G | C7 A B C D E F G | C8 A B C
D E F G | C9 A B C D E F G | CA A B C D E F G | CB A B C D E F G | CC A B C
D E F G | CD A B C D E F G | CE A B C D E F G | CF A B C D E F G
data D = D1 A B C D E F G | D2 A B C D E F G | D3 A B C D E F G | D4 A B C
D E F G | D5 A B C D E F G | D6 A B C D E F G | D7 A B C D E F G | D8 A B C
D E F G | D9 A B C D E F G | DA A B C D E F G | DB A B C D E F G | DC A B C
D E F G | DD A B C D E F G | DE A B C D E F G | DF A B C D E F G
data E = E1 A B C D E F G | E2 A B C D E F G | E3 A B C D E F G | E4 A B C
D E F G | E5 A B C D E F G | E6 A B C D E F G | E7 A B C D E F G | E8 A B C
D E F G | E9 A B C D E F G | EA A B C D E F G | EB A B C D E F G | EC A B C
D E F G | ED A B C D E F G | EE A B C D E F G | EF A B C D E F G
data F = F1 A B C D E F G | F2 A B C D E F G | F3 A B C D E F G | F4 A B C
D E F G | F5 A B C D E F G | F6 A B C D E F G | F7 A B C D E F G | F8 A B C
D E F G | F9 A B C D E F G | FA A B C D E F G | FB A B C D E F G | FC A B C
D E F G | FD A B C D E F G | FE A B C D E F G | FF A B C D E F G
data G = G1 A B C D E F G | G2 A B C D E F G | G3 A B C D E F G | G4 A B C
D E F G | G5 A B C D E F G | G6 A B C D E F G | G7 A B C D E F G | G8 A B C
D E F G | G9 A B C D E F G | GA A B C D E F G | GB A B C D E F G | GC A B C
D E F G | GD A B C D E F G | GE A B C D E F G | GF A B C D E F G
type A' = S Z
type B' = S (S Z)
type C' = S (S (S Z))
type D' = S (S (S (S Z)))
type E' = S (S (S (S (S Z))))
type F' = S (S (S (S (S (S Z)))))
type G' = S (S (S (S (S (S (S Z))))))
pattern SA' = SZ
pattern SB' = (SS SZ)
pattern SC' = (SS (SS SZ))
pattern SD' = (SS (SS (SS SZ)))
pattern SE' = (SS (SS (SS (SS SZ))))
pattern SF' = (SS (SS (SS (SS (SS SZ)))))
pattern SG' = (SS (SS (SS (SS (SS (SS SZ))))))
data Singl (kon :: Kon) :: * where
type FamA = '[A, B, C, D, E, F ,G]
type Prod = '[I A', I B', I C' , I D' , I E' , I F' , I G']
type Sum = '[Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod, Prod,
Prod, Prod, Prod, Prod, Prod]
type CodesA = [Sum, Sum, Sum, Sum, Sum, Sum, Sum]
instance Family Singl FamA CodesA where
sto' = \case
SA' -> \case
(Rep (H (NA_I (El y_aGws) :* (NA_I (El y_aGwt) :* (NA_I (El y_aGwu) :*
(NA_I (El y_aGwv) :* (NA_I (El y_aGww) :* (NA_I (El y_aGwx) :* (NA_I (El
y_aGwy) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGwH) :* (NA_I (El y_aGwI) :* (NA_I (El y_aGwK) :*
(NA_I (El y_aGwL) :* (NA_I (El y_aGwM) :* (NA_I (El y_aGwN) :* (NA_I (El
y_aGwO) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGwZ) :* (NA_I (El y_aGx0) :* (NA_I (El y_aGx1)
:* (NA_I (El y_aGx2) :* (NA_I (El y_aGx3) :* (NA_I (El y_aGx4) :* (NA_I (El
y_aGx5) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGx6) :* (NA_I (El y_aGx7) :* (NA_I (El
y_aGx8) :* (NA_I (El y_aGx9) :* (NA_I (El y_aGxa) :* (NA_I (El y_aGxb) :*
(NA_I (El y_aGxc) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGxd) :* (NA_I (El y_aGxe) :* (NA_I (El
y_aGxg) :* (NA_I (El y_aGxh) :* (NA_I (El y_aGxi) :* (NA_I (El y_aGxj) :*
(NA_I (El y_aGxk) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGxl) :* (NA_I (El y_aGxm) :* (NA_I (El
y_aGxn) :* (NA_I (El y_aGxo) :* (NA_I (El y_aGxp) :* (NA_I (El y_aGxq) :*
(NA_I (El y_aGxr) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGxs) :* (NA_I (El y_aGxt) :* (NA_I
(El y_aGxu) :* (NA_I (El y_aGxv) :* (NA_I (El y_aGxw) :* (NA_I (El y_aGxx)
:* (NA_I (El y_aGxy) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGxz) :* (NA_I (El y_aGxA) :*
(NA_I (El y_aGxB) :* (NA_I (El y_aGxC) :* (NA_I (El y_aGxD) :* (NA_I (El
y_aGxE) :* (NA_I (El y_aGxF) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxG) :* (NA_I (El y_aGxH) :*
(NA_I (El y_aGxI) :* (NA_I (El y_aGxJ) :* (NA_I (El y_aGxK) :* (NA_I (El
y_aGxL) :* (NA_I (El y_aGxM) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxN) :* (NA_I (El y_aGxO)
:* (NA_I (El y_aGxP) :* (NA_I (El y_aGxQ) :* (NA_I (El y_aGxR) :* (NA_I (El
y_aGxS) :* (NA_I (El y_aGxT) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGxU) :* (NA_I (El
y_aGxV) :* (NA_I (El y_aGxW) :* (NA_I (El y_aGxX) :* (NA_I (El y_aGxY) :*
(NA_I (El y_aGxZ) :* (NA_I (El y_aGy0) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGy1) :* (NA_I (El
y_aGy2) :* (NA_I (El y_aGy3) :* (NA_I (El y_aGy4) :* (NA_I (El y_aGy5) :*
(NA_I (El y_aGy6) :* (NA_I (El y_aGy7) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGy8) :* (NA_I (El
y_aGy9) :* (NA_I (El y_aGya) :* (NA_I (El y_aGyb) :* (NA_I (El y_aGyc) :*
(NA_I (El y_aGyd) :* (NA_I (El y_aGye) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGyf) :* (NA_I
(El y_aGyg) :* (NA_I (El y_aGyh) :* (NA_I (El y_aGyi) :* (NA_I (El y_aGyj)
:* (NA_I (El y_aGyk) :* (NA_I (El y_aGyl) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGym) :*
(NA_I (El y_aGyn) :* (NA_I (El y_aGyo) :* (NA_I (El y_aGyp) :* (NA_I (El
y_aGyq) :* (NA_I (El y_aGyr) :* (NA_I (El y_aGys) :*
NP0))))))))))))))))))))))) -> ()
SB' -> \case
(Rep (H (NA_I (El y_aGyt) :* (NA_I (El y_aGyu) :* (NA_I (El y_aGyv) :*
(NA_I (El y_aGyw) :* (NA_I (El y_aGyx) :* (NA_I (El y_aGyy) :* (NA_I (El
y_aGyz) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGyA) :* (NA_I (El y_aGyB) :* (NA_I (El y_aGyC) :*
(NA_I (El y_aGyD) :* (NA_I (El y_aGyE) :* (NA_I (El y_aGyF) :* (NA_I (El
y_aGyG) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGyH) :* (NA_I (El y_aGyI) :* (NA_I (El y_aGyJ)
:* (NA_I (El y_aGyK) :* (NA_I (El y_aGyL) :* (NA_I (El y_aGyM) :* (NA_I (El
y_aGyN) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGyO) :* (NA_I (El y_aGyP) :* (NA_I (El
y_aGyQ) :* (NA_I (El y_aGyR) :* (NA_I (El y_aGyS) :* (NA_I (El y_aGyT) :*
(NA_I (El y_aGyU) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGyV) :* (NA_I (El y_aGyW) :* (NA_I (El
y_aGyX) :* (NA_I (El y_aGyY) :* (NA_I (El y_aGyZ) :* (NA_I (El y_aGz0) :*
(NA_I (El y_aGz1) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGz3) :* (NA_I (El y_aGz4) :* (NA_I (El
y_aGz5) :* (NA_I (El y_aGz6) :* (NA_I (El y_aGz7) :* (NA_I (El y_aGz8) :*
(NA_I (El y_aGz9) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGza) :* (NA_I (El y_aGzb) :* (NA_I
(El y_aGzc) :* (NA_I (El y_aGzd) :* (NA_I (El y_aGze) :* (NA_I (El y_aGzg)
:* (NA_I (El y_aGzh) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGzi) :* (NA_I (El y_aGzj) :*
(NA_I (El y_aGzk) :* (NA_I (El y_aGzl) :* (NA_I (El y_aGzm) :* (NA_I (El
y_aGzn) :* (NA_I (El y_aGzo) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzp) :* (NA_I (El y_aGzq) :*
(NA_I (El y_aGzs) :* (NA_I (El y_aGzt) :* (NA_I (El y_aGzu) :* (NA_I (El
y_aGzv) :* (NA_I (El y_aGzw) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzz) :* (NA_I (El y_aGzA)
:* (NA_I (El y_aGzB) :* (NA_I (El y_aGzC) :* (NA_I (El y_aGzD) :* (NA_I (El
y_aGzE) :* (NA_I (El y_aGzF) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzH) :* (NA_I (El
y_aGzI) :* (NA_I (El y_aGzJ) :* (NA_I (El y_aGzM) :* (NA_I (El y_aGzN) :*
(NA_I (El y_aGzO) :* (NA_I (El y_aGzP) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzQ) :* (NA_I (El
y_aGzR) :* (NA_I (El y_aGzS) :* (NA_I (El y_aGzT) :* (NA_I (El y_aGzU) :*
(NA_I (El y_aGzV) :* (NA_I (El y_aGzW) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGzX) :* (NA_I (El
y_aGzY) :* (NA_I (El y_aGzZ) :* (NA_I (El y_aGA0) :* (NA_I (El y_aGA1) :*
(NA_I (El y_aGA2) :* (NA_I (El y_aGA3) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGA5) :* (NA_I
(El y_aGA6) :* (NA_I (El y_aGA7) :* (NA_I (El y_aGA8) :* (NA_I (El y_aGA9)
:* (NA_I (El y_aGAa) :* (NA_I (El y_aGAb) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGAc) :*
(NA_I (El y_aGAd) :* (NA_I (El y_aGAe) :* (NA_I (El y_aGAf) :* (NA_I (El
y_aGAg) :* (NA_I (El y_aGAh) :* (NA_I (El y_aGAi) :*
NP0))))))))))))))))))))))) -> ()
SC' -> \case
(Rep (H (NA_I (El y_aGAj) :* (NA_I (El y_aGAk) :* (NA_I (El y_aGAl) :*
(NA_I (El y_aGAm) :* (NA_I (El y_aGAn) :* (NA_I (El y_aGAo) :* (NA_I (El
y_aGAp) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGAq) :* (NA_I (El y_aGAr) :* (NA_I (El y_aGAs) :*
(NA_I (El y_aGAt) :* (NA_I (El y_aGAu) :* (NA_I (El y_aGAv) :* (NA_I (El
y_aGAw) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGAx) :* (NA_I (El y_aGAy) :* (NA_I (El y_aGAz)
:* (NA_I (El y_aGAA) :* (NA_I (El y_aGAB) :* (NA_I (El y_aGAC) :* (NA_I (El
y_aGAD) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGAE) :* (NA_I (El y_aGAF) :* (NA_I (El
y_aGAG) :* (NA_I (El y_aGAH) :* (NA_I (El y_aGAI) :* (NA_I (El y_aGAJ) :*
(NA_I (El y_aGAK) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGAL) :* (NA_I (El y_aGAM) :* (NA_I (El
y_aGAN) :* (NA_I (El y_aGAO) :* (NA_I (El y_aGAP) :* (NA_I (El y_aGAQ) :*
(NA_I (El y_aGAR) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGAS) :* (NA_I (El y_aGAT) :* (NA_I (El
y_aGAU) :* (NA_I (El y_aGAV) :* (NA_I (El y_aGAW) :* (NA_I (El y_aGAX) :*
(NA_I (El y_aGAY) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGAZ) :* (NA_I (El y_aGB0) :* (NA_I
(El y_aGB1) :* (NA_I (El y_aGB2) :* (NA_I (El y_aGB3) :* (NA_I (El y_aGB4)
:* (NA_I (El y_aGB5) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGB6) :* (NA_I (El y_aGB7) :*
(NA_I (El y_aGB8) :* (NA_I (El y_aGB9) :* (NA_I (El y_aGBa) :* (NA_I (El
y_aGBb) :* (NA_I (El y_aGBc) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBd) :* (NA_I (El y_aGBe) :*
(NA_I (El y_aGBf) :* (NA_I (El y_aGBg) :* (NA_I (El y_aGBh) :* (NA_I (El
y_aGBi) :* (NA_I (El y_aGBj) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBk) :* (NA_I (El y_aGBl)
:* (NA_I (El y_aGBm) :* (NA_I (El y_aGBn) :* (NA_I (El y_aGBo) :* (NA_I (El
y_aGBp) :* (NA_I (El y_aGBq) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBr) :* (NA_I (El
y_aGBs) :* (NA_I (El y_aGBt) :* (NA_I (El y_aGBu) :* (NA_I (El y_aGBv) :*
(NA_I (El y_aGBw) :* (NA_I (El y_aGBx) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBy) :* (NA_I (El
y_aGBz) :* (NA_I (El y_aGBA) :* (NA_I (El y_aGBB) :* (NA_I (El y_aGBC) :*
(NA_I (El y_aGBD) :* (NA_I (El y_aGBE) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBF) :* (NA_I (El
y_aGBG) :* (NA_I (El y_aGBH) :* (NA_I (El y_aGBI) :* (NA_I (El y_aGBJ) :*
(NA_I (El y_aGBK) :* (NA_I (El y_aGBL) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBM) :* (NA_I
(El y_aGBN) :* (NA_I (El y_aGBO) :* (NA_I (El y_aGBP) :* (NA_I (El y_aGBQ)
:* (NA_I (El y_aGBR) :* (NA_I (El y_aGBS) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGBT) :*
(NA_I (El y_aGBU) :* (NA_I (El y_aGBV) :* (NA_I (El y_aGBW) :* (NA_I (El
y_aGBX) :* (NA_I (El y_aGBY) :* (NA_I (El y_aGBZ) :*
NP0))))))))))))))))))))))) -> ()
SD' -> \case
(Rep (H (NA_I (El y_aGC0) :* (NA_I (El y_aGC1) :* (NA_I (El y_aGC2) :*
(NA_I (El y_aGC3) :* (NA_I (El y_aGC4) :* (NA_I (El y_aGC5) :* (NA_I (El
y_aGC6) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGC7) :* (NA_I (El y_aGC8) :* (NA_I (El y_aGC9) :*
(NA_I (El y_aGCa) :* (NA_I (El y_aGCb) :* (NA_I (El y_aGCc) :* (NA_I (El
y_aGCd) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGCe) :* (NA_I (El y_aGCf) :* (NA_I (El y_aGCg)
:* (NA_I (El y_aGCh) :* (NA_I (El y_aGCi) :* (NA_I (El y_aGCj) :* (NA_I (El
y_aGCk) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGCl) :* (NA_I (El y_aGCm) :* (NA_I (El
y_aGCn) :* (NA_I (El y_aGCo) :* (NA_I (El y_aGCp) :* (NA_I (El y_aGCq) :*
(NA_I (El y_aGCr) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGCs) :* (NA_I (El y_aGCt) :* (NA_I (El
y_aGCu) :* (NA_I (El y_aGCv) :* (NA_I (El y_aGCw) :* (NA_I (El y_aGCx) :*
(NA_I (El y_aGCy) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGCz) :* (NA_I (El y_aGCA) :* (NA_I (El
y_aGCB) :* (NA_I (El y_aGCC) :* (NA_I (El y_aGCD) :* (NA_I (El y_aGCE) :*
(NA_I (El y_aGCF) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGCG) :* (NA_I (El y_aGCH) :* (NA_I
(El y_aGCI) :* (NA_I (El y_aGCJ) :* (NA_I (El y_aGCK) :* (NA_I (El y_aGCL)
:* (NA_I (El y_aGCM) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGCN) :* (NA_I (El y_aGCO) :*
(NA_I (El y_aGCP) :* (NA_I (El y_aGCQ) :* (NA_I (El y_aGCR) :* (NA_I (El
y_aGCS) :* (NA_I (El y_aGCT) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGCU) :* (NA_I (El y_aGCV) :*
(NA_I (El y_aGCW) :* (NA_I (El y_aGCX) :* (NA_I (El y_aGCY) :* (NA_I (El
y_aGCZ) :* (NA_I (El y_aGD0) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGD1) :* (NA_I (El y_aGD2)
:* (NA_I (El y_aGD3) :* (NA_I (El y_aGD4) :* (NA_I (El y_aGD5) :* (NA_I (El
y_aGD6) :* (NA_I (El y_aGD7) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGD8) :* (NA_I (El
y_aGD9) :* (NA_I (El y_aGDa) :* (NA_I (El y_aGDb) :* (NA_I (El y_aGDc) :*
(NA_I (El y_aGDd) :* (NA_I (El y_aGDe) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDf) :* (NA_I (El
y_aGDg) :* (NA_I (El y_aGDh) :* (NA_I (El y_aGDi) :* (NA_I (El y_aGDj) :*
(NA_I (El y_aGDk) :* (NA_I (El y_aGDl) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDm) :* (NA_I (El
y_aGDn) :* (NA_I (El y_aGDo) :* (NA_I (El y_aGDp) :* (NA_I (El y_aGDq) :*
(NA_I (El y_aGDr) :* (NA_I (El y_aGDs) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDt) :* (NA_I
(El y_aGDu) :* (NA_I (El y_aGDv) :* (NA_I (El y_aGDw) :* (NA_I (El y_aGDx)
:* (NA_I (El y_aGDy) :* (NA_I (El y_aGDz) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGDA) :*
(NA_I (El y_aGDB) :* (NA_I (El y_aGDC) :* (NA_I (El y_aGDD) :* (NA_I (El
y_aGDE) :* (NA_I (El y_aGDF) :* (NA_I (El y_aGDG) :*
NP0))))))))))))))))))))))) -> ()
SE' -> \case
(Rep (H (NA_I (El y_aGDH) :* (NA_I (El y_aGDI) :* (NA_I (El y_aGDJ) :*
(NA_I (El y_aGDK) :* (NA_I (El y_aGDL) :* (NA_I (El y_aGDM) :* (NA_I (El
y_aGDN) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGDO) :* (NA_I (El y_aGDP) :* (NA_I (El y_aGDQ) :*
(NA_I (El y_aGDR) :* (NA_I (El y_aGDS) :* (NA_I (El y_aGDT) :* (NA_I (El
y_aGDU) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGDV) :* (NA_I (El y_aGDW) :* (NA_I (El y_aGDX)
:* (NA_I (El y_aGDY) :* (NA_I (El y_aGDZ) :* (NA_I (El y_aGE0) :* (NA_I (El
y_aGE1) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGE2) :* (NA_I (El y_aGE3) :* (NA_I (El
y_aGE4) :* (NA_I (El y_aGE5) :* (NA_I (El y_aGE6) :* (NA_I (El y_aGE7) :*
(NA_I (El y_aGE8) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGE9) :* (NA_I (El y_aGEa) :* (NA_I (El
y_aGEb) :* (NA_I (El y_aGEc) :* (NA_I (El y_aGEd) :* (NA_I (El y_aGEe) :*
(NA_I (El y_aGEf) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGEg) :* (NA_I (El y_aGEh) :* (NA_I (El
y_aGEi) :* (NA_I (El y_aGEj) :* (NA_I (El y_aGEk) :* (NA_I (El y_aGEl) :*
(NA_I (El y_aGEm) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGEv) :* (NA_I (El y_aGEw) :* (NA_I
(El y_aGEx) :* (NA_I (El y_aGEy) :* (NA_I (El y_aGEz) :* (NA_I (El y_aGEA)
:* (NA_I (El y_aGEB) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGEE) :* (NA_I (El y_aGEF) :*
(NA_I (El y_aGEG) :* (NA_I (El y_aGEH) :* (NA_I (El y_aGEI) :* (NA_I (El
y_aGEM) :* (NA_I (El y_aGEN) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGEO) :* (NA_I (El y_aGEP) :*
(NA_I (El y_aGEQ) :* (NA_I (El y_aGER) :* (NA_I (El y_aGES) :* (NA_I (El
y_aGET) :* (NA_I (El y_aGEU) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGEV) :* (NA_I (El y_aGEW)
:* (NA_I (El y_aGEX) :* (NA_I (El y_aGEY) :* (NA_I (El y_aGEZ) :* (NA_I (El
y_aGF0) :* (NA_I (El y_aGF1) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGF2) :* (NA_I (El
y_aGF3) :* (NA_I (El y_aGF4) :* (NA_I (El y_aGF5) :* (NA_I (El y_aGF6) :*
(NA_I (El y_aGF7) :* (NA_I (El y_aGF8) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGF9) :* (NA_I (El
y_aGFa) :* (NA_I (El y_aGFb) :* (NA_I (El y_aGFc) :* (NA_I (El y_aGFd) :*
(NA_I (El y_aGFe) :* (NA_I (El y_aGFf) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFg) :* (NA_I (El
y_aGFh) :* (NA_I (El y_aGFi) :* (NA_I (El y_aGFj) :* (NA_I (El y_aGFk) :*
(NA_I (El y_aGFl) :* (NA_I (El y_aGFm) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFn) :* (NA_I
(El y_aGFo) :* (NA_I (El y_aGFp) :* (NA_I (El y_aGFq) :* (NA_I (El y_aGFr)
:* (NA_I (El y_aGFs) :* (NA_I (El y_aGFt) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGFC) :*
(NA_I (El y_aGFD) :* (NA_I (El y_aGFE) :* (NA_I (El y_aGFF) :* (NA_I (El
y_aGFG) :* (NA_I (El y_aGFH) :* (NA_I (El y_aGFI) :*
NP0))))))))))))))))))))))) -> ()
SF' -> \case
(Rep (H (NA_I (El y_aGFQ) :* (NA_I (El y_aGFR) :* (NA_I (El y_aGFS) :*
(NA_I (El y_aGFT) :* (NA_I (El y_aGFU) :* (NA_I (El y_aGFW) :* (NA_I (El
y_aGFX) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGG1) :* (NA_I (El y_aGG2) :* (NA_I (El y_aGG3) :*
(NA_I (El y_aGG4) :* (NA_I (El y_aGG5) :* (NA_I (El y_aGG6) :* (NA_I (El
y_aGG7) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGG8) :* (NA_I (El y_aGG9) :* (NA_I (El y_aGGa)
:* (NA_I (El y_aGGb) :* (NA_I (El y_aGGc) :* (NA_I (El y_aGGd) :* (NA_I (El
y_aGGe) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGGf) :* (NA_I (El y_aGGg) :* (NA_I (El
y_aGGh) :* (NA_I (El y_aGGi) :* (NA_I (El y_aGGj) :* (NA_I (El y_aGGk) :*
(NA_I (El y_aGGl) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGGm) :* (NA_I (El y_aGGn) :* (NA_I (El
y_aGGo) :* (NA_I (El y_aGGp) :* (NA_I (El y_aGGq) :* (NA_I (El y_aGGr) :*
(NA_I (El y_aGGs) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGGt) :* (NA_I (El y_aGGu) :* (NA_I (El
y_aGGv) :* (NA_I (El y_aGGw) :* (NA_I (El y_aGGx) :* (NA_I (El y_aGGy) :*
(NA_I (El y_aGGz) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGGA) :* (NA_I (El y_aGGB) :* (NA_I
(El y_aGGC) :* (NA_I (El y_aGGD) :* (NA_I (El y_aGGE) :* (NA_I (El y_aGGF)
:* (NA_I (El y_aGGG) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGGH) :* (NA_I (El y_aGGI) :*
(NA_I (El y_aGGJ) :* (NA_I (El y_aGGK) :* (NA_I (El y_aGGL) :* (NA_I (El
y_aGGQ) :* (NA_I (El y_aGGV) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGGZ) :* (NA_I (El y_aGH0) :*
(NA_I (El y_aGH1) :* (NA_I (El y_aGH2) :* (NA_I (El y_aGH3) :* (NA_I (El
y_aGH4) :* (NA_I (El y_aGH5) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHf) :* (NA_I (El y_aGHg)
:* (NA_I (El y_aGHh) :* (NA_I (El y_aGHi) :* (NA_I (El y_aGHj) :* (NA_I (El
y_aGHk) :* (NA_I (El y_aGHl) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHq) :* (NA_I (El
y_aGHr) :* (NA_I (El y_aGHs) :* (NA_I (El y_aGHt) :* (NA_I (El y_aGHu) :*
(NA_I (El y_aGHv) :* (NA_I (El y_aGHw) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHx) :* (NA_I (El
y_aGHy) :* (NA_I (El y_aGHz) :* (NA_I (El y_aGHA) :* (NA_I (El y_aGHB) :*
(NA_I (El y_aGHC) :* (NA_I (El y_aGHD) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHE) :* (NA_I (El
y_aGHF) :* (NA_I (El y_aGHG) :* (NA_I (El y_aGHH) :* (NA_I (El y_aGHI) :*
(NA_I (El y_aGHJ) :* (NA_I (El y_aGHK) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHL) :* (NA_I
(El y_aGHM) :* (NA_I (El y_aGHN) :* (NA_I (El y_aGHO) :* (NA_I (El y_aGHP)
:* (NA_I (El y_aGHQ) :* (NA_I (El y_aGHR) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGHS) :*
(NA_I (El y_aGHT) :* (NA_I (El y_aGHU) :* (NA_I (El y_aGHV) :* (NA_I (El
y_aGHW) :* (NA_I (El y_aGHX) :* (NA_I (El y_aGHY) :*
NP0))))))))))))))))))))))) -> ()
SG' -> \case
(Rep (H (NA_I (El y_aGHZ) :* (NA_I (El y_aGI0) :* (NA_I (El y_aGI1) :*
(NA_I (El y_aGI2) :* (NA_I (El y_aGI3) :* (NA_I (El y_aGI4) :* (NA_I (El
y_aGI5) :* NP0))))))))) -> ()
(Rep (T (H (NA_I (El y_aGId) :* (NA_I (El y_aGIe) :* (NA_I (El y_aGIf) :*
(NA_I (El y_aGIg) :* (NA_I (El y_aGIh) :* (NA_I (El y_aGIi) :* (NA_I (El
y_aGIj) :* NP0)))))))))) -> ()
(Rep (T (T (H (NA_I (El y_aGIk) :* (NA_I (El y_aGIl) :* (NA_I (El y_aGIm)
:* (NA_I (El y_aGIn) :* (NA_I (El y_aGIo) :* (NA_I (El y_aGIp) :* (NA_I (El
y_aGIr) :* NP0))))))))))) -> ()
(Rep (T (T (T (H (NA_I (El y_aGIt) :* (NA_I (El y_aGIu) :* (NA_I (El
y_aGIv) :* (NA_I (El y_aGIw) :* (NA_I (El y_aGIx) :* (NA_I (El y_aGIy) :*
(NA_I (El y_aGIz) :* NP0)))))))))))) -> ()
(Rep (T (T (T (T (H (NA_I (El y_aGIA) :* (NA_I (El y_aGIB) :* (NA_I (El
y_aGIC) :* (NA_I (El y_aGID) :* (NA_I (El y_aGIE) :* (NA_I (El y_aGIF) :*
(NA_I (El y_aGIG) :* NP0))))))))))))) -> ()
(Rep (T (T (T (T (T (H (NA_I (El y_aGIH) :* (NA_I (El y_aGII) :* (NA_I (El
y_aGIJ) :* (NA_I (El y_aGIK) :* (NA_I (El y_aGIL) :* (NA_I (El y_aGIM) :*
(NA_I (El y_aGIN) :* NP0)))))))))))))) -> ()
(Rep (T (T (T (T (T (T (H (NA_I (El y_aGIO) :* (NA_I (El y_aGIP) :* (NA_I
(El y_aGIQ) :* (NA_I (El y_aGIR) :* (NA_I (El y_aGIS) :* (NA_I (El y_aGIT)
:* (NA_I (El y_aGIU) :* NP0))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (H (NA_I (El y_aGIV) :* (NA_I (El y_aGIW) :*
(NA_I (El y_aGIX) :* (NA_I (El y_aGIY) :* (NA_I (El y_aGIZ) :* (NA_I (El
y_aGJ0) :* (NA_I (El y_aGJ1) :* NP0)))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJc) :* (NA_I (El y_aGJm) :*
(NA_I (El y_aGJo) :* (NA_I (El y_aGJp) :* (NA_I (El y_aGJq) :* (NA_I (El
y_aGJr) :* (NA_I (El y_aGJs) :* NP0))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJt) :* (NA_I (El y_aGJv)
:* (NA_I (El y_aGJw) :* (NA_I (El y_aGJy) :* (NA_I (El y_aGJz) :* (NA_I (El
y_aGJD) :* (NA_I (El y_aGJE) :* NP0)))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJF) :* (NA_I (El
y_aGJG) :* (NA_I (El y_aGJH) :* (NA_I (El y_aGJI) :* (NA_I (El y_aGJJ) :*
(NA_I (El y_aGJK) :* (NA_I (El y_aGJL) :* NP0))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJM) :* (NA_I (El
y_aGJN) :* (NA_I (El y_aGJO) :* (NA_I (El y_aGJP) :* (NA_I (El y_aGJQ) :*
(NA_I (El y_aGJR) :* (NA_I (El y_aGJS) :* NP0)))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGJT) :* (NA_I (El
y_aGJU) :* (NA_I (El y_aGJV) :* (NA_I (El y_aGJW) :* (NA_I (El y_aGJY) :*
(NA_I (El y_aGJZ) :* (NA_I (El y_aGK0) :* NP0))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGK3) :* (NA_I
(El y_aGK4) :* (NA_I (El y_aGK5) :* (NA_I (El y_aGK6) :* (NA_I (El y_aGK7)
:* (NA_I (El y_aGK8) :* (NA_I (El y_aGK9) :* NP0)))))))))))))))))))))) -> ()
(Rep (T (T (T (T (T (T (T (T (T (T (T (T (T (T (H (NA_I (El y_aGKc) :*
(NA_I (El y_aGKd) :* (NA_I (El y_aGKe) :* (NA_I (El y_aGKf) :* (NA_I (El
y_aGKg) :* (NA_I (El y_aGKh) :* (NA_I (El y_aGKi) :*
NP0))))))))))))))))))))))) -> ()
sfrom' = \case
SA' -> \case
(El (A1 x_a7So x_a7Sp x_a7Sq x_a7Sr x_a7Ss x_a7St x_a7Su)) -> ()
(El (A2 x_a7Sv x_a7Sw x_a7Sx x_a7Sy x_a7Sz x_a7SA x_a7SB)) -> ()
(El (A3 x_a7SC x_a7SD x_a7SE x_a7SF x_a7SG x_a7SH x_a7SI)) -> ()
(El (A4 x_a7SJ x_a7SK x_a7SL x_a7SM x_a7SN x_a7SO x_a7SP)) -> ()
(El (A5 x_a7SQ x_a7SR x_a7SS x_a7ST x_a7SU x_a7SV x_a7SW)) -> ()
(El (A6 x_a7SX x_a7SY x_a7SZ x_a7T0 x_a7T1 x_a7T2 x_a7T3)) -> ()
(El (A7 x_a7T4 x_a7T5 x_a7T6 x_a7T7 x_a7T8 x_a7T9 x_a7Ta)) -> ()
(El (A8 x_a7Tb x_a7Tc x_a7Td x_a7Te x_a7Tf x_a7Tg x_a7Th)) -> ()
(El (A9 x_a7Ti x_a7Tj x_a7Tk x_a7Tl x_a7Tm x_a7Tn x_a7To)) -> ()
(El (AA x_a7Tp x_a7Tq x_a7Tr x_a7Ts x_a7Tt x_a7Tu x_a7Tv)) -> ()
(El (AB x_a7Tw x_a7Tx x_a7Ty x_a7Tz x_a7TA x_a7TB x_a7TC)) -> ()
(El (AC x_a7TD x_a7TE x_a7TF x_a7TG x_a7TH x_a7TI x_a7TJ)) -> ()
(El (AD x_a7TK x_a7TL x_a7TM x_a7TN x_a7TO x_a7TP x_a7TQ)) -> ()
(El (AE x_a7TR x_a7TS x_a7TT x_a7TU x_a7TV x_a7TW x_a7TX)) -> ()
(El (AF x_a7TY x_a7TZ x_a7U0 x_a7U1 x_a7U2 x_a7U3 x_a7U4)) -> ()
SB' -> \case
(El (B1 x_a7U5 x_a7U6 x_a7U7 x_a7U8 x_a7U9 x_a7Ua x_a7Ub)) -> ()
(El (B2 x_a7Uc x_a7Ud x_a7Ue x_a7Uf x_a7Ug x_a7Uh x_a7Ui)) -> ()
(El (B3 x_a7Uj x_a7Uk x_a7Ul x_a7Um x_a7Un x_a7Uo x_a7Up)) -> ()
(El (B4 x_a7Uq x_a7Ur x_a7Us x_a7Ut x_a7Uu x_a7Uv x_a7Uw)) -> ()
(El (B5 x_a7Ux x_a7Uy x_a7Uz x_a7UA x_a7UB x_a7UC x_a7UD)) -> ()
(El (B6 x_a7UE x_a7UF x_a7UG x_a7UH x_a7UI x_a7UJ x_a7UK)) -> ()
(El (B7 x_a7UL x_a7UM x_a7UN x_a7UO x_a7UP x_a7UQ x_a7UR)) -> ()
(El (B8 x_a7US x_a7UT x_a7UU x_a7UV x_a7UW x_a7UX x_a7UY)) -> ()
(El (B9 x_a7UZ x_a7V0 x_a7V1 x_a7V2 x_a7V3 x_a7V4 x_a7V5)) -> ()
(El (BA x_a7V6 x_a7V7 x_a7V8 x_a7V9 x_a7Va x_a7Vb x_a7Vc)) -> ()
(El (BB x_a7Vd x_a7Ve x_a7Vf x_a7Vg x_a7Vh x_a7Vi x_a7Vj)) -> ()
(El (BC x_a7Vk x_a7Vl x_a7Vm x_a7Vn x_a7Vo x_a7Vp x_a7Vq)) -> ()
(El (BD x_a7Vr x_a7Vs x_a7Vt x_a7Vu x_a7Vv x_a7Vw x_a7Vx)) -> ()
(El (BE x_a7Vy x_a7Vz x_a7VA x_a7VB x_a7VC x_a7VD x_a7VE)) -> ()
(El (BF x_a7VF x_a7VG x_a7VH x_a7VI x_a7VJ x_a7VK x_a7VL)) -> ()
SC' -> \case
(El (C1 x_a7VM x_a7VN x_a7VO x_a7VP x_a7VQ x_a7VR x_a7VS)) -> ()
(El (C2 x_a7VT x_a7VU x_a7VV x_a7VW x_a7VX x_a7VY x_a7VZ)) -> ()
(El (C3 x_a7W0 x_a7W1 x_a7W2 x_a7W3 x_a7W4 x_a7W5 x_a7W6)) -> ()
(El (C4 x_a7W7 x_a7W8 x_a7W9 x_a7Wa x_a7Wb x_a7Wc x_a7Wd)) -> ()
(El (C5 x_a7We x_a7Wf x_a7Wg x_a7Wh x_a7Wi x_a7Wj x_a7Wk)) -> ()
(El (C6 x_a7Wl x_a7Wm x_a7Wn x_a7Wo x_a7Wp x_a7Wq x_a7Wr)) -> ()
(El (C7 x_a7Ws x_a7Wt x_a7Wu x_a7Wv x_a7Ww x_a7Wx x_a7Wy)) -> ()
(El (C8 x_a7Wz x_a7WA x_a7WB x_a7WC x_a7WD x_a7WE x_a7WF)) -> ()
(El (C9 x_a7WG x_a7WH x_a7WI x_a7WJ x_a7WK x_a7WL x_a7WM)) -> ()
(El (CA x_a7WN x_a7WO x_a7WP x_a7WQ x_a7WR x_a7WS x_a7WT)) -> ()
(El (CB x_a7WU x_a7WV x_a7WW x_a7WX x_a7WY x_a7WZ x_a7X0)) -> ()
(El (CC x_a7X1 x_a7X2 x_a7X3 x_a7X4 x_a7X5 x_a7X6 x_a7X7)) -> ()
(El (CD x_a7X8 x_a7X9 x_a7Xa x_a7Xb x_a7Xc x_a7Xd x_a7Xe)) -> ()
(El (CE x_a7Xf x_a7Xg x_a7Xh x_a7Xi x_a7Xj x_a7Xk x_a7Xl)) -> ()
(El (CF x_a7Xm x_a7Xn x_a7Xo x_a7Xp x_a7Xq x_a7Xr x_a7Xs)) -> ()
SD' -> \case
(El (D1 x_a7Xt x_a7Xu x_a7Xv x_a7Xw x_a7Xx x_a7Xy x_a7Xz)) -> ()
(El (D2 x_a7XA x_a7XB x_a7XC x_a7XD x_a7XE x_a7XF x_a7XG)) -> ()
(El (D3 x_a7XH x_a7XI x_a7XJ x_a7XK x_a7XL x_a7XM x_a7XN)) -> ()
(El (D4 x_a7XO x_a7XP x_a7XQ x_a7XR x_a7XS x_a7XT x_a7XU)) -> ()
(El (D5 x_a7XV x_a7XW x_a7XX x_a7XY x_a7XZ x_a7Y0 x_a7Y1)) -> ()
(El (D6 x_a7Y2 x_a7Y3 x_a7Y4 x_a7Y5 x_a7Y6 x_a7Y7 x_a7Y8)) -> ()
(El (D7 x_a7Y9 x_a7Ya x_a7Yb x_a7Yc x_a7Yd x_a7Ye x_a7Yf)) -> ()
(El (D8 x_a7Yg x_a7Yh x_a7Yi x_a7Yj x_a7Yk x_a7Yl x_a7Ym)) -> ()
(El (D9 x_a7Yn x_a7Yo x_a7Yp x_a7Yq x_a7Yr x_a7Ys x_a7Yt)) -> ()
(El (DA x_a7Yu x_a7Yv x_a7Yw x_a7Yx x_a7Yy x_a7Yz x_a7YA)) -> ()
(El (DB x_a7YB x_a7YC x_a7YD x_a7YE x_a7YF x_a7YG x_a7YH)) -> ()
(El (DC x_a7YI x_a7YJ x_a7YK x_a7YL x_a7YM x_a7YN x_a7YO)) -> ()
(El (DD x_a7YP x_a7YQ x_a7YR x_a7YS x_a7YT x_a7YU x_a7YV)) -> ()
(El (DE x_a7YW x_a7YX x_a7YY x_a7YZ x_a7Z0 x_a7Z1 x_a7Z2)) -> ()
(El (DF x_a7Z3 x_a7Z4 x_a7Z5 x_a7Z6 x_a7Z7 x_a7Z8 x_a7Z9)) -> ()
SE' -> \case
(El (E1 x_a7Za x_a7Zb x_a7Zc x_a7Zd x_a7Ze x_a7Zf x_a7Zg)) -> ()
(El (E2 x_a7Zh x_a7Zi x_a7Zj x_a7Zk x_a7Zl x_a7Zm x_a7Zn)) -> ()
(El (E3 x_a7Zo x_a7Zp x_a7Zq x_a7Zr x_a7Zs x_a7Zt x_a7Zu)) -> ()
(El (E4 x_a7Zv x_a7Zw x_a7Zx x_a7Zy x_a7Zz x_a7ZA x_a7ZB)) -> ()
(El (E5 x_a7ZC x_a7ZD x_a7ZE x_a7ZF x_a7ZG x_a7ZH x_a7ZI)) -> ()
(El (E6 x_a7ZJ x_a7ZK x_a7ZL x_a7ZM x_a7ZN x_a7ZO x_a7ZP)) -> ()
(El (E7 x_a7ZQ x_a7ZR x_a7ZS x_a7ZT x_a7ZU x_a7ZV x_a7ZW)) -> ()
(El (E8 x_a7ZX x_a7ZY x_a7ZZ x_a800 x_a801 x_a802 x_a803)) -> ()
(El (E9 x_a804 x_a805 x_a806 x_a807 x_a808 x_a809 x_a80a)) -> ()
(El (EA x_a80b x_a80c x_a80d x_a80e x_a80f x_a80g x_a80h)) -> ()
(El (EB x_a80i x_a80j x_a80k x_a80l x_a80m x_a80n x_a80o)) -> ()
(El (EC x_a80p x_a80q x_a80r x_a80s x_a80t x_a80u x_a80v)) -> ()
(El (ED x_a80w x_a80x x_a80y x_a80z x_a80A x_a80B x_a80C)) -> ()
(El (EE x_a80D x_a80E x_a80F x_a80G x_a80H x_a80I x_a80J)) -> ()
(El (EF x_a80K x_a80L x_a80M x_a80N x_a80O x_a80P x_a80Q)) -> ()
SF' -> \case
(El (F1 x_a80R x_a80S x_a80T x_a80U x_a80V x_a80W x_a80X)) -> ()
(El (F2 x_a80Y x_a80Z x_a810 x_a811 x_a812 x_a813 x_a814)) -> ()
(El (F3 x_a815 x_a816 x_a817 x_a818 x_a819 x_a81a x_a81b)) -> ()
(El (F4 x_a81c x_a81d x_a81e x_a81f x_a81g x_a81h x_a81i)) -> ()
(El (F5 x_a81j x_a81k x_a81l x_a81m x_a81n x_a81o x_a81p)) -> ()
(El (F6 x_a81q x_a81r x_a81s x_a81t x_a81u x_a81v x_a81w)) -> ()
(El (F7 x_a81x x_a81y x_a81z x_a81A x_a81B x_a81C x_a81D)) -> ()
(El (F8 x_a81E x_a81F x_a81G x_a81H x_a81I x_a81J x_a81K)) -> ()
(El (F9 x_a81L x_a81M x_a81N x_a81O x_a81P x_a81Q x_a81R)) -> ()
(El (FA x_a81S x_a81T x_a81U x_a81V x_a81W x_a81X x_a81Y)) -> ()
(El (FB x_a81Z x_a820 x_a821 x_a822 x_a823 x_a824 x_a825)) -> ()
(El (FC x_a826 x_a827 x_a828 x_a829 x_a82a x_a82b x_a82c)) -> ()
(El (FD x_a82d x_a82e x_a82f x_a82g x_a82h x_a82i x_a82j)) -> ()
(El (FE x_a82k x_a82l x_a82m x_a82n x_a82o x_a82p x_a82q)) -> ()
(El (FF x_a82r x_a82s x_a82t x_a82u x_a82v x_a82w x_a82x)) -> ()
SG' -> \case
(El (G1 x_a82y x_a82z x_a82A x_a82B x_a82C x_a82D x_a82E)) -> ()
(El (G2 x_a82F x_a82G x_a82H x_a82I x_a82J x_a82K x_a82L)) -> ()
(El (G3 x_a82M x_a82N x_a82O x_a82P x_a82Q x_a82R x_a82S)) -> ()
(El (G4 x_a82T x_a82U x_a82V x_a82W x_a82X x_a82Y x_a82Z)) -> ()
(El (G5 x_a830 x_a831 x_a832 x_a833 x_a834 x_a835 x_a836)) -> ()
(El (G6 x_a837 x_a838 x_a839 x_a83a x_a83b x_a83c x_a83d)) -> ()
(El (G7 x_a83e x_a83f x_a83g x_a83h x_a83i x_a83j x_a83k)) -> ()
(El (G8 x_a83l x_a83m x_a83n x_a83o x_a83p x_a83q x_a83r)) -> ()
(El (G9 x_a83s x_a83t x_a83u x_a83v x_a83w x_a83x x_a83y)) -> ()
(El (GA x_a83z x_a83A x_a83B x_a83C x_a83D x_a83E x_a83F)) -> ()
(El (GB x_a83G x_a83H x_a83I x_a83J x_a83K x_a83L x_a83M)) -> ()
(El (GC x_a83N x_a83O x_a83P x_a83Q x_a83R x_a83S x_a83T)) -> ()
(El (GD x_a83U x_a83V x_a83W x_a83X x_a83Y x_a83Z x_a840)) -> ()
(El (GE x_a841 x_a842 x_a843 x_a844 x_a845 x_a846 x_a847)) -> ()
(El (GF x_a848 x_a849 x_a84a x_a84b x_a84c x_a84d x_a84e)) -> ()
main = undefined
</details>
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#6 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AE-l31o55r8oZi1pQt3YU0fb6iF1zV9Uks5tk17RgaJpZM4S7Ngd>
.
from generics-mrsop.
arianvp
commented on August 22, 2024
Okay, so using pattern synonyms, we can 'disable' the exhaustiveness checker. According to @serras, pattern synonyms are not checked!
Maybe we can also add pattern synonyms for the Heres and Theres to further reduce memory usage
from generics-mrsop.
serras
commented on August 22, 2024
To be more specific, the "pattern match checker" (PMC) checks that all the "constructor-like" patterns form a complete set. We do not know this for most pattern synonyms, so I guess this check is omitted. There is some work in being able to declare that a given set of pattern synonyms in complete, as outlined in the wiki.
from generics-mrsop.
arianvp
commented on August 22, 2024
I tried giving a shot today at modifying the TH generation, but it's really aba kadabra for me.. :')
from generics-mrsop.
arianvp
commented on August 22, 2024
We can add some readable pattern synonyms like below. I also tried Pattern Synonyming the Reps to even further reduce the exhaustiveness checking, but I have a hard time convincing the compiler to still typecheck then. Which probably is due to GADTs and such.
While we're at it, and as already mentioned in the comments in TH.hs it would probably also be useful to add pattern synonyms for Tags so that pattern matching becomes easy in user code:
pattern a :>:: as = Tag CZ (NA_K a :* NA_I (El as) :* NP0)
pattern Leaf_ a = Tag (CS CZ) (NA_K a :* NP0)
pattern Nil_ = Tag CZ NP0
pattern Cons_ a as = Tag (CS CZ) (NA_I a :* NA_I (El as) :* NP0)
type ListCode = '[ '[] , '[I (S Z) , I Z] ]
type RTCode = '[ '[K KInt , I Z] , '[K KInt] ]
type CodesRose = '[ListCode , RTCode]
type FamRose = '[ [R Int] , R Int]
-- * Pattern synonyms type indices
pattern List_R_Int_ = SZ
pattern R_Int_ = SS SZ
-- * Pattern synonyms for Reps
-- TODO: This would probably further reduce mem usage. But they're hard to get right :(
-- TODO: having a hard time making this typecheck. probably due to GADTs etc
-- pattern Cons_ x xs = Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0)))
-- pattern Nil_ = Rep ( Here NP0)
-- pattern a :>:: as = Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0))
-- pattern Leaf_ a = Rep (There (Here (NA_K (SInt a) :* NP0)))
-- ** Instance Decl
instance Family Singl FamRose CodesRose where
sfrom' R_Int_ (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)
sfrom' R_Int_ (El (Leaf a)) = Rep $ There (Here (NA_K (SInt a) :* NP0))
sfrom' List_R_Int_ (El []) = Rep $ Here NP0
sfrom' List_R_Int_ (El (x:xs)) = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))
sto' List_R_Int_ Nil_
= El []
sto' List_R_Int_ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))
= El (x : xs)
sto' R_Int_ (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))
= El (a :>: as)
sto' R_Int_ (Rep (There (Here (NA_K (SInt a) :* NP0))))
= El (Leaf a)from generics-mrsop.
serras
commented on August 22, 2024
I think we can convince the compiler if we give those patterns a pattern signature. Be aware that those signatures are quite weird, as they have two blocks of constraints separated by => and each of them has a different meaning for the pattern.
Maybe we can gather and give it a try tomorrow. I am free after the AFP lecture, which runs from 9 to 11.
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
I'm generating pattern synonyms for the indexes, but it still does not work...
commit: 1efd295
I noticed you also generate a bunch of type synonyms; could this be a thing?
Will try anyway
from generics-mrsop.
arianvp
commented on August 22, 2024
With 'still doesn't work' you mean "still uses too much memory" ?
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
Yes.
I have just finished generating type synonyms for numbers too, here's the splice for rose trees:
type D0_ = Z
type D1_ = S Z
type FamRoseInt = '[Rose Int, [Rose Int]]
type CodesRoseInt =
'['['[K KInt, I D1_], '[K KInt]], '['[], '[I D0_, I D1_]]]
pattern IdxRoseInt = SZ
pattern IdxListRoseInt = SS SZ
instance Family Singl FamRoseInt CodesRoseInt where
sfrom'
= \case
\ IdxRoseInt
-> \case
\ (El ((:>:) x_avK9 x_avKa))
-> Rep (Here ((NA_K (SInt x_avK9)) :* ((NA_I (El x_avKa)) :* NP0)))
\ (El (Leaf x_avKb))
-> Rep (There (Here ((NA_K (SInt x_avKb)) :* NP0)))
\ IdxListRoseInt
-> \case
\ (El ghc-prim-0.5.2.0:GHC.Types.[]) -> Rep (Here NP0)
\ (El ((ghc-prim-0.5.2.0:GHC.Types.:) x_avKc x_avKd))
-> Rep
(There (Here ((NA_I (El x_avKc)) :* ((NA_I (El x_avKd)) :* NP0))))
sto'
= \case
\ IdxRoseInt
-> \case
\ (Rep (Here (NA_K (SInt y_avKe) :* (NA_I (El y_avKf) :* NP0))))
-> El (((:>:) y_avKe) y_avKf)
\ (Rep (There (Here (NA_K (SInt y_avKg) :* NP0))))
-> El (Leaf y_avKg)
\ _ -> error "matchAll"
\ IdxListRoseInt
-> \case
\ (Rep (Here NP0)) -> El ghc-prim-0.5.2.0:GHC.Types.[]
\ (Rep (There (Here (NA_I (El y_avKh) :* (NA_I (El y_avKi) :* NP0)))))
-> El (((ghc-prim-0.5.2.0:GHC.Types.:) y_avKh) y_avKi)
\ _ -> error "matchAll"
\ _ -> error "matchAll"The memory usage for GoAST was much smoother in the beginning, and the increments are
slower. It is better, for sure! Still leaks, though. :/
edit: this is all in the ghc-bug branch.
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
I tried adding more pattern synonyms to the mix. I think we reached the edge of GHC.
SimpTH, RoseTreeTH and LambdaAlphaEqTH compile fine, which indicates that
the TH is generating the correct things. Still, GoAST now breaks with gigantic errors such as this one (warning: not for the faint of heart).
The current Rose tree splice looks like:
type D0_ = Z
type D1_ = S Z
type FamRoseInt = '[Rose Int, [Rose Int]]
type CodesRoseInt =
'['['[K KInt, I D1_], '[K KInt]], '['[], '[I D0_, I D1_]]]
pattern IdxRoseInt = SZ
pattern IdxListRoseInt = SS SZ
pattern HT0_0_ d_awsz = Here d_awsz
pattern HT0_1_ d_awsA = There (Here d_awsA)
pattern HT1_0_ d_awsC = Here d_awsC
pattern HT1_1_ d_awsD = There (Here d_awsD)
instance Family Singl FamRoseInt CodesRoseInt where
sfrom'
= \case
\ IdxRoseInt
-> \case
\ (El ((:>:) x_awsF x_awsG))
-> Rep
(HT0_0_ ((NA_K (SInt x_awsF)) :* ((NA_I (El x_awsG)) :* NP0)))
\ (El (Leaf x_awsH)) -> Rep (HT0_1_ ((NA_K (SInt x_awsH)) :* NP0))
\ IdxListRoseInt
-> \case
\ (El ghc-prim-0.5.2.0:GHC.Types.[]) -> Rep (HT1_0_ NP0)
\ (El ((ghc-prim-0.5.2.0:GHC.Types.:) x_awsI x_awsJ))
-> Rep (HT1_1_ ((NA_I (El x_awsI)) :* ((NA_I (El x_awsJ)) :* NP0)))
sto'
= \case
\ IdxRoseInt
-> \case
\ (Rep (HT0_0_ (NA_K (SInt y_awsK) :* (NA_I (El y_awsL) :* NP0))))
-> El (((:>:) y_awsK) y_awsL)
\ (Rep (HT0_1_ (NA_K (SInt y_awsM) :* NP0))) -> El (Leaf y_awsM)
\ _ -> error "matchAll"
\ IdxListRoseInt
-> \case
\ (Rep (HT1_0_ NP0)) -> El ghc-prim-0.5.2.0:GHC.Types.[]
\ (Rep (HT1_1_ (NA_I (El y_awsN) :* (NA_I (El y_awsO) :* NP0))))
-> El (((ghc-prim-0.5.2.0:GHC.Types.:) y_awsN) y_awsO)
\ _ -> error "matchAll"
\ _ -> error "matchAll"from generics-mrsop.
serras
commented on August 22, 2024
We might require some pattern synonym signatures...
El jue., 5 abr. 2018 19:12, Victor Cacciari Miraldo <
[email protected]> escribió:
… I tried adding more pattern synonyms to the mix. I think we reached the
edge of GHC.
SimpTH, RoseTreeTH and LambdaAlphaEqTH compile fine, which indicates that
the TH is generating the correct things. Still, GoAST now breaks with gigantic
errors such as this one <https://pastebin.com/1FJdr9DJ> (warning: not for
the faint of heart).
The current Rose tree splice looks like:
type D0_ = Ztype D1_ = S Z
type FamRoseInt = '[Rose Int, [Rose Int]]type CodesRoseInt =
'['['[K KInt, I D1_], '[K KInt]], '['[], '[I D0_, I D1_]]]
pattern IdxRoseInt = SZ
pattern IdxListRoseInt = SS SZ
pattern HT0_0_ d_awsz = Here d_awsz
pattern HT0_1_ d_awsA = There (Here d_awsA)
pattern HT1_0_ d_awsC = Here d_awsC
pattern HT1_1_ d_awsD = There (Here d_awsD)
instance Family Singl FamRoseInt CodesRoseInt where
sfrom'
= \case
\ IdxRoseInt
-> \case
\ (El ((:>:) x_awsF x_awsG))
-> Rep
(HT0_0_ ((NA_K (SInt x_awsF)) :* ((NA_I (El x_awsG)) :* NP0)))
\ (El (Leaf x_awsH)) -> Rep (HT0_1_ ((NA_K (SInt x_awsH)) :* NP0))
\ IdxListRoseInt
-> \case
\ (El ghc-prim-0.5.2.0:GHC.Types.[]) -> Rep (HT1_0_ NP0)
\ (El ((ghc-prim-0.5.2.0:GHC.Types.:) x_awsI x_awsJ))
-> Rep (HT1_1_ ((NA_I (El x_awsI)) :* ((NA_I (El x_awsJ)) :* NP0)))
sto'
= \case
\ IdxRoseInt
-> \case
\ (Rep (HT0_0_ (NA_K (SInt y_awsK) :* (NA_I (El y_awsL) :* NP0))))
-> El (((:>:) y_awsK) y_awsL)
\ (Rep (HT0_1_ (NA_K (SInt y_awsM) :* NP0))) -> El (Leaf y_awsM)
\ _ -> error "matchAll"
\ IdxListRoseInt
-> \case
\ (Rep (HT1_0_ NP0)) -> El ghc-prim-0.5.2.0:GHC.Types.[]
\ (Rep (HT1_1_ (NA_I (El y_awsN) :* (NA_I (El y_awsO) :* NP0))))
-> El (((ghc-prim-0.5.2.0:GHC.Types.:) y_awsN) y_awsO)
\ _ -> error "matchAll"
\ _ -> error "matchAll"
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#6 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAS4VvOn7sS7tUUjBwruhRfCTaphNY5Kks5tllADgaJpZM4S7Ngd>
.
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
With pattern synonym signatures it explodes even faster!! 🤕 🤒
This is what we're generating now:
type D0_ = Z
type D1_ = S Z
type FamRoseInt = '[Rose Int, [Rose Int]]
type CodesRoseInt =
'['['[K KInt, I D1_], '[K KInt]], '['[], '[I D0_, I D1_]]]
pattern IdxRoseInt = SZ
pattern IdxListRoseInt = SS SZ
pattern Pat158 ::
PoA Singl (El FamRoseInt) '[I D0_, I D1_]
-> NS (PoA Singl (El FamRoseInt)) '['[], '[I D0_, I D1_]]
pattern Pat158 d_axMo = There (Here d_axMo)
pattern Pat19193 ::
PoA Singl (El FamRoseInt) '[]
-> NS (PoA Singl (El FamRoseInt)) '['[], '[I D0_, I D1_]]
pattern Pat19193 d_axMn = Here d_axMn
pattern Pat0Leaf ::
PoA Singl (El FamRoseInt) '[K KInt]
-> NS (PoA Singl (El FamRoseInt)) '['[K KInt, I D1_], '[K KInt]]
pattern Pat0Leaf d_axMm = There (Here d_axMm)
pattern Pat0586258 ::
PoA Singl (El FamRoseInt) '[K KInt, I D1_]
-> NS (PoA Singl (El FamRoseInt)) '['[K KInt, I D1_], '[K KInt]]
pattern Pat0586258 d_axMl = Here d_axMl
instance Family Singl FamRoseInt CodesRoseInt where
sfrom'
= \case
\ IdxRoseInt
-> \case
\ (El ((:>:) x_axMp x_axMq))
-> Rep
(Pat0586258 ((NA_K (SInt x_axMp)) :* ((NA_I (El x_axMq)) :* NP0)))
\ (El (Leaf x_axMr))
-> Rep (Pat0Leaf ((NA_K (SInt x_axMr)) :* NP0))
\ IdxListRoseInt
-> \case
\ (El ghc-prim-0.5.2.0:GHC.Types.[]) -> Rep (Pat19193 NP0)
\ (El ((ghc-prim-0.5.2.0:GHC.Types.:) x_axMs x_axMt))
-> Rep (Pat158 ((NA_I (El x_axMs)) :* ((NA_I (El x_axMt)) :* NP0)))
sto'
= \case
\ IdxRoseInt
-> \case
\ (Rep (Pat0586258 (NA_K (SInt y_axMu) :* (NA_I (El y_axMv) :* NP0))))
-> El (((:>:) y_axMu) y_axMv)
\ (Rep (Pat0Leaf (NA_K (SInt y_axMw) :* NP0))) -> El (Leaf y_axMw)
\ _ -> error "matchAll"
\ IdxListRoseInt
-> \case
\ (Rep (Pat19193 NP0)) -> El ghc-prim-0.5.2.0:GHC.Types.[]
\ (Rep (Pat158 (NA_I (El y_axMx) :* (NA_I (El y_axMy) :* NP0))))
-> El (((ghc-prim-0.5.2.0:GHC.Types.:) y_axMx) y_axMy)
\ _ -> error "matchAll"
\ _ -> error "matchAll"@arianvp can you try to typecheck on your machine to see if at least the ceiling is lower?
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
https://github.com/VictorCMiraldo/ghc-14987-repro-pipeline
from generics-mrsop.
arianvp
commented on August 22, 2024
Simon asked us to file a new Trac ticket for the bug that causes some of the generated code to not compile at all.
Also, we should probably file a bug for the fact that the exhaustiveness checker can not be disabled.
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
For posterity's and documentation sake:
We thought that since GHC does not complain about non-exhaustive patterns on function
declarations, only on case statements, the exhaustiveness checker would not run
on those cases. False.
Nevertheless, we have a branch where our TH engine generates function decls instead
of case statements for the Family instance ( 661dc32 )
from generics-mrsop.
serras
commented on August 22, 2024
One of the main goals of GHC 8.8 is to improve compilation of type-family-heavy programs -> https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.8.1
from generics-mrsop.
arianvp
commented on August 22, 2024
We should resubmit a ticket probably and add it to the list of performance-related tickets . Our previous one was closed I think.
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
This is the bug report: https://ghc.haskell.org/trac/ghc/ticket/14987
I don't think it is closed
from generics-mrsop.
VictorCMiraldo
commented on August 22, 2024
For the sake of documentation; This have generated yet another bug report:
https://gitlab.haskell.org/ghc/ghc/issues/17223
We might be uncovering multiple problems in GHC.
Sorry and thanks for the attention, ghc developers!
from generics-mrsop.
Related Issues (20)
- Create pattern synonyms for `Tag` automatically
- Implement Attribute Grammars HOT 8
- TH Generates dupicate pattern synonyms if type is in AST multiple times HOT 1
- GHC 8.4.3 triggers GHC Bug during Haddock generations :( HOT 3
- Use Generic Generic Programming to avoid Template Haskell? HOT 2
- Fix is AnnFix HOT 1
- Use efficient indexed Sum from Oleg's Freer Monads paper HOT 3
- Depend on sop-core HOT 14
- Change Eq1 and Show1 names HOT 1
- Drop Monad constraint on mapNPM and friends HOT 1
- Slightly tweak Rep and Fix for pedagogical reasons HOT 5
- Can only derive one datatype per module HOT 4
- Hide examples from documentation
- Make Attribute Grammar combinators monadic HOT 1
- Bring Treefixes into mrsop. HOT 1
- GHC 8.4.3 crashes with hs-elisp parser. HOT 2
- Better Naming Framework for TH code
- Use `th-abstraction`
- Bring back `ShowHO` and `EqHO` as we had before HOT 3
- Rename Holes constructors; make it standard HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from generics-mrsop.