{-# 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
