{-# LANGUAGE ViewPatterns #-}

module PLpatt.StaticAnaPLpatt

where

import qualified PLpatt.AS_BASIC_PLpatt as As

import qualified PLpatt.Sign as Sign

import PLpatt.Tools

import Common.AS_Annotation

import Common.GlobalAnnotations

import Common.Result

import Common.ExtSign

import Common.Id

import Data.Maybe

import qualified Data.Set as Set

import System.IO.Unsafe (unsafePerformIO)

import qualified MMT.XMLtoPT as XML

import qualified MMT.Tools as PT

import System.IO.Temp

import System.IO

import qualified MMT.Hets2mmt as MMT

import Data.List

import qualified Data.Map as Map

import System.Directory (removeFile)

import Common.Utils (getEnvDef)

import Debug.Trace

basicAna :: (As.Basic_spec, Sign.Sigs, GlobalAnnos) ->

Result (

As.Basic_spec,

ExtSign Sign.Sigs As.Symb,

[Named As.Bool']

)

basicAna (bs, Sign.Sigs sg, ann) = let

def_namespace = "http://cds.omdoc.org/hets-test"

namespace = case Map.lookup "namespace:"

(prefix_map ann) of

Just x -> show x

Nothing -> def_namespace

(newsg, symbs) = mmtAna namespace bs

(sens, sgdcl) = getSens $ Sign.Sigs newsg

sgn = ExtSign (Sign.Sigs (sgdcl ++ sg))

symbs

in

return (bs, sgn, sens)

-- logic id is inserted by MMT

lid :: String

lid = "PLpatt"

hetslib :: String

hetslib = unsafePerformIO $ getEnvDef "HETS_LIB" ""

mmtAna :: String -> As.Basic_spec -> ([As.Decl], Set.Set As.Symb)

mmtAna namespace (As.Basic_spec bs) = let

tdecls = unsafePerformIO $

getDecls namespace bs

decls = map decl2decl tdecls

symbs = newSymbs $ map (fromJust . maybeResult) tdecls

in

(map (fromJust . maybeResult) decls, symbs)

-- separators used by MMT: group s, unit s, record s

gs :: String

gs = "\29"

us :: String

us = "\31"

rs :: String

rs = "\30"

-- compile lines into a temp file

compileMMTsrc :: String -> [String] -> IO FilePath

compileMMTsrc ns rest = do let cont = "namespace " ++ ns ++ gs ++ "\n" ++

"theory " ++ lid ++ "spec : " ++

"?" ++ lid ++

" = \n" ++ "\n" ++

unlines (map (++ rs) rest) ++

"\n" ++ gs

(fpath, fhand) <- openTempFile "MMTtmp"

"input.mmt"

hPutStr fhand cont

hClose fhand

return fpath

-- sort declarations

arrangeFileSrc :: String -> [String] -> [String]

arrangeFileSrc (stripPrefix "namespace" -> Just uri) ls =

("namespace" ++ uri) : ls

arrangeFileSrc s ls = ls ++ [s]

-- grab namespace uri

getNamespace :: String -> Maybe String

getNamespace (stripPrefix "namespace " -> Just uri) = Just uri

getNamespace _ = Nothing

getDecls :: String -> [String] -> IO [Result PT.Decl]

getDecls ns sl = do

fp <- compileMMTsrc ns $ filter (/= "") sl

MMT.callSpec fp

XML.parse $ hetslib ++ "MMT/xml/" ++ lid ++ "spec.xml"

{- helper method that translates

parse tree declarations to logic declarations -}

decl2decl :: Result PT.Decl -> Result As.Decl

decl2decl rsptdcl = let dcl = maybeResult rsptdcl

in

case dcl of

Just mbds -> case decl_from_pt mbds of

(Just ds) -> Result [] (Just ds )

Nothing -> fatal_error

"failed to parse parse-tree"

nullRange

Nothing -> fatal_error "Result of parse tree failure"

nullRange

isSen :: As.Decl -> Bool

isSen (As.Dot_decl _) = True

isSen _ = False

splitSen :: [As.Decl] -> ([As.Decl], [As.Decl])

splitSen = partition isSen

decl2sen :: As.Decl -> Maybe (Named As.Bool')

decl2sen (As.Dot_decl (As.Dot name f)) = Just $ makeNamed name f

decl2sen _ = Nothing

getSens :: Sign.Sigs -> ([Named As.Bool'], [As.Decl])

getSens (Sign.Sigs decls) = let

(sendcl, sgsdcl) = splitSen decls

sens = map (fromJust . decl2sen) sendcl

in

(sens, sgsdcl)

decl2symb :: PT.Decl -> As.Symb

decl2symb (PT.Decl _ iname _) = As.Symb iname

newSymbs :: [PT.Decl] -> Set.Set As.Symb

newSymbs dcls = let sls = map decl2symb dcls

in foldr Set.insert Set.empty sls