{-# LANGUAGE FlexibleContexts #-}

module ASTAnno where

import AST
import ASTTHUse

import qualified Generics.Annotations.Yield as Y
import Generics.Annotations.Annotations
import Generics.Annotations.ShowFam

import Generics.MultiRec hiding (show)
import Control.Monad.Identity

example :: Ann String AST Expr
Just example = Y.runYield proof $ do
  var    <- yield "var" "x"
  six    <- yield "six" (Const 6)
  nine   <- yield "nine" (Const 9)
  mul    <- yield "mul" (Mul six nine)
  assign <- yield "assign" (var := mul)
  none   <- yield "none" None
  decls  <- yield "decls" (Seq assign none)
  x      <- yield "x" "x"
  xvar   <- yield "xvar" (EVar x)
  y      <- yield "y" "y"
  yvar   <- yield "yvar" (EVar y)
  add    <- yield "add" (Add xvar yvar)
  lets   <- yield "lets" (Let decls add)
  return lets

yield :: El AST ix => x -> ix -> Y.YieldT x AST Identity ix
yield = Y.yield proof

-- instance Eq1 AST where
--   eq1 Expr Expr = Just Refl
--   eq1 Decl Decl = Just Refl
--   eq1 Var  Var  = Just Refl
--   eq1 _    _    = Nothing

instance ShowFam AST where
  showFam Expr = show
  showFam Decl = show
  showFam Var  = show

five :: Int
Just five = Just 5

a, b, c :: Char
[a,b,c] = "abc"