{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}

#ifndef MIN_VERSION_GLASGOW_HASKELL
#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0
#endif
  -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10

#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
#else
{-# LANGUAGE OverlappingInstances #-}
#endif

#if __GLASGOW_HASKELL__ < 708
#define TYPEABLE Typeable1
#else
#define TYPEABLE Typeable
#endif

-- | Basics for implementing functional EDSLs

module Language.Syntactic.Functional
    ( -- * Syntactic constructs
      Name (..)
    , Literal (..)
    , Construct (..)
    , Binding (..)
    , maxLam
    , lam_template
    , lam
    , fromDeBruijn
    , BindingT (..)
    , maxLamT
    , lamT_template
    , lamT
    , lamTyped
    , BindingDomain (..)
    , Let (..)
    , MONAD (..)
    , Remon (..)
    , desugarMonad
    , desugarMonadTyped
      -- * Free and bound variables
    , freeVars
    , allVars
    , renameUnique'
    , renameUnique
      -- * Alpha-equivalence
    , AlphaEnv
    , alphaEq'
    , alphaEq
      -- * Evaluation
    , Denotation
    , Eval (..)
    , evalDen
    , DenotationM
    , liftDenotationM
    , RunEnv
    , EvalEnv (..)
    , compileSymDefault
    , evalOpen
    , evalClosed
    ) where



#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
#else
import Control.Applicative
#endif
import Control.DeepSeq (NFData (..))
import Control.Monad.Cont
import Control.Monad.Reader
import Control.Monad.State
import Data.Dynamic
import Data.List (genericIndex)
import Data.Proxy
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Tree

import Data.Hash (hashInt)

import Language.Syntactic



----------------------------------------------------------------------------------------------------
-- * Syntactic constructs
----------------------------------------------------------------------------------------------------

-- | Literal
data Literal sig
  where
    Literal :: Show a => a -> Literal (Full a)

instance Symbol Literal
  where
    symSig :: Literal sig -> SigRep sig
symSig (Literal a
_) = SigRep sig
forall sig. Signature sig => SigRep sig
signature

instance Render Literal
  where
    renderSym :: Literal sig -> String
renderSym (Literal a
a) = a -> String
forall a. Show a => a -> String
show a
a

instance Equality Literal
instance StringTree Literal

-- | Generic N-ary syntactic construct
--
-- 'Construct' gives a quick way to introduce a syntactic construct by giving its name and semantic
-- function.
data Construct sig
  where
    Construct :: Signature sig => String -> Denotation sig -> Construct sig
  -- There is no `NFData1` instance for `Construct` because that would give rise
  -- to a constraint `NFData (Denotation sig)`, which easily spreads to other
  -- functions.

instance Symbol Construct
  where
    symSig :: Construct sig -> SigRep sig
symSig (Construct String
_ Denotation sig
_) = SigRep sig
forall sig. Signature sig => SigRep sig
signature

instance Render Construct
  where
    renderSym :: Construct sig -> String
renderSym (Construct String
name Denotation sig
_) = String
name
    renderArgs :: [String] -> Construct sig -> String
renderArgs = [String] -> Construct sig -> String
forall (sym :: * -> *) a. Render sym => [String] -> sym a -> String
renderArgsSmart

instance Equality Construct
  where
    equal :: Construct a -> Construct b -> Bool
equal = Construct a -> Construct b -> Bool
forall (sym :: * -> *) a b. Render sym => sym a -> sym b -> Bool
equalDefault
    hash :: Construct a -> Hash
hash  = Construct a -> Hash
forall (sym :: * -> *) a. Render sym => sym a -> Hash
hashDefault

instance StringTree Construct

-- | Variable name
newtype Name = Name Integer
  deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq, Eq Name
Eq Name
-> (Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
$cp1Ord :: Eq Name
Ord, Integer -> Name
Name -> Name
Name -> Name -> Name
(Name -> Name -> Name)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> (Name -> Name)
-> (Name -> Name)
-> (Name -> Name)
-> (Integer -> Name)
-> Num Name
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Name
$cfromInteger :: Integer -> Name
signum :: Name -> Name
$csignum :: Name -> Name
abs :: Name -> Name
$cabs :: Name -> Name
negate :: Name -> Name
$cnegate :: Name -> Name
* :: Name -> Name -> Name
$c* :: Name -> Name -> Name
- :: Name -> Name -> Name
$c- :: Name -> Name -> Name
+ :: Name -> Name -> Name
$c+ :: Name -> Name -> Name
Num, Int -> Name
Name -> Int
Name -> [Name]
Name -> Name
Name -> Name -> [Name]
Name -> Name -> Name -> [Name]
(Name -> Name)
-> (Name -> Name)
-> (Int -> Name)
-> (Name -> Int)
-> (Name -> [Name])
-> (Name -> Name -> [Name])
-> (Name -> Name -> [Name])
-> (Name -> Name -> Name -> [Name])
-> Enum Name
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Name -> Name -> Name -> [Name]
$cenumFromThenTo :: Name -> Name -> Name -> [Name]
enumFromTo :: Name -> Name -> [Name]
$cenumFromTo :: Name -> Name -> [Name]
enumFromThen :: Name -> Name -> [Name]
$cenumFromThen :: Name -> Name -> [Name]
enumFrom :: Name -> [Name]
$cenumFrom :: Name -> [Name]
fromEnum :: Name -> Int
$cfromEnum :: Name -> Int
toEnum :: Int -> Name
$ctoEnum :: Int -> Name
pred :: Name -> Name
$cpred :: Name -> Name
succ :: Name -> Name
$csucc :: Name -> Name
Enum, Num Name
Ord Name
Num Name -> Ord Name -> (Name -> Rational) -> Real Name
Name -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Name -> Rational
$ctoRational :: Name -> Rational
$cp2Real :: Ord Name
$cp1Real :: Num Name
Real, Enum Name
Real Name
Real Name
-> Enum Name
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> (Name -> Name -> (Name, Name))
-> (Name -> Name -> (Name, Name))
-> (Name -> Integer)
-> Integral Name
Name -> Integer
Name -> Name -> (Name, Name)
Name -> Name -> Name
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: Name -> Integer
$ctoInteger :: Name -> Integer
divMod :: Name -> Name -> (Name, Name)
$cdivMod :: Name -> Name -> (Name, Name)
quotRem :: Name -> Name -> (Name, Name)
$cquotRem :: Name -> Name -> (Name, Name)
mod :: Name -> Name -> Name
$cmod :: Name -> Name -> Name
div :: Name -> Name -> Name
$cdiv :: Name -> Name -> Name
rem :: Name -> Name -> Name
$crem :: Name -> Name -> Name
quot :: Name -> Name -> Name
$cquot :: Name -> Name -> Name
$cp2Integral :: Enum Name
$cp1Integral :: Real Name
Integral, Name -> ()
(Name -> ()) -> NFData Name
forall a. (a -> ()) -> NFData a
rnf :: Name -> ()
$crnf :: Name -> ()
NFData)

instance Show Name
  where
    show :: Name -> String
show (Name Integer
n) = Integer -> String
forall a. Show a => a -> String
show Integer
n

-- | Variables and binders
data Binding sig
  where
    Var :: Name -> Binding (Full a)
    Lam :: Name -> Binding (b :-> Full (a -> b))

instance Symbol Binding
  where
    symSig :: Binding sig -> SigRep sig
symSig (Var Name
_) = SigRep sig
forall sig. Signature sig => SigRep sig
signature
    symSig (Lam Name
_) = SigRep sig
forall sig. Signature sig => SigRep sig
signature

instance NFData1 Binding
  where
    rnf1 :: Binding a -> ()
rnf1 (Var Name
v) = Name -> ()
forall a. NFData a => a -> ()
rnf Name
v
    rnf1 (Lam Name
v) = Name -> ()
forall a. NFData a => a -> ()
rnf Name
v

-- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.
--
-- 'hash' assigns the same hash to all variables and binders. This is a valid over-approximation
-- that enables the following property:
--
-- @`alphaEq` a b ==> `hash` a == `hash` b@
instance Equality Binding
  where
    equal :: Binding a -> Binding b -> Bool
equal (Var Name
v1) (Var Name
v2) = Name
v1Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
v2
    equal (Lam Name
v1) (Lam Name
v2) = Name
v1Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
v2
    equal Binding a
_ Binding b
_ = Bool
False

    hash :: Binding a -> Hash
hash (Var Name
_) = Int -> Hash
hashInt Int
0
    hash (Lam Name
_) = Int -> Hash
hashInt Int
0

instance Render Binding
  where
    renderSym :: Binding sig -> String
renderSym (Var Name
v) = Char
'v' Char -> ShowS
forall a. a -> [a] -> [a]
: Name -> String
forall a. Show a => a -> String
show Name
v
    renderSym (Lam Name
v) = String
"Lam v" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
v
    renderArgs :: [String] -> Binding sig -> String
renderArgs []     (Var Name
v) = Char
'v' Char -> ShowS
forall a. a -> [a] -> [a]
: Name -> String
forall a. Show a => a -> String
show Name
v
    renderArgs [String
body] (Lam Name
v) = String
"(\\" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Char
'v'Char -> ShowS
forall a. a -> [a] -> [a]
:Name -> String
forall a. Show a => a -> String
show Name
v) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
body String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance StringTree Binding
  where
    stringTreeSym :: [Tree String] -> Binding a -> Tree String
stringTreeSym []     (Var Name
v) = String -> [Tree String] -> Tree String
forall a. a -> Forest a -> Tree a
Node (Char
'v' Char -> ShowS
forall a. a -> [a] -> [a]
: Name -> String
forall a. Show a => a -> String
show Name
v) []
    stringTreeSym [Tree String
body] (Lam Name
v) = String -> [Tree String] -> Tree String
forall a. a -> Forest a -> Tree a
Node (String
"Lam " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char
'v' Char -> ShowS
forall a. a -> [a] -> [a]
: Name -> String
forall a. Show a => a -> String
show Name
v) [Tree String
body]

-- | Get the highest name bound by the first 'Lam' binders at every path from the root. If the term
-- has /ordered binders/ \[1\], 'maxLam' returns the highest name introduced in the whole term.
--
-- \[1\] Ordered binders means that the names of 'Lam' nodes are decreasing along every path from
-- the root.
maxLam :: (Project Binding s) => AST s a -> Name
maxLam :: AST s a -> Name
maxLam (Sym s (a :-> a)
lam :$ AST s (Full a)
_) | Just (Lam Name
v) <- s (a :-> a) -> Maybe (Binding (a :-> a))
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj s (a :-> a)
lam = Name
v
maxLam (AST s (a :-> a)
s :$ AST s (Full a)
a) = AST s (a :-> a) -> Name
forall (s :: * -> *) a. Project Binding s => AST s a -> Name
maxLam AST s (a :-> a)
s Name -> Name -> Name
forall a. Ord a => a -> a -> a
`Prelude.max` AST s (Full a) -> Name
forall (s :: * -> *) a. Project Binding s => AST s a -> Name
maxLam AST s (Full a)
a
maxLam AST s a
_ = Name
0

-- | Higher-order interface for variable binding for domains based on 'Binding'
--
-- Assumptions:
--
--   * The body @f@ does not inspect its argument.
--
--   * Applying @f@ to a term with ordered binders results in a term with /ordered binders/ \[1\].
--
-- \[1\] Ordered binders means that the names of 'Lam' nodes are decreasing along every path from
-- the root.
--
-- See \"Using Circular Programs for Higher-Order Syntax\"
-- (ICFP 2013, <https://emilaxelsson.github.io/documents/axelsson2013using.pdf>).
lam_template :: (Project Binding sym)
    => (Name -> sym (Full a))
         -- ^ Variable symbol constructor
    -> (Name -> ASTF sym b -> ASTF sym (a -> b))
         -- ^ Lambda constructor
    -> (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lam_template :: (Name -> sym (Full a))
-> (Name -> ASTF sym b -> ASTF sym (a -> b))
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)
lam_template Name -> sym (Full a)
mkVar Name -> ASTF sym b -> ASTF sym (a -> b)
mkLam ASTF sym a -> ASTF sym b
f = Name -> ASTF sym b -> ASTF sym (a -> b)
mkLam Name
v ASTF sym b
body
  where
    body :: ASTF sym b
body = ASTF sym a -> ASTF sym b
f (ASTF sym a -> ASTF sym b) -> ASTF sym a -> ASTF sym b
forall a b. (a -> b) -> a -> b
$ sym (Full a) -> ASTF sym a
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (sym (Full a) -> ASTF sym a) -> sym (Full a) -> ASTF sym a
forall a b. (a -> b) -> a -> b
$ Name -> sym (Full a)
mkVar Name
v
    v :: Name
v    = Name -> Name
forall a. Enum a => a -> a
succ (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ ASTF sym b -> Name
forall (s :: * -> *) a. Project Binding s => AST s a -> Name
maxLam ASTF sym b
body

-- | Higher-order interface for variable binding
--
-- This function is 'lamT_template' specialized to domains @sym@ satisfying
-- @(`Binding` `:<:` sym)@.
lam :: (Binding :<: sym) => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lam :: (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lam = (Name -> sym (Full a))
-> (Name -> ASTF sym b -> ASTF sym (a -> b))
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)
forall (sym :: * -> *) a b.
Project Binding sym =>
(Name -> sym (Full a))
-> (Name -> ASTF sym b -> ASTF sym (a -> b))
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)
lam_template (Binding (Full a) -> sym (Full a)
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (Binding (Full a) -> sym (Full a))
-> (Name -> Binding (Full a)) -> Name -> sym (Full a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Binding (Full a)
forall a. Name -> Binding (Full a)
Var) (\Name
v ASTF sym b
a -> sym (b :-> Full (a -> b)) -> AST sym (b :-> Full (a -> b))
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (Binding (b :-> Full (a -> b)) -> sym (b :-> Full (a -> b))
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (Name -> Binding (b :-> Full (a -> b))
forall b a. Name -> Binding (b :-> Full (a -> b))
Lam Name
v)) AST sym (b :-> Full (a -> b)) -> ASTF sym b -> ASTF sym (a -> b)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF sym b
a)

-- | Convert from a term with De Bruijn indexes to one with explicit names
--
-- In the argument term, variable 'Name's are treated as De Bruijn indexes, and lambda 'Name's are
-- ignored. (Ideally, one should use a different type for De Bruijn terms.)
fromDeBruijn :: (Binding :<: sym) => ASTF sym a -> ASTF sym a
fromDeBruijn :: ASTF sym a -> ASTF sym a
fromDeBruijn = [Name] -> ASTF sym a -> ASTF sym a
forall (sym :: * -> *) a.
(Binding :<: sym) =>
[Name] -> ASTF sym a -> ASTF sym a
go []
  where
    go :: (Binding :<: sym) => [Name] -> ASTF sym a -> (ASTF sym a)
    go :: [Name] -> ASTF sym a -> ASTF sym a
go [Name]
vs ASTF sym a
var           | Just (Var Name
i) <- ASTF sym a -> Maybe (Binding (Full a))
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj ASTF sym a
var = Binding (Full a) -> ASTF sym a
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (Binding (Full a) -> ASTF sym a) -> Binding (Full a) -> ASTF sym a
forall a b. (a -> b) -> a -> b
$ Name -> Binding (Full a)
forall a. Name -> Binding (Full a)
Var (Name -> Binding (Full a)) -> Name -> Binding (Full a)
forall a b. (a -> b) -> a -> b
$ [Name] -> Name -> Name
forall i a. Integral i => [a] -> i -> a
genericIndex [Name]
vs Name
i
    go [Name]
vs (AST sym (a :-> Full a)
lam :$ AST sym (Full a)
body) | Just (Lam Name
_) <- AST sym (a :-> Full a) -> Maybe (Binding (a :-> Full a))
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj AST sym (a :-> Full a)
lam = Binding (a :-> Full (a -> a)) -> AST sym (a :-> Full (a -> a))
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (Name -> Binding (a :-> Full (a -> a))
forall b a. Name -> Binding (b :-> Full (a -> b))
Lam Name
v) AST sym (a :-> Full (a -> a))
-> AST sym (Full a) -> AST sym (Full (a -> a))
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST sym (Full a)
body'
      where
        body' :: AST sym (Full a)
body' = [Name] -> AST sym (Full a) -> AST sym (Full a)
forall (sym :: * -> *) a.
(Binding :<: sym) =>
[Name] -> ASTF sym a -> ASTF sym a
go (Name
vName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
vs) AST sym (Full a)
body
        v :: Name
v     = Name -> Name
forall a. Enum a => a -> a
succ (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ AST sym (Full a) -> Name
forall (s :: * -> *) a. Project Binding s => AST s a -> Name
maxLam AST sym (Full a)
body'
          -- Same trick as in `lam`
    go [Name]
vs ASTF sym a
a = (forall a. ASTF sym a -> ASTF sym a) -> ASTF sym a -> ASTF sym a
forall (sym :: * -> *).
(forall a. ASTF sym a -> ASTF sym a)
-> forall a. ASTF sym a -> ASTF sym a
gmapT ([Name] -> ASTF sym a -> ASTF sym a
forall (sym :: * -> *) a.
(Binding :<: sym) =>
[Name] -> ASTF sym a -> ASTF sym a
go [Name]
vs) ASTF sym a
a

-- | Typed variables and binders
data BindingT sig
  where
    VarT :: Typeable a => Name -> BindingT (Full a)
    LamT :: Typeable a => Name -> BindingT (b :-> Full (a -> b))

instance Symbol BindingT
  where
    symSig :: BindingT sig -> SigRep sig
symSig (VarT Name
_) = SigRep sig
forall sig. Signature sig => SigRep sig
signature
    symSig (LamT Name
_) = SigRep sig
forall sig. Signature sig => SigRep sig
signature

instance NFData1 BindingT
  where
    rnf1 :: BindingT a -> ()
rnf1 (VarT Name
v) = Name -> ()
forall a. NFData a => a -> ()
rnf Name
v
    rnf1 (LamT Name
v) = Name -> ()
forall a. NFData a => a -> ()
rnf Name
v

-- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.
--
-- 'hash' assigns the same hash to all variables and binders. This is a valid over-approximation
-- that enables the following property:
--
-- @`alphaEq` a b ==> `hash` a == `hash` b@
instance Equality BindingT
  where
    equal :: BindingT a -> BindingT b -> Bool
equal (VarT Name
v1) (VarT Name
v2) = Name
v1Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
v2
    equal (LamT Name
v1) (LamT Name
v2) = Name
v1Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
v2
    equal BindingT a
_ BindingT b
_ = Bool
False

    hash :: BindingT a -> Hash
hash (VarT Name
_) = Int -> Hash
hashInt Int
0
    hash (LamT Name
_) = Int -> Hash
hashInt Int
0

instance Render BindingT
  where
    renderSym :: BindingT sig -> String
renderSym (VarT Name
v) = Binding (Full Any) -> String
forall (sym :: * -> *) sig. Render sym => sym sig -> String
renderSym (Name -> Binding (Full Any)
forall a. Name -> Binding (Full a)
Var Name
v)
    renderSym (LamT Name
v) = Binding (Any :-> Full (Any -> Any)) -> String
forall (sym :: * -> *) sig. Render sym => sym sig -> String
renderSym (Name -> Binding (Any :-> Full (Any -> Any))
forall b a. Name -> Binding (b :-> Full (a -> b))
Lam Name
v)
    renderArgs :: [String] -> BindingT sig -> String
renderArgs [String]
args (VarT Name
v) = [String] -> Binding (Full Any) -> String
forall (sym :: * -> *) sig.
Render sym =>
[String] -> sym sig -> String
renderArgs [String]
args (Name -> Binding (Full Any)
forall a. Name -> Binding (Full a)
Var Name
v)
    renderArgs [String]
args (LamT Name
v) = [String] -> Binding (Any :-> Full (Any -> Any)) -> String
forall (sym :: * -> *) sig.
Render sym =>
[String] -> sym sig -> String
renderArgs [String]
args (Name -> Binding (Any :-> Full (Any -> Any))
forall b a. Name -> Binding (b :-> Full (a -> b))
Lam Name
v)

instance StringTree BindingT
  where
    stringTreeSym :: [Tree String] -> BindingT a -> Tree String
stringTreeSym [Tree String]
args (VarT Name
v) = [Tree String] -> Binding (Full Any) -> Tree String
forall (sym :: * -> *) a.
StringTree sym =>
[Tree String] -> sym a -> Tree String
stringTreeSym [Tree String]
args (Name -> Binding (Full Any)
forall a. Name -> Binding (Full a)
Var Name
v)
    stringTreeSym [Tree String]
args (LamT Name
v) = [Tree String] -> Binding (Any :-> Full (Any -> Any)) -> Tree String
forall (sym :: * -> *) a.
StringTree sym =>
[Tree String] -> sym a -> Tree String
stringTreeSym [Tree String]
args (Name -> Binding (Any :-> Full (Any -> Any))
forall b a. Name -> Binding (b :-> Full (a -> b))
Lam Name
v)

-- | Get the highest name bound by the first 'LamT' binders at every path from the root. If the term
-- has /ordered binders/ \[1\], 'maxLamT' returns the highest name introduced in the whole term.
--
-- \[1\] Ordered binders means that the names of 'LamT' nodes are decreasing along every path from
-- the root.
maxLamT :: Project BindingT sym => AST sym a -> Name
maxLamT :: AST sym a -> Name
maxLamT (Sym sym (a :-> a)
lam :$ AST sym (Full a)
_) | Just (LamT Name
n :: BindingT (b :-> a)) <- sym (a :-> a) -> Maybe (BindingT (a :-> a))
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj sym (a :-> a)
lam = Name
n
maxLamT (AST sym (a :-> a)
s :$ AST sym (Full a)
a) = AST sym (a :-> a) -> Name
forall (sym :: * -> *) a. Project BindingT sym => AST sym a -> Name
maxLamT AST sym (a :-> a)
s Name -> Name -> Name
forall a. Ord a => a -> a -> a
`Prelude.max` AST sym (Full a) -> Name
forall (sym :: * -> *) a. Project BindingT sym => AST sym a -> Name
maxLamT AST sym (Full a)
a
maxLamT AST sym a
_ = Name
0

-- | Higher-order interface for variable binding
--
-- Assumptions:
--
--   * The body @f@ does not inspect its argument.
--
--   * Applying @f@ to a term with ordered binders results in a term with /ordered binders/ \[1\].
--
-- \[1\] Ordered binders means that the names of 'LamT' nodes are decreasing along every path from
-- the root.
--
-- See \"Using Circular Programs for Higher-Order Syntax\"
-- (ICFP 2013, <https://emilaxelsson.github.io/documents/axelsson2013using.pdf>).
lamT_template :: Project BindingT sym
    => (Name -> sym (Full a))
         -- ^ Variable symbol constructor
    -> (Name -> ASTF sym b -> ASTF sym (a -> b))
         -- ^ Lambda constructor
    -> (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lamT_template :: (Name -> sym (Full a))
-> (Name -> ASTF sym b -> ASTF sym (a -> b))
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)
lamT_template Name -> sym (Full a)
mkVar Name -> ASTF sym b -> ASTF sym (a -> b)
mkLam ASTF sym a -> ASTF sym b
f = Name -> ASTF sym b -> ASTF sym (a -> b)
mkLam Name
v ASTF sym b
body
  where
    body :: ASTF sym b
body = ASTF sym a -> ASTF sym b
f (ASTF sym a -> ASTF sym b) -> ASTF sym a -> ASTF sym b
forall a b. (a -> b) -> a -> b
$ sym (Full a) -> ASTF sym a
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (sym (Full a) -> ASTF sym a) -> sym (Full a) -> ASTF sym a
forall a b. (a -> b) -> a -> b
$ Name -> sym (Full a)
mkVar Name
v
    v :: Name
v    = Name -> Name
forall a. Enum a => a -> a
succ (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ ASTF sym b -> Name
forall (sym :: * -> *) a. Project BindingT sym => AST sym a -> Name
maxLamT ASTF sym b
body

-- | Higher-order interface for variable binding
--
-- This function is 'lamT_template' specialized to domains @sym@ satisfying
-- @(`BindingT` `:<:` sym)@.
lamT :: (BindingT :<: sym, Typeable a) =>
    (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lamT :: (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lamT = (Name -> sym (Full a))
-> (Name -> ASTF sym b -> ASTF sym (a -> b))
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)
forall (sym :: * -> *) a b.
Project BindingT sym =>
(Name -> sym (Full a))
-> (Name -> ASTF sym b -> ASTF sym (a -> b))
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)
lamT_template (BindingT (Full a) -> sym (Full a)
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (BindingT (Full a) -> sym (Full a))
-> (Name -> BindingT (Full a)) -> Name -> sym (Full a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindingT (Full a)
forall a. Typeable a => Name -> BindingT (Full a)
VarT) (\Name
v ASTF sym b
a -> sym (b :-> Full (a -> b)) -> AST sym (b :-> Full (a -> b))
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (BindingT (b :-> Full (a -> b)) -> sym (b :-> Full (a -> b))
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (Name -> BindingT (b :-> Full (a -> b))
forall a b. Typeable a => Name -> BindingT (b :-> Full (a -> b))
LamT Name
v)) AST sym (b :-> Full (a -> b)) -> ASTF sym b -> ASTF sym (a -> b)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF sym b
a)

-- | Higher-order interface for variable binding
--
-- This function is 'lamT_template' specialized to domains @sym@ satisfying
-- @(sym ~ `Typed` s, `BindingT` `:<:` s)@.
lamTyped :: (sym ~ Typed s, BindingT :<: s, Typeable a, Typeable b) =>
    (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lamTyped :: (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lamTyped = (Name -> Typed s (Full a))
-> (Name -> ASTF (Typed s) b -> ASTF (Typed s) (a -> b))
-> (ASTF (Typed s) a -> ASTF (Typed s) b)
-> ASTF (Typed s) (a -> b)
forall (sym :: * -> *) a b.
Project BindingT sym =>
(Name -> sym (Full a))
-> (Name -> ASTF sym b -> ASTF sym (a -> b))
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)
lamT_template
    (s (Full a) -> Typed s (Full a)
forall sig (sym :: * -> *).
Typeable (DenResult sig) =>
sym sig -> Typed sym sig
Typed (s (Full a) -> Typed s (Full a))
-> (Name -> s (Full a)) -> Name -> Typed s (Full a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindingT (Full a) -> s (Full a)
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (BindingT (Full a) -> s (Full a))
-> (Name -> BindingT (Full a)) -> Name -> s (Full a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindingT (Full a)
forall a. Typeable a => Name -> BindingT (Full a)
VarT)
    (\Name
v ASTF (Typed s) b
a -> Typed s (b :-> Full (a -> b))
-> AST (Typed s) (b :-> Full (a -> b))
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (s (b :-> Full (a -> b)) -> Typed s (b :-> Full (a -> b))
forall sig (sym :: * -> *).
Typeable (DenResult sig) =>
sym sig -> Typed sym sig
Typed (BindingT (b :-> Full (a -> b)) -> s (b :-> Full (a -> b))
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj (Name -> BindingT (b :-> Full (a -> b))
forall a b. Typeable a => Name -> BindingT (b :-> Full (a -> b))
LamT Name
v))) AST (Typed s) (b :-> Full (a -> b))
-> ASTF (Typed s) b -> ASTF (Typed s) (a -> b)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ ASTF (Typed s) b
a)

-- | Domains that \"might\" include variables and binders
class BindingDomain sym
  where
    prVar :: sym sig -> Maybe Name
    prLam :: sym sig -> Maybe Name

    -- | Rename a variable or a lambda (no effect for other symbols)
    renameBind :: (Name -> Name) -> sym sig -> sym sig

instance {-# OVERLAPPING #-}
         (BindingDomain sym1, BindingDomain sym2) => BindingDomain (sym1 :+: sym2)
  where
    prVar :: (:+:) sym1 sym2 sig -> Maybe Name
prVar (InjL sym1 sig
s) = sym1 sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar sym1 sig
s
    prVar (InjR sym2 sig
s) = sym2 sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar sym2 sig
s
    prLam :: (:+:) sym1 sym2 sig -> Maybe Name
prLam (InjL sym1 sig
s) = sym1 sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam sym1 sig
s
    prLam (InjR sym2 sig
s) = sym2 sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam sym2 sig
s
    renameBind :: (Name -> Name) -> (:+:) sym1 sym2 sig -> (:+:) sym1 sym2 sig
renameBind Name -> Name
re (InjL sym1 sig
s) = sym1 sig -> (:+:) sym1 sym2 sig
forall (sym1 :: * -> *) a (sym2 :: * -> *).
sym1 a -> (:+:) sym1 sym2 a
InjL (sym1 sig -> (:+:) sym1 sym2 sig)
-> sym1 sig -> (:+:) sym1 sym2 sig
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> sym1 sig -> sym1 sig
forall (sym :: * -> *) sig.
BindingDomain sym =>
(Name -> Name) -> sym sig -> sym sig
renameBind Name -> Name
re sym1 sig
s
    renameBind Name -> Name
re (InjR sym2 sig
s) = sym2 sig -> (:+:) sym1 sym2 sig
forall (sym2 :: * -> *) a (sym1 :: * -> *).
sym2 a -> (:+:) sym1 sym2 a
InjR (sym2 sig -> (:+:) sym1 sym2 sig)
-> sym2 sig -> (:+:) sym1 sym2 sig
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> sym2 sig -> sym2 sig
forall (sym :: * -> *) sig.
BindingDomain sym =>
(Name -> Name) -> sym sig -> sym sig
renameBind Name -> Name
re sym2 sig
s

instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (Typed sym)
  where
    prVar :: Typed sym sig -> Maybe Name
prVar (Typed sym sig
s) = sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar sym sig
s
    prLam :: Typed sym sig -> Maybe Name
prLam (Typed sym sig
s) = sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam sym sig
s
    renameBind :: (Name -> Name) -> Typed sym sig -> Typed sym sig
renameBind Name -> Name
re (Typed sym sig
s) = sym sig -> Typed sym sig
forall sig (sym :: * -> *).
Typeable (DenResult sig) =>
sym sig -> Typed sym sig
Typed (sym sig -> Typed sym sig) -> sym sig -> Typed sym sig
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> sym sig -> sym sig
forall (sym :: * -> *) sig.
BindingDomain sym =>
(Name -> Name) -> sym sig -> sym sig
renameBind Name -> Name
re sym sig
s

instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (sym :&: i)
  where
    prVar :: (:&:) sym i sig -> Maybe Name
prVar = sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar (sym sig -> Maybe Name)
-> ((:&:) sym i sig -> sym sig) -> (:&:) sym i sig -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) sym i sig -> sym sig
forall (expr :: * -> *) (info :: * -> *) sig.
(:&:) expr info sig -> expr sig
decorExpr
    prLam :: (:&:) sym i sig -> Maybe Name
prLam = sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam (sym sig -> Maybe Name)
-> ((:&:) sym i sig -> sym sig) -> (:&:) sym i sig -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) sym i sig -> sym sig
forall (expr :: * -> *) (info :: * -> *) sig.
(:&:) expr info sig -> expr sig
decorExpr
    renameBind :: (Name -> Name) -> (:&:) sym i sig -> (:&:) sym i sig
renameBind Name -> Name
re (sym sig
s :&: i (DenResult sig)
d) = (Name -> Name) -> sym sig -> sym sig
forall (sym :: * -> *) sig.
BindingDomain sym =>
(Name -> Name) -> sym sig -> sym sig
renameBind Name -> Name
re sym sig
s sym sig -> i (DenResult sig) -> (:&:) sym i sig
forall (expr :: * -> *) sig (info :: * -> *).
expr sig -> info (DenResult sig) -> (:&:) expr info sig
:&: i (DenResult sig)
d

instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (AST sym)
  where
    prVar :: AST sym sig -> Maybe Name
prVar (Sym sym sig
s) = sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar sym sig
s
    prVar AST sym sig
_       = Maybe Name
forall a. Maybe a
Nothing
    prLam :: AST sym sig -> Maybe Name
prLam (Sym sym sig
s) = sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam sym sig
s
    prLam AST sym sig
_       = Maybe Name
forall a. Maybe a
Nothing
    renameBind :: (Name -> Name) -> AST sym sig -> AST sym sig
renameBind Name -> Name
re (Sym sym sig
s) = sym sig -> AST sym sig
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (sym sig -> AST sym sig) -> sym sig -> AST sym sig
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> sym sig -> sym sig
forall (sym :: * -> *) sig.
BindingDomain sym =>
(Name -> Name) -> sym sig -> sym sig
renameBind Name -> Name
re sym sig
s

instance {-# OVERLAPPING #-} BindingDomain Binding
  where
    prVar :: Binding sig -> Maybe Name
prVar (Var Name
v) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
v
    prLam :: Binding sig -> Maybe Name
prLam (Lam Name
v) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
v
    renameBind :: (Name -> Name) -> Binding sig -> Binding sig
renameBind Name -> Name
re (Var Name
v) = Name -> Binding (Full a)
forall a. Name -> Binding (Full a)
Var (Name -> Binding (Full a)) -> Name -> Binding (Full a)
forall a b. (a -> b) -> a -> b
$ Name -> Name
re Name
v
    renameBind Name -> Name
re (Lam Name
v) = Name -> Binding (b :-> Full (a -> b))
forall b a. Name -> Binding (b :-> Full (a -> b))
Lam (Name -> Binding (b :-> Full (a -> b)))
-> Name -> Binding (b :-> Full (a -> b))
forall a b. (a -> b) -> a -> b
$ Name -> Name
re Name
v

instance {-# OVERLAPPING #-} BindingDomain BindingT
  where
    prVar :: BindingT sig -> Maybe Name
prVar (VarT Name
v) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
v
    prLam :: BindingT sig -> Maybe Name
prLam (LamT Name
v) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
v
    renameBind :: (Name -> Name) -> BindingT sig -> BindingT sig
renameBind Name -> Name
re (VarT Name
v) = Name -> BindingT (Full a)
forall a. Typeable a => Name -> BindingT (Full a)
VarT (Name -> BindingT (Full a)) -> Name -> BindingT (Full a)
forall a b. (a -> b) -> a -> b
$ Name -> Name
re Name
v
    renameBind Name -> Name
re (LamT Name
v) = Name -> BindingT (b :-> Full (a -> b))
forall a b. Typeable a => Name -> BindingT (b :-> Full (a -> b))
LamT (Name -> BindingT (b :-> Full (a -> b)))
-> Name -> BindingT (b :-> Full (a -> b))
forall a b. (a -> b) -> a -> b
$ Name -> Name
re Name
v

instance {-# OVERLAPPABLE #-} BindingDomain sym
  where
    prVar :: sym sig -> Maybe Name
prVar sym sig
_ = Maybe Name
forall a. Maybe a
Nothing
    prLam :: sym sig -> Maybe Name
prLam sym sig
_ = Maybe Name
forall a. Maybe a
Nothing
    renameBind :: (Name -> Name) -> sym sig -> sym sig
renameBind Name -> Name
_ sym sig
a = sym sig
a
  -- This instance seems to overlap all others on GHC 8.2.2. This leads to
  -- failures in the test suite. Removing the instance and declaring one
  -- instance per type solves the problem. Earlier and later GHC versions don't
  -- have this problem, so I assume it's a bug in 8.2.

-- | A symbol for let bindings
--
-- This symbol is just an application operator. The actual binding has to be
-- done by a lambda that constructs the second argument.
--
-- The provided string is just a tag and has nothing to do with the name of the
-- variable of the second argument (if that argument happens to be a lambda).
-- However, a back end may use the tag to give a sensible name to the generated
-- variable.
--
-- The string tag may be empty.
data Let sig
  where
    Let :: String -> Let (a :-> (a -> b) :-> Full b)

instance Symbol Let where symSig :: Let sig -> SigRep sig
symSig (Let String
_) = SigRep sig
forall sig. Signature sig => SigRep sig
signature

instance Render Let
  where
    renderSym :: Let sig -> String
renderSym (Let String
"") = String
"Let"
    renderSym (Let String
nm) = String
"Let " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm

instance Equality Let
  where
    equal :: Let a -> Let b -> Bool
equal = Let a -> Let b -> Bool
forall (sym :: * -> *) a b. Render sym => sym a -> sym b -> Bool
equalDefault
    hash :: Let a -> Hash
hash  = Let a -> Hash
forall (sym :: * -> *) a. Render sym => sym a -> Hash
hashDefault

instance StringTree Let
  where
    stringTreeSym :: [Tree String] -> Let a -> Tree String
stringTreeSym [Tree String
a, Node String
lam [Tree String
body]] Let a
letSym
        | (String
"Lam",String
v) <- Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
3 String
lam = String -> [Tree String] -> Tree String
forall a. a -> Forest a -> Tree a
Node (Let a -> String
forall (sym :: * -> *) sig. Render sym => sym sig -> String
renderSym Let a
letSym String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v) [Tree String
a,Tree String
body]
    stringTreeSym [Tree String
a,Tree String
f] Let a
letSym = String -> [Tree String] -> Tree String
forall a. a -> Forest a -> Tree a
Node (Let a -> String
forall (sym :: * -> *) sig. Render sym => sym sig -> String
renderSym Let a
letSym) [Tree String
a,Tree String
f]

-- | Monadic constructs
--
-- See \"Generic Monadic Constructs for Embedded Languages\" (Persson et al., IFL 2011
-- <https://emilaxelsson.github.io/documents/persson2011generic.pdf>).
data MONAD m sig
  where
    Return :: MONAD m (a :-> Full (m a))
    Bind   :: MONAD m (m a :-> (a -> m b) :-> Full (m b))

instance Symbol (MONAD m)
  where
    symSig :: MONAD m sig -> SigRep sig
symSig MONAD m sig
Return = SigRep sig
forall sig. Signature sig => SigRep sig
signature
    symSig MONAD m sig
Bind   = SigRep sig
forall sig. Signature sig => SigRep sig
signature

instance Render (MONAD m)
  where
    renderSym :: MONAD m sig -> String
renderSym MONAD m sig
Return = String
"return"
    renderSym MONAD m sig
Bind   = String
"(>>=)"
    renderArgs :: [String] -> MONAD m sig -> String
renderArgs = [String] -> MONAD m sig -> String
forall (sym :: * -> *) a. Render sym => [String] -> sym a -> String
renderArgsSmart

instance Equality (MONAD m)
  where
    equal :: MONAD m a -> MONAD m b -> Bool
equal = MONAD m a -> MONAD m b -> Bool
forall (sym :: * -> *) a b. Render sym => sym a -> sym b -> Bool
equalDefault
    hash :: MONAD m a -> Hash
hash  = MONAD m a -> Hash
forall (sym :: * -> *) a. Render sym => sym a -> Hash
hashDefault

instance StringTree (MONAD m)

-- | Reifiable monad
--
-- See \"Generic Monadic Constructs for Embedded Languages\" (Persson et al.,
-- IFL 2011 <https://emilaxelsson.github.io/documents/persson2011generic.pdf>).
--
-- It is advised to convert to/from 'Remon' using the 'Syntactic' instance
-- provided in the modules "Language.Syntactic.Sugar.Monad" or
-- "Language.Syntactic.Sugar.MonadT".
newtype Remon sym m a
  where
    Remon
        :: { Remon sym m a -> forall r. Typeable r => Cont (ASTF sym (m r)) a
unRemon :: forall r . Typeable r => Cont (ASTF sym (m r)) a }
        -> Remon sym m a
  deriving (a -> Remon sym m b -> Remon sym m a
(a -> b) -> Remon sym m a -> Remon sym m b
(forall a b. (a -> b) -> Remon sym m a -> Remon sym m b)
-> (forall a b. a -> Remon sym m b -> Remon sym m a)
-> Functor (Remon sym m)
forall a b. a -> Remon sym m b -> Remon sym m a
forall a b. (a -> b) -> Remon sym m a -> Remon sym m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (sym :: * -> *) (m :: * -> *) a b.
a -> Remon sym m b -> Remon sym m a
forall (sym :: * -> *) (m :: * -> *) a b.
(a -> b) -> Remon sym m a -> Remon sym m b
<$ :: a -> Remon sym m b -> Remon sym m a
$c<$ :: forall (sym :: * -> *) (m :: * -> *) a b.
a -> Remon sym m b -> Remon sym m a
fmap :: (a -> b) -> Remon sym m a -> Remon sym m b
$cfmap :: forall (sym :: * -> *) (m :: * -> *) a b.
(a -> b) -> Remon sym m a -> Remon sym m b
Functor)
  -- The `Typeable` constraint is a bit unfortunate. It's only needed when using
  -- a `Typed` domain. Since this is probably the most common case I decided to
  -- bake in `Typeable` here. A more flexible solution would be to parameterize
  -- `Remon` on the constraint.

  -- Note that `Remon` can be seen as a variant of the codensity monad:
  -- <https://hackage.haskell.org/package/kan-extensions/docs/Control-Monad-Codensity.html>

instance Applicative (Remon sym m)
  where
    pure :: a -> Remon sym m a
pure a
a  = (forall r. Typeable r => Cont (ASTF sym (m r)) a) -> Remon sym m a
forall (sym :: * -> *) (m :: * -> *) a.
(forall r. Typeable r => Cont (ASTF sym (m r)) a) -> Remon sym m a
Remon ((forall r. Typeable r => Cont (ASTF sym (m r)) a)
 -> Remon sym m a)
-> (forall r. Typeable r => Cont (ASTF sym (m r)) a)
-> Remon sym m a
forall a b. (a -> b) -> a -> b
$ a -> ContT (ASTF sym (m r)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
    Remon sym m (a -> b)
f <*> :: Remon sym m (a -> b) -> Remon sym m a -> Remon sym m b
<*> Remon sym m a
a = (forall r. Typeable r => Cont (ASTF sym (m r)) b) -> Remon sym m b
forall (sym :: * -> *) (m :: * -> *) a.
(forall r. Typeable r => Cont (ASTF sym (m r)) a) -> Remon sym m a
Remon ((forall r. Typeable r => Cont (ASTF sym (m r)) b)
 -> Remon sym m b)
-> (forall r. Typeable r => Cont (ASTF sym (m r)) b)
-> Remon sym m b
forall a b. (a -> b) -> a -> b
$ Remon sym m (a -> b)
-> forall r. Typeable r => Cont (ASTF sym (m r)) (a -> b)
forall (sym :: * -> *) (m :: * -> *) a.
Remon sym m a -> forall r. Typeable r => Cont (ASTF sym (m r)) a
unRemon Remon sym m (a -> b)
f Cont (ASTF sym (m r)) (a -> b)
-> ContT (ASTF sym (m r)) Identity a
-> ContT (ASTF sym (m r)) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Remon sym m a -> forall r. Typeable r => Cont (ASTF sym (m r)) a
forall (sym :: * -> *) (m :: * -> *) a.
Remon sym m a -> forall r. Typeable r => Cont (ASTF sym (m r)) a
unRemon Remon sym m a
a

instance Monad (Remon dom m)
  where
    return :: a -> Remon dom m a
return a
a = (forall r. Typeable r => Cont (ASTF dom (m r)) a) -> Remon dom m a
forall (sym :: * -> *) (m :: * -> *) a.
(forall r. Typeable r => Cont (ASTF sym (m r)) a) -> Remon sym m a
Remon ((forall r. Typeable r => Cont (ASTF dom (m r)) a)
 -> Remon dom m a)
-> (forall r. Typeable r => Cont (ASTF dom (m r)) a)
-> Remon dom m a
forall a b. (a -> b) -> a -> b
$ a -> ContT (ASTF dom (m r)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    Remon dom m a
ma >>= :: Remon dom m a -> (a -> Remon dom m b) -> Remon dom m b
>>= a -> Remon dom m b
f = (forall r. Typeable r => Cont (ASTF dom (m r)) b) -> Remon dom m b
forall (sym :: * -> *) (m :: * -> *) a.
(forall r. Typeable r => Cont (ASTF sym (m r)) a) -> Remon sym m a
Remon ((forall r. Typeable r => Cont (ASTF dom (m r)) b)
 -> Remon dom m b)
-> (forall r. Typeable r => Cont (ASTF dom (m r)) b)
-> Remon dom m b
forall a b. (a -> b) -> a -> b
$ Remon dom m a -> forall r. Typeable r => Cont (ASTF dom (m r)) a
forall (sym :: * -> *) (m :: * -> *) a.
Remon sym m a -> forall r. Typeable r => Cont (ASTF sym (m r)) a
unRemon Remon dom m a
ma Cont (ASTF dom (m r)) a
-> (a -> ContT (ASTF dom (m r)) Identity b)
-> ContT (ASTF dom (m r)) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> Remon dom m b -> forall r. Typeable r => Cont (ASTF dom (m r)) b
forall (sym :: * -> *) (m :: * -> *) a.
Remon sym m a -> forall r. Typeable r => Cont (ASTF sym (m r)) a
unRemon (a -> Remon dom m b
f a
a)

-- | One-layer desugaring of monadic actions
desugarMonad
    :: ( MONAD m :<: sym
       , Typeable a
       , TYPEABLE m
       )
    => Remon sym m (ASTF sym a) -> ASTF sym (m a)
desugarMonad :: Remon sym m (ASTF sym a) -> ASTF sym (m a)
desugarMonad (Remon forall r. Typeable r => Cont (ASTF sym (m r)) (ASTF sym a)
m) = (Cont (ASTF sym (m a)) (ASTF sym a)
 -> (ASTF sym a -> ASTF sym (m a)) -> ASTF sym (m a))
-> (ASTF sym a -> ASTF sym (m a))
-> Cont (ASTF sym (m a)) (ASTF sym a)
-> ASTF sym (m a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Cont (ASTF sym (m a)) (ASTF sym a)
-> (ASTF sym a -> ASTF sym (m a)) -> ASTF sym (m a)
forall r a. Cont r a -> (a -> r) -> r
runCont (MONAD m (a :-> Full (m a)) -> ASTF sym a -> ASTF sym (m a)
forall sig fi (sup :: * -> *) f (sub :: * -> *).
(Signature sig, fi ~ SmartFun sup sig, sig ~ SmartSig fi,
 sup ~ SmartSym fi, SyntacticN f fi, sub :<: sup) =>
sub sig -> f
sugarSym MONAD m (a :-> Full (m a))
forall (m :: * -> *) a. MONAD m (a :-> Full (m a))
Return) Cont (ASTF sym (m a)) (ASTF sym a)
forall r. Typeable r => Cont (ASTF sym (m r)) (ASTF sym a)
m

-- | One-layer desugaring of monadic actions
desugarMonadTyped
    :: ( MONAD m :<: s
       , sym ~ Typed s
       , Typeable a
       , TYPEABLE m
       )
    => Remon sym m (ASTF sym a) -> ASTF sym (m a)
desugarMonadTyped :: Remon sym m (ASTF sym a) -> ASTF sym (m a)
desugarMonadTyped (Remon forall r. Typeable r => Cont (ASTF sym (m r)) (ASTF sym a)
m) = (Cont (ASTF sym (m a)) (ASTF sym a)
 -> (ASTF sym a -> ASTF sym (m a)) -> ASTF sym (m a))
-> (ASTF sym a -> ASTF sym (m a))
-> Cont (ASTF sym (m a)) (ASTF sym a)
-> ASTF sym (m a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Cont (ASTF sym (m a)) (ASTF sym a)
-> (ASTF sym a -> ASTF sym (m a)) -> ASTF sym (m a)
forall r a. Cont r a -> (a -> r) -> r
runCont (MONAD m (a :-> Full (m a)) -> ASTF sym a -> ASTF sym (m a)
forall sig fi (sup :: * -> *) f (sub :: * -> *).
(Signature sig, fi ~ SmartFun (Typed sup) sig, sig ~ SmartSig fi,
 Typed sup ~ SmartSym fi, SyntacticN f fi, sub :<: sup,
 Typeable (DenResult sig)) =>
sub sig -> f
sugarSymTyped MONAD m (a :-> Full (m a))
forall (m :: * -> *) a. MONAD m (a :-> Full (m a))
Return) Cont (ASTF sym (m a)) (ASTF sym a)
forall r. Typeable r => Cont (ASTF sym (m r)) (ASTF sym a)
m



----------------------------------------------------------------------------------------------------
-- * Free and bound variables
----------------------------------------------------------------------------------------------------

-- | Get the set of free variables in an expression
freeVars :: BindingDomain sym => AST sym sig -> Set Name
freeVars :: AST sym sig -> Set Name
freeVars AST sym sig
var
    | Just Name
v <- AST sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar AST sym sig
var = Name -> Set Name
forall a. a -> Set a
Set.singleton Name
v
freeVars (AST sym (a :-> sig)
lam :$ AST sym (Full a)
body)
    | Just Name
v <- AST sym (a :-> sig) -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam AST sym (a :-> sig)
lam = Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.delete Name
v (AST sym (Full a) -> Set Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
AST sym sig -> Set Name
freeVars AST sym (Full a)
body)
freeVars (AST sym (a :-> sig)
s :$ AST sym (Full a)
a) = Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.union (AST sym (a :-> sig) -> Set Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
AST sym sig -> Set Name
freeVars AST sym (a :-> sig)
s) (AST sym (Full a) -> Set Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
AST sym sig -> Set Name
freeVars AST sym (Full a)
a)
freeVars AST sym sig
_ = Set Name
forall a. Set a
Set.empty

-- | Get the set of variables (free, bound and introduced by lambdas) in an
-- expression
allVars :: BindingDomain sym => AST sym sig -> Set Name
allVars :: AST sym sig -> Set Name
allVars AST sym sig
var
    | Just Name
v <- AST sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar AST sym sig
var = Name -> Set Name
forall a. a -> Set a
Set.singleton Name
v
allVars (AST sym (a :-> sig)
lam :$ AST sym (Full a)
body)
    | Just Name
v <- AST sym (a :-> sig) -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam AST sym (a :-> sig)
lam = Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.insert Name
v (AST sym (Full a) -> Set Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
AST sym sig -> Set Name
allVars AST sym (Full a)
body)
allVars (AST sym (a :-> sig)
s :$ AST sym (Full a)
a) = Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.union (AST sym (a :-> sig) -> Set Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
AST sym sig -> Set Name
allVars AST sym (a :-> sig)
s) (AST sym (Full a) -> Set Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
AST sym sig -> Set Name
allVars AST sym (Full a)
a)
allVars AST sym sig
_ = Set Name
forall a. Set a
Set.empty

-- | Generate an infinite list of fresh names given a list of allocated names
--
-- The argument is assumed to be sorted and not contain an infinite number of adjacent names.
freshVars :: [Name] -> [Name]
freshVars :: [Name] -> [Name]
freshVars [Name]
as = Name -> [Name] -> [Name]
forall a. (Enum a, Ord a, Num a) => a -> [a] -> [a]
go Name
0 [Name]
as
  where
    go :: a -> [a] -> [a]
go a
c [] = [a
c..]
    go a
c (a
v:[a]
as)
      | a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
v     = a
c a -> [a] -> [a]
forall a. a -> [a] -> [a]
: a -> [a] -> [a]
go (a
ca -> a -> a
forall a. Num a => a -> a -> a
+a
1) (a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as)
      | a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v    = a -> [a] -> [a]
go (a
ca -> a -> a
forall a. Num a => a -> a -> a
+a
1) [a]
as
      | Bool
otherwise = a -> [a] -> [a]
go a
c [a]
as

freshVar :: MonadState [Name] m => m Name
freshVar :: m Name
freshVar = do
    [Name]
vs <- m [Name]
forall s (m :: * -> *). MonadState s m => m s
get
    case [Name]
vs of
      Name
v:[Name]
vs' -> do
        [Name] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [Name]
vs'
        Name -> m Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
v

-- | Rename the bound variables in a term
--
-- The free variables are left untouched. The bound variables are given unique
-- names using as small names as possible. The first argument is a list of
-- reserved names. Reserved names and names of free variables are not used when
-- renaming bound variables.
renameUnique' :: forall sym a . BindingDomain sym =>
    [Name] -> ASTF sym a -> ASTF sym a
renameUnique' :: [Name] -> ASTF sym a -> ASTF sym a
renameUnique' [Name]
vs ASTF sym a
a = (State [Name] (ASTF sym a) -> [Name] -> ASTF sym a)
-> [Name] -> State [Name] (ASTF sym a) -> ASTF sym a
forall a b c. (a -> b -> c) -> b -> a -> c
flip State [Name] (ASTF sym a) -> [Name] -> ASTF sym a
forall s a. State s a -> s -> a
evalState [Name]
fs (State [Name] (ASTF sym a) -> ASTF sym a)
-> State [Name] (ASTF sym a) -> ASTF sym a
forall a b. (a -> b) -> a -> b
$ Map Name Name -> ASTF sym a -> State [Name] (ASTF sym a)
forall sig.
Map Name Name -> AST sym sig -> State [Name] (AST sym sig)
go Map Name Name
forall k a. Map k a
Map.empty ASTF sym a
a
  where
    fs :: [Name]
fs = [Name] -> [Name]
freshVars ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
Set.toAscList (ASTF sym a -> Set Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
AST sym sig -> Set Name
freeVars ASTF sym a
a Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList [Name]
vs)

    go :: Map Name Name -> AST sym sig -> State [Name] (AST sym sig)
    go :: Map Name Name -> AST sym sig -> State [Name] (AST sym sig)
go Map Name Name
env AST sym sig
var
      | Just Name
v <- AST sym sig -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar AST sym sig
var = case Name -> Map Name Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
v Map Name Name
env of
          Just Name
w -> AST sym sig -> State [Name] (AST sym sig)
forall (m :: * -> *) a. Monad m => a -> m a
return (AST sym sig -> State [Name] (AST sym sig))
-> AST sym sig -> State [Name] (AST sym sig)
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> AST sym sig -> AST sym sig
forall (sym :: * -> *) sig.
BindingDomain sym =>
(Name -> Name) -> sym sig -> sym sig
renameBind (\Name
_ -> Name
w) AST sym sig
var
          Maybe Name
_ -> AST sym sig -> State [Name] (AST sym sig)
forall (m :: * -> *) a. Monad m => a -> m a
return AST sym sig
var  -- Free variable
    go Map Name Name
env (AST sym (a :-> sig)
lam :$ AST sym (Full a)
body)
      | Just Name
v <- AST sym (a :-> sig) -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam AST sym (a :-> sig)
lam = do
          Name
w     <- StateT [Name] Identity Name
forall (m :: * -> *). MonadState [Name] m => m Name
freshVar
          AST sym (Full a)
body' <- Map Name Name
-> AST sym (Full a) -> State [Name] (AST sym (Full a))
forall sig.
Map Name Name -> AST sym sig -> State [Name] (AST sym sig)
go (Name -> Name -> Map Name Name -> Map Name Name
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
v Name
w Map Name Name
env) AST sym (Full a)
body
          AST sym sig -> State [Name] (AST sym sig)
forall (m :: * -> *) a. Monad m => a -> m a
return (AST sym sig -> State [Name] (AST sym sig))
-> AST sym sig -> State [Name] (AST sym sig)
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> AST sym (a :-> sig) -> AST sym (a :-> sig)
forall (sym :: * -> *) sig.
BindingDomain sym =>
(Name -> Name) -> sym sig -> sym sig
renameBind (\Name
_ -> Name
w) AST sym (a :-> sig)
lam AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST sym (Full a)
body'
    go Map Name Name
env (AST sym (a :-> sig)
s :$ AST sym (Full a)
a) = (AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig)
-> StateT [Name] Identity (AST sym (a :-> sig))
-> StateT [Name] Identity (AST sym (Full a))
-> State [Name] (AST sym sig)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
(:$) (Map Name Name
-> AST sym (a :-> sig)
-> StateT [Name] Identity (AST sym (a :-> sig))
forall sig.
Map Name Name -> AST sym sig -> State [Name] (AST sym sig)
go Map Name Name
env AST sym (a :-> sig)
s) (Map Name Name
-> AST sym (Full a) -> StateT [Name] Identity (AST sym (Full a))
forall sig.
Map Name Name -> AST sym sig -> State [Name] (AST sym sig)
go Map Name Name
env AST sym (Full a)
a)
    go Map Name Name
env AST sym sig
s = AST sym sig -> State [Name] (AST sym sig)
forall (m :: * -> *) a. Monad m => a -> m a
return AST sym sig
s

-- | Rename the bound variables in a term
--
-- The free variables are left untouched. The bound variables are given unique
-- names using as small names as possible. Names of free variables are not used
-- when renaming bound variables.
renameUnique :: BindingDomain sym => ASTF sym a -> ASTF sym a
renameUnique :: ASTF sym a -> ASTF sym a
renameUnique = [Name] -> ASTF sym a -> ASTF sym a
forall (sym :: * -> *) a.
BindingDomain sym =>
[Name] -> ASTF sym a -> ASTF sym a
renameUnique' []



----------------------------------------------------------------------------------------------------
-- * Alpha-equivalence
----------------------------------------------------------------------------------------------------

-- | Environment used by 'alphaEq''
type AlphaEnv = [(Name,Name)]

alphaEq' :: (Equality sym, BindingDomain sym) => AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool
alphaEq' :: AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool
alphaEq' AlphaEnv
env ASTF sym a
var1 ASTF sym b
var2
    | Just Name
v1 <- ASTF sym a -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar ASTF sym a
var1
    , Just Name
v2 <- ASTF sym b -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prVar ASTF sym b
var2
    = case (Name -> AlphaEnv -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
v1 AlphaEnv
env, Name -> AlphaEnv -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
v2 AlphaEnv
env') of
        (Maybe Name
Nothing, Maybe Name
Nothing)   -> Name
v1Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
v2  -- Free variables
        (Just Name
v2', Just Name
v1') -> Name
v1Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
v1' Bool -> Bool -> Bool
&& Name
v2Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
v2'
        (Maybe Name, Maybe Name)
_                    -> Bool
False
  where
    env' :: AlphaEnv
env' = [(Name
v2,Name
v1) | (Name
v1,Name
v2) <- AlphaEnv
env]
alphaEq' AlphaEnv
env (AST sym (a :-> Full a)
lam1 :$ AST sym (Full a)
body1) (AST sym (a :-> Full b)
lam2 :$ AST sym (Full a)
body2)
    | Just Name
v1 <- AST sym (a :-> Full a) -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam AST sym (a :-> Full a)
lam1
    , Just Name
v2 <- AST sym (a :-> Full b) -> Maybe Name
forall (sym :: * -> *) sig.
BindingDomain sym =>
sym sig -> Maybe Name
prLam AST sym (a :-> Full b)
lam2
    = AlphaEnv -> AST sym (Full a) -> AST sym (Full a) -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool
alphaEq' ((Name
v1,Name
v2)(Name, Name) -> AlphaEnv -> AlphaEnv
forall a. a -> [a] -> [a]
:AlphaEnv
env) AST sym (Full a)
body1 AST sym (Full a)
body2
alphaEq' AlphaEnv
env ASTF sym a
a ASTF sym b
b = (forall sig.
 (a ~ DenResult sig) =>
 sym sig -> Args (AST sym) sig -> Bool)
-> ASTF sym a -> Bool
forall (sym :: * -> *) a b.
(forall sig.
 (a ~ DenResult sig) =>
 sym sig -> Args (AST sym) sig -> b)
-> ASTF sym a -> b
simpleMatch (AlphaEnv -> ASTF sym b -> sym sig -> Args (AST sym) sig -> Bool
forall (sym :: * -> *) b a.
(Equality sym, BindingDomain sym) =>
AlphaEnv -> ASTF sym b -> sym a -> Args (AST sym) a -> Bool
alphaEq'' AlphaEnv
env ASTF sym b
b) ASTF sym a
a

alphaEq'' :: (Equality sym, BindingDomain sym) =>
    AlphaEnv -> ASTF sym b -> sym a -> Args (AST sym) a -> Bool
alphaEq'' :: AlphaEnv -> ASTF sym b -> sym a -> Args (AST sym) a -> Bool
alphaEq'' AlphaEnv
env ASTF sym b
b sym a
a Args (AST sym) a
aArgs = (forall sig.
 (b ~ DenResult sig) =>
 sym sig -> Args (AST sym) sig -> Bool)
-> ASTF sym b -> Bool
forall (sym :: * -> *) a b.
(forall sig.
 (a ~ DenResult sig) =>
 sym sig -> Args (AST sym) sig -> b)
-> ASTF sym a -> b
simpleMatch (AlphaEnv
-> sym a
-> Args (AST sym) a
-> sym sig
-> Args (AST sym) sig
-> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
AlphaEnv
-> sym a -> Args (AST sym) a -> sym b -> Args (AST sym) b -> Bool
alphaEq''' AlphaEnv
env sym a
a Args (AST sym) a
aArgs) ASTF sym b
b

alphaEq''' :: (Equality sym, BindingDomain sym) =>
    AlphaEnv -> sym a -> Args (AST sym) a -> sym b -> Args (AST sym) b -> Bool
alphaEq''' :: AlphaEnv
-> sym a -> Args (AST sym) a -> sym b -> Args (AST sym) b -> Bool
alphaEq''' AlphaEnv
env sym a
a Args (AST sym) a
aArgs sym b
b Args (AST sym) b
bArgs
    | sym a -> sym b -> Bool
forall (e :: * -> *) a b. Equality e => e a -> e b -> Bool
equal sym a
a sym b
b = AlphaEnv
-> AST sym (Full (DenResult a))
-> AST sym (Full (DenResult b))
-> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
AlphaEnv -> AST sym a -> AST sym b -> Bool
alphaEqChildren AlphaEnv
env AST sym (Full (DenResult a))
a' AST sym (Full (DenResult b))
b'
    | Bool
otherwise = Bool
False
  where
    a' :: AST sym (Full (DenResult a))
a' = AST sym a -> Args (AST sym) a -> AST sym (Full (DenResult a))
forall (sym :: * -> *) sig.
AST sym sig -> Args (AST sym) sig -> ASTF sym (DenResult sig)
appArgs (sym a -> AST sym a
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym sym a
forall a. HasCallStack => a
undefined) Args (AST sym) a
aArgs
    b' :: AST sym (Full (DenResult b))
b' = AST sym b -> Args (AST sym) b -> AST sym (Full (DenResult b))
forall (sym :: * -> *) sig.
AST sym sig -> Args (AST sym) sig -> ASTF sym (DenResult sig)
appArgs (sym b -> AST sym b
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym sym b
forall a. HasCallStack => a
undefined) Args (AST sym) b
bArgs

alphaEqChildren :: (Equality sym, BindingDomain sym) => AlphaEnv -> AST sym a -> AST sym b -> Bool
alphaEqChildren :: AlphaEnv -> AST sym a -> AST sym b -> Bool
alphaEqChildren AlphaEnv
_ (Sym sym a
_) (Sym sym b
_) = Bool
True
alphaEqChildren AlphaEnv
env (AST sym (a :-> a)
s :$ AST sym (Full a)
a) (AST sym (a :-> b)
t :$ AST sym (Full a)
b) = AlphaEnv -> AST sym (a :-> a) -> AST sym (a :-> b) -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
AlphaEnv -> AST sym a -> AST sym b -> Bool
alphaEqChildren AlphaEnv
env AST sym (a :-> a)
s AST sym (a :-> b)
t Bool -> Bool -> Bool
&& AlphaEnv -> AST sym (Full a) -> AST sym (Full a) -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool
alphaEq' AlphaEnv
env AST sym (Full a)
a AST sym (Full a)
b
alphaEqChildren AlphaEnv
_ AST sym a
_ AST sym b
_ = Bool
False

-- | Alpha-equivalence
alphaEq :: (Equality sym, BindingDomain sym) => ASTF sym a -> ASTF sym b -> Bool
alphaEq :: ASTF sym a -> ASTF sym b -> Bool
alphaEq = AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool
forall (sym :: * -> *) a b.
(Equality sym, BindingDomain sym) =>
AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool
alphaEq' []



----------------------------------------------------------------------------------------------------
-- * Evaluation
----------------------------------------------------------------------------------------------------

-- | Semantic function type of the given symbol signature
type family   Denotation sig
type instance Denotation (Full a)    = a
type instance Denotation (a :-> sig) = a -> Denotation sig

class Eval s
  where
    evalSym :: s sig -> Denotation sig

instance (Eval s, Eval t) => Eval (s :+: t)
  where
    evalSym :: (:+:) s t sig -> Denotation sig
evalSym (InjL s sig
s) = s sig -> Denotation sig
forall (s :: * -> *) sig. Eval s => s sig -> Denotation sig
evalSym s sig
s
    evalSym (InjR t sig
s) = t sig -> Denotation sig
forall (s :: * -> *) sig. Eval s => s sig -> Denotation sig
evalSym t sig
s

instance Eval Empty
  where
    evalSym :: Empty sig -> Denotation sig
evalSym = String -> Empty sig -> Denotation sig
forall a. HasCallStack => String -> a
error String
"evalSym: Empty"

instance Eval sym => Eval (sym :&: info)
  where
    evalSym :: (:&:) sym info sig -> Denotation sig
evalSym = sym sig -> Denotation sig
forall (s :: * -> *) sig. Eval s => s sig -> Denotation sig
evalSym (sym sig -> Denotation sig)
-> ((:&:) sym info sig -> sym sig)
-> (:&:) sym info sig
-> Denotation sig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) sym info sig -> sym sig
forall (expr :: * -> *) (info :: * -> *) sig.
(:&:) expr info sig -> expr sig
decorExpr

instance Eval Literal
  where
    evalSym :: Literal sig -> Denotation sig
evalSym (Literal a
a) = a
Denotation sig
a

instance Eval Construct
  where
    evalSym :: Construct sig -> Denotation sig
evalSym (Construct String
_ Denotation sig
d) = Denotation sig
d

instance Eval Let
  where
    evalSym :: Let sig -> Denotation sig
evalSym (Let String
_) = ((a -> b) -> a -> b) -> a -> (a -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)

instance Monad m => Eval (MONAD m)
  where
    evalSym :: MONAD m sig -> Denotation sig
evalSym MONAD m sig
Return = Denotation sig
forall (m :: * -> *) a. Monad m => a -> m a
return
    evalSym MONAD m sig
Bind   = Denotation sig
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
(>>=)

-- | Evaluation
evalDen :: Eval s => AST s sig -> Denotation sig
evalDen :: AST s sig -> Denotation sig
evalDen = AST s sig -> Denotation sig
forall (s :: * -> *) sig. Eval s => AST s sig -> Denotation sig
go
  where
    go :: Eval s => AST s sig -> Denotation sig
    go :: AST s sig -> Denotation sig
go (Sym s sig
s)  = s sig -> Denotation sig
forall (s :: * -> *) sig. Eval s => s sig -> Denotation sig
evalSym s sig
s
    go (AST s (a :-> sig)
s :$ AST s (Full a)
a) = AST s (a :-> sig) -> Denotation (a :-> sig)
forall (s :: * -> *) sig. Eval s => AST s sig -> Denotation sig
go AST s (a :-> sig)
s (a -> Denotation sig) -> a -> Denotation sig
forall a b. (a -> b) -> a -> b
$ AST s (Full a) -> Denotation (Full a)
forall (s :: * -> *) sig. Eval s => AST s sig -> Denotation sig
go AST s (Full a)
a

-- | Monadic denotation; mapping from a symbol signature
--
-- > a :-> b :-> Full c
--
-- to
--
-- > m a -> m b -> m c
type family   DenotationM (m :: * -> *) sig
type instance DenotationM m (Full a)    = m a
type instance DenotationM m (a :-> sig) = m a -> DenotationM m sig

-- | Lift a 'Denotation' to 'DenotationM'
liftDenotationM :: forall m sig proxy1 proxy2 . Monad m =>
    SigRep sig -> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig
liftDenotationM :: SigRep sig
-> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig
liftDenotationM SigRep sig
sig proxy1 m
_ proxy2 sig
_ = SigRep sig
-> (Args (WrapFull m) sig -> m (DenResult sig))
-> DenotationM m sig
forall sig'.
SigRep sig'
-> (Args (WrapFull m) sig' -> m (DenResult sig'))
-> DenotationM m sig'
help2 SigRep sig
sig ((Args (WrapFull m) sig -> m (DenResult sig)) -> DenotationM m sig)
-> (Denotation sig -> Args (WrapFull m) sig -> m (DenResult sig))
-> Denotation sig
-> DenotationM m sig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigRep sig
-> Denotation sig -> Args (WrapFull m) sig -> m (DenResult sig)
forall sig'.
Monad m =>
SigRep sig'
-> Denotation sig' -> Args (WrapFull m) sig' -> m (DenResult sig')
help1 SigRep sig
sig
  where
    help1 :: Monad m =>
        SigRep sig' -> Denotation sig' -> Args (WrapFull m) sig' -> m (DenResult sig')
    help1 :: SigRep sig'
-> Denotation sig' -> Args (WrapFull m) sig' -> m (DenResult sig')
help1 SigRep sig'
SigFull Denotation sig'
f Args (WrapFull m) sig'
_ = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
Denotation sig'
f
    help1 (SigMore SigRep sig
sig) Denotation sig'
f (WrapFull m a
ma :* Args (WrapFull m) sig
as) = do
        a
a <- m a
ma
        SigRep sig
-> Denotation sig -> Args (WrapFull m) sig -> m (DenResult sig)
forall sig'.
Monad m =>
SigRep sig'
-> Denotation sig' -> Args (WrapFull m) sig' -> m (DenResult sig')
help1 SigRep sig
sig (Denotation sig'
a -> Denotation sig
f a
a) Args (WrapFull m) sig
Args (WrapFull m) sig
as

    help2 :: SigRep sig' -> (Args (WrapFull m) sig' -> m (DenResult sig')) -> DenotationM m sig'
    help2 :: SigRep sig'
-> (Args (WrapFull m) sig' -> m (DenResult sig'))
-> DenotationM m sig'
help2 SigRep sig'
SigFull Args (WrapFull m) sig' -> m (DenResult sig')
f = Args (WrapFull m) sig' -> m (DenResult sig')
f Args (WrapFull m) sig'
forall (c :: * -> *) a. Args c (Full a)
Nil
    help2 (SigMore SigRep sig
sig) Args (WrapFull m) sig' -> m (DenResult sig')
f = \m a
a -> SigRep sig
-> (Args (WrapFull m) sig -> m (DenResult sig))
-> DenotationM m sig
forall sig'.
SigRep sig'
-> (Args (WrapFull m) sig' -> m (DenResult sig'))
-> DenotationM m sig'
help2 SigRep sig
sig (\Args (WrapFull m) sig
as -> Args (WrapFull m) sig' -> m (DenResult sig')
f (m a -> WrapFull m (Full a)
forall (c :: * -> *) a. c a -> WrapFull c (Full a)
WrapFull m a
a WrapFull m (Full a)
-> Args (WrapFull m) sig -> Args (WrapFull m) (a :-> sig)
forall (c :: * -> *) a sig.
c (Full a) -> Args c sig -> Args c (a :-> sig)
:* Args (WrapFull m) sig
as))

-- | Runtime environment
type RunEnv = [(Name, Dynamic)]
  -- TODO Use a more efficient data structure?

-- | Evaluation
class EvalEnv sym env
  where
    compileSym :: proxy env -> sym sig -> DenotationM (Reader env) sig

    default compileSym :: (Symbol sym, Eval sym) =>
        proxy env -> sym sig -> DenotationM (Reader env) sig
    compileSym proxy env
p sym sig
s = SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig
forall (proxy :: * -> *) env (sym :: * -> *) sig.
Eval sym =>
SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig
compileSymDefault (sym sig -> SigRep sig
forall (sym :: * -> *) sig. Symbol sym => sym sig -> SigRep sig
symSig sym sig
s) proxy env
p sym sig
s

-- | Simple implementation of `compileSym` from a 'Denotation'
compileSymDefault :: forall proxy env sym sig . Eval sym =>
    SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig
compileSymDefault :: SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig
compileSymDefault SigRep sig
sig proxy env
p sym sig
s = SigRep sig
-> Proxy (Reader env)
-> sym sig
-> Denotation sig
-> DenotationM (Reader env) sig
forall (m :: * -> *) sig (proxy1 :: (* -> *) -> *)
       (proxy2 :: * -> *).
Monad m =>
SigRep sig
-> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig
liftDenotationM SigRep sig
sig (Proxy (Reader env)
forall k (t :: k). Proxy t
Proxy :: Proxy (Reader env)) sym sig
s (sym sig -> Denotation sig
forall (s :: * -> *) sig. Eval s => s sig -> Denotation sig
evalSym sym sig
s)

instance (EvalEnv sym1 env, EvalEnv sym2 env) => EvalEnv (sym1 :+: sym2) env
  where
    compileSym :: proxy env -> (:+:) sym1 sym2 sig -> DenotationM (Reader env) sig
compileSym proxy env
p (InjL sym1 sig
s) = proxy env -> sym1 sig -> DenotationM (Reader env) sig
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> sym sig -> DenotationM (Reader env) sig
compileSym proxy env
p sym1 sig
s
    compileSym proxy env
p (InjR sym2 sig
s) = proxy env -> sym2 sig -> DenotationM (Reader env) sig
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> sym sig -> DenotationM (Reader env) sig
compileSym proxy env
p sym2 sig
s

instance EvalEnv Empty env
  where
    compileSym :: proxy env -> Empty sig -> DenotationM (Reader env) sig
compileSym = String -> proxy env -> Empty sig -> DenotationM (Reader env) sig
forall a. HasCallStack => String -> a
error String
"compileSym: Empty"

instance EvalEnv sym env => EvalEnv (Typed sym) env
  where
    compileSym :: proxy env -> Typed sym sig -> DenotationM (Reader env) sig
compileSym proxy env
p (Typed sym sig
s) = proxy env -> sym sig -> DenotationM (Reader env) sig
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> sym sig -> DenotationM (Reader env) sig
compileSym proxy env
p sym sig
s

instance EvalEnv sym env => EvalEnv (sym :&: info) env
  where
    compileSym :: proxy env -> (:&:) sym info sig -> DenotationM (Reader env) sig
compileSym proxy env
p = proxy env -> sym sig -> DenotationM (Reader env) sig
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> sym sig -> DenotationM (Reader env) sig
compileSym proxy env
p (sym sig -> DenotationM (Reader env) sig)
-> ((:&:) sym info sig -> sym sig)
-> (:&:) sym info sig
-> DenotationM (Reader env) sig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) sym info sig -> sym sig
forall (expr :: * -> *) (info :: * -> *) sig.
(:&:) expr info sig -> expr sig
decorExpr

instance EvalEnv Literal env

instance EvalEnv Construct env

instance EvalEnv Let env

instance Monad m => EvalEnv (MONAD m) env

instance EvalEnv BindingT RunEnv
  where
    compileSym :: proxy RunEnv -> BindingT sig -> DenotationM (Reader RunEnv) sig
compileSym proxy RunEnv
_ (VarT Name
v) = (RunEnv -> a) -> ReaderT RunEnv Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((RunEnv -> a) -> ReaderT RunEnv Identity a)
-> (RunEnv -> a) -> ReaderT RunEnv Identity a
forall a b. (a -> b) -> a -> b
$ \RunEnv
env ->
        case Name -> RunEnv -> Maybe Dynamic
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
v RunEnv
env of
          Maybe Dynamic
Nothing -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"compileSym: Variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in scope"
          Just Dynamic
d  -> case Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
            Maybe a
Nothing -> String -> a
forall a. HasCallStack => String -> a
error String
"compileSym: type error"  -- TODO Print types
            Just a
a -> a
a
    compileSym proxy RunEnv
_ (LamT Name
v) = \Reader RunEnv b
body -> (RunEnv -> a -> b) -> ReaderT RunEnv Identity (a -> b)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((RunEnv -> a -> b) -> ReaderT RunEnv Identity (a -> b))
-> (RunEnv -> a -> b) -> ReaderT RunEnv Identity (a -> b)
forall a b. (a -> b) -> a -> b
$ \RunEnv
env a
a -> Reader RunEnv b -> RunEnv -> b
forall r a. Reader r a -> r -> a
runReader Reader RunEnv b
body ((Name
v, a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
a) (Name, Dynamic) -> RunEnv -> RunEnv
forall a. a -> [a] -> [a]
: RunEnv
env)

-- | \"Compile\" a term to a Haskell function
compile :: EvalEnv sym env => proxy env -> AST sym sig -> DenotationM (Reader env) sig
compile :: proxy env -> AST sym sig -> DenotationM (Reader env) sig
compile proxy env
p (Sym sym sig
s)  = proxy env -> sym sig -> DenotationM (Reader env) sig
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> sym sig -> DenotationM (Reader env) sig
compileSym proxy env
p sym sig
s
compile proxy env
p (AST sym (a :-> sig)
s :$ AST sym (Full a)
a) = proxy env
-> AST sym (a :-> sig) -> DenotationM (Reader env) (a :-> sig)
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> AST sym sig -> DenotationM (Reader env) sig
compile proxy env
p AST sym (a :-> sig)
s (ReaderT env Identity a -> DenotationM (Reader env) sig)
-> ReaderT env Identity a -> DenotationM (Reader env) sig
forall a b. (a -> b) -> a -> b
$ proxy env -> AST sym (Full a) -> DenotationM (Reader env) (Full a)
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> AST sym sig -> DenotationM (Reader env) sig
compile proxy env
p AST sym (Full a)
a
  -- This use of the term \"compile\" comes from \"Typing Dynamic Typing\" (Baars and Swierstra,
  -- ICFP 2002, <http://doi.acm.org/10.1145/581478.581494>)

-- | Evaluation of open terms
evalOpen :: EvalEnv sym env => env -> ASTF sym a -> a
evalOpen :: env -> ASTF sym a -> a
evalOpen env
env ASTF sym a
a = Reader env a -> env -> a
forall r a. Reader r a -> r -> a
runReader (Proxy env -> ASTF sym a -> DenotationM (Reader env) (Full a)
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> AST sym sig -> DenotationM (Reader env) sig
compile Proxy env
forall k (t :: k). Proxy t
Proxy ASTF sym a
a) env
env

-- | Evaluation of closed terms where 'RunEnv' is used as the internal environment
--
-- (Note that there is no guarantee that the term is actually closed.)
evalClosed :: EvalEnv sym RunEnv => ASTF sym a -> a
evalClosed :: ASTF sym a -> a
evalClosed ASTF sym a
a = Reader RunEnv a -> RunEnv -> a
forall r a. Reader r a -> r -> a
runReader (Proxy RunEnv -> ASTF sym a -> DenotationM (Reader RunEnv) (Full a)
forall (sym :: * -> *) env (proxy :: * -> *) sig.
EvalEnv sym env =>
proxy env -> AST sym sig -> DenotationM (Reader env) sig
compile (Proxy RunEnv
forall k (t :: k). Proxy t
Proxy :: Proxy RunEnv) ASTF sym a
a) []