Merge Predicate and Value types

bugarela · Jun 29, 2022 · 50346da · 50346da
1 parent 7ff22bb
commit 50346da
Show file tree

Hide file tree

Showing 13 changed files with 7,759 additions and 260 deletions.
diff --git a/Elixir.hs b/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 (If p t e) = let cp = predicate 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])
+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])
@@ -115,89 +116,49 @@ action _ (Unchanged is) =  let u = \i -> snake i ++ ": variables[:" ++ snake i +
                            in "%{ " ++ intercalate ",\n" (map u is) ++ " }"
 
 -- [new] needs testing
-action g (Value v) = value g v
+-- action g (Value v) = value g v
+
+action _ a = error("Missing action case: " ++ show a)
 
-action _ a = error(show a)
 {-- \vdash_p --}
-predicate :: Context -> Predicate -> 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,34 +190,76 @@ 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"
 
 -- Others, not specified
-value _ (Str s) = show s
 value g (Range n1 n2) = value g n1 ++ ".." ++ value g n2
-value _ (Boolean b) = if b then "true" else "false"
 value g (Ref i) = reference g i
 value g (Tuple as) = "{" ++ intercalate ", " (map (value g) as) ++ "}"
-value _ (Num d) = show d
 value g (Neg a) = "-" ++ value' g a
 value g (Add a b) = value' g a ++ " + " ++ value' g b
 value g (Sub a b) = value' g a ++ " - " ++ value' g b
 value g (Mul a b) = value' g a ++ " * " ++ value' g b
 value g (Div a b) = value' g a ++ " / " ++ value' g b
 value g (Mod a b) = "rem(" ++ value' g a ++ ", " ++ value' g b ++ ")"
 value g (Domain v) = "Map.keys(" ++ value g v ++ ")"
+value _ (Lit l) = lit l
 value _ v = error("Missing value case: " ++ show v)
 
-value' _ (Num d) = show d
+value' _ (Lit (Num d)) = show d
 value' g (Ref i) = reference g i
 value' g e = "(" ++ value g e ++ ")"
 
+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) = snake i ++ ": " ++ value g v
+mapping g ((Key i), v) = show i ++ ": " ++ value g v
 mapping g ((All i a), v) = let ig = (i, "param"):g
                            in value g a ++ " |> Enum.map(fn (" ++ i ++ ") -> {" ++ i ++ ", " ++ value ig v ++ "} end)"
 -- (VAL-*)

diff --git a/Head.hs b/Head.hs
@@ -21,37 +21,61 @@ data Definition = ActionDefinition Identifier [Parameter] Documentation Action
                 | Comment String
                 deriving(Show, Eq)
 
-data Key = Key Identifier | All Identifier Value deriving(Show, Eq)
-
-data CaseMatch = Match Predicate Value | DefaultMatch Value deriving(Show, Eq)
-
-data Predicate = Equality Value Value | Inequality Value Value
-               | Gt Value Value | Lt Value Value
-               | Gte Value Value | Lte Value Value
-               | RecordBelonging Value Value
-               | RecordNotBelonging Value Value
-               | And [Predicate]
-               | Or [Predicate]
-               | Not Predicate
-               | ConditionCall Identifier [Value]
-               | PExists Identifier Value Predicate
-               | PForAll Identifier Value Predicate
-               deriving(Show, Eq)
-
-data Action = Condition Predicate | Value Value | Primed Identifier Value | Unchanged [Identifier] | ActionNot Action
-            | ActionAnd [Action] | ActionOr [Action] | ActionCall Identifier [Value]
-            | If Predicate Action Action | Exists Identifier Value Action | ForAll Identifier Value Action deriving(Show, Eq)
-
-data Value = Set [Value] | Tuple [Value] | FunSet Value Value | FunGen Identifier Value Value | SetTimes Value Value
-           | Union Value Value | Filtered Identifier Value Predicate | Cardinality Value
-           | Record [(Key, Value)] | Except Identifier [(Value, Value)] | Case [CaseMatch] | Domain Value
-           | Str String | Boolean Bool | FullSet String | Index Value Value | Range Value Value
-           | Num Integer
+data Lit = Str String | Boolean Bool | Num Integer | FullSet String deriving(Show, Eq)
+
+data Key = Key Lit | All Identifier Value deriving(Show, Eq)
+
+data CaseMatch = Match Value Value | DefaultMatch Value deriving(Show, Eq)
+
+data Action = Condition Value
+            | Primed Identifier Value
+            | Unchanged [Identifier]
+            | ActionNot Action
+            | ActionAnd [Action]
+            | ActionOr [Action]
+            | ActionCall Identifier [Value]
+            | ActionIf Value Action Action
+            | Exists Identifier Value Action
+            | ForAll Identifier Value Action
+            deriving(Show, Eq)
+
+data Value = Equality Value Value
+           | Inequality Value Value
+           | Gt Value Value | Lt Value Value
+           | Gte Value Value | Lte Value Value
+           | RecordBelonging Value Value
+           | RecordNotBelonging Value Value
+           | And [Value]
+           | Or [Value]
+           | Not Value
+           | If Value Value Value
+           | ConditionCall Identifier [Value]
+           | PExists Identifier Value Value
+           | PForAll Identifier Value Value
+           | Let [Definition] Value
+           | Set [Value]
+           | Tuple [Value]
+           | FunSet Value Value
+           | FunGen Identifier Value Value
+           | SetTimes Value Value
+           | SetIn Value Value
+           | SetMinus Value Value
+           | Union Value Value
+           | Filtered Identifier Value Value
+           | Cardinality Value
+           | Record [(Key, Value)]
+           | RecordSet [(Key, Value)]
+           | Except Identifier [(Value, Value)]
+           | Case [CaseMatch]
+           | Domain Value
+           | Index Value Value
+           | Range Value Value
            | Ref String
            | Neg Value
            | Add Value Value
            | Sub Value Value
            | Mul Value Value
            | Div Value Value
            | Mod Value Value
+           | Lit Lit
            deriving (Show, Eq)
diff --git a/Helpers.hs b/Helpers.hs
@@ -71,7 +71,7 @@ mapMerge (m:ms) = "Map.merge(\n  " ++ m ++ ",\n" ++ ident (mapMerge ms) ++ ")\n"
 
 preassignment as = (head as) == '(' || take 2 as == "if" || dropWhile (/= ':') as == [] || take 4 as == "Enum" || take 3 as == "Map" || take 4 as == "List"
 
-interpolate (Str i) = "#{inspect " ++ i ++ "}"
+interpolate (Lit (Str i)) = "#{inspect " ++ i ++ "}"
 interpolate (Ref i) = "#{inspect " ++ i ++ "}"
 interpolate i = show i
 
@@ -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)