content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./Syntax/AS_Structured.der.hs
  Description :  abstract syntax of DOL OMS and CASL structured specifications
  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 (heterogeneous) structured specifications
     Follows Sect. II:2.2.3 of the CASL Reference Manual.
  Abstract syntax of DOL OMS and networks
     Follows the DOL OMG standard, clauses 9.4, 9.5, M.2 and M.3
  -}
  
  module Syntax.AS_Structured where
  
  -- DrIFT command:
  {-! global: GetRange !-}
  
  import Common.Id
  import Common.IRI
  import Common.AS_Annotation
  
  import Data.Typeable
  import qualified Data.Set as Set
  
  import Logic.Logic
  import Logic.Grothendieck
      ( G_basic_spec
      , G_symb_items_list
      , G_symb_map_items_list
      , LogicGraph
      , setCurLogic
      , setSyntax )
  
  -- for spec-defn and view-defn see AS_Library
  
  data SPEC = Basic_spec G_basic_spec Range
            | EmptySpec Range
            | Extraction (Annoted SPEC) EXTRACTION
            | Translation (Annoted SPEC) RENAMING
            | Reduction (Annoted SPEC) RESTRICTION
            | Approximation (Annoted SPEC) APPROXIMATION
            | Minimization (Annoted SPEC) MINIMIZATION
            | Filtering (Annoted SPEC) FILTERING
            | Bridge (Annoted SPEC) [RENAMING] (Annoted SPEC) Range
            | Union [Annoted SPEC] Range
              -- pos: "and"s
            | Intersection [Annoted SPEC] Range
              -- pos: "intersect"s
            | Extension [Annoted SPEC] Range
              -- pos: "then"s
            | Free_spec (Annoted SPEC) Range
              -- pos: "free"
            | Cofree_spec (Annoted SPEC) Range
              -- pos: "cofree"
            | Minimize_spec (Annoted SPEC) Range
              -- pos: "minimize", "closed-world"
            | Local_spec (Annoted SPEC) (Annoted SPEC) Range
              -- pos: "local", "within"
            | Closed_spec (Annoted SPEC) Range
              -- pos: "closed"
            | Group (Annoted SPEC) Range
              -- pos: "{","}"
            | Spec_inst SPEC_NAME [Annoted FIT_ARG] (Maybe IRI) Range
              {- pos: many of "[","]"; one balanced pair per FIT_ARG
              an optional ImpName for DOL -}
            | Qualified_spec LogicDescr (Annoted SPEC) Range
              -- pos: "logic", Logic_name,":"
            | Data AnyLogic AnyLogic (Annoted SPEC) (Annoted SPEC) Range
              -- pos: "data"
            | Combination Network Range
              -- pos: "combine"
            | Apply IRI G_basic_spec Range
              -- pos: "apply", use a basic spec parser to parse a sentence
              deriving (Show, Typeable)
  
  data Network = Network [LABELED_ONTO_OR_INTPR_REF] [IRI] Range
    deriving (Show, Eq, Typeable)
  
  data FILTERING = FilterBasicSpec Bool G_basic_spec Range
                 | FilterSymbolList Bool  G_symb_items_list Range
    deriving (Show, Eq, Typeable)
  
  data EXTRACTION = ExtractOrRemove Bool [IRI] Range
    deriving (Show, Eq, Typeable)
  
  data APPROXIMATION = ForgetOrKeep Bool [G_hiding] (Maybe IRI) Range
    deriving (Show, Eq, Typeable)
  
  data MINIMIZATION = Mini Token [IRI] [IRI] Range
    deriving (Show, Eq, Typeable)
  
  
  data RENAMING = Renaming [G_mapping] Range
                  -- pos: "with", list of comma pos
                   deriving (Show, Eq, Typeable)
  
  data RESTRICTION = Hidden [G_hiding] Range
                     -- pos: "hide", list of comma pos
                   | Revealed G_symb_map_items_list Range
                     -- pos: "reveal", list of comma pos
                     deriving (Show, Eq, Typeable)
  
  {- Renaming and Hiding can be performend with intermediate Logic
     mappings / Logic projections.
  -}
  
  data G_mapping = G_symb_map G_symb_map_items_list
                 | G_logic_translation Logic_code
                   deriving (Show, Eq, Typeable)
  
  data G_hiding = G_symb_list G_symb_items_list
                 | G_logic_projection Logic_code
                   deriving (Show, Eq, Typeable)
  
  data FIT_ARG = Fit_spec (Annoted SPEC) [G_mapping] Range
                 -- pos: opt "fit"
               | Fit_view IRI [Annoted FIT_ARG] Range
                 -- annotations before the view keyword are stored in Spec_inst
                 deriving (Show, Typeable)
  
  type SPEC_NAME = IRI
  
  -- | a logic with serialization or a DOL qualification
  data LogicDescr = LogicDescr Logic_name (Maybe IRI) Range
    -- pos: "serialization"
    | SyntaxQual IRI
    | LanguageQual IRI
    deriving (Show, Typeable)
  
  data Logic_code = Logic_code (Maybe String)
                               (Maybe Logic_name)
                               (Maybe Logic_name) Range
                   {- pos: "logic",<encoding>,":",<src-logic>,"->",<targ-logic>
                   one of <encoding>, <src-logic> or <targ-logic>
                   must be given (by Just)
                   "logic bla"    => <encoding> only
                   "logic bla ->" => <src-logic> only
                   "logic -> bla" => <targ-logic> only
                   "logic bla1 -> bla2" => <src-logic> and <targ-logic>
                   -- "logic bla1:bla2"    => <encoding> and <src-logic>
                   this notation is not very useful and is not maintained
                   "logic bla1:bla2 ->" => <encoding> and <src-logic> (!)
                   "logic bla1: ->bla2" => <encoding> and <targ-logic> -}
                    deriving (Show, Eq, Typeable)
  
  data Logic_name = Logic_name
    String -- looked-up logic name
    (Maybe Token) -- sublogic part
    (Maybe SPEC_NAME) -- for a sublogic based on the given theory
    deriving (Show, Eq, Typeable)
  
  data LABELED_ONTO_OR_INTPR_REF = Labeled (Maybe Token) IRI
    deriving (Show, Eq, Typeable)
  
  nameToLogicDescr :: Logic_name -> LogicDescr
  nameToLogicDescr n = LogicDescr n Nothing nullRange
  
  setLogicName :: LogicDescr -> LogicGraph -> LogicGraph
  setLogicName ld = case ld of
    LogicDescr (Logic_name lid _ _) s _ -> setSyntax s . setCurLogic lid
    _ -> id
  
  makeSpec :: G_basic_spec -> Annoted SPEC
  makeSpec gbs = emptyAnno $ Basic_spec gbs nullRange
  
  makeSpecInst :: SPEC_NAME -> Annoted SPEC
  makeSpecInst n = emptyAnno $ Spec_inst n [] Nothing nullRange
  
  addImports :: [SPEC_NAME] -> Annoted SPEC -> Annoted SPEC
  addImports is bs = case map makeSpecInst is of
    [] -> bs
    js@(i : rs) -> emptyAnno $ Extension
      [ if null rs then i else
            emptyAnno $ Union js nullRange, bs] nullRange
  
  data CORRESPONDENCE = Correspondence_block
                          (Maybe RELATION_REF)
                          (Maybe CONFIDENCE)
                          [CORRESPONDENCE]
                      | Single_correspondence
                          (Maybe Annotation)
                          G_symb_items_list -- was ENTITY_REF
                          G_symb_items_list -- was TERM_OR_ENTITY_REF
                          (Maybe RELATION_REF)
                          (Maybe CONFIDENCE)
                      | Default_correspondence
                        deriving (Show, Eq, Typeable)
  
  data RELATION_REF = Subsumes | IsSubsumed | Equivalent | Incompatible
                    | HasInstance | InstanceOf | DefaultRelation
                    | Iri IRI
                      deriving (Show, Eq, Typeable)
  
  refToRel :: RELATION_REF -> REL_REF
  refToRel Subsumes = Subs
  refToRel IsSubsumed = IsSubs
  refToRel Equivalent = Equiv
  refToRel Incompatible = Incomp
  refToRel HasInstance = HasInst
  refToRel InstanceOf = InstOf
  refToRel DefaultRelation = DefRel
  refToRel (Iri i) = RelName i
  
  type CONFIDENCE = Double -- NOTE: will be revised
  
  instance GetRange Double where
    getRange = const nullRange
  
  getSpecNames :: SPEC -> Set.Set SPEC_NAME
  getSpecNames sp = let f = getSpecNames . item in case sp of
    Translation as _ -> f as
    Reduction as _ -> f as
    Approximation as _ -> f as
    Minimization as _ -> f as
    Filtering as _ -> f as
    Union as _ -> Set.unions $ map f as
    Intersection as _ -> Set.unions $ map f as
    Extraction as _ -> f as
    Extension as _ -> Set.unions $ map f as
    Free_spec as _ -> f as
    Cofree_spec as _ -> f as
    Minimize_spec as _ -> f as
    Local_spec s1 s2 _ -> Set.union (f s1) $ f s2
    Closed_spec as _ -> f as
    Group as _ -> f as
    Spec_inst sn fas _ _ -> Set.insert sn
      . Set.unions . map f $ concatMap (getSpecs . item) fas
    Qualified_spec _ as _ -> f as
    Data _ _ s1 s2 _ -> Set.union (f s1) $ f s2
    _ -> Set.empty
  
  getSpecs :: FIT_ARG -> [Annoted SPEC]
  getSpecs fa = case fa of
    Fit_spec as _ _ -> [as]
    Fit_view _ fas _ -> concatMap (getSpecs . item) fas
  