License	GPLv2 or higher, see LICENSE.txt
Maintainer	nevrenato@gmail.com
Stability	experimental
Portability	not portable
Safe Haskell	None

TopHybrid.StatAna

Contents

Orphan instances

Description

Static analysis of hybrid logic with an arbitrary logic below.

Synopsis

thAna :: (Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])
anaForm' :: (Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap
simSen :: Sgn_Wrap -> Frm_Wrap -> Frm_Wrap

Documentation

thAna :: (Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]) Source #

Examining the list of formulas and collecting results

Analyses first the underlying spec; Then analyses the top spec (without the axioms) and merges the resulting sig with the underlying one. Also translates the underlying axioms into hybridized ones, so that in the end all axioms are of the same type; Next analyses the hybrid axioms and puts them together with the already translated axioms. Finnaly prepares the tuple format for outputting.

anaForm' :: (Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap Source #

simSen :: Sgn_Wrap -> Frm_Wrap -> Frm_Wrap Source #

Orphan instances

FromJSON Spc_Wrap Source #
Instance details Methods parseJSON :: Value -> Parser Spc_Wrap parseJSONList :: Value -> Parser [Spc_Wrap]
FromJSON Frm_Wrap Source #
Instance details Methods parseJSON :: Value -> Parser Frm_Wrap parseJSONList :: Value -> Parser [Frm_Wrap]
FromJSON Sgn_Wrap Source #
Instance details Methods parseJSON :: Value -> Parser Sgn_Wrap parseJSONList :: Value -> Parser [Sgn_Wrap]
ToJSON Spc_Wrap Source #
Instance details Methods toJSON :: Spc_Wrap -> Value toEncoding :: Spc_Wrap -> Encoding toJSONList :: [Spc_Wrap] -> Value toEncodingList :: [Spc_Wrap] -> Encoding
ToJSON Frm_Wrap Source #
Instance details Methods toJSON :: Frm_Wrap -> Value toEncoding :: Frm_Wrap -> Encoding toJSONList :: [Frm_Wrap] -> Value toEncodingList :: [Frm_Wrap] -> Encoding
ToJSON Sgn_Wrap Source #
Instance details Methods toJSON :: Sgn_Wrap -> Value toEncoding :: Sgn_Wrap -> Encoding toJSONList :: [Sgn_Wrap] -> Value toEncodingList :: [Sgn_Wrap] -> Encoding
ShATermConvertible Spc_Wrap Source #
Instance details Methods toShATermAux :: ATermTable -> Spc_Wrap -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Spc_Wrap] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Spc_Wrap) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Spc_Wrap])
ShATermConvertible Frm_Wrap Source #
Instance details Methods toShATermAux :: ATermTable -> Frm_Wrap -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Frm_Wrap] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Frm_Wrap) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Frm_Wrap])
ShATermConvertible Sgn_Wrap Source #
Instance details Methods toShATermAux :: ATermTable -> Sgn_Wrap -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sgn_Wrap] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sgn_Wrap) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sgn_Wrap])