never executed always true always false
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE FunctionalDependencies #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE OverloadedStrings #-}
6 {-# LANGUAGE NoMonomorphismRestriction #-}
7
8 {- |
9 Module : NITTA.Synthesis.Types
10 Description : Synthesis tree representation
11 Copyright : (c) Aleksandr Penskoi, 2021
12 License : BSD3
13 Maintainer : aleksandr.penskoi@gmail.com
14 Stability : experimental
15
16 Synthesis can be represented as a graph (tree), where each 'Node' describes the
17 target system 'ModelState' and each 'Edge' synthesis decision.
18
19 A synthesis graph is very large and calculating and storing it in memory is very
20 bad idea. Also, working with synthesis graph usually making from the specific
21 node, not from the root. As a result, synthesis graph design as a explicit lazy
22 mutable structure implemented by 'TVar'.
23
24 From this point of view, the synthesis process is a finding of the best tree
25 leaf (lowest process duration for finished synthesis), and the best synthesis
26 method - a method which directly walks over the tree to the best leaf without
27 wrong steps.
28 -}
29 module NITTA.Synthesis.Types (
30 SynthesisDecisionCls (..),
31 Tree (..),
32 SynthesisDecision (..),
33 SynthesisState (..),
34 SynthesisMethodConstraints,
35 Sid (..),
36 DefTree,
37 SynthesisMethod,
38 (<?>),
39 targetUnit,
40 targetDFG,
41 defScore,
42 mlScoreKeyPrefix,
43 ) where
44
45 import Control.Concurrent.STM (TMVar)
46 import Data.Aeson (ToJSON, toJSON)
47 import Data.Default
48 import Data.List.Split
49 import Data.Map.Strict (Map)
50 import Data.Map.Strict qualified as M
51 import Data.Set qualified as S
52 import Data.Text (Text, isPrefixOf)
53 import Data.Typeable
54 import NITTA.Intermediate.Analysis (ProcessWave)
55 import NITTA.Intermediate.Types
56 import NITTA.Model.Networks.Bus
57 import NITTA.Model.Problems.Allocation
58 import NITTA.Model.Problems.Bind
59 import NITTA.Model.Problems.Dataflow
60 import NITTA.Model.Problems.Refactor
61 import NITTA.Model.Problems.ViewHelper
62 import NITTA.Model.ProcessorUnits.Types (UnitTag)
63 import NITTA.Model.TargetSystem
64 import NITTA.Model.Time
65 import NITTA.UIBackend.ViewHelperCls
66 import NITTA.Utils.Base
67 import Servant
68
69 -- | Default synthesis tree type.
70 type DefTree tag v x t =
71 Tree (TargetSystem (BusNetwork tag v x t) tag v x t) tag v x t
72
73 {- | The synthesis method is a function, which manipulates a synthesis tree. It
74 receives a node and explores it deeply by IO.
75 -}
76 type SynthesisMethod tag v x t = DefTree tag v x t -> IO (DefTree tag v x t)
77
78 {- | Shortcut for constraints in signatures of synthesis method functions.
79 This used to be (VarValTime v x t, UnitTag tag). See below for more info.
80 -}
81 type SynthesisMethodConstraints tag v x t = (VarValTimeJSON v x t, ToJSON tag, UnitTag tag)
82
83 {- | Synthesis node ID. ID is a relative path, encoded as a sequence of an option
84 index.
85 -}
86 newtype Sid = Sid [Int]
87
88 -- | Sid separator for @Show Sid@ and @Read Sid@.
89 sidSep = '-'
90
91 instance Show Sid where
92 show (Sid []) = [sidSep]
93 show (Sid is) = show' is
94 where
95 show' [] = ""
96 show' (x : xs) = sidSep : show x ++ show' xs
97
98 instance Read Sid where
99 readsPrec _ [x] | x == sidSep = [(Sid [], "")]
100 readsPrec d (x : xs)
101 | x == sidSep
102 , let is = map (readsPrec d) $ splitOn [sidSep] xs
103 , not $ any null is =
104 [(Sid $ map fst $ concat is, "")]
105 readsPrec _ _ = []
106
107 instance Default Sid where
108 def = Sid []
109
110 instance Semigroup Sid where
111 (Sid a) <> (Sid b) = Sid (a <> b)
112
113 instance Monoid Sid where
114 mempty = Sid []
115 mappend = (<>)
116
117 instance ToJSON Sid where
118 toJSON sid = toJSON $ show sid
119
120 instance FromHttpApiData Sid where
121 parseUrlPiece = Right . readText
122
123 -- | Synthesis tree
124 data Tree m tag v x t = Tree
125 { sID :: Sid
126 , sState :: SynthesisState m tag v x t
127 , sDecision :: SynthesisDecision (SynthesisState m tag v x t) m
128 , sSubForestVar :: TMVar [Tree m tag v x t]
129 -- ^ lazy mutable field with different synthesis options and sub nodes
130 , isLeaf :: Bool
131 , isComplete :: Bool
132 }
133
134 targetUnit = mUnit . sTarget . sState
135 targetDFG = mDataFlowGraph . sTarget . sState
136
137 data SynthesisDecision ctx m where
138 Root :: SynthesisDecision ctx m
139 SynthesisDecision ::
140 (Typeable p, SynthesisDecisionCls ctx m o d p, Show d, ToJSON p, Viewable d DecisionView) =>
141 {option :: o, decision :: d, metrics :: p, scores :: Map Text Float} ->
142 SynthesisDecision ctx m
143
144 mlScoreKeyPrefix = "ml_"
145
146 defScore :: SynthesisDecision ctx m -> Float
147 defScore sDecision =
148 let allScores = scores sDecision
149 mlScores = filter (isPrefixOf mlScoreKeyPrefix . fst) $ M.assocs allScores
150 in case mlScores of
151 [] -> allScores M.! "default"
152 (_key, mlScore) : _ -> mlScore
153
154 class SynthesisDecisionCls ctx m o d p | ctx o -> m d p where
155 decisions :: ctx -> o -> [(d, m)]
156 parameters :: ctx -> o -> d -> p
157 estimate :: ctx -> o -> d -> p -> Float
158
159 data SynthesisState m tag v x t = SynthesisState
160 { sParent :: Maybe (Tree m tag v x t)
161 , sTarget :: m
162 , sAllocationOptions :: [Allocation tag]
163 -- ^ PU allocation options cache
164 , sBindOptions :: [Bind tag v x]
165 -- ^ bind options cache
166 , sResolveDeadlockOptions :: [ResolveDeadlock v x]
167 , sOptimizeAccumOptions :: [OptimizeAccum v x]
168 , sConstantFoldingOptions :: [ConstantFolding v x]
169 , sBreakLoopOptions :: [BreakLoop v x]
170 , sDataflowOptions :: [DataflowSt tag v (TimeConstraint t)]
171 -- ^ dataflow options cache
172 , bindingAlternative :: M.Map (F v x) [tag]
173 -- ^ a map from functions to possible processor unit tags
174 , possibleDeadlockBinds :: S.Set (F v x)
175 -- ^ a function set, which binding may cause dead lock
176 , bindWaves :: M.Map v Int
177 -- ^ if algorithm will be represented as a graph, where nodes -
178 -- variables of not bound functions, edges - casuality, wave is a
179 -- minimal number of a step from an initial node to selected
180 , processWaves :: [ProcessWave v x]
181 -- ^ Execution waves of the algorithm. See detailed description in NITTA.Intermediate.Analysis module.
182 , numberOfProcessWaves :: Int
183 -- ^ Number of execution waves of the algorithm.
184 , numberOfDataflowOptions :: Int
185 -- ^ number of dataflow options
186 , transferableVars :: S.Set v
187 -- ^ a variable set, which can be transferred on the current
188 -- synthesis step
189 , unitWorkloadInFunction :: M.Map tag Int
190 -- ^ dictionary with number of bound functions for each unit
191 }
192
193 -- * Utils
194
195 True <?> v = v
196 False <?> _ = 0