{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Symantic.Univariant.Lang where

import Data.Char (Char)
import Data.Bool (Bool(..))
import Data.Either (Either(..))
import Data.Eq (Eq)
import Data.Kind
import Data.Maybe (Maybe(..))
import Prelude (undefined)
import Text.Show (Show(..))
import qualified Data.Eq as Eq
import qualified Data.Function as Fun
import qualified Prelude

import Symantic.Univariant.Trans

class Abstractable repr where
  -- | Application, aka. unabstract.
  (.@) :: repr (a->b) -> repr a -> repr b; infixl 9 .@
  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  lam :: (repr a -> repr b) -> repr (a->b)
  -- | Like 'lam' but whose argument is used only once,
  -- hence safe to beta-reduce (inline) without duplicating work.
  lam1 :: (repr a -> repr b) -> repr (a->b)
  const :: repr (a -> b -> a)
  flip :: repr ((a -> b -> c) -> b -> a -> c)
  id :: repr (a->a)
  (.) :: repr ((b->c) -> (a->b) -> a -> c); infixr 9 .
  ($) :: repr ((a->b) -> a -> b); infixr 0 $
  var :: repr a -> repr a
  default (.@) ::
    Liftable2 repr => Abstractable (Output repr) =>
    repr (a->b) -> repr a -> repr b
  default lam ::
    Liftable repr => Unliftable repr => Abstractable (Output repr) =>
    (repr a -> repr b) -> repr (a->b)
  default lam1 ::
    Liftable repr => Unliftable repr => Abstractable (Output repr) =>
    (repr a -> repr b) -> repr (a->b)
  default const ::
    Liftable repr => Abstractable (Output repr) =>
    repr (a -> b -> a)
  default flip ::
    Liftable repr => Abstractable (Output repr) =>
    repr ((a -> b -> c) -> b -> a -> c)
  default id ::
    Liftable repr => Abstractable (Output repr) =>
    repr (a->a)
  default (.) ::
    Liftable repr => Abstractable (Output repr) =>
    repr ((b->c) -> (a->b) -> a -> c)
  default ($) ::
    Liftable repr => Abstractable (Output repr) =>
    repr ((a->b) -> a -> b)
  default var ::
    Liftable1 repr => Abstractable (Output repr) =>
    repr a -> repr a
  (.@) = lift2 (.@)
  lam f = lift (lam (trans Fun.. f Fun.. trans))
  lam1 f = lift (lam1 (trans Fun.. f Fun.. trans))
  const = lift const
  flip = lift flip
  id = lift id
  (.) = lift (.)
  ($) = lift ($)
  var = lift1 var
class Anythingable repr where
  anything :: repr a -> repr a
  anything = Fun.id
class Constantable c repr where
  constant :: c -> repr c
  default constant ::
    Liftable repr => Constantable c (Output repr) =>
    c -> repr c
  constant = lift Fun.. constant
bool = constant @Bool
char = constant @Char
unit = constant @() ()
class Eitherable repr where
  left :: repr (l -> Either l r)
  right :: repr (r -> Either l r)
  default left ::
    Liftable repr => Eitherable (Output repr) =>
    repr (l -> Either l r)
  default right ::
    Liftable repr => Eitherable (Output repr) =>
    repr (r -> Either l r)
  left = lift left
  right = lift right
class Equalable repr where
  equal :: Eq a => repr (a -> a -> Bool)
  default equal ::
    Liftable repr => Equalable (Output repr) =>
    Eq a => repr (a -> a -> Bool)
  equal = lift equal
infix 4 `equal`, ==
(==) = lam (\x -> lam (\y -> equal .@ x .@ y))
class Listable repr where
  cons :: repr (a -> [a] -> [a])
  nil :: repr [a]
  default cons ::
    Liftable repr => Listable (Output repr) =>
    repr (a -> [a] -> [a])
  default nil ::
    Liftable repr => Listable (Output repr) =>
    repr [a]
  cons = lift cons
  nil = lift nil
class Maybeable repr where
  nothing :: repr (Maybe a)
  just :: repr (a -> Maybe a)
  default nothing ::
    Liftable repr => Maybeable (Output repr) =>
    repr (Maybe a)
  default just ::
    Liftable repr => Maybeable (Output repr) =>
    repr (a -> Maybe a)
  nothing = lift nothing
  just = lift just