{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./LF/Sign.hs
Description :  Definition of signatures for the Edinburgh
               Logical Framework
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module LF.Sign
       ( VAR
       , NAME
       , MODULE
       , BASE
       , Symbol (..)
       , RAW_SYM
       , EXP (..)
       , Sentence
       , CONTEXT
       , DEF (..)
       , Sign (..)
       , isSym
       , toSym
       , gen_base
       , gen_module
       , emptySig
       , addDef
       , getSymbols
       , getDeclaredSyms
       , getDefinedSyms
       , getLocalSyms
       , getLocalDefs
       , getGlobalSyms
       , getGlobalDefs
       , isConstant
       , isDeclaredSym
       , isDefinedSym
       , isLocalSym
       , isGlobalSym
       , getSymType
       , getSymValue
       , getSymsOfType
       , getFreeVars
       , getConstants
       , recForm
       , isSubsig
       , sigUnion
       , sigIntersection
       , genSig
       , coGenSig
       ) where

import Common.Id
import Common.Doc
import Common.DocUtils
import Common.Result
import Common.Keywords

import Data.Data
import Data.Maybe
import Data.List
import qualified Data.Set as Set
import qualified Data.Map as Map

type VAR = String
type NAME = String
type MODULE = String
type BASE = String

gen_base :: String
gen_base :: String
gen_base = "gen_twelf_file.elf"

gen_module :: String
gen_module :: String
gen_module = "GEN_SIG"

data Symbol = Symbol
            { Symbol -> String
symBase :: BASE
            , Symbol -> String
symModule :: MODULE
            , Symbol -> String
symName :: NAME
            } deriving (Eq Symbol
Eq Symbol =>
(Symbol -> Symbol -> Ordering)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Symbol)
-> (Symbol -> Symbol -> Symbol)
-> Ord Symbol
Symbol -> Symbol -> Bool
Symbol -> Symbol -> Ordering
Symbol -> Symbol -> Symbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Symbol -> Symbol -> Symbol
$cmin :: Symbol -> Symbol -> Symbol
max :: Symbol -> Symbol -> Symbol
$cmax :: Symbol -> Symbol -> Symbol
>= :: Symbol -> Symbol -> Bool
$c>= :: Symbol -> Symbol -> Bool
> :: Symbol -> Symbol -> Bool
$c> :: Symbol -> Symbol -> Bool
<= :: Symbol -> Symbol -> Bool
$c<= :: Symbol -> Symbol -> Bool
< :: Symbol -> Symbol -> Bool
$c< :: Symbol -> Symbol -> Bool
compare :: Symbol -> Symbol -> Ordering
$ccompare :: Symbol -> Symbol -> Ordering
$cp1Ord :: Eq Symbol
Ord, Symbol -> Symbol -> Bool
(Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool) -> Eq Symbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c== :: Symbol -> Symbol -> Bool
Eq, Int -> Symbol -> ShowS
[Symbol] -> ShowS
Symbol -> String
(Int -> Symbol -> ShowS)
-> (Symbol -> String) -> ([Symbol] -> ShowS) -> Show Symbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Symbol] -> ShowS
$cshowList :: [Symbol] -> ShowS
show :: Symbol -> String
$cshow :: Symbol -> String
showsPrec :: Int -> Symbol -> ShowS
$cshowsPrec :: Int -> Symbol -> ShowS
Show, Typeable, Typeable Symbol
Constr
DataType
Typeable Symbol =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Symbol -> c Symbol)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Symbol)
-> (Symbol -> Constr)
-> (Symbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Symbol))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol))
-> ((forall b. Data b => b -> b) -> Symbol -> Symbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Symbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Symbol -> r)
-> (forall u. (forall d. Data d => d -> u) -> Symbol -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> Data Symbol
Symbol -> Constr
Symbol -> DataType
(forall b. Data b => b -> b) -> Symbol -> Symbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u
forall u. (forall d. Data d => d -> u) -> Symbol -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Symbol)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
$cSymbol :: Constr
$tSymbol :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapMp :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapM :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u
gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Symbol -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol
$cgmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Symbol)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Symbol)
dataTypeOf :: Symbol -> DataType
$cdataTypeOf :: Symbol -> DataType
toConstr :: Symbol -> Constr
$ctoConstr :: Symbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
$cp1Data :: Typeable Symbol
Data)

type RAW_SYM = String

instance GetRange Symbol

data EXP = Type
         | Var VAR
         | Const Symbol
         | Appl EXP [EXP]
         | Func [EXP] EXP
         | Pi CONTEXT EXP
         | Lamb CONTEXT EXP
           deriving (Eq EXP
Eq EXP =>
(EXP -> EXP -> Ordering)
-> (EXP -> EXP -> Bool)
-> (EXP -> EXP -> Bool)
-> (EXP -> EXP -> Bool)
-> (EXP -> EXP -> Bool)
-> (EXP -> EXP -> EXP)
-> (EXP -> EXP -> EXP)
-> Ord EXP
EXP -> EXP -> Bool
EXP -> EXP -> Ordering
EXP -> EXP -> EXP
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: EXP -> EXP -> EXP
$cmin :: EXP -> EXP -> EXP
max :: EXP -> EXP -> EXP
$cmax :: EXP -> EXP -> EXP
>= :: EXP -> EXP -> Bool
$c>= :: EXP -> EXP -> Bool
> :: EXP -> EXP -> Bool
$c> :: EXP -> EXP -> Bool
<= :: EXP -> EXP -> Bool
$c<= :: EXP -> EXP -> Bool
< :: EXP -> EXP -> Bool
$c< :: EXP -> EXP -> Bool
compare :: EXP -> EXP -> Ordering
$ccompare :: EXP -> EXP -> Ordering
$cp1Ord :: Eq EXP
Ord, Int -> EXP -> ShowS
[EXP] -> ShowS
EXP -> String
(Int -> EXP -> ShowS)
-> (EXP -> String) -> ([EXP] -> ShowS) -> Show EXP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EXP] -> ShowS
$cshowList :: [EXP] -> ShowS
show :: EXP -> String
$cshow :: EXP -> String
showsPrec :: Int -> EXP -> ShowS
$cshowsPrec :: Int -> EXP -> ShowS
Show, Typeable, Typeable EXP
Constr
DataType
Typeable EXP =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EXP -> c EXP)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EXP)
-> (EXP -> Constr)
-> (EXP -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EXP))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EXP))
-> ((forall b. Data b => b -> b) -> EXP -> EXP)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EXP -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EXP -> r)
-> (forall u. (forall d. Data d => d -> u) -> EXP -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> EXP -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EXP -> m EXP)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EXP -> m EXP)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EXP -> m EXP)
-> Data EXP
EXP -> Constr
EXP -> DataType
(forall b. Data b => b -> b) -> EXP -> EXP
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EXP -> c EXP
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EXP
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> EXP -> u
forall u. (forall d. Data d => d -> u) -> EXP -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EXP -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EXP -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EXP -> m EXP
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EXP -> m EXP
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EXP
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EXP -> c EXP
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EXP)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EXP)
$cLamb :: Constr
$cPi :: Constr
$cFunc :: Constr
$cAppl :: Constr
$cConst :: Constr
$cVar :: Constr
$cType :: Constr
$tEXP :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> EXP -> m EXP
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EXP -> m EXP
gmapMp :: (forall d. Data d => d -> m d) -> EXP -> m EXP
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EXP -> m EXP
gmapM :: (forall d. Data d => d -> m d) -> EXP -> m EXP
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EXP -> m EXP
gmapQi :: Int -> (forall d. Data d => d -> u) -> EXP -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EXP -> u
gmapQ :: (forall d. Data d => d -> u) -> EXP -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EXP -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EXP -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EXP -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EXP -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EXP -> r
gmapT :: (forall b. Data b => b -> b) -> EXP -> EXP
$cgmapT :: (forall b. Data b => b -> b) -> EXP -> EXP
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EXP)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EXP)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EXP)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EXP)
dataTypeOf :: EXP -> DataType
$cdataTypeOf :: EXP -> DataType
toConstr :: EXP -> Constr
$ctoConstr :: EXP -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EXP
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EXP
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EXP -> c EXP
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EXP -> c EXP
$cp1Data :: Typeable EXP
Data)

instance GetRange EXP

type Sentence = EXP

type CONTEXT = [(VAR, EXP)]

data DEF = Def
         { DEF -> Symbol
getSym :: Symbol
         , DEF -> EXP
getType :: EXP
         , DEF -> Maybe EXP
getValue :: Maybe EXP
         } deriving (DEF -> DEF -> Bool
(DEF -> DEF -> Bool) -> (DEF -> DEF -> Bool) -> Eq DEF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DEF -> DEF -> Bool
$c/= :: DEF -> DEF -> Bool
== :: DEF -> DEF -> Bool
$c== :: DEF -> DEF -> Bool
Eq, Eq DEF
Eq DEF =>
(DEF -> DEF -> Ordering)
-> (DEF -> DEF -> Bool)
-> (DEF -> DEF -> Bool)
-> (DEF -> DEF -> Bool)
-> (DEF -> DEF -> Bool)
-> (DEF -> DEF -> DEF)
-> (DEF -> DEF -> DEF)
-> Ord DEF
DEF -> DEF -> Bool
DEF -> DEF -> Ordering
DEF -> DEF -> DEF
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DEF -> DEF -> DEF
$cmin :: DEF -> DEF -> DEF
max :: DEF -> DEF -> DEF
$cmax :: DEF -> DEF -> DEF
>= :: DEF -> DEF -> Bool
$c>= :: DEF -> DEF -> Bool
> :: DEF -> DEF -> Bool
$c> :: DEF -> DEF -> Bool
<= :: DEF -> DEF -> Bool
$c<= :: DEF -> DEF -> Bool
< :: DEF -> DEF -> Bool
$c< :: DEF -> DEF -> Bool
compare :: DEF -> DEF -> Ordering
$ccompare :: DEF -> DEF -> Ordering
$cp1Ord :: Eq DEF
Ord, Int -> DEF -> ShowS
[DEF] -> ShowS
DEF -> String
(Int -> DEF -> ShowS)
-> (DEF -> String) -> ([DEF] -> ShowS) -> Show DEF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DEF] -> ShowS
$cshowList :: [DEF] -> ShowS
show :: DEF -> String
$cshow :: DEF -> String
showsPrec :: Int -> DEF -> ShowS
$cshowsPrec :: Int -> DEF -> ShowS
Show, Typeable, Typeable DEF
Constr
DataType
Typeable DEF =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DEF -> c DEF)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DEF)
-> (DEF -> Constr)
-> (DEF -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DEF))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DEF))
-> ((forall b. Data b => b -> b) -> DEF -> DEF)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DEF -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DEF -> r)
-> (forall u. (forall d. Data d => d -> u) -> DEF -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> DEF -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DEF -> m DEF)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DEF -> m DEF)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DEF -> m DEF)
-> Data DEF
DEF -> Constr
DEF -> DataType
(forall b. Data b => b -> b) -> DEF -> DEF
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DEF -> c DEF
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DEF
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DEF -> u
forall u. (forall d. Data d => d -> u) -> DEF -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DEF -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DEF -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DEF -> m DEF
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DEF -> m DEF
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DEF
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DEF -> c DEF
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DEF)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DEF)
$cDef :: Constr
$tDEF :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> DEF -> m DEF
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DEF -> m DEF
gmapMp :: (forall d. Data d => d -> m d) -> DEF -> m DEF
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DEF -> m DEF
gmapM :: (forall d. Data d => d -> m d) -> DEF -> m DEF
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DEF -> m DEF
gmapQi :: Int -> (forall d. Data d => d -> u) -> DEF -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DEF -> u
gmapQ :: (forall d. Data d => d -> u) -> DEF -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DEF -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DEF -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DEF -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DEF -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DEF -> r
gmapT :: (forall b. Data b => b -> b) -> DEF -> DEF
$cgmapT :: (forall b. Data b => b -> b) -> DEF -> DEF
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DEF)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DEF)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DEF)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DEF)
dataTypeOf :: DEF -> DataType
$cdataTypeOf :: DEF -> DataType
toConstr :: DEF -> Constr
$ctoConstr :: DEF -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DEF
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DEF
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DEF -> c DEF
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DEF -> c DEF
$cp1Data :: Typeable DEF
Data)

data Sign = Sign
          { Sign -> String
sigBase :: BASE
          , Sign -> String
sigModule :: MODULE
          , Sign -> [DEF]
getDefs :: [DEF]
          } deriving (Sign -> Sign -> Bool
(Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sign -> Sign -> Bool
$c/= :: Sign -> Sign -> Bool
== :: Sign -> Sign -> Bool
$c== :: Sign -> Sign -> Bool
Eq, Eq Sign
Eq Sign =>
(Sign -> Sign -> Ordering)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Sign)
-> (Sign -> Sign -> Sign)
-> Ord Sign
Sign -> Sign -> Bool
Sign -> Sign -> Ordering
Sign -> Sign -> Sign
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Sign -> Sign -> Sign
$cmin :: Sign -> Sign -> Sign
max :: Sign -> Sign -> Sign
$cmax :: Sign -> Sign -> Sign
>= :: Sign -> Sign -> Bool
$c>= :: Sign -> Sign -> Bool
> :: Sign -> Sign -> Bool
$c> :: Sign -> Sign -> Bool
<= :: Sign -> Sign -> Bool
$c<= :: Sign -> Sign -> Bool
< :: Sign -> Sign -> Bool
$c< :: Sign -> Sign -> Bool
compare :: Sign -> Sign -> Ordering
$ccompare :: Sign -> Sign -> Ordering
$cp1Ord :: Eq Sign
Ord, Int -> Sign -> ShowS
[Sign] -> ShowS
Sign -> String
(Int -> Sign -> ShowS)
-> (Sign -> String) -> ([Sign] -> ShowS) -> Show Sign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sign] -> ShowS
$cshowList :: [Sign] -> ShowS
show :: Sign -> String
$cshow :: Sign -> String
showsPrec :: Int -> Sign -> ShowS
$cshowsPrec :: Int -> Sign -> ShowS
Show, Typeable, Typeable Sign
Constr
DataType
Typeable Sign =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sign -> c Sign)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sign)
-> (Sign -> Constr)
-> (Sign -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sign))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign))
-> ((forall b. Data b => b -> b) -> Sign -> Sign)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sign -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> Data Sign
Sign -> Constr
Sign -> DataType
(forall b. Data b => b -> b) -> Sign -> Sign
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u
forall u. (forall d. Data d => d -> u) -> Sign -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sign)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
$cSign :: Constr
$tSign :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapMp :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapM :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u
gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sign -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign
$cgmapT :: (forall b. Data b => b -> b) -> Sign -> Sign
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sign)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sign)
dataTypeOf :: Sign -> DataType
$cdataTypeOf :: Sign -> DataType
toConstr :: Sign -> Constr
$ctoConstr :: Sign -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
$cp1Data :: Typeable Sign
Data)

emptySig :: Sign
emptySig :: Sign
emptySig = String -> String -> [DEF] -> Sign
Sign String
gen_base String
gen_module []

addDef :: DEF -> Sign -> Sign
addDef :: DEF -> Sign -> Sign
addDef d :: DEF
d (Sign b :: String
b m :: String
m ds :: [DEF]
ds) = String -> String -> [DEF] -> Sign
Sign String
b String
m ([DEF] -> Sign) -> [DEF] -> Sign
forall a b. (a -> b) -> a -> b
$ [DEF]
ds [DEF] -> [DEF] -> [DEF]
forall a. [a] -> [a] -> [a]
++ [DEF
d]

{- tests whether a raw symbol represents a valid identifier (True) or
   an expression (False) -}
isSym :: RAW_SYM -> Bool
isSym :: String -> Bool
isSym s :: String
s =
  let forbidden :: String
forbidden = String
whiteChars String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String
twelfDeclChars String -> ShowS
forall a. Eq a => [a] -> [a] -> [a]
\\ String
twelfSymChars)
  in String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> ShowS
forall a. Eq a => [a] -> [a] -> [a]
intersect String
s String
forbidden)

-- converts a raw symbol to a symbol; must be a valid identifier
toSym :: RAW_SYM -> Symbol
toSym :: String -> Symbol
toSym = String -> String -> String -> Symbol
Symbol String
gen_base String
gen_module

-- get the set of all symbols
getSymbols :: Sign -> Set.Set Symbol
getSymbols :: Sign -> Set Symbol
getSymbols (Sign _ _ ds :: [DEF]
ds) = [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
Set.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ (DEF -> Symbol) -> [DEF] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map DEF -> Symbol
getSym [DEF]
ds

-- checks if the symbol is defined or declared in the signature
isConstant :: Symbol -> Sign -> Bool
isConstant :: Symbol -> Sign -> Bool
isConstant s :: Symbol
s sig :: Sign
sig = Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
s (Set Symbol -> Bool) -> Set Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
getSymbols Sign
sig

-- get the set of declared symbols
getDeclaredSyms :: Sign -> Set.Set Symbol
getDeclaredSyms :: Sign -> Set Symbol
getDeclaredSyms (Sign _ _ ds :: [DEF]
ds) =
  [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
Set.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ (DEF -> Symbol) -> [DEF] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map DEF -> Symbol
getSym ([DEF] -> [Symbol]) -> [DEF] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe EXP -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe EXP -> Bool) -> (DEF -> Maybe EXP) -> DEF -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DEF -> Maybe EXP
getValue) [DEF]
ds

-- checks if the symbol is declared in the signature
isDeclaredSym :: Symbol -> Sign -> Bool
isDeclaredSym :: Symbol -> Sign -> Bool
isDeclaredSym s :: Symbol
s sig :: Sign
sig = Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
s (Set Symbol -> Bool) -> Set Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
getDeclaredSyms Sign
sig

-- get the set of declared symbols
getDefinedSyms :: Sign -> Set.Set Symbol
getDefinedSyms :: Sign -> Set Symbol
getDefinedSyms (Sign _ _ ds :: [DEF]
ds) =
  [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
Set.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ (DEF -> Symbol) -> [DEF] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map DEF -> Symbol
getSym ([DEF] -> [Symbol]) -> [DEF] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe EXP -> Bool
forall a. Maybe a -> Bool
isJust (Maybe EXP -> Bool) -> (DEF -> Maybe EXP) -> DEF -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DEF -> Maybe EXP
getValue) [DEF]
ds

-- checks if the symbol is defined in the signature
isDefinedSym :: Symbol -> Sign -> Bool
isDefinedSym :: Symbol -> Sign -> Bool
isDefinedSym s :: Symbol
s sig :: Sign
sig = Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
s (Set Symbol -> Bool) -> Set Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
getDefinedSyms Sign
sig

-- get the set of symbols not included from other signatures
getLocalSyms :: Sign -> Set.Set Symbol
getLocalSyms :: Sign -> Set Symbol
getLocalSyms sig :: Sign
sig = (Symbol -> Bool) -> Set Symbol -> Set Symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Symbol -> Sign -> Bool
`isLocalSym` Sign
sig) (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
getSymbols Sign
sig

-- checks if the symbol is local to the signature
isLocalSym :: Symbol -> Sign -> Bool
isLocalSym :: Symbol -> Sign -> Bool
isLocalSym s :: Symbol
s sig :: Sign
sig = Sign -> String
sigBase Sign
sig String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> String
symBase Symbol
s Bool -> Bool -> Bool
&& Sign -> String
sigModule Sign
sig String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> String
symModule Symbol
s

-- get the list of local definitions
getLocalDefs :: Sign -> [DEF]
getLocalDefs :: Sign -> [DEF]
getLocalDefs sig :: Sign
sig = (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Def s :: Symbol
s _ _) -> Symbol -> Sign -> Bool
isLocalSym Symbol
s Sign
sig) ([DEF] -> [DEF]) -> [DEF] -> [DEF]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig

-- get the set of symbols included from other signatures
getGlobalSyms :: Sign -> Set.Set Symbol
getGlobalSyms :: Sign -> Set Symbol
getGlobalSyms sig :: Sign
sig = (Symbol -> Bool) -> Set Symbol -> Set Symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Symbol -> Sign -> Bool
`isGlobalSym` Sign
sig) (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
getSymbols Sign
sig

-- checks if the symbol is global
isGlobalSym :: Symbol -> Sign -> Bool
isGlobalSym :: Symbol -> Sign -> Bool
isGlobalSym s :: Symbol
s sig :: Sign
sig = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> Sign -> Bool
isLocalSym Symbol
s Sign
sig

-- get the list of global definitions
getGlobalDefs :: Sign -> [DEF]
getGlobalDefs :: Sign -> [DEF]
getGlobalDefs sig :: Sign
sig = (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Def s :: Symbol
s _ _) -> Symbol -> Sign -> Bool
isGlobalSym Symbol
s Sign
sig) ([DEF] -> [DEF]) -> [DEF] -> [DEF]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig

-- returns the type/kind for the given symbol
getSymType :: Symbol -> Sign -> Maybe EXP
getSymType :: Symbol -> Sign -> Maybe EXP
getSymType sym :: Symbol
sym sig :: Sign
sig =
  let res :: Maybe DEF
res = (DEF -> Bool) -> [DEF] -> Maybe DEF
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ d :: DEF
d -> DEF -> Symbol
getSym DEF
d Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
sym) ([DEF] -> Maybe DEF) -> [DEF] -> Maybe DEF
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig
      in case Maybe DEF
res of
              Nothing -> Maybe EXP
forall a. Maybe a
Nothing
              Just (Def _ t :: EXP
t _) -> EXP -> Maybe EXP
forall a. a -> Maybe a
Just EXP
t

-- returns the value for the given symbol, if it exists
getSymValue :: Symbol -> Sign -> Maybe EXP
getSymValue :: Symbol -> Sign -> Maybe EXP
getSymValue sym :: Symbol
sym sig :: Sign
sig =
  let res :: Maybe DEF
res = (DEF -> Bool) -> [DEF] -> Maybe DEF
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ d :: DEF
d -> DEF -> Symbol
getSym DEF
d Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
sym) ([DEF] -> Maybe DEF) -> [DEF] -> Maybe DEF
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig
      in case Maybe DEF
res of
              Nothing -> Maybe EXP
forall a. Maybe a
Nothing
              Just (Def _ _ v :: Maybe EXP
v) -> Maybe EXP
v

-- returns the set of symbols of the given type
getSymsOfType :: EXP -> Sign -> Set.Set Symbol
getSymsOfType :: EXP -> Sign -> Set Symbol
getSymsOfType t :: EXP
t sig :: Sign
sig =
  [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
Set.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ (DEF -> Symbol) -> [DEF] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map DEF -> Symbol
getSym ([DEF] -> [Symbol]) -> [DEF] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Def _ t' :: EXP
t' _) -> EXP
t' EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
t) ([DEF] -> [DEF]) -> [DEF] -> [DEF]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig

-- pretty printing
instance Pretty Sign where
   pretty :: Sign -> Doc
pretty = Sign -> Doc
printSig
instance Pretty DEF where
   pretty :: DEF -> Doc
pretty = DEF -> Doc
printDef
instance Pretty EXP where
   pretty :: EXP -> Doc
pretty = EXP -> Doc
printExp
instance Pretty Symbol where
   pretty :: Symbol -> Doc
pretty = Symbol -> Doc
printSymbol

printSig :: Sign -> Doc
printSig :: Sign -> Doc
printSig sig :: Sign
sig = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (DEF -> Doc) -> [DEF] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DEF -> Doc
printDef (Sign -> [DEF]
getDefs Sign
sig)

printDef :: DEF -> Doc
printDef :: DEF -> Doc
printDef (Def s :: Symbol
s t :: EXP
t v :: Maybe EXP
v) =
  case Maybe EXP
v of
    Nothing -> [Doc] -> Doc
fsep [ Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s
                    , Doc
colon Doc -> Doc -> Doc
<+> EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
t Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot ]
    Just val :: EXP
val -> [Doc] -> Doc
fsep [ Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s
                     , Doc
colon Doc -> Doc -> Doc
<+> EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
t
                     , String -> Doc
text "=" Doc -> Doc -> Doc
<+> EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
val Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot ]

printSymbol :: Symbol -> Doc
printSymbol :: Symbol -> Doc
printSymbol s :: Symbol
s = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Symbol -> String
symName Symbol
s

printExp :: EXP -> Doc
printExp :: EXP -> Doc
printExp Type = String -> Doc
text "type"
printExp (Const s :: Symbol
s) = Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s
printExp (Var n :: String
n) = String -> Doc
text String
n
printExp (Appl e :: EXP
e es :: [EXP]
es) =
  let f :: Doc
f = Int -> EXP -> Doc
printExpWithPrec (Int
precAppl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) EXP
e
      as :: [Doc]
as = (EXP -> Doc) -> [EXP] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> EXP -> Doc
printExpWithPrec Int
precAppl) [EXP]
es
      in [Doc] -> Doc
hsep (Doc
f Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
as)
printExp (Func es :: [EXP]
es e :: EXP
e) =
  let as :: [Doc]
as = (EXP -> Doc) -> [EXP] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> EXP -> Doc
printExpWithPrec Int
precFunc) [EXP]
es
      val :: Doc
val = Int -> EXP -> Doc
printExpWithPrec (Int
precFunc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) EXP
e
      in [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text " ->") ([Doc]
as [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
val])
printExp (Pi ds :: CONTEXT
ds e :: EXP
e) = [Doc] -> Doc
sep [Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ CONTEXT -> Doc
printContext CONTEXT
ds, EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
e]
printExp (Lamb ds :: CONTEXT
ds e :: EXP
e) = [Doc] -> Doc
sep [Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ CONTEXT -> Doc
printContext CONTEXT
ds, EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
e]

printExpWithPrec :: Int -> EXP -> Doc
printExpWithPrec :: Int -> EXP -> Doc
printExpWithPrec i :: Int
i e :: EXP
e =
  if EXP -> Int
prec EXP
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
i
     then Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ EXP -> Doc
printExp EXP
e
     else EXP -> Doc
printExp EXP
e

prec :: EXP -> Int
prec :: EXP -> Int
prec Type = 0
prec Const {} = 0
prec Var {} = 0
prec Appl {} = 1
prec Func {} = 2
prec Pi {} = 3
prec Lamb {} = 3

precFunc, precAppl :: Int
precFunc :: Int
precFunc = 2
precAppl :: Int
precAppl = 1

printContext :: CONTEXT -> Doc
printContext :: CONTEXT -> Doc
printContext xs :: CONTEXT
xs = [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((String, EXP) -> Doc) -> CONTEXT -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, EXP) -> Doc
printVarDecl CONTEXT
xs

printVarDecl :: (VAR, EXP) -> Doc
printVarDecl :: (String, EXP) -> Doc
printVarDecl (n :: String
n, e :: EXP
e) = [Doc] -> Doc
sep [String -> Doc
text String
n, Doc
colon Doc -> Doc -> Doc
<+> EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
e]

{- converts the expression into a form where each construct takes
   exactly one argument -}
recForm :: EXP -> EXP
recForm :: EXP -> EXP
recForm (Appl f :: EXP
f []) = EXP -> EXP
recForm EXP
f
recForm (Appl f :: EXP
f as :: [EXP]
as) = EXP -> [EXP] -> EXP
Appl (EXP -> EXP
recForm (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ EXP -> [EXP] -> EXP
Appl EXP
f ([EXP] -> EXP) -> [EXP] -> EXP
forall a b. (a -> b) -> a -> b
$ [EXP] -> [EXP]
forall a. [a] -> [a]
init [EXP]
as) [EXP -> EXP
recForm (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ [EXP] -> EXP
forall a. [a] -> a
last [EXP]
as]
recForm (Func [] a :: EXP
a) = EXP -> EXP
recForm EXP
a
recForm (Func (t :: EXP
t : ts :: [EXP]
ts) a :: EXP
a) = [EXP] -> EXP -> EXP
Func [EXP -> EXP
recForm EXP
t] (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ EXP -> EXP
recForm (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ [EXP] -> EXP -> EXP
Func [EXP]
ts EXP
a
recForm (Pi [] t :: EXP
t) = EXP -> EXP
recForm EXP
t
recForm (Pi ((n :: String
n, t :: EXP
t) : ds :: CONTEXT
ds) a :: EXP
a) =
  CONTEXT -> EXP -> EXP
Pi [(String
n, EXP -> EXP
recForm EXP
t)] (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ EXP -> EXP
recForm (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ CONTEXT -> EXP -> EXP
Pi CONTEXT
ds EXP
a
recForm (Lamb [] t :: EXP
t) = EXP -> EXP
recForm EXP
t
recForm (Lamb ((n :: String
n, t :: EXP
t) : ds :: CONTEXT
ds) a :: EXP
a) =
  CONTEXT -> EXP -> EXP
Lamb [(String
n, EXP -> EXP
recForm EXP
t)] (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ EXP -> EXP
recForm (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ CONTEXT -> EXP -> EXP
Lamb CONTEXT
ds EXP
a
recForm t :: EXP
t = EXP
t

{- modifies the given name until it is different from each of the names
   in the input set -}
getNewName :: VAR -> Set.Set VAR -> VAR
getNewName :: String -> Set String -> String
getNewName var :: String
var names :: Set String
names = String -> Set String -> String -> Int -> String
getNewNameH String
var Set String
names String
var 0

getNewNameH :: VAR -> Set.Set VAR -> VAR -> Int -> VAR
getNewNameH :: String -> Set String -> String -> Int -> String
getNewNameH var :: String
var names :: Set String
names root :: String
root i :: Int
i =
  if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember String
var Set String
names
     then String
var
     else let newVar :: String
newVar = String
root String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
          in String -> Set String -> String -> Int -> String
getNewNameH String
newVar Set String
names String
root (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1

-- returns the set of free Variables used within an expression
getFreeVars :: EXP -> Set.Set VAR
getFreeVars :: EXP -> Set String
getFreeVars e :: EXP
e = EXP -> Set String
getFreeVarsH (EXP -> Set String) -> EXP -> Set String
forall a b. (a -> b) -> a -> b
$ EXP -> EXP
recForm EXP
e

getFreeVarsH :: EXP -> Set.Set VAR
getFreeVarsH :: EXP -> Set String
getFreeVarsH Type = Set String
forall a. Set a
Set.empty
getFreeVarsH (Const _) = Set String
forall a. Set a
Set.empty
getFreeVarsH (Var x :: String
x) = String -> Set String
forall a. a -> Set a
Set.singleton String
x
getFreeVarsH (Appl f :: EXP
f [a :: EXP
a]) =
  Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EXP -> Set String
getFreeVarsH EXP
f) (EXP -> Set String
getFreeVarsH EXP
a)
getFreeVarsH (Func [t :: EXP
t] v :: EXP
v) =
  Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EXP -> Set String
getFreeVarsH EXP
t) (EXP -> Set String
getFreeVarsH EXP
v)
getFreeVarsH (Pi [(n :: String
n, t :: EXP
t)] a :: EXP
a) =
  String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.delete String
n (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EXP -> Set String
getFreeVarsH EXP
t) (EXP -> Set String
getFreeVarsH EXP
a)
getFreeVarsH (Lamb [(n :: String
n, t :: EXP
t)] a :: EXP
a) =
  String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.delete String
n (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EXP -> Set String
getFreeVarsH EXP
t) (EXP -> Set String
getFreeVarsH EXP
a)
getFreeVarsH _ = Set String
forall a. Set a
Set.empty

-- returns the set of symbols used within an expression
getConstants :: EXP -> Set.Set Symbol
getConstants :: EXP -> Set Symbol
getConstants e :: EXP
e = EXP -> Set Symbol
getConstantsH (EXP -> Set Symbol) -> EXP -> Set Symbol
forall a b. (a -> b) -> a -> b
$ EXP -> EXP
recForm EXP
e

getConstantsH :: EXP -> Set.Set Symbol
getConstantsH :: EXP -> Set Symbol
getConstantsH Type = Set Symbol
forall a. Set a
Set.empty
getConstantsH (Const s :: Symbol
s) = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton Symbol
s
getConstantsH (Var _) = Set Symbol
forall a. Set a
Set.empty
getConstantsH (Appl f :: EXP
f [a :: EXP
a]) =
  Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EXP -> Set Symbol
getConstantsH EXP
f) (EXP -> Set Symbol
getConstantsH EXP
a)
getConstantsH (Func [t :: EXP
t] v :: EXP
v) =
  Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EXP -> Set Symbol
getConstantsH EXP
t) (EXP -> Set Symbol
getConstantsH EXP
v)
getConstantsH (Pi [(_, t :: EXP
t)] a :: EXP
a) =
  Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EXP -> Set Symbol
getConstantsH EXP
t) (EXP -> Set Symbol
getConstantsH EXP
a)
getConstantsH (Lamb [(_, t :: EXP
t)] a :: EXP
a) =
  Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EXP -> Set Symbol
getConstantsH EXP
t) (EXP -> Set Symbol
getConstantsH EXP
a)
getConstantsH _ = Set Symbol
forall a. Set a
Set.empty

{- Variable renamings:
   - the first argument specifies the desired variable renamings
   - the second argument specifies the set of variables which cannot
     be used as new variable names -}
rename :: Map.Map VAR VAR -> Set.Set VAR -> EXP -> EXP
rename :: Map String String -> Set String -> EXP -> EXP
rename m :: Map String String
m s :: Set String
s e :: EXP
e = Map String String -> Set String -> EXP -> EXP
renameH Map String String
m Set String
s (EXP -> EXP
recForm EXP
e)

renameH :: Map.Map VAR VAR -> Set.Set VAR -> EXP -> EXP
renameH :: Map String String -> Set String -> EXP -> EXP
renameH _ _ Type = EXP
Type
renameH _ _ (Const n :: Symbol
n) = Symbol -> EXP
Const Symbol
n
renameH m :: Map String String
m _ (Var n :: String
n) = String -> EXP
Var (String -> EXP) -> String -> EXP
forall a b. (a -> b) -> a -> b
$ String -> String -> Map String String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault String
n String
n Map String String
m
renameH m :: Map String String
m s :: Set String
s (Appl f :: EXP
f [a :: EXP
a]) = EXP -> [EXP] -> EXP
Appl (Map String String -> Set String -> EXP -> EXP
rename Map String String
m Set String
s EXP
f) [Map String String -> Set String -> EXP -> EXP
rename Map String String
m Set String
s EXP
a]
renameH m :: Map String String
m s :: Set String
s (Func [t :: EXP
t] u :: EXP
u) = [EXP] -> EXP -> EXP
Func [Map String String -> Set String -> EXP -> EXP
rename Map String String
m Set String
s EXP
t] (Map String String -> Set String -> EXP -> EXP
rename Map String String
m Set String
s EXP
u)
renameH m :: Map String String
m s :: Set String
s (Pi [(x :: String
x, t :: EXP
t)] a :: EXP
a) =
  let t1 :: EXP
t1 = Map String String -> Set String -> EXP -> EXP
rename Map String String
m Set String
s EXP
t
      x1 :: String
x1 = String -> Set String -> String
getNewName String
x Set String
s
      a1 :: EXP
a1 = Map String String -> Set String -> EXP -> EXP
rename (String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
x String
x1 Map String String
m) (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
x1 Set String
s) EXP
a
      in CONTEXT -> EXP -> EXP
Pi [(String
x1, EXP
t1)] EXP
a1
renameH m :: Map String String
m s :: Set String
s (Lamb [(x :: String
x, t :: EXP
t)] a :: EXP
a) =
  let t1 :: EXP
t1 = Map String String -> Set String -> EXP -> EXP
rename Map String String
m Set String
s EXP
t
      x1 :: String
x1 = String -> Set String -> String
getNewName String
x Set String
s
      a1 :: EXP
a1 = Map String String -> Set String -> EXP -> EXP
rename (String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
x String
x1 Map String String
m) (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
x1 Set String
s) EXP
a
      in CONTEXT -> EXP -> EXP
Lamb [(String
x1, EXP
t1)] EXP
a1
renameH _ _ t :: EXP
t = EXP
t

-- equality
instance Eq EXP where
    e1 :: EXP
e1 == :: EXP -> EXP -> Bool
== e2 :: EXP
e2 = EXP -> EXP -> Bool
eqExp (EXP -> EXP
recForm EXP
e1) (EXP -> EXP
recForm EXP
e2)

eqExp :: EXP -> EXP -> Bool
eqExp :: EXP -> EXP -> Bool
eqExp Type Type = Bool
True
eqExp (Const x1 :: Symbol
x1) (Const x2 :: Symbol
x2) = Symbol
x1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x2
eqExp (Var x1 :: String
x1) (Var x2 :: String
x2) = String
x1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
x2
eqExp (Appl f1 :: EXP
f1 [a1 :: EXP
a1]) (Appl f2 :: EXP
f2 [a2 :: EXP
a2]) = EXP
f1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
f2 Bool -> Bool -> Bool
&& EXP
a1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
a2
eqExp (Func [t1 :: EXP
t1] s1 :: EXP
s1) (Func [t2 :: EXP
t2] s2 :: EXP
s2) = EXP
t1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
t2 Bool -> Bool -> Bool
&& EXP
s1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
s2
eqExp (Pi [(n1 :: String
n1, t1 :: EXP
t1)] s1 :: EXP
s1) (Pi [(n2 :: String
n2, t2 :: EXP
t2)] s2 :: EXP
s2) =
  let vars :: Set String
vars = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.delete String
n1 (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ EXP -> Set String
getFreeVars EXP
s1
      vars1 :: Set String
vars1 = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.delete String
n2 (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ EXP -> Set String
getFreeVars EXP
s2
      in Set String
vars1 Set String -> Set String -> Bool
forall a. Eq a => a -> a -> Bool
== Set String
vars Bool -> Bool -> Bool
&&
          let s3 :: EXP
s3 = Map String String -> Set String -> EXP -> EXP
rename (String -> String -> Map String String
forall k a. k -> a -> Map k a
Map.singleton String
n2 String
n1) (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
n1 Set String
vars) EXP
s2
          in EXP
t1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
t2 Bool -> Bool -> Bool
&& EXP
s1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
s3
eqExp (Lamb [(n1 :: String
n1, t1 :: EXP
t1)] s1 :: EXP
s1) (Lamb [(n2 :: String
n2, t2 :: EXP
t2)] s2 :: EXP
s2) =
  let vars :: Set String
vars = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.delete String
n1 (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ EXP -> Set String
getFreeVars EXP
s1
      vars1 :: Set String
vars1 = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.delete String
n2 (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ EXP -> Set String
getFreeVars EXP
s2
      in Set String
vars1 Set String -> Set String -> Bool
forall a. Eq a => a -> a -> Bool
== Set String
vars Bool -> Bool -> Bool
&&
          let s3 :: EXP
s3 = Map String String -> Set String -> EXP -> EXP
rename (String -> String -> Map String String
forall k a. k -> a -> Map k a
Map.singleton String
n2 String
n1) (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
n1 Set String
vars) EXP
s2
          in EXP
t1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
t2 Bool -> Bool -> Bool
&& EXP
s1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
s3
eqExp _ _ = Bool
False

-- tests for inclusion of signatures
isSubsig :: Sign -> Sign -> Bool
isSubsig :: Sign -> Sign -> Bool
isSubsig (Sign _ _ ds1 :: [DEF]
ds1) (Sign _ _ ds2 :: [DEF]
ds2) =
  Set DEF -> Set DEF -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf ([DEF] -> Set DEF
forall a. Ord a => [a] -> Set a
Set.fromList [DEF]
ds1) ([DEF] -> Set DEF
forall a. Ord a => [a] -> Set a
Set.fromList [DEF]
ds2)

-- constructs the union of two signatures
sigUnion :: Sign -> Sign -> Result Sign
sigUnion :: Sign -> Sign -> Result Sign
sigUnion sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$
  (Sign -> DEF -> Sign) -> Sign -> [DEF] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ sig :: Sign
sig d :: DEF
d@(Def s :: Symbol
s t :: EXP
t v :: Maybe EXP
v) ->
           if Symbol -> Sign -> Bool
isConstant Symbol
s Sign
sig
              then let Just t1 :: EXP
t1 = Symbol -> Sign -> Maybe EXP
getSymType Symbol
s Sign
sig
                       v1 :: Maybe EXP
v1 = Symbol -> Sign -> Maybe EXP
getSymValue Symbol
s Sign
sig
                       in if EXP
t EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
t1 Bool -> Bool -> Bool
&& Maybe EXP
v Maybe EXP -> Maybe EXP -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe EXP
v1 then Sign
sig else
                             String -> Sign
forall a. HasCallStack => String -> a
error (String -> Sign) -> String -> Sign
forall a b. (a -> b) -> a -> b
$ Symbol -> String
conflictDefsError Symbol
s
              else DEF -> Sign -> Sign
addDef DEF
d Sign
sig
        ) Sign
sig1 ([DEF] -> Sign) -> [DEF] -> Sign
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig2

-- constructs the intersection of two signatures
sigIntersection :: Sign -> Sign -> Result Sign
sigIntersection :: Sign -> Sign -> Result Sign
sigIntersection sig1 :: Sign
sig1 sig2 :: Sign
sig2 = do
  let defs1 :: Set DEF
defs1 = [DEF] -> Set DEF
forall a. Ord a => [a] -> Set a
Set.fromList ([DEF] -> Set DEF) -> [DEF] -> Set DEF
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig1
  let defs2 :: Set DEF
defs2 = [DEF] -> Set DEF
forall a. Ord a => [a] -> Set a
Set.fromList ([DEF] -> Set DEF) -> [DEF] -> Set DEF
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig2
  let defs :: Set DEF
defs = Set DEF -> Set DEF -> Set DEF
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set DEF
defs1 Set DEF
defs2
  let syms :: Set Symbol
syms = (DEF -> Symbol) -> Set DEF -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map DEF -> Symbol
getSym Set DEF
defs
  Set Symbol -> Sign -> Result Sign
coGenSig Set Symbol
syms Sign
sig1

-- constructs the signature generated by the specified symbol set
genSig :: Set.Set Symbol -> Sign -> Result Sign
genSig :: Set Symbol -> Sign -> Result Sign
genSig syms :: Set Symbol
syms sig :: Sign
sig = do
  let syms' :: Set Symbol
syms' = Set Symbol -> Sign -> Set Symbol
inclSyms Set Symbol
syms Sign
sig
  let defs' :: [DEF]
defs' = (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ d :: DEF
d -> Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (DEF -> Symbol
getSym DEF
d) Set Symbol
syms') ([DEF] -> [DEF]) -> [DEF] -> [DEF]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig
  Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ String -> String -> [DEF] -> Sign
Sign String
gen_base String
gen_module [DEF]
defs'

inclSyms :: Set.Set Symbol -> Sign -> Set.Set Symbol
inclSyms :: Set Symbol -> Sign -> Set Symbol
inclSyms syms :: Set Symbol
syms sig :: Sign
sig =
  (Set Symbol -> DEF -> Set Symbol)
-> Set Symbol -> [DEF] -> Set Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ syms' :: Set Symbol
syms' (Def s :: Symbol
s t :: EXP
t v :: Maybe EXP
v) ->
           if Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Symbol
s Set Symbol
syms' then Set Symbol
syms' else
              let syms1 :: Set Symbol
syms1 = EXP -> Set Symbol
getConstants EXP
t
                  syms2 :: Set Symbol
syms2 = case Maybe EXP
v of
                            Nothing -> Set Symbol
forall a. Set a
Set.empty
                            Just v' :: EXP
v' -> EXP -> Set Symbol
getConstants EXP
v'
                  in Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Symbol
syms' (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Symbol
syms1 Set Symbol
syms2
        ) Set Symbol
syms ([DEF] -> Set Symbol) -> [DEF] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ [DEF] -> [DEF]
forall a. [a] -> [a]
reverse ([DEF] -> [DEF]) -> [DEF] -> [DEF]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig

-- constructs the signature cogenerated by the specified symbol set
coGenSig :: Set.Set Symbol -> Sign -> Result Sign
coGenSig :: Set Symbol -> Sign -> Result Sign
coGenSig syms :: Set Symbol
syms sig :: Sign
sig = do
  let syms' :: Set Symbol
syms' = Set Symbol -> Sign -> Set Symbol
exclSyms Set Symbol
syms Sign
sig
  let defs' :: [DEF]
defs' = (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ d :: DEF
d -> Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember (DEF -> Symbol
getSym DEF
d) Set Symbol
syms') ([DEF] -> [DEF]) -> [DEF] -> [DEF]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig
  Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ String -> String -> [DEF] -> Sign
Sign String
gen_base String
gen_module [DEF]
defs'

exclSyms :: Set.Set Symbol -> Sign -> Set.Set Symbol
exclSyms :: Set Symbol -> Sign -> Set Symbol
exclSyms syms :: Set Symbol
syms sig :: Sign
sig =
  (Set Symbol -> DEF -> Set Symbol)
-> Set Symbol -> [DEF] -> Set Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ syms' :: Set Symbol
syms' (Def s :: Symbol
s t :: EXP
t v :: Maybe EXP
v) ->
           if Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
s Set Symbol
syms' then Set Symbol
syms' else
              let syms1 :: Set Symbol
syms1 = EXP -> Set Symbol
getConstants EXP
t
                  syms2 :: Set Symbol
syms2 = case Maybe EXP
v of
                            Nothing -> Set Symbol
forall a. Set a
Set.empty
                            Just v' :: EXP
v' -> EXP -> Set Symbol
getConstants EXP
v'
                  diff :: Set Symbol
diff = Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Symbol
syms' (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Symbol
syms1 Set Symbol
syms2
                  in if Set Symbol -> Bool
forall a. Set a -> Bool
Set.null Set Symbol
diff then Set Symbol
syms' else Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
s Set Symbol
syms'
        ) Set Symbol
syms ([DEF] -> Set Symbol) -> [DEF] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig

{- ------------------------------------------------------------------
------------------------------------------------------------------- -}

-- ERROR MESSAGES
conflictDefsError :: Symbol -> String
conflictDefsError :: Symbol -> String
conflictDefsError s :: Symbol
s =
  "Symbol " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " has conflicting declarations " String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "in the signature union and hence the union is not defined."