{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# OPTIONS_GHC -Wno-orphans #-}
-- | 'Binary' instances for the scope-safe syntax: the wire view of a term
-- is the term itself, raw ids and all.
--
-- The instances are deliberately orphans in a module of their own, so that
-- they are opt-in: importing this module is what brings them into scope,
-- and nothing else in the library does. (The dependency this costs is
-- @binary@, a GHC boot library.)
--
-- Note that decoding /mints/ scope evidence: a 'Foil.Name' comes back at
-- whatever scope index the context asks for, and the existential scope
-- under a binder is chosen arbitrarily. Thus the instances are a trust
-- boundary, in the sense of 'Control.Monad.Foil.Blocks.checkExtScope'. The
-- bytes are meaningful only under the discipline of the layer that wrote
-- them, and that layer is expected to validate what it can on the way in.
-- In particular, it should resolve the references it made
-- world-independent, and check that the names it left verbatim lie where its
-- allocation policy says. "Control.Monad.Free.Foil.Artifact" supplies those
-- checks.
module Control.Monad.Free.Foil.Binary () where

import           Data.Binary                 (Binary (..))
import           Data.Binary.Get             (Get, getWord8)
import           Data.Binary.Put             (putWord8)

import           Control.Monad.Foil.Internal
import           Control.Monad.Free.Foil     (AST (..), ScopedAST (..))

-- | The raw id and nothing else. See the module documentation for what
-- decoding trusts.
instance Binary (Name n) where
  put :: Name n -> Put
put (UnsafeName RawName
raw) = RawName -> Put
forall t. Binary t => t -> Put
put RawName
raw
  get :: Get (Name n)
get = RawName -> Name n
forall (n :: S). RawName -> Name n
UnsafeName (RawName -> Name n) -> Get RawName -> Get (Name n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get RawName
forall t. Binary t => Get t
get

-- | See the 'Binary' instance of 'Name'.
instance Binary (NameBinder n l) where
  put :: NameBinder n l -> Put
put (UnsafeNameBinder Name l
name) = Name l -> Put
forall t. Binary t => t -> Put
put Name l
name
  get :: Get (NameBinder n l)
get = Name l -> NameBinder n l
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder (Name l -> NameBinder n l) -> Get (Name l) -> Get (NameBinder n l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (Name l)
forall t. Binary t => Get t
get

-- | The two bounds. A range carries no scope index, so nothing is minted:
-- this instance is layout metadata for the serialising layer.
instance Binary NameRange where
  put :: NameRange -> Put
put (NameRange RawName
lo RawName
hi) = RawName -> Put
forall t. Binary t => t -> Put
put RawName
lo Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> RawName -> Put
forall t. Binary t => t -> Put
put RawName
hi
  get :: Get NameRange
get = RawName -> RawName -> NameRange
NameRange (RawName -> RawName -> NameRange)
-> Get RawName -> Get (RawName -> NameRange)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get RawName
forall t. Binary t => Get t
get Get (RawName -> NameRange) -> Get RawName -> Get NameRange
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get RawName
forall t. Binary t => Get t
get

-- | The binder and the body, one after the other. Decoding mints the scope
-- under the binder. See the module documentation.
instance (forall x y. Binary (binder x y), forall l. Binary (AST binder sig l))
    => Binary (ScopedAST binder sig n) where
  put :: ScopedAST binder sig n -> Put
put (ScopedAST binder n l
binder AST binder sig l
body) = binder n l -> Put
forall t. Binary t => t -> Put
put binder n l
binder Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> AST binder sig l -> Put
forall t. Binary t => t -> Put
put AST binder sig l
body
  get :: Get (ScopedAST binder sig n)
get = do
    binder <- Get (binder n n)
forall t. Binary t => Get t
get :: Get (binder n n)
    body <- get
    pure (ScopedAST binder body)

-- | A tag byte, then the name or the node.
instance ( forall x y. Binary (binder x y)
         , forall scope term. (Binary scope, Binary term) => Binary (sig scope term)
         ) => Binary (AST binder sig n) where
  put :: AST binder sig n -> Put
put (Var Name n
x)     = Word8 -> Put
putWord8 Word8
0 Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> Name n -> Put
forall t. Binary t => t -> Put
put Name n
x
  put (Node sig (ScopedAST binder sig n) (AST binder sig n)
node) = Word8 -> Put
putWord8 Word8
1 Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> sig (ScopedAST binder sig n) (AST binder sig n) -> Put
forall t. Binary t => t -> Put
put sig (ScopedAST binder sig n) (AST binder sig n)
node
  get :: Get (AST binder sig n)
get = Get Word8
getWord8 Get Word8
-> (Word8 -> Get (AST binder sig n)) -> Get (AST binder sig n)
forall a b. Get a -> (a -> Get b) -> Get b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Word8
0   -> Name n -> AST binder sig n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (Name n -> AST binder sig n)
-> Get (Name n) -> Get (AST binder sig n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (Name n)
forall t. Binary t => Get t
get
    Word8
1   -> sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node (sig (ScopedAST binder sig n) (AST binder sig n)
 -> AST binder sig n)
-> Get (sig (ScopedAST binder sig n) (AST binder sig n))
-> Get (AST binder sig n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (sig (ScopedAST binder sig n) (AST binder sig n))
forall t. Binary t => Get t
get
    Word8
tag -> String -> Get (AST binder sig n)
forall a. String -> Get a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"unknown AST tag " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Word8 -> String
forall a. Show a => a -> String
show Word8
tag)