{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}

-- |
-- Module      : OAlg.Homology.IO.FSequence
-- Description : sequneces with finite support
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- Total sequences according to a index with finite support, i.e only finite many values are not equal
-- to the default value.
--
-- The implementation is optimized for:
--
-- - retrieving the values by an index.
--
-- - values which may have a very time consuming evaluation. 
module OAlg.Entity.Sequence.FSequence
  (
    -- * FSequence
    FSequence(), Behavior(..), fsqIsEmpty
  , fsqxs, fsqx
  , fsqSpan, fsqMin, fsqMax, fsqD, fsqForm, fsqMakeStrict, fsqMakeLazy
  , fsqMap, fsqMapShift
  , fsqMapWithIndex, fsqMapWithIndexStrict, fsqMapWithIndexLazy
  , fsqFilter

    -- * Form
  , FSequenceForm(..), rdcFSequenceForm

    -- * Default Value
  , DefaultValue(..), isDefaultValue

    -- * Proposition
  , relHomogenRoot
  , prpFSequenceSpan
  , prpFSequence
  ) where

import Data.Typeable
import Data.List ((++),filter)
import Data.Foldable

import Data.Maybe

import OAlg.Prelude

import OAlg.Data.Tree
import OAlg.Data.Constructable

import OAlg.Entity.Sequence.PSequence

import OAlg.Structure.Fibred
import OAlg.Structure.Oriented
import OAlg.Structure.Additive
import OAlg.Structure.Number

--------------------------------------------------------------------------------
-- DefaultValue -

-- | defining a default for every index.
class DefaultValue d i x where
  defaultValue :: d -> i -> x

--------------------------------------------------------------------------------
-- isDefaultValue -

-- | test for being the default value according to the given index.
isDefaultValue :: (DefaultValue d i x, Eq x) => d -> (x,i) -> Bool
isDefaultValue :: forall d i x. (DefaultValue d i x, Eq x) => d -> (x, i) -> Bool
isDefaultValue d
d (x
x,i
i) = x
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== d -> i -> x
forall d i x. DefaultValue d i x => d -> i -> x
defaultValue d
d i
i

--------------------------------------------------------------------------------
-- FSeqenceForm -

-- | form for total sequences with finite support.
data FSequenceForm d i x = FSequenceForm d (PSequence i x)
  deriving (Int -> FSequenceForm d i x -> ShowS
[FSequenceForm d i x] -> ShowS
FSequenceForm d i x -> String
(Int -> FSequenceForm d i x -> ShowS)
-> (FSequenceForm d i x -> String)
-> ([FSequenceForm d i x] -> ShowS)
-> Show (FSequenceForm d i x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall d i x.
(Show d, Show x, Show i) =>
Int -> FSequenceForm d i x -> ShowS
forall d i x.
(Show d, Show x, Show i) =>
[FSequenceForm d i x] -> ShowS
forall d i x.
(Show d, Show x, Show i) =>
FSequenceForm d i x -> String
$cshowsPrec :: forall d i x.
(Show d, Show x, Show i) =>
Int -> FSequenceForm d i x -> ShowS
showsPrec :: Int -> FSequenceForm d i x -> ShowS
$cshow :: forall d i x.
(Show d, Show x, Show i) =>
FSequenceForm d i x -> String
show :: FSequenceForm d i x -> String
$cshowList :: forall d i x.
(Show d, Show x, Show i) =>
[FSequenceForm d i x] -> ShowS
showList :: [FSequenceForm d i x] -> ShowS
Show,FSequenceForm d i x -> FSequenceForm d i x -> Bool
(FSequenceForm d i x -> FSequenceForm d i x -> Bool)
-> (FSequenceForm d i x -> FSequenceForm d i x -> Bool)
-> Eq (FSequenceForm d i x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall d i x.
(Eq d, Eq x, Eq i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Bool
$c== :: forall d i x.
(Eq d, Eq x, Eq i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Bool
== :: FSequenceForm d i x -> FSequenceForm d i x -> Bool
$c/= :: forall d i x.
(Eq d, Eq x, Eq i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Bool
/= :: FSequenceForm d i x -> FSequenceForm d i x -> Bool
Eq,Eq (FSequenceForm d i x)
Eq (FSequenceForm d i x) =>
(FSequenceForm d i x -> FSequenceForm d i x -> Ordering)
-> (FSequenceForm d i x -> FSequenceForm d i x -> Bool)
-> (FSequenceForm d i x -> FSequenceForm d i x -> Bool)
-> (FSequenceForm d i x -> FSequenceForm d i x -> Bool)
-> (FSequenceForm d i x -> FSequenceForm d i x -> Bool)
-> (FSequenceForm d i x
    -> FSequenceForm d i x -> FSequenceForm d i x)
-> (FSequenceForm d i x
    -> FSequenceForm d i x -> FSequenceForm d i x)
-> Ord (FSequenceForm d i x)
FSequenceForm d i x -> FSequenceForm d i x -> Bool
FSequenceForm d i x -> FSequenceForm d i x -> Ordering
FSequenceForm d i x -> FSequenceForm d i x -> FSequenceForm d i x
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 d i x. (Ord d, Ord x, Ord i) => Eq (FSequenceForm d i x)
forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Bool
forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Ordering
forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> FSequenceForm d i x
$ccompare :: forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Ordering
compare :: FSequenceForm d i x -> FSequenceForm d i x -> Ordering
$c< :: forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Bool
< :: FSequenceForm d i x -> FSequenceForm d i x -> Bool
$c<= :: forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Bool
<= :: FSequenceForm d i x -> FSequenceForm d i x -> Bool
$c> :: forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Bool
> :: FSequenceForm d i x -> FSequenceForm d i x -> Bool
$c>= :: forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> Bool
>= :: FSequenceForm d i x -> FSequenceForm d i x -> Bool
$cmax :: forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> FSequenceForm d i x
max :: FSequenceForm d i x -> FSequenceForm d i x -> FSequenceForm d i x
$cmin :: forall d i x.
(Ord d, Ord x, Ord i) =>
FSequenceForm d i x -> FSequenceForm d i x -> FSequenceForm d i x
min :: FSequenceForm d i x -> FSequenceForm d i x -> FSequenceForm d i x
Ord)

instance (Validable d, Entity i, Ord i, Entity x) => Validable (FSequenceForm d i x) where
  valid :: FSequenceForm d i x -> Statement
valid (FSequenceForm d
d PSequence i x
xs) = String -> Label
Label String
"FSequence"
    Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ d -> Statement
forall a. Validable a => a -> Statement
valid d
d
              , PSequence i x -> Statement
forall a. Validable a => a -> Statement
valid PSequence i x
xs
              ]

-- instance (Entity d, Entity i, Ord i, Entity x) => Entity (FSequenceForm d i x)

type instance Root (FSequenceForm d i x) = d

instance Show d => ShowRoot (FSequenceForm d i x)
instance Eq d => EqRoot (FSequenceForm d i x)
instance Validable d => ValidableRoot (FSequenceForm d i x)
instance Typeable d => TypeableRoot (FSequenceForm d i x)

instance (Entity d, Entity i, Ord i, Entity x) => Fibred (FSequenceForm d i x) where
  root :: FSequenceForm d i x -> Root (FSequenceForm d i x)
root (FSequenceForm d
d PSequence i x
_) = d
Root (FSequenceForm d i x)
d

--------------------------------------------------------------------------------
-- rdcFSequenceForm -

-- | reducing a sequence form, i.e. eliminates all default values according to the given index.
rdcFSequenceForm :: (DefaultValue d i x, Eq x) => FSequenceForm d i x -> FSequenceForm d i x
rdcFSequenceForm :: forall d i x.
(DefaultValue d i x, Eq x) =>
FSequenceForm d i x -> FSequenceForm d i x
rdcFSequenceForm (FSequenceForm d
d (PSequence [(x, i)]
xis)) = d -> PSequence i x -> FSequenceForm d i x
forall d i x. d -> PSequence i x -> FSequenceForm d i x
FSequenceForm d
d ([(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence [(x, i)]
xis') where
  xis' :: [(x, i)]
xis' = ((x, i) -> Bool) -> [(x, i)] -> [(x, i)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> ((x, i) -> Bool) -> (x, i) -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. d -> (x, i) -> Bool
forall d i x. (DefaultValue d i x, Eq x) => d -> (x, i) -> Bool
isDefaultValue d
d) [(x, i)]
xis

--------------------------------------------------------------------------------
-- Behavior -

-- | the evaluation behavior of a 'FSequence'.
data Behavior = Strict | Lazy deriving (Int -> Behavior -> ShowS
[Behavior] -> ShowS
Behavior -> String
(Int -> Behavior -> ShowS)
-> (Behavior -> String) -> ([Behavior] -> ShowS) -> Show Behavior
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Behavior -> ShowS
showsPrec :: Int -> Behavior -> ShowS
$cshow :: Behavior -> String
show :: Behavior -> String
$cshowList :: [Behavior] -> ShowS
showList :: [Behavior] -> ShowS
Show,Behavior -> Behavior -> Bool
(Behavior -> Behavior -> Bool)
-> (Behavior -> Behavior -> Bool) -> Eq Behavior
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Behavior -> Behavior -> Bool
== :: Behavior -> Behavior -> Bool
$c/= :: Behavior -> Behavior -> Bool
/= :: Behavior -> Behavior -> Bool
Eq,Eq Behavior
Eq Behavior =>
(Behavior -> Behavior -> Ordering)
-> (Behavior -> Behavior -> Bool)
-> (Behavior -> Behavior -> Bool)
-> (Behavior -> Behavior -> Bool)
-> (Behavior -> Behavior -> Bool)
-> (Behavior -> Behavior -> Behavior)
-> (Behavior -> Behavior -> Behavior)
-> Ord Behavior
Behavior -> Behavior -> Bool
Behavior -> Behavior -> Ordering
Behavior -> Behavior -> Behavior
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
$ccompare :: Behavior -> Behavior -> Ordering
compare :: Behavior -> Behavior -> Ordering
$c< :: Behavior -> Behavior -> Bool
< :: Behavior -> Behavior -> Bool
$c<= :: Behavior -> Behavior -> Bool
<= :: Behavior -> Behavior -> Bool
$c> :: Behavior -> Behavior -> Bool
> :: Behavior -> Behavior -> Bool
$c>= :: Behavior -> Behavior -> Bool
>= :: Behavior -> Behavior -> Bool
$cmax :: Behavior -> Behavior -> Behavior
max :: Behavior -> Behavior -> Behavior
$cmin :: Behavior -> Behavior -> Behavior
min :: Behavior -> Behavior -> Behavior
Ord,Int -> Behavior
Behavior -> Int
Behavior -> [Behavior]
Behavior -> Behavior
Behavior -> Behavior -> [Behavior]
Behavior -> Behavior -> Behavior -> [Behavior]
(Behavior -> Behavior)
-> (Behavior -> Behavior)
-> (Int -> Behavior)
-> (Behavior -> Int)
-> (Behavior -> [Behavior])
-> (Behavior -> Behavior -> [Behavior])
-> (Behavior -> Behavior -> [Behavior])
-> (Behavior -> Behavior -> Behavior -> [Behavior])
-> Enum Behavior
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Behavior -> Behavior
succ :: Behavior -> Behavior
$cpred :: Behavior -> Behavior
pred :: Behavior -> Behavior
$ctoEnum :: Int -> Behavior
toEnum :: Int -> Behavior
$cfromEnum :: Behavior -> Int
fromEnum :: Behavior -> Int
$cenumFrom :: Behavior -> [Behavior]
enumFrom :: Behavior -> [Behavior]
$cenumFromThen :: Behavior -> Behavior -> [Behavior]
enumFromThen :: Behavior -> Behavior -> [Behavior]
$cenumFromTo :: Behavior -> Behavior -> [Behavior]
enumFromTo :: Behavior -> Behavior -> [Behavior]
$cenumFromThenTo :: Behavior -> Behavior -> Behavior -> [Behavior]
enumFromThenTo :: Behavior -> Behavior -> Behavior -> [Behavior]
Enum)

--------------------------------------------------------------------------------
-- FSequcne -

-- | total sequence according to the index @__i__@ with finite support, i.e only finite many values
-- are not equal to the default value according to a given index.
--
-- It comes with to /flavors/ which defines the behavior of creating the sequence via 'make':
--
-- 'Strict': eliminates all default values from the form to create the sequence. In this case for
-- example the testing of equality is efficient.
--
-- 'Lazy': takes all the values form the form to create the sequence. In this case for example
-- the testing of equality is less efficient.
--
-- Both /flavors/ have equal 'form's.
data FSequence s d i x where
  FSequenceStrict :: d -> PTree i x -> FSequence Strict d i x
  FSequenceLazy   :: d -> PTree i x -> FSequence Lazy d i x

deriving instance Foldable (FSequence s d i)

--------------------------------------------------------------------------------
-- fsqD -

-- | the underlying definition.
fsqD :: FSequence s d i x -> d
fsqD :: forall (s :: Behavior) d i x. FSequence s d i x -> d
fsqD (FSequenceStrict d
d PTree i x
_) = d
d
fsqD (FSequenceLazy d
d PTree i x
_)   = d
d

--------------------------------------------------------------------------------
-- fsqT -

-- | the underlying tree.
fsqT :: FSequence s d i x -> PTree i x
fsqT :: forall (s :: Behavior) d i x. FSequence s d i x -> PTree i x
fsqT (FSequenceStrict d
_ PTree i x
t) = PTree i x
t
fsqT (FSequenceLazy d
_ PTree i x
t)   = PTree i x
t

--------------------------------------------------------------------------------
-- fsqIsEmpty -

-- | testing the first entry of being empty.
fsqIsEmpty :: (DefaultValue d i x, Eq x) => FSequence s d i x -> Bool
fsqIsEmpty :: forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> Bool
fsqIsEmpty FSequence s d i x
f = PSequence i x -> Bool
forall i x. PSequence i x -> Bool
psqIsEmpty PSequence i x
xis where FSequenceForm d
_ PSequence i x
xis = FSequence s d i x -> Form (FSequence s d i x)
forall x. Exposable x => x -> Form x
form FSequence s d i x
f

--------------------------------------------------------------------------------
-- fsqx -

-- | retrieving a value according to a given index.
fsqx :: (DefaultValue d i x, Ord i) => FSequence s d i x -> i -> x
fsqx :: forall d i x (s :: Behavior).
(DefaultValue d i x, Ord i) =>
FSequence s d i x -> i -> x
fsqx FSequence s d i x
xs i
i = case PTree i x -> i -> Maybe x
forall i x. Ord i => PTree i x -> i -> Maybe x
ptrx (FSequence s d i x -> PTree i x
forall (s :: Behavior) d i x. FSequence s d i x -> PTree i x
fsqT FSequence s d i x
xs) i
i of
  Just x
x  -> x
x
  Maybe x
Nothing -> d -> i -> x
forall d i x. DefaultValue d i x => d -> i -> x
defaultValue (FSequence s d i x -> d
forall (s :: Behavior) d i x. FSequence s d i x -> d
fsqD FSequence s d i x
xs) i
i

--------------------------------------------------------------------------------
-- fsqMin -

-- | the minimal index.
fsqMin :: (DefaultValue d i x, Eq x, Ord i) => FSequence s d i x -> Closure i
fsqMin :: forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x, Ord i) =>
FSequence s d i x -> Closure i
fsqMin (FSequenceStrict d
_ PTree i x
t)              = PTree i x -> Closure i
forall i x. PTree i x -> Closure i
ptrMin PTree i x
t
fsqMin (FSequenceLazy d
_ (PTree Maybe (Tree i (x, i))
Nothing))  = Closure i
forall x. Closure x
PosInf
fsqMin (FSequenceLazy d
d (PTree (Just Tree i (x, i)
t))) = Closure i -> Tree i (x, i) -> Closure i
tmin Closure i
forall x. Closure x
PosInf Tree i (x, i)
t where
  tmin :: Closure i -> Tree i (x, i) -> Closure i
tmin Closure i
m (Leaf xi :: (x, i)
xi@(x
_,i
i)) = if d -> (x, i) -> Bool
forall d i x. (DefaultValue d i x, Eq x) => d -> (x, i) -> Bool
isDefaultValue d
d (x, i)
xi then Closure i
m else Closure i -> Closure i -> Closure i
forall a. Ord a => a -> a -> a
min Closure i
m (i -> Closure i
forall x. x -> Closure x
It i
i)
  tmin Closure i
m (Node i
_ Tree i (x, i)
l Tree i (x, i)
r)    = if Closure i
ml Closure i -> Closure i -> Bool
forall a. Ord a => a -> a -> Bool
< Closure i
m then Closure i
ml else Closure i -> Tree i (x, i) -> Closure i
tmin Closure i
m Tree i (x, i)
r where ml :: Closure i
ml = Closure i -> Tree i (x, i) -> Closure i
tmin Closure i
m Tree i (x, i)
l 

--------------------------------------------------------------------------------
-- fsqMax -

-- | the maxiaml index.
fsqMax :: (DefaultValue d i x, Eq x, Ord i) => FSequence s d i x -> Closure i
fsqMax :: forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x, Ord i) =>
FSequence s d i x -> Closure i
fsqMax (FSequenceStrict d
_ PTree i x
t) = PTree i x -> Closure i
forall i x. PTree i x -> Closure i
ptrMax PTree i x
t
fsqMax (FSequenceLazy d
_ (PTree Maybe (Tree i (x, i))
Nothing))  = Closure i
forall x. Closure x
NegInf
fsqMax (FSequenceLazy d
d (PTree (Just Tree i (x, i)
t))) = Closure i -> Tree i (x, i) -> Closure i
tmax Closure i
forall x. Closure x
NegInf Tree i (x, i)
t where
  tmax :: Closure i -> Tree i (x, i) -> Closure i
tmax Closure i
m (Leaf xi :: (x, i)
xi@(x
_,i
i)) = if d -> (x, i) -> Bool
forall d i x. (DefaultValue d i x, Eq x) => d -> (x, i) -> Bool
isDefaultValue d
d (x, i)
xi then Closure i
m else Closure i -> Closure i -> Closure i
forall a. Ord a => a -> a -> a
max Closure i
m (i -> Closure i
forall x. x -> Closure x
It i
i)
  tmax Closure i
m (Node i
_ Tree i (x, i)
l Tree i (x, i)
r)    = if Closure i
mr Closure i -> Closure i -> Bool
forall a. Ord a => a -> a -> Bool
> Closure i
m then Closure i
mr else Closure i -> Tree i (x, i) -> Closure i
tmax Closure i
m Tree i (x, i)
l where mr :: Closure i
mr = Closure i -> Tree i (x, i) -> Closure i
tmax Closure i
m Tree i (x, i)
r 

--------------------------------------------------------------------------------
-- fsqSpan -

-- | the support, i.e the minimal and the maximal index of the 'FSequence'.
fsqSpan :: (DefaultValue d i x, Eq x, Ord i) => FSequence s d i x -> Span i
fsqSpan :: forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x, Ord i) =>
FSequence s d i x -> Span i
fsqSpan FSequence s d i x
f = (FSequence s d i x -> Closure i
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x, Ord i) =>
FSequence s d i x -> Closure i
fsqMin FSequence s d i x
f,FSequence s d i x -> Closure i
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x, Ord i) =>
FSequence s d i x -> Closure i
fsqMax FSequence s d i x
f)

--------------------------------------------------------------------------------
-- fsqFilter -

-- | the sub sequence all values satisfying the given predicate.
fsqFilter :: (x -> Bool) -> FSequence s d i x -> FSequence s d i x
fsqFilter :: forall x (s :: Behavior) d i.
(x -> Bool) -> FSequence s d i x -> FSequence s d i x
fsqFilter x -> Bool
p FSequence s d i x
xis = case FSequence s d i x
xis of
  FSequenceStrict d
d PTree i x
t -> d -> PTree i x -> FSequence 'Strict d i x
forall d i x. d -> PTree i x -> FSequence 'Strict d i x
FSequenceStrict d
d ((x -> Bool) -> PTree i x -> PTree i x
forall x i. (x -> Bool) -> PTree i x -> PTree i x
ptrFilter x -> Bool
p PTree i x
t)
  FSequenceLazy d
d PTree i x
t   -> d -> PTree i x -> FSequence 'Lazy d i x
forall d i x. d -> PTree i x -> FSequence 'Lazy d i x
FSequenceLazy d
d ((x -> Bool) -> PTree i x -> PTree i x
forall x i. (x -> Bool) -> PTree i x -> PTree i x
ptrFilter x -> Bool
p PTree i x
t)

--------------------------------------------------------------------------------
-- fsqMapWithIndex -

-- | maps a sequence according to the given mappings.
fsqMapWithIndexStrict :: (DefaultValue e j y, Eq y)
  => (d -> e) -> Monotone i j -> ((x,i) -> y) -> FSequence Strict d i x -> FSequence Strict e j y
fsqMapWithIndexStrict :: forall e j y d i x.
(DefaultValue e j y, Eq y) =>
(d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence 'Strict d i x
-> FSequence 'Strict e j y
fsqMapWithIndexStrict d -> e
e Monotone i j
j (x, i) -> y
y (FSequenceStrict d
d PTree i x
t) = e -> PTree j y -> FSequence 'Strict e j y
forall d i x. d -> PTree i x -> FSequence 'Strict d i x
FSequenceStrict e
d' PTree j y
t' where
  d' :: e
d' = d -> e
e d
d
  t' :: PTree j y
t' = ((y, j) -> Bool) -> PTree j y -> PTree j y
forall x i. ((x, i) -> Bool) -> PTree i x -> PTree i x
ptrFilterWithIndex (Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> ((y, j) -> Bool) -> (y, j) -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. e -> (y, j) -> Bool
forall d i x. (DefaultValue d i x, Eq x) => d -> (x, i) -> Bool
isDefaultValue e
d') (PTree j y -> PTree j y) -> PTree j y -> PTree j y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Monotone i j -> ((x, i) -> y) -> PTree i x -> PTree j y
forall i j x y.
Monotone i j -> ((x, i) -> y) -> PTree i x -> PTree j y
ptrMapWithIndex Monotone i j
j (x, i) -> y
y PTree i x
t

-- | maps a sequence according to the given mappings.
fsqMapWithIndexLazy :: (d -> e) -> Monotone i j -> ((x,i) -> y)
  -> FSequence Lazy d i x -> FSequence Lazy e j y
fsqMapWithIndexLazy :: forall d e i j x y.
(d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence 'Lazy d i x
-> FSequence 'Lazy e j y
fsqMapWithIndexLazy d -> e
e Monotone i j
j (x, i) -> y
y (FSequenceLazy d
d PTree i x
t) = e -> PTree j y -> FSequence 'Lazy e j y
forall d i x. d -> PTree i x -> FSequence 'Lazy d i x
FSequenceLazy e
d' PTree j y
t' where
  d' :: e
d' = d -> e
e d
d
  t' :: PTree j y
t' = Monotone i j -> ((x, i) -> y) -> PTree i x -> PTree j y
forall i j x y.
Monotone i j -> ((x, i) -> y) -> PTree i x -> PTree j y
ptrMapWithIndex Monotone i j
j (x, i) -> y
y PTree i x
t

-- | maps a sequence according to the given mappings.
fsqMapWithIndex :: (DefaultValue e j y, Eq y)
  => (d -> e) -> Monotone i j -> ((x,i) -> y) -> FSequence s d i x -> FSequence s e j y
fsqMapWithIndex :: forall e j y d i x (s :: Behavior).
(DefaultValue e j y, Eq y) =>
(d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence s d i x
-> FSequence s e j y
fsqMapWithIndex d -> e
e Monotone i j
j (x, i) -> y
y FSequence s d i x
xis = case FSequence s d i x
xis of
  FSequenceStrict d
_ PTree i x
_ -> (d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence 'Strict d i x
-> FSequence 'Strict e j y
forall e j y d i x.
(DefaultValue e j y, Eq y) =>
(d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence 'Strict d i x
-> FSequence 'Strict e j y
fsqMapWithIndexStrict d -> e
e Monotone i j
j (x, i) -> y
y FSequence s d i x
FSequence 'Strict d i x
xis
  FSequenceLazy d
_ PTree i x
_   -> (d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence 'Lazy d i x
-> FSequence 'Lazy e j y
forall d e i j x y.
(d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence 'Lazy d i x
-> FSequence 'Lazy e j y
fsqMapWithIndexLazy d -> e
e Monotone i j
j (x, i) -> y
y FSequence s d i x
FSequence 'Lazy d i x
xis

--------------------------------------------------------------------------------
-- fsqMapShift -

-- | maps a sequence according to the given mappings.
fsqMapShift :: (DefaultValue e i y, Eq y, Number i)
  => (d -> e) -> i -> ((x,i) -> y) -> FSequence s d i x -> FSequence s e i y
fsqMapShift :: forall e i y d x (s :: Behavior).
(DefaultValue e i y, Eq y, Number i) =>
(d -> e)
-> i -> ((x, i) -> y) -> FSequence s d i x -> FSequence s e i y
fsqMapShift d -> e
e i
t = (d -> e)
-> Monotone i i
-> ((x, i) -> y)
-> FSequence s d i x
-> FSequence s e i y
forall e j y d i x (s :: Behavior).
(DefaultValue e j y, Eq y) =>
(d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence s d i x
-> FSequence s e j y
fsqMapWithIndex d -> e
e ((i -> i) -> Monotone i i
forall i j. (i -> j) -> Monotone i j
Monotone (i -> i -> i
forall a. Additive a => a -> a -> a
+i
t))

--------------------------------------------------------------------------------
-- fsqMap -

-- | maps a sequence according to the given mappings.
fsqMap :: (DefaultValue d i y, Eq y)
  => (x -> y) -> FSequence s d i x -> FSequence s d i y
fsqMap :: forall d i y x (s :: Behavior).
(DefaultValue d i y, Eq y) =>
(x -> y) -> FSequence s d i x -> FSequence s d i y
fsqMap x -> y
f = (d -> d)
-> Monotone i i
-> ((x, i) -> y)
-> FSequence s d i x
-> FSequence s d i y
forall e j y d i x (s :: Behavior).
(DefaultValue e j y, Eq y) =>
(d -> e)
-> Monotone i j
-> ((x, i) -> y)
-> FSequence s d i x
-> FSequence s e j y
fsqMapWithIndex d -> d
forall x. x -> x
id ((i -> i) -> Monotone i i
forall i j. (i -> j) -> Monotone i j
Monotone i -> i
forall x. x -> x
id) (x -> y
f (x -> y) -> ((x, i) -> x) -> (x, i) -> y
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (x, i) -> x
forall a b. (a, b) -> a
fst)

--------------------------------------------------------------------------------
-- fsqForm -

-- | the underlying form.
fsqForm :: (DefaultValue d i x, Eq x) => FSequence s d i x -> FSequenceForm d i x
fsqForm :: forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> FSequenceForm d i x
fsqForm (FSequenceStrict d
d PTree i x
t) = d -> PSequence i x -> FSequenceForm d i x
forall d i x. d -> PSequence i x -> FSequenceForm d i x
FSequenceForm d
d (PTree i x -> PSequence i x
forall i x. PTree i x -> PSequence i x
psqFromTree PTree i x
t)
fsqForm (FSequenceLazy d
d PTree i x
t)   = FSequenceForm d i x -> FSequenceForm d i x
forall d i x.
(DefaultValue d i x, Eq x) =>
FSequenceForm d i x -> FSequenceForm d i x
rdcFSequenceForm (FSequenceForm d i x -> FSequenceForm d i x)
-> FSequenceForm d i x -> FSequenceForm d i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d -> PSequence i x -> FSequenceForm d i x
forall d i x. d -> PSequence i x -> FSequenceForm d i x
FSequenceForm d
d (PTree i x -> PSequence i x
forall i x. PTree i x -> PSequence i x
psqFromTree PTree i x
t)

--------------------------------------------------------------------------------
-- fsqxs -

-- | the underlying list of non-default, indexed values, 
fsqxs :: (DefaultValue d i x, Eq x) => FSequence s d i x -> [(x,i)]
fsqxs :: forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> [(x, i)]
fsqxs FSequence s d i x
xis = PSequence i x -> [(x, i)]
forall i x. PSequence i x -> [(x, i)]
psqxs PSequence i x
xis' where FSequenceForm d
_ PSequence i x
xis' = FSequence s d i x -> FSequenceForm d i x
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> FSequenceForm d i x
fsqForm FSequence s d i x
xis

--------------------------------------------------------------------------------
-- fsqMakeStrict -

-- | makes a 'FSequence' with a strict behavior.
fsqMakeStrict :: (DefaultValue d i x, Eq x) => FSequenceForm d i x -> FSequence Strict d i x
fsqMakeStrict :: forall d i x.
(DefaultValue d i x, Eq x) =>
FSequenceForm d i x -> FSequence 'Strict d i x
fsqMakeStrict FSequenceForm d i x
f = d -> PTree i x -> FSequence 'Strict d i x
forall d i x. d -> PTree i x -> FSequence 'Strict d i x
FSequenceStrict d
d (PSequence i x -> PTree i x
forall i x. PSequence i x -> PTree i x
psqTree PSequence i x
xis) where
  FSequenceForm d
d PSequence i x
xis = FSequenceForm d i x -> FSequenceForm d i x
forall d i x.
(DefaultValue d i x, Eq x) =>
FSequenceForm d i x -> FSequenceForm d i x
rdcFSequenceForm FSequenceForm d i x
f

--------------------------------------------------------------------------------
-- fsqMakeLazy -

-- | makes a 'FSequence' with a lazy behavior.
fsqMakeLazy :: FSequenceForm d i x -> FSequence Lazy d i x
fsqMakeLazy :: forall d i x. FSequenceForm d i x -> FSequence 'Lazy d i x
fsqMakeLazy (FSequenceForm d
d PSequence i x
xis) = d -> PTree i x -> FSequence 'Lazy d i x
forall d i x. d -> PTree i x -> FSequence 'Lazy d i x
FSequenceLazy d
d (PSequence i x -> PTree i x
forall i x. PSequence i x -> PTree i x
psqTree PSequence i x
xis)

--------------------------------------------------------------------------------
-- FSequence - Entity -

instance (DefaultValue d i x,Eq x, Show d, Show i, Show x) => Show (FSequence s d i x) where
  show :: FSequence s d i x -> String
show FSequence s d i x
f = String
"FSequence (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ d -> String
forall a. Show a => a -> String
show d
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ PSequence i x -> String
forall a. Show a => a -> String
show PSequence i x
xis String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" where
    FSequenceForm d
d PSequence i x
xis = FSequence s d i x -> FSequenceForm d i x
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> FSequenceForm d i x
fsqForm FSequence s d i x
f


instance (DefaultValue d i x,Eq d, Eq i,Eq x) => Eq (FSequence s d i x) where
  FSequence s d i x
f == :: FSequence s d i x -> FSequence s d i x -> Bool
== FSequence s d i x
g = FSequence s d i x -> FSequenceForm d i x
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> FSequenceForm d i x
fsqForm FSequence s d i x
f FSequenceForm d i x -> FSequenceForm d i x -> Bool
forall a. Eq a => a -> a -> Bool
== FSequence s d i x -> FSequenceForm d i x
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> FSequenceForm d i x
fsqForm FSequence s d i x
g

instance (DefaultValue d i x,Ord d, Ord i,Ord x) => Ord (FSequence s d i x) where
  compare :: FSequence s d i x -> FSequence s d i x -> Ordering
compare FSequence s d i x
f FSequence s d i x
g = FSequenceForm d i x -> FSequenceForm d i x -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (FSequence s d i x -> FSequenceForm d i x
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> FSequenceForm d i x
fsqForm FSequence s d i x
f) (FSequence s d i x -> FSequenceForm d i x
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> FSequenceForm d i x
fsqForm FSequence s d i x
g)


instance (Entity d, Entity i, Entity x, Ord i) => Validable (FSequence s d i x) where
  valid :: FSequence s d i x -> Statement
valid FSequence s d i x
f = String -> Label
Label String
"FSequence" Label -> Statement -> Statement
:<=>: (d -> Statement
forall a. Validable a => a -> Statement
valid (d -> Statement) -> d -> Statement
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FSequence s d i x -> d
forall (s :: Behavior) d i x. FSequence s d i x -> d
fsqD FSequence s d i x
f) Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& (PTree i x -> Statement
forall a. Validable a => a -> Statement
valid (PTree i x -> Statement) -> PTree i x -> Statement
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FSequence s d i x -> PTree i x
forall (s :: Behavior) d i x. FSequence s d i x -> PTree i x
fsqT FSequence s d i x
f)

{-
instance (DefaultValue d i x, Entity d, Entity i, Entity x, Ord i, Typeable s)
  => Entity (FSequence s d i x)
-}

type instance Root (FSequence s d i x) = d

instance Show d => ShowRoot (FSequence s d i x)
instance Eq d => EqRoot (FSequence s d i x)
instance Validable d => ValidableRoot (FSequence s d i x)
instance Typeable d => TypeableRoot (FSequence s d i x)

instance (DefaultValue d i x, Entity d, Entity i, Entity x, Ord i, Typeable s)
  => Fibred (FSequence s d i x) where
  root :: FSequence s d i x -> Root (FSequence s d i x)
root = FSequence s d i x -> d
FSequence s d i x -> Root (FSequence s d i x)
forall (s :: Behavior) d i x. FSequence s d i x -> d
fsqD
  
--------------------------------------------------------------------------------
-- FSequence - Constructable -

instance (DefaultValue d i x, Eq x) => Exposable (FSequence s d i x) where
  type Form (FSequence s d i x) = FSequenceForm d i x
  form :: FSequence s d i x -> Form (FSequence s d i x)
form = FSequence s d i x -> Form (FSequence s d i x)
FSequence s d i x -> FSequenceForm d i x
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x) =>
FSequence s d i x -> FSequenceForm d i x
fsqForm

instance (DefaultValue d i x, Eq x) => Constructable (FSequence Strict d i x) where
  make :: Form (FSequence 'Strict d i x) -> FSequence 'Strict d i x
make = Form (FSequence 'Strict d i x) -> FSequence 'Strict d i x
FSequenceForm d i x -> FSequence 'Strict d i x
forall d i x.
(DefaultValue d i x, Eq x) =>
FSequenceForm d i x -> FSequence 'Strict d i x
fsqMakeStrict

instance (DefaultValue d i x, Eq x) => Constructable (FSequence Lazy d i x) where
  make :: Form (FSequence 'Lazy d i x) -> FSequence 'Lazy d i x
make = Form (FSequence 'Lazy d i x) -> FSequence 'Lazy d i x
FSequenceForm d i x -> FSequence 'Lazy d i x
forall d i x. FSequenceForm d i x -> FSequence 'Lazy d i x
fsqMakeLazy

--------------------------------------------------------------------------------
-- DefaultZeroValue -

newtype DefaultZeroValue a = DefaultZeroValue (Root a)

deriving instance Fibred a => Show (DefaultZeroValue a)
deriving instance Fibred a => Eq (DefaultZeroValue a)
deriving instance (Fibred a, OrdRoot a) => Ord (DefaultZeroValue a)

instance Fibred a => Validable (DefaultZeroValue a) where
  valid :: DefaultZeroValue a -> Statement
valid (DefaultZeroValue Root a
r) = String -> Label
Label String
"DefaultZeroValue" Label -> Statement -> Statement
:<=>: Root a -> Statement
forall a. Validable a => a -> Statement
valid Root a
r

-- instance Fibred a => Entity (DefaultZeroValue a)

instance Additive a => DefaultValue (DefaultZeroValue a) i a where
  defaultValue :: DefaultZeroValue a -> i -> a
defaultValue (DefaultZeroValue Root a
r) i
_ = Root a -> a
forall a. Additive a => Root a -> a
zero Root a
r
  
--------------------------------------------------------------------------------
-- relHomogenRoot -

-- | relation for validating a 'FSequence' such that the 'root' of every element of the sequence
-- is equal to the 'root' of the default value according to the index.
relHomogenRoot :: (DefaultValue d i x, Fibred x, Show i) => FSequence s d i x -> Statement
relHomogenRoot :: forall d i x (s :: Behavior).
(DefaultValue d i x, Fibred x, Show i) =>
FSequence s d i x -> Statement
relHomogenRoot FSequence s d i x
f = case FSequence s d i x -> PTree i x
forall (s :: Behavior) d i x. FSequence s d i x -> PTree i x
fsqT FSequence s d i x
f of
  PTree Maybe (Tree i (x, i))
Nothing  -> Statement
SValid
  PTree (Just Tree i (x, i)
t) -> d -> Tree i (x, i) -> Statement
forall d i x.
(DefaultValue d i x, Fibred x, Show i) =>
d -> Tree i (x, i) -> Statement
vld (FSequence s d i x -> d
forall (s :: Behavior) d i x. FSequence s d i x -> d
fsqD FSequence s d i x
f) Tree i (x, i)
t where
    vld :: (DefaultValue d i x, Fibred x, Show i) => d -> Tree i (x,i) -> Statement
    vld :: forall d i x.
(DefaultValue d i x, Fibred x, Show i) =>
d -> Tree i (x, i) -> Statement
vld d
d (Leaf (x
x,i
i)) = x -> x -> Bool
forall x. Fibred x => x -> x -> Bool
eqRoot (d -> i -> x
forall d i x. DefaultValue d i x => d -> i -> x
defaultValue d
d i
i) x
x Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=i -> String
forall a. Show a => a -> String
show i
i,String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]
    vld d
d (Node i
_ Tree i (x, i)
l Tree i (x, i)
r) = d -> Tree i (x, i) -> Statement
forall d i x.
(DefaultValue d i x, Fibred x, Show i) =>
d -> Tree i (x, i) -> Statement
vld d
d Tree i (x, i)
l Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& d -> Tree i (x, i) -> Statement
forall d i x.
(DefaultValue d i x, Fibred x, Show i) =>
d -> Tree i (x, i) -> Statement
vld d
d Tree i (x, i)
r
    
    eqRoot :: Fibred x => x -> x -> Bool
    eqRoot :: forall x. Fibred x => x -> x -> Bool
eqRoot x
a x
b = x -> Root x
forall f. Fibred f => f -> Root f
root x
a Root x -> Root x -> Bool
forall a. Eq a => a -> a -> Bool
== x -> Root x
forall f. Fibred f => f -> Root f
root x
b

--------------------------------------------------------------------------------
-- prpFSequenceSpan -

-- | support of the two flavors are equal.
prpFSequenceSpan :: N -> Statement
prpFSequenceSpan :: N -> Statement
prpFSequenceSpan N
l = String -> Label
Prp (String
"FSequenceSpan " String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
l)
  Label -> Statement -> Statement
:<=>: X (FSequenceForm (DefaultZeroValue Z) N Z)
-> (FSequenceForm (DefaultZeroValue Z) N Z -> Statement)
-> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (N -> X (FSequenceForm (DefaultZeroValue Z) N Z)
xForm N
l) (\FSequenceForm (DefaultZeroValue Z) N Z
xis -> ((FSequence 'Strict (DefaultZeroValue Z) N Z -> Span N
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x, Ord i) =>
FSequence s d i x -> Span i
fsqSpan (FSequence 'Strict (DefaultZeroValue Z) N Z -> Span N)
-> FSequence 'Strict (DefaultZeroValue Z) N Z -> Span N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FSequenceForm (DefaultZeroValue Z) N Z
-> FSequence 'Strict (DefaultZeroValue Z) N Z
forall d i x.
(DefaultValue d i x, Eq x) =>
FSequenceForm d i x -> FSequence 'Strict d i x
fsqMakeStrict FSequenceForm (DefaultZeroValue Z) N Z
xis) Span N -> Span N -> Bool
forall a. Eq a => a -> a -> Bool
== (FSequence 'Lazy (DefaultZeroValue Z) N Z -> Span N
forall d i x (s :: Behavior).
(DefaultValue d i x, Eq x, Ord i) =>
FSequence s d i x -> Span i
fsqSpan (FSequence 'Lazy (DefaultZeroValue Z) N Z -> Span N)
-> FSequence 'Lazy (DefaultZeroValue Z) N Z -> Span N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FSequenceForm (DefaultZeroValue Z) N Z
-> FSequence 'Lazy (DefaultZeroValue Z) N Z
forall d i x. FSequenceForm d i x -> FSequence 'Lazy d i x
fsqMakeLazy FSequenceForm (DefaultZeroValue Z) N Z
xis))
                                       Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"xis"String -> String -> Parameter
:=FSequenceForm (DefaultZeroValue Z) N Z -> String
forall a. Show a => a -> String
show FSequenceForm (DefaultZeroValue Z) N Z
xis]
                         )
  where zForm :: PSequence N Z -> FSequenceForm (DefaultZeroValue Z) N Z
        zForm :: PSequence N Z -> FSequenceForm (DefaultZeroValue Z) N Z
zForm = DefaultZeroValue Z
-> PSequence N Z -> FSequenceForm (DefaultZeroValue Z) N Z
forall d i x. d -> PSequence i x -> FSequenceForm d i x
FSequenceForm (Root Z -> DefaultZeroValue Z
forall a. Root a -> DefaultZeroValue a
DefaultZeroValue (()() -> () -> Orientation ()
forall p. p -> p -> Orientation p
:>()))

        xForm :: N -> X (FSequenceForm (DefaultZeroValue Z) N Z)
        xForm :: N -> X (FSequenceForm (DefaultZeroValue Z) N Z)
xForm N
l = (PSequence N Z -> FSequenceForm (DefaultZeroValue Z) N Z)
-> X (PSequence N Z) -> X (FSequenceForm (DefaultZeroValue Z) N Z)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 PSequence N Z -> FSequenceForm (DefaultZeroValue Z) N Z
zForm (X (PSequence N Z) -> X (FSequenceForm (DefaultZeroValue Z) N Z))
-> X (PSequence N Z) -> X (FSequenceForm (DefaultZeroValue Z) N Z)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> X (PSequence N Z)
xis N
l

        xis :: N -> X (PSequence N Z)
        xis :: N -> X (PSequence N Z)
xis N
n = N -> N -> X Z -> X N -> X (PSequence N Z)
forall i x. Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence N
n N
n ([(Q, Z)] -> X Z
forall a. [(Q, a)] -> X a
xOneOfW [(Q
2,Z
0),(Q
1,Z
1)]) X N
xN

--------------------------------------------------------------------------------
-- prpFSequence -

-- | validating 'FSequence'.
prpFSequence :: Statement
prpFSequence :: Statement
prpFSequence = String -> Label
Prp String
"FSequence" Label -> Statement -> Statement
:<=>: N -> Statement
prpFSequenceSpan N
50