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

import Data.Char (Char)
import Data.Bool (Bool(..))
import Data.Either (Either(..))
import Data.Eq (Eq)
import Data.Maybe (Maybe(..))
import qualified Data.Function as Fun

import Symantic.Typed.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 (Unlifted repr) =>
    repr (a->b) -> repr a -> repr b
  default lam ::
    Liftable repr => Unliftable repr => Abstractable (Unlifted repr) =>
    (repr a -> repr b) -> repr (a->b)
  default lam1 ::
    Liftable repr => Unliftable repr => Abstractable (Unlifted repr) =>
    (repr a -> repr b) -> repr (a->b)
  default const ::
    Liftable repr => Abstractable (Unlifted repr) =>
    repr (a -> b -> a)
  default flip ::
    Liftable repr => Abstractable (Unlifted repr) =>
    repr ((a -> b -> c) -> b -> a -> c)
  default id ::
    Liftable repr => Abstractable (Unlifted repr) =>
    repr (a->a)
  default (.) ::
    Liftable repr => Abstractable (Unlifted repr) =>
    repr ((b->c) -> (a->b) -> a -> c)
  default ($) ::
    Liftable repr => Abstractable (Unlifted repr) =>
    repr ((a->b) -> a -> b)
  default var ::
    Liftable1 repr => Abstractable (Unlifted 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 (Unlifted repr) =>
    c -> repr c
  constant = lift Fun.. constant
bool :: Constantable Bool repr => Bool -> repr Bool
bool = constant @Bool
char :: Constantable Char repr => Char -> repr Char
char = constant @Char
unit :: Constantable () repr => repr ()
unit = constant @() ()
class Eitherable repr where
  left :: repr (l -> Either l r)
  right :: repr (r -> Either l r)
  default left ::
    Liftable repr => Eitherable (Unlifted repr) =>
    repr (l -> Either l r)
  default right ::
    Liftable repr => Eitherable (Unlifted 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 (Unlifted repr) =>
    Eq a => repr (a -> a -> Bool)
  equal = lift equal
infix 4 `equal`, ==
(==) :: (Abstractable repr, Equalable repr, Eq a) => repr (a -> a -> Bool)
(==) = lam (\x -> lam (\y -> equal .@ x .@ y))
class IfThenElseable repr where
  ifThenElse :: repr Bool -> repr a -> repr a -> repr a
  default ifThenElse ::
    Liftable3 repr => IfThenElseable (Unlifted repr) =>
    repr Bool -> repr a -> repr a -> repr a
  ifThenElse = lift3 ifThenElse
class Listable repr where
  cons :: repr (a -> [a] -> [a])
  nil :: repr [a]
  default cons ::
    Liftable repr => Listable (Unlifted repr) =>
    repr (a -> [a] -> [a])
  default nil ::
    Liftable repr => Listable (Unlifted 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 (Unlifted repr) =>
    repr (Maybe a)
  default just ::
    Liftable repr => Maybeable (Unlifted repr) =>
    repr (a -> Maybe a)
  nothing = lift nothing
  just = lift just