{-# 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 (Int -> LIB_DEFN -> ShowS
[LIB_DEFN] -> ShowS
LIB_DEFN -> String
(Int -> LIB_DEFN -> ShowS)
-> (LIB_DEFN -> String) -> ([LIB_DEFN] -> ShowS) -> Show LIB_DEFN
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LIB_DEFN] -> ShowS
$cshowList :: [LIB_DEFN] -> ShowS
show :: LIB_DEFN -> String
$cshow :: LIB_DEFN -> String
showsPrec :: Int -> LIB_DEFN -> ShowS
$cshowsPrec :: Int -> LIB_DEFN -> ShowS
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 (Int -> LIB_ITEM -> ShowS
[LIB_ITEM] -> ShowS
LIB_ITEM -> String
(Int -> LIB_ITEM -> ShowS)
-> (LIB_ITEM -> String) -> ([LIB_ITEM] -> ShowS) -> Show LIB_ITEM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LIB_ITEM] -> ShowS
$cshowList :: [LIB_ITEM] -> ShowS
show :: LIB_ITEM -> String
$cshow :: LIB_ITEM -> String
showsPrec :: Int -> LIB_ITEM -> ShowS
$cshowsPrec :: Int -> LIB_ITEM -> ShowS
Show, Typeable)

data AlignSem = SingleDomain | GlobalDomain | ContextualizedDomain
  deriving (Int -> AlignSem -> ShowS
[AlignSem] -> ShowS
AlignSem -> String
(Int -> AlignSem -> ShowS)
-> (AlignSem -> String) -> ([AlignSem] -> ShowS) -> Show AlignSem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AlignSem] -> ShowS
$cshowList :: [AlignSem] -> ShowS
show :: AlignSem -> String
$cshow :: AlignSem -> String
showsPrec :: Int -> AlignSem -> ShowS
$cshowsPrec :: Int -> AlignSem -> ShowS
Show, Typeable, AlignSem
AlignSem -> AlignSem -> Bounded AlignSem
forall a. a -> a -> Bounded a
maxBound :: AlignSem
$cmaxBound :: AlignSem
minBound :: AlignSem
$cminBound :: AlignSem
Bounded, Int -> AlignSem
AlignSem -> Int
AlignSem -> [AlignSem]
AlignSem -> AlignSem
AlignSem -> AlignSem -> [AlignSem]
AlignSem -> AlignSem -> AlignSem -> [AlignSem]
(AlignSem -> AlignSem)
-> (AlignSem -> AlignSem)
-> (Int -> AlignSem)
-> (AlignSem -> Int)
-> (AlignSem -> [AlignSem])
-> (AlignSem -> AlignSem -> [AlignSem])
-> (AlignSem -> AlignSem -> [AlignSem])
-> (AlignSem -> AlignSem -> AlignSem -> [AlignSem])
-> Enum AlignSem
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: AlignSem -> AlignSem -> AlignSem -> [AlignSem]
$cenumFromThenTo :: AlignSem -> AlignSem -> AlignSem -> [AlignSem]
enumFromTo :: AlignSem -> AlignSem -> [AlignSem]
$cenumFromTo :: AlignSem -> AlignSem -> [AlignSem]
enumFromThen :: AlignSem -> AlignSem -> [AlignSem]
$cenumFromThen :: AlignSem -> AlignSem -> [AlignSem]
enumFrom :: AlignSem -> [AlignSem]
$cenumFrom :: AlignSem -> [AlignSem]
fromEnum :: AlignSem -> Int
$cfromEnum :: AlignSem -> Int
toEnum :: Int -> AlignSem
$ctoEnum :: Int -> AlignSem
pred :: AlignSem -> AlignSem
$cpred :: AlignSem -> AlignSem
succ :: AlignSem -> AlignSem
$csucc :: AlignSem -> AlignSem
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 (Int -> DownloadItems -> ShowS
[DownloadItems] -> ShowS
DownloadItems -> String
(Int -> DownloadItems -> ShowS)
-> (DownloadItems -> String)
-> ([DownloadItems] -> ShowS)
-> Show DownloadItems
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DownloadItems] -> ShowS
$cshowList :: [DownloadItems] -> ShowS
show :: DownloadItems -> String
$cshow :: DownloadItems -> String
showsPrec :: Int -> DownloadItems -> ShowS
$cshowsPrec :: Int -> DownloadItems -> ShowS
Show, Typeable)

addDownload :: Bool -> SPEC_NAME -> Annoted LIB_ITEM
addDownload :: Bool -> SPEC_NAME -> Annoted LIB_ITEM
addDownload unique :: Bool
unique = LIB_ITEM -> Annoted LIB_ITEM
forall a. a -> Annoted a
emptyAnno (LIB_ITEM -> Annoted LIB_ITEM)
-> (SPEC_NAME -> LIB_ITEM) -> SPEC_NAME -> Annoted LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SPEC_NAME -> LIB_ITEM
addDownloadAux Bool
unique

addDownloadAux :: Bool -> SPEC_NAME -> LIB_ITEM
addDownloadAux :: Bool -> SPEC_NAME -> LIB_ITEM
addDownloadAux unique :: Bool
unique j :: SPEC_NAME
j =
  let libPath :: SPEC_NAME
libPath = SPEC_NAME -> SPEC_NAME
deleteQuery SPEC_NAME
j
      query :: String
query = SPEC_NAME -> String
iriQuery SPEC_NAME
j -- this used to be the fragment
      i :: SPEC_NAME
i = case String
query of
        "" -> SPEC_NAME
j
        "?" -> SPEC_NAME
libPath
        _ : r :: String
r -> SPEC_NAME -> Maybe SPEC_NAME -> SPEC_NAME
forall a. a -> Maybe a -> a
fromMaybe SPEC_NAME
libPath (Maybe SPEC_NAME -> SPEC_NAME) -> Maybe SPEC_NAME -> SPEC_NAME
forall a b. (a -> b) -> a -> b
$ String -> Maybe SPEC_NAME
parseIRICurie String
r
  in LibName -> DownloadItems -> Range -> LIB_ITEM
Download_items (SPEC_NAME -> LibName
iriLibName SPEC_NAME
i)
    (if Bool
unique then SPEC_NAME -> DownloadItems
UniqueItem SPEC_NAME
i else [ItemNameMap] -> DownloadItems
ItemMaps [SPEC_NAME -> Maybe SPEC_NAME -> ItemNameMap
ItemNameMap SPEC_NAME
i Maybe SPEC_NAME
forall a. Maybe a
Nothing])
    (Range -> LIB_ITEM) -> Range -> LIB_ITEM
forall a b. (a -> b) -> a -> b
$ SPEC_NAME -> Range
iriPos SPEC_NAME
i

data GENERICITY = Genericity PARAMS IMPORTED Range deriving (Int -> GENERICITY -> ShowS
[GENERICITY] -> ShowS
GENERICITY -> String
(Int -> GENERICITY -> ShowS)
-> (GENERICITY -> String)
-> ([GENERICITY] -> ShowS)
-> Show GENERICITY
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GENERICITY] -> ShowS
$cshowList :: [GENERICITY] -> ShowS
show :: GENERICITY -> String
$cshow :: GENERICITY -> String
showsPrec :: Int -> GENERICITY -> ShowS
$cshowsPrec :: Int -> GENERICITY -> ShowS
Show, Typeable)
                  -- pos: many of "[","]" opt ("given", commas)

emptyGenericity :: GENERICITY
emptyGenericity :: GENERICITY
emptyGenericity = PARAMS -> IMPORTED -> Range -> GENERICITY
Genericity ([Annoted SPEC] -> PARAMS
Params []) ([Annoted SPEC] -> IMPORTED
Imported []) Range
nullRange

data PARAMS = Params [Annoted SPEC] deriving (Int -> PARAMS -> ShowS
[PARAMS] -> ShowS
PARAMS -> String
(Int -> PARAMS -> ShowS)
-> (PARAMS -> String) -> ([PARAMS] -> ShowS) -> Show PARAMS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PARAMS] -> ShowS
$cshowList :: [PARAMS] -> ShowS
show :: PARAMS -> String
$cshow :: PARAMS -> String
showsPrec :: Int -> PARAMS -> ShowS
$cshowsPrec :: Int -> PARAMS -> ShowS
Show, Typeable)

data IMPORTED = Imported [Annoted SPEC] deriving (Int -> IMPORTED -> ShowS
[IMPORTED] -> ShowS
IMPORTED -> String
(Int -> IMPORTED -> ShowS)
-> (IMPORTED -> String) -> ([IMPORTED] -> ShowS) -> Show IMPORTED
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IMPORTED] -> ShowS
$cshowList :: [IMPORTED] -> ShowS
show :: IMPORTED -> String
$cshow :: IMPORTED -> String
showsPrec :: Int -> IMPORTED -> ShowS
$cshowsPrec :: Int -> IMPORTED -> ShowS
Show, Typeable)

data VIEW_TYPE = View_type (Annoted SPEC) (Annoted SPEC) Range
  deriving (Int -> VIEW_TYPE -> ShowS
[VIEW_TYPE] -> ShowS
VIEW_TYPE -> String
(Int -> VIEW_TYPE -> ShowS)
-> (VIEW_TYPE -> String)
-> ([VIEW_TYPE] -> ShowS)
-> Show VIEW_TYPE
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VIEW_TYPE] -> ShowS
$cshowList :: [VIEW_TYPE] -> ShowS
show :: VIEW_TYPE -> String
$cshow :: VIEW_TYPE -> String
showsPrec :: Int -> VIEW_TYPE -> ShowS
$cshowsPrec :: Int -> VIEW_TYPE -> ShowS
Show, Typeable)
  -- pos: "to"

data EQUIV_TYPE = Equiv_type OmsOrNetwork OmsOrNetwork Range
  deriving (Int -> EQUIV_TYPE -> ShowS
[EQUIV_TYPE] -> ShowS
EQUIV_TYPE -> String
(Int -> EQUIV_TYPE -> ShowS)
-> (EQUIV_TYPE -> String)
-> ([EQUIV_TYPE] -> ShowS)
-> Show EQUIV_TYPE
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EQUIV_TYPE] -> ShowS
$cshowList :: [EQUIV_TYPE] -> ShowS
show :: EQUIV_TYPE -> String
$cshow :: EQUIV_TYPE -> String
showsPrec :: Int -> EQUIV_TYPE -> ShowS
$cshowsPrec :: Int -> EQUIV_TYPE -> ShowS
Show, Typeable)
  -- pos: "<->"

data MODULE_TYPE = Module_type (Annoted SPEC) (Annoted SPEC) Range
  deriving (Int -> MODULE_TYPE -> ShowS
[MODULE_TYPE] -> ShowS
MODULE_TYPE -> String
(Int -> MODULE_TYPE -> ShowS)
-> (MODULE_TYPE -> String)
-> ([MODULE_TYPE] -> ShowS)
-> Show MODULE_TYPE
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MODULE_TYPE] -> ShowS
$cshowList :: [MODULE_TYPE] -> ShowS
show :: MODULE_TYPE -> String
$cshow :: MODULE_TYPE -> String
showsPrec :: Int -> MODULE_TYPE -> ShowS
$cshowsPrec :: Int -> MODULE_TYPE -> ShowS
Show, Typeable)

data ALIGN_ARITIES = Align_arities ALIGN_ARITY ALIGN_ARITY
  deriving (Int -> ALIGN_ARITIES -> ShowS
[ALIGN_ARITIES] -> ShowS
ALIGN_ARITIES -> String
(Int -> ALIGN_ARITIES -> ShowS)
-> (ALIGN_ARITIES -> String)
-> ([ALIGN_ARITIES] -> ShowS)
-> Show ALIGN_ARITIES
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ALIGN_ARITIES] -> ShowS
$cshowList :: [ALIGN_ARITIES] -> ShowS
show :: ALIGN_ARITIES -> String
$cshow :: ALIGN_ARITIES -> String
showsPrec :: Int -> ALIGN_ARITIES -> ShowS
$cshowsPrec :: Int -> ALIGN_ARITIES -> ShowS
Show, Typeable)

data ALIGN_ARITY = AA_InjectiveAndTotal | AA_Injective | AA_Total
                 | AA_NeitherInjectiveNorTotal
                   deriving (Int -> ALIGN_ARITY -> ShowS
[ALIGN_ARITY] -> ShowS
ALIGN_ARITY -> String
(Int -> ALIGN_ARITY -> ShowS)
-> (ALIGN_ARITY -> String)
-> ([ALIGN_ARITY] -> ShowS)
-> Show ALIGN_ARITY
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ALIGN_ARITY] -> ShowS
$cshowList :: [ALIGN_ARITY] -> ShowS
show :: ALIGN_ARITY -> String
$cshow :: ALIGN_ARITY -> String
showsPrec :: Int -> ALIGN_ARITY -> ShowS
$cshowsPrec :: Int -> ALIGN_ARITY -> ShowS
Show, Int -> ALIGN_ARITY
ALIGN_ARITY -> Int
ALIGN_ARITY -> [ALIGN_ARITY]
ALIGN_ARITY -> ALIGN_ARITY
ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY]
ALIGN_ARITY -> ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY]
(ALIGN_ARITY -> ALIGN_ARITY)
-> (ALIGN_ARITY -> ALIGN_ARITY)
-> (Int -> ALIGN_ARITY)
-> (ALIGN_ARITY -> Int)
-> (ALIGN_ARITY -> [ALIGN_ARITY])
-> (ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY])
-> (ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY])
-> (ALIGN_ARITY -> ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY])
-> Enum ALIGN_ARITY
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: ALIGN_ARITY -> ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY]
$cenumFromThenTo :: ALIGN_ARITY -> ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY]
enumFromTo :: ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY]
$cenumFromTo :: ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY]
enumFromThen :: ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY]
$cenumFromThen :: ALIGN_ARITY -> ALIGN_ARITY -> [ALIGN_ARITY]
enumFrom :: ALIGN_ARITY -> [ALIGN_ARITY]
$cenumFrom :: ALIGN_ARITY -> [ALIGN_ARITY]
fromEnum :: ALIGN_ARITY -> Int
$cfromEnum :: ALIGN_ARITY -> Int
toEnum :: Int -> ALIGN_ARITY
$ctoEnum :: Int -> ALIGN_ARITY
pred :: ALIGN_ARITY -> ALIGN_ARITY
$cpred :: ALIGN_ARITY -> ALIGN_ARITY
succ :: ALIGN_ARITY -> ALIGN_ARITY
$csucc :: ALIGN_ARITY -> ALIGN_ARITY
Enum, ALIGN_ARITY
ALIGN_ARITY -> ALIGN_ARITY -> Bounded ALIGN_ARITY
forall a. a -> a -> Bounded a
maxBound :: ALIGN_ARITY
$cmaxBound :: ALIGN_ARITY
minBound :: ALIGN_ARITY
$cminBound :: ALIGN_ARITY
Bounded, Typeable)

data OmsOrNetwork = MkOms (Annoted SPEC)
  | MkNetwork Network
  deriving (Int -> OmsOrNetwork -> ShowS
[OmsOrNetwork] -> ShowS
OmsOrNetwork -> String
(Int -> OmsOrNetwork -> ShowS)
-> (OmsOrNetwork -> String)
-> ([OmsOrNetwork] -> ShowS)
-> Show OmsOrNetwork
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OmsOrNetwork] -> ShowS
$cshowList :: [OmsOrNetwork] -> ShowS
show :: OmsOrNetwork -> String
$cshow :: OmsOrNetwork -> String
showsPrec :: Int -> OmsOrNetwork -> ShowS
$cshowsPrec :: Int -> OmsOrNetwork -> ShowS
Show, Typeable)

data ENTAIL_TYPE = Entail_type OmsOrNetwork OmsOrNetwork Range
  | OMSInNetwork IRI Network SPEC Range
  deriving (Int -> ENTAIL_TYPE -> ShowS
[ENTAIL_TYPE] -> ShowS
ENTAIL_TYPE -> String
(Int -> ENTAIL_TYPE -> ShowS)
-> (ENTAIL_TYPE -> String)
-> ([ENTAIL_TYPE] -> ShowS)
-> Show ENTAIL_TYPE
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ENTAIL_TYPE] -> ShowS
$cshowList :: [ENTAIL_TYPE] -> ShowS
show :: ENTAIL_TYPE -> String
$cshow :: ENTAIL_TYPE -> String
showsPrec :: Int -> ENTAIL_TYPE -> ShowS
$cshowsPrec :: Int -> ENTAIL_TYPE -> ShowS
Show, Typeable)
  -- pos "entails"

showAlignArity :: ALIGN_ARITY -> String
showAlignArity :: ALIGN_ARITY -> String
showAlignArity ar :: ALIGN_ARITY
ar = case ALIGN_ARITY
ar of
  AA_InjectiveAndTotal -> "1"
  AA_Injective -> "?"
  AA_Total -> "+"
  AA_NeitherInjectiveNorTotal -> "*"

data ItemNameMap =
    ItemNameMap IRI (Maybe IRI)
    deriving (Int -> ItemNameMap -> ShowS
[ItemNameMap] -> ShowS
ItemNameMap -> String
(Int -> ItemNameMap -> ShowS)
-> (ItemNameMap -> String)
-> ([ItemNameMap] -> ShowS)
-> Show ItemNameMap
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ItemNameMap] -> ShowS
$cshowList :: [ItemNameMap] -> ShowS
show :: ItemNameMap -> String
$cshow :: ItemNameMap -> String
showsPrec :: Int -> ItemNameMap -> ShowS
$cshowsPrec :: Int -> ItemNameMap -> ShowS
Show, ItemNameMap -> ItemNameMap -> Bool
(ItemNameMap -> ItemNameMap -> Bool)
-> (ItemNameMap -> ItemNameMap -> Bool) -> Eq ItemNameMap
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ItemNameMap -> ItemNameMap -> Bool
$c/= :: ItemNameMap -> ItemNameMap -> Bool
== :: ItemNameMap -> ItemNameMap -> Bool
$c== :: ItemNameMap -> ItemNameMap -> Bool
Eq, Typeable)

makeLogicItem :: Language lid => lid -> Annoted LIB_ITEM
makeLogicItem :: lid -> Annoted LIB_ITEM
makeLogicItem lid :: lid
lid = LIB_ITEM -> Annoted LIB_ITEM
forall a. a -> Annoted a
emptyAnno (LIB_ITEM -> Annoted LIB_ITEM) -> LIB_ITEM -> Annoted LIB_ITEM
forall a b. (a -> b) -> a -> b
$ LogicDescr -> Range -> LIB_ITEM
Logic_decl
  (Logic_name -> LogicDescr
nameToLogicDescr (Logic_name -> LogicDescr) -> Logic_name -> LogicDescr
forall a b. (a -> b) -> a -> b
$ String -> Maybe Token -> Maybe SPEC_NAME -> Logic_name
Logic_name
   (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid) Maybe Token
forall a. Maybe a
Nothing Maybe SPEC_NAME
forall a. Maybe a
Nothing) Range
nullRange

makeSpecItem :: SPEC_NAME -> Annoted SPEC -> Annoted LIB_ITEM
makeSpecItem :: SPEC_NAME -> Annoted SPEC -> Annoted LIB_ITEM
makeSpecItem sn :: SPEC_NAME
sn as :: Annoted SPEC
as =
    LIB_ITEM -> Annoted LIB_ITEM
forall a. a -> Annoted a
emptyAnno (LIB_ITEM -> Annoted LIB_ITEM) -> LIB_ITEM -> Annoted LIB_ITEM
forall a b. (a -> b) -> a -> b
$ SPEC_NAME -> GENERICITY -> Annoted SPEC -> Range -> LIB_ITEM
Spec_defn SPEC_NAME
sn GENERICITY
emptyGenericity Annoted SPEC
as Range
nullRange

fromBasicSpec :: LibName -> SPEC_NAME -> G_basic_spec -> LIB_DEFN
fromBasicSpec :: LibName -> SPEC_NAME -> G_basic_spec -> LIB_DEFN
fromBasicSpec ln :: LibName
ln sn :: SPEC_NAME
sn gbs :: G_basic_spec
gbs =
    LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn LibName
ln [SPEC_NAME -> Annoted SPEC -> Annoted LIB_ITEM
makeSpecItem SPEC_NAME
sn (Annoted SPEC -> Annoted LIB_ITEM)
-> Annoted SPEC -> Annoted LIB_ITEM
forall a b. (a -> b) -> a -> b
$ G_basic_spec -> Annoted SPEC
makeSpec G_basic_spec
gbs] Range
nullRange []

getDeclSpecNames :: LIB_ITEM -> [IRI]
getDeclSpecNames :: LIB_ITEM -> [SPEC_NAME]
getDeclSpecNames li :: LIB_ITEM
li = case LIB_ITEM
li of
  Spec_defn sn :: SPEC_NAME
sn _ _ _ -> [SPEC_NAME
sn]
  Download_items _ di :: DownloadItems
di _ -> DownloadItems -> [SPEC_NAME]
getImportNames DownloadItems
di
  _ -> []

getImportNames :: DownloadItems -> [IRI]
getImportNames :: DownloadItems -> [SPEC_NAME]
getImportNames di :: DownloadItems
di = case DownloadItems
di of
  ItemMaps im :: [ItemNameMap]
im -> (ItemNameMap -> SPEC_NAME) -> [ItemNameMap] -> [SPEC_NAME]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ItemNameMap i :: SPEC_NAME
i mi :: Maybe SPEC_NAME
mi) -> SPEC_NAME -> Maybe SPEC_NAME -> SPEC_NAME
forall a. a -> Maybe a -> a
fromMaybe SPEC_NAME
i Maybe SPEC_NAME
mi) [ItemNameMap]
im
  UniqueItem i :: SPEC_NAME
i -> [SPEC_NAME
i]

getOms :: OmsOrNetwork -> [SPEC]
getOms :: OmsOrNetwork -> [SPEC]
getOms o :: OmsOrNetwork
o = case OmsOrNetwork
o of
  MkOms s :: Annoted SPEC
s -> [Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
s]
  MkNetwork _ -> []

getSpecDef :: LIB_ITEM -> [SPEC]
getSpecDef :: LIB_ITEM -> [SPEC]
getSpecDef li :: LIB_ITEM
li = case LIB_ITEM
li of
  Spec_defn _ _ as :: Annoted SPEC
as _ -> [Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
as]
  View_defn _ _ (View_type s1 :: Annoted SPEC
s1 s2 :: Annoted SPEC
s2 _) _ _ -> [Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
s1, Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
s2]
  Entail_defn _ (Entail_type s1 :: OmsOrNetwork
s1 s2 :: OmsOrNetwork
s2 _) _ -> OmsOrNetwork -> [SPEC]
getOms OmsOrNetwork
s1 [SPEC] -> [SPEC] -> [SPEC]
forall a. [a] -> [a] -> [a]
++ OmsOrNetwork -> [SPEC]
getOms OmsOrNetwork
s2
  Equiv_defn _ (Equiv_type s1 :: OmsOrNetwork
s1 s2 :: OmsOrNetwork
s2 _) as :: OmsOrNetwork
as _ ->
    OmsOrNetwork -> [SPEC]
getOms OmsOrNetwork
s1 [SPEC] -> [SPEC] -> [SPEC]
forall a. [a] -> [a] -> [a]
++ OmsOrNetwork -> [SPEC]
getOms OmsOrNetwork
s2 [SPEC] -> [SPEC] -> [SPEC]
forall a. [a] -> [a] -> [a]
++ OmsOrNetwork -> [SPEC]
getOms OmsOrNetwork
as
  Align_defn _ _ (View_type s1 :: Annoted SPEC
s1 s2 :: Annoted SPEC
s2 _) _ _ _ -> [Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
s1, Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
s2]
  Module_defn _ (Module_type s1 :: Annoted SPEC
s1 s2 :: Annoted SPEC
s2 _) _ _ -> [Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
s1, Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
s2]
  _ -> []

-- Generated by DrIFT, look but don't touch!

instance GetRange LIB_DEFN where
  getRange :: LIB_DEFN -> Range
getRange x :: LIB_DEFN
x = case LIB_DEFN
x of
    Lib_defn _ _ p :: Range
p _ -> Range
p
  rangeSpan :: LIB_DEFN -> [Pos]
rangeSpan x :: LIB_DEFN
x = case LIB_DEFN
x of
    Lib_defn a :: LibName
a b :: [Annoted LIB_ITEM]
b c :: Range
c d :: [Annotation]
d -> [[Pos]] -> [Pos]
joinRanges [LibName -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan LibName
a, [Annoted LIB_ITEM] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted LIB_ITEM]
b,
                                    Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c, [Annotation] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annotation]
d]

instance GetRange LIB_ITEM where
  getRange :: LIB_ITEM -> Range
getRange x :: LIB_ITEM
x = case LIB_ITEM
x of
    Spec_defn _ _ _ p :: Range
p -> Range
p
    View_defn _ _ _ _ p :: Range
p -> Range
p
    Entail_defn _ _ p :: Range
p -> Range
p
    Equiv_defn _ _ _ p :: Range
p -> Range
p
    Align_defn _ _ _ _ _ p :: Range
p -> Range
p
    Module_defn _ _ _ p :: Range
p -> Range
p
    Query_defn _ _ _ _ _ p :: Range
p -> Range
p
    Subst_defn _ _ _ p :: Range
p -> Range
p
    Result_defn _ _ _ _ p :: Range
p -> Range
p
    Arch_spec_defn _ _ p :: Range
p -> Range
p
    Unit_spec_defn _ _ p :: Range
p -> Range
p
    Ref_spec_defn _ _ p :: Range
p -> Range
p
    Network_defn _ _ p :: Range
p -> Range
p
    Download_items _ _ p :: Range
p -> Range
p
    Logic_decl _ p :: Range
p -> Range
p
    Newlogic_defn _ p :: Range
p -> Range
p
    Newcomorphism_defn _ p :: Range
p -> Range
p
  rangeSpan :: LIB_ITEM -> [Pos]
rangeSpan x :: LIB_ITEM
x = case LIB_ITEM
x of
    Spec_defn a :: SPEC_NAME
a b :: GENERICITY
b c :: Annoted SPEC
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, GENERICITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan GENERICITY
b,
                                     Annoted SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted SPEC
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    View_defn a :: SPEC_NAME
a b :: GENERICITY
b c :: VIEW_TYPE
c d :: [G_mapping]
d e :: Range
e -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, GENERICITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan GENERICITY
b,
                                       VIEW_TYPE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan VIEW_TYPE
c, [G_mapping] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [G_mapping]
d, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
e]
    Entail_defn a :: SPEC_NAME
a b :: ENTAIL_TYPE
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, ENTAIL_TYPE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan ENTAIL_TYPE
b,
                                     Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Equiv_defn a :: SPEC_NAME
a b :: EQUIV_TYPE
b c :: OmsOrNetwork
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, EQUIV_TYPE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan EQUIV_TYPE
b,
                                      OmsOrNetwork -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan OmsOrNetwork
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    Align_defn a :: SPEC_NAME
a b :: Maybe ALIGN_ARITIES
b c :: VIEW_TYPE
c d :: [CORRESPONDENCE]
d e :: AlignSem
e f :: Range
f -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, Maybe ALIGN_ARITIES -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Maybe ALIGN_ARITIES
b,
                                          VIEW_TYPE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan VIEW_TYPE
c, [CORRESPONDENCE] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [CORRESPONDENCE]
d, AlignSem -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan AlignSem
e, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
f]
    Module_defn a :: SPEC_NAME
a b :: MODULE_TYPE
b c :: G_symb_items_list
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, MODULE_TYPE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan MODULE_TYPE
b,
                                       G_symb_items_list -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan G_symb_items_list
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    Query_defn a :: SPEC_NAME
a b :: G_symb_items_list
b c :: G_basic_spec
c d :: Annoted SPEC
d e :: Maybe SPEC_NAME
e f :: Range
f -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, G_symb_items_list -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan G_symb_items_list
b,
                                          G_basic_spec -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan G_basic_spec
c, Annoted SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted SPEC
d, Maybe SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Maybe SPEC_NAME
e, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
f]
    Subst_defn a :: SPEC_NAME
a b :: VIEW_TYPE
b c :: G_symb_map_items_list
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, VIEW_TYPE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan VIEW_TYPE
b,
                                      G_symb_map_items_list -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan G_symb_map_items_list
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    Result_defn a :: SPEC_NAME
a b :: [SPEC_NAME]
b c :: SPEC_NAME
c d :: Bool
d e :: Range
e -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, [SPEC_NAME] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [SPEC_NAME]
b,
                                         SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
c, Bool -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Bool
d, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
e]
    Arch_spec_defn a :: SPEC_NAME
a b :: Annoted ARCH_SPEC
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, Annoted ARCH_SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted ARCH_SPEC
b,
                                        Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Unit_spec_defn a :: SPEC_NAME
a b :: UNIT_SPEC
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, UNIT_SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan UNIT_SPEC
b,
                                        Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Ref_spec_defn a :: SPEC_NAME
a b :: REF_SPEC
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, REF_SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan REF_SPEC
b,
                                       Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Network_defn a :: SPEC_NAME
a b :: Network
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, Network -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Network
b,
                                      Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Download_items a :: LibName
a b :: DownloadItems
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [LibName -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan LibName
a, DownloadItems -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan DownloadItems
b,
                                        Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Logic_decl a :: LogicDescr
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [LogicDescr -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan LogicDescr
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    Newlogic_defn a :: LogicDef
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [LogicDef -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan LogicDef
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    Newcomorphism_defn a :: ComorphismDef
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [ComorphismDef -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan ComorphismDef
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]

instance GetRange AlignSem where
  getRange :: AlignSem -> Range
getRange = Range -> AlignSem -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: AlignSem -> [Pos]
rangeSpan x :: AlignSem
x = case AlignSem
x of
    SingleDomain -> []
    GlobalDomain -> []
    ContextualizedDomain -> []

instance GetRange DownloadItems where
  getRange :: DownloadItems -> Range
getRange = Range -> DownloadItems -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: DownloadItems -> [Pos]
rangeSpan x :: DownloadItems
x = case DownloadItems
x of
    ItemMaps a :: [ItemNameMap]
a -> [[Pos]] -> [Pos]
joinRanges [[ItemNameMap] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [ItemNameMap]
a]
    UniqueItem a :: SPEC_NAME
a -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a]

instance GetRange GENERICITY where
  getRange :: GENERICITY -> Range
getRange x :: GENERICITY
x = case GENERICITY
x of
    Genericity _ _ p :: Range
p -> Range
p
  rangeSpan :: GENERICITY -> [Pos]
rangeSpan x :: GENERICITY
x = case GENERICITY
x of
    Genericity a :: PARAMS
a b :: IMPORTED
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PARAMS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PARAMS
a, IMPORTED -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan IMPORTED
b,
                                    Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

instance GetRange PARAMS where
  getRange :: PARAMS -> Range
getRange = Range -> PARAMS -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: PARAMS -> [Pos]
rangeSpan x :: PARAMS
x = case PARAMS
x of
    Params a :: [Annoted SPEC]
a -> [[Pos]] -> [Pos]
joinRanges [[Annoted SPEC] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted SPEC]
a]

instance GetRange IMPORTED where
  getRange :: IMPORTED -> Range
getRange = Range -> IMPORTED -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: IMPORTED -> [Pos]
rangeSpan x :: IMPORTED
x = case IMPORTED
x of
    Imported a :: [Annoted SPEC]
a -> [[Pos]] -> [Pos]
joinRanges [[Annoted SPEC] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted SPEC]
a]

instance GetRange VIEW_TYPE where
  getRange :: VIEW_TYPE -> Range
getRange x :: VIEW_TYPE
x = case VIEW_TYPE
x of
    View_type _ _ p :: Range
p -> Range
p
  rangeSpan :: VIEW_TYPE -> [Pos]
rangeSpan x :: VIEW_TYPE
x = case VIEW_TYPE
x of
    View_type a :: Annoted SPEC
a b :: Annoted SPEC
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [Annoted SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted SPEC
a, Annoted SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted SPEC
b,
                                   Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

instance GetRange EQUIV_TYPE where
  getRange :: EQUIV_TYPE -> Range
getRange x :: EQUIV_TYPE
x = case EQUIV_TYPE
x of
    Equiv_type _ _ p :: Range
p -> Range
p
  rangeSpan :: EQUIV_TYPE -> [Pos]
rangeSpan x :: EQUIV_TYPE
x = case EQUIV_TYPE
x of
    Equiv_type a :: OmsOrNetwork
a b :: OmsOrNetwork
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [OmsOrNetwork -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan OmsOrNetwork
a, OmsOrNetwork -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan OmsOrNetwork
b,
                                    Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

instance GetRange MODULE_TYPE where
  getRange :: MODULE_TYPE -> Range
getRange x :: MODULE_TYPE
x = case MODULE_TYPE
x of
    Module_type _ _ p :: Range
p -> Range
p
  rangeSpan :: MODULE_TYPE -> [Pos]
rangeSpan x :: MODULE_TYPE
x = case MODULE_TYPE
x of
    Module_type a :: Annoted SPEC
a b :: Annoted SPEC
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [Annoted SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted SPEC
a, Annoted SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted SPEC
b,
                                     Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

instance GetRange ALIGN_ARITIES where
  getRange :: ALIGN_ARITIES -> Range
getRange = Range -> ALIGN_ARITIES -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: ALIGN_ARITIES -> [Pos]
rangeSpan x :: ALIGN_ARITIES
x = case ALIGN_ARITIES
x of
    Align_arities a :: ALIGN_ARITY
a b :: ALIGN_ARITY
b -> [[Pos]] -> [Pos]
joinRanges [ALIGN_ARITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan ALIGN_ARITY
a, ALIGN_ARITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan ALIGN_ARITY
b]

instance GetRange ALIGN_ARITY where
  getRange :: ALIGN_ARITY -> Range
getRange = Range -> ALIGN_ARITY -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: ALIGN_ARITY -> [Pos]
rangeSpan x :: ALIGN_ARITY
x = case ALIGN_ARITY
x of
    AA_InjectiveAndTotal -> []
    AA_Injective -> []
    AA_Total -> []
    AA_NeitherInjectiveNorTotal -> []

instance GetRange OmsOrNetwork where
  getRange :: OmsOrNetwork -> Range
getRange = Range -> OmsOrNetwork -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: OmsOrNetwork -> [Pos]
rangeSpan x :: OmsOrNetwork
x = case OmsOrNetwork
x of
    MkOms a :: Annoted SPEC
a -> [[Pos]] -> [Pos]
joinRanges [Annoted SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted SPEC
a]
    MkNetwork a :: Network
a -> [[Pos]] -> [Pos]
joinRanges [Network -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Network
a]

instance GetRange ENTAIL_TYPE where
  getRange :: ENTAIL_TYPE -> Range
getRange x :: ENTAIL_TYPE
x = case ENTAIL_TYPE
x of
    Entail_type _ _ p :: Range
p -> Range
p
    OMSInNetwork _ _ _ p :: Range
p -> Range
p
  rangeSpan :: ENTAIL_TYPE -> [Pos]
rangeSpan x :: ENTAIL_TYPE
x = case ENTAIL_TYPE
x of
    Entail_type a :: OmsOrNetwork
a b :: OmsOrNetwork
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [OmsOrNetwork -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan OmsOrNetwork
a, OmsOrNetwork -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan OmsOrNetwork
b,
                                     Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    OMSInNetwork a :: SPEC_NAME
a b :: Network
b c :: SPEC
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, Network -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Network
b,
                                        SPEC -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]

instance GetRange ItemNameMap where
  getRange :: ItemNameMap -> Range
getRange = Range -> ItemNameMap -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: ItemNameMap -> [Pos]
rangeSpan x :: ItemNameMap
x = case ItemNameMap
x of
    ItemNameMap a :: SPEC_NAME
a b :: Maybe SPEC_NAME
b -> [[Pos]] -> [Pos]
joinRanges [SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SPEC_NAME
a, Maybe SPEC_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Maybe SPEC_NAME
b]