{-# LANGUAGE ScopedTypeVariables #-}
module Language.Trans.Spec2Copilot where
import Data.List ( intercalate, intersect, lookup, union )
import Data.Maybe ( fromMaybe )
import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier )
import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..),
Requirement (..), Spec (..))
spec2Copilot :: forall a
. String
-> [(String, String)]
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> Spec a
-> Either String (String, String, String, String, String)
spec2Copilot :: forall a.
String
-> [(String, String)]
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> Spec a
-> Either String (String, String, String, String, String)
spec2Copilot String
specName [(String, String)]
typeMaps [(String, String)] -> a -> a
exprTransform a -> String
showExpr Spec a
spec =
(String, String, String, String, String)
-> Either String (String, String, String, String, String)
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
externs, String
internals, String
reqs, String
triggers, String
specName)
where
externs :: String
externs = [String] -> String
unlines'
([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [[String]] -> [String]
forall a. [a] -> [[a]] -> [a]
intercalate [String
""]
([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ (ExternalVariableDef -> [String])
-> [ExternalVariableDef] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map ExternalVariableDef -> [String]
externVarToDecl
(Spec a -> [ExternalVariableDef]
forall a. Spec a -> [ExternalVariableDef]
externalVariables Spec a
spec)
where
externVarToDecl :: ExternalVariableDef -> [String]
externVarToDecl ExternalVariableDef
i = [ String
propName
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: Stream "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"("
String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
safeMap [(String, String)]
typeMaps (ExternalVariableDef -> String
externalVariableType ExternalVariableDef
i)
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
, String
propName
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"extern"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (ExternalVariableDef -> String
externalVariableName ExternalVariableDef
i)
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Nothing"
]
where
propName :: String
propName = [(String, String)] -> String -> String
safeMap [(String, String)]
nameSubstitutions (ExternalVariableDef -> String
externalVariableName ExternalVariableDef
i)
internals :: String
internals = [String] -> String
unlines'
([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [[String]] -> [String]
forall a. [a] -> [[a]] -> [a]
intercalate [String
""]
([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ (InternalVariableDef -> [String])
-> [InternalVariableDef] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map InternalVariableDef -> [String]
internalVarToDecl
(Spec a -> [InternalVariableDef]
forall a. Spec a -> [InternalVariableDef]
internalVariables Spec a
spec)
where
internalVarToDecl :: InternalVariableDef -> [String]
internalVarToDecl InternalVariableDef
i = (\String
implem ->
[ String
propName
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: Stream "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"("
String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
safeMap [(String, String)]
typeMaps (InternalVariableDef -> String
internalVariableType InternalVariableDef
i)
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
, String
propName
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
implem
]) String
implementation
where
propName :: String
propName = [(String, String)] -> String -> String
safeMap [(String, String)]
nameSubstitutions (InternalVariableDef -> String
internalVariableName InternalVariableDef
i)
implementation :: String
implementation = (InternalVariableDef -> String
internalVariableExpr InternalVariableDef
i)
reqs :: String
reqs :: String
reqs = [String] -> String
unlines'
([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [[String]] -> [String]
forall a. [a] -> [[a]] -> [a]
intercalate [String
""]
([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ (Requirement a -> [String]) -> [Requirement a] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map Requirement a -> [String]
reqToDecl (Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
spec)
where
reqToDecl :: Requirement a -> [String]
reqToDecl Requirement a
i = [ String
reqComment, String
reqSignature
, [(String, String)] -> String
reqBody [(String, String)]
nameSubstitutions
]
where
reqName :: String
reqName = [(String, String)] -> String -> String
safeMap [(String, String)]
nameSubstitutions (Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
i)
reqComment :: String
reqComment = String
"-- | " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"-- @" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"-- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Requirement a -> String
forall a. Requirement a -> String
requirementDescription Requirement a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"-- @"
reqSignature :: String
reqSignature = String
reqName
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Stream" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Bool"
reqBody :: [(String, String)] -> String
reqBody [(String, String)]
subs = String
reqName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++
(a -> String
showExpr ([(String, String)] -> a -> a
exprTransform [(String, String)]
subs (Requirement a -> a
forall a. Requirement a -> a
requirementExpr Requirement a
i)))
triggers :: String
triggers :: String
triggers = [String] -> String
unlines' ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Requirement a -> String) -> [Requirement a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Requirement a -> String
reqTrigger (Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
spec)
where
reqTrigger :: Requirement a -> String
reqTrigger :: Requirement a -> String
reqTrigger Requirement a
r = String
" trigger " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
handlerName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (not "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
propName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
handlerArg
where
handlerName :: String
handlerName = String
"handler" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
sanitizeUCIdentifier (Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
r)
propName :: String
propName = [(String, String)] -> String -> String
safeMap [(String, String)]
nameSubstitutions (Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
r)
handlerArg :: String
handlerArg =
case (Requirement a -> Maybe String
forall a. Requirement a -> Maybe String
requirementResultType Requirement a
r, Requirement a -> Maybe a
forall a. Requirement a -> Maybe a
requirementResultExpr Requirement a
r) of
(Just String
ty, Just a
ex) -> String
"[ arg (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
showExpr a
ex String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ) ]"
(Maybe String, Maybe a)
_ -> String
"[]"
internalVariableMap :: [(String, String)]
internalVariableMap =
(String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String -> String
sanitizeLCIdentifier String
x)) [String]
internalVariableNames
externalVariableMap :: [(String, String)]
externalVariableMap =
(String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String -> String
sanitizeLCIdentifier String
x)) [String]
externalVariableNames
requirementNameMap :: [(String, String)]
requirementNameMap =
(String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String
"prop" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
sanitizeUCIdentifier String
x)) [String]
requirementNames
nameSubstitutions :: [(String, String)]
nameSubstitutions = [(String, String)]
internalVariableMap
[(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++ [(String, String)]
externalVariableMap
[(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++ [(String, String)]
requirementNameMap
internalVariableNames :: [String]
internalVariableNames = (InternalVariableDef -> String)
-> [InternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map InternalVariableDef -> String
internalVariableName
([InternalVariableDef] -> [String])
-> [InternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [InternalVariableDef]
forall a. Spec a -> [InternalVariableDef]
internalVariables Spec a
spec
externalVariableNames :: [String]
externalVariableNames = (ExternalVariableDef -> String)
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ExternalVariableDef -> String
externalVariableName
([ExternalVariableDef] -> [String])
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [ExternalVariableDef]
forall a. Spec a -> [ExternalVariableDef]
externalVariables Spec a
spec
requirementNames :: [String]
requirementNames = (Requirement a -> String) -> [Requirement a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Requirement a -> String
forall a. Requirement a -> String
requirementName
([Requirement a] -> [String]) -> [Requirement a] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
spec
specAnalyze :: Spec a -> Either String (Spec a)
specAnalyze :: forall a. Spec a -> Either String (Spec a)
specAnalyze Spec a
spec
| Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
evnClash)
= String -> Either String (Spec a)
forall a b. a -> Either a b
Left (String -> Either String (Spec a))
-> String -> Either String (Spec a)
forall a b. (a -> b) -> a -> b
$ String
"Name clash detected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
evnClash
| Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
ivnClash)
= String -> Either String (Spec a)
forall a b. a -> Either a b
Left (String -> Either String (Spec a))
-> String -> Either String (Spec a)
forall a b. (a -> b) -> a -> b
$ String
"Name clash detected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
ivnClash
| Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
reqClash)
= String -> Either String (Spec a)
forall a b. a -> Either a b
Left (String -> Either String (Spec a))
-> String -> Either String (Spec a)
forall a b. (a -> b) -> a -> b
$ String
"Name clash detected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
reqClash
| Bool
otherwise
= Spec a -> Either String (Spec a)
forall a b. b -> Either a b
Right Spec a
spec
where
ivnClash :: [String]
ivnClash = [String]
internalVariableNames'
[String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([String]
externalVariableNames' [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` [String]
requirementNames')
evnClash :: [String]
evnClash = [String]
externalVariableNames'
[String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([String]
internalVariableNames' [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` [String]
requirementNames')
reqClash :: [String]
reqClash = [String]
requirementNames'
[String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([String]
internalVariableNames'
[String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` [String]
externalVariableNames')
internalVariableNames' :: [String]
internalVariableNames' = ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
internalVariableMap
externalVariableNames' :: [String]
externalVariableNames' = ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
externalVariableMap
requirementNames' :: [String]
requirementNames' = ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
requirementNameMap
internalVariableMap :: [(String, String)]
internalVariableMap =
(String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String -> String
sanitizeLCIdentifier String
x)) [String]
internalVariableNames
externalVariableMap :: [(String, String)]
externalVariableMap =
(String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String -> String
sanitizeLCIdentifier String
x)) [String]
externalVariableNames
requirementNameMap :: [(String, String)]
requirementNameMap =
(String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> (String
x, String
"prop" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
sanitizeUCIdentifier String
x)) [String]
requirementNames
internalVariableNames :: [String]
internalVariableNames = (InternalVariableDef -> String)
-> [InternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map InternalVariableDef -> String
internalVariableName
([InternalVariableDef] -> [String])
-> [InternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [InternalVariableDef]
forall a. Spec a -> [InternalVariableDef]
internalVariables Spec a
spec
externalVariableNames :: [String]
externalVariableNames = (ExternalVariableDef -> String)
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ExternalVariableDef -> String
externalVariableName
([ExternalVariableDef] -> [String])
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [ExternalVariableDef]
forall a. Spec a -> [ExternalVariableDef]
externalVariables Spec a
spec
requirementNames :: [String]
requirementNames = (Requirement a -> String) -> [Requirement a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Requirement a -> String
forall a. Requirement a -> String
requirementName
([Requirement a] -> [String]) -> [Requirement a] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
spec
safeMap :: [(String, String)] -> String -> String
safeMap :: [(String, String)] -> String -> String
safeMap [(String, String)]
ls String
k = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
k (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
k [(String, String)]
ls
unlines' :: [String] -> String
unlines' :: [String] -> String
unlines' = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n"