{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Reserved name blocks, and linking of independently checked scopes.
--
-- Each unit of a module system allocates its names inside its own
-- reservation (a 'NameRange', via 'withFreshIn'), so that units checked
-- independently can be linked afterwards without renaming. 'ExtWithin' is
-- the evidence for that: scope @l@ extends scope @n@ only within a set of
-- reserved ranges. Note that the ranges bound the /extension/ and not the
-- scope, so the names of @n@ itself (typically, a unit's imports) may lie
-- anywhere.
--
-- Two units that extend a common scope within disjoint reservations have
-- disjoint extensions. 'withDisjointUnion' links them by comparing the
-- reservations rather than the scopes, and hands the continuation the
-- extension evidence for both sides, a 'ScopeUnion' witness that the result
-- is the union and nothing more, and the union's own evidence, so that a
-- linked unit is itself linkable. Evidence composes along a chain of units
-- with 'composeExtWithin'. To link more than two units, or to re-attach a
-- unit loaded from a cache, rebuild the union scope and mint the evidence
-- again with 'checkExtScope' and 'checkScopeUnion'.
--
-- 'checkExtScope' and 'checkScopeUnion' are a trust boundary. They compare
-- raw names across independently built scopes, which is meaningful only
-- under a deterministic reservation policy. Everything else in this module
-- either tests what it claims or constructs it.
module Control.Monad.Foil.Blocks (
  -- * Extension-within-a-range evidence
  ExtWithin,
  extWithinRanges,
  extWithinRefl,
  extWithinStep,
  composeExtWithin,
  -- * Blocks in use
  Block,
  beginBlock,
  resumeBlock,
  blockRange,
  blockExt,
  withFreshInBlock,
  -- * Bulk extension of a scope by a range
  withExtendScopeRange,
  -- * Linking
  ScopeUnion,
  withDisjointUnion,
  checkScopeUnion,
  checkExtScope,
  unionNameMaps,
) where

import           Data.List                   (sortOn)
import qualified Data.IntMap                 as IntMap
import qualified Data.IntSet                 as IntSet
import           Unsafe.Coerce               (unsafeCoerce)

import           Control.Monad.Foil.Internal

-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XFlexibleContexts
-- >>> import Control.Monad.Foil.Internal

-- | Evidence that scope @l@ extends scope @n@ only within a set of reserved
-- ranges: every name of @l@ that is not a name of @n@ lies inside one of
-- them.
--
-- The evidence is built alongside allocation, with 'extWithinRefl' at the
-- start of a unit and 'extWithinStep' at each binder, and composes along a
-- chain of scopes with 'composeExtWithin'. Its runtime content is the
-- ranges, sorted and disjoint.
--
-- @since 0.4.0
data ExtWithin (n :: S) (l :: S) = UnsafeExtWithin [NameRange]

-- | The reservations an 'ExtWithin' is evidence about: sorted, disjoint,
-- adjacent ranges coalesced, empty ones dropped.
--
-- @since 0.4.0
extWithinRanges :: ExtWithin n l -> [NameRange]
extWithinRanges :: forall (n :: S) (l :: S). ExtWithin n l -> [NameRange]
extWithinRanges (UnsafeExtWithin [NameRange]
ranges) = [NameRange]
ranges

-- | A scope extends itself within any range: the extension is empty.
--
-- Note that this does /not/ say the range is disjoint from the scope. It is
-- 'withExtendScopeRange' that checks that, because it allocates blindly.
--
-- @since 0.4.0
extWithinRefl :: NameRange -> ExtWithin n n
extWithinRefl :: forall (n :: S). NameRange -> ExtWithin n n
extWithinRefl NameRange
range = [NameRange] -> ExtWithin n n
forall (n :: S) (l :: S). [NameRange] -> ExtWithin n l
UnsafeExtWithin ([NameRange] -> [NameRange]
normaliseRanges [NameRange
range])

-- | Extend the evidence across one more binder, if its name lies inside one
-- of the ranges. One membership test per range.
--
-- A binder allocated by 'withFreshIn' at one of these ranges always passes.
-- A binder allocated elsewhere, by 'withFresh' or 'withRefreshed', is
-- rejected with 'Nothing' unless it happens to land inside them, so the
-- evidence cannot be extended past a name that escapes the reservations.
--
-- >>> let range = NameRange 100 199
-- >>> withFreshIn range emptyScope (\b -> fmap extWithinRanges (extWithinStep b (extWithinRefl range)))
-- Just [NameRange {nameRangeLo = 100, nameRangeHi = 199}]
--
-- @since 0.4.0
extWithinStep :: NameBinder l l' -> ExtWithin n l -> Maybe (ExtWithin n l')
extWithinStep :: forall (l :: S) (l' :: S) (n :: S).
NameBinder l l' -> ExtWithin n l -> Maybe (ExtWithin n l')
extWithinStep NameBinder l l'
binder (UnsafeExtWithin [NameRange]
ranges)
  | (NameRange -> Bool) -> [NameRange] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(NameRange RawName
lo RawName
hi) -> RawName
lo RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
x Bool -> Bool -> Bool
&& RawName
x RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi) [NameRange]
ranges = ExtWithin n l' -> Maybe (ExtWithin n l')
forall a. a -> Maybe a
Just ([NameRange] -> ExtWithin n l'
forall (n :: S) (l :: S). [NameRange] -> ExtWithin n l
UnsafeExtWithin [NameRange]
ranges)
  | Bool
otherwise = Maybe (ExtWithin n l')
forall a. Maybe a
Nothing
  where
    x :: RawName
x = Name l' -> RawName
forall (l :: S). Name l -> RawName
nameId (NameBinder l l' -> Name l'
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder l l'
binder)

-- | Compose evidence along a chain of scopes: if @m@ extends @n@ only within
-- one set of ranges and @l@ extends @m@ only within another, then @l@
-- extends @n@ only within their union.
--
-- The bound is the union of the two sets and not their hull, so a
-- reservation lying between them stays linkable. Adjacent ranges are
-- coalesced, so a chain of units with consecutive stripes collapses back to
-- a single range.
--
-- >>> extWithinRanges (composeExtWithin (extWithinRefl (NameRange 0 9)) (extWithinRefl (NameRange 30 39)))
-- [NameRange {nameRangeLo = 0, nameRangeHi = 9},NameRange {nameRangeLo = 30, nameRangeHi = 39}]
-- >>> extWithinRanges (composeExtWithin (extWithinRefl (NameRange 0 9)) (extWithinRefl (NameRange 10 19)))
-- [NameRange {nameRangeLo = 0, nameRangeHi = 19}]
--
-- @since 0.4.0
composeExtWithin :: ExtWithin n m -> ExtWithin m l -> ExtWithin n l
composeExtWithin :: forall (n :: S) (m :: S) (l :: S).
ExtWithin n m -> ExtWithin m l -> ExtWithin n l
composeExtWithin (UnsafeExtWithin [NameRange]
rs1) (UnsafeExtWithin [NameRange]
rs2) =
  [NameRange] -> ExtWithin n l
forall (n :: S) (l :: S). [NameRange] -> ExtWithin n l
UnsafeExtWithin ([NameRange] -> [NameRange]
normaliseRanges ([NameRange]
rs1 [NameRange] -> [NameRange] -> [NameRange]
forall a. Semigroup a => a -> a -> a
<> [NameRange]
rs2))

-- | Sort ranges, drop empty ones, and coalesce overlapping or adjacent ones.
normaliseRanges :: [NameRange] -> [NameRange]
normaliseRanges :: [NameRange] -> [NameRange]
normaliseRanges = [NameRange] -> [NameRange]
go ([NameRange] -> [NameRange])
-> ([NameRange] -> [NameRange]) -> [NameRange] -> [NameRange]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameRange -> RawName) -> [NameRange] -> [NameRange]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn NameRange -> RawName
nameRangeLo ([NameRange] -> [NameRange])
-> ([NameRange] -> [NameRange]) -> [NameRange] -> [NameRange]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameRange -> Bool) -> [NameRange] -> [NameRange]
forall a. (a -> Bool) -> [a] -> [a]
filter NameRange -> Bool
nonEmpty
  where
    nonEmpty :: NameRange -> Bool
nonEmpty (NameRange RawName
lo RawName
hi) = RawName
lo RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi
    go :: [NameRange] -> [NameRange]
go (NameRange RawName
lo1 RawName
hi1 : r2 :: NameRange
r2@(NameRange RawName
lo2 RawName
hi2) : [NameRange]
rs)
      | RawName
lo2 RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi1                      = [NameRange] -> [NameRange]
go (RawName -> RawName -> NameRange
NameRange RawName
lo1 (RawName -> RawName -> RawName
forall a. Ord a => a -> a -> a
max RawName
hi1 RawName
hi2) NameRange -> [NameRange] -> [NameRange]
forall a. a -> [a] -> [a]
: [NameRange]
rs)
      | RawName
hi1 RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
/= RawName
forall a. Bounded a => a
maxBound, RawName
lo2 RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
hi1 RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
+ RawName
1 = [NameRange] -> [NameRange]
go (RawName -> RawName -> NameRange
NameRange RawName
lo1 RawName
hi2 NameRange -> [NameRange] -> [NameRange]
forall a. a -> [a] -> [a]
: [NameRange]
rs)
      | Bool
otherwise = RawName -> RawName -> NameRange
NameRange RawName
lo1 RawName
hi1 NameRange -> [NameRange] -> [NameRange]
forall a. a -> [a] -> [a]
: [NameRange] -> [NameRange]
go (NameRange
r2 NameRange -> [NameRange] -> [NameRange]
forall a. a -> [a] -> [a]
: [NameRange]
rs)
    go [NameRange]
rs = [NameRange]
rs

-- | Whether two sorted sets of disjoint ranges share a name. One sweep.
rangeSetsOverlap :: [NameRange] -> [NameRange] -> Bool
rangeSetsOverlap :: [NameRange] -> [NameRange] -> Bool
rangeSetsOverlap (r1 :: NameRange
r1@(NameRange RawName
lo1 RawName
hi1) : [NameRange]
rs1) (r2 :: NameRange
r2@(NameRange RawName
lo2 RawName
hi2) : [NameRange]
rs2)
  | RawName
hi1 RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
< RawName
lo2 = [NameRange] -> [NameRange] -> Bool
rangeSetsOverlap [NameRange]
rs1 (NameRange
r2 NameRange -> [NameRange] -> [NameRange]
forall a. a -> [a] -> [a]
: [NameRange]
rs2)
  | RawName
hi2 RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
< RawName
lo1 = [NameRange] -> [NameRange] -> Bool
rangeSetsOverlap (NameRange
r1 NameRange -> [NameRange] -> [NameRange]
forall a. a -> [a] -> [a]
: [NameRange]
rs1) [NameRange]
rs2
  | Bool
otherwise = Bool
True
rangeSetsOverlap [NameRange]
_ [NameRange]
_ = Bool
False

-- | A reservation in use: the range fresh names are allocated from, paired
-- with the evidence that everything allocated since the base scope @c@ lies
-- within the unit's ranges.
--
-- The allocation range is always among the evidence's ranges, so stepping
-- the evidence at a freshly allocated name cannot fail and 'withFreshInBlock'
-- is total. The two components are not redundant: the evidence is a
-- normalised set bounding the whole extension, and once units are composed
-- the range to allocate from can no longer be read off it.
--
-- @since 0.0.1
data Block (c :: S) (l :: S) = UnsafeBlock !NameRange (ExtWithin c l)

-- | Start a unit: no names allocated yet, so the evidence is trivial.
--
-- @since 0.4.0
beginBlock :: NameRange -> Block c c
beginBlock :: forall (c :: S). NameRange -> Block c c
beginBlock NameRange
range = NameRange -> ExtWithin c c -> Block c c
forall (c :: S) (l :: S). NameRange -> ExtWithin c l -> Block c l
UnsafeBlock NameRange
range (NameRange -> ExtWithin c c
forall (n :: S). NameRange -> ExtWithin n n
extWithinRefl NameRange
range)

-- | Resume allocating from a range once the evidence has grown past what a
-- 'Block' tracked by itself, after composing in a loaded unit's evidence
-- with 'composeExtWithin'. This is what lets an interactive unit keep
-- allocating in its own reservation over the enlarged scope.
--
-- The allocation range must lie inside one of the evidence's ranges. The
-- ranges are normalised, so covering is containment in a single one, and
-- 'Nothing' says the range is not covered.
--
-- >>> let grown = composeExtWithin (extWithinRefl (NameRange 0 9)) (extWithinRefl (NameRange 10 19))
-- >>> fmap blockRange (resumeBlock (NameRange 0 9) grown)
-- Just (NameRange {nameRangeLo = 0, nameRangeHi = 9})
-- >>> fmap blockRange (resumeBlock (NameRange 30 39) grown)
-- Nothing
--
-- @since 0.4.0
resumeBlock :: NameRange -> ExtWithin c l -> Maybe (Block c l)
resumeBlock :: forall (c :: S) (l :: S).
NameRange -> ExtWithin c l -> Maybe (Block c l)
resumeBlock range :: NameRange
range@(NameRange RawName
lo RawName
hi) ExtWithin c l
ext
  | RawName
lo RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
> RawName
hi = Maybe (Block c l)
forall a. Maybe a
Nothing
  | (NameRange -> Bool) -> [NameRange] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any NameRange -> Bool
covers (ExtWithin c l -> [NameRange]
forall (n :: S) (l :: S). ExtWithin n l -> [NameRange]
extWithinRanges ExtWithin c l
ext) = Block c l -> Maybe (Block c l)
forall a. a -> Maybe a
Just (NameRange -> ExtWithin c l -> Block c l
forall (c :: S) (l :: S). NameRange -> ExtWithin c l -> Block c l
UnsafeBlock NameRange
range ExtWithin c l
ext)
  | Bool
otherwise = Maybe (Block c l)
forall a. Maybe a
Nothing
  where
    covers :: NameRange -> Bool
covers (NameRange RawName
lo' RawName
hi') = RawName
lo' RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
lo Bool -> Bool -> Bool
&& RawName
hi RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi'

-- | The range 'withFreshInBlock' allocates from.
--
-- @since 0.4.0
blockRange :: Block c l -> NameRange
blockRange :: forall (c :: S) (l :: S). Block c l -> NameRange
blockRange (UnsafeBlock NameRange
range ExtWithin c l
_) = NameRange
range

-- | The evidence accumulated so far: what a finished unit hands to
-- 'withDisjointUnion', or to 'composeExtWithin' for the next unit of a
-- chain.
--
-- @since 0.4.0
blockExt :: Block c l -> ExtWithin c l
blockExt :: forall (c :: S) (l :: S). Block c l -> ExtWithin c l
blockExt (UnsafeBlock NameRange
_ ExtWithin c l
ext) = ExtWithin c l
ext

-- | Allocate a fresh name in the block's range, stepping the evidence in
-- the same motion. Fails with 'error' only on an exhausted range, exactly
-- as 'withFreshIn' does.
--
-- >>> withFreshInBlock (beginBlock (NameRange 7 9)) emptyScope (\b block -> (nameId (nameOf b), extWithinRanges (blockExt block)))
-- (7,[NameRange {nameRangeLo = 7, nameRangeHi = 9}])
--
-- @since 0.4.0
withFreshInBlock
  :: Distinct l
  => Block c l  -- ^ The block to allocate from.
  -> Scope l    -- ^ The ambient scope.
  -> (forall l'. DExt l l' => NameBinder l l' -> Block c l' -> r)
  -> r
withFreshInBlock :: forall (l :: S) (c :: S) r.
Distinct l =>
Block c l
-> Scope l
-> (forall (l' :: S).
    DExt l l' =>
    NameBinder l l' -> Block c l' -> r)
-> r
withFreshInBlock (UnsafeBlock NameRange
range ExtWithin c l
ext) Scope l
scope forall (l' :: S). DExt l l' => NameBinder l l' -> Block c l' -> r
cont =
  NameRange
-> Scope l
-> (forall (l :: S). DExt l l => NameBinder l l -> r)
-> r
forall (n :: S) r.
Distinct n =>
NameRange
-> Scope n
-> (forall (l :: S). DExt n l => NameBinder n l -> r)
-> r
withFreshIn NameRange
range Scope l
scope ((forall (l :: S). DExt l l => NameBinder l l -> r) -> r)
-> (forall (l :: S). DExt l l => NameBinder l l -> r) -> r
forall a b. (a -> b) -> a -> b
$ \NameBinder l l
binder ->
    case NameBinder l l -> ExtWithin c l -> Maybe (ExtWithin c l)
forall (l :: S) (l' :: S) (n :: S).
NameBinder l l' -> ExtWithin n l -> Maybe (ExtWithin n l')
extWithinStep NameBinder l l
binder ExtWithin c l
ext of
      Just ExtWithin c l
ext' -> NameBinder l l -> Block c l -> r
forall (l' :: S). DExt l l' => NameBinder l l' -> Block c l' -> r
cont NameBinder l l
binder (NameRange -> ExtWithin c l -> Block c l
forall (c :: S) (l :: S). NameRange -> ExtWithin c l -> Block c l
UnsafeBlock NameRange
range ExtWithin c l
ext')
      Maybe (ExtWithin c l)
Nothing   -> [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: withFreshIn allocated outside its own range"

-- | Extend a scope with the first @k@ names of a range, in one step.
--
-- This is the bulk form of a unit's allocation, for loading a cached unit
-- whose extension is known to be @k@ consecutive names, or for pre-allocating
-- a unit's names before checking its bodies. The range part of the scope must
-- be empty, which is checked, so the extension is fresh by construction.
-- 'Nothing' reports an occupied range, and also a range with fewer than @k@
-- names.
--
-- The continuation receives the extended scope, the binders in ascending
-- order (for extending a 'NameMap' in the same step), and the 'ExtWithin'
-- evidence. The scope extension is a dense 'IntSet.fromRange', \(O(k/W)\).
--
-- >>> withExtendScopeRange emptyScope (NameRange 100 199) 3 (\_ binders _ -> rawNameBinderList binders)
-- Just [100,101,102]
--
-- @since 0.4.0
withExtendScopeRange
  :: forall c r. Distinct c
  => Scope c      -- ^ The scope to extend (typically, a unit's imports).
  -> NameRange    -- ^ The unit's reservation.
  -> Int          -- ^ How many names to allocate.
  -> (forall n. DExt c n => Scope n -> NameBinderList c n -> ExtWithin c n -> r)
  -> Maybe r
withExtendScopeRange :: forall (c :: S) r.
Distinct c =>
Scope c
-> NameRange
-> RawName
-> (forall (n :: S).
    DExt c n =>
    Scope n -> NameBinderList c n -> ExtWithin c n -> r)
-> Maybe r
withExtendScopeRange (UnsafeScope RawScope
scope) range :: NameRange
range@(NameRange RawName
lo RawName
hi) RawName
k forall (n :: S).
DExt c n =>
Scope n -> NameBinderList c n -> ExtWithin c n -> r
cont
  | RawName
k RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
< RawName
0                        = Maybe r
forall a. Maybe a
Nothing
  | Bool
rangeOccupied                = Maybe r
forall a. Maybe a
Nothing
  | RawName -> Integer
forall a. Integral a => a -> Integer
toInteger RawName
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
rangeCapacity  = Maybe r
forall a. Maybe a
Nothing
  | Bool
otherwise =
      r -> Maybe r
forall a. a -> Maybe a
Just (Scope (ZonkAny 2)
-> NameBinderList c (ZonkAny 2)
-> ExtWithin c (ZonkAny 2)
-> (DExt c (ZonkAny 2) =>
    Scope (ZonkAny 2)
    -> NameBinderList c (ZonkAny 2) -> ExtWithin c (ZonkAny 2) -> r)
-> r
forall (c :: S) (n :: S) r.
Scope n
-> NameBinderList c n
-> ExtWithin c n
-> (DExt c n =>
    Scope n -> NameBinderList c n -> ExtWithin c n -> r)
-> r
unsafeExtendedWithin (RawScope -> Scope (ZonkAny 2)
forall (n :: S). RawScope -> Scope n
UnsafeScope RawScope
scope') NameBinderList c (ZonkAny 2)
forall (n :: S). NameBinderList c n
binders ([NameRange] -> ExtWithin c (ZonkAny 2)
forall (n :: S) (l :: S). [NameRange] -> ExtWithin n l
UnsafeExtWithin ([NameRange] -> [NameRange]
normaliseRanges [NameRange
range])) DExt c (ZonkAny 2) =>
Scope (ZonkAny 2)
-> NameBinderList c (ZonkAny 2) -> ExtWithin c (ZonkAny 2) -> r
Scope (ZonkAny 2)
-> NameBinderList c (ZonkAny 2) -> ExtWithin c (ZonkAny 2) -> r
forall (n :: S).
DExt c n =>
Scope n -> NameBinderList c n -> ExtWithin c n -> r
cont)
  where
    rangeOccupied :: Bool
rangeOccupied = case RawName -> RawScope -> Maybe RawName
IntSet.lookupGE RawName
lo RawScope
scope of
      Just RawName
y  -> RawName
y RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
<= RawName
hi
      Maybe RawName
Nothing -> Bool
False
    rangeCapacity :: Integer
rangeCapacity = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 (RawName -> Integer
forall a. Integral a => a -> Integer
toInteger RawName
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- RawName -> Integer
forall a. Integral a => a -> Integer
toInteger RawName
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
    scope' :: RawScope
scope'
      | RawName
k RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
0    = RawScope
scope
      | Bool
otherwise = RawScope -> RawScope -> RawScope
IntSet.union RawScope
scope ((RawName, RawName) -> RawScope
IntSet.fromRange (RawName
lo, RawName
lo RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
+ (RawName
k RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
- RawName
1)))
    binders :: forall n. NameBinderList c n
    binders :: forall (n :: S). NameBinderList c n
binders = [RawName] -> NameBinderList c n
forall (m :: S) (m' :: S). [RawName] -> NameBinderList m m'
go (if RawName
k RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
0 then [] else [RawName
lo .. RawName
lo RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
+ (RawName
k RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
- RawName
1)])
      where
        go :: forall m m'. [RawName] -> NameBinderList m m'
        go :: forall (m :: S) (m' :: S). [RawName] -> NameBinderList m m'
go []       = NameBinderList (ZonkAny 0) (ZonkAny 0) -> NameBinderList m m'
forall a b. a -> b
unsafeCoerce NameBinderList (ZonkAny 0) (ZonkAny 0)
forall (n :: S). NameBinderList n n
NameBinderListEmpty
        go (RawName
x : [RawName]
xs) = NameBinder m (ZonkAny 1)
-> NameBinderList (ZonkAny 1) m' -> NameBinderList m m'
forall (n :: S) (i :: S) (l :: S).
NameBinder n i -> NameBinderList i l -> NameBinderList n l
NameBinderListCons (Name (ZonkAny 1) -> NameBinder m (ZonkAny 1)
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder (RawName -> Name (ZonkAny 1)
forall (n :: S). RawName -> Name n
UnsafeName RawName
x)) ([RawName] -> NameBinderList (ZonkAny 1) m'
forall (m :: S) (m' :: S). [RawName] -> NameBinderList m m'
go [RawName]
xs)

-- | Unsafely mint the evidence for an extension built by this module.
--
-- Sound when the scope really is the given base extended by the binders, and
-- the binders' names lie inside the evidence's range and are fresh in the
-- base. The callers here check or construct all three.
unsafeExtendedWithin
  :: forall c n r
   . Scope n -> NameBinderList c n -> ExtWithin c n
  -> (DExt c n => Scope n -> NameBinderList c n -> ExtWithin c n -> r)
  -> r
unsafeExtendedWithin :: forall (c :: S) (n :: S) r.
Scope n
-> NameBinderList c n
-> ExtWithin c n
-> (DExt c n =>
    Scope n -> NameBinderList c n -> ExtWithin c n -> r)
-> r
unsafeExtendedWithin Scope n
scope NameBinderList c n
binders ExtWithin c n
ext DExt c n => Scope n -> NameBinderList c n -> ExtWithin c n -> r
cont =
  case forall (n :: S). DistinctEvidence n
unsafeDistinct @n of
    DistinctEvidence n
Distinct -> case forall (n :: S) (l :: S). ExtEvidence n l
unsafeExt @c @n of
      ExtEvidence c n
Ext -> DExt c n => Scope n -> NameBinderList c n -> ExtWithin c n -> r
Scope n -> NameBinderList c n -> ExtWithin c n -> r
cont Scope n
scope NameBinderList c n
binders ExtWithin c n
ext

-- | Link two scopes that extend a common scope @c@ within their respective
-- reservations. The evidence check is one sweep over the two range sets;
-- the scope union is one 'IntSet.union'.
--
-- 'Nothing' when the two range sets overlap. The test is soundness and not
-- an optimisation. The extensions @n \\ c@ and @m \\ c@ lie inside their
-- respective range sets, so their disjointness is what guarantees that no
-- raw name denotes two different variables in the union. The names the two
-- scopes share are exactly the names of @c@, identified rather than renamed
-- apart, which is what linking two units over a common import must do.
--
-- The continuation receives both extension facts at once, a 'ScopeUnion'
-- witness (which 'unionNameMaps' requires), and the union's own 'ExtWithin',
-- so that a linked unit is itself linkable and a whole build folds through
-- this one function. It also receives @'Ext' c k@, which a caller cannot
-- derive on the spot.
--
-- @since 0.4.0
withDisjointUnion
  :: forall c n m r. (Distinct n, Distinct m)
  => ExtWithin c n  -- ^ Evidence for the first unit.
  -> ExtWithin c m  -- ^ Evidence for the second unit.
  -> Scope n        -- ^ The first unit's scope.
  -> Scope m        -- ^ The second unit's scope.
  -> (forall k. (Ext n k, Ext m k, Ext c k, Distinct k)
        => Scope k -> ScopeUnion n m k -> ExtWithin c k -> r)
  -> Maybe r
withDisjointUnion :: forall (c :: S) (n :: S) (m :: S) r.
(Distinct n, Distinct m) =>
ExtWithin c n
-> ExtWithin c m
-> Scope n
-> Scope m
-> (forall (k :: S).
    (Ext n k, Ext m k, Ext c k, Distinct k) =>
    Scope k -> ScopeUnion n m k -> ExtWithin c k -> r)
-> Maybe r
withDisjointUnion (UnsafeExtWithin [NameRange]
rs1) (UnsafeExtWithin [NameRange]
rs2) (UnsafeScope RawScope
s1) (UnsafeScope RawScope
s2) forall (k :: S).
(Ext n k, Ext m k, Ext c k, Distinct k) =>
Scope k -> ScopeUnion n m k -> ExtWithin c k -> r
cont
  | [NameRange] -> [NameRange] -> Bool
rangeSetsOverlap [NameRange]
rs1 [NameRange]
rs2 = Maybe r
forall a. Maybe a
Nothing
  | Bool
otherwise           = r -> Maybe r
forall a. a -> Maybe a
Just (Scope (ZonkAny 3) -> r
forall (k :: S). Scope k -> r
unsafeUnion (RawScope -> Scope (ZonkAny 3)
forall (n :: S). RawScope -> Scope n
UnsafeScope (RawScope -> RawScope -> RawScope
IntSet.union RawScope
s1 RawScope
s2)))
  where
    unsafeUnion :: forall k. Scope k -> r
    unsafeUnion :: forall (k :: S). Scope k -> r
unsafeUnion Scope k
scope =
      case forall (n :: S). DistinctEvidence n
unsafeDistinct @k of
        DistinctEvidence k
Distinct -> case forall (n :: S) (l :: S). ExtEvidence n l
unsafeExt @n @k of
          ExtEvidence n k
Ext -> case forall (n :: S) (l :: S). ExtEvidence n l
unsafeExt @m @k of
            ExtEvidence m k
Ext -> case forall (n :: S) (l :: S). ExtEvidence n l
unsafeExt @c @k of
              -- Each side extends the base within its own ranges, so the
              -- names of c are in n and in m, hence in the union. This is
              -- handed to the continuation as a given because deriving it
              -- from Ext c n and Ext n k leaves the solver two candidate
              -- paths and it commits to neither.
              ExtEvidence c k
Ext -> Scope k -> ScopeUnion n m k -> ExtWithin c k -> r
forall (k :: S).
(Ext n k, Ext m k, Ext c k, Distinct k) =>
Scope k -> ScopeUnion n m k -> ExtWithin c k -> r
cont Scope k
scope ScopeUnion n m k
forall (n :: S) (m :: S) (k :: S). ScopeUnion n m k
UnsafeScopeUnion
                          ([NameRange] -> ExtWithin c k
forall (n :: S) (l :: S). [NameRange] -> ExtWithin n l
UnsafeExtWithin ([NameRange] -> [NameRange]
normaliseRanges ([NameRange]
rs1 [NameRange] -> [NameRange] -> [NameRange]
forall a. Semigroup a => a -> a -> a
<> [NameRange]
rs2)))

-- | Evidence that scope @k@ is /precisely/ the union of scopes @n@ and @m@:
-- every name of @n@ and of @m@ is a name of @k@, and nothing else is.
--
-- The extension constraints @('Ext' n k, 'Ext' m k)@ state only the first
-- half, since a strict superset of the union satisfies them too. The second
-- half is what totality of a merged 'NameMap' rests on, so 'unionNameMaps'
-- demands this witness. It comes from 'withDisjointUnion', which builds the
-- union, or from 'checkScopeUnion', which tests for it.
--
-- @since 0.4.0
data ScopeUnion (n :: S) (m :: S) (k :: S) = UnsafeScopeUnion

-- | Test that a scope is precisely the union of two others, and produce the
-- witness if so. \(O(n+m)\).
--
-- This is the union witness for the re-attachment path, where the union
-- scope was rebuilt rather than handed down by 'withDisjointUnion'. Like
-- 'checkExtScope', it compares raw names across independently built scopes,
-- and is meaningful only under a deterministic reservation policy.
--
-- @since 0.4.0
checkScopeUnion :: Scope n -> Scope m -> Scope k -> Maybe (ScopeUnion n m k)
checkScopeUnion :: forall (n :: S) (m :: S) (k :: S).
Scope n -> Scope m -> Scope k -> Maybe (ScopeUnion n m k)
checkScopeUnion (UnsafeScope RawScope
s1) (UnsafeScope RawScope
s2) (UnsafeScope RawScope
s3)
  | RawScope -> RawScope -> RawScope
IntSet.union RawScope
s1 RawScope
s2 RawScope -> RawScope -> Bool
forall a. Eq a => a -> a -> Bool
== RawScope
s3 = ScopeUnion n m k -> Maybe (ScopeUnion n m k)
forall a. a -> Maybe a
Just ScopeUnion n m k
forall (n :: S) (m :: S) (k :: S). ScopeUnion n m k
UnsafeScopeUnion
  | Bool
otherwise                = Maybe (ScopeUnion n m k)
forall a. Maybe a
Nothing

-- | Test that every name of one scope is a name of another, and mint the
-- extension evidence if so. \(O(n+m)\) ('IntSet.isSubsetOf').
--
-- __This is a trust boundary.__ The test compares raw names, and raw names
-- from independently built scopes need not mean the same variable. The type
-- system tracks meaning through binders, and this function goes around it
-- deliberately, to re-attach a scope built elsewhere: in an earlier run, in
-- a cache, or in a parallel session. It is sound only under the external
-- discipline that a raw name has one global meaning, which a deterministic
-- reservation policy provides. Nothing here checks that discipline, and the
-- caller's allocator is what has to.
--
-- @since 0.4.0
checkExtScope :: Scope n -> Scope l -> Maybe (ExtEvidence n l)
checkExtScope :: forall (n :: S) (l :: S).
Scope n -> Scope l -> Maybe (ExtEvidence n l)
checkExtScope (UnsafeScope RawScope
s1) (UnsafeScope RawScope
s2)
  | RawScope
s1 RawScope -> RawScope -> Bool
`IntSet.isSubsetOf` RawScope
s2 = ExtEvidence n l -> Maybe (ExtEvidence n l)
forall a. a -> Maybe a
Just ExtEvidence n l
forall (n :: S) (l :: S). ExtEvidence n l
unsafeExt
  | Bool
otherwise                 = Maybe (ExtEvidence n l)
forall a. Maybe a
Nothing

-- | Union of two total maps into a map on the union of their scopes.
-- Left-biased, like 'IntMap.union'.
--
-- The witness is what makes the result total on @k@. The inputs are total on
-- @n@ and @m@, and 'ScopeUnion' says that @k@ holds their names and no
-- others. (It also determines @k@, which an extension constraint alone would
-- leave open.)
--
-- What no witness can say is that the two maps agree on the names their
-- scopes share. Linked units agree there when the shared part comes from the
-- same checked imports, and the left bias then only ever chooses between
-- equal entries.
--
-- @since 0.4.0
unionNameMaps :: ScopeUnion n m k -> NameMap n a -> NameMap m a -> NameMap k a
unionNameMaps :: forall (n :: S) (m :: S) (k :: S) a.
ScopeUnion n m k -> NameMap n a -> NameMap m a -> NameMap k a
unionNameMaps ScopeUnion n m k
UnsafeScopeUnion (NameMap IntMap a
m1) (NameMap IntMap a
m2) = IntMap a -> NameMap k a
forall (n :: S) a. IntMap a -> NameMap n a
NameMap (IntMap a -> IntMap a -> IntMap a
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union IntMap a
m1 IntMap a
m2)