{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE EmptyDataDecls        #-}
{-# LANGUAGE FlexibleInstances     #-}

module ASTUse where

import Generics.MultiRec.Elems.None
import AST

-- * Instantiating the library for AST 

-- ** Index type

data AST :: (* -> *) -> * -> * -> * where
  Expr  ::  AST NoElems Expr Zero
  Decl  ::  AST NoElems Decl (Suc Zero)
  Var   ::  AST NoElems Var  (Suc (Suc Zero))

-- ** Constructors

data Const
instance Constructor Const  where conName _ = "Const"
data Add
instance Constructor Add    where conName _ = "Add"
data Mul
instance Constructor Mul    where conName _ = "Mul"
data EVar
instance Constructor EVar   where conName _ = "EVar"
data Let
instance Constructor Let    where conName _ = "Let"
data Assign
instance Constructor Assign where
  conName _ = ":="
  conFixity _ = Infix NotAssociative 1
data Seq
instance Constructor Seq   where conName _ = "Seq"
data None
instance Constructor None  where conName _ = "None"

-- ** Functor encoding

-- Variations of the encoding below are possible. For instance,
-- the 'C' applications can be omitted if no functions that require
-- constructor information are needed. Furthermore, it is possible
-- to tag every constructor rather than every datatype. That makes
-- the overall structure slightly simpler, but makes the nesting
-- of 'L' and 'R' constructors larger in turn.

type instance PF AST  =    
      (     C Const   (K Int)
       :+:  C Add     (I (Rec Zero) :*: I (Rec Zero))
       :+:  C Mul     (I (Rec Zero) :*: I (Rec Zero))
       :+:  C EVar    (I (Rec (Suc (Suc Zero))))
       :+:  C Let     (I (Rec (Suc Zero)) :*: I (Rec Zero))
      ) :>: Zero
  :+: (     C Assign  (I (Rec (Suc (Suc Zero)))  :*: I (Rec Zero))
       :+:  C Seq     (I (Rec (Suc Zero)) :*: I (Rec (Suc Zero)))
       :+:  C None    U
      ) :>: Suc Zero
  :+: (               (K String)
      ) :>: Suc (Suc Zero)

-- ** 'El' instances

instance El (Proof (AST NoElems)) Zero where proof = Proof Expr
instance El (Proof (AST NoElems)) (Suc Zero) where proof = Proof Decl
instance El (Proof (AST NoElems)) (Suc (Suc Zero))  where proof = Proof Var

-- ** 'Fam' instance

instance Fam AST NoElems where

  from Expr (Const i)  =  L (Tag (L          (C (K i))))
  from Expr (Add e f)  =  L (Tag (R (L       (C (I (CR (R0 Expr e)) :*: I (CR (R0 Expr f)))))))
  from Expr (Mul e f)  =  L (Tag (R (R (L    (C (I (CR (R0 Expr e)) :*: I (CR (R0 Expr f))))))))
  from Expr (EVar x)   =  L (Tag (R (R (R (L (C (I (CR (R0 Var x)))))))))
  from Expr (Let d e)  =  L (Tag (R (R (R (R (C (I (CR (R0 Decl d)) :*: I (CR (R0 Expr e)))))))))

  from Decl (x := e)   =  R (L (Tag (L    (C (I (CR (R0 Var x)) :*: I (CR (R0 Expr e)))))))
  from Decl (Seq c d)  =  R (L (Tag (R (L (C (I (CR (R0 Decl c)) :*: I (CR (R0 Decl d))))))))
  from Decl (None)     =  R (L (Tag (R (R (C U)))))

  from Var  x          =  R (R (Tag (K x)))

  to Expr (L (Tag (L          (C (K i)))))                       =  Const i
  to Expr (L (Tag (R (L       (C (I (CR (R0 Expr e)) :*: I (CR (R0 Expr f))))))))    =  Add e f
  to Expr (L (Tag (R (R (L    (C (I (CR (R0 Expr e)) :*: I (CR (R0 Expr f)))))))))   =  Mul e f
  to Expr (L (Tag (R (R (R (L (C (I (CR (R0 Var x))))))))))               =  EVar x
  to Expr (L (Tag (R (R (R (R (C (I (CR (R0 Decl d)) :*: I (CR (R0 Expr e))))))))))  =  Let d e

  to Decl (R (L (Tag (L    (C (I (CR (R0 Var x)) :*: I (CR (R0 Expr e))))))))       =  x := e
  to Decl (R (L (Tag (R (L (C (I (CR (R0 Decl c)) :*: I (CR (R0 Decl d)))))))))      =  Seq c d
  to Decl (R (L (Tag (R (R (C U))))))                            =  None

  to Var  (R (R (Tag (K x))))                                    =  x

instance EqS (Proof (AST NoElems)) where
  eqS (Proof Expr) (Proof Expr) = Just Refl
  eqS (Proof Decl) (Proof Decl) = Just Refl
  eqS (Proof Var)  (Proof Var)  = Just Refl
  eqS _            _            = Nothing
instance EqS2 (AST NoElems) where
  eqS2 Expr Expr = Just (Refl, Refl)
  eqS2 Decl Decl = Just (Refl, Refl)
  eqS2 Var  Var  = Just (Refl, Refl)
  eqS2 _    _    = Nothing