<commit_before>{-# LANGUAGE DataKinds, KindSignatures, FlexibleContexts, StandaloneDeriving
           , UndecidableInstances, FlexibleInstances #-}

data Nat = Z | S Nat

class LC (rep :: Nat -> *) where
  var :: rep n
  lam :: rep n -> rep n
  app :: rep n -> rep n -> rep n

class TypedLC (rep :: Nat -> *) where
  annot :: rep n -> rep (S n) -> rep n
  typeof :: rep n -> rep (S n)
  arr :: rep (S n) -> rep (S n) -> rep (S n)
  pi' :: rep (S n) -> rep (S n)

class BuiltinLC (rep :: Nat -> *) where
  star :: rep (S (S n))
  int :: rep (S n)
  cnst :: Int -> rep Z


-- ## TESTS ##

t1, t2 :: LC rep => rep Z
t1 = lam var
t2 = t1 `app` t1

t3 :: (LC rep, BuiltinLC rep) => rep Z
t3 = t1 `app` cnst 42

newtype LString (n :: Nat) = L { unL :: String } deriving Show

instance {-HasLevel (LString n) => -}LC LString where
  var = {-addLevel $-} L "?"
  lam body = L $ "(\\" ++ unL body ++ ")"
  app e1 e2 = L $ "(" ++ unL e1 ++ " " ++ unL e2 ++ ")"

class HasLevel p where
  addLevel :: p -> p
  level :: p -> Int

instance HasLevel (LString Z) where
  addLevel p = L $ unL p ++ "@" ++ (show . level) p
  level _ = 0

instance HasLevel (LString n) => HasLevel (LString (S n)) where
  addLevel p = L $ unL p ++ "@" ++ (show . level) p
  level _ = 1

instance BuiltinLC LString where
  cnst i = L $ show i
  star = L "*"

instance TypedLC LString where
  --pi' -- TODO

newtype TypeOf (rep :: Nat -> *) (n :: Nat) = T { unT :: rep (S n) }

deriving instance Show (rep (S n)) => Show (TypeOf rep n)

instance (LC rep, TypedLC rep) => LC (TypeOf rep) where
  var = T var
  lam (T body) = T $ pi' body

instance BuiltinLC rep => TypedLC (TypeOf rep) where
  pi' _ = T star<commit_msg>tau star = star<commit_after>{-# LANGUAGE DataKinds, KindSignatures, FlexibleContexts, StandaloneDeriving
           , UndecidableInstances, FlexibleInstances #-}

data Nat = Z | S Nat

class LC (rep :: Nat -> *) where
  var :: rep n
  lam :: rep n -> rep n
  app :: rep n -> rep n -> rep n

class TypedLC (rep :: Nat -> *) where
  annot :: rep n -> rep (S n) -> rep n
  typeof :: rep n -> rep (S n)
  arr :: rep (S n) -> rep (S n) -> rep (S n)
  pi' :: rep (S n) -> rep (S n)

class BuiltinLC (rep :: Nat -> *) where
  star :: rep (S (S n))
  int :: rep (S n)
  cnst :: Int -> rep Z


-- ## TESTS ##

t1, t2 :: LC rep => rep Z
t1 = lam var
t2 = t1 `app` t1

t3 :: (LC rep, BuiltinLC rep) => rep Z
t3 = t1 `app` cnst 42

newtype LString (n :: Nat) = L { unL :: String } deriving Show

instance {-HasLevel (LString n) => -}LC LString where
  var = {-addLevel $-} L "?"
  lam body = L $ "(\\ " ++ unL body ++ ")"
  app e1 e2 = L $ "(" ++ unL e1 ++ " " ++ unL e2 ++ ")"

class HasLevel p where
  addLevel :: p -> p
  level :: p -> Int

instance HasLevel (LString Z) where
  addLevel p = L $ unL p ++ "@" ++ (show . level) p
  level _ = 0

instance HasLevel (LString n) => HasLevel (LString (S n)) where
  addLevel p = L $ unL p ++ "@" ++ (show . level) p
  level _ = 1

instance BuiltinLC LString where
  cnst i = L $ show i
  star = L "*"

instance TypedLC LString where
  pi' body = L $ "(|| " ++ unL body ++ ")"

newtype TypeOf (rep :: Nat -> *) (n :: Nat) = T { unT :: rep (S n) }

deriving instance Show (rep (S n)) => Show (TypeOf rep n)

instance (LC rep, TypedLC rep) => LC (TypeOf rep) where
  var = T var
  lam (T body) = T $ pi' body

instance BuiltinLC rep => TypedLC (TypeOf rep) where
  pi' _ = T star

instance BuiltinLC rep => BuiltinLC (TypeOf rep) where
  star = T star
{'fraction_non_alphanumeric': 0.16676283900750144, 'fraction_numerical': 0.009809578765147143, 'mean_word_length': 2.5486182190378712, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 50, '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': '1855438', 'n_tokens_mistral': 1359, 'n_tokens_neox': 1316, 'n_words': 524}