{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}

module Data.SBV.Program.Types (
  module Data.Biapplicative,
  module Data.Bifoldable,
  module Data.Bitraversable,

  Location,
  SLocation,

  SynthSpec(..),
  SynthComponent(..),

  SimpleSpec(..),
  SimpleComponent(..),

  SynthesisError(..),

  IOs(..),
  Instruction(..),
  Program(..),
  toIOsList,
  sortInstructions,

  ProgramTree(..),
  buildProgramTree,
  buildForestResult,
  )
where

import Data.Biapplicative
import Data.Bifoldable
import Data.Bitraversable
import Data.Foldable
import Data.List
import qualified Data.Map as M
import qualified Data.Set as S
import Data.SBV


-- | Type used to represent a value from the __set of location variables__ \(l_x \in L\).
type Location = Word64
-- | Symbolic 'Location'.
type SLocation = SWord64


-- | Class for a program or a component __specification__ \(φ(\vec I, O)\). Type
-- variable 'a' stands for function's domain type.
class SynthSpec s a where
  -- | Number of inputs the specification function takes.
  specArity :: s a -> Word
  -- | An equation that relates input variables to the output one. The equation is
  -- build up either using '(.==)' or in a "tabular" way using multiple '(.=>)'
  -- expressions. See definitions from the Data.SBV.Program.SimpleLibrary module
  -- for examples.
  specFunc :: s a
    -- | Input variables. The list should be of 'specArity' size.
    -> [SBV a]
    -- | Output variable.
    -> SBV a
    -> SBool

-- | A class for a __library component__.
class SynthSpec spec a => SynthComponent comp spec a | comp -> spec where
  -- | Component name (optional). Used for naming SBV variables and when rendering the resulting program.
  compName :: comp a -> String
  -- | Component's __specification__.
  compSpec :: comp a -> spec a
  -- | Optional constraints to set on __location variables__ \(l_x \in L\).
  extraLocConstrs :: comp a -> [[SLocation] -> SLocation -> SBool]

  compName = forall a b. a -> b -> a
const String
""
  extraLocConstrs = forall a b. a -> b -> a
const []


-- | A simplest __specification__ datatype possible. Type variable 'a' stands
-- for function's domain type.
data SimpleSpec a = SimpleSpec {
    forall a. SimpleSpec a -> Word
simpleArity :: Word
  , forall a. SimpleSpec a -> [SBV a] -> SBV a -> SBool
simpleFunc :: [SBV a] -> SBV a -> SBool
  }

instance SynthSpec SimpleSpec a where
  specArity :: SimpleSpec a -> Word
specArity = forall a. SimpleSpec a -> Word
simpleArity
  specFunc :: SimpleSpec a -> [SBV a] -> SBV a -> SBool
specFunc = forall a. SimpleSpec a -> [SBV a] -> SBV a -> SBool
simpleFunc

-- | A simplest __library component__ datatype possible.
data SimpleComponent a = SimpleComponent {
    forall a. SimpleComponent a -> String
simpleName :: String
  , forall a. SimpleComponent a -> SimpleSpec a
simpleSpec :: SimpleSpec a
  }

instance SynthComponent SimpleComponent SimpleSpec a where
  compName :: SimpleComponent a -> String
compName = forall a. SimpleComponent a -> String
simpleName
  compSpec :: SimpleComponent a -> SimpleSpec a
compSpec = forall a. SimpleComponent a -> SimpleSpec a
simpleSpec
  extraLocConstrs :: SimpleComponent a -> [[SLocation] -> SLocation -> SBool]
extraLocConstrs = forall a b. a -> b -> a
const []

instance Show (SimpleComponent spec) where
  show :: SimpleComponent spec -> String
show = forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> String
compName


-- | Possible failure reasons during synthesis operation.
data SynthesisError = ErrorUnsat
                    | ErrorUnknown String
                    | ErrorZeroResultsRequested
                    | ErrorSeedingFailed
  deriving Int -> SynthesisError -> ShowS
[SynthesisError] -> ShowS
SynthesisError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SynthesisError] -> ShowS
$cshowList :: [SynthesisError] -> ShowS
show :: SynthesisError -> String
$cshow :: SynthesisError -> String
showsPrec :: Int -> SynthesisError -> ShowS
$cshowsPrec :: Int -> SynthesisError -> ShowS
Show


-- | A datatype holding inputs and output of something. Usual types for 'l' are 'Location' and 'SLocation'.
data IOs l = IOs {
    forall l. IOs l -> [l]
_ins :: [l],
    forall l. IOs l -> l
_out :: l
  }
  deriving (Int -> IOs l -> ShowS
forall l. Show l => Int -> IOs l -> ShowS
forall l. Show l => [IOs l] -> ShowS
forall l. Show l => IOs l -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IOs l] -> ShowS
$cshowList :: forall l. Show l => [IOs l] -> ShowS
show :: IOs l -> String
$cshow :: forall l. Show l => IOs l -> String
showsPrec :: Int -> IOs l -> ShowS
$cshowsPrec :: forall l. Show l => Int -> IOs l -> ShowS
Show, IOs l -> IOs l -> Bool
forall l. Eq l => IOs l -> IOs l -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IOs l -> IOs l -> Bool
$c/= :: forall l. Eq l => IOs l -> IOs l -> Bool
== :: IOs l -> IOs l -> Bool
$c== :: forall l. Eq l => IOs l -> IOs l -> Bool
Eq, IOs l -> IOs l -> Bool
IOs l -> IOs l -> Ordering
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 {l}. Ord l => Eq (IOs l)
forall l. Ord l => IOs l -> IOs l -> Bool
forall l. Ord l => IOs l -> IOs l -> Ordering
forall l. Ord l => IOs l -> IOs l -> IOs l
min :: IOs l -> IOs l -> IOs l
$cmin :: forall l. Ord l => IOs l -> IOs l -> IOs l
max :: IOs l -> IOs l -> IOs l
$cmax :: forall l. Ord l => IOs l -> IOs l -> IOs l
>= :: IOs l -> IOs l -> Bool
$c>= :: forall l. Ord l => IOs l -> IOs l -> Bool
> :: IOs l -> IOs l -> Bool
$c> :: forall l. Ord l => IOs l -> IOs l -> Bool
<= :: IOs l -> IOs l -> Bool
$c<= :: forall l. Ord l => IOs l -> IOs l -> Bool
< :: IOs l -> IOs l -> Bool
$c< :: forall l. Ord l => IOs l -> IOs l -> Bool
compare :: IOs l -> IOs l -> Ordering
$ccompare :: forall l. Ord l => IOs l -> IOs l -> Ordering
Ord, forall a b. a -> IOs b -> IOs a
forall a b. (a -> b) -> IOs a -> IOs b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> IOs b -> IOs a
$c<$ :: forall a b. a -> IOs b -> IOs a
fmap :: forall a b. (a -> b) -> IOs a -> IOs b
$cfmap :: forall a b. (a -> b) -> IOs a -> IOs b
Functor)

instance Foldable IOs where
  foldMap :: forall m a. Monoid m => (a -> m) -> IOs a -> m
foldMap a -> m
f (IOs {a
[a]
_out :: a
_ins :: [a]
_out :: forall l. IOs l -> l
_ins :: forall l. IOs l -> [l]
..}) = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map a -> m
f [a]
_ins) forall a. Monoid a => a -> a -> a
`mappend` a -> m
f a
_out

instance Traversable IOs where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> IOs a -> f (IOs b)
traverse a -> f b
f (IOs {a
[a]
_out :: a
_ins :: [a]
_out :: forall l. IOs l -> l
_ins :: forall l. IOs l -> [l]
..}) = forall l. [l] -> l -> IOs l
IOs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f [a]
_ins forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f b
f a
_out

instance EqSymbolic l => EqSymbolic (IOs l) where
  IOs l
l .== :: IOs l -> IOs l -> SBool
.== IOs l
r = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList IOs l
l forall a. EqSymbolic a => a -> a -> SBool
.== forall (t :: * -> *) a. Foldable t => t a -> [a]
toList IOs l
r


-- | A datatype that holds a 'SynthComponent' with inputs and output locations.
data Instruction l a = Instruction {
    forall l a. Instruction l a -> IOs l
instructionIOs :: IOs l,
    forall l a. Instruction l a -> a
instructionComponent :: a
  }
  deriving (Int -> Instruction l a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall l a. (Show l, Show a) => Int -> Instruction l a -> ShowS
forall l a. (Show l, Show a) => [Instruction l a] -> ShowS
forall l a. (Show l, Show a) => Instruction l a -> String
showList :: [Instruction l a] -> ShowS
$cshowList :: forall l a. (Show l, Show a) => [Instruction l a] -> ShowS
show :: Instruction l a -> String
$cshow :: forall l a. (Show l, Show a) => Instruction l a -> String
showsPrec :: Int -> Instruction l a -> ShowS
$cshowsPrec :: forall l a. (Show l, Show a) => Int -> Instruction l a -> ShowS
Show, Instruction l a -> Instruction l a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall l a.
(Eq l, Eq a) =>
Instruction l a -> Instruction l a -> Bool
/= :: Instruction l a -> Instruction l a -> Bool
$c/= :: forall l a.
(Eq l, Eq a) =>
Instruction l a -> Instruction l a -> Bool
== :: Instruction l a -> Instruction l a -> Bool
$c== :: forall l a.
(Eq l, Eq a) =>
Instruction l a -> Instruction l a -> Bool
Eq, Instruction l a -> Instruction l a -> Bool
Instruction l a -> Instruction l a -> Ordering
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 {l} {a}. (Ord l, Ord a) => Eq (Instruction l a)
forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Bool
forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Ordering
forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Instruction l a
min :: Instruction l a -> Instruction l a -> Instruction l a
$cmin :: forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Instruction l a
max :: Instruction l a -> Instruction l a -> Instruction l a
$cmax :: forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Instruction l a
>= :: Instruction l a -> Instruction l a -> Bool
$c>= :: forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Bool
> :: Instruction l a -> Instruction l a -> Bool
$c> :: forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Bool
<= :: Instruction l a -> Instruction l a -> Bool
$c<= :: forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Bool
< :: Instruction l a -> Instruction l a -> Bool
$c< :: forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Bool
compare :: Instruction l a -> Instruction l a -> Ordering
$ccompare :: forall l a.
(Ord l, Ord a) =>
Instruction l a -> Instruction l a -> Ordering
Ord)

instance Bifunctor Instruction where
  bimap :: forall a b c d.
(a -> b) -> (c -> d) -> Instruction a c -> Instruction b d
bimap a -> b
iosF c -> d
compF (Instruction {c
IOs a
instructionComponent :: c
instructionIOs :: IOs a
instructionComponent :: forall l a. Instruction l a -> a
instructionIOs :: forall l a. Instruction l a -> IOs l
..}) = forall l a. IOs l -> a -> Instruction l a
Instruction (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
iosF IOs a
instructionIOs) (c -> d
compF c
instructionComponent)

instance Bitraversable Instruction where
  bitraverse :: forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> Instruction a b -> f (Instruction c d)
bitraverse a -> f c
iosF b -> f d
compF (Instruction IOs a
ios b
comp) = forall l a. IOs l -> a -> Instruction l a
Instruction forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f c
iosF IOs a
ios forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> f d
compF b
comp

instance Bifoldable Instruction where
  bifoldMap :: forall m a b.
Monoid m =>
(a -> m) -> (b -> m) -> Instruction a b -> m
bifoldMap a -> m
f1 b -> m
f2 (Instruction {b
IOs a
instructionComponent :: b
instructionIOs :: IOs a
instructionComponent :: forall l a. Instruction l a -> a
instructionIOs :: forall l a. Instruction l a -> IOs l
..}) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f1 IOs a
instructionIOs forall a. Monoid a => a -> a -> a
`mappend` b -> m
f2 b
instructionComponent


-- | A datatype that unites program instructions with 'IOs' of the program itself.
data Program l a = Program {
    forall l a. Program l a -> IOs l
programIOs :: IOs l,
    forall l a. Program l a -> [Instruction l a]
programInstructions :: [Instruction l a]
  }
  deriving (Int -> Program l a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall l a. (Show l, Show a) => Int -> Program l a -> ShowS
forall l a. (Show l, Show a) => [Program l a] -> ShowS
forall l a. (Show l, Show a) => Program l a -> String
showList :: [Program l a] -> ShowS
$cshowList :: forall l a. (Show l, Show a) => [Program l a] -> ShowS
show :: Program l a -> String
$cshow :: forall l a. (Show l, Show a) => Program l a -> String
showsPrec :: Int -> Program l a -> ShowS
$cshowsPrec :: forall l a. (Show l, Show a) => Int -> Program l a -> ShowS
Show, Program l a -> Program l a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall l a. (Eq l, Eq a) => Program l a -> Program l a -> Bool
/= :: Program l a -> Program l a -> Bool
$c/= :: forall l a. (Eq l, Eq a) => Program l a -> Program l a -> Bool
== :: Program l a -> Program l a -> Bool
$c== :: forall l a. (Eq l, Eq a) => Program l a -> Program l a -> Bool
Eq, Program l a -> Program l a -> Bool
Program l a -> Program l a -> Ordering
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 {l} {a}. (Ord l, Ord a) => Eq (Program l a)
forall l a. (Ord l, Ord a) => Program l a -> Program l a -> Bool
forall l a.
(Ord l, Ord a) =>
Program l a -> Program l a -> Ordering
forall l a.
(Ord l, Ord a) =>
Program l a -> Program l a -> Program l a
min :: Program l a -> Program l a -> Program l a
$cmin :: forall l a.
(Ord l, Ord a) =>
Program l a -> Program l a -> Program l a
max :: Program l a -> Program l a -> Program l a
$cmax :: forall l a.
(Ord l, Ord a) =>
Program l a -> Program l a -> Program l a
>= :: Program l a -> Program l a -> Bool
$c>= :: forall l a. (Ord l, Ord a) => Program l a -> Program l a -> Bool
> :: Program l a -> Program l a -> Bool
$c> :: forall l a. (Ord l, Ord a) => Program l a -> Program l a -> Bool
<= :: Program l a -> Program l a -> Bool
$c<= :: forall l a. (Ord l, Ord a) => Program l a -> Program l a -> Bool
< :: Program l a -> Program l a -> Bool
$c< :: forall l a. (Ord l, Ord a) => Program l a -> Program l a -> Bool
compare :: Program l a -> Program l a -> Ordering
$ccompare :: forall l a.
(Ord l, Ord a) =>
Program l a -> Program l a -> Ordering
Ord)

instance Bifunctor Program where
  bimap :: forall a b c d. (a -> b) -> (c -> d) -> Program a c -> Program b d
bimap a -> b
iosF c -> d
compF (Program {[Instruction a c]
IOs a
programInstructions :: [Instruction a c]
programIOs :: IOs a
programInstructions :: forall l a. Program l a -> [Instruction l a]
programIOs :: forall l a. Program l a -> IOs l
..}) = forall l a. IOs l -> [Instruction l a] -> Program l a
Program (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
iosF IOs a
programIOs) (forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
iosF c -> d
compF) [Instruction a c]
programInstructions)

instance Bitraversable Program where
  bitraverse :: forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> Program a b -> f (Program c d)
bitraverse a -> f c
iosF b -> f d
compF (Program IOs a
ios [Instruction a b]
instrs) = forall l a. IOs l -> [Instruction l a] -> Program l a
Program forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f c
iosF IOs a
ios forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse a -> f c
iosF b -> f d
compF) [Instruction a b]
instrs

instance Bifoldable Program where
  bifoldMap :: forall m a b. Monoid m => (a -> m) -> (b -> m) -> Program a b -> m
bifoldMap a -> m
f1 b -> m
f2 (Program {[Instruction a b]
IOs a
programInstructions :: [Instruction a b]
programIOs :: IOs a
programInstructions :: forall l a. Program l a -> [Instruction l a]
programIOs :: forall l a. Program l a -> IOs l
..}) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f1 IOs a
programIOs forall a. Monoid a => a -> a -> a
`mappend` forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap a -> m
f1 b -> m
f2) [Instruction a b]
programInstructions

-- | Extract all locations from the program as a list, including locations of instructions.
toIOsList :: Program l a -> [l]
toIOsList :: forall l a. Program l a -> [l]
toIOsList = forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap (forall a. a -> [a] -> [a]
:[]) (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty)

-- | Sorts program's instructions by their output location.
sortInstructions :: Ord l => Program l a -> Program l a
sortInstructions :: forall l a. Ord l => Program l a -> Program l a
sortInstructions Program l a
p = Program l a
p { programInstructions :: [Instruction l a]
programInstructions = forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (forall l. IOs l -> l
_out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> IOs l
instructionIOs) (forall l a. Program l a -> [Instruction l a]
programInstructions Program l a
p) }


-- | A `Program` converted into a tree-like structure.
data ProgramTree a = InstructionNode a [ProgramTree a]
                   | InputLeaf Location
    deriving (Int -> ProgramTree a -> ShowS
forall a. Show a => Int -> ProgramTree a -> ShowS
forall a. Show a => [ProgramTree a] -> ShowS
forall a. Show a => ProgramTree a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProgramTree a] -> ShowS
$cshowList :: forall a. Show a => [ProgramTree a] -> ShowS
show :: ProgramTree a -> String
$cshow :: forall a. Show a => ProgramTree a -> String
showsPrec :: Int -> ProgramTree a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ProgramTree a -> ShowS
Show, ProgramTree a -> ProgramTree a -> Bool
forall a. Eq a => ProgramTree a -> ProgramTree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProgramTree a -> ProgramTree a -> Bool
$c/= :: forall a. Eq a => ProgramTree a -> ProgramTree a -> Bool
== :: ProgramTree a -> ProgramTree a -> Bool
$c== :: forall a. Eq a => ProgramTree a -> ProgramTree a -> Bool
Eq, ProgramTree a -> ProgramTree a -> Bool
ProgramTree a -> ProgramTree a -> Ordering
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 {a}. Ord a => Eq (ProgramTree a)
forall a. Ord a => ProgramTree a -> ProgramTree a -> Bool
forall a. Ord a => ProgramTree a -> ProgramTree a -> Ordering
forall a. Ord a => ProgramTree a -> ProgramTree a -> ProgramTree a
min :: ProgramTree a -> ProgramTree a -> ProgramTree a
$cmin :: forall a. Ord a => ProgramTree a -> ProgramTree a -> ProgramTree a
max :: ProgramTree a -> ProgramTree a -> ProgramTree a
$cmax :: forall a. Ord a => ProgramTree a -> ProgramTree a -> ProgramTree a
>= :: ProgramTree a -> ProgramTree a -> Bool
$c>= :: forall a. Ord a => ProgramTree a -> ProgramTree a -> Bool
> :: ProgramTree a -> ProgramTree a -> Bool
$c> :: forall a. Ord a => ProgramTree a -> ProgramTree a -> Bool
<= :: ProgramTree a -> ProgramTree a -> Bool
$c<= :: forall a. Ord a => ProgramTree a -> ProgramTree a -> Bool
< :: ProgramTree a -> ProgramTree a -> Bool
$c< :: forall a. Ord a => ProgramTree a -> ProgramTree a -> Bool
compare :: ProgramTree a -> ProgramTree a -> Ordering
$ccompare :: forall a. Ord a => ProgramTree a -> ProgramTree a -> Ordering
Ord, forall a b. a -> ProgramTree b -> ProgramTree a
forall a b. (a -> b) -> ProgramTree a -> ProgramTree b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> ProgramTree b -> ProgramTree a
$c<$ :: forall a b. a -> ProgramTree b -> ProgramTree a
fmap :: forall a b. (a -> b) -> ProgramTree a -> ProgramTree b
$cfmap :: forall a b. (a -> b) -> ProgramTree a -> ProgramTree b
Functor)

instance Foldable ProgramTree where
  foldMap :: forall m a. Monoid m => (a -> m) -> ProgramTree a -> m
foldMap a -> m
_ (InputLeaf Location
_) = forall a. Monoid a => a
mempty
  foldMap a -> m
f (InstructionNode a
comp [ProgramTree a]
children) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) [ProgramTree a]
children forall a. Semigroup a => a -> a -> a
<> a -> m
f a
comp

-- | Create a 'ProgramTree' for a given 'Program' by resolving its 'Location's.
-- This function effectively performs dead code elimination.
buildProgramTree :: Program Location a -> ProgramTree a
buildProgramTree :: forall a. Program Location a -> ProgramTree a
buildProgramTree Program Location a
prog = forall a. Program Location a -> Location -> ProgramTree a
buildProgramTree' Program Location a
prog (forall l. IOs l -> l
_out forall a b. (a -> b) -> a -> b
$ forall l a. Program l a -> IOs l
programIOs Program Location a
prog)

-- | A variant of 'buildProgramTree' that builds from a specified starting point.
buildProgramTree' :: Program Location a -> Location -> ProgramTree a
buildProgramTree' :: forall a. Program Location a -> Location -> ProgramTree a
buildProgramTree' prog :: Program Location a
prog@(Program {[Instruction Location a]
IOs Location
programInstructions :: [Instruction Location a]
programIOs :: IOs Location
programInstructions :: forall l a. Program l a -> [Instruction l a]
programIOs :: forall l a. Program l a -> IOs l
..}) Location
startingOutputLoc =
  if Location
startingOutputLoc forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall l. IOs l -> [l]
_ins IOs Location
programIOs
    then forall a. a -> [ProgramTree a] -> ProgramTree a
InstructionNode
        (forall l a. Instruction l a -> a
instructionComponent (Map Location (Instruction Location a)
instsMap forall k a. Ord k => Map k a -> k -> a
M.! Location
startingOutputLoc))
        (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Program Location a -> Location -> ProgramTree a
buildProgramTree' Program Location a
prog) forall a b. (a -> b) -> a -> b
$ forall l. IOs l -> [l]
_ins forall a b. (a -> b) -> a -> b
$ forall l a. Instruction l a -> IOs l
instructionIOs (Map Location (Instruction Location a)
instsMap forall k a. Ord k => Map k a -> k -> a
M.! Location
startingOutputLoc))
    else forall a. Location -> ProgramTree a
InputLeaf Location
startingOutputLoc
  where
    instsMap :: Map Location (Instruction Location a)
instsMap = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Instruction Location a
inst -> (forall l. IOs l -> l
_out forall a b. (a -> b) -> a -> b
$ forall l a. Instruction l a -> IOs l
instructionIOs Instruction Location a
inst, Instruction Location a
inst)) [Instruction Location a]
programInstructions

-- | Create a 'ProgramTree' for each unused output in the 'Program'
buildForestResult :: Program Location a -> [ProgramTree a]
buildForestResult sr :: Program Location a
sr@(Program {[Instruction Location a]
IOs Location
programInstructions :: [Instruction Location a]
programIOs :: IOs Location
programInstructions :: forall l a. Program l a -> [Instruction l a]
programIOs :: forall l a. Program l a -> IOs l
..}) = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Program Location a -> Location -> ProgramTree a
buildProgramTree' Program Location a
sr) [Location]
rootOutputs
  where
    inputsSet :: Set Location
inputsSet = forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall l. IOs l -> [l]
_ins IOs Location
programIOs forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall l. IOs l -> [l]
_ins forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> IOs l
instructionIOs) [Instruction Location a]
programInstructions
    rootOutputs :: [Location]
rootOutputs = forall a. (a -> Bool) -> [a] -> [a]
filter Location -> Bool
isRootOutput forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall l. IOs l -> l
_out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> IOs l
instructionIOs) [Instruction Location a]
programInstructions
    isRootOutput :: Location -> Bool
isRootOutput Location
o = Location
o forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set Location
inputsSet