{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- | Serialisation support for checked units: stored terms, spelling tables,
-- name-range metadata, and relocation.
--
-- The machinery here assumes only that a unit's /interned constants/ and its
-- /locals/ (the names its binders bind) occupy disjoint name ranges, and it
-- checks that assumption from the recorded metadata rather than taking it on
-- faith. A stored term is then meaningful verbatim: a local keeps its raw id,
-- and a constant is resolved through a spelling table on load.
--
-- One policy that provides the disjointness globally and by construction is
-- to keep constants below zero and locals at or above, which is what the
-- guarded successor allocator protects.
--
-- What loading trusts, and what it checks, is the client's decision, and the
-- functions here supply the checkable facts. 'checkStoredLayout' judges the
-- recorded ranges and 'constantRelocation' judges the constants, both from
-- metadata alone, so no stored term is ever walked for checking. Only
-- 'relocateConstants' walks a term, and only when a constant actually moved.
module Control.Monad.Free.Foil.Artifact (
  -- * Errors
  ArtifactError (..),
  prettyArtifactError,
  -- * Stored terms
  StoredTerm (..),
  storeTerm,
  decodeStored,
  -- * Spelling tables and locals
  termSpellings,
  localsOf,
  spanOfNames,
  -- * Range metadata and its checks
  StoredLayout (..),
  nameRangeSize,
  nameRangeContains,
  nameRangesOverlap,
  checkStoredLayout,
  -- * Relocation
  constantRelocation,
  relocateConstants,
) where

import           Data.Binary                    (Binary, get)
import qualified Data.Binary                    as Binary
import           Data.Binary.Get                (runGetOrFail)
import           Data.Bifoldable                (Bifoldable, bifoldMap)
import           Data.Bifunctor                 (Bifunctor, bimap)
import qualified Data.ByteString.Lazy           as BSL
import qualified Data.IntMap                    as IntMap
import qualified Data.IntSet                    as IntSet
import           Data.Map                       (Map)
import qualified Data.Map                       as Map
import           GHC.Generics                   (Generic)
import           Unsafe.Coerce                  (unsafeCoerce)

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

-- $setup
-- >>> import Control.Monad.Foil (NameRange (..))
-- >>> import qualified Data.Map as Map

-- * Errors

-- | What the machinery here can report. The type is parametric in the
-- spelling, as the tables are, and a 'Functor' over it.
--
-- @since 0.4.0
data ArtifactError ident
  = MalformedStoredTerm String
      -- ^ The bytes did not decode. The message is the decoder's.
  | OverlappingRegions NameRange NameRange
      -- ^ The recorded constants and locals ranges share a name.
  | SpellingForLocal RawName
      -- ^ The spelling table names something inside the locals region.
  | WrongDeclarationCount NameRange Int
      -- ^ The constants range does not hold one name per declaration.
  | UnknownConstant ident
      -- ^ A spelling the loading world does not know.
  | ConstantAmongLocals ident RawName
      -- ^ A relocation target inside the locals region, where the verbatim
      -- locals could capture it.
  deriving (ArtifactError ident -> ArtifactError ident -> Bool
(ArtifactError ident -> ArtifactError ident -> Bool)
-> (ArtifactError ident -> ArtifactError ident -> Bool)
-> Eq (ArtifactError ident)
forall ident.
Eq ident =>
ArtifactError ident -> ArtifactError ident -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall ident.
Eq ident =>
ArtifactError ident -> ArtifactError ident -> Bool
== :: ArtifactError ident -> ArtifactError ident -> Bool
$c/= :: forall ident.
Eq ident =>
ArtifactError ident -> ArtifactError ident -> Bool
/= :: ArtifactError ident -> ArtifactError ident -> Bool
Eq, RawName -> ArtifactError ident -> ShowS
[ArtifactError ident] -> ShowS
ArtifactError ident -> String
(RawName -> ArtifactError ident -> ShowS)
-> (ArtifactError ident -> String)
-> ([ArtifactError ident] -> ShowS)
-> Show (ArtifactError ident)
forall ident. Show ident => RawName -> ArtifactError ident -> ShowS
forall ident. Show ident => [ArtifactError ident] -> ShowS
forall ident. Show ident => ArtifactError ident -> String
forall a.
(RawName -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall ident. Show ident => RawName -> ArtifactError ident -> ShowS
showsPrec :: RawName -> ArtifactError ident -> ShowS
$cshow :: forall ident. Show ident => ArtifactError ident -> String
show :: ArtifactError ident -> String
$cshowList :: forall ident. Show ident => [ArtifactError ident] -> ShowS
showList :: [ArtifactError ident] -> ShowS
Show, (forall a b. (a -> b) -> ArtifactError a -> ArtifactError b)
-> (forall a b. a -> ArtifactError b -> ArtifactError a)
-> Functor ArtifactError
forall a b. a -> ArtifactError b -> ArtifactError a
forall a b. (a -> b) -> ArtifactError a -> ArtifactError b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ArtifactError a -> ArtifactError b
fmap :: forall a b. (a -> b) -> ArtifactError a -> ArtifactError b
$c<$ :: forall a b. a -> ArtifactError b -> ArtifactError a
<$ :: forall a b. a -> ArtifactError b -> ArtifactError a
Functor)

-- | Render an error, given a renderer for the spellings.
--
-- @since 0.4.0
prettyArtifactError :: (ident -> String) -> ArtifactError ident -> String
prettyArtifactError :: forall ident. (ident -> String) -> ArtifactError ident -> String
prettyArtifactError ident -> String
prettyIdent = \case
  MalformedStoredTerm String
msg -> String
"malformed stored term: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg
  OverlappingRegions NameRange
_ NameRange
_ -> String
"the constants and locals regions overlap"
  SpellingForLocal RawName
i -> String
"a spelling for local " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RawName -> String
forall a. Show a => a -> String
show RawName
i
  WrongDeclarationCount NameRange
range RawName
count ->
    String
"the constants range holds " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RawName -> String
forall a. Show a => a -> String
show (NameRange -> RawName
nameRangeSize NameRange
range)
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" names for " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RawName -> String
forall a. Show a => a -> String
show RawName
count String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" declarations"
  UnknownConstant ident
x -> String
"not in scope: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ident -> String
prettyIdent ident
x
  ConstantAmongLocals ident
x RawName
_ ->
    String
"constant " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ident -> String
prettyIdent ident
x String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" would land in the locals region"

-- * Stored terms

-- | A term as stored: canonical bytes. Equality of stored terms is byte
-- equality, which is what a canonical-artifact property tests.
--
-- @since 0.4.0
newtype StoredTerm = StoredTerm { StoredTerm -> ByteString
storedBytes :: BSL.ByteString }
  deriving (StoredTerm -> StoredTerm -> Bool
(StoredTerm -> StoredTerm -> Bool)
-> (StoredTerm -> StoredTerm -> Bool) -> Eq StoredTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StoredTerm -> StoredTerm -> Bool
== :: StoredTerm -> StoredTerm -> Bool
$c/= :: StoredTerm -> StoredTerm -> Bool
/= :: StoredTerm -> StoredTerm -> Bool
Eq, RawName -> StoredTerm -> ShowS
[StoredTerm] -> ShowS
StoredTerm -> String
(RawName -> StoredTerm -> ShowS)
-> (StoredTerm -> String)
-> ([StoredTerm] -> ShowS)
-> Show StoredTerm
forall a.
(RawName -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: RawName -> StoredTerm -> ShowS
showsPrec :: RawName -> StoredTerm -> ShowS
$cshow :: StoredTerm -> String
show :: StoredTerm -> String
$cshowList :: [StoredTerm] -> ShowS
showList :: [StoredTerm] -> ShowS
Show, (forall x. StoredTerm -> Rep StoredTerm x)
-> (forall x. Rep StoredTerm x -> StoredTerm) -> Generic StoredTerm
forall x. Rep StoredTerm x -> StoredTerm
forall x. StoredTerm -> Rep StoredTerm x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. StoredTerm -> Rep StoredTerm x
from :: forall x. StoredTerm -> Rep StoredTerm x
$cto :: forall x. Rep StoredTerm x -> StoredTerm
to :: forall x. Rep StoredTerm x -> StoredTerm
Generic, Get StoredTerm
[StoredTerm] -> Put
StoredTerm -> Put
(StoredTerm -> Put)
-> Get StoredTerm -> ([StoredTerm] -> Put) -> Binary StoredTerm
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
$cput :: StoredTerm -> Put
put :: StoredTerm -> Put
$cget :: Get StoredTerm
get :: Get StoredTerm
$cputList :: [StoredTerm] -> Put
putList :: [StoredTerm] -> Put
Binary)

-- | Store a term verbatim, through the instances of
-- "Control.Monad.Free.Foil.Binary".
--
-- The disjoint layout is what makes verbatim enough. A constant's spelling
-- goes into the unit's table ('termSpellings'), and a local needs no
-- table: its id is expected to be canonical, which it is when elaboration
-- allocates locals in a region of their own.
--
-- @since 0.4.0
storeTerm :: Binary (AST binder sig n) => AST binder sig n -> StoredTerm
storeTerm :: forall (binder :: S -> S -> *) (sig :: * -> * -> *) (n :: S).
Binary (AST binder sig n) =>
AST binder sig n -> StoredTerm
storeTerm = ByteString -> StoredTerm
StoredTerm (ByteString -> StoredTerm)
-> (AST binder sig n -> ByteString)
-> AST binder sig n
-> StoredTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST binder sig n -> ByteString
forall a. Binary a => a -> ByteString
Binary.encode

-- | Decode a stored term's bytes: the instances alone, no meaning yet.
-- Meaning is given per unit, by 'constantRelocation' and
-- 'relocateConstants'.
--
-- @since 0.4.0
decodeStored
  :: Binary (AST binder sig n)
  => StoredTerm -> Either (ArtifactError ident) (AST binder sig n)
decodeStored :: forall (binder :: S -> S -> *) (sig :: * -> * -> *) (n :: S) ident.
Binary (AST binder sig n) =>
StoredTerm -> Either (ArtifactError ident) (AST binder sig n)
decodeStored (StoredTerm ByteString
bytes) =
  case Get (AST binder sig n)
-> ByteString
-> Either
     (ByteString, ByteOffset, String)
     (ByteString, ByteOffset, AST binder sig n)
forall a.
Get a
-> ByteString
-> Either
     (ByteString, ByteOffset, String) (ByteString, ByteOffset, a)
runGetOrFail Get (AST binder sig n)
forall t. Binary t => Get t
get ByteString
bytes of
    Left (ByteString
_, ByteOffset
_, String
err) -> ArtifactError ident
-> Either (ArtifactError ident) (AST binder sig n)
forall a b. a -> Either a b
Left (String -> ArtifactError ident
forall ident. String -> ArtifactError ident
MalformedStoredTerm String
err)
    Right (ByteString
rest, ByteOffset
_, AST binder sig n
term)
      | Bool -> Bool
not (ByteString -> Bool
BSL.null ByteString
rest) -> ArtifactError ident
-> Either (ArtifactError ident) (AST binder sig n)
forall a b. a -> Either a b
Left (String -> ArtifactError ident
forall ident. String -> ArtifactError ident
MalformedStoredTerm String
"trailing bytes")
      | Bool
otherwise -> AST binder sig n -> Either (ArtifactError ident) (AST binder sig n)
forall a b. b -> Either a b
Right AST binder sig n
term

-- * Spelling tables and locals

-- | The spelling-table entries a term needs. Its free variables are exactly
-- its constants, provided the stored declaration is closed over everything
-- local. Each is mapped to its spelling from the display table.
--
-- Note that the table should cover the referenced constants and only
-- those. A table of everything in scope would let an unused import dirty a
-- dependant's content hash, and would differ between build schedules.
--
-- @since 0.4.0
termSpellings
  :: (Distinct n, CoSinkable binder, Bifoldable sig)
  => NameMap n ident      -- ^ Spellings of the top-level names.
  -> AST binder sig n
  -> Map RawName ident
termSpellings :: forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *) ident.
(Distinct n, CoSinkable binder, Bifoldable sig) =>
NameMap n ident -> AST binder sig n -> Map RawName ident
termSpellings NameMap n ident
display AST binder sig n
t = [(RawName, ident)] -> Map RawName ident
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  [ (Name n -> RawName
forall (l :: S). Name l -> RawName
nameId Name n
x, Name n -> NameMap n ident -> ident
forall (n :: S) a. Name n -> NameMap n a -> a
lookupName Name n
x NameMap n ident
display)
  | Name n
x <- NameSet n -> [Name n]
forall (n :: S). NameSet n -> [Name n]
nameSetToList (AST binder sig n -> NameSet n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> NameSet n
supportOf AST binder sig n
t)
  ]

-- | The names a term's binders bind: what a unit's locals range covers.
-- Note that 'supportOf' cannot see them, since they are bound and not free.
--
-- @since 0.4.0
localsOf
  :: (Bifoldable sig, HasNameBinders binder)
  => AST binder sig n -> [RawName]
localsOf :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
(Bifoldable sig, HasNameBinders binder) =>
AST binder sig n -> [RawName]
localsOf = \case
  Var Name n
_    -> []
  Node sig (ScopedAST binder sig n) (AST binder sig n)
sig -> (ScopedAST binder sig n -> [RawName])
-> (AST binder sig n -> [RawName])
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> [RawName]
forall m a b. Monoid m => (a -> m) -> (b -> m) -> sig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap ScopedAST binder sig n -> [RawName]
forall {binder :: S -> S -> *} {sig :: * -> * -> *} {n :: S}.
(HasNameBinders binder, Bifoldable sig) =>
ScopedAST binder sig n -> [RawName]
scopedLocals AST binder sig n -> [RawName]
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
(Bifoldable sig, HasNameBinders binder) =>
AST binder sig n -> [RawName]
localsOf sig (ScopedAST binder sig n) (AST binder sig n)
sig
  where
    scopedLocals :: ScopedAST binder sig n -> [RawName]
scopedLocals (ScopedAST binder n l
pat AST binder sig l
body) =
      binder n l -> [RawName]
forall {f :: S -> S -> *} {n :: S} {l :: S}.
HasNameBinders f =>
f n l -> [RawName]
binderNames binder n l
pat [RawName] -> [RawName] -> [RawName]
forall a. Semigroup a => a -> a -> a
<> AST binder sig l -> [RawName]
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
(Bifoldable sig, HasNameBinders binder) =>
AST binder sig n -> [RawName]
localsOf AST binder sig l
body
    binderNames :: f n l -> [RawName]
binderNames f n l
pat = case f n l -> NameBinders n l
forall (n :: S) (l :: S). f n l -> NameBinders n l
forall (f :: S -> S -> *) (n :: S) (l :: S).
HasNameBinders f =>
f n l -> NameBinders n l
getNameBinders f n l
pat of
      UnsafeNameBinders IntSet
ids -> IntSet -> [RawName]
IntSet.toList IntSet
ids

-- | The tightest range covering the given names, or 'Nothing' for none.
-- The caller picks its own convention for the empty range.
--
-- >>> spanOfNames [7, 3, 5]
-- Just (NameRange {nameRangeLo = 3, nameRangeHi = 7})
--
-- @since 0.4.0
spanOfNames :: [RawName] -> Maybe NameRange
spanOfNames :: [RawName] -> Maybe NameRange
spanOfNames [] = Maybe NameRange
forall a. Maybe a
Nothing
spanOfNames [RawName]
ids = NameRange -> Maybe NameRange
forall a. a -> Maybe a
Just (RawName -> RawName -> NameRange
NameRange ([RawName] -> RawName
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [RawName]
ids) ([RawName] -> RawName
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [RawName]
ids))

-- * Range metadata and its checks

-- | A unit's recorded name layout: the actual names of its own constants, and
-- of its locals. The two travel together, so that they cannot be mixed up with
-- the ranges of the loading world. An artifact records them as one field, and
-- the checks and the relocation consume them as one value.
--
-- @since 0.4.0
data StoredLayout = StoredLayout
  { StoredLayout -> NameRange
storedConstants :: NameRange
  , StoredLayout -> NameRange
storedLocals    :: NameRange
  }
  deriving (StoredLayout -> StoredLayout -> Bool
(StoredLayout -> StoredLayout -> Bool)
-> (StoredLayout -> StoredLayout -> Bool) -> Eq StoredLayout
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StoredLayout -> StoredLayout -> Bool
== :: StoredLayout -> StoredLayout -> Bool
$c/= :: StoredLayout -> StoredLayout -> Bool
/= :: StoredLayout -> StoredLayout -> Bool
Eq, RawName -> StoredLayout -> ShowS
[StoredLayout] -> ShowS
StoredLayout -> String
(RawName -> StoredLayout -> ShowS)
-> (StoredLayout -> String)
-> ([StoredLayout] -> ShowS)
-> Show StoredLayout
forall a.
(RawName -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: RawName -> StoredLayout -> ShowS
showsPrec :: RawName -> StoredLayout -> ShowS
$cshow :: StoredLayout -> String
show :: StoredLayout -> String
$cshowList :: [StoredLayout] -> ShowS
showList :: [StoredLayout] -> ShowS
Show, (forall x. StoredLayout -> Rep StoredLayout x)
-> (forall x. Rep StoredLayout x -> StoredLayout)
-> Generic StoredLayout
forall x. Rep StoredLayout x -> StoredLayout
forall x. StoredLayout -> Rep StoredLayout x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. StoredLayout -> Rep StoredLayout x
from :: forall x. StoredLayout -> Rep StoredLayout x
$cto :: forall x. Rep StoredLayout x -> StoredLayout
to :: forall x. Rep StoredLayout x -> StoredLayout
Generic, Get StoredLayout
[StoredLayout] -> Put
StoredLayout -> Put
(StoredLayout -> Put)
-> Get StoredLayout
-> ([StoredLayout] -> Put)
-> Binary StoredLayout
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
$cput :: StoredLayout -> Put
put :: StoredLayout -> Put
$cget :: Get StoredLayout
get :: Get StoredLayout
$cputList :: [StoredLayout] -> Put
putList :: [StoredLayout] -> Put
Binary)

-- | How many names a range holds.
--
-- >>> nameRangeSize (NameRange 3 5)
-- 3
--
-- @since 0.4.0
nameRangeSize :: NameRange -> Int
nameRangeSize :: NameRange -> RawName
nameRangeSize (NameRange RawName
lo RawName
hi) = RawName -> RawName -> RawName
forall a. Ord a => a -> a -> a
max RawName
0 (RawName
hi RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
- RawName
lo RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
+ RawName
1)

-- | Whether a raw name lies in a range.
--
-- @since 0.4.0
nameRangeContains :: NameRange -> RawName -> Bool
nameRangeContains :: NameRange -> RawName -> Bool
nameRangeContains (NameRange RawName
lo RawName
hi) RawName
i = RawName
lo RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
i Bool -> Bool -> Bool
&& RawName
i RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi

-- | Whether two ranges share a name. An empty range overlaps nothing.
--
-- >>> nameRangesOverlap (NameRange 0 4) (NameRange 4 9)
-- True
-- >>> nameRangesOverlap (NameRange 0 4) (NameRange 5 9)
-- False
--
-- @since 0.4.0
nameRangesOverlap :: NameRange -> NameRange -> Bool
nameRangesOverlap :: NameRange -> NameRange -> Bool
nameRangesOverlap (NameRange RawName
lo1 RawName
hi1) (NameRange RawName
lo2 RawName
hi2) =
  RawName
lo1 RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi1 Bool -> Bool -> Bool
&& RawName
lo2 RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi2 Bool -> Bool -> Bool
&& RawName
lo1 RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi2 Bool -> Bool -> Bool
&& RawName
lo2 RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi1

-- | The checks a unit's recorded layout admits, judged from metadata alone.
-- The constants and locals ranges must not overlap, no spelling may be
-- recorded for a local, and the constants range must hold exactly one name
-- per declaration, since allocation is dense from the range's low end.
--
-- >>> layout = StoredLayout (NameRange (-10) (-9)) (NameRange 0 5)
-- >>> checkStoredLayout layout (Map.fromList [(-20, "P.base")]) 2
-- Right ()
-- >>> checkStoredLayout layout (Map.fromList [(3, "q")]) 2
-- Left (SpellingForLocal 3)
--
-- @since 0.4.0
checkStoredLayout
  :: StoredLayout         -- ^ The unit's recorded layout.
  -> Map RawName ident    -- ^ Its spelling table.
  -> Int                  -- ^ Its declaration count.
  -> Either (ArtifactError ident) ()
checkStoredLayout :: forall ident.
StoredLayout
-> Map RawName ident -> RawName -> Either (ArtifactError ident) ()
checkStoredLayout (StoredLayout NameRange
constants NameRange
locals) Map RawName ident
table RawName
declCount
  | NameRange -> NameRange -> Bool
nameRangesOverlap NameRange
constants NameRange
locals =
      ArtifactError ident -> Either (ArtifactError ident) ()
forall a b. a -> Either a b
Left (NameRange -> NameRange -> ArtifactError ident
forall ident. NameRange -> NameRange -> ArtifactError ident
OverlappingRegions NameRange
constants NameRange
locals)
  | (RawName
i : [RawName]
_) <- (RawName -> Bool) -> [RawName] -> [RawName]
forall a. (a -> Bool) -> [a] -> [a]
filter (NameRange -> RawName -> Bool
nameRangeContains NameRange
locals) (Map RawName ident -> [RawName]
forall k a. Map k a -> [k]
Map.keys Map RawName ident
table) =
      ArtifactError ident -> Either (ArtifactError ident) ()
forall a b. a -> Either a b
Left (RawName -> ArtifactError ident
forall ident. RawName -> ArtifactError ident
SpellingForLocal RawName
i)
  | NameRange -> RawName
nameRangeSize NameRange
constants RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
/= RawName
declCount =
      ArtifactError ident -> Either (ArtifactError ident) ()
forall a b. a -> Either a b
Left (NameRange -> RawName -> ArtifactError ident
forall ident. NameRange -> RawName -> ArtifactError ident
WrongDeclarationCount NameRange
constants RawName
declCount)
  | Bool
otherwise = () -> Either (ArtifactError ident) ()
forall a b. b -> Either a b
Right ()

-- * Relocation

-- | What a unit's constants need in the loading world, judged once, from
-- the spelling table alone. 'Nothing' says every constant already has the
-- id its spelling means here, which is the fast path, on which no term is
-- walked at all. Otherwise the result is the renaming to apply. Its domain
-- is a scope of the unit's world, which no longer exists, so its index is
-- the caller's phantom.
--
-- The unit's own constants (table entries inside the recorded range) do
-- not consult the world: they are being loaded right now, in the same
-- order they were allocated, so their relocation is the affine shift
-- between the recorded range and the one this run assigned. Their new
-- names are thereby minted ahead of their allocation, which the caller's
-- trust covers. An imported constant resolves by its spelling, and one this
-- world does not know is reported. Finally, no relocation target may land
-- among the locals, since verbatim locals rest on the two never meeting.
--
-- @since 0.4.0
constantRelocation
  :: Ord ident
  => StoredLayout         -- ^ The unit's recorded layout.
  -> NameRange            -- ^ The range this run assigned to the unit.
  -> Map RawName ident    -- ^ Its spelling table.
  -> Map ident (Name n')  -- ^ What each spelling means here.
  -> Either (ArtifactError ident) (Maybe (NameMap old (Name n')))
constantRelocation :: forall ident (n' :: S) (old :: S).
Ord ident =>
StoredLayout
-> NameRange
-> Map RawName ident
-> Map ident (Name n')
-> Either (ArtifactError ident) (Maybe (NameMap old (Name n')))
constantRelocation (StoredLayout NameRange
old NameRange
locals) (NameRange RawName
newLo RawName
_) Map RawName ident
table Map ident (Name n')
globals = do
  entries <- (RawName
 -> ident
 -> Either (ArtifactError ident) [(RawName, Name n')]
 -> Either (ArtifactError ident) [(RawName, Name n')])
-> Either (ArtifactError ident) [(RawName, Name n')]
-> Map RawName ident
-> Either (ArtifactError ident) [(RawName, Name n')]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey RawName
-> ident
-> Either (ArtifactError ident) [(RawName, Name n')]
-> Either (ArtifactError ident) [(RawName, Name n')]
step ([(RawName, Name n')]
-> Either (ArtifactError ident) [(RawName, Name n')]
forall a b. b -> Either a b
Right []) Map RawName ident
table
  pure $
    if any (\(RawName
i, Name n'
name) -> Name n' -> RawName
forall (l :: S). Name l -> RawName
nameId Name n'
name RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
/= RawName
i) entries
      then Just (NameMap (IntMap.fromList entries))
      else Nothing
  where
    NameRange RawName
oldLo RawName
_ = NameRange
old
    shift :: RawName
shift = RawName
newLo RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
- RawName
oldLo
    step :: RawName
-> ident
-> Either (ArtifactError ident) [(RawName, Name n')]
-> Either (ArtifactError ident) [(RawName, Name n')]
step RawName
i ident
spelling Either (ArtifactError ident) [(RawName, Name n')]
acc = do
      rest <- Either (ArtifactError ident) [(RawName, Name n')]
acc
      name <-
        if nameRangeContains old i
          then Right (UnsafeName (i + shift))
          else case Map.lookup spelling globals of
            Maybe (Name n')
Nothing   -> ArtifactError ident -> Either (ArtifactError ident) (Name n')
forall a b. a -> Either a b
Left (ident -> ArtifactError ident
forall ident. ident -> ArtifactError ident
UnknownConstant ident
spelling)
            Just Name n'
name -> Name n' -> Either (ArtifactError ident) (Name n')
forall a b. b -> Either a b
Right Name n'
name
      if nameRangeContains locals (nameId name)
        then Left (ConstantAmongLocals spelling (nameId name))
        else pure ((i, name) : rest)

-- | Rename every constant reference through the map, moving the term from
-- the unit's world into the loading one. This is the restriction to
-- constants of a general renaming @'Name' n -> 'Name' n'@.
-- 'sinkabilityProof' embodies the general renaming, but its efficient
-- implementations degenerate the renaming to a coercion under binders,
-- which is sound only for inclusions, whereas this walk carries an arbitrary
-- map through.
--
-- The invariant that lets the walk ignore the binders is the disjointness
-- the recorded layout certifies: every name in the map's domain is a
-- constant, and a binder binds locals, so no binder can shadow a name in
-- the domain and no local can be in it. Note that this covers imported
-- constants too, since 'checkStoredLayout' refuses a spelling for any name
-- among the locals. Thus the map never needs extending under a binder, and
-- locals and patterns cross by coercion. A constant outside the map (bytes
-- referencing something the spelling table does not cover) is re-minted
-- unchanged, trusted like everything else about the term. Note that a map
-- that is the identity on raw ids would make the whole walk a coercion,
-- which is why 'constantRelocation' reports it as no relocation at all.
--
-- @since 0.4.0
relocateConstants
  :: forall binder sig n n'. Bifunctor sig
  => NameMap n (Name n') -> AST binder sig n -> AST binder sig n'
relocateConstants :: forall (binder :: S -> S -> *) (sig :: * -> * -> *) (n :: S)
       (n' :: S).
Bifunctor sig =>
NameMap n (Name n') -> AST binder sig n -> AST binder sig n'
relocateConstants (NameMap IntMap (Name n')
moved) = AST binder sig n -> AST binder sig n'
forall (o :: S) (o' :: S). AST binder sig o -> AST binder sig o'
walk
  where
    walk :: forall o o'. AST binder sig o -> AST binder sig o'
    walk :: forall (o :: S) (o' :: S). AST binder sig o -> AST binder sig o'
walk = \case
      Var Name o
x -> case RawName -> IntMap (Name n') -> Maybe (Name n')
forall a. RawName -> IntMap a -> Maybe a
IntMap.lookup (Name o -> RawName
forall (l :: S). Name l -> RawName
nameId Name o
x) IntMap (Name n')
moved of
        Just Name n'
new -> Name o' -> AST binder sig o'
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (RawName -> Name o'
forall (n :: S). RawName -> Name n
UnsafeName (Name n' -> RawName
forall (l :: S). Name l -> RawName
nameId Name n'
new))
        Maybe (Name n')
Nothing  -> Name o' -> AST binder sig o'
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (RawName -> Name o'
forall (n :: S). RawName -> Name n
UnsafeName (Name o -> RawName
forall (l :: S). Name l -> RawName
nameId Name o
x))
      Node sig (ScopedAST binder sig o) (AST binder sig o)
sig -> sig (ScopedAST binder sig o') (AST binder sig o')
-> AST binder sig o'
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig o -> ScopedAST binder sig o')
-> (AST binder sig o -> AST binder sig o')
-> sig (ScopedAST binder sig o) (AST binder sig o)
-> sig (ScopedAST binder sig o') (AST binder sig o')
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST binder sig o -> ScopedAST binder sig o'
forall (o :: S) (o' :: S).
ScopedAST binder sig o -> ScopedAST binder sig o'
walkScoped AST binder sig o -> AST binder sig o'
forall (o :: S) (o' :: S). AST binder sig o -> AST binder sig o'
walk sig (ScopedAST binder sig o) (AST binder sig o)
sig)

    walkScoped :: forall o o'. ScopedAST binder sig o -> ScopedAST binder sig o'
    walkScoped :: forall (o :: S) (o' :: S).
ScopedAST binder sig o -> ScopedAST binder sig o'
walkScoped (ScopedAST binder o l
pat AST binder sig l
body) = binder o' (ZonkAny 0)
-> AST binder sig (ZonkAny 0) -> ScopedAST binder sig o'
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST (binder o l -> binder o' (ZonkAny 0)
forall a b. a -> b
unsafeCoerce binder o l
pat) (AST binder sig l -> AST binder sig (ZonkAny 0)
forall (o :: S) (o' :: S). AST binder sig o -> AST binder sig o'
walk AST binder sig l
body)