{-# LANGUAGE DeriveDataTypeable #-}

{- |

Module : ./Syntax/AS_Library.der.hs

Description : abstract syntax of DOL documents and CASL specification libraries

Copyright : (c) Klaus Luettich, Uni Bremen 2002-2016

License : GPLv2 or higher, see LICENSE.txt

Maintainer : till@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable(Grothendieck)

Abstract syntax of HetCASL specification libraries

Follows Sect. II:2.2.5 of the CASL Reference Manual.

Abstract syntax of DOL documents

Follows the DOL OMG standard, clauses 9.3 and M.1

-}

module Syntax.AS_Library where

-- DrIFT command:

{-! global: GetRange !-}

import Common.Id

import Common.IRI

import Common.AS_Annotation

import Common.LibName

import Data.Maybe

import Data.Typeable

import Logic.Grothendieck

import Logic.Logic

import Syntax.AS_Architecture

import Syntax.AS_Structured

import Framework.AS

import Framework.ATC_Framework ()

data LIB_DEFN = Lib_defn LibName [Annoted LIB_ITEM] Range [Annotation]

{- pos: "library"

list of annotations is parsed preceding the first LIB_ITEM

the last LIB_ITEM may be annotated with a following comment

the first LIB_ITEM cannot be annotated -}

deriving (Show, Typeable)

{- for information on the list of Pos see the documentation in

AS_Structured.hs and AS_Architecture.hs -}

data LIB_ITEM = Spec_defn SPEC_NAME GENERICITY (Annoted SPEC) Range

-- pos: "spec", "=", opt "end"

| View_defn IRI GENERICITY VIEW_TYPE [G_mapping] Range

-- pos: "view", ":", opt "=", opt "end"

| Entail_defn IRI ENTAIL_TYPE Range

-- pos: "entailment", "=", opt "end"

| Equiv_defn IRI EQUIV_TYPE OmsOrNetwork Range

-- pos: "equivalence", ":", "=", opt "end"

| Align_defn IRI (Maybe ALIGN_ARITIES) VIEW_TYPE

[CORRESPONDENCE] AlignSem Range

| Module_defn IRI MODULE_TYPE G_symb_items_list Range

{- G_symb_items_list is RESTRICTION-SIGNATURE

TODO: CONSERVATIVE? -}

| Query_defn IRI G_symb_items_list G_basic_spec (Annoted SPEC)

(Maybe IRI) Range

-- pos: "query", "=", "select", "where", "in", "along"

| Subst_defn IRI VIEW_TYPE G_symb_map_items_list Range

-- pos: "substitution", ":", "=", opt "end"

| Result_defn IRI [IRI] IRI Bool Range

-- pos: "result", commas, "for", "%complete", opt "end"

| Arch_spec_defn ARCH_SPEC_NAME (Annoted ARCH_SPEC) Range

-- pos: "arch", "spec", "=", opt "end"

| Unit_spec_defn SPEC_NAME UNIT_SPEC Range

-- pos: "unit", "spec", "=", opt "end"

| Ref_spec_defn SPEC_NAME REF_SPEC Range

-- pos: "refinement", "=", opt "end"

| Network_defn IRI Network Range

-- pos: "network", "=", opt "end"

| Download_items LibName DownloadItems Range

-- pos: "from", "get", "|->", commas, opt "end"

| Logic_decl LogicDescr Range

-- pos: "logic", Logic_name

| Newlogic_defn LogicDef Range

-- pos: "newlogic", Logic_name, "=", opt "end"

| Newcomorphism_defn ComorphismDef Range

-- pos: "newcomorphism", Comorphism_name, "=", opt "end"

deriving (Show, Typeable)

data AlignSem = SingleDomain | GlobalDomain | ContextualizedDomain

deriving (Show, Typeable, Bounded, Enum)

{- Item maps are the documented CASL renamed entities whereas a unique item

contains the new target name of the single arbitrarily named item from the

downloaded library. -}

data DownloadItems =

ItemMaps [ItemNameMap]

| UniqueItem IRI

deriving (Show, Typeable)

addDownload :: Bool -> SPEC_NAME -> Annoted LIB_ITEM

addDownload unique = emptyAnno . addDownloadAux unique

addDownloadAux :: Bool -> SPEC_NAME -> LIB_ITEM

addDownloadAux unique j =

let libPath = deleteQuery j

query = iriQuery j -- this used to be the fragment

i = case query of

"" -> j

"?" -> libPath

_ : r -> fromMaybe libPath $ parseIRICurie r

in Download_items (iriLibName i)

(if unique then UniqueItem i else ItemMaps [ItemNameMap i Nothing])

$ iriPos i

data GENERICITY = Genericity PARAMS IMPORTED Range deriving (Show, Typeable)

-- pos: many of "[","]" opt ("given", commas)

emptyGenericity :: GENERICITY

emptyGenericity = Genericity (Params []) (Imported []) nullRange

data PARAMS = Params [Annoted SPEC] deriving (Show, Typeable)

data IMPORTED = Imported [Annoted SPEC] deriving (Show, Typeable)

data VIEW_TYPE = View_type (Annoted SPEC) (Annoted SPEC) Range

deriving (Show, Typeable)

-- pos: "to"

data EQUIV_TYPE = Equiv_type OmsOrNetwork OmsOrNetwork Range

deriving (Show, Typeable)

-- pos: "<->"

data MODULE_TYPE = Module_type (Annoted SPEC) (Annoted SPEC) Range

deriving (Show, Typeable)

data ALIGN_ARITIES = Align_arities ALIGN_ARITY ALIGN_ARITY

deriving (Show, Typeable)

data ALIGN_ARITY = AA_InjectiveAndTotal | AA_Injective | AA_Total

| AA_NeitherInjectiveNorTotal

deriving (Show, Enum, Bounded, Typeable)

data OmsOrNetwork = MkOms (Annoted SPEC)

| MkNetwork Network

deriving (Show, Typeable)

data ENTAIL_TYPE = Entail_type OmsOrNetwork OmsOrNetwork Range

| OMSInNetwork IRI Network SPEC Range

deriving (Show, Typeable)

-- pos "entails"

showAlignArity :: ALIGN_ARITY -> String

showAlignArity ar = case ar of

AA_InjectiveAndTotal -> "1"

AA_Injective -> "?"

AA_Total -> "+"

AA_NeitherInjectiveNorTotal -> "*"

data ItemNameMap =

ItemNameMap IRI (Maybe IRI)

deriving (Show, Eq, Typeable)

makeLogicItem :: Language lid => lid -> Annoted LIB_ITEM

makeLogicItem lid = emptyAnno $ Logic_decl

(nameToLogicDescr $ Logic_name

(language_name lid) Nothing Nothing) nullRange

makeSpecItem :: SPEC_NAME -> Annoted SPEC -> Annoted LIB_ITEM

makeSpecItem sn as =

emptyAnno $ Spec_defn sn emptyGenericity as nullRange

fromBasicSpec :: LibName -> SPEC_NAME -> G_basic_spec -> LIB_DEFN

fromBasicSpec ln sn gbs =

Lib_defn ln [makeSpecItem sn $ makeSpec gbs] nullRange []

getDeclSpecNames :: LIB_ITEM -> [IRI]

getDeclSpecNames li = case li of

Spec_defn sn _ _ _ -> [sn]

Download_items _ di _ -> getImportNames di

_ -> []

getImportNames :: DownloadItems -> [IRI]

getImportNames di = case di of

ItemMaps im -> map (\ (ItemNameMap i mi) -> fromMaybe i mi) im

UniqueItem i -> [i]

getOms :: OmsOrNetwork -> [SPEC]

getOms o = case o of

MkOms s -> [item s]

MkNetwork _ -> []

getSpecDef :: LIB_ITEM -> [SPEC]

getSpecDef li = case li of

Spec_defn _ _ as _ -> [item as]

View_defn _ _ (View_type s1 s2 _) _ _ -> [item s1, item s2]

Entail_defn _ (Entail_type s1 s2 _) _ -> getOms s1 ++ getOms s2

Equiv_defn _ (Equiv_type s1 s2 _) as _ ->

getOms s1 ++ getOms s2 ++ getOms as

Align_defn _ _ (View_type s1 s2 _) _ _ _ -> [item s1, item s2]

Module_defn _ (Module_type s1 s2 _) _ _ -> [item s1, item s2]

_ -> []