<commit_before>{-# LANGUAGE DataKinds, KindSignatures, QuasiQuotes, GADTs,
             StandaloneDeriving, UnicodeSyntax #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies, TypeOperators, PolyKinds
           , MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}

import OmegaParser
import InhabitantTH

(°) :: Int -> Int -> Int
a ° b = a + b

-- Ω values

data Ω :: * -> * where
  Bottom :: Ω a  -- (⊥)
  Int :: Int -> Ω Int
  Apply :: Ω (a -> b) -> Ω a -> Ω b -- (⋅)
deriving instance Show (Ω a)

(⋅) = Apply
(⊥) = Bottom

µ s h = [ω|s * h|]

a = µ 1 2

c = [ω|33|]

c1 = [e|33|]
c2 = [e||id 33||]

stuff = [d| data Nat = Z | S Nat |]
data Nat = Z | S Nat deriving Show

--refinementPlus =
refined
  [d| plus :: (a ° Nat) -> (b ° Nat) -> (a `plus` b ° Nat)
      Z `plus` n = n
      (S m) `plus` n = S (m `plus` n)
    |]

--refined refinementPlus

class (a :: k) °° (b :: *) | a -> b

instance True °° Bool
instance False °° Bool

instance Z °° Nat
instance S n °° Nat

--instance (Nothing :: Maybe k) °° Maybe a
instance (b °° a) => Just b °° Maybe a
--instance (k °° a) => Just k °° Maybe a

class (a :: k) °°° (b :: * -> *) | a -> b
instance Nothing °°° Maybe
--instance (Nothing :: Maybe k) °°° Maybe

data Stuff a b where
  Full :: (a °° b) => Stuff a b
  Part :: (a °°° b) => Stuff a (b c)

deriving instance Show (Stuff a b)

[d|data H|] -- standalone
id [d|data H'|] -- also works

dataRewrite
  [d| data A :: * -> * where B :: A x; C :: B y; D :: !(A z) -> A Char
    |]

dataRewrite -- proper GADT
  [d| data A a where B :: A x; C :: B y; D :: !(A z) -> A Char
    |]

dataRewrite -- very exotic, (C :: B) is not correctly recorded
  [d| data A where B :: A; C :: B; D :: !(C :: A) -> (C :: A)
    |]

<commit_msg>more experiments: data families<commit_after>{-# LANGUAGE DataKinds, KindSignatures, QuasiQuotes, GADTs,
             StandaloneDeriving, UnicodeSyntax #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies, TypeOperators, PolyKinds
           , MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}

import OmegaParser
import InhabitantTH

(°) :: Int -> Int -> Int
a ° b = a + b

-- Ω values

data Ω :: * -> * where
  Bottom :: Ω a  -- (⊥)
  Int :: Int -> Ω Int
  Apply :: Ω (a -> b) -> Ω a -> Ω b -- (⋅)
deriving instance Show (Ω a)

(⋅) = Apply
(⊥) = Bottom

µ s h = [ω|s * h|]

a = µ 1 2

c = [ω|33|]

c1 = [e|33|]
c2 = [e||id 33||]

stuff = [d| data Nat = Z | S Nat |]
data Nat = Z | S Nat deriving Show

--refinementPlus =
refined
  [d| plus :: (a ° Nat) -> (b ° Nat) -> (a `plus` b ° Nat)
      Z `plus` n = n
      (S m) `plus` n = S (m `plus` n)
    |]

--refined refinementPlus

class (a :: k) °° (b :: *) | a -> b where
  data a <° b
  refine :: b -> Maybe (a <° b)

instance True °° Bool where
  newtype True <° Bool = True' Bool deriving Show
  refine t@True = Just $ True' t
  refine _ = Nothing

instance False °° Bool where
  newtype False <° Bool = False' Bool

instance Z °° Nat
instance S n °° Nat

--instance (Nothing :: Maybe k) °° Maybe a
instance (b °° a) => Just b °° Maybe a
--instance (k °° a) => Just k °° Maybe a

class (a :: k) °°° (b :: * -> *) | a -> b where
  data a <°° b

instance Nothing °°° Maybe
--instance (Nothing :: Maybe k) °°° Maybe

data Stuff a b where
  Full :: (a °° b) => Stuff a b
  Part :: (a °°° b) => Stuff a (b c)

deriving instance Show (Stuff a b)

[d|data H|] -- standalone
id [d|data H'|] -- also works


dataRewrite
  [d| data A :: * -> * where B :: A x; C :: B y; D :: !(A z) -> A Char
    |]

dataRewrite -- proper GADT
  [d| data A a where B :: A x; C :: B y; D :: !(A z) -> A Char
    |]

dataRewrite -- very exotic, (C :: B) is not correctly recorded
  [d| data A where B :: A; C :: B; D :: !(C :: A) -> (C :: A)
    |]


-- Things to try: Wire up my equation parser as DecsQ

{'fraction_non_alphanumeric': 0.18666666666666668, 'fraction_numerical': 0.00522875816993464, 'mean_word_length': 2.468721668177697, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 44, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '727822', 'n_tokens_mistral': 1580, 'n_tokens_neox': 1528, 'n_words': 606}