As.hs revision 4eeeca8e688ff5fb58bad5610d12f3f7a9866e85
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaederModule : $Header$
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederDescription : abstract syntax of VSE programs and dynamic logic
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) C. Maeder, DFKI 2008
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederMaintainer : Christian.Maeder@dfki.de
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : provisional
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederCASL extention to VSE programs and dynamic logic
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederas described on page 4-7 (Sec 2.3.1, 2.5.2, 2.5.4, 2.6) of
0095c7efbddd0ffeed6aaf8ec015346be161d819Till MossakowskiBruno Langenstein's API description
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | procedure or function declaration
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata Profile = Profile [Procparam] (Maybe SORT) deriving (Show, Eq)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- | further VSE signature entries
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdata Sigentry = Procedure Id Profile Range deriving (Show, Eq)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdata Procdecls = Procdecls [Annoted Sigentry] Range deriving (Show, Eq)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | a procedure parameter
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata Procparam = Procparam Paramkind SORT deriving (Show, Eq, Ord)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | input or output procedure parameter kind
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata Paramkind = In | Out deriving (Show, Eq, Ord)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | wrapper for positions
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederdata Ranged a = Ranged { unRanged :: a, range :: Range }
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder deriving (Show, Eq, Ord)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | programs with ranges
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedertype Program = Ranged PlainProgram
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | programs based on restricted terms and formulas
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata PlainProgram =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | Assign VAR (TERM ())
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | Call Id [TERM ()] -- ^ a procedure call
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | Return (TERM ())
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | Block [VAR_DECL] Program
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | Seq Program Program
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | If (FORMULA ()) Program Program
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | While (FORMULA ()) Program
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski deriving (Show, Eq, Ord)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | alternative variable declaration
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata VarDecl = VarDecl VAR SORT (Maybe (TERM ())) Range deriving Show
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertoVarDecl :: [VAR_DECL] -> [VarDecl]
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertoVarDecl = concatMap
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder (\ (Var_decl vs s r) -> map (\ v -> VarDecl v s Nothing r) vs)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiaddInits :: [VarDecl] -> Program -> ([VarDecl], Program)
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederaddInits vs p = case vs of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski vd@(VarDecl v s Nothing z) : r -> case unRanged p of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Seq (Ranged (Assign av t) _) p2 | v == av
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -> let (rs, q) = addInits r p2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in (VarDecl v s (Just t) z : rs, q)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski _ -> let (rs, q) = addInits r p
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in (vd : rs, q)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | extend CASL formulas by box or diamond formulas
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdata Dlformula = Dlformula BoxOrDiamond Program (FORMULA Dlformula) Range
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski deriving (Show, Eq, Ord)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | box or diamond indicator
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederdata BoxOrDiamond = Box | Diamond deriving (Show, Eq, Ord)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata ProcKind = Proc | Func deriving (Show, Eq, Ord)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | procedure definitions as basic items becoming sentences
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdata Defproc = Defproc ProcKind Id [VAR] Program Range deriving (Show, Eq, Ord)
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder-- | a label plus a list of procedure definitions
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederdata Procdefs = Procdefs [Defproc] Range deriving (Show, Eq, Ord)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | the sentences for the logic
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata Sentence =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski FormulaSen Dlformula
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | DefprocSen [Defproc]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder deriving (Show, Eq, Ord)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- * Pretty instances
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederppWithSemis :: Pretty a => [a] -> Doc
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskippWithSemis = fsep . punctuate semi . map pretty
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Pretty Profile where
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski pretty (Profile ps ores) = fsep
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski [ ppWithCommas ps
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , case ores of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Nothing -> empty
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just s -> funArrow <+> idDoc s]
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance Pretty Sigentry where
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu pretty (Procedure i p _) = fsep [idDoc i, pretty p]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Pretty Procdecls where
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski pretty (Procdecls l _) = fsep
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder [ text $ "PROCEDURE" ++ case l of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , semiAnnos pretty l ]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Pretty Procparam where
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski pretty (Procparam m s) = text (map toUpper $ show m) <+> idDoc s
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiblock :: Doc -> Doc
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederblock d = sep [text "BEGIN", d, text "END"]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiprettyProcKind :: ProcKind -> Doc
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederprettyProcKind k = text $ case k of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Proc -> "PROCEDURE"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Func -> "FUNCTION"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiassign = text ":="
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Pretty Defproc where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder pretty (Defproc pk p ps pr _) = vcat
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder [ prettyProcKind pk <+> idDoc p <> parens (ppWithCommas ps)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , pretty pr ]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Pretty a => Pretty (Ranged a) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder pretty (Ranged a _) = pretty a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Pretty VarDecl where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder pretty (VarDecl v s mt _) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sidDoc v <+> colon <+> idDoc s <+> case mt of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> empty
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just t -> assign <+> pretty t
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Pretty PlainProgram where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty prg = case prg of
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Abort -> text "ABORT"
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Skip -> text "SKIP"
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Assign v t -> pretty v <+> assign <+> pretty t
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Call p ts -> idDoc p <>
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu if null ts then empty else parens $ ppWithCommas ts
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Return t -> text "RETURN" <+> pretty t
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Block vs p -> if null vs then block $ pretty p else
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let (vds, q) = addInits (toVarDecl vs) p
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in sep [ text "DECLARE"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , ppWithCommas vds <> semi
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Seq p1 p2 -> vcat [pretty p1 <> semi, pretty p2]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder If f t e -> sep
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [ text "IF" <+> pretty f
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , text "THEN" <+> pretty t
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , text "ELSE" <+> pretty e
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , text "FI" ]
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder While f p -> sep
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [ text "WHILE" <+> pretty f
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , text "DO" <+> pretty p
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , text "OD" ]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Pretty Dlformula where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder pretty (Dlformula b p f _) = let d = pretty p in
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Box -> brackets d
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Diamond -> less <> d <> greater)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder <+> parens (pretty f)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Pretty Procdefs where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder pretty (Procdefs ps _) = prettyProcdefs ps
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederprettyProcdefs :: [Defproc] -> Doc
a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescuprettyProcdefs ps = vcat
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu [ text "DEFPROCS"
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu , ppWithSemis ps
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu , text "DEFPROCSEND" ]
c18a07fe36512679e66faa59274bb273e735738aMihai Codescuinstance Pretty Sentence where
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu pretty sen = case sen of
da955132262baab309a50fdffe228c9efe68251dCui Jian FormulaSen f -> pretty f
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu DefprocSen ps -> prettyProcdefs ps