{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
Description :  prenex normal form for sentences of a CASL theory
Copyright   :  (c) Mihai Codescu, 2016
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  codescu@iws.cs.uni-magdeburg.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Comorphism)

-}

module Comorphisms.CASL2Prenex where

import Logic.Logic
import Logic.Comorphism

import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Sublogic as SL hiding (bottom)
import CASL.Induction
import CASL.Quantification

import Common.Result
import Common.Id
import qualified Data.Set as Set

import Common.AS_Annotation
import Common.ProofTree

data CASL2Prenex = CASL2Prenex deriving Int -> CASL2Prenex -> ShowS
[CASL2Prenex] -> ShowS
CASL2Prenex -> String
(Int -> CASL2Prenex -> ShowS)
-> (CASL2Prenex -> String)
-> ([CASL2Prenex] -> ShowS)
-> Show CASL2Prenex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2Prenex] -> ShowS
$cshowList :: [CASL2Prenex] -> ShowS
show :: CASL2Prenex -> String
$cshow :: CASL2Prenex -> String
showsPrec :: Int -> CASL2Prenex -> ShowS
$cshowsPrec :: Int -> CASL2Prenex -> ShowS
Show

instance Language CASL2Prenex where
    language_name :: CASL2Prenex -> String
language_name CASL2Prenex = "CASL2Prenex"

instance Comorphism CASL2Prenex
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree where
    sourceLogic :: CASL2Prenex -> CASL
sourceLogic CASL2Prenex = CASL
CASL
    sourceSublogic :: CASL2Prenex -> CASL_Sublogics
sourceSublogic CASL2Prenex = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
    targetLogic :: CASL2Prenex -> CASL
targetLogic CASL2Prenex = CASL
CASL
    mapSublogic :: CASL2Prenex -> CASL_Sublogics -> Maybe CASL_Sublogics
mapSublogic CASL2Prenex sl :: CASL_Sublogics
sl = 
      CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> CASL_Sublogics -> Maybe CASL_Sublogics
forall a b. (a -> b) -> a -> b
$ CASL_Sublogics -> CASL_Sublogics -> CASL_Sublogics
forall a. Ord a => a -> a -> a
min CASL_Sublogics
sl (CASL_Sublogics
sl{which_logic :: CASL_Formulas
SL.which_logic = CASL_Formulas
SL.Prenex})
    map_theory :: CASL2Prenex
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory CASL2Prenex = (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory
    map_morphism :: CASL2Prenex -> CASLMor -> Result CASLMor
map_morphism CASL2Prenex = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return
    map_sentence :: CASL2Prenex -> CASLSign -> CASLFORMULA -> Result CASLFORMULA
map_sentence CASL2Prenex sig :: CASLSign
sig = CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA)
-> CASLFORMULA
-> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CASLSign -> CASLFORMULA -> CASLFORMULA
mapSentence CASLSign
sig)
    map_symbol :: CASL2Prenex -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2Prenex _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: CASL2Prenex -> Bool
has_model_expansion CASL2Prenex = Bool
True
    is_weakly_amalgamable :: CASL2Prenex -> Bool
is_weakly_amalgamable CASL2Prenex = Bool
True

-- remove equivalences
preprocessSen :: CASLFORMULA -> CASLFORMULA
preprocessSen :: CASLFORMULA -> CASLFORMULA
preprocessSen sen :: CASLFORMULA
sen = case CASLFORMULA
sen of
 Quantification q :: QUANTIFIER
q vdecls :: [VAR_DECL]
vdecls sen' :: CASLFORMULA
sen' r :: Range
r ->
   QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vdecls (CASLFORMULA -> CASLFORMULA
preprocessSen CASLFORMULA
sen') Range
r
 Junction j :: Junctor
j sens :: [CASLFORMULA]
sens r :: Range
r -> 
   Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map CASLFORMULA -> CASLFORMULA
preprocessSen [CASLFORMULA]
sens) Range
r
 Relation sen1 :: CASLFORMULA
sen1 Equivalence sen2 :: CASLFORMULA
sen2 _ -> let
    sen1' :: CASLFORMULA
sen1' = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen1 Relation
Implication CASLFORMULA
sen2 Range
nullRange
    sen2' :: CASLFORMULA
sen2' = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen2 Relation
Implication CASLFORMULA
sen1 Range
nullRange
   in Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [CASLFORMULA
sen1', CASLFORMULA
sen2'] Range
nullRange
 Relation sen1 :: CASLFORMULA
sen1 rel :: Relation
rel sen2 :: CASLFORMULA
sen2 r :: Range
r -> 
   CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (CASLFORMULA -> CASLFORMULA
preprocessSen CASLFORMULA
sen1) Relation
rel 
            (CASLFORMULA -> CASLFORMULA
preprocessSen CASLFORMULA
sen2) Range
r
 Negation sen' :: CASLFORMULA
sen' r :: Range
r -> 
   CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (CASLFORMULA -> CASLFORMULA
preprocessSen CASLFORMULA
sen') Range
r
 _ -> CASLFORMULA
sen

-- make variables distinct: 
-- if a variable v of sort s already appears in a formula
-- substitute it with a fresh variable
mkDistVars :: CASLFORMULA -> CASLFORMULA
mkDistVars :: CASLFORMULA -> CASLFORMULA
mkDistVars sen :: CASLFORMULA
sen = 
 let (_, _, sen' :: CASLFORMULA
sen') = Int
-> [(VAR, SORT)]
-> CASLFORMULA
-> (Int, [(VAR, SORT)], CASLFORMULA)
mkDistVarsAux 0 [] CASLFORMULA
sen
 in CASLFORMULA
sen'

mkDistVarsAux :: Int -- first available suffix for vars
              -> [(VAR, SORT)] -- vars encountered so far
              -> CASLFORMULA
              -> (Int, [(VAR, SORT)], CASLFORMULA)
mkDistVarsAux :: Int
-> [(VAR, SORT)]
-> CASLFORMULA
-> (Int, [(VAR, SORT)], CASLFORMULA)
mkDistVarsAux n :: Int
n vlist :: [(VAR, SORT)]
vlist sen :: CASLFORMULA
sen = case CASLFORMULA
sen of
 Quantification q :: QUANTIFIER
q vdecls :: [VAR_DECL]
vdecls form :: CASLFORMULA
form range :: Range
range -> let
   -- first make variables distinct for form
   dvars :: [(VAR, SORT)]
dvars = [VAR_DECL] -> [(VAR, SORT)]
flatVAR_DECLs [VAR_DECL]
vdecls
   (n' :: Int
n', _, form' :: CASLFORMULA
form') = Int
-> [(VAR, SORT)]
-> CASLFORMULA
-> (Int, [(VAR, SORT)], CASLFORMULA)
mkDistVarsAux Int
n ([(VAR, SORT)]
dvars [(VAR, SORT)] -> [(VAR, SORT)] -> [(VAR, SORT)]
forall a. [a] -> [a] -> [a]
++ [(VAR, SORT)]
vlist) CASLFORMULA
form
   -- here we are not interested in the variables generated for the quantified form, so we can forget them
   replVarDecl :: t VAR_DECL -> VAR -> VAR -> SORT -> [VAR_DECL]
replVarDecl vds :: t VAR_DECL
vds oN :: VAR
oN nN :: VAR
nN s :: SORT
s = [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a]
reverse ([VAR_DECL] -> [VAR_DECL]) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ 
                              ([VAR_DECL] -> VAR_DECL -> [VAR_DECL])
-> [VAR_DECL] -> t VAR_DECL -> [VAR_DECL]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\usedD :: [VAR_DECL]
usedD vd :: VAR_DECL
vd@(Var_decl names :: [VAR]
names sort :: SORT
sort r :: Range
r) -> 
                                       if SORT
sort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s then -- found it, replace oN with nN in names
                                         let vd' :: VAR_DECL
vd' = [VAR] -> SORT -> Range -> VAR_DECL
Var_decl ((VAR -> VAR) -> [VAR] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: VAR
x -> if VAR
x VAR -> VAR -> Bool
forall a. Eq a => a -> a -> Bool
== VAR
oN then VAR
nN else VAR
x) [VAR]
names) SORT
sort Range
r  
                                         in VAR_DECL
vd'VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
:[VAR_DECL]
usedD
                                       else VAR_DECL
vdVAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
:[VAR_DECL]
usedD 
                                 ) [] t VAR_DECL
vds
   checkAndReplace :: (Int, [(VAR, SORT)], FORMULA f, [VAR_DECL])
-> (VAR, SORT) -> (Int, [(VAR, SORT)], FORMULA f, [VAR_DECL])
checkAndReplace (n0 :: Int
n0, knownV :: [(VAR, SORT)]
knownV, quantF :: FORMULA f
quantF, quants :: [VAR_DECL]
quants) (x :: VAR
x, s :: SORT
s) =
      if (VAR
x,SORT
s) (VAR, SORT) -> [(VAR, SORT)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(VAR, SORT)]
knownV 
       then
         let  
           x' :: VAR
x' = String -> Int -> VAR
genNumVar "x" Int
n0
           quants' :: [VAR_DECL]
quants' = [VAR_DECL] -> VAR -> VAR -> SORT -> [VAR_DECL]
forall (t :: * -> *).
Foldable t =>
t VAR_DECL -> VAR -> VAR -> SORT -> [VAR_DECL]
replVarDecl [VAR_DECL]
quants VAR
x VAR
x' SORT
s
           quantF' :: FORMULA f
quantF' = VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f
forall f.
FormExtension f =>
VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f
substitute VAR
x SORT
s (VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
x' SORT
s Range
nullRange) FORMULA f
quantF
         in (Int
n0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, (VAR
x', SORT
s)(VAR, SORT) -> [(VAR, SORT)] -> [(VAR, SORT)]
forall a. a -> [a] -> [a]
:[(VAR, SORT)]
knownV, FORMULA f
quantF', [VAR_DECL]
quants')
       else (Int
n0    , (VAR
x , SORT
s)(VAR, SORT) -> [(VAR, SORT)] -> [(VAR, SORT)]
forall a. a -> [a] -> [a]
:[(VAR, SORT)]
knownV, FORMULA f
quantF , [VAR_DECL]
quants )  
   (n'' :: Int
n'', vlist' :: [(VAR, SORT)]
vlist', form'' :: CASLFORMULA
form'', vdecls' :: [VAR_DECL]
vdecls') = ((Int, [(VAR, SORT)], CASLFORMULA, [VAR_DECL])
 -> (VAR, SORT) -> (Int, [(VAR, SORT)], CASLFORMULA, [VAR_DECL]))
-> (Int, [(VAR, SORT)], CASLFORMULA, [VAR_DECL])
-> [(VAR, SORT)]
-> (Int, [(VAR, SORT)], CASLFORMULA, [VAR_DECL])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Int, [(VAR, SORT)], CASLFORMULA, [VAR_DECL])
-> (VAR, SORT) -> (Int, [(VAR, SORT)], CASLFORMULA, [VAR_DECL])
forall f.
FormExtension f =>
(Int, [(VAR, SORT)], FORMULA f, [VAR_DECL])
-> (VAR, SORT) -> (Int, [(VAR, SORT)], FORMULA f, [VAR_DECL])
checkAndReplace (Int
n', [(VAR, SORT)]
vlist, CASLFORMULA
form', [VAR_DECL]
vdecls) [(VAR, SORT)]
dvars
  in (Int
n'', [(VAR, SORT)]
vlist', QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vdecls' CASLFORMULA
form'' Range
range)
 Junction j :: Junctor
j sens :: [CASLFORMULA]
sens r :: Range
r -> let
   (n' :: Int
n', vlist' :: [(VAR, SORT)]
vlist', sens' :: [CASLFORMULA]
sens') = ((Int, [(VAR, SORT)], [CASLFORMULA])
 -> CASLFORMULA -> (Int, [(VAR, SORT)], [CASLFORMULA]))
-> (Int, [(VAR, SORT)], [CASLFORMULA])
-> [CASLFORMULA]
-> (Int, [(VAR, SORT)], [CASLFORMULA])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(x :: Int
x, vs :: [(VAR, SORT)]
vs, osens :: [CASLFORMULA]
osens) s :: CASLFORMULA
s -> 
                           let
                            (x' :: Int
x', vs' :: [(VAR, SORT)]
vs', s' :: CASLFORMULA
s') = Int
-> [(VAR, SORT)]
-> CASLFORMULA
-> (Int, [(VAR, SORT)], CASLFORMULA)
mkDistVarsAux Int
x [(VAR, SORT)]
vs CASLFORMULA
s
                           in (Int
x', [(VAR, SORT)]
vs', CASLFORMULA
s'CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
:[CASLFORMULA]
osens)) (Int
n, [(VAR, SORT)]
vlist, []) [CASLFORMULA]
sens
  in (Int
n', [(VAR, SORT)]
vlist', Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j ([CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a]
reverse [CASLFORMULA]
sens') Range
r)
 Relation sen1 :: CASLFORMULA
sen1 rel :: Relation
rel sen2 :: CASLFORMULA
sen2 r :: Range
r -> let
   (n1 :: Int
n1, vlist1 :: [(VAR, SORT)]
vlist1, sen1' :: CASLFORMULA
sen1') = Int
-> [(VAR, SORT)]
-> CASLFORMULA
-> (Int, [(VAR, SORT)], CASLFORMULA)
mkDistVarsAux Int
n  [(VAR, SORT)]
vlist  CASLFORMULA
sen1
   (n2 :: Int
n2, vlist2 :: [(VAR, SORT)]
vlist2, sen2' :: CASLFORMULA
sen2') = Int
-> [(VAR, SORT)]
-> CASLFORMULA
-> (Int, [(VAR, SORT)], CASLFORMULA)
mkDistVarsAux Int
n1 [(VAR, SORT)]
vlist1 CASLFORMULA
sen2
  in (Int
n2, [(VAR, SORT)]
vlist2, CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen1' Relation
rel CASLFORMULA
sen2' Range
r)
 Negation sen' :: CASLFORMULA
sen' r :: Range
r -> let 
   (n' :: Int
n', vlist' :: [(VAR, SORT)]
vlist', sen'' :: CASLFORMULA
sen'') = Int
-> [(VAR, SORT)]
-> CASLFORMULA
-> (Int, [(VAR, SORT)], CASLFORMULA)
mkDistVarsAux Int
n [(VAR, SORT)]
vlist CASLFORMULA
sen' 
  in (Int
n', [(VAR, SORT)]
vlist', CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
sen'' Range
r)
 _ -> (Int
n, [(VAR, SORT)]
vlist, CASLFORMULA
sen)
       
computePNF :: CASLFORMULA -> CASLFORMULA
computePNF :: CASLFORMULA -> CASLFORMULA
computePNF sen :: CASLFORMULA
sen = case CASLFORMULA
sen of 
 Negation nsen :: CASLFORMULA
nsen _ -> let 
   nsen' :: CASLFORMULA
nsen' = CASLFORMULA -> CASLFORMULA
computePNF CASLFORMULA
nsen
   in case CASLFORMULA
nsen' of 
       Quantification q :: QUANTIFIER
q vdecls :: [VAR_DECL]
vdecls qsen :: CASLFORMULA
qsen _ -> 
         QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification (QUANTIFIER -> QUANTIFIER
dualQuant QUANTIFIER
q) [VAR_DECL]
vdecls 
                        (CASLFORMULA -> CASLFORMULA
computePNF (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
qsen Range
nullRange) Range
nullRange
       _ -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
nsen' Range
nullRange
 Relation sen1 :: CASLFORMULA
sen1 Implication sen2 :: CASLFORMULA
sen2 _ -> let 
   sen1' :: CASLFORMULA
sen1' = CASLFORMULA -> CASLFORMULA
computePNF CASLFORMULA
sen1
   sen2' :: CASLFORMULA
sen2' = CASLFORMULA -> CASLFORMULA
computePNF CASLFORMULA
sen2
   in case CASLFORMULA
sen1' of 
      Quantification q :: QUANTIFIER
q vdecls :: [VAR_DECL]
vdecls qsen :: CASLFORMULA
qsen _ -> 
        QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification (QUANTIFIER -> QUANTIFIER
dualQuant QUANTIFIER
q) [VAR_DECL]
vdecls (CASLFORMULA -> CASLFORMULA
computePNF (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
qsen Relation
Implication CASLFORMULA
sen2 Range
nullRange) Range
nullRange
      _ -> case CASLFORMULA
sen2' of 
        Quantification q :: QUANTIFIER
q vdecls :: [VAR_DECL]
vdecls qsen :: CASLFORMULA
qsen _ -> 
          QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vdecls 
            (CASLFORMULA -> CASLFORMULA
computePNF (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen1' Relation
Implication CASLFORMULA
qsen Range
nullRange) Range
nullRange 
          -- recursive call to catch multiple quantifiers for sen2'
        _ -> -- no quantifications
          CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen1' Relation
Implication CASLFORMULA
sen2' Range
nullRange
 -- During parsing, "f2 if f1" is saved as "Relation f1 RevImpl f2 _"
 Relation sen1 :: CASLFORMULA
sen1 RevImpl sen2 :: CASLFORMULA
sen2 _ -> 
  CASLFORMULA -> CASLFORMULA
computePNF (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen1 Relation
Implication CASLFORMULA
sen2 Range
nullRange
 Quantification q :: QUANTIFIER
q vdecls :: [VAR_DECL]
vdecls qsen :: CASLFORMULA
qsen _ -> 
  QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vdecls (CASLFORMULA -> CASLFORMULA
computePNF CASLFORMULA
qsen) Range
nullRange
 Junction j :: Junctor
j sens :: [CASLFORMULA]
sens _ -> let
   sens' :: [CASLFORMULA]
sens' = (CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map CASLFORMULA -> CASLFORMULA
computePNF [CASLFORMULA]
sens
   collectQuants :: FORMULA f -> ([(QUANTIFIER, [VAR_DECL])], FORMULA f)
collectQuants s :: FORMULA f
s = case FORMULA f
s of 
                       Quantification q :: QUANTIFIER
q vd :: [VAR_DECL]
vd qs :: FORMULA f
qs _ -> let (vs :: [(QUANTIFIER, [VAR_DECL])]
vs, qs' :: FORMULA f
qs') = FORMULA f -> ([(QUANTIFIER, [VAR_DECL])], FORMULA f)
collectQuants FORMULA f
qs in ((QUANTIFIER
q,[VAR_DECL]
vd)(QUANTIFIER, [VAR_DECL])
-> [(QUANTIFIER, [VAR_DECL])] -> [(QUANTIFIER, [VAR_DECL])]
forall a. a -> [a] -> [a]
:[(QUANTIFIER, [VAR_DECL])]
vs, FORMULA f
qs')
                       _ -> ([], FORMULA f
s)
   (vdecls :: [(QUANTIFIER, [VAR_DECL])]
vdecls, sens'' :: [CASLFORMULA]
sens'') = (([(QUANTIFIER, [VAR_DECL])], [CASLFORMULA])
 -> CASLFORMULA -> ([(QUANTIFIER, [VAR_DECL])], [CASLFORMULA]))
-> ([(QUANTIFIER, [VAR_DECL])], [CASLFORMULA])
-> [CASLFORMULA]
-> ([(QUANTIFIER, [VAR_DECL])], [CASLFORMULA])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(vs :: [(QUANTIFIER, [VAR_DECL])]
vs, ss :: [CASLFORMULA]
ss) s :: CASLFORMULA
s -> case CASLFORMULA
s of 
                                           Quantification q :: QUANTIFIER
q vd :: [VAR_DECL]
vd qs :: CASLFORMULA
qs _ -> let (vs' :: [(QUANTIFIER, [VAR_DECL])]
vs', qs' :: CASLFORMULA
qs') = CASLFORMULA -> ([(QUANTIFIER, [VAR_DECL])], CASLFORMULA)
forall f. FORMULA f -> ([(QUANTIFIER, [VAR_DECL])], FORMULA f)
collectQuants CASLFORMULA
qs
                                                                          in ([(QUANTIFIER, [VAR_DECL])]
vs' [(QUANTIFIER, [VAR_DECL])]
-> [(QUANTIFIER, [VAR_DECL])] -> [(QUANTIFIER, [VAR_DECL])]
forall a. [a] -> [a] -> [a]
++ (QUANTIFIER
q,[VAR_DECL]
vd)(QUANTIFIER, [VAR_DECL])
-> [(QUANTIFIER, [VAR_DECL])] -> [(QUANTIFIER, [VAR_DECL])]
forall a. a -> [a] -> [a]
:[(QUANTIFIER, [VAR_DECL])]
vs, CASLFORMULA
qs'CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
:[CASLFORMULA]
ss)
                                           _ -> ([(QUANTIFIER, [VAR_DECL])]
vs, CASLFORMULA
sCASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
:[CASLFORMULA]
ss)) 
                    ([], []) [CASLFORMULA]
sens'
   qsen :: CASLFORMULA
qsen = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j ([CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a]
reverse [CASLFORMULA]
sens'') Range
nullRange
   rsen :: CASLFORMULA
rsen = (CASLFORMULA -> (QUANTIFIER, [VAR_DECL]) -> CASLFORMULA)
-> CASLFORMULA -> [(QUANTIFIER, [VAR_DECL])] -> CASLFORMULA
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\s :: CASLFORMULA
s (q :: QUANTIFIER
q, vd :: [VAR_DECL]
vd) -> QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vd CASLFORMULA
s Range
nullRange) CASLFORMULA
qsen [(QUANTIFIER, [VAR_DECL])]
vdecls 
  in CASLFORMULA
rsen
 _ -> CASLFORMULA
sen 

mapSentence :: CASLSign -> CASLFORMULA -> CASLFORMULA
mapSentence :: CASLSign -> CASLFORMULA -> CASLFORMULA
mapSentence _ =
 CASLFORMULA -> CASLFORMULA
computePNF (CASLFORMULA -> CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> CASLFORMULA
mkDistVars (CASLFORMULA -> CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> CASLFORMULA
preprocessSen

mapTheory :: (CASLSign, [Named CASLFORMULA]) ->
          Result (CASLSign, [Named CASLFORMULA])
mapTheory :: (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory (sig :: CASLSign
sig, nsens :: [Named CASLFORMULA]
nsens) = do
 let nsens' :: [Named CASLFORMULA]
nsens' = (Named CASLFORMULA -> Named CASLFORMULA)
-> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (\nsen :: Named CASLFORMULA
nsen -> Named CASLFORMULA
nsen{
                             sentence :: CASLFORMULA
sentence = CASLSign -> CASLFORMULA -> CASLFORMULA
mapSentence CASLSign
sig (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
nsen
                             }) 
              [Named CASLFORMULA]
nsens
 (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
sig, [Named CASLFORMULA]
nsens')