content: module LF.MorphParser where
  
  import LF.Sign
  import LF.Morphism
  
  import Common.Lexer
  import Common.Parsec
  import Common.AnnoParser (commentLine)
  
  import Text.ParserCombinators.Parsec
  
  import System.Directory
  import System.IO.Unsafe
  
  import qualified Data.Map as Map
  import Data.Maybe (fromMaybe)
  
  
  readMorphism :: FilePath -> Morphism
  readMorphism file =
       let mor = unsafePerformIO $ readMorph file
       in fromMaybe (error $ "readMorphism : Could not read the " ++
                             "morphism from " ++ show file) mor
  
  readMorph :: FilePath -> IO (Maybe Morphism)
  readMorph file = do
    e <- doesFileExist file
    if e then do
         content <- readFile file
         case runParser (parseMorphism << eof) () file content of
                 Right m -> return $ Just m
                 Left err -> error $ show err
         else return Nothing
  
  
  parseMorphism :: CharParser st Morphism
  parseMorphism = do
       skips $ manyTill anyChar (string "=")
       pkeyword "Morphism"
       skipChar '{'
       mb <- parseWithEq "morphBase"
       skipChar ','
       mm <- parseWithEq "morphModule"
       skipChar ','
       mn <- parseWithEq "morphName"
       skipChar ','
       pkeyword "source"
       skipChar '='
       s <- parseSignature
       skipChar ','
       pkeyword "target"
       skipChar '='
       t <- parseSignature
       skipChar ','
       pkeyword "morphType"
       skipChar '='
       mt <- parseMorphType
       skipChar ','
       pkeyword "symMap"
       skipChar '='
       sm <- parseMap
       skipChar '}'
       return $ Morphism mb mm mn s t mt sm
  
  -- | plain string parser with skip
  pkeyword :: String -> CharParser st ()
  pkeyword s = keywordNotFollowedBy s (alphaNum <|> char '/') >> return ()
  
  keywordNotFollowedBy :: String -> CharParser st Char -> CharParser st String
  keywordNotFollowedBy s c = skips $ try $ string s << notFollowedBy c
  
  skips :: CharParser st a -> CharParser st a
  skips = (<< skipMany
          (forget space <|> forget commentLine <|> nestCommentOut <?> ""))
  
  qString :: CharParser st String
  qString = skips endsWithQuot
  
  parensP :: CharParser st a -> CharParser st a
  parensP p = between (skipChar '(') (skipChar ')') p
       <|> p
  
  bracesP :: CharParser st a -> CharParser st a
  bracesP = between (skipChar '{') (skipChar '}')
  
  bracketsP :: CharParser st a -> CharParser st a
  bracketsP = between (skipChar '[') (skipChar ']')
  
  endsWithQuot :: CharParser st String
  endsWithQuot = do
       skipChar '"'
       manyTill anyChar (string "\"")
  
  commaP :: CharParser st ()
  commaP = skipChar ',' >> return ()
  
  sepByComma :: CharParser st a -> CharParser st [a]
  sepByComma p = sepBy1 p commaP
  
  skipChar :: Char -> CharParser st ()
  skipChar = forget . skips . char
  
  parseWithEq :: String -> CharParser st String
  parseWithEq s = do
      pkeyword s
      skipChar '='
      qString
  
  parseSym :: CharParser st Symbol
  parseSym = do
      pkeyword "Symbol"
      skipChar '{'
      sb <- parseWithEq "symBase"
      skipChar ','
      sm <- parseWithEq "symModule"
      skipChar ','
      sn <- parseWithEq "symName"
      skipChar '}'
      return $ Symbol sb sm sn
  
  parse1Context :: CharParser st CONTEXT
  parse1Context = do
      skipChar '('
      v <- qString
      skipChar ','
      e <- parseExp
      option () $ skipChar ')'
      return [(v, e)]
  
  parseExp :: CharParser st EXP
  parseExp = (pkeyword "Type" >> return Type)
     <|> do
      pkeyword "Var"
      fmap Var qString
     <|> do
      pkeyword "Const"
      fmap Const parseSym
     <|> do
      pkeyword "Appl"
      ex <- parensP parseExp
      exl <- bracketsP $ option [] $ sepByComma parseExp
      return $ Appl ex exl
     <|> do
      pkeyword "Func"
      exl <- bracketsP $ option [] $ sepByComma parseExp
      ex <- parensP parseExp
      return $ Func exl ex
     <|> do
      ty <- choice $ map (\ ty -> pkeyword ty >> return ty)
                 ["Pi", "Lamb"]
      c <- bracketsP $ option [] $ sepByComma parse1Context
      e <- parensP parseExp
      return $ (case ty of
          "Pi" -> Pi
          "Lamb" -> Lamb
          _ -> error "Pi or Lamb expected.\n") (concat c) e
  
  parseDef :: CharParser st DEF
  parseDef = do
      pkeyword "Def"
      skipChar '{'
      pkeyword "getSym"
      skipChar '='
      sym <- parseSym
      skipChar ','
      pkeyword "getType"
      skipChar '='
      tp <- parseExp
      skipChar ','
      pkeyword "getValue"
      skipChar '='
      val <- (pkeyword "Nothing" >> return Nothing)
               <|> do pkeyword "Just"
                      e <- parensP parseExp
                      return $ Just e
      skipChar '}'
      return $ Def sym tp val
  
  parseSignature :: CharParser st Sign
  parseSignature = do
      pkeyword "Sign"
      skipChar '{'
      sb <- parseWithEq "sigBase"
      skipChar ','
      sm <- parseWithEq "sigModule"
      skipChar ','
      pkeyword "getDefs"
      skipChar '='
      sd <- bracketsP $ option [] $ sepByComma parseDef
      skipChar '}'
      return $ Sign sb sm sd
  
  parseMorphType :: CharParser st MorphType
  parseMorphType =
       choice $ map (\ t -> pkeyword (show t) >> return t)
            [Definitional, Postulated, Unknown ]
  
  parse1Map :: CharParser st (Symbol, EXP)
  parse1Map = do
      skipChar '('
      s <- parseSym
      skipChar ','
      e <- parseExp
      skipChar ')'
      return (s, e)
  
  parseMap :: CharParser st (Map.Map Symbol EXP)
  parseMap = do
       pkeyword "fromList"
       fmap Map.fromList $ bracketsP $ option [] $ sepByComma parse1Map
  