{- |

Module : $EmptyHeader$

Description : <optional short description entry>

Copyright : (c) <Authors or Affiliations>

License : GPLv2 or higher, see LICENSE.txt

Maintainer : <email>

Stability : unstable | experimental | provisional | stable | frozen

Portability : portable | non-portable (<reason>)

<optional description>

-}

module Main where

import Comorphisms.HetLogicGraph

import Comorphisms.LogicGraph

import Logic.Comorphism

import Logic.Logic

import Data.Maybe (catMaybes)

import qualified Data.Map as Map

main :: IO ()

main = do

testInj_mapSublogicAll

putStrLn ("Size of HetSublogicGraph (n,e): "++ show (size hetSublogicGraph))

size :: HetSublogicGraph -> (Int,Int)

size hsg = (Map.size $ sublogicNodes hsg,

Map.fold (\ x y -> length x + y) 0 $ comorphismEdges hsg)

testInj_mapSublogic :: (Comorphism cid

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

=> cid -> Bool

testInj_mapSublogic cid = and $

map (`elem` all_sublogics (targetLogic cid)) $ catMaybes $

map (mapSublogic cid) (all_sublogics $ sourceLogic cid)

testInj_mapSublogicAll :: IO ()

testInj_mapSublogicAll = do

putStrLn "Every Comorphism should be followed by True"

let testResults = map (\ (Comorphism c) -> testInj_mapSublogic c)

comorphismList

mapM_ showTest $ zip comorphismList testResults

putStrLn ("Test " ++ if and testResults then "succeeded." else "failed!")

where showTest (acm, res) = putStrLn (show acm ++ " : " ++ show res)