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