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

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

{- |

Module      :  Examples.TermGeneric
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.TermBase.Type', 'Examples.TermBase.Term',
and 'Examples.TermBase.Decl' into @yoko@. This will eventually be generated via
Template Haskell.

-}
module Examples.TermGeneric where

import qualified Examples.TermBase as B

import Examples.ReflectAux

data TBool; data TInt; data TArrow
data Lam; data Var; data App; data Let
data Decl

concat `fmap` mapM derive
  [''B.Type, ''TBool, ''TInt, ''TArrow,
   ''B.Term, ''Lam, ''Var, ''App, ''Let,
   ''B.Decl, ''Decl]

type instance Tag TBool = $(return $ encode "TBool")
type instance Recurs TBool = U
instance DC TBool where
  occName _ = "TBool"
  type Range TBool = B.Type
  fr _ = B.TBool
data instance RM m (N TBool) = TBool
type instance Tag TInt = $(return $ encode "TInt")
type instance Recurs TInt = U
instance DC TInt where
  occName _ = "TInt"
  type Range TInt = B.Type
  fr _ = B.TInt
data instance RM m (N TInt) = TInt
type instance Tag TArrow = $(return $ encode "TArrow")
type instance Recurs TArrow = N B.Type
instance DC TArrow where
  occName _ = "TArrow"
  type Range TArrow = B.Type
  fr ~(TArrow d r) = B.TArrow d r
data instance RM m (N TArrow) = TArrow (Med m B.Type) (Med m B.Type)
instance DT B.Type where
  packageName _ = "datatype-reflect"
  moduleName _ = "TermBase"
  type Siblings B.Type = N B.Type
  data DCU B.Type dc where
    TBool_ :: DCU B.Type TBool; TInt_ :: DCU B.Type TInt
    TArrow_ :: DCU B.Type TArrow
  disband B.TBool        = disbanded TBool
  disband B.TInt         = disbanded TInt
  disband (B.TArrow d r) = disbanded $ TArrow d r
type instance Inhabitants (DCU B.Type) = N TBool :+ N TInt :+ N TArrow
instance Finite (DCU B.Type) where
  toUni TBool_ = inhabits; toUni TInt_ = inhabits; toUni TArrow_ = inhabits
instance Etinif (DCU B.Type) where
  frUni (Uni x) = case x of
    (OnLeft          (Here Refl)) -> TBool_
    (OnRight (OnLeft  (Here Refl))) -> TInt_
    (OnRight (OnRight (Here Refl))) -> TArrow_
instance (t ::: Uni (DCs B.Type)) => t ::: DCU B.Type where
  inhabits = frUni inhabits
instance EqT (DCU B.Type) where eqT = eqTFin

type instance Tag Lam = $(return $ encode "Lam")
type instance Recurs Lam = N B.Term
instance DC Lam where
  occName _ = "Lam"
  type Range Lam = B.Term
  fr ~(Lam ty tm) = B.Lam ty tm
data instance RM m (N Lam) = Lam B.Type (Med m B.Term)
type instance Tag Var = $(return $ encode "Var")
type instance Recurs Var = U
instance DC Var where
  occName _ = "Var"
  type Range Var = B.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 B.Term
instance DC App where
  occName _ = "App"
  type Range App = B.Term
  fr ~(App tm0 tm1) = B.App tm0 tm1
data instance RM m (N App) = App (Med m B.Term) (Med m B.Term)
type instance Tag Let = $(return $ encode "Let")
type instance Recurs Let = N B.Decl :+ N B.Term
instance DC Let where
  occName _ = "Let"
  type Range Let = B.Term
  fr ~(Let ds tm) = B.Let ds tm
data instance RM m (N Let) = Let [Med m B.Decl] (Med m B.Term)
instance DT B.Term where
  packageName _ = "datatype-reflect"
  moduleName _ = "TermBase"
  type Siblings B.Term = N B.Term :+ N B.Decl
  data DCU B.Term dc where
    Lam_ :: DCU B.Term Lam; Var_ :: DCU B.Term Var
    App_ :: DCU B.Term App; Let_ :: DCU B.Term Let
  disband (B.Lam ty tm)   = disbanded $ Lam ty tm
  disband (B.Var i)       = disbanded $ Var i
  disband (B.App tm0 tm1) = disbanded $ App tm0 tm1
  disband (B.Let ds tm)   = disbanded $ Let ds tm
type instance Inhabitants (DCU B.Term) = (N Lam :+ N Var) :+ (N App :+ N Let)
instance Finite (DCU B.Term) where
  toUni Lam_ = inhabits; toUni Var_ = inhabits
  toUni App_ = inhabits; toUni Let_ = inhabits
instance Etinif (DCU B.Term) where
  frUni (Uni x) = case x of
    (OnLeft  (OnLeft (Here Refl))) -> Lam_
    (OnLeft  (OnRight (Here Refl))) -> Var_
    (OnRight (OnLeft (Here Refl))) -> App_
    (OnRight (OnRight (Here Refl))) -> Let_
instance (t ::: Uni (DCs B.Term)) => t ::: DCU B.Term where
  inhabits = frUni inhabits
instance EqT (DCU B.Term) where eqT = eqTFin

type instance Tag Decl = $(return $ encode "Decl")
type instance Recurs Decl = N B.Term
instance DC Decl where
  occName _ = "Decl"
  type Range Decl = B.Decl
  to = Just . uniqueDC; fr ~(Decl ds tm) = B.Decl ds tm
data instance RM m (N Decl) = Decl B.Type (Med m B.Term)
instance DT B.Decl where
  packageName _ = "datatype-reflect"
  moduleName _ = "DeclBase"
  type Siblings B.Decl = N B.Term :+ N B.Decl
  data DCU B.Decl dc where Decl_ :: DCU B.Decl Decl
  disband ~(B.Decl ty tm) = disbanded $ Decl ty tm
type instance Inhabitants (DCU B.Decl) = N Decl
instance Finite (DCU B.Decl) where
  toUni Decl_ = inhabits
instance Etinif (DCU B.Decl) where
  frUni (Uni (Here Refl)) = Decl_
instance (t ::: Uni (DCs B.Decl)) => t ::: DCU B.Decl where
  inhabits = frUni inhabits
instance EqT (DCU B.Decl) where eqT = eqTFin



type instance Rep TBool = V
instance Generic TBool where
  rep _ = void "rep[TBool]"
  obj _ = TBool
type instance Rep TInt = V
instance Generic TInt where
  rep _ = void "rep[TInt]"
  obj _ = TInt
type instance Rep TArrow = R B.Type :* R B.Type
instance Generic TArrow where
  rep ~(TArrow ty0 ty1) = FF (R ty0, R ty1)
  obj ~(FF (R ty0, R ty1)) = TArrow ty0 ty1

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 B.Term
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 B.Term :* R B.Term
instance Generic App where
  rep ~(App tm0 tm1) = FF (R tm0, R tm1)
  obj ~(FF (R tm0, R tm1)) = App tm0 tm1
type instance Rep Let = F [] (R B.Decl) :* R B.Term
instance Generic Let where
  rep ~(Let ds tm) = FF (F (map R ds), R tm)
  obj ~(FF (F rds, R tm)) = Let (map unR rds) tm

type instance Rep Decl = D B.Type :* R B.Term
instance Generic Decl where
  rep ~(Decl ty tm) = FF (D ty, R tm)
  obj ~(FF (D ty, R tm)) = Decl ty tm