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

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

{- |

Module      :  Examples.LLGeneric
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.LLBase.Term' into @yoko@. This will
eventually be generated via Template Haskell.

-}
module Examples.LLGeneric where

import Examples.LLBase (Term)
import qualified Examples.LLBase as B

import Examples.ReflectAux

data DVar; data Var; data App

concat `fmap` mapM derive [''Term, ''DVar, ''Var, ''App]

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




type instance Rep DVar = D Int
instance Generic DVar where
  rep ~(DVar i) = D i
  obj ~(D i) = DVar i
type instance Rep Var = D Int
instance Generic Var where
  rep ~(Var i) = D i
  obj ~(D i) = Var i
type instance Rep App = R Term :* R Term
instance Generic App where
  rep ~(App tm0 tm1) = FF (R tm0, R tm1)
  obj ~(FF (R tm0, R tm1)) = App tm0 tm1