Add simpler example and extend parsing

Elixir.hs

@@ -73,26 +73,27 @@ actionsAndConditions g (ActionOr as) = let (ics, ias) = unzipAndFold (map (actio
                                        in (if allUnchanged as then ["false"] else [orFold ics], if ias == [] then [] else [decide g as])
 
 -- (IF)
-actionsAndConditions g (ActionIf p t e) = let cp = predicate g p
+actionsAndConditions g (ActionIf p t e) = let cp = value g p
                                               (ct, at) = actionsAndConditions g t
                                               (ce, ae) = actionsAndConditions g e
                                               c = ifExpr cp (if isUnchanged t then "false" else cFold ct) (if isUnchanged e then "false" else cFold ce)
                                               a = ifExpr cp (aFold at) (aFold ae)
                                           in ([c], [a])
 
 -- (COND)
-actionsAndConditions g (Condition p) = ([predicate g p], [])
+actionsAndConditions g (Condition p) = ([value g p], [])
 
 -- [new] (EXT)
-actionsAndConditions g (Exists i v (ActionOr as)) = let ig = (i, "param"):g
-                                                        (ics, _) = unzipAndFold (map (actionsAndConditions ig) as)
-                                                        c = "Enum.any?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ orFold ics ++ "end\n)"
-                                                    in ([c], [decide g [Exists i v (ActionOr as)]])
+actionsAndConditions g (Exists i v a) = let ig = (i, "param"):g
+                                            (ics, _) = actionsAndConditions ig a
+                                            c = "Enum.any?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ "end\n)"
+                                        in ([c], [decide g [a]])
+
 -- [new]: must test
-actionsAndConditions g (ForAll i v (ActionAnd as)) = let ig = (i, "param"):g
-                                                         (ics, ias) = unzipAndFold (map (actionsAndConditions ig) as)
-                                                         c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ "end\n)"
-                                                     in ([c], ias)
+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)"
+                                        in ([c], ias)
 
 -- (TRA)
 actionsAndConditions g a = ([], [action g a])
@@ -117,87 +118,47 @@ action _ (Unchanged is) =  let u = \i -> snake i ++ ": variables[:" ++ snake i +
 -- [new] needs testing
 -- action g (Value v) = value g v
 
-action _ a = error(show a)
+action _ a = error("Missing action case: " ++ show a)
+
 {-- \vdash_p --}
-predicate :: Context -> Value -> ElixirCode
+value :: Context -> Value -> ElixirCode
 
 -- (PRED-EQ)
-predicate g (Equality v1 v2) = value g v1 ++ " == " ++ value g v2
+value g (Equality v1 v2) = value g v1 ++ " == " ++ value g v2
 
 -- (PRED-INEQ)
-predicate g (Inequality v1 v2) = value g v1 ++ " != " ++ value g v2
+value g (Inequality v1 v2) = value g v1 ++ " != " ++ value g v2
 
 -- Similar rules
-predicate g (Gt v1 v2) = value g v1 ++ " > " ++ value g v2
-predicate g (Lt v1 v2) = value g v1 ++ " < " ++ value g v2
-predicate g (Gte v1 v2) = value g v1 ++ " >= " ++ value g v2
-predicate g (Lte v1 v2) = value g v1 ++ " <= " ++ value g v2
+value g (Gt v1 v2) = value g v1 ++ " > " ++ value g v2
+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)
-predicate g (ConditionCall i ps) = call (i ++ "Condition") ("variables":map (value g) ps)
+value g (ConditionCall i ps) = call (i ++ "Condition") ("variables":map (value g) ps)
 
 -- (PRED-IN)
-predicate g (RecordBelonging v1 v2) = "Enum.member?(" ++ value g v2 ++ ", " ++ value g v1 ++ ")"
+value g (RecordBelonging v1 v2) = "Enum.member?(" ++ value g v2 ++ ", " ++ value g v1 ++ ")"
 
 -- [new] (PRED-NOTIN)
-predicate g (RecordNotBelonging v1 v2) = "not " ++ predicate g (RecordBelonging v1 v2)
+value g (RecordNotBelonging v1 v2) = "not " ++ value g (RecordBelonging v1 v2)
 
 -- (PRED-NOT)
-predicate g (Not p) = "not " ++ predicate g p
+value g (Not p) = "not " ++ value g p
 
 -- [new] (PRED-AND)
-predicate g (And ps) =  intercalate " and " (map (predicate g) ps)
+value g (And ps) =  intercalate " and " (map (value g) ps)
 
 -- [new] (PRED-OR)
-predicate g (Or ps) =  intercalate " or " (map (predicate g) ps)
-
--- [new] (PRED-ALL)
-predicate g (PForAll i v p) = "Enum.all?(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ predicate ((i, "param"):g) p ++ " end)"
-
-predicate _ p = error("Missing predicate case: " ++ show p)
-
-{-- \vdash_init --}
-initialState :: Context -> Action -> ElixirCode
-
--- (INIT-AND)
-initialState g (ActionAnd as) = aFold (map (initialState g) as)
-
--- (INIT-EQ)
-initialState g (Condition (Equality (Ref i) v)) = "%{ " ++ snake i ++ ": " ++ value g v ++ " }"
-
--- Restriction
-initialState _ p = error("Init condition ambiguous: " ++ show p)
-
--- Comment extraction
-ini g (ActionDefinition _ _ doc a) = comment doc ++ initialState g a
-
-
-{-- \vdash_next --}
-next :: Context -> Definition -> ElixirCode
-
--- (NEXT)
-next g (ActionDefinition _ _ doc a) = let (_, actions) = actionsAndConditions g a
-                                in funDoc doc ++ "def main(variables) do\n" ++ ident (logState ++ "main(" ++ (aFold actions)) ++ ")\nend\n"
-
-
-{-- \vdash_i -}
-actionInfo :: Context -> Action -> ElixirCode
--- (INFO-EX)
-actionInfo g (Exists i v (ActionOr as)) = let ig = (i, "param"):g
-                                              l = map (actionInfo ig) as
-                                              s = intercalate ",\n" l
-                                          in "Enum.map(" ++ value ig v ++ ", fn (" ++ i ++ ") -> [\n" ++ ident s ++ "\n] end\n)"
+value g (Or ps) =  intercalate " or " (map (value g) ps)
 
--- (INFO-DEF)
-actionInfo g a = let (cs, as) = actionsAndConditions g a
-                     n = "action: \"" ++ actionName a ++ "\""
-                     c = "condition: " ++ cFold cs
-                     s = "state: " ++ aFold as
-                 in "%{ " ++ intercalate ", " [n,c,s] ++  " }"
+value g (If c t e) = "if " ++ value g c ++ ", do: " ++ value g t ++ ", else: " ++ value g e
 
+-- [new] (PRED-ALL)
+value g (PForAll i v p) = "Enum.all?(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) p ++ " end)"
 
-{-- \vdash_v --}
-value :: Context -> Value -> ElixirCode
+value g (PExists i v p) = "Enum.any?(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) p ++ " end)"
 
 -- (REC-INDEX)
 value g (Index v k) = value g v ++ "[" ++ value g k ++ "]"
@@ -211,11 +172,15 @@ value g (Union s (Set [v])) = "MapSet.put(" ++ value g s ++ ", " ++ value g v ++
 value g (Union s1 s2) = "MapSet.union(" ++ value g s1 ++ ", " ++ value g s2 ++ ")"
 
 -- [new] (SET-FILT)
-value g (Filtered i v p) = "Enum.filter(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ predicate ((i, "param"):g) p ++ " end)"
+value g (Filtered i v p) = "Enum.filter(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) p ++ " end)"
 
 -- [new] (SET-CAR)
 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 ++ ")"
+
 -- (REC-LIT) and (REC-EX), aggregated to ensure ordering
 value g (Record rs) = let (literals, generations) = partition isLiteral rs
                           m = intercalate " ++ " (map (mapping g) generations) -- merge
@@ -225,6 +190,8 @@ value g (Record rs) = let (literals, generations) = partition isLiteral rs
 -- (REC-EXCEPT)
 value g (Except i es) = unlines (map (\(k,v) -> "Map.put(" ++ reference g i ++ ", " ++ value g k ++ ", " ++ value g v ++ ")") es)
 
+value g (FunGen i s v) = "MapSet.new(" ++ value g s ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) v ++ " end)"
+
 -- [new] (CASE)
 value g (Case ms) = "cond do\n" ++ intercalate "\n" (map (caseMatch g) ms) ++ "\nend\n"
 
@@ -250,8 +217,46 @@ lit (Str s) = show s
 lit (Num d) = show d
 lit (Boolean b) = if b then "true" else "false"
 
+{-- \vdash_init --}
+initialState :: Context -> Value -> ElixirCode
+
+-- (INIT-AND)
+initialState g (And as) = aFold (map (initialState g) as)
+
+-- (INIT-EQ)
+initialState g (Equality (Ref i) v) = "%{ " ++ snake i ++ ": " ++ value g v ++ " }"
+
+-- Restriction
+initialState _ p = error("Init condition ambiguous: " ++ show p)
+
+-- Comment extraction
+ini g (ActionDefinition _ _ doc (Condition a)) = comment doc ++ initialState g a
+
+
+{-- \vdash_next --}
+next :: Context -> Definition -> ElixirCode
+
+-- (NEXT)
+next g (ActionDefinition _ _ doc a) = let (_, actions) = actionsAndConditions g a
+                                in funDoc doc ++ "def main(variables) do\n" ++ ident (logState ++ "main(" ++ (aFold actions)) ++ ")\nend\n"
+
+
+{-- \vdash_i -}
+actionInfo :: Context -> Action -> ElixirCode
+-- (INFO-EX)
+actionInfo g (Exists i v (ActionOr as)) = let ig = (i, "param"):g
+                                              l = map (actionInfo ig) as
+                                              s = intercalate ",\n" l
+                                          in "Enum.map(" ++ value ig v ++ ", fn (" ++ i ++ ") -> [\n" ++ ident s ++ "\n] end\n)"
+
+-- (INFO-DEF)
+actionInfo g a = let (cs, as) = actionsAndConditions g a
+                     n = "action: \"" ++ actionName a ++ "\""
+                     c = "condition: " ++ cFold cs
+                     s = "state: " ++ aFold as
+                 in "%{ " ++ intercalate ", " [n,c,s] ++  " }"
 
-caseMatch g (Match p v) = predicate g p ++ " -> " ++ value g v
+caseMatch g (Match p v) = value g p ++ " -> " ++ value g v
 caseMatch g (DefaultMatch v) = "true -> " ++ value g v
 
 mapping g ((Key i), v) = show i ++ ": " ++ value g v

Helpers.hs

@@ -113,5 +113,4 @@ findVariables ds = concat (map (\d -> case d of {Variables cs -> cs; _ -> [] })
 
 findIdentifier i ds = case find (isNamed i) ds of
                         Just a -> a
-                        Nothing -> error("Definition not found: " ++ (show i))
-
+                        Nothing -> error("Definition not found: " ++ show i ++ " in " ++ show ds)

JSONParser.hs

@@ -70,6 +70,7 @@ instance FromJSON Expression where
         "NameEx" -> fmap NameEx (obj .: "name")
         "OperEx" -> liftA2 OperEx (obj .: "oper") (obj .: "args")
         "LetInEx" -> liftA2 LetInEx (obj .: "decls") (obj .: "body")
+        _ -> fail ("Unknown expression kind: " ++ exprKind)
 
 notIgnored Ignored = False
 notIgnored _ = True
@@ -89,7 +90,7 @@ convertDefinitions (Declaration k n body) = case body of
 convertBody :: Kind -> String -> Expression -> Either String H.Definition
 convertBody k i e = case k of
                       "OperEx" -> Right (H.Comment "A")
-                      "TlaOperDecl" -> convertExpression e >>= \x -> Right (H.ActionDefinition i [] [] x)
+                      "TlaOperDecl" -> if isTemporal e then Right (H.Comment (show e)) else convertExpression e >>= \x -> Right (H.ActionDefinition i [] [] x)
                       "TlaAssumeDecl" -> Right (H.Comment (show e))
                       _ -> Left ("Unknown body kind " ++ show k)
 
@@ -109,9 +110,6 @@ manyIdentifiers (OperEx o as) = case o of
                                   "TUPLE" -> mapM identifier as
                                   _ -> Left ("Not tuple operator: " ++ o)
 
--- identifierFromString :: Expression -> Either String H.Identifier
--- identifierFromString (ValEx (TlaStr s)) = Right s
-
 val :: TlaValue -> H.Lit
 val (TlaStr s) = H.Str s
 val (TlaBool b) = H.Boolean b
@@ -164,6 +162,8 @@ convertValue (OperEx o as) = let r = case o of
                                         [x1, x2] -> liftA2 H.Equality (convertValue x1) (convertValue x2)
                                       "GT" -> case as of
                                         [x1, x2] -> liftA2 H.Gt (convertValue x1) (convertValue x2)
+                                      "LT" -> case as of
+                                        [x1, x2] -> liftA2 H.Lt (convertValue x1) (convertValue x2)
                                       "GE" -> case as of
                                         [x1, x2] -> liftA2 H.Gte (convertValue x1) (convertValue x2)
                                       "LE" -> case as of
@@ -185,7 +185,6 @@ convertValue (OperEx o as) = let r = case o of
                                       op -> Left ("Unknown value operator " ++ op)
                              in left (\s -> s ++ "\nwhen converting " ++ show (OperEx o as)) r
 convertValue (LetInEx ds b) = liftA2 H.Let (mapM convertDefinitions ds) (convertValue b)
--- convertValue e = Left ("Unexpected expression while converting value: " ++ show e)
 
 convertAction :: Expression -> Either String H.Action
 convertAction (OperEx o as) = let r = case o of
@@ -203,16 +202,23 @@ convertAction (OperEx o as) = let r = case o of
                              in left (\s -> s ++ "\nwhen converting " ++ show (OperEx o as)) r
 
 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 (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)
 
 actionOperators :: [String]
 actionOperators = ["PRIME", "UNCHANGED"]
 
+temporalOperators :: [String]
+temporalOperators = ["GLOBALLY", "STUTTER", "IMPLIES", "LEADS_TO"]
+
 isPredicate :: Expression -> Bool
 isPredicate (OperEx o as) = o `notElem` actionOperators && all isPredicate as
 isPredicate _ = True
 
+isTemporal :: Expression -> Bool
+isTemporal (OperEx o as) = o `elem` temporalOperators || any isTemporal as
+isTemporal _ = False
+
 convertRecordValues :: [Expression] -> Either String [(H.Key, H.Value)]
 convertRecordValues [] = Right []
 convertRecordValues (ValEx l:v:vs) = do e <- convertValue v