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

-- | Well-scoped terms

module Language.Syntactic.Functional.WellScoped where



import Control.Monad.Reader
import Data.Proxy

import Language.Syntactic
import Language.Syntactic.Functional



-- | Environment extension
class Ext ext orig
  where
    -- | Remove the extension of an environment
    unext :: ext -> orig
    -- | Return the amount by which an environment has been extended
    diff :: Num a => Proxy ext -> Proxy orig -> a

instance {-# OVERLAPS #-} Ext env env
  where
    unext :: env -> env
unext = env -> env
forall env. env -> env
id
    diff :: Proxy env -> Proxy env -> a
diff Proxy env
_ Proxy env
_ = a
0

instance {-# OVERLAPS #-} (Ext env e, ext ~ (a,env)) => Ext ext e
  where
    unext :: ext -> e
unext = env -> e
forall ext orig. Ext ext orig => ext -> orig
unext (env -> e) -> ((a, env) -> env) -> (a, env) -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, env) -> env
forall a b. (a, b) -> b
snd
    diff :: Proxy ext -> Proxy e -> a
diff Proxy ext
m Proxy e
n = Proxy env -> Proxy e -> a
forall ext orig a.
(Ext ext orig, Num a) =>
Proxy ext -> Proxy orig -> a
diff (((a, env) -> env) -> Proxy (a, env) -> Proxy env
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, env) -> env
forall a b. (a, b) -> b
snd Proxy ext
Proxy (a, env)
m) Proxy e
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1

-- | Lookup in an extended environment
lookEnv :: forall env a e . Ext env (a,e) => Proxy e -> Reader env a
lookEnv :: Proxy e -> Reader env a
lookEnv Proxy e
_ = (env -> a) -> Reader env a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((env -> a) -> Reader env a) -> (env -> a) -> Reader env a
forall a b. (a -> b) -> a -> b
$ \env
env -> let (a
a, e
_ :: e) = env -> (a, e)
forall ext orig. Ext ext orig => ext -> orig
unext env
env in a
a

-- | Well-scoped variable binding
--
-- Well-scoped terms are introduced to be able to evaluate without type casting. The implementation
-- is inspired by \"Typing Dynamic Typing\" (Baars and Swierstra, ICFP 2002,
-- <http://doi.acm.org/10.1145/581478.581494>) where expressions are represented as (essentially)
-- @`Reader` env a@ after \"compilation\". However, a major difference is that
-- \"Typing Dynamic Typing\" starts from an untyped term, and thus needs (safe) dynamic type casting
-- during compilation. In contrast, the denotational semantics of 'BindingWS' (the 'Eval' instance)
-- uses no type casting.
data BindingWS sig
  where
    VarWS :: Ext env (a,e) => Proxy e -> BindingWS (Full (Reader env a))
    LamWS :: BindingWS (Reader (a,e) b :-> Full (Reader e (a -> b)))

instance Symbol BindingWS
  where
    symSig :: BindingWS sig -> SigRep sig
symSig (VarWS Proxy e
_) = SigRep sig
forall sig. Signature sig => SigRep sig
signature
    symSig BindingWS sig
LamWS     = SigRep sig
forall sig. Signature sig => SigRep sig
signature

instance NFData1 BindingWS
  where
    rnf1 :: BindingWS a -> ()
rnf1 (VarWS Proxy e
Proxy) = ()
    rnf1 BindingWS a
LamWS         = ()

instance Eval BindingWS
  where
    evalSym :: BindingWS sig -> Denotation sig
evalSym (VarWS Proxy e
p) = Proxy e -> Reader env a
forall env a e. Ext env (a, e) => Proxy e -> Reader env a
lookEnv Proxy e
p
    evalSym BindingWS sig
LamWS     = \Reader (a, e) b
f -> (e -> a -> b) -> ReaderT e Identity (a -> b)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((e -> a -> b) -> ReaderT e Identity (a -> b))
-> (e -> a -> b) -> ReaderT e Identity (a -> b)
forall a b. (a -> b) -> a -> b
$ \e
e -> \a
a -> Reader (a, e) b -> (a, e) -> b
forall r a. Reader r a -> r -> a
runReader Reader (a, e) b
f (a
a,e
e)

-- | Higher-order interface for well-scoped variable binding
--
-- Inspired by Conor McBride's "I am not a number, I am a classy hack"
-- (<http://mazzo.li/epilogue/index.html%3Fp=773.html>).
lamWS :: forall a e sym b . (BindingWS :<: sym)
    => ((forall env . (Ext env (a,e)) => ASTF sym (Reader env a)) -> ASTF sym (Reader (a,e) b))
    -> ASTF sym (Reader e (a -> b))
lamWS :: ((forall env. Ext env (a, e) => ASTF sym (Reader env a))
 -> ASTF sym (Reader (a, e) b))
-> ASTF sym (Reader e (a -> b))
lamWS (forall env. Ext env (a, e) => ASTF sym (Reader env a))
-> ASTF sym (Reader (a, e) b)
f = BindingWS (Reader (a, e) b :-> Full (Reader e (a -> b)))
-> ASTF sym (Reader (a, e) b) -> ASTF sym (Reader e (a -> b))
forall sig f (sup :: * -> *) (sub :: * -> *).
(Signature sig, f ~ SmartFun sup sig, sig ~ SmartSig f,
 sup ~ SmartSym f, sub :<: sup) =>
sub sig -> f
smartSym BindingWS (Reader (a, e) b :-> Full (Reader e (a -> b)))
forall a e b.
BindingWS (Reader (a, e) b :-> Full (Reader e (a -> b)))
LamWS (ASTF sym (Reader (a, e) b) -> ASTF sym (Reader e (a -> b)))
-> ASTF sym (Reader (a, e) b) -> ASTF sym (Reader e (a -> b))
forall a b. (a -> b) -> a -> b
$ (forall env. Ext env (a, e) => ASTF sym (Reader env a))
-> ASTF sym (Reader (a, e) b)
f ((forall env. Ext env (a, e) => ASTF sym (Reader env a))
 -> ASTF sym (Reader (a, e) b))
-> (forall env. Ext env (a, e) => ASTF sym (Reader env a))
-> ASTF sym (Reader (a, e) b)
forall a b. (a -> b) -> a -> b
$ BindingWS (Full (Reader env a)) -> ASTF sym (Reader env a)
forall sig f (sup :: * -> *) (sub :: * -> *).
(Signature sig, f ~ SmartFun sup sig, sig ~ SmartSig f,
 sup ~ SmartSym f, sub :<: sup) =>
sub sig -> f
smartSym (Proxy e -> BindingWS (Full (Reader env a))
forall env a e.
Ext env (a, e) =>
Proxy e -> BindingWS (Full (Reader env a))
VarWS (Proxy e
forall k (t :: k). Proxy t
Proxy :: Proxy e))

-- | Evaluation of open well-scoped terms
evalOpenWS :: Eval s => env -> ASTF s (Reader env a) -> a
evalOpenWS :: env -> ASTF s (Reader env a) -> a
evalOpenWS env
e = ((env -> a) -> env -> a
forall a b. (a -> b) -> a -> b
$ env
e) ((env -> a) -> a)
-> (ASTF s (Reader env a) -> env -> a)
-> ASTF s (Reader env a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reader env a -> env -> a
forall r a. Reader r a -> r -> a
runReader (Reader env a -> env -> a)
-> (ASTF s (Reader env a) -> Reader env a)
-> ASTF s (Reader env a)
-> env
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASTF s (Reader env a) -> Reader env a
forall (s :: * -> *) sig. Eval s => AST s sig -> Denotation sig
evalDen

-- | Evaluation of closed well-scoped terms
evalClosedWS :: Eval s => ASTF s (Reader () a) -> a
evalClosedWS :: ASTF s (Reader () a) -> a
evalClosedWS = () -> ASTF s (Reader () a) -> a
forall (s :: * -> *) env a.
Eval s =>
env -> ASTF s (Reader env a) -> a
evalOpenWS ()

-- | Mapping from a symbol signature
--
-- > a :-> b :-> Full c
--
-- to
--
-- > Reader env a :-> Reader env b :-> Full (Reader env c)
type family   LiftReader env sig
type instance LiftReader env (Full a)    = Full (Reader env a)
type instance LiftReader env (a :-> sig) = Reader env a :-> LiftReader env sig

type family UnReader a
type instance UnReader (Reader e a) = a

-- | Mapping from a symbol signature
--
-- > Reader e a :-> Reader e b :-> Full (Reader e c)
--
-- to
--
-- > a :-> b :-> Full c
type family   LowerReader sig
type instance LowerReader (Full a)    = Full (UnReader a)
type instance LowerReader (a :-> sig) = UnReader a :-> LowerReader sig

-- | Wrap a symbol to give it a 'LiftReader' signature
data ReaderSym sym sig
  where
    ReaderSym
        :: ( Signature sig
           , Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig
           , LowerReader (LiftReader env sig) ~ sig
           )
        => Proxy env
        -> sym sig
        -> ReaderSym sym (LiftReader env sig)

instance Eval sym => Eval (ReaderSym sym)
  where
    evalSym :: ReaderSym sym sig -> Denotation sig
evalSym (ReaderSym (Proxy env
_ :: Proxy env) 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
forall sig. Signature sig => SigRep sig
signature Proxy (Reader env)
p sym sig
s (Denotation sig -> DenotationM (Reader env) sig)
-> Denotation sig -> DenotationM (Reader env) sig
forall a b. (a -> b) -> a -> b
$ sym sig -> Denotation sig
forall (s :: * -> *) sig. Eval s => s sig -> Denotation sig
evalSym sym sig
s
      where
        p :: Proxy (Reader env)
p = Proxy (Reader env)
forall k (t :: k). Proxy t
Proxy :: Proxy (Reader env)

-- | Well-scoped 'AST'
type WS sym env a = ASTF (BindingWS :+: ReaderSym sym) (Reader env a)

-- | Convert the representation of variables and binders from 'BindingWS' to 'Binding'. The latter
-- is easier to analyze, has a 'Render' instance, etc.
fromWS :: WS sym env a -> ASTF (Binding :+: sym) a
fromWS :: WS sym env a -> ASTF (Binding :+: sym) a
fromWS = ASTF (Binding :+: sym) a -> ASTF (Binding :+: sym) a
forall (sym :: * -> *) a.
(Binding :<: sym) =>
ASTF sym a -> ASTF sym a
fromDeBruijn (ASTF (Binding :+: sym) a -> ASTF (Binding :+: sym) a)
-> (WS sym env a -> ASTF (Binding :+: sym) a)
-> WS sym env a
-> ASTF (Binding :+: sym) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WS sym env a -> ASTF (Binding :+: sym) a
forall (sym :: * -> *) sig.
AST (BindingWS :+: ReaderSym sym) sig
-> AST (Binding :+: sym) (LowerReader sig)
go
  where
    go :: AST (BindingWS :+: ReaderSym sym) sig -> AST (Binding :+: sym) (LowerReader sig)
    go :: AST (BindingWS :+: ReaderSym sym) sig
-> AST (Binding :+: sym) (LowerReader sig)
go (Sym (InjL s :: BindingWS sig
s@(VarWS Proxy e
p)))     = (:+:) Binding sym (Full a) -> AST (Binding :+: sym) (Full a)
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (Binding (Full a) -> (:+:) Binding sym (Full a)
forall (sym1 :: * -> *) a (sym2 :: * -> *).
sym1 a -> (:+:) sym1 sym2 a
InjL (Name -> Binding (Full a)
forall a. Name -> Binding (Full a)
Var (Proxy env -> Proxy (a, e) -> Name
forall ext orig a.
(Ext ext orig, Num a) =>
Proxy ext -> Proxy orig -> a
diff (BindingWS (Full (Reader env a)) -> Proxy env
forall e' a. BindingWS (Full (Reader e' a)) -> Proxy e'
mkProxy2 BindingWS sig
BindingWS (Full (Reader env a))
s) (BindingWS (Full (Reader env a)) -> Proxy e -> Proxy (a, e)
forall e' a e.
BindingWS (Full (Reader e' a)) -> Proxy e -> Proxy (a, e)
mkProxy1 BindingWS sig
BindingWS (Full (Reader env a))
s Proxy e
p))))
      where
        mkProxy1 :: BindingWS (Full (Reader e' a)) -> Proxy e -> Proxy (a, e)
mkProxy1 = (\BindingWS (Full (Reader e' a))
_ Proxy e
_ -> Proxy (a, e)
forall k (t :: k). Proxy t
Proxy) :: BindingWS (Full (Reader e' a)) -> Proxy e -> Proxy (a,e)
        mkProxy2 :: BindingWS (Full (Reader e' a)) -> Proxy e'
mkProxy2 = (\BindingWS (Full (Reader e' a))
_ -> Proxy e'
forall k (t :: k). Proxy t
Proxy)   :: BindingWS (Full (Reader e' a)) -> Proxy e'
    go (Sym (InjL BindingWS sig
LamWS))           = (:+:) Binding sym (b :-> Full (a -> b))
-> AST (Binding :+: sym) (b :-> Full (a -> b))
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym ((:+:) Binding sym (b :-> Full (a -> b))
 -> AST (Binding :+: sym) (b :-> Full (a -> b)))
-> (:+:) Binding sym (b :-> Full (a -> b))
-> AST (Binding :+: sym) (b :-> Full (a -> b))
forall a b. (a -> b) -> a -> b
$ Binding (b :-> Full (a -> b))
-> (:+:) Binding sym (b :-> Full (a -> b))
forall (sym1 :: * -> *) a (sym2 :: * -> *).
sym1 a -> (:+:) sym1 sym2 a
InjL (Binding (b :-> Full (a -> b))
 -> (:+:) Binding sym (b :-> Full (a -> b)))
-> Binding (b :-> Full (a -> b))
-> (:+:) Binding sym (b :-> Full (a -> b))
forall a b. (a -> b) -> a -> b
$ Name -> Binding (b :-> Full (a -> b))
forall b a. Name -> Binding (b :-> Full (a -> b))
Lam (-Name
1) -- -1 since we're using De Bruijn
    go (AST (BindingWS :+: ReaderSym sym) (a :-> sig)
s :$ AST (BindingWS :+: ReaderSym sym) (Full a)
a)                     = AST (BindingWS :+: ReaderSym sym) (a :-> sig)
-> AST (Binding :+: sym) (LowerReader (a :-> sig))
forall (sym :: * -> *) sig.
AST (BindingWS :+: ReaderSym sym) sig
-> AST (Binding :+: sym) (LowerReader sig)
go AST (BindingWS :+: ReaderSym sym) (a :-> sig)
s AST (Binding :+: sym) (UnReader a :-> LowerReader sig)
-> AST (Binding :+: sym) (Full (UnReader a))
-> AST (Binding :+: sym) (LowerReader sig)
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST (BindingWS :+: ReaderSym sym) (Full a)
-> AST (Binding :+: sym) (LowerReader (Full a))
forall (sym :: * -> *) sig.
AST (BindingWS :+: ReaderSym sym) sig
-> AST (Binding :+: sym) (LowerReader sig)
go AST (BindingWS :+: ReaderSym sym) (Full a)
a
    go (Sym (InjR (ReaderSym Proxy env
_ sym sig
s))) = (:+:) Binding sym sig -> AST (Binding :+: sym) sig
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym ((:+:) Binding sym sig -> AST (Binding :+: sym) sig)
-> (:+:) Binding sym sig -> AST (Binding :+: sym) sig
forall a b. (a -> b) -> a -> b
$ sym sig -> (:+:) Binding sym sig
forall (sym2 :: * -> *) a (sym1 :: * -> *).
sym2 a -> (:+:) sym1 sym2 a
InjR sym sig
s

-- | Make a smart constructor for well-scoped terms. 'smartWS' has any type of the form:
--
-- > smartWS :: (sub :<: sup, bsym ~ (BindingWS :+: ReaderSym sup))
-- >     => sub (a :-> b :-> ... :-> Full x)
-- >     -> ASTF bsym (Reader env a) -> ASTF bsym (Reader env b) -> ... -> ASTF bsym (Reader env x)
smartWS :: forall sig sig' bsym f sub sup env a
    .  ( Signature sig
       , Signature sig'
       , sub :<: sup
       , bsym ~ (BindingWS :+: ReaderSym sup)
       , f    ~ SmartFun bsym sig'
       , sig' ~ SmartSig f
       , bsym ~ SmartSym f
       , sig' ~ LiftReader env sig
       , Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig
       , LowerReader (LiftReader env sig) ~ sig
       , Reader env a ~ DenResult sig'
       )
    => sub sig -> f
smartWS :: sub sig -> f
smartWS sub sig
s = (:+:) BindingWS (ReaderSym sup) sig' -> f
forall sig f (sym :: * -> *).
(Signature sig, f ~ SmartFun sym sig, sig ~ SmartSig f,
 sym ~ SmartSym f) =>
sym sig -> f
smartSym' ((:+:) BindingWS (ReaderSym sup) sig' -> f)
-> (:+:) BindingWS (ReaderSym sup) sig' -> f
forall a b. (a -> b) -> a -> b
$ ReaderSym sup sig' -> (:+:) BindingWS (ReaderSym sup) sig'
forall (sym2 :: * -> *) a (sym1 :: * -> *).
sym2 a -> (:+:) sym1 sym2 a
InjR (ReaderSym sup sig' -> (:+:) BindingWS (ReaderSym sup) sig')
-> ReaderSym sup sig' -> (:+:) BindingWS (ReaderSym sup) sig'
forall a b. (a -> b) -> a -> b
$ Proxy env -> sup sig -> ReaderSym sup (LiftReader env sig)
forall sig env (sym :: * -> *).
(Signature sig,
 Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig,
 LowerReader (LiftReader env sig) ~ sig) =>
Proxy env -> sym sig -> ReaderSym sym (LiftReader env sig)
ReaderSym (Proxy env
forall k (t :: k). Proxy t
Proxy :: Proxy env) (sup sig -> ReaderSym sup (LiftReader env sig))
-> sup sig -> ReaderSym sup (LiftReader env sig)
forall a b. (a -> b) -> a -> b
$ sub sig -> sup sig
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj sub sig
s