interpreting variables as anchors

This commit is contained in:
David Mosbach 2023-09-02 02:11:21 +02:00
parent 46b038bd47
commit 79fd7c8ab6
4 changed files with 110 additions and 43 deletions

View File

@ -33,6 +33,7 @@ module Main where
import Data.Text.Encoding (encodeUtf8, decodeUtf8) import Data.Text.Encoding (encodeUtf8, decodeUtf8)
import Data.Text.Lazy (toStrict) import Data.Text.Lazy (toStrict)
import Debug.Trace (trace) import Debug.Trace (trace)
import DSLMain (dslMain)
--------------------------------------- ---------------------------------------
@ -45,6 +46,7 @@ module Main where
main :: IO () main :: IO ()
main = getArgs >>= process >>= finish where main = getArgs >>= process >>= finish where
process :: [String] -> IO Bool process :: [String] -> IO Bool
process ["--dsl"] = dslMain >> return True
process [path] = printEvents path >> runParser path >> return True process [path] = printEvents path >> runParser path >> return True
process args@[_, _] = generateJSON args >> return False process args@[_, _] = generateJSON args >> return False
process args@["--all", src, to] = processDirectory src to >> return False process args@["--all", src, to] = processDirectory src to >> return False

View File

@ -2,7 +2,10 @@
-- --
-- SPDX-License-Identifier: AGPL-3.0-or-later -- SPDX-License-Identifier: AGPL-3.0-or-later
{-# LANGUAGE FlexibleInstances, NoFieldSelectors, OverloadedRecordDot, DuplicateRecordFields #-} {-# LANGUAGE FlexibleInstances,
NoFieldSelectors,
OverloadedRecordDot,
DuplicateRecordFields #-}
module DSL ( module DSL (
parseSubStageDef, parseSubStageDef,
@ -13,7 +16,8 @@ module DSL (
Literal (..), Literal (..),
Variable (..), Variable (..),
Conjunction (..), Conjunction (..),
Predicate (..) Predicate (..),
LogVar
) where ) where
import qualified Data.ByteString.Lazy as BSL import qualified Data.ByteString.Lazy as BSL
@ -59,14 +63,14 @@ module DSL (
| Var String -- TODO refine to Single | Var String -- TODO refine to Single
| Neg Literal deriving Show | Neg Literal deriving Show
data Predicate = EdgeInHistory LogVar data Predicate = EdgeInHistory { ref :: LogVar }
| NodeInHistory LogVar | NodeInHistory { ref :: LogVar }
| PayloadFilled LogVar | PayloadFilled { ref :: LogVar }
| PreviousNode LogVar | PreviousNode { ref :: LogVar }
| EdgesInHistory [LogVar] | EdgesInHistory { refs :: [LogVar] }
| NodesInHistory [LogVar] | NodesInHistory { refs :: [LogVar] }
| PayloadsFilled [LogVar] | PayloadsFilled { refs :: [LogVar] }
| PreviousNodes [LogVar] deriving Show | PreviousNodes { refs :: [LogVar] } deriving Show
type LogVar = String type LogVar = String
@ -118,9 +122,10 @@ module DSL (
| otherwise = undefined | otherwise = undefined
parseShowWhen :: Parsec BSL.ByteString u When parseShowWhen :: Parsec BSL.ByteString u When
parseShowWhen = string "when" parseShowWhen = toWhen <$> optionMaybe (
string "when"
*> skipMany1 space *> skipMany1 space
*> (toWhen <$> optionMaybe (try (string isFulfilled) <|> string isUnfulfilled)) *> (try (string isFulfilled) <|> string isUnfulfilled))
where where
toWhen :: Maybe String -> When toWhen :: Maybe String -> When
toWhen Nothing = Always toWhen Nothing = Always

View File

@ -2,11 +2,14 @@
-- --
-- SPDX-License-Identifier: AGPL-3.0-or-later -- SPDX-License-Identifier: AGPL-3.0-or-later
module DSLMain where module DSLMain (dslMain) where
import DSL (parseSubStageDef) import DSL (parseSubStageDef)
import Data.ByteString.Lazy.UTF8 as BSLU import Data.ByteString.Lazy.UTF8 as BSLU
import Transpiler (resolve)
import Control.Monad (unless)
import Data.Either (isLeft, fromRight)
program = program =
"required substage InterneBearbeitung when unfulfilled {\n" ++ "required substage InterneBearbeitung when unfulfilled {\n" ++
@ -26,5 +29,32 @@ module DSLMain where
"}\n" ++ "}\n" ++
"}\n" "}\n"
main :: IO ()
main = print . parseSubStageDef $ BSLU.fromString program program2 =
"optional substage Vorbereitung {\n" ++
"let always_required = not edge_in_history(some-edge)\n" ++
"let sometimes_required = { payload_filled(foo), not bar }\n" ++
"case {\n" ++
"always_required,\n" ++
"edge_in_history(abbrechen),\n" ++
"not payload_filled(some-payload)\n" ++
"}\n" ++
"case {\n" ++
"always_required,\n" ++
"not previous_node(last-node)\n" ++
"}\n" ++
"}\n"
dslMain :: IO ()
dslMain = do
putStrLn "\n\t ### AST ###\n"
let subStage = parseSubStageDef $ BSLU.fromString program2
print subStage
unless (isLeft subStage) $ do
putStrLn "\n\t### Transpiler ###\n"
let transp = resolve $ fromRight undefined subStage
print transp

View File

@ -2,14 +2,17 @@
-- --
-- SPDX-License-Identifier: AGPL-3.0-or-later -- SPDX-License-Identifier: AGPL-3.0-or-later
{-# LANGUAGE OverloadedRecordDot, OverloadedStrings, NoFieldSelectors, DuplicateRecordFields, TupleSections #-} {-# LANGUAGE OverloadedRecordDot,
OverloadedStrings,
NoFieldSelectors,
DuplicateRecordFields,
TupleSections #-}
module Transpiler where module Transpiler where
import DSL import DSL
import Data.YAML (ToYAML (..), mapping, (.=)) import Data.YAML (ToYAML (..), mapping, (.=))
import Data.Text (Text, pack) import Data.Text (Text, pack)
import YamlParser (AnchorData (..)) import YamlParser (AnchorData (..), YAMLNode (Sequence))
import Data.YAML.Event (ScalarStyle(Literal))
import Control.Monad.State (State, evalState, get, put, unless, when) import Control.Monad.State (State, evalState, get, put, unless, when)
import Data.Map (Map, empty) import Data.Map (Map, empty)
import qualified Data.Map as M import qualified Data.Map as M
@ -24,32 +27,57 @@ module Transpiler where
data DNFLiteral = DNFLit { data DNFLiteral = DNFLit {
anchor :: AnchorData, anchor :: AnchorData,
literal :: ResolvedLiteral literal :: ResolvedLiteral
} } deriving (Show)
type DNF = [[DNFLiteral]] type DNF = [[DNFLiteral]]
data ResolvedSubStage = RSubStage {
head :: Head,
body :: DNF
} deriving (Show)
instance ToYAML SubStage where instance ToYAML ResolvedSubStage where
toYAML(SubStage head body) = mapping [ toYAML(RSubStage head body) = mapping [
"mode" .= if head.required then "required" else "optional" :: Text, "mode" .= if head.required then "required" else "optional" :: Text,
"show-when" .= case head.showWhen of "show-when" .= case head.showWhen of
Always -> "always" Always -> "always"
Fulfilled -> "fulfilled" Fulfilled -> "fulfilled"
Unfulfilled -> "unfulfilled" :: Text, Unfulfilled -> "unfulfilled" :: Text,
"predicate" .= mapping [ "dnf-terms" .= ("" :: Text)] -- toYAML (resolve body) ] "display-label" .= (undefined :: Text),
"predicate" .= mapping [ "dnf-terms" .= toYAML body ]
] ]
instance ToYAML DNFLiteral where
toYAML (DNFLit anchor (Pred' p)) = mapping [
"tag" .= ("variable" :: Text),
"var" .= mapping [
"tag" .= predToText p,
predToText p .= pack p.ref
]
]
where
predToText :: Predicate -> Text
predToText (EdgeInHistory _) = "edge-in-history"
predToText (NodeInHistory _) = "node-in-history"
predToText (PayloadFilled _) = "payload-filled"
predToText (PreviousNode _) = "previous-node"
predToText x = error $ show x ++ " is not fully resolved"
newtype ResolveError = ResolveError String newtype ResolveError = ResolveError String
instance Show ResolveError where
show (ResolveError s) = s
data StateData = StateData { data StateData = StateData {
innerVariables :: Map String (Variable, Bool), -- True means "already used" => anchor ref. False means "not used before" => new anchor innerVariables :: Map String (Variable, Bool), -- True means "already used" => anchor ref. False means "not used before" => new anchor
outerVariables :: Map String (Variable, Bool), outerVariables :: Map String (Variable, Bool),
disjunction :: DNF disjunction :: DNF
} }
type Resolver = ExceptT ResolveError (State StateData) --(Either ResolveError) type Resolver = ExceptT ResolveError (State StateData)
resolve :: Body -> Either ResolveError DNF resolve :: SubStage -> Either ResolveError ResolvedSubStage
resolve body = evalState (runExceptT (eval body)) initState resolve (SubStage head body) = evalState (runExceptT (RSubStage head <$> eval body)) initState
where where
initState = StateData empty (M.map (, False) body.variables) [] initState = StateData empty (M.map (, False) body.variables) []
@ -91,7 +119,7 @@ module Transpiler where
countNot x (Neg n) = countNot (x+1) n countNot x (Neg n) = countNot (x+1) n
countNot x lit = (lit, x) countNot x lit = (lit, x)
evalPredicate :: Literal -> Resolver DNFLiteral evalPredicate :: Literal -> Resolver DNFLiteral
evalPredicate (Pred (EdgesInHistory _)) = undefined evalPredicate (Pred (EdgesInHistory _)) = undefined -- Problem: how to handle negations without de morgan? forbid like negating block vars?
evalPredicate (Pred (NodesInHistory _)) = undefined evalPredicate (Pred (NodesInHistory _)) = undefined
evalPredicate (Pred (PayloadsFilled _)) = undefined evalPredicate (Pred (PayloadsFilled _)) = undefined
evalPredicate (Pred (PreviousNodes _)) = undefined evalPredicate (Pred (PreviousNodes _)) = undefined
@ -100,23 +128,25 @@ module Transpiler where
evalVariable :: Bool -> Literal -> Resolver (Either DNFLiteral [DNFLiteral]) evalVariable :: Bool -> Literal -> Resolver (Either DNFLiteral [DNFLiteral])
evalVariable negated (Var v) = do evalVariable negated (Var v) = do
state <- get state <- get
let maybeVar = M.lookup v state.innerVariables case M.lookup v state.innerVariables of
if isNothing maybeVar then throwError . ResolveError $ "Reference of unassigned variable: " ++ v else do Just (var, alreadyUsed) -> processVarRef var alreadyUsed True negated
let (var, alreadyUsed) = fromJust maybeVar Nothing -> case M.lookup v state.outerVariables of
unless alreadyUsed . put $ state { innerVariables = M.adjust (\(x,_) -> (x,True)) v state.innerVariables } Just (var, alreadyUsed) -> processVarRef var alreadyUsed False negated
let anchor = if alreadyUsed then AnchorAlias (pack v) else AnchorDef (pack v) Nothing -> throwError . ResolveError $ "Reference of unassigned variable: " ++ v
case var of processVarRef :: Variable -> Bool -> Bool -> Bool -> Resolver (Either DNFLiteral [DNFLiteral])
Single _ (Pred p) -> return $ Left DNFLit { anchor = anchor, literal = Pred' p } processVarRef var alreadyUsed isInner negated = do
Single _ v'@(Var _) -> evalVariable negated v' let updateVars = M.adjust (\(x,_) -> (x,True)) var.id
Single _ n@(Neg _) -> Left <$> (evalNegation n >>= \x -> return $ if x.anchor == NoAnchor then x {anchor = anchor} else x) state <- get
Block id conj -> preventBlockNegation negated id >> Right <$> evalConjunction conj [] unless alreadyUsed . put $ if isInner
then state { innerVariables = updateVars state.innerVariables }
else state { outerVariables = updateVars state.outerVariables }
let anchor = if alreadyUsed then AnchorAlias (pack var.id) else AnchorDef (pack var.id)
case var of
Single _ (Pred p) -> return $ Left DNFLit { anchor = anchor, literal = Pred' p }
Single _ v'@(Var _) -> evalVariable negated v'
Single _ n@(Neg _) -> Left <$> (evalNegation n >>= \x -> return $ if x.anchor == NoAnchor then x {anchor = anchor} else x)
Block id conj -> preventBlockNegation negated id >> Right <$> evalConjunction conj []
preventBlockNegation :: Bool -> String -> Resolver () preventBlockNegation :: Bool -> String -> Resolver ()
preventBlockNegation True s = throwError . ResolveError $ "Negating conjunction blocks is not permitted: " ++ s preventBlockNegation True s = throwError . ResolveError $ "Negating conjunction blocks is not permitted: " ++ s
preventBlockNegation False _ = return () preventBlockNegation False _ = return ()
instance ToYAML DNFLiteral where
toYAML (DNFLit anchor literal) = mapping [
-- "dnf-terms" .= toYAML
]