hets/Syntax/Print_AS_Library.hs

	Print_AS_Library.hs revision 704c2a3f6a085d60339b9213731e09d0f57e3c5f
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder{-|
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederModule      :  $Header$
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederCopyright   :  (c) Klaus L�ttich, Uni Bremen 2002-2004
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederMaintainer  :  hets@tzi.de
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederStability   :  provisional
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability :  non-portable(Grothendieck)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder   pretty printing for heterogenous libraries in HetCASL.
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedermodule Syntax.Print_AS_Library where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.Lib.Pretty
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.PrettyPrint
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.GlobalAnnotations
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.Keywords
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport qualified Syntax.AS_Structured as AS_Struct
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Syntax.AS_Library
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.AS_Annotation
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Syntax.Print_AS_Architecture
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Syntax.Print_AS_Structured
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedernl :: Doc
b53688bfed888214b485cf76439d57262d80e0a7Christian Maedernl = char '\n' -- isn't this uncool?
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance PrettyPrint LIB_DEFN where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Lib_defn aa ab _ ad) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa              -- lib name
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = vcat $ map (printText0 ga) ab -- LIB_ITEMs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ad' = vcat $ map (printText0 ga) ad -- global ANNOTATIONs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in text libraryS <+> aa' <> nl $$ ad' $$ nl $$ ab'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance PrettyPrint LIB_ITEM where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Spec_defn aa ab ac _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = printText0 ga ab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        spec_head = text specS <+> aa' <+> ab' <+> equals
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ac' = spAnnotedPrint (printText0 ga) (printText0 ga) (<+>)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder          (spec_head) ac
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder         -- nesting is done by the instance for SPEC now
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in ac' $$ text endS <> nl
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (View_defn aa ab ac ad _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = printText0 ga ab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        -- ac' = printText0 ga ac
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        (frm,to) = case ac of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder               AS_Struct.View_type vaa vab _ ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder               (condBracesGroupSpec printText0 braces
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder                    Nothing ga vaa,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder                condBracesGroupSpec printText0 braces
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder                    Nothing ga vab)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ad' = sep $ punctuate comma $ map (printText0 ga) ad
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        eq' = if null ad then empty else equals
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in (hang (hang (hang (hang (text viewS <+> aa' <+> ab')
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder                       6
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder                       (colon <+> frm <+> text toS))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder                 4
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder                             to)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder               2
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder               eq')
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder             4
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder             ad')
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder       $$ text endS <> nl
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder{-
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata VIEW_DEFN = View_defn VIEW_NAME GENERICITY VIEW_TYPE
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder               [G_mapping] [Pos]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Arch_spec_defn aa ab _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = printText0 ga ab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in (hang (text archS <+> text specS <+> aa' <+> equals) 4 ab')
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder               $$ text endS <> nl
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Unit_spec_defn aa ab _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = printText0 ga ab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in (hang (text unitS <+> text specS <+> aa' <+> equals) 4 ab')
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder               $$ text endS <> nl
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Ref_spec_defn aa ab _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = printText0 ga ab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in (hang (text refinementS <+> aa' <+> equals) 4 ab')
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder               $$ text endS <> nl
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Download_items aa ab _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = fsep $ punctuate comma $ map (printText0 ga) ab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in (hang (text fromS <+> aa' <+> text getS) 4 ab') <> nl
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Syntax.AS_Library.Logic_decl aa _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in text logicS <+> aa'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercondBracesGroupSpec4View_defn ::
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    (GlobalAnnos -> (Annoted AS_Struct.SPEC) -> Doc)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    -> (Doc -> Doc) -- ^ a function enclosing the Doc
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder                        -- in braces
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    -> GlobalAnnos -> (Annoted AS_Struct.SPEC) -> Doc
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercondBracesGroupSpec4View_defn pf b_fun ga as =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    case skip_Group $ item as of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder         AS_Struct.Spec_inst _ _ _ -> as'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder         AS_Struct.Union _ _       -> nested'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder         AS_Struct.Extension _ _   -> nested'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder         _                         -> nested'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    where nested' = b_fun as'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder          as' = pf ga as
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance PrettyPrint ITEM_NAME_OR_MAP where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Item_name aa) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in aa'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Item_name_map aa ab _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = printText0 ga ab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in aa' <+> text mapsTo <+> ab'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance PrettyPrint LIB_NAME where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Lib_version aa ab) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    let aa' = printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder        ab' = printText0 ga ab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    in aa' <+> text versionS <+> ab'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga (Lib_id aa) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 ga aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance PrettyPrint LIB_ID where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 _ (Direct_link aa _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    text aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 _ (Indirect_link aa _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    text aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance PrettyPrint VERSION_NUMBER where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    printText0 _ (Version_number aa _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder    hcat $ punctuate (char '.') $ map text aa
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder