RankB.hs

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}
module BioModels.Definitions.Model.LocalDefault
  where

import Data.Kind
import Data.Reflection
import GHC.Generics

-- * A class for defaults that can be overridden

-- | A class for all datatypes which can be split in several fields whose
-- default values can be different from one part of the code to the next.
--
-- This works thanks to the `Given` class in Data.Reflection. This API provides
-- two functions, 'given' which gets a value from the context, and 'give' which
-- sets a value in the context of some expression. An example:
--
-- let f :: (Given Int) => Int -> Int
--     f x = x + g x
--     g :: (Given Int) => Int -> Int
--     g x = x * given
-- in give 2 (f 3)
--
-- The @f x@ function actually has a extra constraint: @Given Int@, as
-- internally it needs an extra 'Int' to be passed via the context. @give 2
-- expr@ sets this Int in the context of @expr@.
--
-- 'LocalDefault' generalizes that behavior to records which can 'give'
-- several values ('withLocalDef'), or require several values to be 'given'
-- to be reconstructed ('localDef'). Indeed we do not pass the records
-- themselves via the context, but their individuals components. This way, when
-- we use 'withLocalDef' to set some 'PipelineOpts' in the context of an
-- expression, this expression does not have to retrieve a 'PipelineOpts', it can
-- use 'localDef' to retrieve any subset of them (like SolverOpts,
-- InlineOpts, OdeOpts, etc). A function using internally 'localDef' to get
-- SolverOpts for instance will have a @Needs SolverOpts@ constraint, just as
-- any function calling it until we set the SolverOpts or a superset of them
-- with 'withLocalDef'.
--
-- Note that having a 'withLocalDef' inside another call to 'withLocalDef' will
-- create two incoherent instances, so this should be avoided.
--
-- IMPORTANT: This requires all the subfields to be individual data or newtypes,
-- to remove any ambiguity.
class LocalDefault a where
  -- | The subfields of the datatype @a@
  type LocalDefaultFields a :: [Type]
  --
  -- | Override the default value of some type @a@ in the context of an
  -- expression
  withLocalDef :: forall t. a -> ((Needs a) => t) -> t

  -- | Get the overridden value of @a@ from the context
  localDef :: (Needs a) => a

-- | Tells which individual option fields we need to be able to read from the
-- context to construct some datatype
type family Needs a where 
  Needs (GenericDeriving t) = Needs t
  Needs a = GivenAll (LocalDefaultFields a)

-- | A constraint to specify that a function needs to access a list of datatypes
-- from the context
type family GivenAll a :: Constraint where
  GivenAll '[o] = Given o
  GivenAll (o ': os) = (Given o, GivenAll os)

-- * Generic implementation

-- * Generic localDef
type family ConcatConList a b where
  ConcatConList '[] b = b
  ConcatConList (a ': xa) b = a ': ConcatConList xa b

class GLocalDefault f where
  gLocalDef :: (GGivenCons f) => f a
  gWithLocalDef :: f x -> (GGivenCons f => t) -> t
  type GGivenCons f :: Constraint
  type GLocalDefaultFieldsRep f :: [Type]

instance GLocalDefault f => GLocalDefault (M1 i c f) where
  gLocalDef = M1 gLocalDef
  gWithLocalDef (M1 v) x = gWithLocalDef v x

  type GGivenCons (M1 i c f) = GGivenCons f
  type GLocalDefaultFieldsRep (M1 i c f) = GLocalDefaultFieldsRep f

instance (GLocalDefault fa, GLocalDefault fb) => GLocalDefault (fa :*: fb) where
  gLocalDef = gLocalDef :*: gLocalDef
  gWithLocalDef (a :*: b) x = gWithLocalDef a (gWithLocalDef b x)

  type GGivenCons (fa :*: fb) = (GGivenCons fa, GGivenCons fb)
  type GLocalDefaultFieldsRep (fa :*: fb) = ConcatConList (GLocalDefaultFieldsRep fa) (GLocalDefaultFieldsRep fb)

instance (LocalDefault a) => GLocalDefault (K1 i a) where
  gLocalDef = K1 localDef
  gWithLocalDef (K1 v) x = withLocalDef v x

  type GGivenCons (K1 i a) = Needs a -- [1], GGivenCons (Rep t) = Needs t
  type GLocalDefaultFieldsRep (K1 i a) = '[a]


genericLocalDef :: forall t. (Needs t ~ GGivenCons (Rep t), Generic t, GLocalDefault (Rep t), Needs t) => t
genericLocalDef = to gLocalDef

genericWithLocalDef :: forall t a. (Needs t ~ GGivenCons (Rep t), Generic t, GLocalDefault (Rep t)) => t -> (Needs t => a) -> a
genericWithLocalDef v x = gWithLocalDef (from v) x


-- *
type GLocalDefaultFields t = GLocalDefaultFieldsRep (Rep t)

-- * Derivation VIA WIP

-- | A type wrapper for deriving via using generic
newtype FlatLocalDefaultGenericDeriving t = FlatLocalDefaultGenericDeriving t

instance LocalDefault (FlatLocalDefaultGenericDeriving a) where
  type LocalDefaultFields (FlatLocalDefaultGenericDeriving a) = '[ a ] -- By default, we treat @a@ as one
                                           -- big field
  -- | Override the default value of some type @a@ in the context of an
  -- expression
  withLocalDef (FlatLocalDefaultGenericDeriving a) x = give a x
  {-# INLINE withLocalDef #-}

  -- | Get the overridden value of @a@ from the context
  localDef = FlatLocalDefaultGenericDeriving given
  {-# INLINE localDef #-}

newtype GenericDeriving t = GenericDeriving t
  deriving (Show, Generic)

instance
  (
    Generic t
  , GLocalDefault (GHC.Generics.Rep t)
  , GGivenCons (Rep t) ~ Needs t
  ) =>
  LocalDefault (GenericDeriving t)
  where
  withLocalDef (GenericDeriving t) x = genericWithLocalDef t x
  localDef = GenericDeriving genericLocalDef
  type LocalDefaultFields (GenericDeriving t) = GLocalDefaultFieldsRep (Rep t)

data A = A
  deriving (Show)
data B = B
  deriving (Show)

data Rec = Rec {
    aa :: A,
    bb :: B
               }
  deriving (Generic, Show)

deriving via (FlatLocalDefaultGenericDeriving A) instance LocalDefault A
deriving via (FlatLocalDefaultGenericDeriving B) instance LocalDefault B

data Rec2 = Rec2 {
    aaa :: A,
    bbb :: B
               }
  deriving (Generic, Show)


-- This one works
instance LocalDefault Rec2 where
  type LocalDefaultFields Rec2 = GLocalDefaultFields Rec2
  withLocalDef = genericWithLocalDef
  localDef = genericLocalDef

-- But that one, does not (well, it does now)
deriving via (GenericDeriving Rec) instance LocalDefault Rec