{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,
  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,
  TypeSynonymInstances, EmptyDataDecls #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

{- |

Module      :  Examples.InnerGeneric
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

The declaration that hook 'Examples.InnerBase.Inner' into @yoko@. This will
eventually be generated via Template Haskell.

-}
module Examples.InnerGeneric where

import qualified Examples.TermBase as B
import Examples.InnerBase (Inner)
import qualified Examples.InnerBase as I

import Examples.ReflectAux

data Lam; data Var; data App

concat `fmap` mapM derive [''Inner, ''Lam, ''Var, ''App]

type instance Tag Lam = $(return $ encode "Lam")
type instance Recurs Lam = N Inner
instance DC Lam where
  occName _ = "Lam"
  type Range Lam = Inner
  fr ~(Lam ty tm) = I.Lam ty tm
data instance RM m (N Lam) = Lam B.Type (Med m Inner)
type instance Tag Var = $(return $ encode "Var")
type instance Recurs Var = V
instance DC Var where
  occName _ = "Var"
  type Range Var = Inner
  fr ~(Var i) = I.Var i
data instance RM m (N Var) = Var Int
type instance Tag App = $(return $ encode "App")
type instance Recurs App = N Inner
instance DC App where
  occName _ = "App"
  type Range App = Inner
  fr ~(App tm0 tm1) = I.App tm0 tm1
data instance RM m (N App) = App (Med m Inner) (Med m Inner)
instance DT Inner where
  packageName _ = "datatype-reflect"
  moduleName _ = "InnerBase"
  type Siblings Inner = N Inner
  data DCU Inner dc where
    Lam_ :: DCU Inner Lam; Var_ :: DCU Inner Var
    App_ :: DCU Inner App
  disband (I.Lam ty tm)   = disbanded $ Lam ty tm
  disband (I.Var i)       = disbanded $ Var i
  disband (I.App tm0 tm1) = disbanded $ App tm0 tm1
type instance Inhabitants (DCU Inner) = (N Lam :+ N Var) :+ N App
instance Finite (DCU Inner) where
  toUni Lam_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits
instance Etinif (DCU Inner) where
  fromUni (Uni x) = case x of
    (OnLeft  (OnLeft  (Here Refl))) -> Lam_
    (OnLeft  (OnRight (Here Refl))) -> Var_
    (OnRight (Here Refl))  -> App_
instance (t ::: Uni (DCs Inner)) => t ::: DCU Inner where
  inhabits = fromUni inhabits
instance EqT (DCU Inner) where eqT = eqTFin




type instance Rep Var = D Int
instance Generic Var where
  rep ~(Var i) = D i
  obj ~(D i) = Var i
type instance Rep Lam = D B.Type :* R Inner
instance Generic Lam where
  rep ~(Lam ty tm) = FF (D ty, R tm)
  obj ~(FF (D ty, R tm)) = Lam ty tm
type instance Rep App = R Inner :* R Inner
instance Generic App where
  rep ~(App tm0 tm1) = FF (R tm0, R tm1)
  obj ~(FF (R tm0, R tm1)) = App tm0 tm1