{-# 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