{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

{- | Semiring scores with "holes".
 Holes are used to express "partially applied" scores that occur
 when the score of a verticalization (unspread) is distributed to the two parent edges.
 The full score of the operation is restored when the two parent edges are eventually combined again.

 This module implements partial scores as typesafe functions with phantom types
 that indicate the number of holes on each side.
 The grammatical combinators use an existential type 'Score'
 that reifies the phantom types as singletons,
 which allows different scores to be easily stored together
 and is compatible with the 'Score' types from the other Scoring* modules.
 Thus, the grammatical combinators are partial
 and fail when used with incompatible scores, indicating a parser bug.
-}
module Scoring.FunTyped
  ( -- * The Score Type
    Score (..)
  , TypedScore (..)
  , val
  , showScore

    -- ** IDs
  , LeftId (..)
  , RightId (..)
  , leftSide
  , rightSide

    -- ** Hole Types
  , LeftHoles
  , RightHoles
  , RightHole
  , BothHoles

    -- * Semiring operations

    -- | Semiring operations can be lifted to partial scores,
    -- but since it is not guaranteed that their arguments can be combined,
    -- they are partial.
  , times
  , plus

    -- * grammatical combinators

    -- | The following combinators correspond to the unsplit and unspread operations
    -- of the path-graph grammar.
  , unsplitScores
  , unspreadScoresLeft
  , unspreadScoresRight
  , addScores
  , getScoreVal
  ) where

import Control.DeepSeq
  ( NFData (rnf)
  , deepseq
  )
import Data.Hashable (Hashable)
import Data.Kind (Type)
import Data.Maybe (fromMaybe)
import Data.Semiring qualified as R
import Data.Type.Equality
import Data.Type.Nat
  ( Nat (..)
  , SNat (..)
  )
import GHC.Generics (Generic)

----------------
-- Score type --
----------------

-- | Newtype for the left ID of a partial score.
newtype LeftId i = LeftId i
  deriving (LeftId i -> LeftId i -> Bool
(LeftId i -> LeftId i -> Bool)
-> (LeftId i -> LeftId i -> Bool) -> Eq (LeftId i)
forall i. Eq i => LeftId i -> LeftId i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall i. Eq i => LeftId i -> LeftId i -> Bool
== :: LeftId i -> LeftId i -> Bool
$c/= :: forall i. Eq i => LeftId i -> LeftId i -> Bool
/= :: LeftId i -> LeftId i -> Bool
Eq, Eq (LeftId i)
Eq (LeftId i) =>
(LeftId i -> LeftId i -> Ordering)
-> (LeftId i -> LeftId i -> Bool)
-> (LeftId i -> LeftId i -> Bool)
-> (LeftId i -> LeftId i -> Bool)
-> (LeftId i -> LeftId i -> Bool)
-> (LeftId i -> LeftId i -> LeftId i)
-> (LeftId i -> LeftId i -> LeftId i)
-> Ord (LeftId i)
LeftId i -> LeftId i -> Bool
LeftId i -> LeftId i -> Ordering
LeftId i -> LeftId i -> LeftId i
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
forall i. Ord i => Eq (LeftId i)
forall i. Ord i => LeftId i -> LeftId i -> Bool
forall i. Ord i => LeftId i -> LeftId i -> Ordering
forall i. Ord i => LeftId i -> LeftId i -> LeftId i
$ccompare :: forall i. Ord i => LeftId i -> LeftId i -> Ordering
compare :: LeftId i -> LeftId i -> Ordering
$c< :: forall i. Ord i => LeftId i -> LeftId i -> Bool
< :: LeftId i -> LeftId i -> Bool
$c<= :: forall i. Ord i => LeftId i -> LeftId i -> Bool
<= :: LeftId i -> LeftId i -> Bool
$c> :: forall i. Ord i => LeftId i -> LeftId i -> Bool
> :: LeftId i -> LeftId i -> Bool
$c>= :: forall i. Ord i => LeftId i -> LeftId i -> Bool
>= :: LeftId i -> LeftId i -> Bool
$cmax :: forall i. Ord i => LeftId i -> LeftId i -> LeftId i
max :: LeftId i -> LeftId i -> LeftId i
$cmin :: forall i. Ord i => LeftId i -> LeftId i -> LeftId i
min :: LeftId i -> LeftId i -> LeftId i
Ord, (forall x. LeftId i -> Rep (LeftId i) x)
-> (forall x. Rep (LeftId i) x -> LeftId i) -> Generic (LeftId i)
forall x. Rep (LeftId i) x -> LeftId i
forall x. LeftId i -> Rep (LeftId i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall i x. Rep (LeftId i) x -> LeftId i
forall i x. LeftId i -> Rep (LeftId i) x
$cfrom :: forall i x. LeftId i -> Rep (LeftId i) x
from :: forall x. LeftId i -> Rep (LeftId i) x
$cto :: forall i x. Rep (LeftId i) x -> LeftId i
to :: forall x. Rep (LeftId i) x -> LeftId i
Generic, LeftId i -> ()
(LeftId i -> ()) -> NFData (LeftId i)
forall i. NFData i => LeftId i -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall i. NFData i => LeftId i -> ()
rnf :: LeftId i -> ()
NFData, Eq (LeftId i)
Eq (LeftId i) =>
(Int -> LeftId i -> Int)
-> (LeftId i -> Int) -> Hashable (LeftId i)
Int -> LeftId i -> Int
LeftId i -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall i. Hashable i => Eq (LeftId i)
forall i. Hashable i => Int -> LeftId i -> Int
forall i. Hashable i => LeftId i -> Int
$chashWithSalt :: forall i. Hashable i => Int -> LeftId i -> Int
hashWithSalt :: Int -> LeftId i -> Int
$chash :: forall i. Hashable i => LeftId i -> Int
hash :: LeftId i -> Int
Hashable)

instance Show i => Show (LeftId i) where
  show :: LeftId i -> String
show (LeftId i
i) = i -> String
forall a. Show a => a -> String
show i
i

-- | Newtype for the right ID of a partial score.
newtype RightId i = RightId i
  deriving (RightId i -> RightId i -> Bool
(RightId i -> RightId i -> Bool)
-> (RightId i -> RightId i -> Bool) -> Eq (RightId i)
forall i. Eq i => RightId i -> RightId i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall i. Eq i => RightId i -> RightId i -> Bool
== :: RightId i -> RightId i -> Bool
$c/= :: forall i. Eq i => RightId i -> RightId i -> Bool
/= :: RightId i -> RightId i -> Bool
Eq, Eq (RightId i)
Eq (RightId i) =>
(RightId i -> RightId i -> Ordering)
-> (RightId i -> RightId i -> Bool)
-> (RightId i -> RightId i -> Bool)
-> (RightId i -> RightId i -> Bool)
-> (RightId i -> RightId i -> Bool)
-> (RightId i -> RightId i -> RightId i)
-> (RightId i -> RightId i -> RightId i)
-> Ord (RightId i)
RightId i -> RightId i -> Bool
RightId i -> RightId i -> Ordering
RightId i -> RightId i -> RightId i
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
forall i. Ord i => Eq (RightId i)
forall i. Ord i => RightId i -> RightId i -> Bool
forall i. Ord i => RightId i -> RightId i -> Ordering
forall i. Ord i => RightId i -> RightId i -> RightId i
$ccompare :: forall i. Ord i => RightId i -> RightId i -> Ordering
compare :: RightId i -> RightId i -> Ordering
$c< :: forall i. Ord i => RightId i -> RightId i -> Bool
< :: RightId i -> RightId i -> Bool
$c<= :: forall i. Ord i => RightId i -> RightId i -> Bool
<= :: RightId i -> RightId i -> Bool
$c> :: forall i. Ord i => RightId i -> RightId i -> Bool
> :: RightId i -> RightId i -> Bool
$c>= :: forall i. Ord i => RightId i -> RightId i -> Bool
>= :: RightId i -> RightId i -> Bool
$cmax :: forall i. Ord i => RightId i -> RightId i -> RightId i
max :: RightId i -> RightId i -> RightId i
$cmin :: forall i. Ord i => RightId i -> RightId i -> RightId i
min :: RightId i -> RightId i -> RightId i
Ord, (forall x. RightId i -> Rep (RightId i) x)
-> (forall x. Rep (RightId i) x -> RightId i)
-> Generic (RightId i)
forall x. Rep (RightId i) x -> RightId i
forall x. RightId i -> Rep (RightId i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall i x. Rep (RightId i) x -> RightId i
forall i x. RightId i -> Rep (RightId i) x
$cfrom :: forall i x. RightId i -> Rep (RightId i) x
from :: forall x. RightId i -> Rep (RightId i) x
$cto :: forall i x. Rep (RightId i) x -> RightId i
to :: forall x. Rep (RightId i) x -> RightId i
Generic, RightId i -> ()
(RightId i -> ()) -> NFData (RightId i)
forall i. NFData i => RightId i -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall i. NFData i => RightId i -> ()
rnf :: RightId i -> ()
NFData, Eq (RightId i)
Eq (RightId i) =>
(Int -> RightId i -> Int)
-> (RightId i -> Int) -> Hashable (RightId i)
Int -> RightId i -> Int
RightId i -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall i. Hashable i => Eq (RightId i)
forall i. Hashable i => Int -> RightId i -> Int
forall i. Hashable i => RightId i -> Int
$chashWithSalt :: forall i. Hashable i => Int -> RightId i -> Int
hashWithSalt :: Int -> RightId i -> Int
$chash :: forall i. Hashable i => RightId i -> Int
hash :: RightId i -> Int
Hashable)

instance Show i => Show (RightId i) where
  show :: RightId i -> String
show (RightId i
i) = i -> String
forall a. Show a => a -> String
show i
i

match :: Eq a => RightId a -> LeftId a -> Bool
match :: forall a. Eq a => RightId a -> LeftId a -> Bool
match (RightId a
ir) (LeftId a
il) = a
il a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
ir

-- | A single right hole (helper for 'RightHoles').
data RightHole (n :: Nat) s where
  RightHole :: !(RightHoles n s) -> RightHole ('S n) s
  RightEnd :: !s -> RightHole 'Z s

instance (NFData s) => NFData (RightHole n s) where
  rnf :: RightHole n s -> ()
rnf (RightHole RightHoles n s
f) = RightHoles n s -> ()
forall a. NFData a => a -> ()
rnf RightHoles n s
f
  rnf (RightEnd s
s) = s -> ()
forall a. NFData a => a -> ()
rnf s
s

-- | The type of a function representing @n@ right holes.
type RightHoles (n :: Nat) s = s -> RightHole n s

-- | The type of a function representing @n@ left holes.
type LeftHoles (n :: Nat) s = (RightHoles n s -> s)

-- | The type of a function containing @nl@ left and @nr@ right holes.
type BothHoles (nl :: Nat) (nr :: Nat) s = (RightHoles nr s -> RightHoles nl s)

{- | A partially applied score of type @s@.
 Comes in four variants,
 depending on whether the score is fully applied
 or needs to be combined on either or both sides.
 Values that need to be combined are lists that represent scores with holes.
 Each variant carries IDs of type @i@ that determine which objects fit on either of its sides.
 Only score objects with matching IDs can be combined.

 As a shorthand notation, we use @a-b@ to indicate a value
 that depends on @a@ on its left and on @b@ on its right.
 If the value does not depend on anything on either side, we use @()@,
 i.e. @()-a@ stands for @SLeft _ a@ and @()-()@ stands for @SVal _@.
-}
data TypedScore (nl :: Nat) (nr :: Nat) s i where
  -- | Carries a fully applied value
  SVal :: !s -> TypedScore 'Z 'Z s i
  -- | The right part of a combination, expects an argument to its left.
  -- Implemented as a function that takes a left counterpart
  -- and returns a score with fewer holes.
  SRight :: !(LeftId i) -> !(RightHoles nl s) -> TypedScore ('S nl) 'Z s i
  -- | The left part of a combination, expects an argument to its right.
  -- Implemented as a function that takes a right hole and applies it.
  SLeft :: !(LeftHoles nr s) -> !(RightId i) -> TypedScore 'Z ('S nr) s i
  -- | A combination of 'SLeft' and 'SRight' that expects arguments on both sides.
  -- Implemented as a function that expects both a right and a left hole to be complete.
  SBoth :: !(LeftId i) -> !(BothHoles nl nr s) -> !(RightId i) -> TypedScore ('S nl) ('S nr) s i

instance (NFData s, NFData i) => NFData (TypedScore nl nr s i) where
  rnf :: TypedScore nl nr s i -> ()
rnf (SVal s
s) = s -> ()
forall a. NFData a => a -> ()
rnf s
s
  rnf (SRight LeftId i
i RightHoles nl s
_) = LeftId i -> ()
forall a. NFData a => a -> ()
rnf LeftId i
i
  rnf (SLeft LeftHoles nr s
_ RightId i
i) = RightId i -> ()
forall a. NFData a => a -> ()
rnf RightId i
i
  rnf (SBoth LeftId i
il BothHoles nl nr s
_ RightId i
ir) = LeftId i
il LeftId i -> () -> ()
forall a b. NFData a => a -> b -> b
`deepseq` RightId i -> ()
forall a. NFData a => a -> ()
rnf RightId i
ir

{- | A paritally applied score of type @s@
 with an unknown number of holes (as used by the "ChartParser").
 Wraps a 'TypedScore' together with witnesses for the number of holes on each side.
-}
data Score s i :: Type where
  MkScore :: SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i

instance (NFData s, NFData i) => NFData (Score s i) where
  rnf :: Score s i -> ()
rnf (MkScore SNat nl
_ SNat nr
_ TypedScore nl nr s i
s) = TypedScore nl nr s i -> ()
forall a. NFData a => a -> ()
rnf TypedScore nl nr s i
s

-- | Creates a simple value score of type ()-().
val :: s -> Score s i
val :: forall s i. s -> Score s i
val s
s = SNat 'Z -> SNat 'Z -> TypedScore 'Z 'Z s i -> Score s i
forall (nl :: Nat) (nr :: Nat) s i.
SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
MkScore SNat 'Z
SZ SNat 'Z
SZ (s -> TypedScore 'Z 'Z s i
forall s i. s -> TypedScore 'Z 'Z s i
SVal s
s)

{- | Returns the ID on the left side of an 'Score',
 or 'Nothing' for 'SVal' and 'SLeft'.

 > a-b -> a
-}
leftSide :: Score s i -> Maybe (LeftId i)
leftSide :: forall s i. Score s i -> Maybe (LeftId i)
leftSide (MkScore SNat nl
_ SNat nr
_ (SVal s
_)) = Maybe (LeftId i)
forall a. Maybe a
Nothing
leftSide (MkScore SNat nl
_ SNat nr
_ (SLeft LeftHoles nr s
_ RightId i
_)) = Maybe (LeftId i)
forall a. Maybe a
Nothing
leftSide (MkScore SNat nl
_ SNat nr
_ (SRight LeftId i
i RightHoles nl s
_)) = LeftId i -> Maybe (LeftId i)
forall a. a -> Maybe a
Just LeftId i
i
leftSide (MkScore SNat nl
_ SNat nr
_ (SBoth LeftId i
i BothHoles nl nr s
_ RightId i
_)) = LeftId i -> Maybe (LeftId i)
forall a. a -> Maybe a
Just LeftId i
i

{- | Returns the ID on the right side of an 'Score',
 or 'Nothing' for 'SVal' and 'SRight'.

 > a-b -> b
-}
rightSide :: Score s i -> Maybe (RightId i)
rightSide :: forall s i. Score s i -> Maybe (RightId i)
rightSide (MkScore SNat nl
_ SNat nr
_ (SVal s
_)) = Maybe (RightId i)
forall a. Maybe a
Nothing
rightSide (MkScore SNat nl
_ SNat nr
_ (SLeft LeftHoles nr s
_ RightId i
i)) = RightId i -> Maybe (RightId i)
forall a. a -> Maybe a
Just RightId i
i
rightSide (MkScore SNat nl
_ SNat nr
_ (SRight LeftId i
_ RightHoles nl s
_)) = Maybe (RightId i)
forall a. Maybe a
Nothing
rightSide (MkScore SNat nl
_ SNat nr
_ (SBoth LeftId i
_ BothHoles nl nr s
_ RightId i
i)) = RightId i -> Maybe (RightId i)
forall a. a -> Maybe a
Just RightId i
i

instance (Show i) => Show (TypedScore nl nr s i) where
  show :: TypedScore nl nr s i -> String
show (SVal s
_) = String
"()-()"
  show (SLeft LeftHoles nr s
_ RightId i
ir) = String
"()-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RightId i -> String
forall a. Show a => a -> String
show RightId i
ir
  show (SRight LeftId i
il RightHoles nl s
_) = LeftId i -> String
forall a. Show a => a -> String
show LeftId i
il String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"-()"
  show (SBoth LeftId i
il BothHoles nl nr s
_ RightId i
ir) = LeftId i -> String
forall a. Show a => a -> String
show LeftId i
il String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RightId i -> String
forall a. Show a => a -> String
show RightId i
ir

instance (Show i) => Show (Score s i) where
  show :: Score s i -> String
show (MkScore SNat nl
_ SNat nr
_ TypedScore nl nr s i
s) = TypedScore nl nr s i -> String
forall a. Show a => a -> String
show TypedScore nl nr s i
s

showTScore :: (Show s, Show i) => TypedScore nl nr s i -> String
showTScore :: forall s i (nl :: Nat) (nr :: Nat).
(Show s, Show i) =>
TypedScore nl nr s i -> String
showTScore (SVal s
v) = s -> String
forall a. Show a => a -> String
show s
v
showTScore (SLeft LeftHoles nr s
_ RightId i
ir) = String
"()-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RightId i -> String
forall a. Show a => a -> String
show RightId i
ir
showTScore (SRight LeftId i
il RightHoles nl s
_) = LeftId i -> String
forall a. Show a => a -> String
show LeftId i
il String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"-()"
showTScore (SBoth LeftId i
il BothHoles nl nr s
_ RightId i
ir) = LeftId i -> String
forall a. Show a => a -> String
show LeftId i
il String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RightId i -> String
forall a. Show a => a -> String
show RightId i
ir

{- | Returns a string representation of a 'Score'
 (more compact than it's 'Show' instance).
-}
showScore :: (Show s, Show i) => Score s i -> String
showScore :: forall s i. (Show s, Show i) => Score s i -> String
showScore (MkScore SNat nl
_ SNat nr
_ TypedScore nl nr s i
s) = TypedScore nl nr s i -> String
forall s i (nl :: Nat) (nr :: Nat).
(Show s, Show i) =>
TypedScore nl nr s i -> String
showTScore TypedScore nl nr s i
s

-------------------------
-- semiring operations --
-------------------------

appendRight :: R.Semiring s => s -> RightHoles n s -> RightHoles n s
appendRight :: forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
appendRight !s
s' RightHoles n s
fr !s
l = RightHole n s -> RightHole n s
app (RightHole n s -> RightHole n s) -> RightHole n s -> RightHole n s
forall a b. (a -> b) -> a -> b
$ RightHoles n s
fr s
l
 where
  app :: RightHole n s -> RightHole n s
app (RightEnd s
r) = s -> RightHole 'Z s
forall s. s -> RightHole 'Z s
RightEnd (s -> RightHole 'Z s) -> s -> RightHole 'Z s
forall a b. (a -> b) -> a -> b
$ s
r s -> s -> s
forall a. Semiring a => a -> a -> a
R.* s
s'
  app (RightHole RightHoles n s
fr') = RightHoles n s -> RightHole ('S n) s
forall (nl :: Nat) s. RightHoles nl s -> RightHole ('S nl) s
RightHole (RightHoles n s -> RightHole ('S n) s)
-> RightHoles n s -> RightHole ('S n) s
forall a b. (a -> b) -> a -> b
$ s -> RightHoles n s -> RightHoles n s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
appendRight s
s' RightHoles n s
fr'

prependLeft :: R.Semiring s => s -> LeftHoles n s -> LeftHoles n s
prependLeft :: forall s (n :: Nat).
Semiring s =>
s -> LeftHoles n s -> LeftHoles n s
prependLeft !s
s LeftHoles n s
fl = (s
s s -> s -> s
forall a. Semiring a => a -> a -> a
R.*) (s -> s) -> LeftHoles n s -> LeftHoles n s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeftHoles n s
fl

prependRight :: R.Semiring s => s -> RightHoles n s -> RightHoles n s
prependRight :: forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
prependRight !s
s RightHoles n s
fr !s
l = RightHole n s -> RightHole n s
prep (RightHole n s -> RightHole n s) -> RightHole n s -> RightHole n s
forall a b. (a -> b) -> a -> b
$ RightHoles n s
fr s
l
 where
  prep :: RightHole n s -> RightHole n s
prep (RightEnd s
r) = s -> RightHole 'Z s
forall s. s -> RightHole 'Z s
RightEnd (s -> RightHole 'Z s) -> s -> RightHole 'Z s
forall a b. (a -> b) -> a -> b
$ s
s s -> s -> s
forall a. Semiring a => a -> a -> a
R.* s
r
  prep (RightHole RightHoles n s
fr') = RightHoles n s -> RightHole ('S n) s
forall (nl :: Nat) s. RightHoles nl s -> RightHole ('S nl) s
RightHole (RightHoles n s -> RightHole ('S n) s)
-> RightHoles n s -> RightHole ('S n) s
forall a b. (a -> b) -> a -> b
$ s -> RightHoles n s -> RightHoles n s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
prependRight s
s RightHoles n s
fr'

{- | Combines two partially applied 'Score's
 by applying them to each other and/or multiplying the underlying semiring values.
 Shapes and IDs at the adjacent sides must match, otherwise 'Nothing' is returned.

 > a-b × b-c -> a-c
-}
times
  :: (R.Semiring s, Eq i, Show i)
  => TypedScore nl n s i
  -> TypedScore n nr s i
  -> Maybe (TypedScore nl nr s i)
-- creates value
times :: forall s i (nl :: Nat) (n :: Nat) (nr :: Nat).
(Semiring s, Eq i, Show i) =>
TypedScore nl n s i
-> TypedScore n nr s i -> Maybe (TypedScore nl nr s i)
times (SVal s
s1) (SVal s
s2) = TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! s -> TypedScore 'Z 'Z s i
forall s i. s -> TypedScore 'Z 'Z s i
SVal (s -> TypedScore 'Z 'Z s i) -> s -> TypedScore 'Z 'Z s i
forall a b. (a -> b) -> a -> b
$ s
s1 s -> s -> s
forall a. Semiring a => a -> a -> a
R.* s
s2
times (SLeft LeftHoles nr s
fl RightId i
il) (SRight LeftId i
ir RightHoles nl s
fr) | RightId i
il RightId i -> LeftId i -> Bool
forall a. Eq a => RightId a -> LeftId a -> Bool
`match` LeftId i
ir = TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! s -> TypedScore 'Z 'Z s i
forall s i. s -> TypedScore 'Z 'Z s i
SVal (s -> TypedScore 'Z 'Z s i) -> s -> TypedScore 'Z 'Z s i
forall a b. (a -> b) -> a -> b
$ LeftHoles nr s
fl s -> RightHole nr s
RightHoles nl s
fr
-- creates right
times (SRight LeftId i
i RightHoles nl s
r) (SVal s
s) = TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
i (RightHoles nl s -> TypedScore ('S nl) 'Z s i)
-> RightHoles nl s -> TypedScore ('S nl) 'Z s i
forall a b. (a -> b) -> a -> b
$ s -> RightHoles nl s -> RightHoles nl s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
appendRight s
s RightHoles nl s
r
times (SBoth LeftId i
il BothHoles nl nr s
fb RightId i
ir) (SRight LeftId i
i RightHoles nl s
fr) | RightId i
ir RightId i -> LeftId i -> Bool
forall a. Eq a => RightId a -> LeftId a -> Bool
`match` LeftId i
i = TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$ LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
il (RightHoles nl s -> TypedScore ('S nl) 'Z s i)
-> RightHoles nl s -> TypedScore ('S nl) 'Z s i
forall a b. (a -> b) -> a -> b
$ BothHoles nl nr s
fb s -> RightHole nr s
RightHoles nl s
fr
-- creates left
times (SVal s
s) (SLeft LeftHoles nr s
fl RightId i
i) = TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! LeftHoles nr s -> RightId i -> TypedScore 'Z ('S nr) s i
forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (s -> LeftHoles nr s -> LeftHoles nr s
forall s (n :: Nat).
Semiring s =>
s -> LeftHoles n s -> LeftHoles n s
prependLeft s
s LeftHoles nr s
fl) RightId i
i
times (SLeft LeftHoles nr s
fl RightId i
i) (SBoth LeftId i
il BothHoles nl nr s
fb RightId i
ir) | RightId i
i RightId i -> LeftId i -> Bool
forall a. Eq a => RightId a -> LeftId a -> Bool
`match` LeftId i
il = TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! LeftHoles nr s -> RightId i -> TypedScore 'Z ('S nr) s i
forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (LeftHoles nr s
fl LeftHoles nr s
-> (RightHoles nr s -> RightHoles nr s) -> LeftHoles nr s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RightHoles nr s -> RightHoles nr s
BothHoles nl nr s
fb) RightId i
ir
-- creates both
times (SRight LeftId i
il RightHoles nl s
fr) (SLeft LeftHoles nr s
fl RightId i
ir) =
  TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
forall i (nl :: Nat) (nr :: Nat) s.
LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
SBoth LeftId i
il ((s -> RightHoles nl s -> RightHoles nl s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
`appendRight` RightHoles nl s
fr) (s -> RightHoles nl s) -> LeftHoles nr s -> BothHoles nl nr s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeftHoles nr s
fl) RightId i
ir
times (SBoth LeftId i
il BothHoles nl nr s
fa RightId i
ia) (SBoth LeftId i
ib BothHoles nl nr s
fb RightId i
ir)
  | RightId i
ia RightId i -> LeftId i -> Bool
forall a. Eq a => RightId a -> LeftId a -> Bool
`match` LeftId i
ib =
      TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
forall i (nl :: Nat) (nr :: Nat) s.
LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
SBoth LeftId i
il (BothHoles nl nr s
fa BothHoles nl nr s
-> (RightHoles nr s -> RightHoles nr s) -> BothHoles nl nr s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RightHoles nr s -> RightHoles nr s
BothHoles nl nr s
fb) RightId i
ir
-- otherwise
times TypedScore nl n s i
_ TypedScore n nr s i
_ = Maybe (TypedScore nl nr s i)
forall a. Maybe a
Nothing

rhplus :: (R.Semiring s) => RightHoles n s -> RightHoles n s -> RightHoles n s
rhplus :: forall s (n :: Nat).
Semiring s =>
RightHoles n s -> RightHoles n s -> RightHoles n s
rhplus RightHoles n s
r1 RightHoles n s
r2 !s
l = case (RightHoles n s
r1 s
l, RightHoles n s
r2 s
l) of
  (RightEnd s
e1, RightEnd s
e2) -> s -> RightHole 'Z s
forall s. s -> RightHole 'Z s
RightEnd (s -> RightHole 'Z s) -> s -> RightHole 'Z s
forall a b. (a -> b) -> a -> b
$ s
e1 s -> s -> s
forall a. Semiring a => a -> a -> a
R.+ s
e2
  (RightHole RightHoles n s
f1, RightHole RightHoles n s
f2) -> RightHoles n s -> RightHole ('S n) s
forall (nl :: Nat) s. RightHoles nl s -> RightHole ('S nl) s
RightHole (RightHoles n s -> RightHole ('S n) s)
-> RightHoles n s -> RightHole ('S n) s
forall a b. (a -> b) -> a -> b
$ RightHoles n s -> RightHoles n s -> RightHoles n s
forall s (n :: Nat).
Semiring s =>
RightHoles n s -> RightHoles n s -> RightHoles n s
rhplus RightHoles n s
f1 RightHoles n s
RightHoles n s
f2

{- | Adds two partially applied 'TypedScore's
 by adding their underlying (or resulting) semiring values.
 This operation is only admitted
 if the two scores are of the same shape and have matching IDs.
 Otherwise, 'Nothing' is returned.

 > a-b + a-b -> a-b
-}
plus
  :: (R.Semiring s, Eq i)
  => TypedScore nl nr s i
  -> TypedScore nl nr s i
  -> Maybe (TypedScore nl nr s i)
plus :: forall s i (nl :: Nat) (nr :: Nat).
(Semiring s, Eq i) =>
TypedScore nl nr s i
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
plus (SVal s
s1) (SVal s
s2) = TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! s -> TypedScore 'Z 'Z s i
forall s i. s -> TypedScore 'Z 'Z s i
SVal (s -> TypedScore 'Z 'Z s i) -> s -> TypedScore 'Z 'Z s i
forall a b. (a -> b) -> a -> b
$ s
s1 s -> s -> s
forall a. Semiring a => a -> a -> a
R.+ s
s2
plus (SRight LeftId i
i RightHoles nl s
fr1) (SRight LeftId i
i' RightHoles nl s
fr2)
  | LeftId i
i LeftId i -> LeftId i -> Bool
forall a. Eq a => a -> a -> Bool
== LeftId i
i' =
      TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
i (RightHoles nl s -> TypedScore ('S nl) 'Z s i)
-> RightHoles nl s -> TypedScore ('S nl) 'Z s i
forall a b. (a -> b) -> a -> b
$ RightHoles nl s -> RightHoles nl s -> RightHoles nl s
forall s (n :: Nat).
Semiring s =>
RightHoles n s -> RightHoles n s -> RightHoles n s
rhplus RightHoles nl s
fr1 RightHoles nl s
RightHoles nl s
fr2
plus (SLeft LeftHoles nr s
fl1 RightId i
i) (SLeft LeftHoles nr s
fl2 RightId i
i')
  | RightId i
i RightId i -> RightId i -> Bool
forall a. Eq a => a -> a -> Bool
== RightId i
i' =
      TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! LeftHoles nr s -> RightId i -> TypedScore 'Z ('S nr) s i
forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (\RightHoles nr s
r -> LeftHoles nr s
fl1 RightHoles nr s
r s -> s -> s
forall a. Semiring a => a -> a -> a
R.+ LeftHoles nr s
fl2 RightHoles nr s
s -> RightHole nr s
r) RightId i
i
plus (SBoth LeftId i
il BothHoles nl nr s
bs1 RightId i
ir) (SBoth LeftId i
il' BothHoles nl nr s
bs2 RightId i
ir')
  | LeftId i
il LeftId i -> LeftId i -> Bool
forall a. Eq a => a -> a -> Bool
== LeftId i
il' Bool -> Bool -> Bool
&& RightId i
ir RightId i -> RightId i -> Bool
forall a. Eq a => a -> a -> Bool
== RightId i
ir' =
      TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a. a -> Maybe a
Just (TypedScore nl nr s i -> Maybe (TypedScore nl nr s i))
-> TypedScore nl nr s i -> Maybe (TypedScore nl nr s i)
forall a b. (a -> b) -> a -> b
$! LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
forall i (nl :: Nat) (nr :: Nat) s.
LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
SBoth LeftId i
il (\RightHoles nr s
r -> RightHoles nl s -> RightHoles nl s -> RightHoles nl s
forall s (n :: Nat).
Semiring s =>
RightHoles n s -> RightHoles n s -> RightHoles n s
rhplus (BothHoles nl nr s
bs1 RightHoles nr s
r) (BothHoles nl nr s
bs2 RightHoles nr s
s -> RightHole nr s
r)) RightId i
ir
plus TypedScore nl nr s i
_ TypedScore nl nr s i
_ = Maybe (TypedScore nl nr s i)
forall a. Maybe a
Nothing

-- helpers for constructing holes
-- ------------------------------

addHoleLeft :: s -> LeftHoles n s -> LeftHoles ('S n) s
addHoleLeft :: forall s (n :: Nat). s -> LeftHoles n s -> LeftHoles ('S n) s
addHoleLeft !s
s LeftHoles n s
fl RightHoles ('S n) s
fr = case RightHoles ('S n) s
fr s
s of
  RightHole RightHoles n s
fr' -> LeftHoles n s
fl s -> RightHole n s
RightHoles n s
fr'

mkLeftHole :: s -> LeftHoles 'Z s
mkLeftHole :: forall s. s -> LeftHoles 'Z s
mkLeftHole !s
s RightHoles 'Z s
fr = case RightHoles 'Z s
fr s
s of
  RightEnd s
v -> s
v

addHoleRight :: R.Semiring s => s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight :: forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight !s
r !RightHoles n s
rh !s
l = RightHoles n s -> RightHole ('S n) s
forall (nl :: Nat) s. RightHoles nl s -> RightHole ('S nl) s
RightHole (RightHoles n s -> RightHole ('S n) s)
-> RightHoles n s -> RightHole ('S n) s
forall a b. (a -> b) -> a -> b
$ s -> RightHoles n s -> RightHoles n s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
prependRight (s
l s -> s -> s
forall a. Semiring a => a -> a -> a
R.* s
r) RightHoles n s
rh

mkRightHole :: R.Semiring s => s -> RightHoles 'Z s
mkRightHole :: forall s. Semiring s => s -> RightHoles 'Z s
mkRightHole !s
r !s
l = s -> RightHole 'Z s
forall s. s -> RightHole 'Z s
RightEnd (s -> RightHole 'Z s) -> s -> RightHole 'Z s
forall a b. (a -> b) -> a -> b
$ s
l s -> s -> s
forall a. Semiring a => a -> a -> a
R.* s
r

-- proof helpers

type family CreateHole (n :: Nat) where
  CreateHole 'Z = 'S ('S 'Z)
  CreateHole ('S n) = 'S ('S n)

class AddHole (n :: Nat) where
  addHole :: SNat n -> SNat (CreateHole n)

instance AddHole 'Z where
  addHole :: SNat 'Z -> SNat (CreateHole 'Z)
addHole SNat 'Z
SZ = SNat ('S ('S 'Z))
SNat (CreateHole 'Z)
forall (n1 :: Nat). SNatI n1 => SNat ('S n1)
SS

instance AddHole ('S n) where
  addHole :: SNat ('S n) -> SNat (CreateHole ('S n))
addHole SNat ('S n)
SS = SNat ('S ('S n))
SNat (CreateHole ('S n))
forall (n1 :: Nat). SNatI n1 => SNat ('S n1)
SS

canAddHole :: SNat n -> (AddHole n => r) -> r
canAddHole :: forall (n :: Nat) r. SNat n -> (AddHole n => r) -> r
canAddHole SNat n
SZ AddHole n => r
r = r
AddHole n => r
r
canAddHole SNat n
SS AddHole n => r
r = r
AddHole n => r
r

-----------
-- rules --
-----------

{- | Extracts the value from a fully applied 'Score'.
 This function is intended to be used to extract the final score of the parser.
 If the score is not fully applied,
 throws an exception to indicate parser bugs.
-}
getScoreVal :: Score s i -> s
getScoreVal :: forall s i. Score s i -> s
getScoreVal (MkScore SNat nl
_ SNat nr
_ (SVal s
s)) = s
s
getScoreVal Score s i
_ = String -> s
forall a. HasCallStack => String -> a
error String
"cannot get value from partial score"

{- | Adds two 'Score's that are alternative derivations of the same transition.
 This is expected to be called on compatible scores
 and will throw an error otherwise to indicate parser bugs.

 > a-b   a-b
 > --------- add
 >    a-b
-}
addScores :: (R.Semiring s, Eq i) => Score s i -> Score s i -> Score s i
addScores :: forall s i.
(Semiring s, Eq i) =>
Score s i -> Score s i -> Score s i
addScores (MkScore SNat nl
nla SNat nr
nra TypedScore nl nr s i
a) (MkScore SNat nl
nlb SNat nr
nrb TypedScore nl nr s i
b) = SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
forall (nl :: Nat) (nr :: Nat) s i.
SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
MkScore SNat nl
nla SNat nr
nra TypedScore nl nr s i
res
 where
  res :: TypedScore nl nr s i
res = TypedScore nl nr s i
-> Maybe (TypedScore nl nr s i) -> TypedScore nl nr s i
forall a. a -> Maybe a -> a
fromMaybe (String -> TypedScore nl nr s i
forall a. HasCallStack => String -> a
error String
"illegal plus") (Maybe (TypedScore nl nr s i) -> TypedScore nl nr s i)
-> Maybe (TypedScore nl nr s i) -> TypedScore nl nr s i
forall a b. (a -> b) -> a -> b
$ do
    Refl <- SNat nl -> SNat nl -> Maybe (nl :~: nl)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
testEquality SNat nl
nla SNat nl
nlb
    Refl <- testEquality nra nrb
    plus a b

{- | Combines the 'Score's of two edges with a @split@ operation into the score of the parent edge.
 This is expected to be called on compatible scores
 and will throw an error otherwise to indicate parser bugs.

 > a-b   b-c
 > --------- unsplit
 >    a-c
-}
unsplitScores
  :: forall s i
   . (R.Semiring s, Eq i, Show i, Show s)
  => s
  -- ^ The score of the split operation.
  -> Score s i
  -- ^ The 'Score' of the left child edge.
  -> Score s i
  -- ^ The 'Score' of the right child edge.
  -> Score s i
  -- ^ The 'Score' of the parent edge, if it exists.
unsplitScores :: forall s i.
(Semiring s, Eq i, Show i, Show s) =>
s -> Score s i -> Score s i -> Score s i
unsplitScores s
op (MkScore SNat nl
nll SNat nr
nrl TypedScore nl nr s i
left) (MkScore SNat nl
nlr SNat nr
nrr TypedScore nl nr s i
right) =
  SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
forall (nl :: Nat) (nr :: Nat) s i.
SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
MkScore SNat nl
nll SNat nr
nrr (TypedScore nl nr s i -> Score s i)
-> TypedScore nl nr s i -> Score s i
forall a b. (a -> b) -> a -> b
$ TypedScore nl nr s i
-> Maybe (TypedScore nl nr s i) -> TypedScore nl nr s i
forall a. a -> Maybe a -> a
fromMaybe TypedScore nl nr s i
err (Maybe (TypedScore nl nr s i) -> TypedScore nl nr s i)
-> Maybe (TypedScore nl nr s i) -> TypedScore nl nr s i
forall a b. (a -> b) -> a -> b
$ do
    Refl <- SNat nr -> SNat nl -> Maybe (nr :~: nl)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
testEquality SNat nr
nrl SNat nl
nlr
    times (prep left) right
 where
  err :: TypedScore nl nr s i
err =
    String -> TypedScore nl nr s i
forall a. HasCallStack => String -> a
error (String -> TypedScore nl nr s i) -> String -> TypedScore nl nr s i
forall a b. (a -> b) -> a -> b
$
      String
"Attempting illegal unsplit: left="
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypedScore nl nr s i -> String
forall a. Show a => a -> String
show TypedScore nl nr s i
left
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", right="
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypedScore nl nr s i -> String
forall a. Show a => a -> String
show TypedScore nl nr s i
right
  prep :: TypedScore nl nr s i -> TypedScore nl nr s i
  prep :: forall (nl :: Nat) (nr :: Nat).
TypedScore nl nr s i -> TypedScore nl nr s i
prep TypedScore nl nr s i
l = case TypedScore nl nr s i
l of
    SVal s
s -> s -> TypedScore 'Z 'Z s i
forall s i. s -> TypedScore 'Z 'Z s i
SVal (s
op s -> s -> s
forall a. Semiring a => a -> a -> a
R.* s
s)
    SLeft LeftHoles nr s
fl RightId i
i -> LeftHoles nr s -> RightId i -> TypedScore 'Z ('S nr) s i
forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (s -> LeftHoles nr s -> LeftHoles nr s
forall s (n :: Nat).
Semiring s =>
s -> LeftHoles n s -> LeftHoles n s
prependLeft s
op LeftHoles nr s
fl) RightId i
i
    SRight LeftId i
i RightHoles nl s
rs -> LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
i (s -> RightHoles nl s -> RightHoles nl s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
prependRight s
op RightHoles nl s
rs)
    SBoth LeftId i
il BothHoles nl nr s
bs RightId i
ir -> LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
forall i (nl :: Nat) (nr :: Nat) s.
LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
SBoth LeftId i
il (s -> RightHoles nl s -> RightHoles nl s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
prependRight s
op (RightHoles nl s -> RightHoles nl s)
-> BothHoles nl nr s -> BothHoles nl nr s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BothHoles nl nr s
bs) RightId i
ir

{- | Creates the 'Score' of a left parent edge from a left child edge of an @unspread@.
 Will throw an error if called on invalid input to indicate parser bugs.
-}
unspreadScoresLeft
  :: forall s i
   . (Eq i, Show i, R.Semiring s, Show s)
  => i
  -- ^ The new ID that marks both parent edges
  -> Score s i
  -- ^ The 'Score' of the left child edge.
  -> Score s i
  -- ^ The 'Score' of the left parent edge, if it exists.
unspreadScoresLeft :: forall s i.
(Eq i, Show i, Semiring s, Show s) =>
i -> Score s i -> Score s i
unspreadScoresLeft i
newid (MkScore SNat nl
SZ SNat nr
nr TypedScore nl nr s i
s) =
  SNat nr -> (AddHole nr => Score s i) -> Score s i
forall (n :: Nat) r. SNat n -> (AddHole n => r) -> r
canAddHole SNat nr
nr ((AddHole nr => Score s i) -> Score s i)
-> (AddHole nr => Score s i) -> Score s i
forall a b. (a -> b) -> a -> b
$ SNat 'Z
-> SNat (CreateHole nr)
-> TypedScore 'Z (CreateHole nr) s i
-> Score s i
forall (nl :: Nat) (nr :: Nat) s i.
SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
MkScore SNat 'Z
SZ (SNat nr -> SNat (CreateHole nr)
forall (n :: Nat). AddHole n => SNat n -> SNat (CreateHole n)
addHole SNat nr
nr) (TypedScore 'Z (CreateHole nr) s i -> Score s i)
-> TypedScore 'Z (CreateHole nr) s i -> Score s i
forall a b. (a -> b) -> a -> b
$ TypedScore 'Z nr s i -> TypedScore 'Z (CreateHole nr) s i
forall (nr :: Nat).
TypedScore 'Z nr s i -> TypedScore 'Z (CreateHole nr) s i
wrap TypedScore nl nr s i
TypedScore 'Z nr s i
s
 where
  newir :: RightId i
newir = i -> RightId i
forall i. i -> RightId i
RightId i
newid
  -- wrap the left input score into a new layer with a new ID
  wrap :: TypedScore 'Z nr s i -> TypedScore 'Z (CreateHole nr) s i
  wrap :: forall (nr :: Nat).
TypedScore 'Z nr s i -> TypedScore 'Z (CreateHole nr) s i
wrap (SVal s
v) = LeftHoles ('S 'Z) s -> RightId i -> TypedScore 'Z ('S ('S 'Z)) s i
forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (s -> LeftHoles 'Z s -> LeftHoles ('S 'Z) s
forall s (n :: Nat). s -> LeftHoles n s -> LeftHoles ('S n) s
addHoleLeft s
forall a. Semiring a => a
R.one (LeftHoles 'Z s -> LeftHoles ('S 'Z) s)
-> LeftHoles 'Z s -> LeftHoles ('S 'Z) s
forall a b. (a -> b) -> a -> b
$ s -> LeftHoles 'Z s
forall s. s -> LeftHoles 'Z s
mkLeftHole s
v) RightId i
newir
  wrap (SLeft LeftHoles nr s
fl RightId i
_) = LeftHoles ('S nr) s -> RightId i -> TypedScore 'Z ('S ('S nr)) s i
forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (s -> LeftHoles nr s -> LeftHoles ('S nr) s
forall s (n :: Nat). s -> LeftHoles n s -> LeftHoles ('S n) s
addHoleLeft s
forall a. Semiring a => a
R.one LeftHoles nr s
fl) RightId i
newir
unspreadScoresLeft i
_ (MkScore SNat nl
_ SNat nr
_ TypedScore nl nr s i
s) =
  String -> Score s i
forall a. HasCallStack => String -> a
error (String -> Score s i) -> String -> Score s i
forall a b. (a -> b) -> a -> b
$ String
"Attempting illegal left-unspread on " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypedScore nl nr s i -> String
forall a. Show a => a -> String
show TypedScore nl nr s i
s

{- | Creates the 'Score' of a right parent edge
 from the middle and right child edges of an @unspread@
 and a @spread@ operation.
-}
unspreadScoresRight
  :: forall i s
   . (Eq i, R.Semiring s, Show i, Show s)
  => i
  -- ^ The new ID that marks both parent edges.
  -> s
  -- ^ The score of the @spread@ operation.
  -> Score s i
  -- ^ The 'Score' of the middle child edge.
  -> Score s i
  -- ^ The 'Score' of the right child edge.
  -> Score s i
  -- ^ The 'Score' of the right parent edge, if it exists.
unspreadScoresRight :: forall i s.
(Eq i, Semiring s, Show i, Show s) =>
i -> s -> Score s i -> Score s i -> Score s i
unspreadScoresRight i
newid s
op (MkScore SNat nl
nlm SNat nr
nrm TypedScore nl nr s i
m) (MkScore SNat nl
nlr SNat nr
nrr TypedScore nl nr s i
r) =
  SNat nl -> (AddHole nl => Score s i) -> Score s i
forall (n :: Nat) r. SNat n -> (AddHole n => r) -> r
canAddHole SNat nl
nlm ((AddHole nl => Score s i) -> Score s i)
-> (AddHole nl => Score s i) -> Score s i
forall a b. (a -> b) -> a -> b
$ SNat (CreateHole nl)
-> SNat nr -> TypedScore (CreateHole nl) nr s i -> Score s i
forall (nl :: Nat) (nr :: Nat) s i.
SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
MkScore (SNat nl -> SNat (CreateHole nl)
forall (n :: Nat). AddHole n => SNat n -> SNat (CreateHole n)
addHole SNat nl
nlm) SNat nr
nrr (TypedScore (CreateHole nl) nr s i -> Score s i)
-> TypedScore (CreateHole nl) nr s i -> Score s i
forall a b. (a -> b) -> a -> b
$ TypedScore (CreateHole nl) nr s i
-> Maybe (TypedScore (CreateHole nl) nr s i)
-> TypedScore (CreateHole nl) nr s i
forall a. a -> Maybe a -> a
fromMaybe TypedScore (CreateHole nl) nr s i
err (Maybe (TypedScore (CreateHole nl) nr s i)
 -> TypedScore (CreateHole nl) nr s i)
-> Maybe (TypedScore (CreateHole nl) nr s i)
-> TypedScore (CreateHole nl) nr s i
forall a b. (a -> b) -> a -> b
$ do
    Refl <- SNat nr -> SNat nl -> Maybe (nr :~: nl)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
testEquality SNat nr
nrm SNat nl
nlr
    mr <- times m r
    pure $ unwrap mr
 where
  err :: TypedScore (CreateHole nl) nr s i
err =
    String -> TypedScore (CreateHole nl) nr s i
forall a. HasCallStack => String -> a
error (String -> TypedScore (CreateHole nl) nr s i)
-> String -> TypedScore (CreateHole nl) nr s i
forall a b. (a -> b) -> a -> b
$
      String
"Attempting illegal right-unspread: m="
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypedScore nl nr s i -> String
forall a. Show a => a -> String
show TypedScore nl nr s i
m
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", r="
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypedScore nl nr s i -> String
forall a. Show a => a -> String
show TypedScore nl nr s i
r
  -- generate a value on the right
  -- that consumes the left parent edge's value when supplied
  -- and combines with m on the right
  newil :: LeftId i
newil = i -> LeftId i
forall i. i -> LeftId i
LeftId i
newid
  unwrap :: TypedScore nl nr s i -> TypedScore (CreateHole nl) nr s i
  unwrap :: forall (nl :: Nat) (nr :: Nat).
TypedScore nl nr s i -> TypedScore (CreateHole nl) nr s i
unwrap (SVal s
s) = LeftId i -> RightHoles ('S 'Z) s -> TypedScore ('S ('S 'Z)) 'Z s i
forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
newil (RightHoles ('S 'Z) s -> TypedScore ('S ('S 'Z)) 'Z s i)
-> RightHoles ('S 'Z) s -> TypedScore ('S ('S 'Z)) 'Z s i
forall a b. (a -> b) -> a -> b
$ s -> RightHoles 'Z s -> RightHoles ('S 'Z) s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight s
op (RightHoles 'Z s -> RightHoles ('S 'Z) s)
-> RightHoles 'Z s -> RightHoles ('S 'Z) s
forall a b. (a -> b) -> a -> b
$ s -> RightHoles 'Z s
forall s. Semiring s => s -> RightHoles 'Z s
mkRightHole s
s -- [op, s]
  unwrap (SRight LeftId i
_ RightHoles nl s
rs) = LeftId i -> RightHoles ('S nl) s -> TypedScore ('S ('S nl)) 'Z s i
forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
newil (s -> RightHoles nl s -> RightHoles ('S nl) s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight s
op RightHoles nl s
rs)
  unwrap (SLeft LeftHoles nr s
fl RightId i
ir) =
    LeftId i
-> BothHoles ('S 'Z) nr s
-> RightId i
-> TypedScore ('S ('S 'Z)) ('S nr) s i
forall i (nl :: Nat) (nr :: Nat) s.
LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
SBoth LeftId i
newil ((s -> RightHoles ('S 'Z) s -> RightHoles ('S 'Z) s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
`appendRight` s -> RightHoles 'Z s -> RightHoles ('S 'Z) s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight s
op (s -> RightHoles 'Z s
forall s. Semiring s => s -> RightHoles 'Z s
mkRightHole s
forall a. Semiring a => a
R.one)) (s -> RightHoles ('S 'Z) s)
-> LeftHoles nr s -> BothHoles ('S 'Z) nr s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeftHoles nr s
fl) RightId i
ir
  unwrap (SBoth LeftId i
_ BothHoles nl nr s
fb RightId i
ir) = LeftId i
-> BothHoles ('S nl) nr s
-> RightId i
-> TypedScore ('S ('S nl)) ('S nr) s i
forall i (nl :: Nat) (nr :: Nat) s.
LeftId i
-> BothHoles nl nr s -> RightId i -> TypedScore ('S nl) ('S nr) s i
SBoth LeftId i
newil (s -> RightHoles nl s -> RightHoles ('S nl) s
forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight s
op (RightHoles nl s -> RightHoles ('S nl) s)
-> BothHoles nl nr s -> BothHoles ('S nl) nr s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BothHoles nl nr s
fb) RightId i
ir