Hets - the Heterogeneous Tool Set

LicenseGPLv2 or higher, see LICENSE.txt
Maintainernevrenato@gmail.com
Stabilityexperimental
Portabilitynot portable
Safe HaskellNone

TopHybrid.StatAna

Contents

Description

Description : Static analysis of hybrid logic with an arbitrary logic below.

Synopsis

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.

Orphan instances

ShATermConvertible Spc_Wrap Source # 

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 # 

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 # 

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])