{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2VSERefine.hs
Description :  VSE refinement as comorphism
Copyright   :  (c) M. Codescu, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Mihai.Codescu@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CASL to VSE.
-}

module Comorphisms.CASL2VSERefine (CASL2VSERefine (..)) where

import Logic.Logic
import Logic.Comorphism

import CASL.Logic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Morphism

import VSE.Logic_VSE
import VSE.As
import VSE.Ana

import Common.AS_Annotation
import Common.Id
import Common.ProofTree
import Common.Result
import Common.Utils (number)
import Common.Lib.State
import qualified Common.Lib.MapSet as MapSet
import qualified Control.Monad.Fail as Fail

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

-- | The identity of the comorphism
data CASL2VSERefine = CASL2VSERefine deriving (Int -> CASL2VSERefine -> ShowS
[CASL2VSERefine] -> ShowS
CASL2VSERefine -> String
(Int -> CASL2VSERefine -> ShowS)
-> (CASL2VSERefine -> String)
-> ([CASL2VSERefine] -> ShowS)
-> Show CASL2VSERefine
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2VSERefine] -> ShowS
$cshowList :: [CASL2VSERefine] -> ShowS
show :: CASL2VSERefine -> String
$cshow :: CASL2VSERefine -> String
showsPrec :: Int -> CASL2VSERefine -> ShowS
$cshowsPrec :: Int -> CASL2VSERefine -> ShowS
Show)

instance Language CASL2VSERefine -- default definition is okay

instance Comorphism CASL2VSERefine
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               VSE ()
               VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS
               VSESign
               VSEMor
               Symbol RawSymbol () where
    sourceLogic :: CASL2VSERefine -> CASL
sourceLogic CASL2VSERefine = CASL
CASL
    sourceSublogic :: CASL2VSERefine -> CASL_Sublogics
sourceSublogic CASL2VSERefine = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.cFol
    targetLogic :: CASL2VSERefine -> VSE
targetLogic CASL2VSERefine = VSE
VSE
    mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe ()
mapSublogic CASL2VSERefine _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    map_theory :: CASL2VSERefine
-> (CASLSign, [Named CASLFORMULA])
-> Result (VSESign, [Named Sentence])
map_theory CASL2VSERefine = (CASLSign, [Named CASLFORMULA])
-> Result (VSESign, [Named Sentence])
mapCASLTheory
    map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor
map_morphism CASL2VSERefine = VSEMor -> Result VSEMor
forall (m :: * -> *) a. Monad m => a -> m a
return (VSEMor -> Result VSEMor)
-> (CASLMor -> VSEMor) -> CASLMor -> Result VSEMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLMor -> VSEMor
mapMor
    map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence
map_sentence CASL2VSERefine _ = String -> CASLFORMULA -> Result Sentence
forall a. HasCallStack => String -> a
error "map sen nyi" -- return. mapCASSen
    map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2VSERefine = String -> CASLSign -> Symbol -> Set Symbol
forall a. HasCallStack => String -> a
error "map symbol nyi"
    has_model_expansion :: CASL2VSERefine -> Bool
has_model_expansion CASL2VSERefine = Bool
True
        -- check these 3, but should be fine
    is_weakly_amalgamable :: CASL2VSERefine -> Bool
is_weakly_amalgamable CASL2VSERefine = Bool
True
    isInclusionComorphism :: CASL2VSERefine -> Bool
isInclusionComorphism CASL2VSERefine = Bool
False

mapCASLTheory :: (CASLSign, [Named CASLFORMULA]) ->
                 Result (VSESign, [Named Sentence])
mapCASLTheory :: (CASLSign, [Named CASLFORMULA])
-> Result (VSESign, [Named Sentence])
mapCASLTheory (sig :: CASLSign
sig, n_sens :: [Named CASLFORMULA]
n_sens) =
  let (tsig :: VSESign
tsig, genAx :: [Named Sentence]
genAx) = CASLSign -> (VSESign, [Named Sentence])
mapSig CASLSign
sig
      tsens :: [Named Sentence]
tsens = (Named CASLFORMULA -> Named Sentence)
-> [Named CASLFORMULA] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Named CASLFORMULA -> Named Sentence
mapNamedSen [Named CASLFORMULA]
n_sens
      allSens :: [Named Sentence]
allSens = [Named Sentence]
tsens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
genAx
  in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Diagnosis] -> Bool) -> [Diagnosis] -> Bool
forall a b. (a -> b) -> a -> b
$ VSESign -> [Named Sentence] -> [Diagnosis]
forall f e. Sign f e -> [Named Sentence] -> [Diagnosis]
checkCases VSESign
tsig [Named Sentence]
allSens then (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (VSESign
tsig, [Named Sentence]
allSens) else
     String -> Result (VSESign, [Named Sentence])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "case error in signature"

mapSig :: CASLSign -> (VSESign, [Named Sentence])
mapSig :: CASLSign -> (VSESign, [Named Sentence])
mapSig sign :: CASLSign
sign =
 let wrapSort :: ([(Id, Profile)], [Named Sentence])
-> Id -> ([(Id, Profile)], [Named Sentence])
wrapSort (procsym :: [(Id, Profile)]
procsym, axs :: [Named Sentence]
axs) s :: Id
s = let
        restrName :: Id
restrName = Id -> Id
gnRestrName Id
s
        eqName :: Id
eqName = Id -> Id
gnEqName Id
s
        sProcs :: [(Id, Profile)]
sProcs = [(Id
restrName, [Procparam] -> Maybe Id -> Profile
Profile [Paramkind -> Id -> Procparam
Procparam Paramkind
In Id
s] Maybe Id
forall a. Maybe a
Nothing),
                   (Id
eqName,
                     [Procparam] -> Maybe Id -> Profile
Profile [Paramkind -> Id -> Procparam
Procparam Paramkind
In Id
s, Paramkind -> Id -> Procparam
Procparam Paramkind
In Id
s]
                             (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
uBoolean))]
        varx :: TERM f
varx = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "x") Id
s Range
nullRange
        vary :: TERM f
vary = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "y") Id
s Range
nullRange
        varz :: TERM f
varz = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "z") Id
s Range
nullRange
        varb :: TERM f
varb = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "b")
                        Id
uBoolean Range
nullRange
        varb1 :: TERM f
varb1 = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "b1")
                        Id
uBoolean Range
nullRange
        varb2 :: TERM f
varb2 = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "b2")
                        Id
uBoolean Range
nullRange
        sSens :: [Named Sentence]
sSens = [ String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_termination_eq_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s) (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$
                  QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [[VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> VAR
genToken "x",
                                                      String -> VAR
genToken "y"] Id
s Range
nullRange
                                           , [VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> VAR
genToken "b"]
                                              Id
uBoolean Range
nullRange]
                  (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                  ([Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct [
                   Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (CASLFORMULA -> PlainProgram
Call
                          (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
restrName
                                         ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
                            [TERM ()
forall f. TERM f
varx] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange,
                   Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (CASLFORMULA -> PlainProgram
Call
                          (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
restrName
                                         ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
                            [TERM ()
forall f. TERM f
vary] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange
                   ])
                  (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                         (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "b")
                          (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
s)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
varx, TERM ()
forall f. TERM f
vary] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange)
                  ) Range
nullRange ,
                  String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_refl_eq_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s) (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$
                  QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [[VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> VAR
genToken "x"] Id
s Range
nullRange
                                           , [VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> VAR
genToken "b"]
                                              Id
uBoolean Range
nullRange]
                  (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                  (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (CASLFORMULA -> PlainProgram
Call
                          (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
restrName
                                          ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange ) Range
nullRange)
                            [TERM ()
forall f. TERM f
varx] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange)

                     (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "b")
                          (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
s)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
varx, TERM ()
forall f. TERM f
varx] Range
nullRange))
                        Range
nullRange)
                      (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
                         TERM (Ranged VSEforms)
forall f. TERM f
varb
                         (OP_SYMB
-> [TERM (Ranged VSEforms)] -> Range -> TERM (Ranged VSEforms)
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
uTrue
                                          (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total []
                                            Id
uBoolean
                                           Range
nullRange) Range
nullRange)
                          [] Range
nullRange)
                      )) Range
nullRange)
                  ) Range
nullRange
                 , String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_sym_eq_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s) (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$
                  QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [[VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> VAR
genToken "x",
                                                      String -> VAR
genToken "y"] Id
s Range
nullRange
                                           , [VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> VAR
genToken "b1",
                                                      String -> VAR
genToken "b2"]
                                              Id
uBoolean Range
nullRange]
                  (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                   ([Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct [
                   Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (CASLFORMULA -> PlainProgram
Call
                          (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
restrName
                                         ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
                            [TERM ()
forall f. TERM f
varx] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange,
                   Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (CASLFORMULA -> PlainProgram
Call
                          (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
restrName
                                         ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
                            [TERM ()
forall f. TERM f
vary] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange,
                    Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "b1")
                          (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
s)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
varx, TERM ()
forall f. TERM f
vary] Range
nullRange))
                          Range
nullRange)
                      (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM (Ranged VSEforms)
forall f. TERM f
varb1 TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
                     ) Range
nullRange
                   ])
                     (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "b2")
                          (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
s)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
vary, TERM ()
forall f. TERM f
varx] Range
nullRange))
                          Range
nullRange)
                      (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM (Ranged VSEforms)
forall f. TERM f
varb2 TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
                     ) Range
nullRange)
                  ) Range
nullRange
                  , String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_trans_eq_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s) (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$
                  QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [[VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> VAR
genToken "x",
                                                      String -> VAR
genToken "y",
                                                      String -> VAR
genToken "z"] Id
s Range
nullRange
                                           , [VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> VAR
genToken "b1",
                                                      String -> VAR
genToken "b2",
                                                      String -> VAR
genToken "b"]
                                              Id
uBoolean Range
nullRange]
                  (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                   ([Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct [
                   Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (CASLFORMULA -> PlainProgram
Call
                          (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
restrName
                                        ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
                            [TERM ()
forall f. TERM f
varx] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange,
                   Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (CASLFORMULA -> PlainProgram
Call
                          (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
restrName
                                        ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange ) Range
nullRange)
                            [TERM ()
forall f. TERM f
vary] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange,
                   Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (CASLFORMULA -> PlainProgram
Call
                          (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
restrName
                                        ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange ) Range
nullRange)
                            [TERM ()
forall f. TERM f
varz] Range
nullRange))
                          Range
nullRange)
                      Sentence
forall f. FORMULA f
trueForm ) Range
nullRange,
                    Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "b1")
                          (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
s)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
varx, TERM ()
forall f. TERM f
vary] Range
nullRange))
                          Range
nullRange)
                      (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM (Ranged VSEforms)
forall f. TERM f
varb1 TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
                      ) Range
nullRange,
                    Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "b2")
                          (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
s)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
vary, TERM ()
forall f. TERM f
varz] Range
nullRange))
                          Range
nullRange)
                      (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM (Ranged VSEforms)
forall f. TERM f
varb2 TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
                     ) Range
nullRange
                   ])
                     (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "b")
                          (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
s)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
varx, TERM ()
forall f. TERM f
varz] Range
nullRange))
                          Range
nullRange)
                      (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM (Ranged VSEforms)
forall f. TERM f
varb TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
                     ) Range
nullRange)
                  ) Range
nullRange ]
                                          in
        ([(Id, Profile)]
sProcs [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
procsym, [Named Sentence]
sSens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
axs)
     (sortProcs :: [(Id, Profile)]
sortProcs, sortSens :: [Named Sentence]
sortSens) = (([(Id, Profile)], [Named Sentence])
 -> Id -> ([(Id, Profile)], [Named Sentence]))
-> ([(Id, Profile)], [Named Sentence])
-> [Id]
-> ([(Id, Profile)], [Named Sentence])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([(Id, Profile)], [Named Sentence])
-> Id -> ([(Id, Profile)], [Named Sentence])
wrapSort ([], []) ([Id] -> ([(Id, Profile)], [Named Sentence]))
-> [Id] -> ([(Id, Profile)], [Named Sentence])
forall a b. (a -> b) -> a -> b
$
                                        Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ CASLSign -> Set Id
forall f e. Sign f e -> Set Id
sortSet CASLSign
sign
     wrapOp :: ([(Id, Profile)], [Named Sentence])
-> (Id, [OpType]) -> ([(Id, Profile)], [Named Sentence])
wrapOp (procsym :: [(Id, Profile)]
procsym, axs :: [Named Sentence]
axs) (i :: Id
i, opTypes :: [OpType]
opTypes) = let
       funName :: Id
funName = Id -> Id
mkGenName Id
i
       fProcs :: [(Id, Profile)]
fProcs = (OpType -> (Id, Profile)) -> [OpType] -> [(Id, Profile)]
forall a b. (a -> b) -> [a] -> [b]
map (\ profile :: OpType
profile ->
                       (Id
funName,
                        [Procparam] -> Maybe Id -> Profile
Profile
                           ((Id -> Procparam) -> [Id] -> [Procparam]
forall a b. (a -> b) -> [a] -> [b]
map (Paramkind -> Id -> Procparam
Procparam Paramkind
In) ([Id] -> [Procparam]) -> [Id] -> [Procparam]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
profile)
                           (Id -> Maybe Id
forall a. a -> Maybe a
Just (Id -> Maybe Id) -> Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ OpType -> Id
opRes OpType
profile))) [OpType]
opTypes
       opTypeSens :: OpType -> [Named Sentence]
opTypeSens (OpType _ w :: [Id]
w s :: Id
s) = let
          xtokens :: [VAR]
xtokens = ((Id, Int) -> VAR) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, ii :: Int
ii) -> String -> Int -> VAR
genNumVar "x" Int
ii) ([(Id, Int)] -> [VAR]) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          xvars :: [TERM f]
xvars = ((Id, Int) -> TERM f) -> [(Id, Int)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (
                  \ (si :: Id
si, ii :: Int
ii) ->
                  VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
ii )
                  Id
si Range
nullRange ) ([(Id, Int)] -> [TERM f]) -> [(Id, Int)] -> [TERM f]
forall a b. (a -> b) -> a -> b
$
                   [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          yvars :: [TERM f]
yvars = ((Id, Int) -> TERM f) -> [(Id, Int)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (
                  \ (si :: Id
si, ii :: Int
ii) ->
                  VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "y" Int
ii )
                  Id
si Range
nullRange ) ([(Id, Int)] -> [TERM f]) -> [(Id, Int)] -> [TERM f]
forall a b. (a -> b) -> a -> b
$
                   [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          ytokens :: [VAR]
ytokens = ((Id, Int) -> VAR) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, ii :: Int
ii) -> String -> Int -> VAR
genNumVar "y" Int
ii) ([(Id, Int)] -> [VAR]) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          btokens :: [VAR]
btokens = ((Id, Int) -> VAR) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, ii :: Int
ii) -> String -> Int -> VAR
genNumVar "b" Int
ii) ([(Id, Int)] -> [VAR]) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          xtoken :: VAR
xtoken = String -> VAR
genToken "x"
          ytoken :: VAR
ytoken = String -> VAR
genToken "y"
          btoken :: VAR
btoken = String -> VAR
genToken "b"
          xvar :: TERM f
xvar = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "x")
                  Id
s Range
nullRange
          yvar :: TERM f
yvar = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "y")
                  Id
s Range
nullRange
          bvar :: TERM f
bvar = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "b")
                  Id
uBoolean Range
nullRange
          congrF :: [Named Sentence]
congrF = [String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$
                  QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal ([[VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
xtoken, VAR
ytoken] Id
s
                                            Range
nullRange
                                           , [VAR] -> Id -> Range -> VAR_DECL
Var_decl (VAR
btoken VAR -> [VAR] -> [VAR]
forall a. a -> [a] -> [a]
: [VAR]
btokens)
                                              Id
uBoolean Range
nullRange
                                            ] [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ (((VAR, VAR), Id) -> VAR_DECL) -> [((VAR, VAR), Id)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map
                                            (\ ((t1 :: VAR
t1, t2 :: VAR
t2), si :: Id
si) ->
                                             [VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
t1, VAR
t2] Id
si
                                             Range
nullRange)
                                             ([(VAR, VAR)] -> [Id] -> [((VAR, VAR), Id)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([VAR] -> [VAR] -> [(VAR, VAR)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VAR]
xtokens [VAR]
ytokens) [Id]
w)
                                            )
               (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                  ([Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct
                   (((Id, Int) -> [Sentence]) -> [(Id, Int)] -> [Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (si :: Id
si, ii :: Int
ii) -> let
                     xv :: TERM f
xv = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
ii)
                           Id
si Range
nullRange
                     yv :: TERM f
yv = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "y" Int
ii)
                           Id
si Range
nullRange
                     varbi :: VAR
varbi = String -> Int -> VAR
genNumVar "b" Int
ii
                     bi1 :: TERM f
bi1 = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "b" Int
ii)
                            Id
uBoolean Range
nullRange
                                          in
                     [Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ( BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                          (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                (CASLFORMULA -> PlainProgram
Call
                                 (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                   (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                    (Id -> Id
gnRestrName Id
si)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type [Id
si] Range
nullRange) Range
nullRange )
                                   [TERM ()
forall f. TERM f
xv] Range
nullRange))
                               Range
nullRange)
                          Sentence
forall f. FORMULA f
trueForm ) Range
nullRange ,
                       Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ( BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                              (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                (CASLFORMULA -> PlainProgram
Call
                                 (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                   (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                    (Id -> Id
gnRestrName Id
si)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type [Id
si] Range
nullRange) Range
nullRange)
                                   [TERM ()
forall f. TERM f
yv] Range
nullRange))
                               Range
nullRange)
                          Sentence
forall f. FORMULA f
trueForm ) Range
nullRange ,
                       Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Ranged VSEforms
forall a. a -> Ranged a
mkRanged (VSEforms -> Ranged VSEforms) -> VSEforms -> Ranged VSEforms
forall a b. (a -> b) -> a -> b
$ BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                              (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                (VAR -> TERM () -> PlainProgram
Assign VAR
varbi
                            (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
si)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
si, Id
si] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
xv, TERM ()
forall f. TERM f
yv] Range
nullRange))
                                Range
nullRange)
                              (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM (Ranged VSEforms)
forall f. TERM f
bi1 TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
                     ] ) ([(Id, Int)] -> [Sentence]) -> [(Id, Int)] -> [Sentence]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w )
                   ) -- hypothesis
                  (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (
                     BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond

                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                        (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "x")
                            (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
mkGenName Id
i)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
w Id
s Range
nullRange)
                              Range
nullRange)
                             [TERM ()]
forall f. [TERM f]
xvars Range
nullRange))
                       Range
nullRange)
                      (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (
                         BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                         (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "y")
                            (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
mkGenName Id
i)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
w Id
s Range
nullRange)
                              Range
nullRange)
                             [TERM ()]
forall f. [TERM f]
yvars Range
nullRange))
                       Range
nullRange)
                       (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$
                        VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (
                          BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                          ( PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                            (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "b")
                            (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
s)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
xvar, TERM ()
forall f. TERM f
yvar] Range
nullRange))
                          Range
nullRange
                          )
                          (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM (Ranged VSEforms)
forall f. TERM f
bvar TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
                        ) Range
nullRange)
                        ) Range
nullRange)
                   ) Range
nullRange) -- conclusion
                  )
               Range
nullRange
              ]
          termF :: [Named Sentence]
termF = if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
w then
                   [ String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal
                     ([VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
xtoken] Id
s Range
nullRange
                      VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: ((VAR, Id) -> VAR_DECL) -> [(VAR, Id)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t1 :: VAR
t1, si :: Id
si) -> [VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
t1] Id
si Range
nullRange)
                        ([VAR] -> [Id] -> [(VAR, Id)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VAR]
xtokens [Id]
w))
                     (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                        ([Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct
                         (((Id, Int) -> [Sentence]) -> [(Id, Int)] -> [Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (si :: Id
si, ii :: Int
ii) -> let
                     xv :: TERM f
xv = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
ii) Id
si Range
nullRange in
                     [Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ( BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                          (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                (CASLFORMULA -> PlainProgram
Call
                                 (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                   (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                    (Id -> Id
gnRestrName Id
si)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type ([Id]
w [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id
s]) Range
nullRange) Range
nullRange)
                                   [TERM ()
forall f. TERM f
xv] Range
nullRange))
                               Range
nullRange)
                          Sentence
forall f. FORMULA f
trueForm ) Range
nullRange
                     ] ) ([(Id, Int)] -> [Sentence]) -> [(Id, Int)] -> [Sentence]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w )
                        )
                        (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                       (
                       BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                       (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                         (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "x")
                            (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
mkGenName Id
i)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
w Id
s Range
nullRange)
                              Range
nullRange)
                             [TERM ()]
forall f. [TERM f]
xvars Range
nullRange))
                        Range
nullRange)
                       (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$
                         VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                         (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                          (CASLFORMULA -> PlainProgram
Call (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                              (Id -> Id
gnRestrName Id
s)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
                              [TERM ()
forall f. TERM f
xvar] Range
nullRange))
                                             Range
nullRange)
                          Sentence
forall f. FORMULA f
trueForm
                          )
                         Range
nullRange)
                       ) Range
nullRange)
                       )
                     Range
nullRange
                   ]
                  else
                   [String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal
                                   [[VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
xtoken] Id
s Range
nullRange]
                     (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                       (
                       BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                       (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                         (VAR -> TERM () -> PlainProgram
Assign (String -> VAR
genToken "x")
                            (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
mkGenName Id
i)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [] Id
s Range
nullRange)
                              Range
nullRange)
                             [] Range
nullRange))
                        Range
nullRange)
                       (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$
                         VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                         (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                          (CASLFORMULA -> PlainProgram
Call (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                              (Id -> Id
gnRestrName Id
s)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
                              [TERM ()
forall f. TERM f
xvar] Range
nullRange))
                                             Range
nullRange)
                          Sentence
forall f. FORMULA f
trueForm
                          )
                         Range
nullRange)
                       ) Range
nullRange) Range
nullRange]
                                   in
         if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
w then [Named Sentence]
termF else [Named Sentence]
congrF [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
termF

       fSens :: [Named Sentence]
fSens = (OpType -> [Named Sentence]) -> [OpType] -> [Named Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap OpType -> [Named Sentence]
opTypeSens [OpType]
opTypes
                                            in
       ([(Id, Profile)]
procsym [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
fProcs, [Named Sentence]
axs [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
fSens)
     (opProcs :: [(Id, Profile)]
opProcs, opSens :: [Named Sentence]
opSens) = (([(Id, Profile)], [Named Sentence])
 -> (Id, [OpType]) -> ([(Id, Profile)], [Named Sentence]))
-> ([(Id, Profile)], [Named Sentence])
-> [(Id, [OpType])]
-> ([(Id, Profile)], [Named Sentence])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([(Id, Profile)], [Named Sentence])
-> (Id, [OpType]) -> ([(Id, Profile)], [Named Sentence])
wrapOp ([], []) ([(Id, [OpType])] -> ([(Id, Profile)], [Named Sentence]))
-> [(Id, [OpType])] -> ([(Id, Profile)], [Named Sentence])
forall a b. (a -> b) -> a -> b
$
                                        MapSet Id OpType -> [(Id, [OpType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (MapSet Id OpType -> [(Id, [OpType])])
-> MapSet Id OpType -> [(Id, [OpType])]
forall a b. (a -> b) -> a -> b
$ CASLSign -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap CASLSign
sign
     wrapPred :: ([(Id, Profile)], [Named Sentence])
-> (Id, [PredType]) -> ([(Id, Profile)], [Named Sentence])
wrapPred (procsym :: [(Id, Profile)]
procsym, axs :: [Named Sentence]
axs) (i :: Id
i, predTypes :: [PredType]
predTypes) = let
       procName :: Id
procName = Id -> Id
mkGenName Id
i
       pProcs :: [(Id, Profile)]
pProcs = (PredType -> (Id, Profile)) -> [PredType] -> [(Id, Profile)]
forall a b. (a -> b) -> [a] -> [b]
map (\ profile :: PredType
profile -> (Id
procName,
                        [Procparam] -> Maybe Id -> Profile
Profile
                           ((Id -> Procparam) -> [Id] -> [Procparam]
forall a b. (a -> b) -> [a] -> [b]
map (Paramkind -> Id -> Procparam
Procparam Paramkind
In) ([Id] -> [Procparam]) -> [Id] -> [Procparam]
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
profile)
                           (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
uBoolean))) [PredType]
predTypes
       predTypeSens :: PredType -> [Named Sentence]
predTypeSens (PredType w :: [Id]
w) = let
          xtokens :: [VAR]
xtokens = ((Id, Int) -> VAR) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, ii :: Int
ii) -> String -> Int -> VAR
genNumVar "x" Int
ii) ([(Id, Int)] -> [VAR]) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          xvars :: [TERM f]
xvars = ((Id, Int) -> TERM f) -> [(Id, Int)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (
                  \ (si :: Id
si, ii :: Int
ii) ->
                  VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
ii )
                  Id
si Range
nullRange ) ([(Id, Int)] -> [TERM f]) -> [(Id, Int)] -> [TERM f]
forall a b. (a -> b) -> a -> b
$
                   [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          ytokens :: [VAR]
ytokens = ((Id, Int) -> VAR) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, ii :: Int
ii) -> String -> Int -> VAR
genNumVar "y" Int
ii) ([(Id, Int)] -> [VAR]) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          btokens :: [VAR]
btokens = ((Id, Int) -> VAR) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, ii :: Int
ii) -> String -> Int -> VAR
genNumVar "b" Int
ii) ([(Id, Int)] -> [VAR]) -> [(Id, Int)] -> [VAR]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w
          btoken :: VAR
btoken = String -> VAR
genToken "b"
          r1 :: VAR
r1 = String -> VAR
genToken "r1"
          r2 :: VAR
r2 = String -> VAR
genToken "r2"
          rvar1 :: TERM f
rvar1 = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "r1")
                  Id
uBoolean Range
nullRange
          rvar2 :: TERM f
rvar2 = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
genToken "r2")
                  Id
uBoolean Range
nullRange
          congrP :: [Named Sentence]
congrP = [String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal
              ([VAR] -> Id -> Range -> VAR_DECL
Var_decl (VAR
btoken VAR -> [VAR] -> [VAR]
forall a. a -> [a] -> [a]
: VAR
r1 VAR -> [VAR] -> [VAR]
forall a. a -> [a] -> [a]
: VAR
r2 VAR -> [VAR] -> [VAR]
forall a. a -> [a] -> [a]
: [VAR]
btokens) Id
uBoolean Range
nullRange
               VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: (((VAR, VAR), Id) -> VAR_DECL) -> [((VAR, VAR), Id)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ ((t1 :: VAR
t1, t2 :: VAR
t2), si :: Id
si) -> [VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
t1, VAR
t2] Id
si Range
nullRange)
                 ([(VAR, VAR)] -> [Id] -> [((VAR, VAR), Id)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([VAR] -> [VAR] -> [(VAR, VAR)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VAR]
xtokens [VAR]
ytokens) [Id]
w))
               (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                  ([Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct
                   (((Id, Int) -> [Sentence]) -> [(Id, Int)] -> [Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (si :: Id
si, ii :: Int
ii) -> let
                     xv :: TERM f
xv = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
ii)
                           Id
si Range
nullRange
                     yv :: TERM f
yv = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "y" Int
ii)
                           Id
si Range
nullRange
                     bi1 :: TERM f
bi1 = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "b" Int
ii)
                            Id
uBoolean Range
nullRange
                                          in
                     [Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ( BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                          (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                (CASLFORMULA -> PlainProgram
Call
                                 (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                   (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                    (Id -> Id
gnRestrName Id
si)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type [Id
si] Range
nullRange) Range
nullRange)
                                   [TERM ()
forall f. TERM f
xv] Range
nullRange))
                               Range
nullRange)
                          Sentence
forall f. FORMULA f
trueForm ) Range
nullRange ,
                       Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ( BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                              (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                (CASLFORMULA -> PlainProgram
Call
                                 (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                   (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                    (Id -> Id
gnRestrName Id
si)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type [Id
si] Range
nullRange) Range
nullRange)
                                   [TERM ()
forall f. TERM f
yv] Range
nullRange))
                               Range
nullRange)
                          Sentence
forall f. FORMULA f
trueForm ) Range
nullRange ,
                       Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Ranged VSEforms
forall a. a -> Ranged a
mkRanged (VSEforms -> Ranged VSEforms) -> VSEforms -> Ranged VSEforms
forall a b. (a -> b) -> a -> b
$ BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                              (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                (VAR -> TERM () -> PlainProgram
Assign (String -> Int -> VAR
genNumVar "b" Int
ii)
                            (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                             (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                               (Id -> Id
gnEqName Id
si)
                               (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
si, Id
si] Id
uBoolean Range
nullRange)
                              Range
nullRange)
                             [TERM ()
forall f. TERM f
xv, TERM ()
forall f. TERM f
yv] Range
nullRange))
                               Range
nullRange)
                              (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
                                  TERM (Ranged VSEforms)
forall f. TERM f
bi1 TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
                     ] ) ([(Id, Int)] -> [Sentence]) -> [(Id, Int)] -> [Sentence]
forall a b. (a -> b) -> a -> b
$
                    [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w )
                   ) -- hypothesis
                  (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (
                     BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (CASLFORMULA -> PlainProgram
Call (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                   (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name (Id -> Id
mkGenName Id
i)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type ([Id]
w [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id
uBoolean]) Range
nullRange)
                                    Range
nullRange)
                                   (((Id, Int) -> TERM ()) -> [(Id, Int)] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map (
                  \ (si :: Id
si, ii :: Int
ii) ->
                  VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
ii )
                  Id
si Range
nullRange )
                   ([Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w) [TERM ()] -> [TERM ()] -> [TERM ()]
forall a. [a] -> [a] -> [a]
++ [TERM ()
forall f. TERM f
rvar1]) Range
nullRange)) Range
nullRange)
                      (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (
                         BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (CASLFORMULA -> PlainProgram
Call (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                   (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name (Id -> Id
mkGenName Id
i)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type ([Id]
w [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id
uBoolean]) Range
nullRange)
                                     Range
nullRange)
                                   (((Id, Int) -> TERM ()) -> [(Id, Int)] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map (
                  \ (si :: Id
si, ii :: Int
ii) ->
                  VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "y" Int
ii )
                  Id
si Range
nullRange )
                   ([Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w) [TERM ()] -> [TERM ()] -> [TERM ()]
forall a. [a] -> [a] -> [a]
++ [TERM ()
forall f. TERM f
rvar2]) Range
nullRange)) Range
nullRange)
                       (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
                                  TERM (Ranged VSEforms)
forall f. TERM f
rvar1
                                  TERM (Ranged VSEforms)
forall f. TERM f
rvar2
                          )
                        ) Range
nullRange)
                   ) Range
nullRange) -- conclusion
                  )
               Range
nullRange
              ]
          termP :: [Named Sentence]
termP = [ String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal
                                     (((VAR, Id) -> VAR_DECL) -> [(VAR, Id)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map
                                             (\ (t1 :: VAR
t1, si :: Id
si) ->
                                              [VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
t1] Id
si
                                              Range
nullRange)
                                              ([VAR] -> [Id] -> [(VAR, Id)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VAR]
xtokens [Id]
w)
                                      [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ [[VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
r1]
                                              Id
uBoolean Range
nullRange])
                      (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                         ([Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct
                          (((Id, Int) -> [Sentence]) -> [(Id, Int)] -> [Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (si :: Id
si, ii :: Int
ii) -> let
                      xv :: TERM f
xv = VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
ii)
                            Id
si Range
nullRange
                                           in
                      [Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ( BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                           (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                 (CASLFORMULA -> PlainProgram
Call
                                  (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                    (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                     (Id -> Id
gnRestrName Id
si)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type [Id
si] Range
nullRange) Range
nullRange)
                                    [TERM ()
forall f. TERM f
xv] Range
nullRange))
                                Range
nullRange)
                           Sentence
forall f. FORMULA f
trueForm ) Range
nullRange
                      ] ) ([(Id, Int)] -> [Sentence]) -> [(Id, Int)] -> [Sentence]
forall a b. (a -> b) -> a -> b
$
                     [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
w )
                          )
                         (Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                        (
                        BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                        (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                          (CASLFORMULA -> PlainProgram
Call (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name (Id -> Id
mkGenName Id
i)
                                    ([Id] -> Range -> PRED_TYPE
Pred_type ([Id]
w [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id
uBoolean]) Range
nullRange)
                                     Range
nullRange)
                                 ([TERM ()]
forall f. [TERM f]
xvars [TERM ()] -> [TERM ()] -> [TERM ()]
forall a. [a] -> [a] -> [a]
++ [TERM ()
forall f. TERM f
rvar1])
                           Range
nullRange))
                         Range
nullRange)
                        Sentence
forall f. FORMULA f
trueForm
                        ) Range
nullRange)
                        )
                      Range
nullRange
                    ]
                                   in [Named Sentence]
congrP [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
termP
       pSens :: [Named Sentence]
pSens = (PredType -> [Named Sentence]) -> [PredType] -> [Named Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PredType -> [Named Sentence]
predTypeSens [PredType]
predTypes
                                                in
      ([(Id, Profile)]
procsym [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
pProcs, [Named Sentence]
axs [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
pSens)
     (predProcs :: [(Id, Profile)]
predProcs, predSens :: [Named Sentence]
predSens) = (([(Id, Profile)], [Named Sentence])
 -> (Id, [PredType]) -> ([(Id, Profile)], [Named Sentence]))
-> ([(Id, Profile)], [Named Sentence])
-> [(Id, [PredType])]
-> ([(Id, Profile)], [Named Sentence])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([(Id, Profile)], [Named Sentence])
-> (Id, [PredType]) -> ([(Id, Profile)], [Named Sentence])
wrapPred ([], []) ([(Id, [PredType])] -> ([(Id, Profile)], [Named Sentence]))
-> [(Id, [PredType])] -> ([(Id, Profile)], [Named Sentence])
forall a b. (a -> b) -> a -> b
$
                                        MapSet Id PredType -> [(Id, [PredType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (MapSet Id PredType -> [(Id, [PredType])])
-> MapSet Id PredType -> [(Id, [PredType])]
forall a b. (a -> b) -> a -> b
$ CASLSign -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap CASLSign
sign
     procs :: Procs
procs = Map Id Profile -> Procs
Procs (Map Id Profile -> Procs) -> Map Id Profile -> Procs
forall a b. (a -> b) -> a -> b
$ [(Id, Profile)] -> Map Id Profile
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, Profile)]
sortProcs [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
opProcs [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
predProcs)
     newPreds :: MapSet Id PredType
newPreds = Procs -> MapSet Id PredType
procsToPredMap Procs
procs
     newOps :: MapSet Id OpType
newOps = Procs -> MapSet Id OpType
procsToOpMap Procs
procs
 in (CASLSign
sign { opMap :: MapSet Id OpType
opMap = MapSet Id OpType
newOps,
           predMap :: MapSet Id PredType
predMap = MapSet Id PredType
newPreds,
           extendedInfo :: Procs
extendedInfo = Procs
procs,
           sentences :: [Named Sentence]
sentences = [] }, [Named Sentence]
sortSens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
opSens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
predSens)

mapNamedSen :: Named CASLFORMULA -> Named Sentence
mapNamedSen :: Named CASLFORMULA -> Named Sentence
mapNamedSen n_sen :: Named CASLFORMULA
n_sen = let
 sen :: CASLFORMULA
sen = Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
n_sen
 trans :: Sentence
trans = CASLFORMULA -> Sentence
mapCASLSen CASLFORMULA
sen
                    in
 Named CASLFORMULA
n_sen {sentence :: Sentence
sentence = Sentence
trans}

mapMor :: CASLMor -> VSEMor
mapMor :: CASLMor -> VSEMor
mapMor m :: CASLMor
m = let
  (om :: Op_map
om, pm :: Pred_map
pm) = CASLMor -> (Op_map, Pred_map)
vseMorExt CASLMor
m
  in CASLMor
m
  { msource :: VSESign
msource = (VSESign, [Named Sentence]) -> VSESign
forall a b. (a, b) -> a
fst ((VSESign, [Named Sentence]) -> VSESign)
-> (VSESign, [Named Sentence]) -> VSESign
forall a b. (a -> b) -> a -> b
$ CASLSign -> (VSESign, [Named Sentence])
mapSig (CASLSign -> (VSESign, [Named Sentence]))
-> CASLSign -> (VSESign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
msource CASLMor
m
  , mtarget :: VSESign
mtarget = (VSESign, [Named Sentence]) -> VSESign
forall a b. (a, b) -> a
fst ((VSESign, [Named Sentence]) -> VSESign)
-> (VSESign, [Named Sentence]) -> VSESign
forall a b. (a -> b) -> a -> b
$ CASLSign -> (VSESign, [Named Sentence])
mapSig (CASLSign -> (VSESign, [Named Sentence]))
-> CASLSign -> (VSESign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CASLMor
m
  , op_map :: Op_map
op_map = Op_map
om
  , pred_map :: Pred_map
pred_map = Pred_map
pm
  , extended_map :: VSEMorExt
extended_map = VSEMorExt
forall e. DefMorExt e
emptyMorExt
  }

mapCASLSen :: CASLFORMULA -> Sentence
mapCASLSen :: CASLFORMULA -> Sentence
mapCASLSen f :: CASLFORMULA
f = let
 (sen :: Sentence
sen, (_i :: Int
_i, vars :: VarSet
vars)) = State (Int, VarSet) Sentence
-> (Int, VarSet) -> (Sentence, (Int, VarSet))
forall s a. State s a -> s -> (a, s)
runState (CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux CASLFORMULA
f) (0, VarSet
forall a. Set a
Set.empty)
               in
 case CASLFORMULA
f of
  Sort_gen_ax _ _ -> Sentence
sen
  _ -> VarSet -> Sentence -> Sentence
addQuantifiers VarSet
vars Sentence
sen

addQuantifiers :: VarSet -> Sentence -> Sentence
addQuantifiers :: VarSet -> Sentence -> Sentence
addQuantifiers vars :: VarSet
vars sen :: Sentence
sen =
 QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal
  (((VAR, Id) -> VAR_DECL) -> [(VAR, Id)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (v :: VAR
v, s :: Id
s) -> [VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
v] Id
s Range
nullRange) ([(VAR, Id)] -> [VAR_DECL]) -> [(VAR, Id)] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ VarSet -> [(VAR, Id)]
forall a. Set a -> [a]
Set.toList VarSet
vars) Sentence
sen Range
nullRange

mapCASLSenAux :: CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux :: CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux f :: CASLFORMULA
f = case CASLFORMULA
f of
  Sort_gen_ax constrs :: [Constraint]
constrs isFree :: Bool
isFree -> do
   let
    (genSorts :: [Id]
genSorts, _, _ ) = [Constraint] -> ([Id], [OP_SYMB], [(Id, Id)])
recover_Sort_gen_ax [Constraint]
constrs
    toProcs :: (OP_SYMB, b) -> (OP_SYMB, b)
toProcs (Op_name _, _) = String -> (OP_SYMB, b)
forall a. HasCallStack => String -> a
error "must be qual names"
    toProcs (Qual_op_name op :: Id
op (Op_type _fkind :: OpKind
_fkind args :: [Id]
args res :: Id
res _range :: Range
_range) _, l :: b
l) =
           ( Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (Id -> Id
mkGenName Id
op)
                           (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
args Id
res Range
nullRange) Range
nullRange,
             b
l)
    opsToProcs :: Constraint -> Constraint
opsToProcs (Constraint nSort :: Id
nSort syms :: [(OP_SYMB, [Int])]
syms oSort :: Id
oSort) =
                Id -> [(OP_SYMB, [Int])] -> Id -> Constraint
Constraint Id
nSort (((OP_SYMB, [Int]) -> (OP_SYMB, [Int]))
-> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map (OP_SYMB, [Int]) -> (OP_SYMB, [Int])
forall b. (OP_SYMB, b) -> (OP_SYMB, b)
toProcs [(OP_SYMB, [Int])]
syms) Id
oSort
   Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
             ([Constraint] -> Map Id Id -> Bool -> VSEforms
RestrictedConstraint
                ((Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> Constraint
opsToProcs [Constraint]
constrs)
                ([(Id, Id)] -> Map Id Id
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, Id)] -> Map Id Id) -> [(Id, Id)] -> Map Id Id
forall a b. (a -> b) -> a -> b
$ (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: Id
s -> (Id
s, Id -> Id
gnRestrName Id
s)) [Id]
genSorts)
              Bool
isFree)
            Range
nullRange
  Atom b :: Bool
b _ps :: Range
_ps -> Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ Bool -> Sentence
forall f. Bool -> FORMULA f
boolForm Bool
b
  Equation t1 :: TERM ()
t1 Strong t2 :: TERM ()
t2 _ps :: Range
_ps -> do
     let sort1 :: Id
sort1 = TERM () -> Id
forall f. TermExtension f => f -> Id
sortOfTerm TERM ()
t1
     Int
n1 <- Id -> State (Int, VarSet) Int
freshIndex Id
sort1 -- (typeof t1)
     Program
prg1 <- Int -> TERM () -> State (Int, VarSet) Program
mapCASLTerm Int
n1 TERM ()
t1
     Int
n2 <- Id -> State (Int, VarSet) Int
freshIndex Id
sort1 -- (typeof t2)
     Program
prg2 <- Int -> TERM () -> State (Int, VarSet) Program
mapCASLTerm Int
n2 TERM ()
t2
     Int
n <- Id -> State (Int, VarSet) Int
freshIndex Id
uBoolean
     Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
      (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
       (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
           (Program -> Program -> PlainProgram
Seq (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq Program
prg1 Program
prg2) Range
nullRange)
                 (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                 (VAR -> TERM () -> PlainProgram
Assign
                    (String -> Int -> VAR
genNumVar "x" Int
n)
                    (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                       (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                         (Id -> Id
gnEqName Id
sort1)
                         (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
sort1, Id
sort1] Id
uBoolean Range
nullRange)
                        Range
nullRange)
                       [VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
n1) Id
sort1 Range
nullRange,
                        VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
n2) Id
sort1 Range
nullRange]
                       Range
nullRange
                    )
                 ) Range
nullRange)
           )
        Range
nullRange)
       (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (VAR -> Id -> Range -> TERM (Ranged VSEforms)
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
n) Id
uBoolean Range
nullRange)
                        TERM (Ranged VSEforms)
forall f. TERM f
aTrue)
      )
      Range
nullRange
     {- here i have to return smth like
     --      <: xn1 := prg1;
     --         xn2 := prg2;
     --         xn := gn_eq_s(xn1,xn2) :> xn = True  " -}
  Predication pn :: PRED_SYMB
pn as :: [TERM ()]
as _qs :: Range
_qs -> do
     [Int]
indexes <- (TERM () -> State (Int, VarSet) Int)
-> [TERM ()] -> State (Int, VarSet) [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Id -> State (Int, VarSet) Int
freshIndex (Id -> State (Int, VarSet) Int)
-> (TERM () -> Id) -> TERM () -> State (Int, VarSet) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM () -> Id
forall f. TermExtension f => f -> Id
sortOfTerm) [TERM ()]
as
     [Program]
prgs <- ((TERM (), Int) -> State (Int, VarSet) Program)
-> [(TERM (), Int)] -> State (Int, VarSet) [Program]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (ti :: TERM ()
ti, i :: Int
i) -> Int -> TERM () -> State (Int, VarSet) Program
mapCASLTerm Int
i TERM ()
ti) ([(TERM (), Int)] -> State (Int, VarSet) [Program])
-> [(TERM (), Int)] -> State (Int, VarSet) [Program]
forall a b. (a -> b) -> a -> b
$ [TERM ()] -> [Int] -> [(TERM (), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TERM ()]
as [Int]
indexes
     let xvars :: [TERM f]
xvars = ((TERM (), Int) -> TERM f) -> [(TERM (), Int)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ti :: TERM ()
ti, i :: Int
i) ->
                     VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
i)
                              (TERM () -> Id
forall f. TermExtension f => f -> Id
sortOfTerm TERM ()
ti) Range
nullRange ) ([(TERM (), Int)] -> [TERM f]) -> [(TERM (), Int)] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ [TERM ()] -> [Int] -> [(TERM (), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TERM ()]
as [Int]
indexes
     Int
n <- Id -> State (Int, VarSet) Int
freshIndex Id
uBoolean
     let asgn :: Program
asgn = if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Program] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Program]
prgs then
                       (Program -> Program -> Program) -> [Program] -> Program
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ p1 :: Program
p1 p2 :: Program
p2 -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq Program
p1 Program
p2) Range
nullRange) [Program]
prgs
                       else PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Skip Range
nullRange
     case PRED_SYMB
pn of
      Pred_name _ -> String -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "must be qualified"
      Qual_pred_name pname :: Id
pname (Pred_type ptype :: [Id]
ptype _) _ -> Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
       (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
        (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
          (Program -> Program -> PlainProgram
Seq
             Program
asgn
             (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (VAR -> TERM () -> PlainProgram
Assign (String -> Int -> VAR
genNumVar "x" Int
n)
                       (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                         (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                          (Id -> Id
mkGenName Id
pname)
                          (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
ptype Id
uBoolean Range
nullRange) Range
nullRange)
                          [TERM ()]
forall f. [TERM f]
xvars Range
nullRange))
              Range
nullRange))
         Range
nullRange)
        (TERM (Ranged VSEforms) -> TERM (Ranged VSEforms) -> Sentence
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
          (VAR -> Id -> Range -> TERM (Ranged VSEforms)
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
n) Id
uBoolean Range
nullRange)
                        TERM (Ranged VSEforms)
forall f. TERM f
aTrue))
       Range
nullRange
     {- <: xi := prgi;
           x:= gn_p(x1,..,xn):> x = True -}
  Junction j :: Junctor
j fs :: [CASLFORMULA]
fs _r :: Range
_r -> do
   [Sentence]
mapFs <- (CASLFORMULA -> State (Int, VarSet) Sentence)
-> [CASLFORMULA] -> State (Int, VarSet) [Sentence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux [CASLFORMULA]
fs
   Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ Junctor -> [Sentence] -> Range -> Sentence
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j [Sentence]
mapFs Range
nullRange
  Relation f1 :: CASLFORMULA
f1 c :: Relation
c f2 :: CASLFORMULA
f2 _r :: Range
_r -> do
   Sentence
trf1 <- CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux CASLFORMULA
f1
   Sentence
trf2 <- CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux CASLFORMULA
f2
   Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ Sentence -> Relation -> Sentence -> Range -> Sentence
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation Sentence
trf1 Relation
c Sentence
trf2 Range
nullRange
  Negation f1 :: CASLFORMULA
f1 _r :: Range
_r -> do
   Sentence
trf <- CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux CASLFORMULA
f1
   Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ Sentence -> Sentence
forall f. FORMULA f -> FORMULA f
mkNeg Sentence
trf
  Quantification q :: QUANTIFIER
q vars :: [VAR_DECL]
vars sen :: CASLFORMULA
sen _ ->
   case QUANTIFIER
q of
    Universal -> do
     Sentence
trSen <- CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux CASLFORMULA
sen
     let h :: [Sentence]
h = (VAR_DECL -> Sentence) -> [VAR_DECL] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Var_decl varS :: [VAR]
varS s :: Id
s _) -> let
           restrs :: [Sentence]
restrs = (VAR -> Sentence) -> [VAR] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: VAR
v -> Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (
                                  BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                                  (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                    (CASLFORMULA -> PlainProgram
Call
                                      (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                         (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                            (Id -> Id
gnRestrName Id
s)
                                            ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange)
                                            Range
nullRange
                                         )
                                         [VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var VAR
v Id
s Range
nullRange]
                                         Range
nullRange
                                      )
                                    )
                                   Range
nullRange)
                                  Sentence
forall f. FORMULA f
trueForm) Range
nullRange)
                 [VAR]
varS
                                         in
           [Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct [Sentence]
restrs)
             [VAR_DECL]
vars
     let sen' :: Sentence
sen' = Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                 ((Sentence -> Sentence -> Sentence) -> [Sentence] -> Sentence
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ sen1 :: Sentence
sen1 sen2 :: Sentence
sen2 -> [Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct [Sentence
sen1, Sentence
sen2]) [Sentence]
h)
                 Sentence
trSen
     Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vars Sentence
sen' Range
nullRange
    Existential -> do
     Sentence
trSen <- CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux CASLFORMULA
sen
     let h :: [Sentence]
h = (VAR_DECL -> Sentence) -> [VAR_DECL] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Var_decl varS :: [VAR]
varS s :: Id
s _) -> let
           restrs :: [Sentence]
restrs = (VAR -> Sentence) -> [VAR] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: VAR
v -> Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (
                                  BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond
                                  (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                    (CASLFORMULA -> PlainProgram
Call
                                      (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                         (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                            (Id -> Id
gnRestrName Id
s)
                                            ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange)
                                            Range
nullRange
                                         )
                                         [VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var VAR
v Id
s Range
nullRange]
                                         Range
nullRange
                                      )
                                    )
                                   Range
nullRange)
                                  Sentence
forall f. FORMULA f
trueForm) Range
nullRange)
                 [VAR]
varS
                                         in
           [Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct [Sentence]
restrs)
             [VAR_DECL]
vars
     let sen' :: Sentence
sen' = [Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct
                 [(Sentence -> Sentence -> Sentence) -> [Sentence] -> Sentence
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ sen1 :: Sentence
sen1 sen2 :: Sentence
sen2 -> [Sentence] -> Sentence
forall f. [FORMULA f] -> FORMULA f
conjunct [Sentence
sen1, Sentence
sen2]) [Sentence]
h,
                 Sentence
trSen]
     Sentence -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> State (Int, VarSet) Sentence)
-> Sentence -> State (Int, VarSet) Sentence
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vars Sentence
sen' Range
nullRange
    Unique_existential -> String -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "nyi Unique_existential"
  _ -> String -> State (Int, VarSet) Sentence
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Comorphisms.CASL2VSERefine.mapCASLSenAux"


mapCASLTerm :: Int -> TERM () -> State (Int, VarSet) Program
mapCASLTerm :: Int -> TERM () -> State (Int, VarSet) Program
mapCASLTerm n :: Int
n t :: TERM ()
t = case TERM ()
t of
  Qual_var v :: VAR
v s :: Id
s _ps :: Range
_ps -> Program -> State (Int, VarSet) Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> State (Int, VarSet) Program)
-> Program -> State (Int, VarSet) Program
forall a b. (a -> b) -> a -> b
$
      PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (VAR -> TERM () -> PlainProgram
Assign (String -> Int -> VAR
genNumVar "x" Int
n)
               (VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var VAR
v Id
s Range
nullRange)) Range
nullRange
  Application opsym :: OP_SYMB
opsym as :: [TERM ()]
as _qs :: Range
_qs -> do
   [Int]
indexes <- (TERM () -> State (Int, VarSet) Int)
-> [TERM ()] -> State (Int, VarSet) [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Id -> State (Int, VarSet) Int
freshIndex (Id -> State (Int, VarSet) Int)
-> (TERM () -> Id) -> TERM () -> State (Int, VarSet) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM () -> Id
forall f. TermExtension f => f -> Id
sortOfTerm) [TERM ()]
as
   let xvars :: [TERM f]
xvars = ((TERM (), Int) -> TERM f) -> [(TERM (), Int)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ti :: TERM ()
ti, i :: Int
i) ->
                     VAR -> Id -> Range -> TERM f
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> Int -> VAR
genNumVar "x" Int
i)
                              (TERM () -> Id
forall f. TermExtension f => f -> Id
sortOfTerm TERM ()
ti) Range
nullRange ) ([(TERM (), Int)] -> [TERM f]) -> [(TERM (), Int)] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ [TERM ()] -> [Int] -> [(TERM (), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TERM ()]
as [Int]
indexes
   [Program]
prgs <- ((TERM (), Int) -> State (Int, VarSet) Program)
-> [(TERM (), Int)] -> State (Int, VarSet) [Program]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (ti :: TERM ()
ti, i :: Int
i) -> Int -> TERM () -> State (Int, VarSet) Program
mapCASLTerm Int
i TERM ()
ti) ([(TERM (), Int)] -> State (Int, VarSet) [Program])
-> [(TERM (), Int)] -> State (Int, VarSet) [Program]
forall a b. (a -> b) -> a -> b
$ [TERM ()] -> [Int] -> [(TERM (), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TERM ()]
as [Int]
indexes
   let asgn :: Program
asgn = if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Program] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Program]
prgs then
                       (Program -> Program -> Program) -> [Program] -> Program
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ p1 :: Program
p1 p2 :: Program
p2 -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq Program
p1 Program
p2) Range
nullRange) [Program]
prgs
                       else PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Skip Range
nullRange
   case OP_SYMB
opsym of
    Op_name _ -> String -> State (Int, VarSet) Program
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "must be qualified"
    Qual_op_name oName :: Id
oName (Op_type _ args :: [Id]
args res :: Id
res _) _ ->
      case [Id]
args of
       [] -> Program -> State (Int, VarSet) Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> State (Int, VarSet) Program)
-> Program -> State (Int, VarSet) Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (VAR -> TERM () -> PlainProgram
Assign (String -> Int -> VAR
genNumVar "x" Int
n)
                       (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                        (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                         (Id -> Id
mkGenName Id
oName)
                         (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
args Id
res Range
nullRange)
                         Range
nullRange
                        )
                       [TERM ()]
forall f. [TERM f]
xvars Range
nullRange))
                       Range
nullRange
       _ -> Program -> State (Int, VarSet) Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> State (Int, VarSet) Program)
-> Program -> State (Int, VarSet) Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
               (Program -> Program -> PlainProgram
Seq
                Program
asgn
                (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (VAR -> TERM () -> PlainProgram
Assign (String -> Int -> VAR
genNumVar "x" Int
n)
                       (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                        (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                         (Id -> Id
mkGenName Id
oName)
                         (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
args Id
res Range
nullRange)
                         Range
nullRange
                        )
                       [TERM ()]
forall f. [TERM f]
xvars Range
nullRange))
                  Range
nullRange))
                Range
nullRange
  _ -> String -> State (Int, VarSet) Program
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "nyi term"

freshIndex :: SORT -> State (Int, VarSet) Int
freshIndex :: Id -> State (Int, VarSet) Int
freshIndex ss :: Id
ss = do
  (i :: Int
i, s :: VarSet
s) <- State (Int, VarSet) (Int, VarSet)
forall s. State s s
get
  let v :: VAR
v = String -> Int -> VAR
genNumVar "x" Int
i
  (Int, VarSet) -> State (Int, VarSet) ()
forall s. s -> State s ()
put (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, (VAR, Id) -> VarSet -> VarSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (VAR
v, Id
ss) VarSet
s)
  Int -> State (Int, VarSet) Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i