{-# 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
forall i. Eq i => LeftId i -> LeftId i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LeftId i -> LeftId i -> Bool
$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
Eq, 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
min :: LeftId i -> LeftId i -> LeftId i
$cmin :: forall i. Ord i => LeftId i -> LeftId i -> LeftId i
max :: LeftId i -> LeftId i -> LeftId i
$cmax :: forall i. Ord i => LeftId i -> LeftId i -> LeftId i
>= :: 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
$c< :: forall i. Ord i => LeftId i -> LeftId i -> Bool
compare :: LeftId i -> LeftId i -> Ordering
$ccompare :: forall i. Ord i => LeftId i -> LeftId i -> Ordering
Ord, 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
$cto :: forall i x. Rep (LeftId i) x -> LeftId i
$cfrom :: forall i x. LeftId i -> Rep (LeftId i) x
Generic, LeftId i -> ()
forall i. NFData i => LeftId i -> ()
forall a. (a -> ()) -> NFData a
rnf :: LeftId i -> ()
$crnf :: forall i. NFData i => LeftId i -> ()
NFData, 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
hash :: LeftId i -> Int
$chash :: forall i. Hashable i => LeftId i -> Int
hashWithSalt :: Int -> LeftId i -> Int
$chashWithSalt :: forall i. Hashable i => Int -> LeftId i -> Int
Hashable)

instance Show i => Show (LeftId i) where
  show :: LeftId i -> String
show (LeftId i
i) = 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
forall i. Eq i => RightId i -> RightId i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RightId i -> RightId i -> Bool
$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
Eq, 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
min :: RightId i -> RightId i -> RightId i
$cmin :: forall i. Ord i => RightId i -> RightId i -> RightId i
max :: RightId i -> RightId i -> RightId i
$cmax :: forall i. Ord i => RightId i -> RightId i -> RightId i
>= :: 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
$c< :: forall i. Ord i => RightId i -> RightId i -> Bool
compare :: RightId i -> RightId i -> Ordering
$ccompare :: forall i. Ord i => RightId i -> RightId i -> Ordering
Ord, 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
$cto :: forall i x. Rep (RightId i) x -> RightId i
$cfrom :: forall i x. RightId i -> Rep (RightId i) x
Generic, RightId i -> ()
forall i. NFData i => RightId i -> ()
forall a. (a -> ()) -> NFData a
rnf :: RightId i -> ()
$crnf :: forall i. NFData i => RightId i -> ()
NFData, 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
hash :: RightId i -> Int
$chash :: forall i. Hashable i => RightId i -> Int
hashWithSalt :: Int -> RightId i -> Int
$chashWithSalt :: forall i. Hashable i => Int -> RightId i -> Int
Hashable)

instance Show i => Show (RightId i) where
  show :: RightId i -> String
show (RightId i
i) = 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 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) = forall a. NFData a => a -> ()
rnf RightHoles n s
f
  rnf (RightEnd 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) = forall a. NFData a => a -> ()
rnf s
s
  rnf (SRight LeftId i
i RightHoles nl s
_) = forall a. NFData a => a -> ()
rnf LeftId i
i
  rnf (SLeft LeftHoles nr s
_ RightId i
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 forall a b. NFData a => a -> b -> b
`deepseq` 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) = 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 = 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 (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
_)) = forall a. Maybe a
Nothing
leftSide (MkScore SNat nl
_ SNat nr
_ (SLeft LeftHoles nr s
_ RightId i
_)) = forall a. Maybe a
Nothing
leftSide (MkScore SNat nl
_ SNat nr
_ (SRight LeftId i
i RightHoles nl s
_)) = 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
_)) = 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
_)) = forall a. Maybe a
Nothing
rightSide (MkScore SNat nl
_ SNat nr
_ (SLeft LeftHoles nr s
_ RightId i
i)) = forall a. a -> Maybe a
Just RightId i
i
rightSide (MkScore SNat nl
_ SNat nr
_ (SRight LeftId i
_ RightHoles nl s
_)) = forall a. Maybe a
Nothing
rightSide (MkScore SNat nl
_ SNat nr
_ (SBoth LeftId i
_ BothHoles nl nr s
_ RightId i
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
"()-" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show RightId i
ir
  show (SRight LeftId i
il RightHoles nl s
_) = forall a. Show a => a -> String
show LeftId i
il forall a. Semigroup a => a -> a -> a
<> String
"-()"
  show (SBoth LeftId i
il BothHoles nl nr s
_ RightId i
ir) = forall a. Show a => a -> String
show LeftId i
il forall a. Semigroup a => a -> a -> a
<> String
"-" forall a. Semigroup a => a -> a -> a
<> 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) = 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) = forall a. Show a => a -> String
show s
v
showTScore (SLeft LeftHoles nr s
_ RightId i
ir) = String
"()-" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show RightId i
ir
showTScore (SRight LeftId i
il RightHoles nl s
_) = forall a. Show a => a -> String
show LeftId i
il forall a. Semigroup a => a -> a -> a
<> String
"-()"
showTScore (SBoth LeftId i
il BothHoles nl nr s
_ RightId i
ir) = forall a. Show a => a -> String
show LeftId i
il forall a. Semigroup a => a -> a -> a
<> String
"-" forall a. Semigroup a => a -> a -> a
<> 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) = 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 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) = forall s. s -> RightHole 'Z s
RightEnd forall a b. (a -> b) -> a -> b
$ s
r forall a. Semiring a => a -> a -> a
R.* s
s'
  app (RightHole RightHoles n s
fr') = forall (nl :: Nat) s. RightHoles nl s -> RightHole ('S nl) s
RightHole forall a b. (a -> b) -> a -> b
$ 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 R.*) 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 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) = forall s. s -> RightHole 'Z s
RightEnd forall a b. (a -> b) -> a -> b
$ s
s forall a. Semiring a => a -> a -> a
R.* s
r
  prep (RightHole RightHoles n s
fr') = forall (nl :: Nat) s. RightHoles nl s -> RightHole ('S nl) s
RightHole forall a b. (a -> b) -> a -> b
$ 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall s i. s -> TypedScore 'Z 'Z s i
SVal forall a b. (a -> b) -> a -> b
$ s
s1 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 forall a. Eq a => RightId a -> LeftId a -> Bool
`match` LeftId i
ir = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall s i. s -> TypedScore 'Z 'Z s i
SVal forall a b. (a -> b) -> a -> b
$ LeftHoles nr s
fl RightHoles nl s
fr
-- creates right
times (SRight LeftId i
i RightHoles nl s
r) (SVal s
s) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
i forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => RightId a -> LeftId a -> Bool
`match` LeftId i
i = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
il forall a b. (a -> b) -> a -> b
$ BothHoles nl nr s
fb RightHoles nl s
fr
-- creates left
times (SVal s
s) (SLeft LeftHoles nr s
fl RightId i
i) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (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 forall a. Eq a => RightId a -> LeftId a -> Bool
`match` LeftId i
il = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (LeftHoles nr s
fl forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! 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 ((forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
`appendRight` RightHoles nl s
fr) 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 forall a. Eq a => RightId a -> LeftId a -> Bool
`match` LeftId i
ib =
      forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. BothHoles nl nr s
fb) RightId i
ir
-- otherwise
times TypedScore nl n s i
_ TypedScore n 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) -> forall s. s -> RightHole 'Z s
RightEnd forall a b. (a -> b) -> a -> b
$ s
e1 forall a. Semiring a => a -> a -> a
R.+ s
e2
  (RightHole RightHoles n s
f1, RightHole RightHoles n s
f2) -> forall (nl :: Nat) s. RightHoles nl s -> RightHole ('S nl) s
RightHole forall a b. (a -> b) -> a -> b
$ forall s (n :: Nat).
Semiring s =>
RightHoles n s -> RightHoles n s -> RightHoles n s
rhplus RightHoles n s
f1 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall s i. s -> TypedScore 'Z 'Z s i
SVal forall a b. (a -> b) -> a -> b
$ s
s1 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 forall a. Eq a => a -> a -> Bool
== LeftId i
i' =
      forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
i forall a b. (a -> b) -> a -> b
$ forall s (n :: Nat).
Semiring s =>
RightHoles n s -> RightHoles n s -> RightHoles n s
rhplus RightHoles nl s
fr1 RightHoles nl s
fr2
plus (SLeft LeftHoles nr s
fl1 RightId i
i) (SLeft LeftHoles nr s
fl2 RightId i
i')
  | RightId i
i forall a. Eq a => a -> a -> Bool
== RightId i
i' =
      forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! 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 forall a. Semiring a => a -> a -> a
R.+ LeftHoles nr s
fl2 RightHoles 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 forall a. Eq a => a -> a -> Bool
== LeftId i
il' Bool -> Bool -> Bool
&& RightId i
ir forall a. Eq a => a -> a -> Bool
== RightId i
ir' =
      forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! 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 -> 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
r)) RightId i
ir
plus TypedScore nl nr s i
_ 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 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 = forall (nl :: Nat) s. RightHoles nl s -> RightHole ('S nl) s
RightHole forall a b. (a -> b) -> a -> b
$ forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
prependRight (s
l 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 = forall s. s -> RightHole 'Z s
RightEnd forall a b. (a -> b) -> a -> b
$ s
l 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 = 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 = 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 = AddHole n => r
r
canAddHole SNat n
SS AddHole n => 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
_ = 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) = 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 = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error String
"illegal plus") forall a b. (a -> b) -> a -> b
$ do
    nl :~: nl
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat nl
nla SNat nl
nlb
    nr :~: nr
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat nr
nra SNat nr
nrb
    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 TypedScore nl nr s i
a TypedScore nl nr s i
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) =
  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 forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe TypedScore nl nr s i
err forall a b. (a -> b) -> a -> b
$ do
    nr :~: nl
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat nr
nrl SNat nl
nlr
    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 (forall (nl :: Nat) (nr :: Nat).
TypedScore nl nr s i -> TypedScore nl nr s i
prep TypedScore nl nr s i
left) TypedScore nl nr s i
right
 where
  err :: TypedScore nl nr s i
err =
    forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
      String
"Attempting illegal unsplit: left="
        forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show TypedScore nl nr s i
left
        forall a. Semigroup a => a -> a -> a
<> String
", right="
        forall a. Semigroup a => a -> a -> a
<> 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 -> forall s i. s -> TypedScore 'Z 'Z s i
SVal (s
op forall a. Semiring a => a -> a -> a
R.* s
s)
    SLeft LeftHoles nr s
fl RightId i
i -> forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (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 -> forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
i (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 -> 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 (forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
prependRight s
op 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) =
  forall (n :: Nat) r. SNat n -> (AddHole n => r) -> r
canAddHole SNat nr
nr forall a b. (a -> b) -> a -> b
$ forall (nl :: Nat) (nr :: Nat) s i.
SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
MkScore SNat 'Z
SZ (forall (n :: Nat). AddHole n => SNat n -> SNat (CreateHole n)
addHole SNat nr
nr) forall a b. (a -> b) -> a -> b
$ forall (nr :: Nat).
TypedScore 'Z nr s i -> TypedScore 'Z (CreateHole nr) s i
wrap TypedScore nl nr s i
s
 where
  newir :: RightId i
newir = 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) = forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (forall s (n :: Nat). s -> LeftHoles n s -> LeftHoles ('S n) s
addHoleLeft forall a. Semiring a => a
R.one forall a b. (a -> b) -> a -> b
$ forall s. s -> LeftHoles 'Z s
mkLeftHole s
v) RightId i
newir
  wrap (SLeft LeftHoles nr s
fl RightId i
_) = forall (nl :: Nat) s i.
LeftHoles nl s -> RightId i -> TypedScore 'Z ('S nl) s i
SLeft (forall s (n :: Nat). s -> LeftHoles n s -> LeftHoles ('S n) s
addHoleLeft 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) =
  forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Attempting illegal left-unspread on " forall a. Semigroup a => a -> a -> a
<> 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) =
  forall (n :: Nat) r. SNat n -> (AddHole n => r) -> r
canAddHole SNat nl
nlm forall a b. (a -> b) -> a -> b
$ forall (nl :: Nat) (nr :: Nat) s i.
SNat nl -> SNat nr -> TypedScore nl nr s i -> Score s i
MkScore (forall (n :: Nat). AddHole n => SNat n -> SNat (CreateHole n)
addHole SNat nl
nlm) SNat nr
nrr forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe TypedScore (CreateHole nl) nr s i
err forall a b. (a -> b) -> a -> b
$ do
    nr :~: nl
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat nr
nrm SNat nl
nlr
    TypedScore nl nr s i
mr <- 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 TypedScore nl nr s i
m TypedScore nl nr s i
r
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (nl :: Nat) (nr :: Nat).
TypedScore nl nr s i -> TypedScore (CreateHole nl) nr s i
unwrap TypedScore nl nr s i
mr
 where
  err :: TypedScore (CreateHole nl) nr s i
err =
    forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
      String
"Attempting illegal right-unspread: m="
        forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show TypedScore nl nr s i
m
        forall a. Semigroup a => a -> a -> a
<> String
", r="
        forall a. Semigroup a => a -> a -> a
<> 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 = 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) = forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
newil forall a b. (a -> b) -> a -> b
$ forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight s
op forall a b. (a -> b) -> a -> b
$ forall s. Semiring s => s -> RightHoles 'Z s
mkRightHole s
s -- [op, s]
  unwrap (SRight LeftId i
_ RightHoles nl s
rs) = forall i (nl :: Nat) s.
LeftId i -> RightHoles nl s -> TypedScore ('S nl) 'Z s i
SRight LeftId i
newil (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) =
    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 ((forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles n s
`appendRight` forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight s
op (forall s. Semiring s => s -> RightHoles 'Z s
mkRightHole forall a. Semiring a => a
R.one)) 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) = 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 (forall s (n :: Nat).
Semiring s =>
s -> RightHoles n s -> RightHoles ('S n) s
addHoleRight s
op forall b c a. (b -> c) -> (a -> b) -> a -> c
. BothHoles nl nr s
fb) RightId i
ir