1  {-
2  SockeyeBackendProlog.hs: Backend for generating ECLiPSe-Prolog for Sockeye
3
4  Part of Sockeye
5
6  Copyright (c) 2018, ETH Zurich.
7
8  All rights reserved.
9
10  This file is distributed under the terms in the attached LICENSE file.
11  If you do not find this file, copies can be found by writing to:
12  ETH Zurich D-INFK, CAB F.78, Universitaetstrasse 6, CH-8092 Zurich,
13  Attn: Systems Group.
14-}
15
16
17{-
18  TODO: This currently works on a subset of the parser AST. Ideally, there would be
19  a transformation first that:
20  * Removes wildcards and replaces it with forall loops (introducing a new variable)
21  * Expands natural expression into a seperate definition blocks (introducing new local
22    variable for each block)
23  * Everytime a range is encountered, it's passed to a natural limit/base range (no more bit ops)
24  * Pushes the type of accepted/translated blocks own to the specific blocks, this should
25    also merge the translte/convert types into one.
26-}
27
28module SockeyeBackendProlog
29( compile, compileDirect ) where
30
31import qualified Data.Map as Map
32import Data.Char
33import Data.List
34import Text.Printf
35import Control.Exception (throw, Exception)
36
37import qualified SockeyeSymbolTable as ST
38import qualified SockeyeAST as SAST
39import qualified SockeyeParserAST as AST
40
41data PrologBackendException
42  =  NYIException String
43  deriving(Show)
44
45instance Exception PrologBackendException
46
47{- The structure of the code generator should be very similar to the old Prolog Backend -}
48compile :: ST.Sockeye -> SAST.Sockeye -> String
49compile symTable ast = "Prolog backend not yet implemented"
50
51compileDirect :: AST.Sockeye -> String
52compileDirect = generate
53
54{- Code Generator -}
55class PrologGenerator a where
56    generate :: a -> String
57
58instance PrologGenerator AST.Sockeye where
59  generate s = let
60    files = map snd (Map.toList (AST.files s))
61    in concat (map generate files)
62
63instance PrologGenerator AST.SockeyeFile where
64  generate f = concat (map generate (AST.modules f))
65
66gen_node_param_list :: [AST.NodeDeclaration] -> [String]
67gen_node_param_list ndl = map AST.nodeName ndl
68
69gen_nat_param_list :: [AST.ModuleParameter] -> [String]
70gen_nat_param_list pp = map AST.paramName pp
71
72
73
74gen_body_def_maps :: ModuleInfo -> [AST.Definition] -> Integer -> [String]
75gen_body_def_maps m [] _ = []
76gen_body_def_maps m (xs:x) i = elms  ++ (gen_body_def_maps m x (ii))
77    where
78        (ii, elms) = (gen_body_defs m xs i)
79
80instance PrologGenerator AST.Module where
81  generate m = let
82    name = "add_" ++ AST.moduleName m
83    mi = gen_module_info m
84    p1 = gen_nat_param_list (AST.parameters m)
85    bodyChecks = ["is_list(Id)"]
86
87    nodeDecls = map gen_node_decls (AST.nodeDecls m)
88    instDecls = map gen_inst_decls (AST.instDecls m)
89
90    -- bodyDefs = concat $ map (gen_body_defs mi) (AST.definitions m)
91    bodyDefs = gen_body_def_maps mi  (AST.definitions m) 0
92    n =  sum $ map (count_num_facts mi) (AST.definitions m)
93
94    body = intercalate ",\n    " $ bodyChecks ++ nodeDecls ++ instDecls ++ bodyDefs
95    in name ++ stringify ([statevar 0, "Id"] ++ p1 ++ [statevar n]) ++ " :- \n    " ++ body ++ ".\n\n"
96    where
97      stringify [] = ""
98      stringify pp = parens $ intercalate "," pp
99
100
101
102
103
104-- Inside each function we add variable that contains
105--  * nodeId
106--  * params
107--  * constants
108-- This will return the name of these variables
109local_nodeid_name :: String -> String
110local_nodeid_name x = "ID_" ++ x
111
112local_inst_name :: String -> String
113local_inst_name x = "ID_" ++ x
114
115-- Prefix tat as well?
116local_param_name :: String -> String
117local_param_name x = x
118
119local_const_name :: String -> String
120local_const_name x = "CONST_" ++ x
121
122-- Generates something a la:
123-- (ID_RAM) = (['ram', Id])
124gen_inst_decls :: AST.InstanceDeclaration -> String
125gen_inst_decls x =
126  let
127    var = local_nodeid_name $ AST.instName x
128    decl = list_prepend (doublequotes $ AST.instName x) (local_param_name "Id")
129    in var ++ " = " ++ decl
130
131-- Generates something a la:
132-- (ID_RAM, INKIND_RAM, OUTKIND_RAM) = (['ram' | Id], memory, memory)
133gen_node_decls :: AST.NodeDeclaration -> String
134gen_node_decls x =
135  let
136    var = local_nodeid_name $ AST.nodeName x
137    decl_kind_in = generate (AST.originDomain (AST.nodeType x))
138    decl_kind_out = generate (AST.targetDomain (AST.nodeType x))
139    decl_id = list_prepend (doublequotes $ AST.nodeName x) (local_param_name "Id")
140    decl_tup = tuple [decl_id, decl_kind_in, decl_kind_out]
141
142    -- Build the variable list
143    pf = AST.nodeName x
144    var_tup = tuple [local_nodeid_name pf, "INKIND_" ++ pf, "OUTKIND_" ++ pf]
145    in var_tup ++ " = " ++ decl_tup
146
147
148-- This transformation is probably better to be in an AST transform
149data MyAddressBlock = MyAddressBlock {
150  domain :: !AST.Domain,
151  addresses     :: AST.Address,
152  properties    :: AST.PropertyExpr
153  }
154
155pack_address_block :: ModuleInfo -> AST.AddressBlock -> MyAddressBlock
156pack_address_block mi ab = MyAddressBlock {
157  domain = AST.Memory,
158  addresses = SAST.addresses ab,
159  properties = SAST.properties ab
160}
161
162data OneMapSpec = OneMapSpec
163  {
164  srcNode :: AST.UnqualifiedRef,
165  srcAddr :: MyAddressBlock,
166  targetNode :: AST.NodeReference,
167  targetAddr :: MyAddressBlock
168  }
169
170
171map_spec_flatten :: ModuleInfo -> AST.Definition -> [OneMapSpec]
172map_spec_flatten mi def = case def of
173  (AST.Maps _ n maps) ->
174    [OneMapSpec n (src_ab n $ AST.mapAddr map_spec) (AST.targetNode map_target) (dest_ab n $ AST.targetAddr map_target)
175      | map_spec <- maps, map_target <- (AST.mapTargets map_spec)]
176  _ -> []
177  where
178    nt uqr = (node_type mi) Map.! (AST.refName uqr)
179    src_ab uqr ab = MyAddressBlock {
180      domain = ST.originDomain $ nt uqr,
181      properties = SAST.properties ab,
182      addresses = SAST.addresses ab
183    }
184    dest_ab uqr ab = MyAddressBlock {
185      domain = ST.targetDomain $ nt uqr,
186      addresses = SAST.addresses ab,
187      properties = SAST.properties ab
188    }
189
190data ModuleInfo = ModuleInfo
191  {
192    params :: [String],
193    node_type :: Map.Map String ST.NodeType
194  }
195
196gen_module_info :: AST.Module -> ModuleInfo
197gen_module_info x =
198  ModuleInfo {
199    params = ["Id"] ++ mparams ++ nodes ++ insts,
200    node_type = Map.fromList [(AST.nodeName z, AST.nodeType $ z) | z <- AST.nodeDecls x]
201  }
202  where
203    insts = [local_inst_name $ AST.instName d | d <- AST.instDecls x]
204    mparams = (gen_nat_param_list $ AST.parameters x)
205    nodes = [local_nodeid_name $ AST.nodeName d | d <- AST.nodeDecls x]
206
207add_param :: ModuleInfo -> String -> ModuleInfo
208add_param mi s = ModuleInfo { params = (params mi) ++ [s], node_type = node_type mi}
209
210param_str :: ModuleInfo -> String
211param_str mi = case params mi of
212  [] -> ""
213  li -> "," ++ intercalate "," [predicate "param" [p] | p <- li]
214
215
216generate_conj :: ModuleInfo -> [AST.Definition] -> String
217generate_conj mi li = "TODO> NYI"
218   -- intercalate ", sss\n" $ concat [snd(gen_body_defs mi inn 0) | inn <- li]
219   -- TODO: fix the 0 here
220
221
222-- generate forall with a explicit variable name
223forall_qual :: ModuleInfo -> String -> AST.NaturalSet -> [AST.Definition] -> String
224forall_qual mi varName ns body =
225  "(" ++
226   predicate "iblock_values" [generate ns, it_list] ++ "," ++
227   "(" ++
228   predicate "foreach" [it_var, it_list]
229   ++ param_str mi
230   ++ " do \n" ++
231   body_str ++ "\n))"
232   where
233     id_var = "ID_" ++ varName
234     it_var = "IDT_" ++ varName
235     it_list = "IDL_" ++ varName
236     body_str = generate_conj (add_param mi it_var) body
237
238forall_uqr :: ModuleInfo -> AST.UnqualifiedRef -> String -> String
239forall_uqr mi ref body_str = case (AST.refIndex ref) of
240  Nothing -> printf "(%s = %s, %s)" it_var id_var body_str
241  Just ai -> "(" ++
242                predicate "iblock_values" [generate ai, it_list] ++ "," ++
243                "(" ++
244                predicate "foreach" [it_var, it_list]
245                ++ param_str mi
246                ++ " do " ++
247                itid_var ++ " = " ++ list_prepend it_var id_var ++ "," ++
248                body_str ++ "))"
249  where
250    id_var = "ID_" ++ (AST.refName ref)
251    it_var = "IDT_" ++ (AST.refName ref)
252    itid_var = "IDI_" ++ (AST.refName ref)
253    it_list = "IDL_" ++ (AST.refName ref)
254
255
256
257gen_bind_defs :: String -> [AST.PortBinding] -> (Integer, [String]) -> (Integer, [String])
258gen_bind_defs uql_var [] s = s
259gen_bind_defs uql_var (x:xs) (i, s) = gen_bind_defs uql_var xs (i + 1, s ++ [ovl])
260    where
261        ovl = state_add_overlay i src dest
262        dest =  generate $ AST.boundNode x
263        src = list_prepend (doublequotes $ AST.refName $ AST.boundPort $ x) uql_var
264
265gen_index :: AST.UnqualifiedRef -> String
266gen_index uqr =
267  case (AST.refIndex uqr) of
268    Nothing -> local_nodeid_name $ AST.refName uqr
269    Just ai -> list_prepend (gen_ai ai) (local_nodeid_name $ AST.refName uqr)
270  where
271    gen_ai (AST.ArrayIndex _ ws) =  list [gen_wildcard_simple w | w <- ws]
272    gen_wildcard_simple (AST.ExplicitSet _ ns) = gen_natural_set ns
273    gen_natural_set (ST.NaturalSet _ nrs) = gen_natural_ranges nrs
274    gen_natural_ranges [nr] = gen_ns_simple nr
275    gen_ns_simple (ST.SingletonRange _ base) = gen_exp_simple base
276    gen_exp_simple (AST.Variable _ vn) = "IDT_" ++ vn
277    gen_exp_simple (AST.Literal _ int) = show int
278
279
280gen_accept :: ModuleInfo -> AST.UnqualifiedRef -> [AST.AddressBlock] -> (Integer, [String]) -> (Integer, [String])
281gen_accept mi _ [] s = s
282gen_accept mi n (xs:x) (i, s) = gen_accept mi n x (i + 1, s ++ [acc])
283    where
284        acc = state_add_accept i (predicate "region" [generate n, generate (pack_address_block mi xs)])
285
286gen_base_address :: AST.Address -> String
287gen_base_address (AST.Address _ ws) = gen_single_ws $ ws !! 0
288  where
289    gen_single_ws (AST.ExplicitSet _ ns) = gen_single_ns ns
290    gen_single_ws (AST.Wildcard _)  = "NYI"
291    gen_single_ns (AST.NaturalSet _ nr) = gen_single_nr (nr !! 0)
292    gen_single_nr nr = case nr of
293        AST.SingletonRange _ b -> generate b
294        AST.LimitRange _ b _ -> generate b
295        AST.BitsRange _ b bits -> "BITSRANGE NYI"
296
297gen_translate :: [OneMapSpec] -> (Integer, [String]) -> (Integer, [String])
298gen_translate [] s = s
299gen_translate (om:x) (i, s) = gen_translate x (i + 1, s ++ [trs])
300    where
301        trs = state_add_mapping i (gen_region (srcNode om) (srcAddr om)) (gen_name (targetNode om) (targetAddr om))
302        gen_region nodeid x = predicate "region" [generate nodeid, generate x]
303        gen_name nodeid x = predicate "name" [generate nodeid, gen_base_address $ addresses x]
304
305gen_blockoverlay :: String -> String -> [Integer] -> (Integer, [String]) -> (Integer, [String])
306gen_blockoverlay src dst [] s = s
307gen_blockoverlay src dst (om:x) (i, s) = gen_blockoverlay src dst  x (i + 1, s ++ [trs])
308    where
309        trs = state_add_block_meta i src (show om) dst
310
311gen_body_defs :: ModuleInfo -> AST.Definition -> Integer -> (Integer, [String])
312gen_body_defs mi x i = case x of
313  (AST.Accepts _ n accepts) -> gen_accept mi n accepts (i, [])
314  --(1, [(assert 0 $ predicate "accept" [generate n, generate (new_ab acc)])
315--    | acc <- accepts])
316  (AST.Maps _ _ _) -> gen_translate (map_spec_flatten mi x) (i, [])
317   --(1, [(assert 0 $ predicate "translate"
318    --[generate $ srcNode om, generate $ srcAddr om, generate $ targetNode om, generate $ targetAddr om])
319    -- | om <- map_spec_flatten mi x])
320  (AST.Overlays _ src dest) -> (i+1, [state_add_overlay i (generate src) (generate dest)])
321  (AST.BlockOverlays _ src dst bits) -> gen_blockoverlay (generate src) (generate dst) bits (i, [])
322  -- (AST.Instantiates _ i im args) -> [forall_uqr mi i (predicate ("add_" ++ im) ["IDT_" ++ (AST.refName i)])]
323  (AST.Instantiates _ ii im args) -> (i+1, [ predicate ("add_" ++ im) ([statevar i] ++ [gen_index ii] ++ [statevar (i+1)]) ])
324  -- (AST.Binds _ i binds) -> [forall_uqr mi i $ gen_bind_defs ("IDT_" ++ (AST.refName i)) binds]
325  (AST.Binds _ ii binds) -> gen_bind_defs (gen_index ii) binds (i, [])
326  (AST.Forall _ varName varRange body) -> (0, [forall_qual mi varName varRange body])
327  (AST.Converts _ _ _ ) -> throw $ NYIException "Converts"
328  where
329    new_ab ab = pack_address_block mi ab
330
331count_num_facts :: ModuleInfo -> AST.Definition -> Integer
332count_num_facts mi x = case x of
333    (AST.Accepts _ n accepts) -> sum([1 | acc <- accepts])
334    (AST.Maps _ _ _) -> sum([1 | om <- map_spec_flatten mi x])
335    (AST.Overlays _ src dest) -> 1
336    -- (AST.Instantiates _ i im args) -> [forall_uqr mi i (predicate ("add_" ++ im) ["IDT_" ++ (AST.refName i)])]
337    (AST.Instantiates _ _ _ _) -> 1
338    (AST.BlockOverlays _ _ _ bits) -> (toInteger (length bits))
339    -- (AST.Binds _ i binds) -> [forall_uqr mi i $ gen_bind_defs ("IDT_" ++ (AST.refName i)) binds]
340    (AST.Binds _ i binds) -> sum([1 | b <- binds])
341    (AST.Forall _ varName varRange body) -> 0
342    (AST.Converts _ _ _ ) -> 0
343
344
345
346instance PrologGenerator AST.UnqualifiedRef where
347  generate uq = case (AST.refIndex uq) of
348    Nothing -> local_nodeid_name $ AST.refName uq
349    Just ai -> list_prepend (generate ai) (local_nodeid_name $ AST.refName uq)
350
351instance PrologGenerator AST.WildcardSet where
352  generate a = case a of
353    AST.ExplicitSet _ ns -> generate ns
354    AST.Wildcard _ -> "NYI!?"
355
356instance PrologGenerator AST.ArrayIndex where
357  generate (AST.ArrayIndex _ wcs) = brackets $ intercalate "," [generate x | x <- wcs]
358
359instance PrologGenerator AST.MapSpec where
360  generate ms = struct "map" [("src_block", generate (AST.mapAddr ms)),
361    ("dests", list $ map generate (AST.mapTargets ms))]
362
363instance PrologGenerator AST.MapTarget where
364  generate mt = struct "dest" [("id", generate (AST.targetNode mt)),
365    ("base", generate (AST.targetAddr mt))]
366
367instance PrologGenerator AST.NodeReference where
368  generate nr = case nr of
369    AST.InternalNodeRef _ nn -> gen_index nn
370    AST.InputPortRef _ inst node -> list_prepend (doublequotes $ AST.refName node) (gen_index inst)
371
372instance PrologGenerator MyAddressBlock where
373  -- TODO: add properties
374  -- We have to generate something like this, probably involves an extra step in the AST.
375  -- pred_99(propspec) :- member(prop1, propspec), member(prop2, propspec
376  -- node_accept( ..., block{propspec: pred_99}).
377  -- to check: B = block{propspec: PS}, call(PS, current_properties)
378  generate ab = blocks !! 0
379    where
380      blocks = gen_a $ addresses ab
381      gen_a (AST.Address _ ws) = map gen_ws ws
382      gen_ws (AST.ExplicitSet _ ns) = generate ns
383      gen_ws (AST.Wildcard _ ) = "NYI"
384
385instance PrologGenerator AST.Domain where
386  generate d = case d of
387    AST.Memory -> atom "memory"
388    AST.Interrupt -> atom "interrupt"
389    AST.Power -> atom "power"
390    AST.Clock -> atom "clock"
391
392instance PrologGenerator AST.AddressBlock where
393  -- TODO: add properties
394  -- We have to generate something like this, probably involves an extra step in the AST.
395  -- pred_99(propspec) :- member(prop1, propspec), member(prop2, propspec
396  -- node_accept( ..., block{propspec: pred_99}).
397  -- to check: B = block{propspec: PS}, call(PS, current_properties)
398  generate ab = generate $ SAST.addresses ab
399
400
401instance PrologGenerator AST.Address where
402  generate a = case a of
403    AST.Address _ ws -> tuple $ map generate ws
404
405instance PrologGenerator AST.NaturalSet where
406  generate a = case a of
407     AST.NaturalSet _ [nrs] -> generate nrs
408     _ -> "SOMETHING"
409
410instance PrologGenerator AST.NaturalRange where
411  generate nr = case nr of
412    AST.SingletonRange _ b -> predicate "block"
413      [generate b, generate b]
414    AST.LimitRange _ b l -> predicate "block"
415      [generate b, generate l]
416    AST.BitsRange _ b bits -> "BITSRANGE NYI"
417      -- struct "block" [("base", generate b), ("limit", show 666)]
418
419instance PrologGenerator AST.NaturalExpr where
420  generate nr = case nr of
421    SAST.Constant _ v -> local_const_name v
422    SAST.Variable _ v -> "IDT_" ++ v
423    SAST.Parameter _ v -> local_param_name v
424    SAST.Literal _ n -> show n
425    SAST.Addition _ a b -> "(" ++ generate a ++ ")+(" ++ generate b ++ ")"
426    SAST.Subtraction _ a b -> "(" ++ generate a ++ ")-(" ++ generate b ++ ")"
427    SAST.Multiplication _ a b -> "(" ++ generate a ++ ")*(" ++ generate b ++ ")"
428    SAST.Slice _ a bitrange -> "SLICE NYI"
429    SAST.Concat _ a b -> "CONCAT NYI"
430
431
432{- Helper functions -}
433atom :: String -> String
434atom "" = ""
435atom name@(c:cs)
436    | isLower c && allAlphaNum cs = name
437    | otherwise = quotes name
438    where
439        allAlphaNum cs = foldl (\acc c -> isAlphaNum c && acc) True cs
440
441predicate :: String -> [String] -> String
442predicate name args = name ++ (parens $ intercalate "," args)
443
444struct :: String -> [(String, String)] -> String
445struct name fields = name ++ (braces $ intercalate "," (map toFieldString fields))
446    where
447        toFieldString (key, value) = key ++ ":" ++ value
448
449tuple :: [String] -> String
450tuple elems = parens $ intercalate "," elems
451
452list :: [String] -> String
453list elems = brackets $ intercalate "," elems
454
455list_prepend :: String -> String -> String
456list_prepend a li = brackets $ a ++ " | " ++ li
457
458enclose :: String -> String -> String -> String
459enclose start end string = start ++ string ++ end
460
461parens :: String -> String
462parens = enclose "(" ")"
463
464brackets :: String -> String
465brackets = enclose "[" "]"
466
467braces :: String -> String
468braces = enclose "{" "}"
469
470quotes :: String -> String
471quotes = enclose "'" "'"
472
473doublequotes :: String -> String
474doublequotes = enclose "\"" "\""
475
476
477nat_range_from :: AST.NaturalRange -> String
478nat_range_from nr = case nr of
479  AST.SingletonRange _ b -> generate b
480  AST.LimitRange _ b _ -> generate b
481  AST.BitsRange _ _ _ -> "BitsRange NOT IMPLEMENTED"
482
483nat_range_to :: AST.NaturalRange -> String
484nat_range_to nr = case nr of
485  AST.SingletonRange _ b -> generate b
486  AST.LimitRange _ _ l -> generate l
487  AST.BitsRange _ _ _ -> "BitsRange NOT IMPLEMENTED"
488
489-- Params are variables passed into the for body
490for_body_inner :: [String] -> String -> String -> (Int, AST.NaturalRange)  -> String
491for_body_inner params itvar body itrange  =
492  let
493    itvar_local = itvar ++ (show $ fst itrange)
494    from = nat_range_from $ (snd itrange)
495    to = nat_range_to $ (snd itrange)
496    for = printf "for(%s,%s,%s)" itvar_local from to :: String
497    paramf x  = printf "param(%s)" x :: String
498    header = intercalate "," ([for] ++ map paramf params)
499    in printf "(%s \ndo\n %s \n)" header body
500
501enumerate = zip [0..]
502
503for_body :: [String] -> String -> AST.NaturalSet -> String -> String
504for_body params itvar (AST.NaturalSet _ ranges) body =
505  foldl fbi body (enumerate ranges)
506  where
507    fbi = for_body_inner params itvar
508
509statevar :: Integer -> String
510statevar i = printf "S%i" i
511
512--assert ::  Integer -> String -> String
513--assert i x = "state_add" ++ parens ((statevar i) ++ ", " ++  x ++ ", " ++ (statevar (i + 1)))
514
515
516state_add_mapping ::  Integer -> String -> String -> String
517state_add_mapping i src dst = "assert_translate" ++ parens ((statevar i) ++ ", " ++  src ++ ", " ++ dst ++ ", " ++ (statevar (i + 1)))
518
519state_add_accept ::  Integer -> String -> String
520state_add_accept i reg = "assert_accept" ++ parens ((statevar i) ++ ", " ++  reg ++ ", " ++ (statevar (i + 1)))
521
522state_add_overlay ::  Integer -> String -> String -> String
523state_add_overlay i src dst = "assert_overlay" ++ parens ((statevar i) ++ ", " ++  src ++ ", " ++ dst ++ ", " ++ (statevar (i + 1)))
524
525state_add_block_meta ::  Integer -> String -> String -> String -> String
526state_add_block_meta i src bits dst = "assert_configurable" ++ parens ((statevar i) ++ ", " ++  src ++ ", " ++ bits ++ ", " ++ dst ++ ", " ++ (statevar (i + 1)))
527