AS_CommonLogic.hs revision fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederModule : $Header$
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederDescription : Abstract syntax for common logic
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederCopyright : (c) Karl Luc, DFKI Bremen 2010
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederMaintainer : kluc@informatik.uni-bremen.de
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederStability : provisional
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederPortability : portable
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederDefinition of abstract syntax for common logic
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ISO/IEC IS 24707:2007(E)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederdata TEXT = Text [PHRASE] Id.Range
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder deriving (Show, Ord, Eq)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederdata PHRASE = Module MODULE Id.Range
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder | Sentence SENTENCE Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Importation IMPORTATION Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Comment_Text TEXT COMMENT Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata COMMENT = Comment String Id.Range
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata MODULE = Mod NAME [NAME] TEXT Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata IMPORTATION = Imp_name NAME Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata SENTENCE = Quant_sent QUANT_SENT Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Bool_sent BOOL_SENT Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Atom_sent ATOM Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Comment_sent SENTENCE COMMENT Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Irregular_sent SENTENCE Id.Range -- opt
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata QUANT_SENT = Universal [BINDING_SEQ] SENTENCE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Existential [BINDING_SEQ] SENTENCE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata BINDING_SEQ = B_name NAME Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | B_seqmark SEQ_MARK Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata BOOL_SENT = Conjunction [SENTENCE]
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Disjunction [SENTENCE]
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Negation SENTENCE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Implication SENTENCE SENTENCE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Biconditional SENTENCE SENTENCE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata ATOM = Equation TERM TERM
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Atom TERM TERM_SEQ
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata TERM = Name NAME Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Funct_term TERM TERM_SEQ Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Comment_term TERM COMMENT Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata TERM_SEQ = Term_seq [TERM] Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder | Seq_marks [SEQ_MARK] Id.Range
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder deriving (Show, Ord, Eq)
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maedertype SEQ_MARK = Id.Token
f799084b320209cdd71a29e74fff1be054c1d342Christian Maedernewtype NAME = Name Id.Token
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder deriving (Show, Eq)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maedernewtype SEQ_MARK = SeqMark Id.Token
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder deriving (Show, Eq)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- pretty printing using CLIF
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederinstance Pretty SENTENCE where
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder pretty = printSentence
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederinstance Pretty BOOL_SENT where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printBoolSent
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance Pretty QUANT_SENT where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printQuantSent
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederinstance Pretty ATOM where
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder pretty = printAtom
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederinstance Pretty TERM where
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder pretty = printTerm
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederinstance Pretty TERM_SEQ where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printTermSeq
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance Pretty BINDING_SEQ where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printBindingSeq
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederinstance Pretty COMMENT where
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder pretty = printComment
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintSentence :: SENTENCE -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintSentence s = case s of
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder Quant_sent xs _ -> parens $ pretty xs
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder Bool_sent xs _ -> parens $ pretty xs
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder Atom_sent xs _ -> pretty xs
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Comment_sent x y _ -> parens $ pretty y <+> pretty x
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Irregular_sent xs _ -> parens $ pretty xs
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintComment :: COMMENT -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintComment s = case s of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Comment x _ -> text x
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaederprintQuantSent :: QUANT_SENT -> Doc
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaederprintQuantSent s = case s of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Universal x y -> text forallS <+> parens (sep $ map pretty x)<+> pretty y
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Existential x y -> text existsS <+> parens (sep $ map pretty x) <+> pretty y
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaederprintBindingSeq :: BINDING_SEQ -> Doc
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaederprintBindingSeq s = case s of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder B_name xs _ -> pretty xs
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder B_seqmark xs _ -> text seqmark <> pretty xs
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaederprintBoolSent :: BOOL_SENT -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintBoolSent s = case s of
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder Conjunction xs -> text andS <+> (fsep $ map pretty xs)
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder Disjunction xs -> text orS <+> (fsep $ map pretty xs)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Negation xs -> text notS <+> pretty xs
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Implication x y -> text ifS <+> pretty x <+> pretty y
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Biconditional x y -> text iffS <+> pretty x <+> pretty y
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian MaederprintAtom :: ATOM -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintAtom s = case s of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Equation a b -> parens $ equals <+> pretty a <+> pretty b
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Atom t ts -> parens $ pretty t <+> pretty ts
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintTerm :: TERM -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintTerm s = case s of
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian Maeder Name a _ -> pretty a
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Funct_term t ts _ -> parens $ pretty t <+> pretty ts
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Comment_term x y _ -> pretty x <+> pretty y
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintTermSeq :: TERM_SEQ -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintTermSeq s = case s of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Term_seq t _ -> fsep $ map pretty t
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Seq_marks m _ -> fsep $ map pretty m
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- keywords, reservednames in CLIF
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederseqmark :: String
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederseqmark = "..."
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder(...) :: String
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederiffS :: String