{-# LANGUAGE PatternSynonyms #-}
{-|
Module      : Parsley.Internal.Backend.Machine.LetBindings
Description : Let-binding and free registers.
License     : BSD-3-Clause
Maintainer  : Jamie Willis
Stability   : experimental

Definitions for various encapsulating datatypes for machines, and defining
free registers.

@since 1.0.0.0
-}
module Parsley.Internal.Backend.Machine.LetBindings (
    LetBinding(..), Metadata,
    Regs(..),
    makeLetBinding, newMeta,
    successInputCharacteristic, failureInputCharacteristic,
    Binding
  ) where

import Prelude hiding                                             (foldr)
import Data.Kind                                                  (Type)
import Data.Set                                                   (Set, foldr)
import Data.Some                                                  (Some, pattern Some)
import Parsley.Internal.Backend.Machine.Identifiers               (ΣVar, SomeΣVar(..))
import Parsley.Internal.Backend.Machine.Instructions              (Instr)
import Parsley.Internal.Backend.Machine.Types.InputCharacteristic (InputCharacteristic(..))
import Parsley.Internal.Common                                    (Fix4, One)

{-|
Type represents a binding, which is a completed parser that can
be refered to by other parsers. This is characterised by requiring
no initial stack and exactly one handler. The top-level binding is
the one of type @`Binding` o a a@.

@since 1.0.0.0
-}
type Binding o a x = Fix4 (Instr o) '[] One x a

{-|
Packages a binding along with its free registers that are required
for it, which are left existential. This is possible since the `Regs`
datatype serves as a singleton-style witness of the original registers
and their types. It also requires `Metadata` to be provided, sourced
from analysis.

@since 1.5.0.0
-}
data LetBinding o a x = LetBinding {
    forall o a x. LetBinding o a x -> Binding o a x
body :: Binding o a x,
    forall o a x. LetBinding o a x -> Some Regs
freeRegs :: Some Regs,
    forall o a x. LetBinding o a x -> Metadata
meta :: Metadata
  }

{- |
This is used to store useful static information that can be
used to guide code generation.

See `successInputCharacteristic`, and `failureInputCharacteristic`.

@since 1.5.0.0
-}
data Metadata = Metadata {
    {- |
    Characterises the way that a binding consumes input on success.

    @since 1.5.0.0
    -}
    Metadata -> InputCharacteristic
successInputCharacteristic :: !InputCharacteristic,
    {- |
    Characterises the way that a binding consumes input on failure.

    @since 1.5.0.0
    -}
    Metadata -> InputCharacteristic
failureInputCharacteristic :: !InputCharacteristic
  }

{-|
Given a `Binding` , a set of existential `ΣVar`s, and some `Metadata`, produces a
`LetBinding` instance.

@since 1.5.0.0
-}
makeLetBinding :: Binding o a x -> Set SomeΣVar -> Metadata -> LetBinding o a x
makeLetBinding :: forall o a x.
Binding o a x -> Set SomeΣVar -> Metadata -> LetBinding o a x
makeLetBinding Binding o a x
m Set SomeΣVar
rs = forall o a x.
Binding o a x -> Some Regs -> Metadata -> LetBinding o a x
LetBinding Binding o a x
m (Set SomeΣVar -> Some Regs
makeRegs Set SomeΣVar
rs)

{-|
Produces a new `Metadata` object, with fields initialised to sensible conservative
defaults.

@since 1.5.0.0
-}
newMeta :: Metadata
newMeta :: Metadata
newMeta = Metadata {
    successInputCharacteristic :: InputCharacteristic
successInputCharacteristic = InputCharacteristic
MayConsume,
    failureInputCharacteristic :: InputCharacteristic
failureInputCharacteristic = InputCharacteristic
MayConsume
  }

{-|
Represents a collection of free registers, preserving their type
information as a heterogeneous list.

@since 1.0.0.0
-}
data Regs (rs :: [Type]) where
  NoRegs :: Regs '[]
  FreeReg :: ΣVar r -> Regs rs -> Regs (r : rs)

{-|
Converts a set of existential `ΣVar`s into an existential
heterogeneous list of free registers.

@since 1.4.0.0
-}
makeRegs :: Set SomeΣVar -> Some Regs
makeRegs :: Set SomeΣVar -> Some Regs
makeRegs = forall a b. (a -> b -> b) -> b -> Set a -> b
foldr (\(SomeΣVar ΣVar r
σ) (Some Regs a
rs) -> forall {k} (tag :: k -> Type) (a :: k). tag a -> Some tag
Some (forall r (rs :: [Type]). ΣVar r -> Regs rs -> Regs (r : rs)
FreeReg ΣVar r
σ Regs a
rs)) (forall {k} (tag :: k -> Type) (a :: k). tag a -> Some tag
Some Regs '[]
NoRegs)