{-# LANGUAGE AllowAmbiguousTypes #-} -- For InferRR
{-# LANGUAGE FlexibleInstances #-} -- For InferRR
{-# LANGUAGE MultiParamTypeClasses #-} -- For InferRR
{-# LANGUAGE ScopedTypeVariables #-} -- For InferRR
{-# LANGUAGE TemplateHaskell #-} -- For reifyTH
{-# LANGUAGE TypeFamilies #-} -- For InferRR
{-# LANGUAGE UndecidableInstances #-} -- For InferRR
-- | Reify an Haskell value using type-directed normalisation-by-evaluation (NBE).
module Reify where

import qualified Language.Haskell.TH as TH
import Syntax


-- | 'RR' witnesses the duality between @meta@ and @(repr a)@.
--  It indicates which type variables in @a@ are not to be instantiated
--  with the arrow type, and instantiates them to @(repr _)@ in @meta@.
--  This is directly taken from: http://okmij.org/ftp/tagless-final/course/TDPE.hs
--
-- * @meta@ instantiates polymorphic types of the original Haskell expression
--   with @(repr _)@ types, according to how 'RR' is constructed
--   using 'base' and @('-->')@. This is obviously not possible
--   if the orignal expression uses monomorphic types (like 'Int'),
--   but remains possible with constrained polymorphic types (like @(Num i => i)@),
--   because @(i)@ can still be inferred to @(repr _)@,
--   whereas the finally chosen @(repr)@
--   (eg. 'E', or 'Identity', or 'TH.CodeQ', or ...)
--   can have a 'Num' instance.
-- * @(repr a)@ is the symantic type as it would have been,
--   had the expression been written with explicit 'lam's
--   instead of bare haskell functions.
-- DOC: http://okmij.org/ftp/tagless-final/cookbook.html#TDPE
-- DOC: http://okmij.org/ftp/tagless-final/NBE.html
-- DOC: https://www.dicosmo.org/Articles/2004-BalatDiCosmoFiore-Popl.pdf
data RR repr meta a = RR
  { -- | 'reflect' converts from a *represented* Haskell term of type @a@
    -- to an object *representing* that value of type @a@.
    reify   :: meta -> repr a
    -- | 'reflect' converts back an object *representing* a value of type @a@,
    -- to the *represented* Haskell term of type @a@.
  , reflect :: repr a -> meta
  }

-- | The base of induction : placeholder for a type which is not the arrow type.
base :: RR repr (repr a) a
base = RR{reify = id, reflect = id}

-- | The inductive case : the arrow type.
-- 'reify' and 'reflect' are built together inductively.
infixr 8 -->
(-->) :: Abstractable repr =>
         RR repr m1 o1 -> RR repr m2 o2 ->
         RR repr (m1 -> m2) (o1 -> o2)
r1 --> r2 = RR
  { reify   = \meta -> lam (reify r2 . meta . reflect r1)
  , reflect = \repr -> reflect r2 . (.@) repr . reify r1
  }


-- * Using a type-class to partially infer 'RR'

-- | Try to infer 'RR' from 'meta' and @(a)@.
-- Using 'inferRR' will still require a type annotation,
-- though it can often be partial.
class InferRR repr meta a where
  inferRR :: RR repr meta a
instance {-# OVERLAPPING #-}
  ( InferRR repr m1 a1
  , InferRR repr m2 a2
  , Abstractable repr
  ) => InferRR repr (m1 -> m2) (a1 -> a2) where
  inferRR = inferRR --> inferRR
instance {-# OVERLAPPABLE #-}
  p ~ repr a =>
  InferRR repr p a where inferRR = base

reifyImplicit :: InferRR repr meta a => meta -> repr a
reifyImplicit = reify inferRR


-- * Using TemplateHaskell to fully auto-generate 'RR'

-- | @$(reifyTH 'Foo.bar)@ calls 'reify' on 'Foo.bar'
-- with an 'RR' generated from the infered type of 'Foo.bar'.
reifyTH :: TH.Name -> TH.Q TH.Exp
reifyTH name = do
  info <- TH.reify name
  case info of
    TH.VarI n (TH.ForallT _vs _ctx ty) _dec ->
      [| reify $(genRR ty) $(return (TH.VarE n)) |]
    where
    genRR (TH.AppT (TH.AppT TH.ArrowT a) b) = [| $(genRR a) --> $(genRR b) |]
    genRR TH.VarT{} = [| base |]