content: {- |
  Module      :  ./HasCASL/ParseItem.hs
  Description :  parser for HasCASL basic Items
  Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  parser for HasCASL basic Items
  -}
  
  module HasCASL.ParseItem (basicItems, basicSpec) where
  
  import Text.ParserCombinators.Parsec
  
  import Common.AS_Annotation
  import Common.AnnoState
  import Common.Id
  import Common.Keywords
  import Common.Lexer
  import Common.Parsec
  import Common.Token
  
  import HasCASL.As
  import HasCASL.AsUtils
  import HasCASL.HToken
  import HasCASL.ParseTerm
  
  import Control.Monad
  import qualified Control.Monad.Fail as Fail
  
  -- * adapted item list parser (using 'itemAux')
  
  hasCaslItemList :: String -> AParser st b
                  -> ([Annoted b] -> Range -> a) -> AParser st a
  hasCaslItemList kw ip constr = do
      p <- pluralKeyword kw
      auxItemList hasCaslStartKeywords [p] ip constr
  
  hasCaslItemAux :: [Token] -> AParser st b -> ([Annoted b] -> Range -> a)
                 -> AParser st a
  hasCaslItemAux = auxItemList hasCaslStartKeywords
  
  -- * parsing type items
  
  commaTypeDecl :: TypePattern -> AParser st TypeItem
  commaTypeDecl s = do
      c <- anComma
      (is, cs) <- typePattern `separatedBy` anComma
      let l = s : is
          p = c : cs
      subTypeDecl (l, p) <|> kindedTypeDecl (l, p)
          <|> return (TypeDecl l universe $ catRange p)
  
  kindedTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
  kindedTypeDecl (l, p) = do
      t <- colT
      s <- kind
      let d = TypeDecl l s $ catRange $ p ++ [t]
      case l of
        [hd] -> pseudoTypeDef hd (Just s) [t] <|> dataDef hd s [t] <|> return d
        _ -> return d
  
  isoDecl :: TypePattern -> AParser st TypeItem
  isoDecl s = do
      e <- equalT
      subTypeDefn (s, e) <|> do
          (l, p) <- typePattern `separatedBy` equalT
          return $ IsoDecl (s : l) $ catRange $ e : p
  
  vars :: AParser st Vars
  vars = fmap Var var <|> do
      o <- oParenT
      (vs, ps) <- vars `separatedBy` anComma
      c <- cParenT
      return $ VarTuple vs $ toRange o ps c
  
  subTypeDefn :: (TypePattern, Token) -> AParser st TypeItem
  subTypeDefn (s, e) = do
      a <- annos
      o <- oBraceT << addAnnos
      v <- vars
      c <- colT
      t <- parseType
      d <- dotT -- or bar
      f <- term
      a2 <- annos
      p <- cBraceT
      let qs = toRange e [o, c, d] p
      return $ SubtypeDefn s v t (Annoted f qs a a2) qs
  
  subTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
  subTypeDecl (l, p) = do
      t <- lessT
      s <- parseType
      return $ SubtypeDecl l s $ catRange $ p ++ [t]
  
  sortItem :: AParser st TypeItem
  sortItem = do
      s <- typePattern
      subTypeDecl ([s], [])
          <|> kindedTypeDecl ([s], [])
          <|> commaTypeDecl s
          <|> isoDecl s
          <|> return (TypeDecl [s] universe nullRange)
  
  sortItems :: AParser st SigItems
  sortItems = hasCaslItemList sortS sortItem (TypeItems Plain)
  
  typeItem :: AParser st TypeItem
  typeItem = do
      s <- typePattern
      subTypeDecl ([s], [])
          <|> dataDef s universe []
          <|> pseudoTypeDef s Nothing []
          <|> kindedTypeDecl ([s], [])
          <|> commaTypeDecl s
          <|> isoDecl s
          <|> return (TypeDecl [s] universe nullRange)
  
  typeItemList :: [Token] -> Instance -> AParser st SigItems
  typeItemList ps = hasCaslItemAux ps typeItem . TypeItems
  
  typeItems :: AParser st SigItems
  typeItems = do
      p <- pluralKeyword typeS
      do q <- pluralKeyword instanceS
         typeItemList [p, q] Instance
        <|> typeItemList [p] Plain
  
  pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
  pseudoTypeDef t k l = do
      c <- asKey assignS
      p <- parseType
      return $ AliasType t k (simpleTypeScheme p) $ catRange $ l ++ [c]
  
  -- * parsing datatypes
  
  component :: AParser st [Component]
  component = try (do
      (is, cs) <- opId `separatedBy` anComma
      compType is cs) <|> do
      t <- parseType
      return [NoSelector t]
  
  concatFst :: [[a]] -> Range -> ([a], Range)
  concatFst as ps = (concat as, ps)
  
  tupleComponent :: AParser st ([Component], Range)
  tupleComponent = bracketParser component oParenT cParenT anSemi concatFst
  
  altComponent :: AParser st ([Component], Range)
  altComponent = tupleComponent <|> do
      i <- typeVar
      let t = case i of
            Id [tok] [] _ -> TypeToken tok
            _ -> error "altComponent"
      return ([NoSelector t], nullRange)
  
  compType :: [Id] -> [Token] -> AParser st [Component]
  compType is cs = do
      c <- colonST
      t <- parseType
      let makeComps l1 l2 = case (l1, l2) of
            ([a], [b]) -> [Selector a Total t Other $ tokPos b]
            (a : r, b : s) -> Selector a Total t Comma (tokPos b) : makeComps r s
            _ -> error "makeComps: empty selector list"
      return $ makeComps is $ cs ++ [c]
  
  alternative :: AParser st Alternative
  alternative = do
      s <- pluralKeyword sortS <|> pluralKeyword typeS
      (ts, cs) <- parseType `separatedBy` anComma
      return $ Subtype ts $ catRange $ s : cs
    <|> do
      i <- hconsId
      cps <- many altComponent
      let ps = concatMapRange snd cps
          cs = map fst cps
      do q <- quMarkT
         return $ Constructor i cs Partial $ appRange ps $ tokPos q
        <|> return (Constructor i cs Total ps)
  
  dataDef :: TypePattern -> Kind -> [Token] -> AParser st TypeItem
  dataDef t k l = do
      c <- asKey defnS
      a <- annos
      let aAlternative = liftM2 (\ i -> Annoted i nullRange [])
            alternative annos
      (Annoted v _ _ b : as, ps) <- aAlternative `separatedBy` barT
      let aa = Annoted v nullRange a b : as
          qs = catRange $ l ++ c : ps
      do d <- asKey derivingS
         (cs, cps) <- classId `separatedBy` anComma
         return $ Datatype $ DatatypeDecl t k aa cs
           $ appRange qs $ appRange (tokPos d) $ catRange cps
        <|> return (Datatype (DatatypeDecl t k aa [] qs))
  
  dataItem :: AParser st DatatypeDecl
  dataItem = do
       t <- typePattern
       do c <- colT
          k <- kind
          Datatype d <- dataDef t k [c]
          return d
         <|> do
           Datatype d <- dataDef t universe []
           return d
  
  dataItems :: AParser st BasicItem
  dataItems = hasCaslItemList typeS dataItem FreeDatatype
  
  -- * parse class items
  
  classDecl :: AParser st ClassDecl
  classDecl = do
      (is, cs) <- classId `separatedBy` anComma
      (ps, k) <- option ([], universe) $ pair (single $ lessT <|> colonT) kind
      return $ ClassDecl is k $ catRange $ cs ++ ps
  
  classItem :: AParser st ClassItem
  classItem = do
      c <- classDecl
      do o <- oBraceT
         is <- annosParser basicItems
         p <- cBraceT
         return $ ClassItem c is $ toRange o [] p
        <|> return (ClassItem c [] nullRange)
  
  classItemList :: [Token] -> Instance -> AParser st BasicItem
  classItemList ps = hasCaslItemAux ps classItem . ClassItems
  
  classItems :: AParser st BasicItem
  classItems = do
      p <- asKey (classS ++ "es") <|> asKey classS <?> classS
      do q <- pluralKeyword instanceS
         classItemList [p, q] Instance
        <|> classItemList [p] Plain
  
  -- * parse op items
  
  opAttr :: AParser st OpAttr
  opAttr = let l = [Assoc, Comm, Idem] in
      choice (map ( \ a -> do
        b <- asKey $ show a
        return $ BinOpAttr a $ tokPos b) l)
      <|> do
      a <- asKey unitS
      t <- term
      return $ UnitOpAttr t $ tokPos a
  
  multiTypeScheme :: [PolyId] -> AParser st TypeScheme
  multiTypeScheme os = case os of
      p : r -> if null r || all ( \ (PolyId _ tys _) -> null tys) os
        then typeScheme p
        else Fail.fail $ "instantiation list in identifier list: "
                 ++ show (map ( \ (PolyId i _ _) -> i) os)
      _ -> error "HasCASL.ParseItem.opDecl"
  
  opDecl :: [PolyId] -> [Token] -> AParser st OpItem
  opDecl os ps = do
      c <- colonST
      t <- multiTypeScheme os
      opAttrs os ps c t <|> return (OpDecl os t [] $ catRange $ ps ++ [c])
  
  opAttrs :: [PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
  opAttrs os ps c t = do
      d <- anComma
      (attrs, cs) <- opAttr `separatedBy` anComma
      return $ OpDecl os t attrs $ catRange $ ps ++ [c, d] ++ cs
  
  opArg :: AParser st ([VarDecl], Range)
  opArg = bracketParser varDecls oParenT cParenT anSemi concatFst
  
  opArgs :: AParser st ([[VarDecl]], Range)
  opArgs = do
      cps <- many1 opArg
      return (map fst cps, concatMapRange snd cps)
  
  opDeclOrDefn :: PolyId -> AParser st OpItem
  opDeclOrDefn o = do
      c <- colonST
      t <- typeScheme o
      opAttrs [o] [] c t <|> opTerm o [] nullRange c t
          <|> return (OpDecl [o] t [] $ tokPos c)
    <|> do
      (args, ps) <- opArgs
      c <- colonST
      t <- fmap simpleTypeScheme parseType
      opTerm o args ps c t
  
  opTerm :: PolyId -> [[VarDecl]] -> Range -> Token -> TypeScheme
         -> AParser st OpItem
  opTerm o as ps c sc = do
      e <- equalT
      f <- term
      return $ OpDefn o as sc f $ appRange ps $ toRange c [] e
  
  opItem :: AParser st OpItem
  opItem = do
      (os, ps) <- parsePolyId `separatedBy` anComma
      case os of
        [hd] -> opDeclOrDefn hd
        _ -> opDecl os ps
  
  opItems :: AParser st SigItems
  opItems = hasCaslItemList opS opItem (OpItems Op)
      <|> hasCaslItemList functS opItem (OpItems Fun)
  
  -- * parse pred items as op items
  
  predDecl :: [PolyId] -> [Token] -> AParser st OpItem
  predDecl os ps = do
      c <- colT
      t <- multiTypeScheme os
      let p = catRange $ ps ++ [c]
      return $ OpDecl os (predTypeScheme p t) [] p
  
  predDefn :: PolyId -> AParser st OpItem
  predDefn o = do
      (args, ps) <- opArg
      e <- asKey equivS
      f <- term
      let p = appRange ps $ tokPos e
      return $ OpDefn o [args]
          (simpleTypeScheme $ mkLazyType $ unitTypeWithRange p) f p
  
  predItem :: AParser st OpItem
  predItem = do
      (os, ps) <- parsePolyId `separatedBy` anComma
      let d = predDecl os ps
      case os of
        [hd] -> d <|> predDefn hd
        _ -> d
  
  predItems :: AParser st SigItems
  predItems = hasCaslItemList predS predItem (OpItems Pred)
  
  -- * other items
  
  sigItems :: AParser st SigItems
  sigItems = sortItems <|> opItems <|> predItems <|> typeItems
  
  generatedItems :: AParser st BasicItem
  generatedItems = do
      g <- asKey generatedS
      do FreeDatatype ds ps <- dataItems
         return $ GenItems [Annoted (TypeItems Plain (map ( \ d -> Annoted
              (Datatype $ item d) nullRange (l_annos d) (r_annos d)) ds) ps)
                            nullRange [] []] $ tokPos g
        <|> do
          o <- oBraceT
          is <- annosParser sigItems
          c <- cBraceT
          return $ GenItems is $ toRange g [o] c
  
  genVarItems :: AParser st ([GenVarDecl], [Token])
  genVarItems = do
      vs <- genVarDecls
      do s <- trySemi << addLineAnnos
         do tryItemEnd hasCaslStartKeywords
            return (vs, [s])
           <|> do
              (ws, ts) <- genVarItems
              return (vs ++ ws, s : ts)
        <|> return (vs, [])
  
  freeDatatype :: AParser st BasicItem
  freeDatatype = do
      f <- asKey freeS
      FreeDatatype ds ps <- dataItems
      return $ FreeDatatype ds $ appRange (tokPos f) ps
  
  progItems :: AParser st BasicItem
  progItems = hasCaslItemList programS
      (patternTermPair [equalS] (WithIn, []) equalS) ProgItems
  
  axiomItems :: AParser st BasicItem
  axiomItems = hasCaslItemList axiomS term $ AxiomItems []
  
  forallItem :: AParser st BasicItem
  forallItem = do
      f <- forallT
      (vs, ps) <- genVarDecls `separatedBy` anSemi
      a <- annos
      AxiomItems _ (Annoted ft qs as rs : fs) ds <- dotFormulae
      let aft = Annoted ft qs (a ++ as) rs
      return $ AxiomItems (concat vs) (aft : fs) $ appRange (catRange $ f : ps) ds
  
  genVarItem :: AParser st BasicItem
  genVarItem = do
      v <- pluralKeyword varS
      (vs, ps) <- genVarItems
      return $ GenVarItems vs $ catRange $ v : ps
  
  dotFormulae :: AParser st BasicItem
  dotFormulae = do
      d <- dotT
      (fs, ds) <- allAnnoParser term `separatedBy` dotT
      let ps = catRange $ d : ds
          lst = last fs
      if null $ r_annos lst then do
          (m, an) <- optSemi
          return $ AxiomItems [] (init fs ++ [appendAnno lst an]) $ appRange ps
                 $ catRange m
         else return $ AxiomItems [] fs ps
  
  internalItems :: AParser st BasicItem
  internalItems = do
      i <- asKey internalS
      o <- oBraceT
      is <- annosParser basicItems
      p <- cBraceT
      return (Internal is $ toRange i [o] p)
  
  basicItems :: AParser st BasicItem
  basicItems = fmap SigItems sigItems
      <|> classItems
      <|> progItems
      <|> generatedItems
      <|> freeDatatype
      <|> genVarItem
      <|> forallItem
      <|> dotFormulae
      <|> axiomItems
      <|> internalItems
  
  basicSpec :: AParser st BasicSpec
  basicSpec = fmap BasicSpec (annosParser basicItems)
  