{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./DFOL/AS_DFOL.hs
Description :  Abstract syntax for first-order logic with dependent types (DFOL)
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 DFOL.AS_DFOL
  ( NAME
  , DECL
  , SDECL
  , BASIC_SPEC (..)
  , BASIC_ITEM (..)
  , TYPE (..)
  , TERM (..)
  , FORMULA (..)
  , SYMB
  , SYMB_ITEMS (..)
  , SYMB_MAP_ITEMS (..)
  , SYMB_OR_MAP (..)
  , termRecForm
  , termFlatForm
  , typeRecForm
  , typeFlatForm
  , formulaRecForm
  , formulaFlatForm
  , printNames
  , printDecls
  , getVarsFromDecls
  , getVarTypeFromDecls
  , compactDecls
  , expandDecls
  , Translatable (translate)
  , getNewName
  , getFreeVars
  ) where

import Common.AS_Annotation
import Common.Id
import Common.Doc
import Common.DocUtils

import DFOL.Utils

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

type NAME = Token
type DECL = ([NAME], TYPE)
type SDECL = (NAME, TYPE)

-- grammar for basic specification
data BASIC_SPEC = Basic_spec [Annoted BASIC_ITEM]
                  deriving (Int -> BASIC_SPEC -> ShowS
[BASIC_SPEC] -> ShowS
BASIC_SPEC -> String
(Int -> BASIC_SPEC -> ShowS)
-> (BASIC_SPEC -> String)
-> ([BASIC_SPEC] -> ShowS)
-> Show BASIC_SPEC
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BASIC_SPEC] -> ShowS
$cshowList :: [BASIC_SPEC] -> ShowS
show :: BASIC_SPEC -> String
$cshow :: BASIC_SPEC -> String
showsPrec :: Int -> BASIC_SPEC -> ShowS
$cshowsPrec :: Int -> BASIC_SPEC -> ShowS
Show, Typeable)

instance GetRange BASIC_SPEC

data BASIC_ITEM = Decl_item DECL
                | Axiom_item FORMULA
                  deriving (Int -> BASIC_ITEM -> ShowS
[BASIC_ITEM] -> ShowS
BASIC_ITEM -> String
(Int -> BASIC_ITEM -> ShowS)
-> (BASIC_ITEM -> String)
-> ([BASIC_ITEM] -> ShowS)
-> Show BASIC_ITEM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BASIC_ITEM] -> ShowS
$cshowList :: [BASIC_ITEM] -> ShowS
show :: BASIC_ITEM -> String
$cshow :: BASIC_ITEM -> String
showsPrec :: Int -> BASIC_ITEM -> ShowS
$cshowsPrec :: Int -> BASIC_ITEM -> ShowS
Show, Typeable)

data TYPE = Sort
          | Form
          | Univ TERM
          | Func [TYPE] TYPE
          | Pi [DECL] TYPE
            deriving (Int -> TYPE -> ShowS
[TYPE] -> ShowS
TYPE -> String
(Int -> TYPE -> ShowS)
-> (TYPE -> String) -> ([TYPE] -> ShowS) -> Show TYPE
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TYPE] -> ShowS
$cshowList :: [TYPE] -> ShowS
show :: TYPE -> String
$cshow :: TYPE -> String
showsPrec :: Int -> TYPE -> ShowS
$cshowsPrec :: Int -> TYPE -> ShowS
Show, Eq TYPE
Eq TYPE =>
(TYPE -> TYPE -> Ordering)
-> (TYPE -> TYPE -> Bool)
-> (TYPE -> TYPE -> Bool)
-> (TYPE -> TYPE -> Bool)
-> (TYPE -> TYPE -> Bool)
-> (TYPE -> TYPE -> TYPE)
-> (TYPE -> TYPE -> TYPE)
-> Ord TYPE
TYPE -> TYPE -> Bool
TYPE -> TYPE -> Ordering
TYPE -> TYPE -> TYPE
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 :: TYPE -> TYPE -> TYPE
$cmin :: TYPE -> TYPE -> TYPE
max :: TYPE -> TYPE -> TYPE
$cmax :: TYPE -> TYPE -> TYPE
>= :: TYPE -> TYPE -> Bool
$c>= :: TYPE -> TYPE -> Bool
> :: TYPE -> TYPE -> Bool
$c> :: TYPE -> TYPE -> Bool
<= :: TYPE -> TYPE -> Bool
$c<= :: TYPE -> TYPE -> Bool
< :: TYPE -> TYPE -> Bool
$c< :: TYPE -> TYPE -> Bool
compare :: TYPE -> TYPE -> Ordering
$ccompare :: TYPE -> TYPE -> Ordering
$cp1Ord :: Eq TYPE
Ord, Typeable, Typeable TYPE
Constr
DataType
Typeable TYPE =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TYPE -> c TYPE)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TYPE)
-> (TYPE -> Constr)
-> (TYPE -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TYPE))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TYPE))
-> ((forall b. Data b => b -> b) -> TYPE -> TYPE)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r)
-> (forall u. (forall d. Data d => d -> u) -> TYPE -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TYPE -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TYPE -> m TYPE)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TYPE -> m TYPE)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TYPE -> m TYPE)
-> Data TYPE
TYPE -> Constr
TYPE -> DataType
(forall b. Data b => b -> b) -> TYPE -> TYPE
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TYPE -> c TYPE
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TYPE
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) -> TYPE -> u
forall u. (forall d. Data d => d -> u) -> TYPE -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TYPE -> m TYPE
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TYPE -> m TYPE
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TYPE
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TYPE -> c TYPE
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TYPE)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TYPE)
$cPi :: Constr
$cFunc :: Constr
$cUniv :: Constr
$cForm :: Constr
$cSort :: Constr
$tTYPE :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TYPE -> m TYPE
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TYPE -> m TYPE
gmapMp :: (forall d. Data d => d -> m d) -> TYPE -> m TYPE
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TYPE -> m TYPE
gmapM :: (forall d. Data d => d -> m d) -> TYPE -> m TYPE
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TYPE -> m TYPE
gmapQi :: Int -> (forall d. Data d => d -> u) -> TYPE -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TYPE -> u
gmapQ :: (forall d. Data d => d -> u) -> TYPE -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TYPE -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r
gmapT :: (forall b. Data b => b -> b) -> TYPE -> TYPE
$cgmapT :: (forall b. Data b => b -> b) -> TYPE -> TYPE
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TYPE)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TYPE)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TYPE)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TYPE)
dataTypeOf :: TYPE -> DataType
$cdataTypeOf :: TYPE -> DataType
toConstr :: TYPE -> Constr
$ctoConstr :: TYPE -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TYPE
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TYPE
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TYPE -> c TYPE
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TYPE -> c TYPE
$cp1Data :: Typeable TYPE
Data)

data TERM = Identifier NAME
          | Appl TERM [TERM]
            deriving (Int -> TERM -> ShowS
[TERM] -> ShowS
TERM -> String
(Int -> TERM -> ShowS)
-> (TERM -> String) -> ([TERM] -> ShowS) -> Show TERM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TERM] -> ShowS
$cshowList :: [TERM] -> ShowS
show :: TERM -> String
$cshow :: TERM -> String
showsPrec :: Int -> TERM -> ShowS
$cshowsPrec :: Int -> TERM -> ShowS
Show, Eq TERM
Eq TERM =>
(TERM -> TERM -> Ordering)
-> (TERM -> TERM -> Bool)
-> (TERM -> TERM -> Bool)
-> (TERM -> TERM -> Bool)
-> (TERM -> TERM -> Bool)
-> (TERM -> TERM -> TERM)
-> (TERM -> TERM -> TERM)
-> Ord TERM
TERM -> TERM -> Bool
TERM -> TERM -> Ordering
TERM -> TERM -> TERM
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 :: TERM -> TERM -> TERM
$cmin :: TERM -> TERM -> TERM
max :: TERM -> TERM -> TERM
$cmax :: TERM -> TERM -> TERM
>= :: TERM -> TERM -> Bool
$c>= :: TERM -> TERM -> Bool
> :: TERM -> TERM -> Bool
$c> :: TERM -> TERM -> Bool
<= :: TERM -> TERM -> Bool
$c<= :: TERM -> TERM -> Bool
< :: TERM -> TERM -> Bool
$c< :: TERM -> TERM -> Bool
compare :: TERM -> TERM -> Ordering
$ccompare :: TERM -> TERM -> Ordering
$cp1Ord :: Eq TERM
Ord, Typeable, Typeable TERM
Constr
DataType
Typeable TERM =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TERM -> c TERM)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TERM)
-> (TERM -> Constr)
-> (TERM -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TERM))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TERM))
-> ((forall b. Data b => b -> b) -> TERM -> TERM)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r)
-> (forall u. (forall d. Data d => d -> u) -> TERM -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TERM -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TERM -> m TERM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TERM -> m TERM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TERM -> m TERM)
-> Data TERM
TERM -> Constr
TERM -> DataType
(forall b. Data b => b -> b) -> TERM -> TERM
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TERM -> c TERM
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TERM
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) -> TERM -> u
forall u. (forall d. Data d => d -> u) -> TERM -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TERM -> m TERM
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TERM -> m TERM
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TERM
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TERM -> c TERM
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TERM)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TERM)
$cAppl :: Constr
$cIdentifier :: Constr
$tTERM :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TERM -> m TERM
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TERM -> m TERM
gmapMp :: (forall d. Data d => d -> m d) -> TERM -> m TERM
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TERM -> m TERM
gmapM :: (forall d. Data d => d -> m d) -> TERM -> m TERM
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TERM -> m TERM
gmapQi :: Int -> (forall d. Data d => d -> u) -> TERM -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TERM -> u
gmapQ :: (forall d. Data d => d -> u) -> TERM -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TERM -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r
gmapT :: (forall b. Data b => b -> b) -> TERM -> TERM
$cgmapT :: (forall b. Data b => b -> b) -> TERM -> TERM
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TERM)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TERM)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TERM)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TERM)
dataTypeOf :: TERM -> DataType
$cdataTypeOf :: TERM -> DataType
toConstr :: TERM -> Constr
$ctoConstr :: TERM -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TERM
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TERM
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TERM -> c TERM
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TERM -> c TERM
$cp1Data :: Typeable TERM
Data)

data FORMULA = T
             | F
             | Pred TERM
             | Equality TERM TERM
             | Negation FORMULA
             | Conjunction [FORMULA]
             | Disjunction [FORMULA]
             | Implication FORMULA FORMULA
             | Equivalence FORMULA FORMULA
             | Forall [DECL] FORMULA
             | Exists [DECL] FORMULA
               deriving (Int -> FORMULA -> ShowS
[FORMULA] -> ShowS
FORMULA -> String
(Int -> FORMULA -> ShowS)
-> (FORMULA -> String) -> ([FORMULA] -> ShowS) -> Show FORMULA
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FORMULA] -> ShowS
$cshowList :: [FORMULA] -> ShowS
show :: FORMULA -> String
$cshow :: FORMULA -> String
showsPrec :: Int -> FORMULA -> ShowS
$cshowsPrec :: Int -> FORMULA -> ShowS
Show, Eq FORMULA
Eq FORMULA =>
(FORMULA -> FORMULA -> Ordering)
-> (FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> FORMULA)
-> (FORMULA -> FORMULA -> FORMULA)
-> Ord FORMULA
FORMULA -> FORMULA -> Bool
FORMULA -> FORMULA -> Ordering
FORMULA -> FORMULA -> FORMULA
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 :: FORMULA -> FORMULA -> FORMULA
$cmin :: FORMULA -> FORMULA -> FORMULA
max :: FORMULA -> FORMULA -> FORMULA
$cmax :: FORMULA -> FORMULA -> FORMULA
>= :: FORMULA -> FORMULA -> Bool
$c>= :: FORMULA -> FORMULA -> Bool
> :: FORMULA -> FORMULA -> Bool
$c> :: FORMULA -> FORMULA -> Bool
<= :: FORMULA -> FORMULA -> Bool
$c<= :: FORMULA -> FORMULA -> Bool
< :: FORMULA -> FORMULA -> Bool
$c< :: FORMULA -> FORMULA -> Bool
compare :: FORMULA -> FORMULA -> Ordering
$ccompare :: FORMULA -> FORMULA -> Ordering
$cp1Ord :: Eq FORMULA
Ord, FORMULA -> FORMULA -> Bool
(FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> Bool) -> Eq FORMULA
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FORMULA -> FORMULA -> Bool
$c/= :: FORMULA -> FORMULA -> Bool
== :: FORMULA -> FORMULA -> Bool
$c== :: FORMULA -> FORMULA -> Bool
Eq, Typeable, Typeable FORMULA
Constr
DataType
Typeable FORMULA =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FORMULA -> c FORMULA)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FORMULA)
-> (FORMULA -> Constr)
-> (FORMULA -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FORMULA))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA))
-> ((forall b. Data b => b -> b) -> FORMULA -> FORMULA)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FORMULA -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FORMULA -> r)
-> (forall u. (forall d. Data d => d -> u) -> FORMULA -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FORMULA -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA)
-> Data FORMULA
FORMULA -> Constr
FORMULA -> DataType
(forall b. Data b => b -> b) -> FORMULA -> FORMULA
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FORMULA -> c FORMULA
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FORMULA
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) -> FORMULA -> u
forall u. (forall d. Data d => d -> u) -> FORMULA -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FORMULA
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FORMULA -> c FORMULA
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FORMULA)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA)
$cExists :: Constr
$cForall :: Constr
$cEquivalence :: Constr
$cImplication :: Constr
$cDisjunction :: Constr
$cConjunction :: Constr
$cNegation :: Constr
$cEquality :: Constr
$cPred :: Constr
$cF :: Constr
$cT :: Constr
$tFORMULA :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
gmapMp :: (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
gmapM :: (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
gmapQi :: Int -> (forall d. Data d => d -> u) -> FORMULA -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FORMULA -> u
gmapQ :: (forall d. Data d => d -> u) -> FORMULA -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FORMULA -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
gmapT :: (forall b. Data b => b -> b) -> FORMULA -> FORMULA
$cgmapT :: (forall b. Data b => b -> b) -> FORMULA -> FORMULA
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FORMULA)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FORMULA)
dataTypeOf :: FORMULA -> DataType
$cdataTypeOf :: FORMULA -> DataType
toConstr :: FORMULA -> Constr
$ctoConstr :: FORMULA -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FORMULA
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FORMULA
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FORMULA -> c FORMULA
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FORMULA -> c FORMULA
$cp1Data :: Typeable FORMULA
Data)

instance GetRange FORMULA

-- grammar for symbols and symbol maps
type SYMB = NAME

data SYMB_ITEMS = Symb_items [SYMB]
                  deriving (Int -> SYMB_ITEMS -> ShowS
[SYMB_ITEMS] -> ShowS
SYMB_ITEMS -> String
(Int -> SYMB_ITEMS -> ShowS)
-> (SYMB_ITEMS -> String)
-> ([SYMB_ITEMS] -> ShowS)
-> Show SYMB_ITEMS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SYMB_ITEMS] -> ShowS
$cshowList :: [SYMB_ITEMS] -> ShowS
show :: SYMB_ITEMS -> String
$cshow :: SYMB_ITEMS -> String
showsPrec :: Int -> SYMB_ITEMS -> ShowS
$cshowsPrec :: Int -> SYMB_ITEMS -> ShowS
Show, SYMB_ITEMS -> SYMB_ITEMS -> Bool
(SYMB_ITEMS -> SYMB_ITEMS -> Bool)
-> (SYMB_ITEMS -> SYMB_ITEMS -> Bool) -> Eq SYMB_ITEMS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c/= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
== :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c== :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
Eq, Typeable, Typeable SYMB_ITEMS
Constr
DataType
Typeable SYMB_ITEMS =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS)
-> (SYMB_ITEMS -> Constr)
-> (SYMB_ITEMS -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SYMB_ITEMS))
-> ((forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r)
-> (forall u. (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS)
-> Data SYMB_ITEMS
SYMB_ITEMS -> Constr
SYMB_ITEMS -> DataType
(forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS
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) -> SYMB_ITEMS -> u
forall u. (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)
$cSymb_items :: Constr
$tSYMB_ITEMS :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
gmapMp :: (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
gmapM :: (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u
gmapQ :: (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
gmapT :: (forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS
$cgmapT :: (forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)
dataTypeOf :: SYMB_ITEMS -> DataType
$cdataTypeOf :: SYMB_ITEMS -> DataType
toConstr :: SYMB_ITEMS -> Constr
$ctoConstr :: SYMB_ITEMS -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS
$cp1Data :: Typeable SYMB_ITEMS
Data)

data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP]
                      deriving (Int -> SYMB_MAP_ITEMS -> ShowS
[SYMB_MAP_ITEMS] -> ShowS
SYMB_MAP_ITEMS -> String
(Int -> SYMB_MAP_ITEMS -> ShowS)
-> (SYMB_MAP_ITEMS -> String)
-> ([SYMB_MAP_ITEMS] -> ShowS)
-> Show SYMB_MAP_ITEMS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SYMB_MAP_ITEMS] -> ShowS
$cshowList :: [SYMB_MAP_ITEMS] -> ShowS
show :: SYMB_MAP_ITEMS -> String
$cshow :: SYMB_MAP_ITEMS -> String
showsPrec :: Int -> SYMB_MAP_ITEMS -> ShowS
$cshowsPrec :: Int -> SYMB_MAP_ITEMS -> ShowS
Show, SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
(SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool)
-> (SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool) -> Eq SYMB_MAP_ITEMS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
$c/= :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
== :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
$c== :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
Eq, Typeable, Typeable SYMB_MAP_ITEMS
Constr
DataType
Typeable SYMB_MAP_ITEMS =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMS)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMS)
-> (SYMB_MAP_ITEMS -> Constr)
-> (SYMB_MAP_ITEMS -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SYMB_MAP_ITEMS))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SYMB_MAP_ITEMS))
-> ((forall b. Data b => b -> b)
    -> SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS)
-> Data SYMB_MAP_ITEMS
SYMB_MAP_ITEMS -> Constr
SYMB_MAP_ITEMS -> DataType
(forall b. Data b => b -> b) -> SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMS
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMS
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) -> SYMB_MAP_ITEMS -> u
forall u. (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMS
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMS
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMB_MAP_ITEMS)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SYMB_MAP_ITEMS)
$cSymb_map_items :: Constr
$tSYMB_MAP_ITEMS :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
gmapMp :: (forall d. Data d => d -> m d)
-> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
gmapM :: (forall d. Data d => d -> m d)
-> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> u
gmapQ :: (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r
gmapT :: (forall b. Data b => b -> b) -> SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS
$cgmapT :: (forall b. Data b => b -> b) -> SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SYMB_MAP_ITEMS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SYMB_MAP_ITEMS)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SYMB_MAP_ITEMS)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMB_MAP_ITEMS)
dataTypeOf :: SYMB_MAP_ITEMS -> DataType
$cdataTypeOf :: SYMB_MAP_ITEMS -> DataType
toConstr :: SYMB_MAP_ITEMS -> Constr
$ctoConstr :: SYMB_MAP_ITEMS -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMS
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMS
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMS
$cp1Data :: Typeable SYMB_MAP_ITEMS
Data)

data SYMB_OR_MAP = Symb SYMB
                 | Symb_map SYMB SYMB
                   deriving (Int -> SYMB_OR_MAP -> ShowS
[SYMB_OR_MAP] -> ShowS
SYMB_OR_MAP -> String
(Int -> SYMB_OR_MAP -> ShowS)
-> (SYMB_OR_MAP -> String)
-> ([SYMB_OR_MAP] -> ShowS)
-> Show SYMB_OR_MAP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SYMB_OR_MAP] -> ShowS
$cshowList :: [SYMB_OR_MAP] -> ShowS
show :: SYMB_OR_MAP -> String
$cshow :: SYMB_OR_MAP -> String
showsPrec :: Int -> SYMB_OR_MAP -> ShowS
$cshowsPrec :: Int -> SYMB_OR_MAP -> ShowS
Show, SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
(SYMB_OR_MAP -> SYMB_OR_MAP -> Bool)
-> (SYMB_OR_MAP -> SYMB_OR_MAP -> Bool) -> Eq SYMB_OR_MAP
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
$c/= :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
== :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
$c== :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
Eq, Typeable, Typeable SYMB_OR_MAP
Constr
DataType
Typeable SYMB_OR_MAP =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAP)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAP)
-> (SYMB_OR_MAP -> Constr)
-> (SYMB_OR_MAP -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SYMB_OR_MAP))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SYMB_OR_MAP))
-> ((forall b. Data b => b -> b) -> SYMB_OR_MAP -> SYMB_OR_MAP)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r)
-> (forall u. (forall d. Data d => d -> u) -> SYMB_OR_MAP -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SYMB_OR_MAP -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP)
-> Data SYMB_OR_MAP
SYMB_OR_MAP -> Constr
SYMB_OR_MAP -> DataType
(forall b. Data b => b -> b) -> SYMB_OR_MAP -> SYMB_OR_MAP
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAP
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAP
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) -> SYMB_OR_MAP -> u
forall u. (forall d. Data d => d -> u) -> SYMB_OR_MAP -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAP
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAP
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMB_OR_MAP)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SYMB_OR_MAP)
$cSymb_map :: Constr
$cSymb :: Constr
$tSYMB_OR_MAP :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP
gmapMp :: (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP
gmapM :: (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP
gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_OR_MAP -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SYMB_OR_MAP -> u
gmapQ :: (forall d. Data d => d -> u) -> SYMB_OR_MAP -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SYMB_OR_MAP -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r
gmapT :: (forall b. Data b => b -> b) -> SYMB_OR_MAP -> SYMB_OR_MAP
$cgmapT :: (forall b. Data b => b -> b) -> SYMB_OR_MAP -> SYMB_OR_MAP
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SYMB_OR_MAP)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SYMB_OR_MAP)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SYMB_OR_MAP)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMB_OR_MAP)
dataTypeOf :: SYMB_OR_MAP -> DataType
$cdataTypeOf :: SYMB_OR_MAP -> DataType
toConstr :: SYMB_OR_MAP -> Constr
$ctoConstr :: SYMB_OR_MAP -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAP
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAP
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAP
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAP
$cp1Data :: Typeable SYMB_OR_MAP
Data)

-- canonical forms

{- converts a term into a form where a function is applied to
   exactly one argument -}
termRecForm :: TERM -> TERM
termRecForm :: TERM -> TERM
termRecForm (Identifier t :: NAME
t) = NAME -> TERM
Identifier NAME
t
termRecForm (Appl f :: TERM
f []) = TERM -> TERM
termRecForm TERM
f
termRecForm (Appl f :: TERM
f as :: [TERM]
as) =
  TERM -> [TERM] -> TERM
Appl (TERM -> TERM
termRecForm (TERM -> TERM) -> TERM -> TERM
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM] -> TERM
Appl TERM
f ([TERM] -> TERM) -> [TERM] -> TERM
forall a b. (a -> b) -> a -> b
$ [TERM] -> [TERM]
forall a. [a] -> [a]
init [TERM]
as) [TERM -> TERM
termRecForm (TERM -> TERM) -> TERM -> TERM
forall a b. (a -> b) -> a -> b
$ [TERM] -> TERM
forall a. [a] -> a
last [TERM]
as]

{- converts a type into a form where each construct takes
   exactly one argument -}
typeRecForm :: TYPE -> TYPE
typeRecForm :: TYPE -> TYPE
typeRecForm (Func [] a :: TYPE
a) = TYPE -> TYPE
typeRecForm TYPE
a
typeRecForm (Func (t :: TYPE
t : ts :: [TYPE]
ts) a :: TYPE
a) = [TYPE] -> TYPE -> TYPE
Func [TYPE -> TYPE
typeRecForm TYPE
t] (TYPE -> TYPE) -> TYPE -> TYPE
forall a b. (a -> b) -> a -> b
$ TYPE -> TYPE
typeRecForm (TYPE -> TYPE) -> TYPE -> TYPE
forall a b. (a -> b) -> a -> b
$ [TYPE] -> TYPE -> TYPE
Func [TYPE]
ts TYPE
a
typeRecForm (Pi [] t :: TYPE
t) = TYPE -> TYPE
typeRecForm TYPE
t
typeRecForm (Pi (([], _) : ds :: [DECL]
ds) a :: TYPE
a) = TYPE -> TYPE
typeRecForm (TYPE -> TYPE) -> TYPE -> TYPE
forall a b. (a -> b) -> a -> b
$ [DECL] -> TYPE -> TYPE
Pi [DECL]
ds TYPE
a
typeRecForm (Pi ((n :: NAME
n : ns :: [NAME]
ns, t :: TYPE
t) : ds :: [DECL]
ds) a :: TYPE
a) =
  [DECL] -> TYPE -> TYPE
Pi [([NAME
n], TYPE -> TYPE
typeRecForm TYPE
t)] (TYPE -> TYPE) -> TYPE -> TYPE
forall a b. (a -> b) -> a -> b
$ TYPE -> TYPE
typeRecForm (TYPE -> TYPE) -> TYPE -> TYPE
forall a b. (a -> b) -> a -> b
$ [DECL] -> TYPE -> TYPE
Pi (([NAME]
ns, TYPE
t) DECL -> [DECL] -> [DECL]
forall a. a -> [a] -> [a]
: [DECL]
ds) TYPE
a
typeRecForm t :: TYPE
t = TYPE
t

{- converts a formula into a form where each quantifier takes
   exactly one argument -}
formulaRecForm :: FORMULA -> FORMULA
formulaRecForm :: FORMULA -> FORMULA
formulaRecForm (Negation f :: FORMULA
f) = FORMULA -> FORMULA
formulaRecForm FORMULA
f
formulaRecForm (Conjunction fs :: [FORMULA]
fs) = [FORMULA] -> FORMULA
Conjunction ([FORMULA] -> FORMULA) -> [FORMULA] -> FORMULA
forall a b. (a -> b) -> a -> b
$ (FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
formulaRecForm [FORMULA]
fs
formulaRecForm (Disjunction fs :: [FORMULA]
fs) = [FORMULA] -> FORMULA
Disjunction ([FORMULA] -> FORMULA) -> [FORMULA] -> FORMULA
forall a b. (a -> b) -> a -> b
$ (FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
formulaRecForm [FORMULA]
fs
formulaRecForm (Implication f :: FORMULA
f g :: FORMULA
g) =
  FORMULA -> FORMULA -> FORMULA
Implication (FORMULA -> FORMULA
formulaRecForm FORMULA
f) (FORMULA -> FORMULA
formulaRecForm FORMULA
g)
formulaRecForm (Equivalence f :: FORMULA
f g :: FORMULA
g) =
  FORMULA -> FORMULA -> FORMULA
Equivalence (FORMULA -> FORMULA
formulaRecForm FORMULA
f) (FORMULA -> FORMULA
formulaRecForm FORMULA
g)
formulaRecForm (Forall [] f :: FORMULA
f) = FORMULA -> FORMULA
formulaRecForm FORMULA
f
formulaRecForm (Forall (([], _) : ds :: [DECL]
ds) f :: FORMULA
f) = FORMULA -> FORMULA
formulaRecForm (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ [DECL] -> FORMULA -> FORMULA
Forall [DECL]
ds FORMULA
f
formulaRecForm (Forall ((n :: NAME
n : ns :: [NAME]
ns, t :: TYPE
t) : ds :: [DECL]
ds) f :: FORMULA
f) =
  [DECL] -> FORMULA -> FORMULA
Forall [([NAME
n], TYPE
t)] (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ FORMULA -> FORMULA
formulaRecForm (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ [DECL] -> FORMULA -> FORMULA
Forall (([NAME]
ns, TYPE
t) DECL -> [DECL] -> [DECL]
forall a. a -> [a] -> [a]
: [DECL]
ds) FORMULA
f
formulaRecForm (Exists [] f :: FORMULA
f) = FORMULA -> FORMULA
formulaRecForm FORMULA
f
formulaRecForm (Exists (([], _) : ds :: [DECL]
ds) f :: FORMULA
f) = FORMULA -> FORMULA
formulaRecForm (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ [DECL] -> FORMULA -> FORMULA
Exists [DECL]
ds FORMULA
f
formulaRecForm (Exists ((n :: NAME
n : ns :: [NAME]
ns, t :: TYPE
t) : ds :: [DECL]
ds) f :: FORMULA
f) =
  [DECL] -> FORMULA -> FORMULA
Exists [([NAME
n], TYPE
t)] (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ FORMULA -> FORMULA
formulaRecForm (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ [DECL] -> FORMULA -> FORMULA
Exists (([NAME]
ns, TYPE
t) DECL -> [DECL] -> [DECL]
forall a. a -> [a] -> [a]
: [DECL]
ds) FORMULA
f
formulaRecForm t :: FORMULA
t = FORMULA
t

{- determines the flattened form of a term, i.e. the function symbol
   applied and the argument list -}
termFlatForm :: TERM -> (NAME, [TERM])
termFlatForm :: TERM -> (NAME, [TERM])
termFlatForm (Identifier x :: NAME
x) = (NAME
x, [])
termFlatForm (Appl f :: TERM
f as :: [TERM]
as) = (NAME
x, [TERM]
bs [TERM] -> [TERM] -> [TERM]
forall a. [a] -> [a] -> [a]
++ [TERM]
as)
                          where (x :: NAME
x, bs :: [TERM]
bs) = TERM -> (NAME, [TERM])
termFlatForm TERM
f

{- converts a type into a flattened form where each operator binds maximum
   number of arguments -}
typeFlatForm :: TYPE -> TYPE
typeFlatForm :: TYPE -> TYPE
typeFlatForm (Func [] t :: TYPE
t) = TYPE -> TYPE
typeFlatForm TYPE
t
typeFlatForm (Func ts :: [TYPE]
ts t :: TYPE
t) =
  let ts1 :: [TYPE]
ts1 = (TYPE -> TYPE) -> [TYPE] -> [TYPE]
forall a b. (a -> b) -> [a] -> [b]
map TYPE -> TYPE
typeFlatForm [TYPE]
ts
      t1 :: TYPE
t1 = TYPE -> TYPE
typeFlatForm TYPE
t
      in case TYPE
t1 of
         Func ts2 :: [TYPE]
ts2 t2 :: TYPE
t2 -> [TYPE] -> TYPE -> TYPE
Func ([TYPE]
ts1 [TYPE] -> [TYPE] -> [TYPE]
forall a. [a] -> [a] -> [a]
++ [TYPE]
ts2) TYPE
t2
         _ -> [TYPE] -> TYPE -> TYPE
Func [TYPE]
ts1 TYPE
t1
typeFlatForm (Pi [] t :: TYPE
t) = TYPE -> TYPE
typeFlatForm TYPE
t
typeFlatForm (Pi ds :: [DECL]
ds t :: TYPE
t) =
  let ds1 :: [DECL]
ds1 = (DECL -> DECL) -> [DECL] -> [DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ns :: [NAME]
ns, t3 :: TYPE
t3) -> ([NAME]
ns, TYPE -> TYPE
typeFlatForm TYPE
t3)) [DECL]
ds
      t1 :: TYPE
t1 = TYPE -> TYPE
typeFlatForm TYPE
t
      in case TYPE
t1 of
         Pi ds2 :: [DECL]
ds2 t2 :: TYPE
t2 -> [DECL] -> TYPE -> TYPE
Pi ([DECL] -> [DECL]
compactDecls ([DECL]
ds1 [DECL] -> [DECL] -> [DECL]
forall a. [a] -> [a] -> [a]
++ [DECL]
ds2)) TYPE
t2
         _ -> [DECL] -> TYPE -> TYPE
Pi ([DECL] -> [DECL]
compactDecls [DECL]
ds1) TYPE
t1
typeFlatForm t :: TYPE
t = TYPE
t

{- converts a formula into a flattened form where each quantifier binds maximum
   number of arguments -}
formulaFlatForm :: FORMULA -> FORMULA
formulaFlatForm :: FORMULA -> FORMULA
formulaFlatForm (Negation f :: FORMULA
f) = FORMULA -> FORMULA
formulaFlatForm FORMULA
f
formulaFlatForm (Conjunction []) = FORMULA
T
formulaFlatForm (Conjunction fs :: [FORMULA]
fs) = [FORMULA] -> FORMULA
Conjunction ([FORMULA] -> FORMULA) -> [FORMULA] -> FORMULA
forall a b. (a -> b) -> a -> b
$ (FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
formulaFlatForm [FORMULA]
fs
formulaFlatForm (Disjunction []) = FORMULA
F
formulaFlatForm (Disjunction fs :: [FORMULA]
fs) = [FORMULA] -> FORMULA
Disjunction ([FORMULA] -> FORMULA) -> [FORMULA] -> FORMULA
forall a b. (a -> b) -> a -> b
$ (FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
formulaFlatForm [FORMULA]
fs
formulaFlatForm (Implication f :: FORMULA
f g :: FORMULA
g) =
  FORMULA -> FORMULA -> FORMULA
Implication (FORMULA -> FORMULA
formulaFlatForm FORMULA
f) (FORMULA -> FORMULA
formulaFlatForm FORMULA
g)
formulaFlatForm (Equivalence f :: FORMULA
f g :: FORMULA
g) =
  FORMULA -> FORMULA -> FORMULA
Equivalence (FORMULA -> FORMULA
formulaFlatForm FORMULA
f) (FORMULA -> FORMULA
formulaFlatForm FORMULA
g)
formulaFlatForm (Forall [] f :: FORMULA
f) = FORMULA -> FORMULA
formulaFlatForm FORMULA
f
formulaFlatForm (Forall ds1 :: [DECL]
ds1 f :: FORMULA
f) =
  let f1 :: FORMULA
f1 = FORMULA -> FORMULA
formulaFlatForm FORMULA
f
      in case FORMULA
f1 of
         Forall ds2 :: [DECL]
ds2 f2 :: FORMULA
f2 -> [DECL] -> FORMULA -> FORMULA
Forall ([DECL] -> [DECL]
compactDecls ([DECL]
ds1 [DECL] -> [DECL] -> [DECL]
forall a. [a] -> [a] -> [a]
++ [DECL]
ds2)) FORMULA
f2
         _ -> [DECL] -> FORMULA -> FORMULA
Forall ([DECL] -> [DECL]
compactDecls [DECL]
ds1) FORMULA
f1
formulaFlatForm (Exists [] f :: FORMULA
f) = FORMULA -> FORMULA
formulaFlatForm FORMULA
f
formulaFlatForm (Exists ds1 :: [DECL]
ds1 f :: FORMULA
f) =
  let f1 :: FORMULA
f1 = FORMULA -> FORMULA
formulaFlatForm FORMULA
f
      in case FORMULA
f1 of
         Exists ds2 :: [DECL]
ds2 f2 :: FORMULA
f2 -> [DECL] -> FORMULA -> FORMULA
Exists ([DECL] -> [DECL]
compactDecls ([DECL]
ds1 [DECL] -> [DECL] -> [DECL]
forall a. [a] -> [a] -> [a]
++ [DECL]
ds2)) FORMULA
f2
         _ -> [DECL] -> FORMULA -> FORMULA
Exists ([DECL] -> [DECL]
compactDecls [DECL]
ds1) FORMULA
f1
formulaFlatForm t :: FORMULA
t = FORMULA
t

-- substitutions

{- class of types containing identifiers which may be
   substituted by terms -}
class Translatable a where
   {- substitutions and renamings: the first argument specifies the desired
      term/identifier substitutions and the second the set of identifiers which
      cannot be used as new variable names -}
   translate :: Map.Map NAME TERM -> Set.Set NAME -> a -> a

instance Translatable TERM where
   translate :: Map NAME TERM -> Set NAME -> TERM -> TERM
translate m :: Map NAME TERM
m _ = Map NAME TERM -> TERM -> TERM
translateTerm Map NAME TERM
m (TERM -> TERM) -> (TERM -> TERM) -> TERM -> TERM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM -> TERM
termRecForm
instance Translatable TYPE where
   translate :: Map NAME TERM -> Set NAME -> TYPE -> TYPE
translate m :: Map NAME TERM
m s :: Set NAME
s t :: TYPE
t = let s1 :: Set NAME
s1 = [Set NAME] -> Set NAME
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set NAME] -> Set NAME) -> [Set NAME] -> Set NAME
forall a b. (a -> b) -> a -> b
$ (TERM -> Set NAME) -> [TERM] -> [Set NAME]
forall a b. (a -> b) -> [a] -> [b]
map TERM -> Set NAME
getFreeVarsInTerm ([TERM] -> [Set NAME]) -> [TERM] -> [Set NAME]
forall a b. (a -> b) -> a -> b
$ Map NAME TERM -> [TERM]
forall k a. Map k a -> [a]
Map.elems Map NAME TERM
m
                         in Map NAME TERM -> Set NAME -> TYPE -> TYPE
translateType Map NAME TERM
m (Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set NAME
s Set NAME
s1) (TYPE -> TYPE
typeRecForm TYPE
t)
instance Translatable FORMULA where
   translate :: Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
translate m :: Map NAME TERM
m s :: Set NAME
s f :: FORMULA
f = let s1 :: Set NAME
s1 = [Set NAME] -> Set NAME
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set NAME] -> Set NAME) -> [Set NAME] -> Set NAME
forall a b. (a -> b) -> a -> b
$ (TERM -> Set NAME) -> [TERM] -> [Set NAME]
forall a b. (a -> b) -> [a] -> [b]
map TERM -> Set NAME
getFreeVarsInTerm ([TERM] -> [Set NAME]) -> [TERM] -> [Set NAME]
forall a b. (a -> b) -> a -> b
$ Map NAME TERM -> [TERM]
forall k a. Map k a -> [a]
Map.elems Map NAME TERM
m
                         in Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
translateFormula Map NAME TERM
m (Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set NAME
s Set NAME
s1)
                               (FORMULA -> FORMULA
formulaRecForm FORMULA
f)

translateTerm :: Map.Map NAME TERM -> TERM -> TERM
translateTerm :: Map NAME TERM -> TERM -> TERM
translateTerm m :: Map NAME TERM
m (Identifier x :: NAME
x) = TERM -> NAME -> Map NAME TERM -> TERM
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (NAME -> TERM
Identifier NAME
x) NAME
x Map NAME TERM
m
translateTerm m :: Map NAME TERM
m (Appl f :: TERM
f [a :: TERM
a]) = TERM -> [TERM] -> TERM
Appl (Map NAME TERM -> TERM -> TERM
translateTerm Map NAME TERM
m TERM
f) [Map NAME TERM -> TERM -> TERM
translateTerm Map NAME TERM
m TERM
a]
translateTerm _ t :: TERM
t = TERM
t

translateType :: Map.Map NAME TERM -> Set.Set NAME -> TYPE -> TYPE
translateType :: Map NAME TERM -> Set NAME -> TYPE -> TYPE
translateType _ _ Sort = TYPE
Sort
translateType _ _ Form = TYPE
Form
translateType m :: Map NAME TERM
m s :: Set NAME
s (Univ t :: TERM
t) = TERM -> TYPE
Univ (TERM -> TYPE) -> TERM -> TYPE
forall a b. (a -> b) -> a -> b
$ Map NAME TERM -> Set NAME -> TERM -> TERM
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s TERM
t
translateType m :: Map NAME TERM
m s :: Set NAME
s (Func ts :: [TYPE]
ts t :: TYPE
t) = [TYPE] -> TYPE -> TYPE
Func ((TYPE -> TYPE) -> [TYPE] -> [TYPE]
forall a b. (a -> b) -> [a] -> [b]
map (Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s) [TYPE]
ts) (Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s TYPE
t)
translateType m :: Map NAME TERM
m s :: Set NAME
s (Pi [([x :: NAME
x], t :: TYPE
t)] a :: TYPE
a) =
  let t1 :: TYPE
t1 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s TYPE
t
      x1 :: NAME
x1 = NAME -> Set NAME -> NAME
getNewName NAME
x Set NAME
s
      a1 :: TYPE
a1 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate (NAME -> TERM -> Map NAME TERM -> Map NAME TERM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NAME
x (NAME -> TERM
Identifier NAME
x1) Map NAME TERM
m) (NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert NAME
x1 Set NAME
s) TYPE
a
      in [DECL] -> TYPE -> TYPE
Pi [([NAME
x1], TYPE
t1)] TYPE
a1
translateType _ _ t :: TYPE
t = TYPE
t

translateFormula :: Map.Map NAME TERM -> Set.Set NAME -> FORMULA -> FORMULA
translateFormula :: Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
translateFormula _ _ T = FORMULA
T
translateFormula _ _ F = FORMULA
F
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Pred t :: TERM
t) = TERM -> FORMULA
Pred (TERM -> FORMULA) -> TERM -> FORMULA
forall a b. (a -> b) -> a -> b
$ Map NAME TERM -> Set NAME -> TERM -> TERM
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s TERM
t
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Equality t1 :: TERM
t1 t2 :: TERM
t2) =
  TERM -> TERM -> FORMULA
Equality (Map NAME TERM -> Set NAME -> TERM -> TERM
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s TERM
t1) (Map NAME TERM -> Set NAME -> TERM -> TERM
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s TERM
t2)
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Negation f :: FORMULA
f) = FORMULA -> FORMULA
Negation (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s FORMULA
f
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Conjunction fs :: [FORMULA]
fs) =
  [FORMULA] -> FORMULA
Conjunction ([FORMULA] -> FORMULA) -> [FORMULA] -> FORMULA
forall a b. (a -> b) -> a -> b
$ (FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s) [FORMULA]
fs
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Disjunction fs :: [FORMULA]
fs) =
  [FORMULA] -> FORMULA
Disjunction ([FORMULA] -> FORMULA) -> [FORMULA] -> FORMULA
forall a b. (a -> b) -> a -> b
$ (FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s) [FORMULA]
fs
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Implication f :: FORMULA
f g :: FORMULA
g) =
  FORMULA -> FORMULA -> FORMULA
Implication (Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s FORMULA
f) (Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s FORMULA
g)
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Equivalence f :: FORMULA
f g :: FORMULA
g) =
  FORMULA -> FORMULA -> FORMULA
Equivalence (Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s FORMULA
f) (Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s FORMULA
g)
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Forall [([x :: NAME
x], t :: TYPE
t)] f :: FORMULA
f) =
  let t1 :: TYPE
t1 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s TYPE
t
      x1 :: NAME
x1 = NAME -> Set NAME -> NAME
getNewName NAME
x Set NAME
s
      f1 :: FORMULA
f1 = Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate (NAME -> TERM -> Map NAME TERM -> Map NAME TERM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NAME
x (NAME -> TERM
Identifier NAME
x1) Map NAME TERM
m) (NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert NAME
x1 Set NAME
s) FORMULA
f
      in [DECL] -> FORMULA -> FORMULA
Forall [([NAME
x1], TYPE
t1)] FORMULA
f1
translateFormula m :: Map NAME TERM
m s :: Set NAME
s (Exists [([x :: NAME
x], t :: TYPE
t)] f :: FORMULA
f) =
  let t1 :: TYPE
t1 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
m Set NAME
s TYPE
t
      x1 :: NAME
x1 = NAME -> Set NAME -> NAME
getNewName NAME
x Set NAME
s
      f1 :: FORMULA
f1 = Map NAME TERM -> Set NAME -> FORMULA -> FORMULA
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate (NAME -> TERM -> Map NAME TERM -> Map NAME TERM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NAME
x (NAME -> TERM
Identifier NAME
x1) Map NAME TERM
m) (NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert NAME
x1 Set NAME
s) FORMULA
f
      in [DECL] -> FORMULA -> FORMULA
Exists [([NAME
x1], TYPE
t1)] FORMULA
f1
translateFormula _ _ f :: FORMULA
f = FORMULA
f

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

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

-- equality (should be defined via Ord!)
instance Eq TERM where
    u :: TERM
u == :: TERM -> TERM -> Bool
== v :: TERM
v = TERM -> TERM -> Bool
eqTerm (TERM -> TERM
termRecForm TERM
u) (TERM -> TERM
termRecForm TERM
v)
instance Eq TYPE where
    u :: TYPE
u == :: TYPE -> TYPE -> Bool
== v :: TYPE
v = TYPE -> TYPE -> Bool
eqType (TYPE -> TYPE
typeRecForm TYPE
u) (TYPE -> TYPE
typeRecForm TYPE
v)

eqTerm :: TERM -> TERM -> Bool
eqTerm :: TERM -> TERM -> Bool
eqTerm (Identifier x1 :: NAME
x1) (Identifier x2 :: NAME
x2) = NAME
x1 NAME -> NAME -> Bool
forall a. Eq a => a -> a -> Bool
== NAME
x2
eqTerm (Appl f1 :: TERM
f1 [a1 :: TERM
a1]) (Appl f2 :: TERM
f2 [a2 :: TERM
a2]) = TERM
f1 TERM -> TERM -> Bool
forall a. Eq a => a -> a -> Bool
== TERM
f2 Bool -> Bool -> Bool
&& TERM
a1 TERM -> TERM -> Bool
forall a. Eq a => a -> a -> Bool
== TERM
a2
eqTerm _ _ = Bool
False

eqType :: TYPE -> TYPE -> Bool
eqType :: TYPE -> TYPE -> Bool
eqType Sort Sort = Bool
True
eqType Form Form = Bool
True
eqType (Univ t1 :: TERM
t1) (Univ t2 :: TERM
t2) = TERM
t1 TERM -> TERM -> Bool
forall a. Eq a => a -> a -> Bool
== TERM
t2
eqType (Func [t1 :: TYPE
t1] s1 :: TYPE
s1) (Func [t2 :: TYPE
t2] s2 :: TYPE
s2) = TYPE
t1 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
t2 Bool -> Bool -> Bool
&& TYPE
s1 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
s2
eqType (Pi [([n1 :: NAME
n1], t1 :: TYPE
t1)] s1 :: TYPE
s1) (Pi [([n2 :: NAME
n2], t2 :: TYPE
t2)] s2 :: TYPE
s2) =
  let syms1 :: Set NAME
syms1 = NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.delete NAME
n1 (Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ TYPE -> Set NAME
getFreeVars TYPE
s1
      syms2 :: Set NAME
syms2 = NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.delete NAME
n2 (Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ TYPE -> Set NAME
getFreeVars TYPE
s2
      v :: NAME
v = NAME -> Set NAME -> NAME
getNewName NAME
n1 (Set NAME -> NAME) -> Set NAME -> NAME
forall a b. (a -> b) -> a -> b
$ Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set NAME
syms1 Set NAME
syms2
      type1 :: TYPE
type1 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate (NAME -> TERM -> Map NAME TERM
forall k a. k -> a -> Map k a
Map.singleton NAME
n1 (NAME -> TERM
Identifier NAME
v)) Set NAME
syms1 TYPE
s1
      type2 :: TYPE
type2 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate (NAME -> TERM -> Map NAME TERM
forall k a. k -> a -> Map k a
Map.singleton NAME
n2 (NAME -> TERM
Identifier NAME
v)) Set NAME
syms2 TYPE
s2
      in TYPE
t1 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
t2 Bool -> Bool -> Bool
&& TYPE
type1 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
type2
eqType _ _ = Bool
False

-- returns a set of unbound identifiers used within a type
getFreeVars :: TYPE -> Set.Set NAME
getFreeVars :: TYPE -> Set NAME
getFreeVars e :: TYPE
e = TYPE -> Set NAME
getFreeVarsH (TYPE -> Set NAME) -> TYPE -> Set NAME
forall a b. (a -> b) -> a -> b
$ TYPE -> TYPE
typeRecForm TYPE
e

getFreeVarsH :: TYPE -> Set.Set NAME
getFreeVarsH :: TYPE -> Set NAME
getFreeVarsH Sort = Set NAME
forall a. Set a
Set.empty
getFreeVarsH Form = Set NAME
forall a. Set a
Set.empty
getFreeVarsH (Univ t :: TERM
t) = TERM -> Set NAME
getFreeVarsInTerm TERM
t
getFreeVarsH (Func [t :: TYPE
t] v :: TYPE
v) =
  Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TYPE -> Set NAME
getFreeVarsH TYPE
t) (TYPE -> Set NAME
getFreeVarsH TYPE
v)
getFreeVarsH (Pi [([n :: NAME
n], t :: TYPE
t)] a :: TYPE
a) =
  NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.delete NAME
n (Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TYPE -> Set NAME
getFreeVarsH TYPE
t) (TYPE -> Set NAME
getFreeVarsH TYPE
a)
getFreeVarsH _ = Set NAME
forall a. Set a
Set.empty

getFreeVarsInTerm :: TERM -> Set.Set NAME
getFreeVarsInTerm :: TERM -> Set NAME
getFreeVarsInTerm t :: TERM
t = TERM -> Set NAME
getFreeVarsInTermH (TERM -> Set NAME) -> TERM -> Set NAME
forall a b. (a -> b) -> a -> b
$ TERM -> TERM
termRecForm TERM
t

getFreeVarsInTermH :: TERM -> Set.Set NAME
getFreeVarsInTermH :: TERM -> Set NAME
getFreeVarsInTermH (Identifier x :: NAME
x) = NAME -> Set NAME
forall a. a -> Set a
Set.singleton NAME
x
getFreeVarsInTermH (Appl f :: TERM
f [a :: TERM
a]) =
  Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TERM -> Set NAME
getFreeVarsInTermH TERM
f) (TERM -> Set NAME
getFreeVarsInTermH TERM
a)
getFreeVarsInTermH _ = Set NAME
forall a. Set a
Set.empty

-- precedences - needed for pretty printing
formulaPrec :: FORMULA -> Int
formulaPrec :: FORMULA -> Int
formulaPrec T = Int
truePrec
formulaPrec F = Int
falsePrec
formulaPrec Pred {} = Int
predPrec
formulaPrec Equality {} = Int
equalPrec
formulaPrec Negation {} = Int
negPrec
formulaPrec Disjunction {} = Int
disjPrec
formulaPrec Conjunction {} = Int
conjPrec
formulaPrec Implication {} = Int
implPrec
formulaPrec Equivalence {} = Int
equivPrec
formulaPrec Forall {} = Int
forallPrec
formulaPrec Exists {} = Int
existsPrec

typePrec :: TYPE -> Int
typePrec :: TYPE -> Int
typePrec Sort = Int
sortPrec
typePrec Form = Int
formPrec
typePrec Univ {} = Int
univPrec
typePrec Func {} = Int
funcPrec
typePrec Pi {} = Int
piPrec

-- pretty printing
instance Pretty BASIC_SPEC where
    pretty :: BASIC_SPEC -> Doc
pretty = BASIC_SPEC -> Doc
printBasicSpec
instance Pretty BASIC_ITEM where
    pretty :: BASIC_ITEM -> Doc
pretty = BASIC_ITEM -> Doc
printBasicItem
instance Pretty TYPE where
    pretty :: TYPE -> Doc
pretty = TYPE -> Doc
printType (TYPE -> Doc) -> (TYPE -> TYPE) -> TYPE -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TYPE -> TYPE
typeFlatForm
instance Pretty TERM where
    pretty :: TERM -> Doc
pretty = TERM -> Doc
printTerm
instance Pretty FORMULA where
    pretty :: FORMULA -> Doc
pretty = FORMULA -> Doc
printFormula (FORMULA -> Doc) -> (FORMULA -> FORMULA) -> FORMULA -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
formulaFlatForm
instance Pretty SYMB_ITEMS where
    pretty :: SYMB_ITEMS -> Doc
pretty = SYMB_ITEMS -> Doc
printSymbItems
instance Pretty SYMB_MAP_ITEMS where
    pretty :: SYMB_MAP_ITEMS -> Doc
pretty = SYMB_MAP_ITEMS -> Doc
printSymbMapItems
instance Pretty SYMB_OR_MAP where
    pretty :: SYMB_OR_MAP -> Doc
pretty = SYMB_OR_MAP -> Doc
printSymbOrMap

printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec (Basic_spec xs :: [Annoted BASIC_ITEM]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEM -> Doc) -> [Annoted BASIC_ITEM] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annoted BASIC_ITEM -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted BASIC_ITEM]
xs

printBasicItem :: BASIC_ITEM -> Doc
printBasicItem :: BASIC_ITEM -> Doc
printBasicItem (Decl_item (ns :: [NAME]
ns, t :: TYPE
t)) = [NAME] -> Doc
printNames [NAME]
ns Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+> TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t
printBasicItem (Axiom_item f :: FORMULA
f) = Doc
dot Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty FORMULA
f

printType :: TYPE -> Doc
printType :: TYPE -> Doc
printType (TYPE
Sort) = String -> Doc
text "Sort"
printType (TYPE
Form) = String -> Doc
text "Form"
printType (Univ t :: TERM
t) = TERM -> Doc
forall a. Pretty a => a -> Doc
pretty TERM
t
printType (Func ts :: [TYPE]
ts t :: TYPE
t) =
  [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
prepPunctuate (String -> Doc
text "-> ")
    ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (TYPE -> Doc) -> [TYPE] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TYPE -> Doc
printTypeWithPrec Int
funcPrec) ([TYPE]
ts [TYPE] -> [TYPE] -> [TYPE]
forall a. [a] -> [a] -> [a]
++ [TYPE
t])
printType (Pi xs :: [DECL]
xs x :: TYPE
x) = String -> Doc
text "Pi" Doc -> Doc -> Doc
<+> [DECL] -> Doc
printDecls [DECL]
xs Doc -> Doc -> Doc
<+> TYPE -> Doc
printType TYPE
x

printTypeWithPrec :: Int -> TYPE -> Doc
printTypeWithPrec :: Int -> TYPE -> Doc
printTypeWithPrec prec :: Int
prec t :: TYPE
t = if TYPE -> Int
typePrec TYPE
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
prec
                              then Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TYPE -> Doc
printType TYPE
t
                              else TYPE -> Doc
printType TYPE
t

printTerm :: TERM -> Doc
printTerm :: TERM -> Doc
printTerm t :: TERM
t = if [TERM] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM]
as
                 then NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
x
                 else NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
x Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([TERM] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [TERM]
as)
              where (x :: NAME
x, as :: [TERM]
as) = TERM -> (NAME, [TERM])
termFlatForm TERM
t

printFormula :: FORMULA -> Doc
printFormula :: FORMULA -> Doc
printFormula (FORMULA
T) = String -> Doc
text "true"
printFormula (FORMULA
F) = String -> Doc
text "false"
printFormula (Pred x :: TERM
x) = TERM -> Doc
forall a. Pretty a => a -> Doc
pretty TERM
x
printFormula (Equality x :: TERM
x y :: TERM
y) = TERM -> Doc
forall a. Pretty a => a -> Doc
pretty TERM
x Doc -> Doc -> Doc
<+> String -> Doc
text "==" Doc -> Doc -> Doc
<+> TERM -> Doc
forall a. Pretty a => a -> Doc
pretty TERM
y
printFormula (Negation f :: FORMULA
f) = Doc
notDoc Doc -> Doc -> Doc
<+> Int -> FORMULA -> Doc
printFormulaWithPrec Int
negPrec FORMULA
f
printFormula (Conjunction xs :: [FORMULA]
xs) = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
prepPunctuate (Doc
andDoc Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space)
  ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (FORMULA -> Doc) -> [FORMULA] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> FORMULA -> Doc
printFormulaWithPrec Int
conjPrec) [FORMULA]
xs
printFormula (Disjunction xs :: [FORMULA]
xs) = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
prepPunctuate (Doc
orDoc Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space)
  ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (FORMULA -> Doc) -> [FORMULA] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> FORMULA -> Doc
printFormulaWithPrec Int
disjPrec) [FORMULA]
xs
printFormula (Implication x :: FORMULA
x y :: FORMULA
y) =
  Int -> FORMULA -> Doc
printFormulaWithPrec (Int
implPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) FORMULA
x
  Doc -> Doc -> Doc
<+> Doc
implies
  Doc -> Doc -> Doc
<+> Int -> FORMULA -> Doc
printFormulaWithPrec (Int
implPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) FORMULA
y
printFormula (Equivalence x :: FORMULA
x y :: FORMULA
y) =
  Int -> FORMULA -> Doc
printFormulaWithPrec (Int
equivPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) FORMULA
x
  Doc -> Doc -> Doc
<+> Doc
equiv
  Doc -> Doc -> Doc
<+> Int -> FORMULA -> Doc
printFormulaWithPrec (Int
equivPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) FORMULA
y
printFormula (Forall xs :: [DECL]
xs f :: FORMULA
f) = Doc
forallDoc Doc -> Doc -> Doc
<+> [DECL] -> Doc
printDecls [DECL]
xs Doc -> Doc -> Doc
<+> FORMULA -> Doc
printFormula FORMULA
f
printFormula (Exists xs :: [DECL]
xs f :: FORMULA
f) = Doc
exists Doc -> Doc -> Doc
<+> [DECL] -> Doc
printDecls [DECL]
xs Doc -> Doc -> Doc
<+> FORMULA -> Doc
printFormula FORMULA
f

printFormulaWithPrec :: Int -> FORMULA -> Doc
printFormulaWithPrec :: Int -> FORMULA -> Doc
printFormulaWithPrec prec :: Int
prec f :: FORMULA
f = if FORMULA -> Int
formulaPrec FORMULA
f Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
prec
                                 then Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FORMULA -> Doc
printFormula FORMULA
f
                                 else FORMULA -> Doc
printFormula FORMULA
f

printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems (Symb_items xs :: [NAME]
xs) = [NAME] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [NAME]
xs

printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems (Symb_map_items xs :: [SYMB_OR_MAP]
xs) = [SYMB_OR_MAP] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SYMB_OR_MAP]
xs

printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap (Symb s :: NAME
s) = NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
s
printSymbOrMap (Symb_map s :: NAME
s t :: NAME
t) = NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
s Doc -> Doc -> Doc
<+> Doc
mapsto Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
t

printNames :: [NAME] -> Doc
printNames :: [NAME] -> Doc
printNames = [NAME] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas

printDecl :: DECL -> Doc
printDecl :: DECL -> Doc
printDecl (ns :: [NAME]
ns, t :: TYPE
t) = [NAME] -> Doc
printNames [NAME]
ns Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t

printDecls :: [DECL] -> Doc
printDecls :: [DECL] -> Doc
printDecls xs :: [DECL]
xs = [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (DECL -> Doc) -> [DECL] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DECL -> Doc
printDecl [DECL]
xs) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot

-- operations on a list of declarations
getVarsFromDecls :: [DECL] -> [NAME]
getVarsFromDecls :: [DECL] -> [NAME]
getVarsFromDecls = (DECL -> [NAME]) -> [DECL] -> [NAME]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DECL -> [NAME]
forall a b. (a, b) -> a
fst

getVarTypeFromDecls :: NAME -> [DECL] -> Maybe TYPE
getVarTypeFromDecls :: NAME -> [DECL] -> Maybe TYPE
getVarTypeFromDecls n :: NAME
n ds :: [DECL]
ds = case Maybe DECL
result of
                                Just (_, t :: TYPE
t) -> TYPE -> Maybe TYPE
forall a. a -> Maybe a
Just TYPE
t
                                Nothing -> Maybe TYPE
forall a. Maybe a
Nothing
                           where result :: Maybe DECL
result = (DECL -> Bool) -> [DECL] -> Maybe DECL
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ (ns :: [NAME]
ns, _) -> NAME -> [NAME] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem NAME
n [NAME]
ns) [DECL]
ds

compactDecls :: [DECL] -> [DECL]
compactDecls :: [DECL] -> [DECL]
compactDecls [] = []
compactDecls [d :: DECL
d] = [DECL
d]
compactDecls (d1 :: DECL
d1 : d2 :: DECL
d2 : ds :: [DECL]
ds) =
  let (ns1 :: [NAME]
ns1, t1 :: TYPE
t1) = DECL
d1
      (ns2 :: [NAME]
ns2, t2 :: TYPE
t2) = DECL
d2
      in if TYPE
t1 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
t2
            then [DECL] -> [DECL]
compactDecls ([DECL] -> [DECL]) -> [DECL] -> [DECL]
forall a b. (a -> b) -> a -> b
$ ([NAME]
ns1 [NAME] -> [NAME] -> [NAME]
forall a. [a] -> [a] -> [a]
++ [NAME]
ns2, TYPE
t1) DECL -> [DECL] -> [DECL]
forall a. a -> [a] -> [a]
: [DECL]
ds
            else DECL
d1 DECL -> [DECL] -> [DECL]
forall a. a -> [a] -> [a]
: [DECL] -> [DECL]
compactDecls (DECL
d2 DECL -> [DECL] -> [DECL]
forall a. a -> [a] -> [a]
: [DECL]
ds)

expandDecls :: [DECL] -> [SDECL]
expandDecls :: [DECL] -> [SDECL]
expandDecls = (DECL -> [SDECL]) -> [DECL] -> [SDECL]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (ns :: [NAME]
ns, t :: TYPE
t) -> (NAME -> SDECL) -> [NAME] -> [SDECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: NAME
n -> (NAME
n, TYPE
t)) [NAME]
ns)