diff --git a/CSPM-ToProlog.cabal b/CSPM-ToProlog.cabal
--- a/CSPM-ToProlog.cabal
+++ b/CSPM-ToProlog.cabal
@@ -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
diff --git a/src/Language/CSPM/AstToProlog.hs b/src/Language/CSPM/AstToProlog.hs
--- a/src/Language/CSPM/AstToProlog.hs
+++ b/src/Language/CSPM/AstToProlog.hs
@@ -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
diff --git a/src/Language/CSPM/CompileAstToProlog.hs b/src/Language/CSPM/CompileAstToProlog.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/CSPM/CompileAstToProlog.hs
@@ -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
diff --git a/src/Language/CSPM/TranslateToProlog.hs b/src/Language/CSPM/TranslateToProlog.hs
--- a/src/Language/CSPM/TranslateToProlog.hs
+++ b/src/Language/CSPM/TranslateToProlog.hs
@@ -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]]