Add ERC20 example and make several code generator improvements

ConfigParser.hs

@@ -14,19 +14,24 @@ jsonFile :: FilePath
 jsonFile = "config-sample.json"
 
 data DistributionConfig =
-  Config [ProcessConfig] [String]
+  Config [ProcessConfig] [String] [ConstantConfig]
   deriving (Show, Generic)
 
 data ProcessConfig =
   PConfig String [H.Action]
   deriving (Show, Generic)
 
+data ConstantConfig =
+  Constant String H.Value
+  deriving (Show, Generic)
+
 instance FromJSON DistributionConfig where
   parseJSON =
     withObject "DistribuitionConfig" $ \obj -> do
       ps <- obj .: "processes"
       vs <- obj .: "shared_variables"
-      return (Config ps vs)
+      cs <- obj .: "constants"
+      return (Config ps vs cs)
 
 instance FromJSON ProcessConfig where
   parseJSON =
@@ -37,6 +42,15 @@ instance FromJSON ProcessConfig where
         Left e -> fail ("Invalid action in:" ++ show as ++ ". Error: " ++ show e)
         Right cs -> return (PConfig i cs)
 
+instance FromJSON ConstantConfig where
+  parseJSON =
+    withObject "ConstantConfig" $ \obj -> do
+      n <- obj .: "name"
+      v <- obj .: "value"
+      case parseValue v of
+        Left e -> fail ("Invalid value in:" ++ show v ++ ". Error: " ++ show e)
+        Right val -> return (Constant n val)
+
 parseConfig :: FilePath -> IO (Either String DistributionConfig)
 parseConfig file = do
   content <- B.readFile file
@@ -45,4 +59,4 @@ parseConfig file = do
 -- main = parseJson jsonFile >>= print
 
 processNames :: DistributionConfig -> [String]
-processNames (Config ps _) = map (\(PConfig n _) -> n) ps
+processNames (Config ps _ _) = map (\(PConfig n _) -> n) ps

Elixir.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 module Elixir where
 
 import Data.List
@@ -9,14 +10,14 @@ import Helpers
 import Snippets
 
 generate :: Spec -> DistributionConfig -> [(String, ElixirCode)]
-generate (Spec m i n ds) (Config ps shared) =
+generate (Spec m i n ds) (Config ps shared consts) =
   let defs = filter (not . (specialDef i n)) ds
       cs = findConstants ds
       vs = findVariables ds
       header = moduleHeader (moduleName m) m shared False
       -- defNext = findIdentifier n ds
       base = baseSpec header cs vs defs
-   in (moduleName m, base):map (generateForProcess m n vs defs) ps
+   in (moduleName m, base):map (generateForProcess m n vs cs defs) ps
 
 generateStarter :: Spec -> (String, ElixirCode)
 generateStarter (Spec m i _ ds) =
@@ -27,12 +28,12 @@ generateStarter (Spec m i _ ds) =
    in (moduleName m, starterTask (moduleName m) state)
 
 generateForProcess ::
-     Module -> String -> [Variable] -> [Definition] -> ProcessConfig -> (String, ElixirCode)
-generateForProcess m n vs defs (PConfig p as) =
+     Module -> String -> [Variable] -> [Constant] -> [Definition] -> ProcessConfig -> (String, ElixirCode)
+generateForProcess m n vs cs defs (PConfig p as) =
   let name = moduleName m ++ "_" ++ p
       header = moduleHeader name m [] True
       defNext = ActionDefinition n [] [] (ActionOr as)
-   in (name, spec header [] vs [] defNext)
+   in (name, spec header cs vs [] defNext)
 
 
 -- filterDefs :: [Call] -> [Definition] -> [Definition]
@@ -88,11 +89,16 @@ definition g (ValueDefinition i ps v) = declaration i ps ++ ident (value g v) ++
 -- Comment translation, not specified
 definition _ (Comment s) = "# " ++ cleanTrailing s
 
+definitionName (ActionDefinition i _ _ _) = i
+definitionName (ValueDefinition i _ _) = i
+
+localDefinition g (ValueDefinition i ps v) = snake i ++ " = fn(variables" ++ intercalate "" (map ("," ++) ps) ++ ") -> " ++ value g v ++ "end"
+
 {-- \vdash_d --}
 actionsAndConditions :: Context -> Action -> ([ElixirCode], [ElixirCode])
 -- (CALL)
 actionsAndConditions g (ActionCall i ps) =
-  ([call (i ++ "Condition") ("variables" : map (value g) ps)], [call i ("variables" : map (value g) ps)])
+  ([call g (i ++ "Condition") ("variables" : map (value g) ps)], [call g i ("variables" : map (value g) ps)])
 -- (AND)
 actionsAndConditions g (ActionAnd as) =
   let (ics, ias) = unzipAndFold (map (actionsAndConditions g) as)
@@ -125,6 +131,9 @@ actionsAndConditions g (ActionIf p t e) =
              else cFold ce)
       a = ifExpr cp (aFold at) (aFold ae)
    in ([c], [a])
+actionsAndConditions g (ActionLet ds a) = let (cs, as) = actionsAndConditions (g ++ map ((,"local") . definitionName) ds) a
+                                              defs = unwords (map (localDefinition g) ds)
+                                          in (defs:cs, defs:as)
 -- (COND)
 actionsAndConditions g (Condition p) = ([value g p], [])
 -- [new] (EXT)
@@ -137,7 +146,7 @@ actionsAndConditions g (Exists i v a) =
 actionsAndConditions g (ForAll i v a) =
   let ig = (i, "param") : g
       (ics, ias) = actionsAndConditions ig a
-      c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ " end\n)"
+      c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ " end)"
    in ([c], ias)
 -- (TRA)
 actionsAndConditions g a = ([], [action g a])
@@ -179,7 +188,7 @@ value g (Lt v1 v2) = value g v1 ++ " < " ++ value g v2
 value g (Gte v1 v2) = value g v1 ++ " >= " ++ value g v2
 value g (Lte v1 v2) = value g v1 ++ " <= " ++ value g v2
 -- [new] (PRED-CALL)
-value g (ConditionCall i ps) = call i ("variables" : map (value g) ps)
+value g (ConditionCall i ps) = call g i ("variables" : map (value g) ps)
 -- (PRED-IN)
 value g (RecordBelonging v1 v2) = "Enum.member?(" ++ value g v2 ++ ", " ++ value g v1 ++ ")"
 -- [new] (PRED-NOTIN)
@@ -209,6 +218,7 @@ value g (Filtered i v p) =
 value g (Cardinality s) = "Enum.count(" ++ value g s ++ ")"
 value g (SetIn v s) = "MapSet.member?(" ++ value g s ++ ", " ++ value g v ++ ")"
 value g (SetMinus s1 s2) = "MapSet.difference(" ++ value g s1 ++ ", " ++ value g s2 ++ ")"
+value g (SetTimes s1 s2) = "(for x <- " ++ value g s1 ++ ", y <- " ++ value g s2  ++ ", do: {x, y})"
 -- (REC-LIT) and (REC-EX), aggregated to ensure ordering
 value g (Record rs) =
   let (literals, generations) = partition isLiteral rs
@@ -219,7 +229,7 @@ value g (Record rs) =
         else m ++ " |> Enum.into(" ++ l ++ ")"
 -- (REC-EXCEPT)
 value g (Except i es) =
-  intercalate "\n" (map (\(k, v) -> "Map.put(" ++ reference g i ++ ", " ++ value g k ++ ", " ++ value g v ++ ")") es)
+  intercalate "|>" (reference g i:map (\(k, v) -> "Map.put(" ++ value g k ++ ", " ++ value g v ++ ")") es)
 value g (FunGen i s v) = "Map.new(" ++ value g s ++ ", fn(" ++ i ++ ") -> {" ++ i ++ ", " ++ value ((i, "param") : g) v ++ "} end)"
 -- [new] (CASE)
 value g (Case ms) = "cond do\n" ++ intercalate "\n" (map (caseMatch g) ms) ++ "\nend\n"

Head.hs

@@ -60,6 +60,7 @@ data Action
   | ActionOr [Action]
   | ActionCall Identifier [Value]
   | ActionIf Value Action Action
+  | ActionLet [Definition] Action
   | Exists Identifier Value Action
   | ForAll Identifier Value Action
   deriving (Show, Eq)
@@ -91,6 +92,7 @@ data Value
   | Union Value Value
   | Filtered Identifier Value Value
   | Cardinality Value
+  | Fold Value Value Value
   | Record [(Key, Value)]
   | RecordSet [(Key, Value)]
   | Except Identifier [(Value, Value)]

Helpers.hs

@@ -29,8 +29,9 @@ sharedVariablesDeclaration shared =
 moduleContext (Module m _) = [(m, "module")]
 
 -- (CALL) helpers
-call i [] = snake i
-call i ps = snake i ++ "(" ++ intercalate ", " ps ++ ")"
+call g i [] = snake i
+call g i ps = let divider = if (i, "local") `elem` g then "." else ""
+              in snake i ++ divider ++ "(" ++ intercalate ", " ps ++ ")"
 
 -- (IF) helpers
 ifExpr c t e = "(if " ++ c ++ ", do: " ++ t ++ ", else: " ++ e ++ ")"
@@ -58,18 +59,20 @@ enclose s = "(" ++ s ++ ")"
 cFold :: [ElixirCode] -> ElixirCode
 cFold [] = "true"
 cFold [c] = c
-cFold cs = "Enum.all?([" ++ intercalate ", " cs ++ "])"
+cFold cs = let (preassignments, conditions) = partition preassignment cs
+           in intercalate "" (map (++ "\n") preassignments) ++ "Enum.all?([" ++ intercalate ", " conditions ++ "])"
 
 aFold :: [ElixirCode] -> ElixirCode
 aFold [] = "%{}"
 aFold as =
-  let (otherActions, actions) = partition preassignment as
+  let (preassignments, as') = partition preassignment as
+      (postAssignments, actions) = partition postassignment as'
       kvs = intercalate ",\n" (map keyValue actions)
       initialVariables =
         case actions of
           [] -> []
           _ -> ["%{\n" ++ ident kvs ++ "\n}"]
-   in mapMerge (initialVariables ++ otherActions)
+   in  intercalate "" (map (++ "\n") preassignments) ++ mapMerge (initialVariables ++ postAssignments)
 
 orFold :: [ElixirCode] -> ElixirCode
 orFold [] = "true"
@@ -86,11 +89,12 @@ keyValue a = drop 3 (dropEnd 2 a)
 mapMerge [m] = m
 mapMerge (m:ms) = "Map.merge(\n  " ++ m ++ ",\n" ++ ident (mapMerge ms) ++ ")\n"
 
-preassignment as =
+preassignment as = any (isPrefixOf " = ") (tails as)
+postassignment as =
   (head as) == '(' ||
   take 2 as == "if" || dropWhile (/= ':') as == [] || take 4 as == "Enum" || take 3 as == "Map" || take 4 as == "List"
 
-interpolate (Lit (Str i)) = "#{inspect " ++ i ++ "}"
+interpolate (Lit (Str i)) = i
 interpolate (Ref i) = "#{inspect " ++ i ++ "}"
 interpolate i = show i
 

JSONParser.hs

@@ -71,6 +71,7 @@ instance FromJSON Declaration where
       case filename :: String of
         "Functions" -> return Ignored
         "SequencesExt" -> return Ignored
+        "Apalache" -> return Ignored
         _ -> do
           k <- obj .: "kind"
           n <- obj .: "name"
@@ -110,7 +111,8 @@ instance FromJSON Expression where
 
 -- TODO: Parse this from config or something
 actionNames :: [String]
-actionNames = ["SendMsg", "Deactivate", "Environment", "System", "PassToken", "InitiateProbe", "Next"]
+-- actionNames = ["SendMsg", "Deactivate", "Environment", "System", "PassToken", "InitiateProbe", "Next"]
+actionNames = ["SubmitTransfer", "CommitTransfer", "SubmitTransferFrom", "CommitTransferFrom", "SubmitApprove", "CommitApprove", "Next"]
 
 notIgnored Ignored = False
 notIgnored _ = True
@@ -202,6 +204,12 @@ convertValue (OperEx o as) =
           "SET_FILTER" ->
             case as of
               [a1, a2, a3] -> liftA3 H.Filtered (identifier a1) (convertValue a2) (convertValue a3)
+          "SET_UNION2" ->
+            case as of
+              [a1, a2] -> liftA2 H.Union (convertValue a1) (convertValue a2)
+          "Apalache!ApaFoldSet" ->
+            case as of
+              [a1, a2, a3] -> liftA3 H.Fold (convertValue a1) (convertValue a2) (convertValue a3)
           "INT_RANGE" ->
             case as of
               [a1, a2] -> liftA2 H.Range (convertValue a1) (convertValue a2)
@@ -287,7 +295,7 @@ convertAction (OperEx o as) =
               [a1, a2, a3] -> liftA3 H.ForAll (identifier a1) (convertValue a2) (convertExpression a3)
           "UNCHANGED" ->
             case as of
-              [a] -> liftA H.Unchanged (manyIdentifiers a)
+              [a] -> fmap H.Unchanged (manyIdentifiers a)
           "AND" ->
             case as of
               es -> fmap H.ActionAnd (mapM convertExpression es)
@@ -300,15 +308,19 @@ convertAction (OperEx o as) =
           "OPER_APP" ->
             case as of
               (e:es) -> liftA2 H.ActionCall (identifier e) (mapM convertValue es)
+          "IF_THEN_ELSE" ->
+            case as of
+              [a1, a2, a3] -> liftA3 H.ActionIf (convertValue a1) (convertAction a2) (convertAction a3)
           op -> Left ("Unknown action operator " ++ op ++ " with args " ++ show as)
    in left (\s -> s ++ "\nwhen converting " ++ show (OperEx o as)) r
+convertAction (LetInEx ds b) = liftA2 H.ActionLet (mapM convertDefinitions ds) (convertAction b)
 
 convertExpression :: Expression -> Either String H.Action
-convertExpression (OperEx o as) =
-  if isPredicate (OperEx o as)
-    then convertValue (OperEx o as) >>= \x -> Right (H.Condition x)
-    else convertAction (OperEx o as)
 convertExpression (ValEx v) = convertValue (ValEx v) >>= \cv -> Right (H.Condition cv)
+convertExpression e =
+  if isPredicate e
+    then convertValue e >>= \x -> Right (H.Condition x)
+    else convertAction e
 
 actionOperators :: [String]
 actionOperators = ["PRIME", "UNCHANGED"]
@@ -321,8 +333,12 @@ isPredicate (OperEx o as) =
   all isPredicate as && if o == "OPER_APP"
                           then case identifier (head as) of {Right i -> i `notElem` actionNames}
                           else o `notElem` actionOperators
+isPredicate (LetInEx ds b) = all definitionIsPredicate ds && isPredicate b
 isPredicate _ = True
 
+definitionIsPredicate (Declaration k n ps (Just body)) = isPredicate body
+definitionIsPredicate _ = True
+
 isTemporal :: Expression -> Bool
 isTemporal (OperEx o as) = o `elem` temporalOperators || any isTemporal as
 isTemporal _ = False