{-# LANGUAGE ViewPatterns #-}

module <LogicName>.StaticAna<LogicName>

where

import qualified <LogicName>.AS_BASIC_<LogicName> as As

import qualified <LogicName>.Sign as Sign

import <LogicName>.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

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

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

namespace = "http://cds.omdoc.org/hets-test?<LogicName>"

newsg = mmtAna namespace bs

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

Set.empty

nst = []

in

return (bs, sgn, nst)

-- logic id is generated by MMT

lid :: String

lid = "<LogicName>"

mmtAna :: String -> As.Basic_spec -> [As.Decl]

mmtAna namespace (As.Basic_spec bs) = let

decls = unsafePerformIO $

getDecls namespace bs

in

map (fromJust . maybeResult) decls

-- compile lines into a temp file

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

compileMMTsrc ns rest = do

let cont = "%" ++ ns ++ "\n%spec Spec: " ++ lid ++ " = " ++

"\n{\n" ++ (unlines rest) ++ "\n}."

(fpath, fhand) <- openTempFile "MMTtmp"

"input.elf"

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 s = Nothing

-- probably a studpid idea, intersperce and lines would work better

addPercent :: String -> String

addPercent (stripPrefix "instance " -> Just rest) = "%instance " ++ rest

addPercent s = s

getDecls :: String -> [String] -> IO ([Result As.Decl])

getDecls ns sl = do

fp <- compileMMTsrc ns $ map addPercent sl

-- read fp with MMT, produce xml file

MMT.callSpec fp

rsdcl <- XML.parse "MMTtemp/Spec.xml"

let decls = map decl2decl rsdcl

return decls

{- helper method that translates

parse tree declarations to logic declarations -}

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

decl2decl rs = let dcl = maybeResult rs

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