content: {- |
  Module      :  ./Syntax/Parse_AS_Library.hs
  Description :  parser for DOL documents and CASL specification librariess
  Copyright   :  (c) Maciek Makowski, Uni Bremen 2002-2016
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Grothendieck)
  
  Parser for CASL specification libraries
     Follows Sect. II:3.1.5 of the CASL Reference Manual.
  Parser for DOL documents
     Follows the DOL OMG standard, clause 9.3
  -}
  
  module Syntax.Parse_AS_Library (library) where
  
  import Logic.Grothendieck
  import Syntax.AS_Structured
  import Syntax.AS_Library
  import Syntax.Parse_AS_Structured
  import Syntax.Parse_AS_Architecture
  
  import Common.AS_Annotation
  import Common.AnnoParser
  import Common.AnnoState
  import Common.Id
  import Common.IRI
  
  import Common.Keywords
  import Common.Lexer
  import Common.LibName
  import Common.Parsec
  import Common.Token
  
  import Text.ParserCombinators.Parsec
  import Data.List
  import Data.Maybe (maybeToList)
  import qualified Data.Map as Map
  import Control.Monad
  import qualified Control.Monad.Fail as Fail
  
  import Framework.AS
  
  lGAnnos :: LogicGraph -> AParser st (LogicGraph, [Annotation])
  lGAnnos lG = do
    as <- annos
    let (pfx, _) = partPrefixes as
    return (lG { prefixes = Map.union pfx $ prefixes lG }, as)
  
  -- * Parsing functions
  
  -- | Parse a library of specifications
  library :: LogicGraph -> AParser st LIB_DEFN
  library lG = do
      (lG1, an1) <- lGAnnos lG
      (ps, ln) <- option (nullRange, iriLibName nullIRI) $ do
        s1 <- asKey libraryS <|> asKey "distributed-ontology"
        n <- libName lG1
        return (tokPos s1, n)
      (lG2, an2) <- lGAnnos lG1
      ls <- libItems lG2
      return (Lib_defn ln ls ps (an1 ++ an2))
  
  -- | Parse library name
  -- For expanding the iri of the library name the empty prefix is to `"file://"
  -- to parse the it as an individual file. Otherwise the default empty prefix
  -- would be used.
  libName :: LogicGraph -> AParser st LibName
  libName lG = liftM2 mkLibName (hetIRI lG')
    $ if dolOnly lG then return Nothing else optionMaybe version
    where
      fileIRI = nullIRI { iriScheme = "file://"}
      pm = Map.insert "" fileIRI $ prefixes lG
      lG' = lG {prefixes = pm}
  
  -- | Parse the library version
  version :: AParser st VersionNumber
  version = do
      s <- asKey versionS
      pos <- getPos
      n <- sepBy1 (many1 digit) (string dotS)
      skip
      return (VersionNumber n (tokPos s `appRange` Range [pos]))
  
  -- | Parse the library elements
  libItems :: LogicGraph -> AParser st [Annoted LIB_ITEM]
  libItems l =
       (eof >> return [])
      <|> do
        r <- libItem l
        la <- lineAnnos
        (l', an) <- lGAnnos l
        is <- libItems (case r of
               Logic_decl logD _ ->
                   setLogicName logD l'
               _ -> l')
        case is of
          [] -> return [Annoted r nullRange [] $ la ++ an]
          Annoted i p nl ra : rs ->
            return $ Annoted r nullRange [] la : Annoted i p (an ++ nl) ra : rs
  
  dolImportItem :: LogicGraph -> AParser st LIB_ITEM
  dolImportItem l = do
      s1 <- asKey "import"
      iln <- libName l
      return (Download_items iln (ItemMaps []) $ getRange s1)
  
  networkDefn :: LogicGraph -> AParser st LIB_ITEM
  networkDefn l = do
      kGraph <- asKey "network"
      name <- hetIRI l
      kEqu <- equalT
      n <- parseNetwork l
      kEnd <- asKey endS
      return . Network_defn name n
           . catRange $ [kGraph, kEqu, kEnd]
  
  -- CASL spec-defn or DOL OMSDefn
  specDefn :: LogicGraph -> AParser st LIB_ITEM
  specDefn l = do
      s <- choice $ map asKey
        ["specification", specS, ontologyS, "onto", "model", "OMS", patternS]
      n <- hetIRI l
      g <- generics l
      e <- equalT
      a <- aSpec l
      q <- optEnd
      return . Spec_defn n g a
        . catRange $ [s, e] ++ maybeToList q
  
  -- CASL view-defn or DOL IntprDefn
  viewDefn :: LogicGraph -> AParser st LIB_ITEM
  viewDefn l = do
      s1 <- choice $ map asKey [viewS, interpretationS, refinementS]
      vn <- hetIRI l
      do
         kEqu <- equalT
         rsp <- refSpec l
         kEnd <- optEnd
         return . Ref_spec_defn vn rsp
                     . catRange $ [s1, kEqu] ++ maybeToList kEnd
        <|> do
         g <- generics l
         _ <- annotations -- TODO: store annotations
         s2 <- colonT
         vt <- viewType l
         (symbMap, ps) <- option ([], []) $ do
           s <- equalT
           (m, _) <- parseMapping l
           return (m, [s])
         q <- optEnd
         return . View_defn vn g vt symbMap
           . catRange $ [s1, s2] ++ ps ++ maybeToList q
  
  entailDefn :: LogicGraph -> AParser st LIB_ITEM
  entailDefn l = do
    s <- asKey entailmentS
    n <- hetIRI l
    e <- equalT
    et <- entailType l
    q <- optEnd
    return . Entail_defn n et . catRange $ [s, e] ++ maybeToList q
  
  queryDefn :: LogicGraph -> AParser st LIB_ITEM
  queryDefn l = do
    q <- asKey "query"
    n <- hetIRI l
    e <- equalT
    s <- asKey selectS
    lg <- lookupCurrentLogic "query-defn" l
    (vs, cs) <- parseItemsList lg (prefixes l)
    w <- asKey whereS
    Basic_spec bs _ <- lookupCurrentSyntax "query-defn" l >>= basicSpec l
    i <- asKey inS
    oms <- aSpec l
    mt <- optionMaybe $ asKey "along" >> hetIRI l
    o <- optEnd
    return . Query_defn n vs bs oms mt . catRange
      $ [q, e, s, w] ++ cs ++ [i] ++ maybeToList o
  
  substDefn :: LogicGraph -> AParser st LIB_ITEM
  substDefn l = do
    q <- asKey "substitution"
    n <- hetIRI l
    c <- colonT
    vt <- viewType l
    e <- equalT
    lg <- lookupCurrentLogic "subst-defn" l
    (m, cs) <- parseItemsMap lg (prefixes l)
    o <- optEnd
    return . Subst_defn n vt m . catRange
      $ [q, c, e] ++ cs ++ maybeToList o
  
  resultDefn :: LogicGraph -> AParser st LIB_ITEM
  resultDefn l = do
    q <- asKey resultS
    n <- hetIRI l
    (sns, cs) <- separatedBy (hetIRI l) anComma
    f <- asKey forS
    r <- hetIRI l
    a <- annotations
    o <- optEnd
    return . Result_defn n sns r (any (identAnno "complete") a)
      . catRange $ q : cs ++ [f] ++ maybeToList o
  
  -- | Parse an element of the library
  libItem :: LogicGraph -> AParser st LIB_ITEM
  libItem l = specDefn l
    <|> viewDefn l
    <|> dolImportItem l
    <|> entailDefn l
    <|> queryDefn l
    <|> substDefn l
    <|> resultDefn l
    <|> -- equiv defn
      do s1 <- asKey equivalenceS
         en <- hetIRI l
         s2 <- colonT
         et <- equivType l
         s3 <- equalT
         sp <- fmap MkOms $ aSpec l
         ep <- optEnd
         return . Equiv_defn en et sp
           . catRange $ s1 : s2 : s3 : maybeToList ep
    <|> -- align defn
      do s1 <- asKey alignmentS
         an <- hetIRI l
         ar <- optionMaybe alignArities
         s2 <- colonT
         at <- viewType l
         (corresps, ps, sem) <- option ([], [], SingleDomain) $ do
           s <- equalT
           cs <- parseCorrespondences l
           aSem <- option SingleDomain $ do
              _ <- asKey "assuming"
              choice $ map (\ d -> asKey (show d) >> return d)
                [minBound .. maxBound]
           return (cs, [s], aSem)
         q <- optEnd
         return . Align_defn an ar at corresps sem
           . catRange $ [s1, s2] ++ ps ++ maybeToList q
    <|> -- module defn
      do s1 <- asKey moduleS
         mn <- hetIRI l
         _ <- annotations -- TODO: store annotations
         s2 <- colonT
         mt <- moduleType l
         s3 <- asKey forS
         rs <- restrictionSignature l
         kEnd <- optEnd
         return . Module_defn mn mt rs
           . catRange $ s1 : s2 : s3 : maybeToList kEnd
    <|> -- unit spec
      do kUnit <- asKey unitS
         kSpec <- asKey specS
         name <- hetIRI l
         kEqu <- equalT
         usp <- unitSpec l
         kEnd <- optEnd
         return (Unit_spec_defn name usp
                  (catRange ([kUnit, kSpec, kEqu] ++ maybeToList kEnd)))
    <|> networkDefn l
    <|> -- arch spec
      do kArch <- asKey archS
         kASpec <- asKey specS
         name <- hetIRI l
         kEqu <- equalT
         asp <- annotedArchSpec l
         kEnd <- optEnd
         return (Arch_spec_defn name asp
                  (catRange ([kArch, kASpec, kEqu] ++ maybeToList kEnd)))
    <|> -- download
      do s1 <- asKey fromS
         iln <- libName l
         s2 <- asKey getS
         (il, ps) <- downloadItems l
         q <- optEnd
         return (Download_items iln il
                  (catRange ([s1, s2] ++ ps ++ maybeToList q)))
    <|> -- use (to be removed eventually)
      do asKey "use"
         fmap (addDownloadAux False) $ hetIRI l
    <|> -- logic
      do (s, logD) <- qualification l
         return $ Logic_decl logD $ tokPos s
    <|> -- newlogic
      do (n, s1) <- newlogicP
         s2 <- equalT
         (ml, s3) <- metaP
         (s, s4) <- syntaxP
         (m, s5) <- modelsP
         (f, s6) <- foundationP
         (p, s7) <- proofsP
         (pa, s8) <- patternsP
         q <- optEnd
         return (Newlogic_defn (LogicDef n ml s m f p pa)
            (catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q)))
     <|> -- newcomorphism
       do (n, s1) <- newcomorphismP
          s2 <- equalT
          (ml, s3) <- metaP
          (s, s4) <- sourceP
          (t, s5) <- targetP
          (sv, s6) <- syntaxP
          (pv, s8) <- proofsP
          (mv, s7) <- modelsP
          q <- optEnd
          return (Newcomorphism_defn (ComorphismDef n ml s t sv pv mv)
             (catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q)))
    <|> -- just a spec (turned into "spec spec = sp")
       do p1 <- getPos
          a <- aSpec l
          p2 <- getPos
          if p1 == p2 then Fail.fail "cannot parse spec" else
            return (Spec_defn nullIRI
                 (Genericity (Params []) (Imported []) nullRange) a nullRange)
  
  downloadItems :: LogicGraph -> AParser st (DownloadItems, [Token])
  downloadItems l = do
      (il, ps) <- separatedBy (itemNameOrMap l) anSemiOrComma
      return (ItemMaps il, ps)
    <|> do
      s <- asKey mapsTo
      i <- hetIRI l
      return (UniqueItem i, [s])
  
  entailType :: LogicGraph -> AParser st ENTAIL_TYPE
  entailType l = do
      sp1 <- omsOrNetwork l
      do
          r <- asKey entailsS
          sp2 <- omsOrNetwork l
          return $ Entail_type sp1 sp2 $ tokPos r
        <|> case sp1 of
              MkOms (Annoted (Spec_inst n [] Nothing _) _ _ _) -> do
                i <- asKey inS
                nw <- parseNetwork l
                r <- asKey entailsS
                g <- groupSpec l
                return . OMSInNetwork n nw g $ catRange [i, r]
              _ -> Fail.fail "OMSName expected"
  
  omsOrNetwork :: LogicGraph -> AParser st OmsOrNetwork
  omsOrNetwork l = fmap (MkOms . emptyAnno) $ groupSpec l
  
  equivType :: LogicGraph -> AParser st EQUIV_TYPE
  equivType l = do
      sp1 <- omsOrNetwork l
      r <- equiT
      sp2 <- omsOrNetwork l
      return $ Equiv_type sp1 sp2 $ tokPos r
  
  alignArities :: AParser st ALIGN_ARITIES
  alignArities = do
    asKey alignArityForwardS
    f <- alignArity
    asKey alignArityBackwardS
    b <- alignArity
    return $ Align_arities f b
  
  alignArity :: AParser st ALIGN_ARITY
  alignArity = choice $ map (\ a -> asKey (showAlignArity a) >> return a)
    [minBound .. maxBound]
  
  -- | Parse view type also used in alignments
  viewType :: LogicGraph -> AParser st VIEW_TYPE
  viewType l = do
      sp1 <- annoParser (groupSpec l)
      s <- asKey toS
      sp2 <- annoParser (groupSpec l)
      return $ View_type sp1 sp2 $ tokPos s
  
  moduleType :: LogicGraph -> AParser st MODULE_TYPE
  moduleType l = do
    sp1 <- aSpec l
    s <- asKey ofS
    sp2 <- aSpec l
    return $ Module_type sp1 sp2 (tokPos s)
  
  restrictionSignature :: LogicGraph -> AParser st G_symb_items_list
  restrictionSignature lG = do
    l <- lookupCurrentLogic "restrictionSignature" lG
    fmap fst $ parseItemsList l (prefixes lG)
  
  
  simpleIdOrDDottedId :: GenParser Char st Token
  simpleIdOrDDottedId = pToken $ liftM2 (++)
    (reserved casl_structured_reserved_words scanAnyWords)
    $ optionL $ try $ string ".." <++> scanAnyWords
  
  -- | Parse item name or name map
  itemNameOrMap :: LogicGraph -> AParser st ItemNameMap
  itemNameOrMap l = do
      i1 <- liftM simpleIdToIRI simpleIdOrDDottedId <|> hetIRI l
      i2 <- optionMaybe $ do
          _ <- asKey mapsTo
          if isInfixOf ".." $ iriToStringUnsecure i1
              then liftM simpleIdToIRI simpleIdOrDDottedId
              else hetIRI l
      return $ ItemNameMap i1 i2
  
  optEnd :: AParser st (Maybe Token)
  optEnd = try
      (addAnnos >> optionMaybe (pToken $ keyWord $ string endS))
      << addLineAnnos
  
  generics :: LogicGraph -> AParser st GENERICITY
  generics l = do
      (pa, ps1) <- params l
      (imp, ps2) <- option ([], nullRange) (imports l)
      return $ Genericity (Params pa) (Imported imp) $ appRange ps1 ps2
  
  params :: LogicGraph -> AParser st ([Annoted SPEC], Range)
  params l = do
      pas <- many (param l)
      let (pas1, ps) = unzip pas
      return (pas1, concatMapRange id ps)
  
  param :: LogicGraph -> AParser st (Annoted SPEC, Range)
  param l = do
      b <- oBracketT
      pa <- aSpec l
      c <- cBracketT
      return (pa, toRange b [] c)
  
  imports :: LogicGraph -> AParser st ([Annoted SPEC], Range)
  imports l = do
      s <- asKey givenS
      (sps, ps) <- separatedBy (annoParser $ groupSpec l) anComma
      return (sps, catRange (s : ps))
  
  newlogicP :: AParser st (IRI, Token)
  newlogicP = do
    s <- asKey newlogicS
    n <- simpleId
    return (simpleIdToIRI n, s)
  
  metaP :: AParser st (FRAM, Token)
  metaP = do
    s <- asKey metaS
    f <- framP
    return (f, s)
  
  framP :: AParser st FRAM
  framP = do
      asKey lfS
      return LF
    <|> do
      asKey isabelleS
      return Isabelle
    <|> do
      asKey maudeS
      return Maude
  
  syntaxP :: AParser st (IRI, Token)
  syntaxP = do
    s <- asKey syntaxS
    t <- simpleIdOrDDottedId
    return (simpleIdToIRI t, s)
  
  modelsP :: AParser st (IRI, Token)
  modelsP = do
      s <- asKey modelsS
      m <- simpleIdOrDDottedId
      return (simpleIdToIRI m, s)
    <|> return (nullIRI, nullTok)
  
  foundationP :: AParser st (IRI, Token)
  foundationP = do
      s <- asKey foundationS
      f <- simpleId
      return (simpleIdToIRI f, s)
    <|> return (nullIRI, nullTok)
  
  proofsP :: AParser st (IRI, Token)
  proofsP = do
      s <- asKey proofsS
      p <- simpleIdOrDDottedId
      return (simpleIdToIRI p, s)
    <|> return (nullIRI, nullTok)
  
  patternsP :: AParser st (Token, Token)
  patternsP = do
      s <- asKey patternsS
      p <- simpleId
      return (p, s)
    <|> return (nullTok, nullTok)
  
  newcomorphismP :: AParser st (IRI, Token)
  newcomorphismP = do
    -- add newcomorphismS = "newcomorphism" in
    s <- asKey newcomorphismS
    n <- simpleId
    return (simpleIdToIRI n, s)
  
  sourceP :: AParser st (IRI, Token)
  sourceP = do
    s <- asKey sourceS
    sl <- simpleIdOrDDottedId
    return (simpleIdToIRI sl, s)
  
  targetP :: AParser st (IRI, Token)
  targetP = do
    s <- asKey targetS
    tl <- simpleIdOrDDottedId
    return (simpleIdToIRI tl, s)
  