CSPM-ToProlog 0.4.0.0 → 0.5.0.0

raw patch · 4 files changed

+578/−386 lines, 4 filesdep +arraydep +ghc-primdep ~CSPM-Frontenddep ~prettyPVP ok

version bump matches the API change (PVP)

Dependencies added: array, ghc-prim

Dependency ranges changed: CSPM-Frontend, pretty

API changes (from Hackage documentation)

Files

• CSPM-ToProlog.cabal +10/−6
• src/Language/CSPM/AstToProlog.hs +129/−373
• src/Language/CSPM/CompileAstToProlog.hs +422/−0
• src/Language/CSPM/TranslateToProlog.hs +17/−7

@@ -1,33 +1,37 @@ Name:                CSPM-ToProlog-Version:             0.4.0.0+Version:             0.5.0.0 Synopsis:            some modules specific for the ProB tool Description:-  This package constains a translation from a CSPM AST to the representation+  This package contains a translation from a CSPM AST to the representation   used by the ProB tool.   This code is only interesting for ProB developers.  License:             BSD3 category:            Formal Methods License-File:        LICENSE-Author:              2006-2011 Marc Fontaine+Author:              2006-2012 Marc Fontaine Maintainer:          Marc Fontaine <fontaine@cs.uni-duesseldorf.de> Cabal-Version:  >= 1.10-Tested-With:    GHC==7.0.3+Tested-With:    GHC==7.4.1 Build-Type:     Simple  Library   Default-Language: Haskell2010   Build-Depends:-    CSPM-Frontend >= 0.7 && < 0.8-    ,pretty >= 1.0 && < 1.1+    CSPM-Frontend >= 0.9 && < 0.10+    ,pretty >= 1.1 && < 1.2     ,base >= 4.0 && <5.0     ,containers >= 0.4 && <0.5+    ,array >=0.4 && <0.5+    ,ghc-prim >= 0.2 && <0.3    Hs-Source-Dirs: src   ghc-options: -Wall    Exposed-modules:     Language.CSPM.AstToProlog+    Language.CSPM.CompileAstToProlog     Language.CSPM.TranslateToProlog   Other-modules:+    Paths_CSPM_ToProlog     Language.Prolog.PrettyPrint.Direct

@@ -1,416 +1,172 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Language.CSPM.AstToProlog--- Copyright   :  (c) Fontaine, Dobrikov 2011+-- Copyright   :  (c) Fontaine 2012 -- License     :  BSD3--- --- Maintainer  :  fontaine@cs.uni-duesseldorf.de+--+-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de -- Stability   :  experimental -- Portability :  GHC-only ----- Translation of an AST into Prolog terms, suitable for the ProB CSPM-Interpreter--- -------------------------------------------------------------------------------{-# OPTIONS_GHC -Wall -Werror -fno-warn-warnings-deprecations #-}+-- Convert an AST to Prolog. An experiment with the new GHC-Generic extentions+-- This would be more compact with SYB. +{-# LANGUAGE TypeOperators,FlexibleInstances, FlexibleContexts, DefaultSignatures, OverlappingInstances #-}+ module Language.CSPM.AstToProlog-(- cspToProlog-,mkSymbolTable-,mkSrcLoc-)+  (+    toProlog+  ) where -import Language.CSPM.Frontend (ModuleFromRenaming, frontendVersion)-import Language.CSPM.AST-import qualified Language.CSPM.SrcLoc as SrcLoc-import Language.Prolog.PrettyPrint.Direct+import Language.CSPM.Rename (ModuleFromRenaming)+import Language.CSPM.AST as AST+import Language.CSPM.CompileAstToProlog (mkSrcLoc)+import qualified Language.Prolog.PrettyPrint.Direct as Prolog (unTerm,atom,unAtom)+import Language.CSPM.SrcLoc as SrcLoc +import GHC.Generics as Generics import Text.PrettyPrint-import Data.Set (Set)-import qualified Data.Set as Set+import Data.Array.IArray as Array import qualified Data.IntMap as IntMap-import Data.Version --- | Translate a "LModule" into a "Doc" containing a number of Prolog facts.--- The LModule must be a renamed,i.e. contain only unique "Ident"ifier.-cspToProlog ::-  ModuleFromRenaming -- ^ the renamed Module-  -> Doc  -- ^ prolog facts-cspToProlog ast = header $+$ core-  where-    core = mkModule ast-    header = vcat [-         text ":- dynamic parserVersionNum/1, parserVersionStr/1."-        ,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."-        ,text ":- dynamic pragma/1."-        ,text ":- dynamic comment/2."-        ,text ":- dynamic assertBool/1, assertRef/5, assertTauPrio/6."-        ,text ":- dynamic assertModelCheckExt/4, assertModelCheck/3."-        ]+toProlog :: TP d => d -> Doc+toProlog = tp -plLocatedConstructs :: Set Const-plLocatedConstructs = Set.fromList -  [F_Interleave , F_Interrupt, F_Timeout, F_CHAOS,-   F_ExtChoice, F_IntChoice, F_Sequential, F_Hiding-  ]+class GTP f where+    gtp :: f a -> Doc -mkModule :: ModuleFromRenaming -> Doc-mkModule m-  = plPrg [-      singleClause $ clause $ nTerm "parserVersionNum"-        [pList $ map atom $ versionBranch $ frontendVersion]-     ,singleClause $ clause $ nTerm "parserVersionStr"-        [atom ("CSPM-Frontent-" ++ showVersion frontendVersion)]-     ,declGroup $ map clause $ declList $ moduleDecls m-     ,declGroup $ map mkPragma  $ modulePragmas m-     ,declGroup $ map mkComment $ moduleComments m-     ]+class GTPL f where+    gtpl :: Doc -> f a -> Doc -mkPragma :: String -> Clause-mkPragma s = clause $ nTerm "pragma" [aTerm s]+class TP f where+    tp :: f -> Doc+    default tp :: (Generic f, GTP (Rep f)) => f -> Doc+    tp = gtp . from -mkComment :: (Comment, SrcLoc.SrcLoc) -> Clause-mkComment (c, loc) = clause $ nTerm "comment" [com, mkSrcLoc loc]-  where-    com = case c of-      LineComment s ->  nTerm "lineComment" [aTerm s]-      BlockComment s -> nTerm "blockComment" [aTerm s]-      PragmaComment s -> nTerm "pragmaComment" [aTerm s]+class TPL f where+    tpl :: Doc -> f -> Doc+    default tpl :: (Generic f, GTPL (Rep f)) => Doc -> f -> Doc+    tpl l = gtpl l . from -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"-  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, nTerm "src_span_operator" [plLoc expr, plLoc op]]-    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]+instance TPL f => TP (Labeled f) where+    tp a = tpl (tp $ srcLoc a) $ unLabel a -    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]+instance TPL Decl+instance TPL Ident where tpl l = tpl l . unUIdent+instance TPL Pattern+instance TPL Exp -    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+instance TPL UniqueIdent where+    tpl l ident = text "'UniqueIdent'" <> parens (l<> comma <> i)       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]+         i = case idType ident of+                 TransparentID -> atom $ realName ident+                 _ -> atom $ newName ident -    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]+instance TPL AssertDecl+instance TPL AST.Constructor+instance TPL TypeDef+instance TPL Range+instance TPL CompGen+instance TPL LinkList+instance TPL Rename+instance TPL Link+instance TPL BuiltIn+instance TPL CommField+instance TPL [Labeled CompGen] where tpl _ = tp -eList :: [LExp] -> Term-eList l = pList h-  where h :: [Term]-        h = map te l+instance TPL RefineOp+instance TPL TauRefineOp+instance TPL FDRModels+instance TPL FdrExt -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]+instance TP ModuleFromRenaming where+    tp m = text "module" <> parens ( hcat $ punctuate comma [+         tp $ moduleSrcLoc m+        ,tp $ moduleDecls m+        ,tp $ moduleComments m+        ,tp $ modulePragmas m+        ]) -declList :: [LDecl] -> [Term]-declList l = concatMap td l+instance TP Comment+instance TP SrcLoc where tp = Prolog.unTerm . mkSrcLoc -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 e]-      l -> nTerm "agent_curry" [-              nTerm (plName ident) $ map (pList . map tp) l -             ,te e-             ,plLoc e]-    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]+instance TP [Char] where tp = atom -    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]]+instance TP f => TP [f] where+    tp l = brackets $ hcat $ punctuate comma $ map tp l +instance TP f => TP (Maybe f) where+    tp Nothing = text "none"+    tp (Just x) = tp x +instance (TP a, TP b) => TP (a,b) where+    tp (a,b) = parens (tp a <> comma <> tp b) -    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 -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+instance TP Integer  where  tp = integer+instance TP Int      where tp = integer . fromIntegral+instance TP e => TP (Array Int e)     where tp = tp . Array.elems+instance TP e => TP (IntMap.IntMap e) where tp = tp . IntMap.elems -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 -uniquePlName :: UniqueIdent -> String-uniquePlName i = newName i+instance TP Bool+instance TP Const+instance TP FunCase+instance TP AST.Selector+instance TP UniqueIdent where tp = tpl (text "none") +instance (GTP a, GTP b) => GTP (a :*: b) where+    gtp (a :*: b) = gtp a <+> comma <+> gtp b -plLoc :: Labeled x -> Term-plLoc = mkSrcLoc . srcLoc+instance (GTPL a, GTPL b) => GTPL (a :*: b) where+    gtpl l (a :*: b) = gtpl l a <+> comma <+> gtpl l b --- | Translate a source location to Prolog-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+instance (GTP l, GTP r) => GTP (l :+: r) where+    gtp (L1 l) = gtp l+    gtp (R1 r) = gtp r +instance (GTPL l, GTPL r) => GTPL (l :+: r) where+    gtpl s (L1 l) = gtpl s l+    gtpl s (R1 r) = gtpl s r --- | Translate a "AstAnnotation" with "UnqiueIdentifier" (i.e. a Symboltable)--- into a "Doc" containing Prolog facts-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 -> "Funktion or Process"-    ConstrID   -> "Constructor of Datatype"-    DataTypeID     -> "Datatype"-    TransparentID  -> "Transparent function"-    BuiltInID  -> "BuiltIn primitive"-    VarID -> case prologMode i of-      PrologGround -> "Ident (Groundrep.)"-      PrologVariable -> "Ident (Prolog Variable)"+instance (GTP t, Datatype r) => GTP (M1 D r t)  where+    gtp = gtp . unM1 --- | Map the abstract datatype LBuiltIn back to plain Strings for Prolog-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 -> "\\"        +instance (GTPL t, Datatype r) => GTPL (M1 D r t)  where+    gtpl l = gtpl l . unM1 -unBuiltIn :: LBuiltIn -> Const-unBuiltIn x =  let (BuiltIn fkt) = unLabel x in fkt+instance (GTP t, Generics.Constructor c) => GTP (M1 C c t)  where+    gtp x = hcat [ atom $ conName x, lparen, gtp $ unM1 x, rparen]++instance (GTPL t, Generics.Constructor c) => GTPL (M1 C c t)  where+    gtpl l x = hcat [ atom $ conName x, lparen, l, comma, gtpl l $ unM1 x, rparen]++instance (GTP t, Generics.Selector c) => GTP (M1 S c t)  where+    gtp = gtp . unM1++instance (GTPL t, Generics.Selector c) => GTPL (M1 S c t)  where+    gtpl l = gtpl l . unM1++instance TP t => GTP (K1 R t)  where+    gtp x = tp $ unK1 x++instance TP t => GTPL (K1 R t)  where+    gtpl _l x = tp $ unK1 x++instance TP t => GTP (K1 P t)  where+    gtp x = hsep [ text "rec" , lparen, tp $ unK1 x, rparen]++instance TP t => GTPL (K1 P t)  where+    gtpl _ x = hsep [ text "rec" , lparen, tp $ unK1 x, rparen]++instance GTP V1 where gtp _ = text "V1"+instance GTPL V1 where gtpl _ _ = text "V1"++instance GTP U1 where gtp _ = text "U1"+instance GTPL U1 where gtpl _ _ = text "U1"++atom :: String -> Doc+atom = Prolog.unAtom . Prolog.atom

@@ -0,0 +1,422 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Language.CSPM.CompileAstToProlog+-- Copyright   :  (c) Fontaine, Dobrikov 2011+-- License     :  BSD3+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Translation of an AST into Prolog terms, suitable for the ProB CSPM-Interpreter+-- +-----------------------------------------------------------------------------+{-# OPTIONS_GHC -Wall -Werror -fno-warn-warnings-deprecations #-}++module Language.CSPM.CompileAstToProlog+(+ cspToProlog+,mkSymbolTable+,mkSrcLoc+)+where++import Language.CSPM.Frontend (ModuleFromRenaming, frontendVersion)+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+import Data.Version++-- | Translate a "LModule" into a "Doc" containing a number of Prolog facts.+-- The LModule must be a renamed,i.e. contain only unique "Ident"ifier.+cspToProlog ::+  ModuleFromRenaming -- ^ the renamed Module+  -> Doc  -- ^ prolog facts+cspToProlog ast = header $+$ core+  where+    core = mkModule ast+    header = vcat [+         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."+        ,text ":- dynamic pragma/1."+        ,text ":- dynamic comment/2."+        ,text ":- dynamic assertBool/1, assertRef/5, assertTauPrio/6."+        ,text ":- dynamic assertModelCheckExt/4, assertModelCheck/3."+        ]++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 [+      singleClause $ clause $ nTerm "parserVersionNum"+        [pList $ map atom $ versionBranch $ frontendVersion]+     ,singleClause $ clause $ nTerm "parserVersionStr"+        [atom ("CSPM-Frontent-" ++ showVersion frontendVersion)]+     ,declGroup $ map clause $ declList $ moduleDecls m+     ,declGroup $ map mkPragma  $ modulePragmas m+     ,declGroup $ map mkComment $ moduleComments m+     ]++mkPragma :: String -> Clause+mkPragma s = clause $ nTerm "pragma" [aTerm s]++mkComment :: (Comment, SrcLoc.SrcLoc) -> Clause+mkComment (c, loc) = clause $ nTerm "comment" [com, mkSrcLoc loc]+  where+    com = case c of+      LineComment s ->  nTerm "lineComment" [aTerm s]+      BlockComment s -> nTerm "blockComment" [aTerm s]+      PragmaComment s -> nTerm "pragmaComment" [aTerm s]++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)+  {- evil special case: ProB handles seq as builtin, but it is not -}+  CallFunction fkt args | (isSeq $ unLabel fkt) -> nTerm "builtin_call" [nTerm "seq" ( flatArgs args)]+    where+      isSeq (Var x) = (realName $ unUIdent $ unLabel x) == "seq"+      isSeq _ = False+  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"+  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, nTerm "src_span_operator" [plLoc expr, plLoc op]]+    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 e]+      l -> nTerm "agent_curry" [+              nTerm (plName ident) $ map (pList . map tp) l +             ,te e+             ,plLoc e]+    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++plNameTerm :: LIdent -> Term+plNameTerm l+    = case (idType uIdent,prologMode uIdent) of+        (VarID,PrologVariable) -> plVar ("_" ++ uniquePlName uIdent)+        (VarID,PrologGround)   -> term $ atom $ uniquePlName uIdent+        _             -> term $ plName l+    where uIdent = unUIdent $ unLabel l++plName :: LIdent -> Atom+plName l+    = case idType uIdent of+         TransparentID -> atom $ realName uIdent+         VarID         -> error ("plName : " ++ show l)+         _             -> atom $ uniquePlName uIdent+    where uIdent = unUIdent $ unLabel l++uniquePlName :: UniqueIdent -> String+uniquePlName = newName+++plLoc :: Labeled x -> Term+plLoc = mkSrcLoc . srcLoc++-- | Translate a source location to Prolog+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+++-- | Translate a "AstAnnotation" with "UnqiueIdentifier" (i.e. a Symboltable)+-- into a "Doc" containing Prolog facts+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 -> "Funktion or Process"+    ConstrID   -> "Constructor of Datatype"+    DataTypeID     -> "Datatype"+    TransparentID  -> "Transparent function"+    BuiltInID  -> "BuiltIn primitive"+    VarID -> case prologMode i of+      PrologGround -> "Ident (Groundrep.)"+      PrologVariable -> "Ident (Prolog Variable)"++-- | Map the abstract datatype LBuiltIn back to plain Strings for Prolog+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

@@ -15,15 +15,19 @@ {-# LANGUAGE ScopedTypeVariables #-} module Language.CSPM.TranslateToProlog (-  translateToProlog+   toPrologVersion+  ,translateToProlog ) where  import Language.CSPM.Frontend as Frontend import qualified Language.CSPM.SrcLoc as SrcLoc import qualified Language.CSPM.Token as Token (lexEMsg,lexEPos,alexLine,alexCol,alexPos)-import Language.CSPM.AstToProlog (cspToProlog,mkSymbolTable)+import Language.CSPM.CompileAstToProlog (cspToProlog,mkSymbolTable)+import Language.CSPM.AstToProlog (toProlog) import Language.Prolog.PrettyPrint.Direct+import Paths_CSPM_ToProlog (version)+import Data.Version (Version,showVersion)  import Control.Exception import System.Exit@@ -31,6 +35,10 @@ import System.CPUTime import Text.PrettyPrint +-- | The version of the CSPM-ToProlog library+toPrologVersion :: Version+toPrologVersion = version+ -- | 'translateToProlog' reads a CSPM specification from inFile -- and writes the Prolog representation to outFile. -- It handles all lexer and parser errors and catches all exceptions.@@ -83,10 +91,12 @@   time_start_renaming <- getCPUTime   (astNew, renaming) <- eitherToExc $ renameModule ast   let-    plCode = cspToProlog astNew-    symbolTable = mkSymbolTable $ identDefinition renaming+      plCode = cspToProlog astNew+      symbolTable = mkSymbolTable $ identDefinition renaming+      moduleFact  = toProlog astNew   output <- evaluate $ show $ vcat [        mkResult "ok" "" 0 0 0+     ,moduleFact      ,plCode      ,symbolTable      ]@@ -101,9 +111,9 @@  defaultHeader :: Doc defaultHeader -  = text ":- dynamic parserVersionNum/1, parserVersionStr/1, parseResult/5."---    $$ simpleFact "parserVersionNum" [aTerm versionNum ]---    $$ simpleFact "parserVersionStr" [aTerm versionStr ]+  =    text ":- dynamic parserVersionNum/1, parserVersionStr/1, parseResult/5."+    $$ text ":- dynamic module/4."+    $$ simpleFact "parserVersionStr" [aTerm $ showVersion toPrologVersion]  simpleFact :: String -> [Term] -> Doc simpleFact a l= plPrg [declGroup [clause $ nTerm a l]]