module FreeC.Backend.Agda.Converter.Free
( generatePure
, bind
, free
, applyFreeArgs
, addFreeArgs
, freeArgBinder
, undefinedExpr
, errorExpr
, addPartial
) where
import qualified FreeC.Backend.Agda.Base as Agda.Base
import qualified FreeC.Backend.Agda.Syntax as Agda
generatePure :: Agda.Expr -> Agda.Expr
generatePure = Agda.app $ Agda.Ident $ Agda.qname [] Agda.Base.pure
bind :: Agda.Expr -> Agda.Expr -> Agda.Expr
bind arg k = Agda.RawApp Agda.NoRange [arg, Agda.ident ">>=", k]
free :: Agda.Expr -> Agda.Expr
free = Agda.app $ applyFreeArgs $ Agda.qname' Agda.Base.free
applyFreeArgs :: Agda.QName -> Agda.Expr
applyFreeArgs qname = foldl1 Agda.app
[ Agda.Ident qname
, Agda.Ident (Agda.qname' Agda.Base.shape)
, Agda.Ident (Agda.qname' Agda.Base.position)
]
addFreeArgs :: [Agda.Name] -> [Agda.Name]
addFreeArgs ts = Agda.Base.shape : Agda.Base.position : ts
shape :: Agda.Expr
shape = Agda.Ident $ Agda.qname' $ Agda.Base.shape
position :: Agda.Expr
position = Agda.Ident $ Agda.qname' $ Agda.Base.position
partial :: Agda.Expr
partial = Agda.Ident (Agda.qname' Agda.Base.partial)
freeArgBinder :: [Agda.LamBinding]
freeArgBinder = [ Agda.binding [Agda.Base.shape] Agda.set
, Agda.binding [Agda.Base.position] (shape `Agda.fun` Agda.set)
]
undefinedExpr :: Agda.Expr
undefinedExpr = Agda.ident "undefined"
errorExpr :: Agda.Expr
errorExpr = Agda.ident "error"
addPartial :: Agda.Expr -> Agda.Expr
addPartial = Agda.fun $ Agda.InstanceArg Agda.NoRange $ Agda.unnamed partial'
where
partial' = partial `Agda.app` shape `Agda.app` position