module Language.CSPM.AstToProlog
(
cspToProlog
,mkSymbolTable
,mkSrcLoc
)
where
import Language.CSPM.Frontend (ModuleFromRenaming)
import Language.CSPM.AST
import qualified Language.CSPM.SrcLoc as SrcLoc
import Language.Prolog.PrettyPrint.Direct
import Text.PrettyPrint
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.IntMap as IntMap
cspToProlog ::
ModuleFromRenaming
-> Doc
cspToProlog ast =
let
core = mkModule ast
header =
(text ":- dynamic channel/2, bindval/3, agent/3.")
$+$
(text ":- dynamic agent_curry/3, symbol/4.")
$+$
(text ":- dynamic dataTypeDef/2, subTypeDef/2, nameType/2.")
$+$
(text ":- dynamic cspTransparent/1.")
$+$
(text ":- dynamic cspPrint/1.")
in header $+$ core
plLocatedConstructs :: Set Const
plLocatedConstructs = Set.fromList
[F_Interleave , F_Interrupt, F_Timeout, F_CHAOS,
F_ExtChoice, F_IntChoice, F_Sequential, F_Hiding
]
mkModule :: ModuleFromRenaming -> Doc
mkModule m
= plPrg [declGroup $ map clause $ declList $ moduleDecls m]
te :: LExp -> Term
te expr = case unLabel expr of
Var i -> let u = unUIdent $ unLabel i in
case (prologMode u,idType u) of
(PrologGround,VarID) -> nTerm "val_of" [plNameTerm i, plLoc expr]
_ -> plNameTerm i
IntExp i -> nTerm "int" [atom i]
SetExp r Nothing -> nTerm "setExp" [range r]
SetExp r (Just comp) -> nTerm "setExp" [range r, comprehension comp]
ListExp r Nothing -> nTerm "listExp" [range r]
ListExp r (Just comp) -> nTerm "listExp" [range r, comprehension comp]
ClosureComprehension (e,c) -> nTerm "closureComp" [comprehension c ,eList e]
Let decl e -> nTerm "let" [pList $ declList decl, te e]
Ifte cond t e -> nTerm "ifte" [te cond, te t, te e,condPos,thenPos,elsePos] where
condPos = mkSrcLoc $ SrcLoc.srcLocFromTo (srcLoc expr) (srcLoc cond)
thenPos = mkSrcLoc $ SrcLoc.srcLocBetween (srcLoc cond) (srcLoc t)
elsePos = mkSrcLoc $ SrcLoc.srcLocBetween (srcLoc t) (srcLoc e)
CallFunction fkt args -> case args of
[l] -> nTerm "agent_call" [plLoc fkt, te fkt, eList l]
(_:_:_) -> nTerm "agent_call_curry" [te fkt, pList $ map eList args ]
[] -> error ("CallFunction without args" ++ show expr)
CallBuiltIn builtIn args
-> if ((unBuiltIn builtIn) `Set.member` plLocatedConstructs )
then nTerm "builtin_call" [ nTerm (builtInToString builtIn) (plLoc expr : flatArgs args) ]
else nTerm "builtin_call" [ nTerm (builtInToString builtIn) $ flatArgs args ]
Lambda patl e -> nTerm "lambda" [pList $ map tp patl, te e]
Stop -> nTerm "stop" [plLoc expr]
Skip -> nTerm "skip" [plLoc expr]
CTrue -> aTerm "true"
CFalse -> aTerm "false"
Events -> aTerm "Events"
BoolSet -> aTerm "boolType"
IntSet -> aTerm "intType"
ProcSet -> aTerm "procType"
TupleExp i -> nTerm "tupleExp" [eList i]
Parens e -> term $ te e
AndExp a b -> nTerm "bool_and" [te a, te b]
OrExp a b -> nTerm "bool_or" [te a, te b]
NotExp a -> nTerm "bool_not" [te a]
NegExp a -> nTerm "negate" [te a]
Fun1 op a -> nTerm (builtInToString op) [te a]
Fun2 op a b -> if ((unBuiltIn op) `Set.member` plLocatedConstructs )
then nTerm (builtInToString op) [te a, te b, plLoc expr]
else nTerm (builtInToString op) [te a, te b]
DotTuple a -> nTerm "dotTuple" [eList a]
Closure l -> nTerm "closure" [ eList l]
ProcSharing al p1 p2 -> nTerm "sharing" [te al, te p1, te p2,plLoc expr]
ProcAParallel a1 a2 p1 p2
-> nTerm "aParallel" [te a1, te p1, te a2, te p2, plLoc expr]
ProcLinkParallel ll a b
-> nTerm "lParallel" [ linkList ll, te a, te b, plLoc ll ]
ProcRenaming ren Nothing p
-> nTerm "procRenaming" [ renameList ren, te p, plLoc expr ]
ProcRenaming ren (Just gen) p
-> nTerm "procRenamingComp" [te p, comprehension $ unLabel gen, renameList ren]
ProcException p1 e p2 -> nTerm "exception" [te p1, te e, te p2, plLoc expr]
ProcRepSequence gen proc -> nTerm "repSequence" [comprehension $ unLabel gen, te proc, plLoc gen]
ProcRepInternalChoice gen proc
-> nTerm "repInternalChoice" [comprehension $ unLabel gen, te proc, plLoc gen]
ProcRepInterleave gen proc
-> nTerm "repInterleave" [comprehension $ unLabel gen, te proc, plLoc gen]
ProcRepExternalChoice gen proc -> nTerm "repChoice" [comprehension $ unLabel gen, te proc, plLoc gen]
ProcRepAParallel gen alph proc
-> nTerm "procRepAPrallel" [comprehension $ unLabel gen, nTerm "pair" [te alph, te proc] ,plLoc gen]
ProcRepLinkParallel gen links proc
-> nTerm "procRepLinkPrallel" [linkList links, comprehension $ unLabel gen, te proc, plLoc gen]
ProcRepSharing gen share proc
-> nTerm "procRepSharing" [te share, comprehension $ unLabel gen, te proc, plLoc gen]
PrefixExp ch fields proc -> nTerm "prefix" [plLoc ch, mkCommFields fields, te ch, te proc,prefixLoc ]
where
prefixLoc = mkSrcLoc $ SrcLoc.srcLocBetween
(if null fields then srcLoc $ ch else srcLoc $ last fields)
(srcLoc proc)
PrefixI {} -> missingCase "PrefixI"
ExprWithFreeNames {} -> missingCase "ExprWithFreeNames"
LambdaI {} -> missingCase "LambdaI"
LetI {} -> missingCase "LetI"
where
missingCase :: String -> Term
missingCase s = error $ "missing case in te :" ++ s
flatArgs :: [[LExp]] -> [Term]
flatArgs l = concatMap (map te) l
comprehension :: [LCompGen] -> Term
comprehension l = pList $ map (comp . unLabel ) l
where
comp (Guard e) = nTerm "comprehensionGuard" [te e]
comp (Generator pat e) = nTerm "comprehensionGenerator" [tp pat, te e]
linkList :: LLinkList -> Term
linkList ll = case unLabel ll of
LinkList l -> nTerm "linkList" [ pList $ map (mklink . unLabel) l ]
LinkListComprehension gen l
-> nTerm "linkListComp" [ comprehension gen, pList $ map (mklink . unLabel) l ]
where
mklink (Link a b) = nTerm "link" [te a,te b]
renameList :: [LRename] -> Term
renameList l = pList $ map (mkRen . unLabel) l
where
mkRen (Rename a b) = nTerm "rename" [te a, te b]
mkCommFields :: [LCommField] -> Term
mkCommFields l = pList $ map (mkCF . unLabel) l
where
mkCF (InComm p) = nTerm "in" [tp p]
mkCF (OutComm e) = nTerm "out" [te e]
mkCF (InCommGuarded p e) = nTerm "inGuard" [tp p, te e]
range :: LRange -> Term
range r = case unLabel r of
RangeOpen a -> nTerm "rangeOpen" [te a]
RangeClosed a b -> nTerm "rangeClosed" [te a, te b]
RangeEnum l -> nTerm "rangeEnum" [eList l]
eList :: [LExp] -> Term
eList l = pList h
where h :: [Term]
h = map te l
tp :: LPattern -> Term
tp pattern = case unLabel pattern of
IntPat i -> nTerm "int" [atom i]
TruePat -> aTerm "true"
FalsePat -> aTerm "false"
WildCard -> plWildCard
VarPat i -> plNameTerm i
ConstrPat i -> plNameTerm i
Also l -> tpList "alsoPattern" l
Append l -> tpList "appendPattern" l
DotPat l -> tpList "dotpat" l
SingleSetPat p -> tpList "singleSetPat" [p]
EmptySetPat -> aTerm "emptySet"
ListEnumPat l -> tpList "listPat" l
TuplePat l -> tpList "tuplePat" l
Selector {} -> error "missing case in tp : Selector"
Selectors {} -> error "missing case in tp : Selectors"
where
tpList :: String -> [LPattern] -> Term
tpList f l = nTerm f [pList $ map tp l]
declList :: [LDecl] -> [Term]
declList l = concatMap td l
td :: LDecl -> [Term]
td decl = case unLabel decl of
PatBind pat e -> [ nTerm "bindval" [tp pat, te e, plLoc decl]]
FunBind fkt caseList -> map (mkFunBind fkt) caseList
Assert e -> mkAssert e
Transparent idList
-> [ nTerm "cspTransparent" [pList $ map plName idList] ]
SubType i constrL -> [ nTerm "subTypeDef" [plNameTerm i, mkConstructorList constrL] ]
DataType i constrL -> [ nTerm "dataTypeDef" [plNameTerm i, mkConstructorList constrL] ]
NameType i t -> [ nTerm "nameType" [plNameTerm i, nTerm "type" [mkTypeDef t]] ]
Channel ids tdef -> map (mkChannel tdef) ids
Print e -> [ nTerm "cspPrint" [te e] ]
where
mkFunBind :: LIdent -> FunCase -> Term
mkFunBind ident (FunCase pat e) = case pat of
[p] -> nTerm "agent" [
nTerm (plName ident) $ map tp p
,te e
,plLoc ident]
l -> nTerm "agent_curry" [
nTerm (plName ident) $ map (pList . map tp) l
,te e
,plLoc ident]
mkFunBind _ (FunCaseI {}) = error "unexpected case in mkFunBind: FunCaseI"
mkConstructorList :: [LConstructor] -> Term
mkConstructorList l = pList $ map mkConstructor l
mkConstructor :: LConstructor -> Term
mkConstructor c = case unLabel c of
Constructor i Nothing -> nTerm "constructor" [plNameTerm i]
Constructor i (Just t) -> nTerm "constructorC" [plNameTerm i, mkTypeDef t]
mkTypeDef :: LTypeDef -> Term
mkTypeDef t = case unLabel t of
TypeTuple l -> nTerm "typeTuple" [eList l]
TypeDot l -> nTerm "dotTupleType" [eList l]
mkChannel :: Maybe LTypeDef -> LIdent -> Term
mkChannel Nothing i = nTerm "channel" [ plNameTerm i, nTerm "type" [term $ atom "dotUnitType" ]]
mkChannel (Just t) i = nTerm "channel" [ plNameTerm i, nTerm "type" [mkTypeDef t]]
mkAssert :: LAssertDecl -> [Term]
mkAssert ass = case unLabel ass of
AssertBool e -> [ nTerm "assertBool" [te e] ]
AssertRefine b p1 m p2
-> [ nTerm "assertRef" [aTerm $ show b, te p1, termShow m, te p2, plLoc decl] ]
AssertTauPrio b p1 m p2 e
-> [ nTerm "assertTauPrio" [aTerm $ show b, te p1, termShow m, te p2, te e, plLoc decl] ]
AssertModelCheck b p m (Just ext)
-> [ nTerm "assertModelCheckExt" [aTerm $ show b, te p, termShow m, termShow ext] ]
AssertModelCheck b p m Nothing
-> [ nTerm "assertModelCheck" [aTerm $ show b, te p, termShow m ] ]
termShow :: Show a => Labeled a -> Term
termShow = aTerm . show . unLabel
plName :: LIdent -> Atom
plName l
= let uIdent = unUIdent $ unLabel l in case idType uIdent of
TransparentID -> atom $ realName uIdent
VarID -> error ("plName : " ++ show l)
_ -> atom $ uniquePlName uIdent
plNameTerm :: LIdent -> Term
plNameTerm l
= let uIdent = unUIdent $ unLabel l in case (idType uIdent,prologMode uIdent) of
(VarID,PrologVariable) -> plVar ("_" ++ uniquePlName uIdent)
(VarID,PrologGround) -> term $ atom $ uniquePlName uIdent
_ -> term $ plName l
uniquePlName :: UniqueIdent -> String
uniquePlName i = newName i
plLoc :: Labeled x -> Term
plLoc = mkSrcLoc . srcLoc
mkSrcLoc :: SrcLoc.SrcLoc -> Term
mkSrcLoc loc = case loc of
SrcLoc.TokPos {} -> nTerm "src_position"
[itt $ SrcLoc.getStartLine loc
,itt $ SrcLoc.getStartCol loc
,itt $ SrcLoc.getStartOffset loc
,itt $ SrcLoc.getTokenLen loc ]
SrcLoc.TokSpan {} -> nTerm "src_span"
[itt $ SrcLoc.getStartLine loc
,itt $ SrcLoc.getStartCol loc
,itt $ SrcLoc.getEndLine loc
,itt $ SrcLoc.getEndCol loc
,itt $ SrcLoc.getStartOffset loc
,itt $ SrcLoc.getTokenLen loc ]
SrcLoc.FixedLoc {} -> nTerm "src_span"
[itt $ SrcLoc.getStartLine loc
,itt $ SrcLoc.getStartCol loc
,itt $ SrcLoc.getEndLine loc
,itt $ SrcLoc.getEndCol loc
,itt $ SrcLoc.getStartOffset loc
,itt $ SrcLoc.getTokenLen loc ]
_ -> term $ atom "no_loc_info_available"
where
itt :: Int -> Term
itt = term . iatom . fromIntegral
iatom :: Integer -> Atom
iatom = atom
mkSymbolTable :: AstAnnotation UniqueIdent -> Doc
mkSymbolTable ids
= plPrg [declGroup $ map mkSymbol $ IntMap.elems ids]
where
mkSymbol :: UniqueIdent -> Clause
mkSymbol i = clause $ nTerm "symbol"
[aTerm $ uniquePlName i
,aTerm $ realName i
,mkSrcLoc $ bindingLoc i
,aTerm $ pprintIDType i
]
pprintIDType :: UniqueIdent -> String
pprintIDType i = case idType i of
ChannelID -> "Channel"
NameTypeID -> "Nametype"
(FunID x) -> "Funktion or Process ( Arity :"++show x ++")"
(ConstrID d) -> "Constructor of Datatype "++d
DataTypeID -> "Datatype"
TransparentID -> "Transparent function"
VarID -> case prologMode i of
PrologGround -> "Ident (Groundrep.)"
PrologVariable -> "Ident (Prolog Variable)"
builtInToString :: LBuiltIn -> String
builtInToString x =
let (BuiltIn bi) = unLabel x in
case bi of
F_STOP -> "STOP"
F_SKIP -> "SKIP"
F_true -> "true"
F_false -> "false"
F_not -> "not"
F_and -> "and"
F_or -> "or"
F_Int -> "Int"
F_Bool -> "Bool"
F_Events -> "Events"
F_CHAOS -> "CHAOS"
F_union -> "union"
F_inter -> "inter"
F_diff -> "diff"
F_Union -> "Union"
F_Inter -> "Inter"
F_member -> "member"
F_card -> "card"
F_empty -> "empty"
F_set -> "set"
F_Set -> "Set"
F_Seq -> "Seq"
F_null -> "null"
F_head -> "head"
F_tail -> "tail"
F_concat -> "concat"
F_elem -> "elem"
F_length -> "length"
F_Concat -> "^"
F_Len2 -> "#"
F_Mult -> "*"
F_Div -> "/"
F_Mod -> "%"
F_Add -> "+"
F_Sub -> "-"
F_Eq -> "=="
F_NEq -> "!="
F_GE -> ">="
F_LE -> "<="
F_LT -> "<"
F_GT -> ">"
F_Guard -> "&"
F_Sequential -> ";"
F_Interrupt -> "/\\"
F_ExtChoice -> "[]"
F_Timeout -> "[>"
F_IntChoice -> "|~|"
F_Interleave -> "|||"
F_Hiding -> "\\"
unBuiltIn :: LBuiltIn -> Const
unBuiltIn x = let (BuiltIn fkt) = unLabel x in fkt