{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CommonLogic2IsabelleHOL.hs
Description :  direct comorphism from CommonLogic to Isabelle-HOL
Copyright   :  (c) Soeren Schulze, Uni Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  s.schulze@uni-bremen.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

A direct comorphism from CommonLogic to Isabelle-HOL, passing arguments as
native Isabelle lists.
-}

module Comorphisms.CommonLogic2IsabelleHOL where

import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)

import Logic.Logic
import Logic.Comorphism

import Common.ProofTree
import Common.Result
import Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import Common.GlobalAnnotations (emptyGlobalAnnos)

import qualified CommonLogic.Logic_CommonLogic as ClLogic
import qualified CommonLogic.AS_CommonLogic as ClBasic
import qualified CommonLogic.Sign as ClSign
import qualified CommonLogic.Symbol as ClSymbol
import qualified CommonLogic.Morphism as ClMor
import qualified CommonLogic.Sublogic as ClSl
import CommonLogic.ModuleElimination

import Isabelle.IsaSign hiding (qname)
import Isabelle.IsaConsts
import Isabelle.Logic_Isabelle
import Isabelle.Translate

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

instance Language CommonLogic2IsabelleHOL where
  language_name :: CommonLogic2IsabelleHOL -> String
language_name CommonLogic2IsabelleHOL = "CommonLogic2Isabelle"

instance Comorphism
         CommonLogic2IsabelleHOL -- comorphism
         ClLogic.CommonLogic     -- lid domain
         ClSl.CommonLogicSL      -- sublogics codomain
         ClBasic.BASIC_SPEC      -- Basic spec domain
         ClBasic.TEXT_META       -- sentence domain
         ClBasic.SYMB_ITEMS      -- symbol items domain
         ClBasic.SYMB_MAP_ITEMS  -- symbol map items domain
         ClSign.Sign             -- signature domain
         ClMor.Morphism          -- morphism domain
         ClSymbol.Symbol         -- symbol domain
         ClSymbol.Symbol         -- rawsymbol domain
         ProofTree               -- proof tree codomain
         Isabelle                -- lid codomain
         ()                      -- sublogics codomain [none]
         ()                      -- Basic spec codomain [none]
         Sentence                -- sentence codomain
         ()                      -- symbol items codomain [none]
         ()                      -- symbol map items codomain [none]
         Sign                    -- signature codomain
         IsabelleMorphism        -- morphism codomain
         ()                      -- symbol codomain [none]
         ()                      -- rawsymbol codomain [none]
         ()                      -- proof tree domain [none]
         where
           sourceLogic :: CommonLogic2IsabelleHOL -> CommonLogic
sourceLogic CommonLogic2IsabelleHOL = CommonLogic
ClLogic.CommonLogic
           sourceSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL
sourceSublogic CommonLogic2IsabelleHOL = CommonLogicSL
ClSl.top
           targetLogic :: CommonLogic2IsabelleHOL -> Isabelle
targetLogic CommonLogic2IsabelleHOL = Isabelle
Isabelle
           map_theory :: CommonLogic2IsabelleHOL
-> (Sign, [Named TEXT_META]) -> Result (Sign, [Named Sentence])
map_theory CommonLogic2IsabelleHOL = (Sign, [Named TEXT_META]) -> Result (Sign, [Named Sentence])
mapTheory
           map_sentence :: CommonLogic2IsabelleHOL -> Sign -> TEXT_META -> Result Sentence
map_sentence CommonLogic2IsabelleHOL = Sign -> TEXT_META -> Result Sentence
mapSentence
           has_model_expansion :: CommonLogic2IsabelleHOL -> Bool
has_model_expansion CommonLogic2IsabelleHOL = Bool
True
           is_weakly_amalgamable :: CommonLogic2IsabelleHOL -> Bool
is_weakly_amalgamable CommonLogic2IsabelleHOL = Bool
True
           isInclusionComorphism :: CommonLogic2IsabelleHOL -> Bool
isInclusionComorphism CommonLogic2IsabelleHOL = Bool
True

mapSentence :: ClSign.Sign -> ClBasic.TEXT_META -> Result Sentence
mapSentence :: Sign -> TEXT_META -> Result Sentence
mapSentence sig :: Sign
sig = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (TEXT_META -> Sentence) -> TEXT_META -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sentence
mkSen (Term -> Sentence) -> (TEXT_META -> Term) -> TEXT_META -> Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> TEXT_META -> Term
transTextMeta Sign
sig

mapTheory :: (ClSign.Sign, [AS_Anno.Named ClBasic.TEXT_META])
             -> Result (Sign, [AS_Anno.Named Sentence])
mapTheory :: (Sign, [Named TEXT_META]) -> Result (Sign, [Named Sentence])
mapTheory (sig :: Sign
sig, namedTextMetas :: [Named TEXT_META]
namedTextMetas) =
  (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Sign
mapSig Sign
sig, Named Sentence
ax_that Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: (Named TEXT_META -> Named Sentence)
-> [Named TEXT_META] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> Named TEXT_META -> Named Sentence
transNamed Sign
sig) [Named TEXT_META]
namedTextMetas)

individualS :: String
individualS :: String
individualS = "individual"

individualT :: Typ
individualT :: Typ
individualT = String -> Typ
mkSType String
individualS

ax_that :: AS_Anno.Named Sentence
ax_that :: Named Sentence
ax_that = String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "Ax_that" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Sentence -> Sentence
forceSimp (Sentence -> Sentence) -> Sentence -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
mkSen (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$
          Term -> Term -> Term
termAppl (String -> Term
conDouble "ALL") (Term -> Term -> Continuity -> Term
Abs Term
senTrm Term
s Continuity
NotCont)
  where s :: Term
s = Term -> Term -> Term
binEqv Term
senTrm
            (VName -> Term -> Term -> Term
binVNameAppl
             VName
relSymb (Term -> Term -> Term
termAppl (VName -> Term
con VName
thatSymb) Term
senTrm) (Continuity -> Term
nilPT Continuity
NotCont))
        senTrm :: Term
senTrm = String -> Term
conDouble "sen"
        forceSimp :: Sentence -> Sentence
forceSimp sen :: Sentence
sen = Sentence
sen { isSimp :: Bool
isSimp = Bool
True }

type RENAMES = Map.Map String VName

mkIndName :: String -> VName
mkIndName :: String -> VName
mkIndName name :: String
name = Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
True GlobalAnnos
emptyGlobalAnnos (-1)
                 (String -> Id
Id.stringToId String
name) BaseSig
Main_thy Set String
forall a. Set a
Set.empty

addRenames :: RENAMES -> [String] -> RENAMES
addRenames :: RENAMES -> [String] -> RENAMES
addRenames = (String -> RENAMES -> RENAMES) -> RENAMES -> [String] -> RENAMES
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
             (\ k :: String
k m :: RENAMES
m -> let k' :: String
k' = String -> RENAMES -> String
forall a. String -> Map String a -> String
unclash String
k RENAMES
m
                           v :: VName
v = String -> VName
mkIndName String
k' in
                      String -> VName -> RENAMES -> RENAMES
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
k VName
v (RENAMES -> RENAMES) -> RENAMES -> RENAMES
forall a b. (a -> b) -> a -> b
$ String -> VName -> RENAMES -> RENAMES
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
k' VName
v RENAMES
m)
  where unclash :: String -> Map String a -> String
unclash k :: String
k m :: Map String a
m = if String -> Map String a -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member String
k Map String a
m
                      then String -> Map String a -> String
unclash ("X_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k) Map String a
m
                      else String
k

makeRenames :: [String] -> RENAMES
makeRenames :: [String] -> RENAMES
makeRenames = RENAMES -> [String] -> RENAMES
addRenames RENAMES
forall k a. Map k a
Map.empty

basicRenames :: ClSign.Sign -> RENAMES
basicRenames :: Sign -> RENAMES
basicRenames sig :: Sign
sig = RENAMES -> [String] -> RENAMES
addRenames
                   ([(String, VName)] -> RENAMES
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [("rel", VName
relSymb), ("fun", VName
funSymb),
                                  ("that", VName
thatSymb)])
                   ((Id -> String) -> [Id] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> String
Id.tokStr (Token -> String) -> (Id -> Token) -> Id -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Token
Id.idToSimpleId)
                    ( Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Sign -> Set Id
ClSign.sequenceMarkers Sign
sig)
                     [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Sign -> Set Id
ClSign.discourseNames Sign
sig)))

rename :: RENAMES -> String -> VName
rename :: RENAMES -> String -> VName
rename rn :: RENAMES
rn s :: String
s = VName -> Maybe VName -> VName
forall a. a -> Maybe a -> a
fromMaybe (String -> VName
forall a. HasCallStack => String -> a
error (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ "Symbol " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ "not found") (Maybe VName -> VName) -> Maybe VName -> VName
forall a b. (a -> b) -> a -> b
$
              String -> RENAMES -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
s RENAMES
rn

mapSig :: ClSign.Sign -> Sign
mapSig :: Sign -> Sign
mapSig sig :: Sign
sig = Sign
emptySign {
  tsig :: TypeSig
tsig = TypeSig
emptyTypeSig {
     arities :: Arities
arities = String -> [(IsaClass, [(Typ, Sort)])] -> Arities
forall k a. k -> a -> Map k a
Map.singleton String
individualS [(IsaClass
isaTerm, [])]
     },
  constTab :: ConstTab
constTab = VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VName
relSymb
             ([Typ] -> Typ -> Typ
mkCurryFunType [Typ
individualT, Typ -> Typ
mkListType Typ
individualT] Typ
boolType) (ConstTab -> ConstTab) -> ConstTab -> ConstTab
forall a b. (a -> b) -> a -> b
$
             VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VName
funSymb
             ([Typ] -> Typ -> Typ
mkCurryFunType [Typ
individualT, Typ -> Typ
mkListType Typ
individualT] Typ
individualT) (ConstTab -> ConstTab) -> ConstTab -> ConstTab
forall a b. (a -> b) -> a -> b
$
             VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VName
thatSymb
             ([Typ] -> Typ -> Typ
mkCurryFunType [Typ
boolType] Typ
individualT) (ConstTab -> ConstTab) -> ConstTab -> ConstTab
forall a b. (a -> b) -> a -> b
$
             ConstTab -> ConstTab -> ConstTab
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ([(VName, Typ)] -> ConstTab
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                        ((Id -> (VName, Typ)) -> [Id] -> [(VName, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map ((\ name :: String
name -> (RENAMES -> String -> VName
rename RENAMES
rn String
name, Typ
individualT)) (String -> (VName, Typ)) -> (Id -> String) -> Id -> (VName, Typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                              Token -> String
Id.tokStr (Token -> String) -> (Id -> Token) -> Id -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Token
Id.idToSimpleId) ([Id] -> [(VName, Typ)]) -> [Id] -> [(VName, Typ)]
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
$
                         Sign -> Set Id
ClSign.discourseNames Sign
sig))
             ([(VName, Typ)] -> ConstTab
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
              ((Id -> (VName, Typ)) -> [Id] -> [(VName, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map ((\ name :: String
name -> (RENAMES -> String -> VName
rename RENAMES
rn String
name, Typ -> Typ
mkListType Typ
individualT)) (String -> (VName, Typ)) -> (Id -> String) -> Id -> (VName, Typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                    Token -> String
Id.tokStr (Token -> String) -> (Id -> Token) -> Id -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Token
Id.idToSimpleId) ([Id] -> [(VName, Typ)]) -> [Id] -> [(VName, Typ)]
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
$
               Sign -> Set Id
ClSign.sequenceMarkers Sign
sig))
  }
  where rn :: RENAMES
rn = Sign -> RENAMES
basicRenames Sign
sig

relSymb, funSymb, thatSymb :: VName
relSymb :: VName
relSymb = Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
True GlobalAnnos
emptyGlobalAnnos 2
          (String -> Id
Id.stringToId "rel")
          BaseSig
Main_thy Set String
forall a. Set a
Set.empty

funSymb :: VName
funSymb = Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
False GlobalAnnos
emptyGlobalAnnos 2
          (String -> Id
Id.stringToId "fun")
          BaseSig
Main_thy Set String
forall a. Set a
Set.empty

thatSymb :: VName
thatSymb = Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
False GlobalAnnos
emptyGlobalAnnos 1
           (String -> Id
Id.stringToId "that")
           BaseSig
Main_thy Set String
forall a. Set a
Set.empty

quantify :: RENAMES -> ClBasic.QUANT -> String -> Term -> Term
quantify :: RENAMES -> QUANT -> String -> Term -> Term
quantify rn :: RENAMES
rn q :: QUANT
q v :: String
v s :: Term
s = Term -> Term -> Term
termAppl (String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ QUANT -> String
qname QUANT
q)
                 (Term -> Term -> Continuity -> Term
Abs (VName -> Term
con (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ RENAMES -> String -> VName
rename RENAMES
rn String
v) Term
s Continuity
NotCont)
  where qname :: QUANT -> String
qname ClBasic.Universal = String
allS
        qname ClBasic.Existential = String
exS

transTextMeta :: ClSign.Sign -> ClBasic.TEXT_META -> Term
transTextMeta :: Sign -> TEXT_META -> Term
transTextMeta sig :: Sign
sig = RENAMES -> TEXT -> Term
transText RENAMES
renames (TEXT -> Term) -> (TEXT_META -> TEXT) -> TEXT_META -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TEXT_META -> TEXT
ClBasic.getText (TEXT_META -> TEXT)
-> (TEXT_META -> TEXT_META) -> TEXT_META -> TEXT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TEXT_META -> TEXT_META
eliminateModules
  where renames :: RENAMES
renames = Sign -> RENAMES
basicRenames Sign
sig

transNamed :: ClSign.Sign -> AS_Anno.Named ClBasic.TEXT_META
              -> AS_Anno.Named Sentence
transNamed :: Sign -> Named TEXT_META -> Named Sentence
transNamed sig :: Sign
sig = (TEXT_META -> Sentence) -> Named TEXT_META -> Named Sentence
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed ((TEXT_META -> Sentence) -> Named TEXT_META -> Named Sentence)
-> (TEXT_META -> Sentence) -> Named TEXT_META -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
mkSen (Term -> Sentence) -> (TEXT_META -> Term) -> TEXT_META -> Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> TEXT_META -> Term
transTextMeta Sign
sig

transText :: RENAMES -> ClBasic.TEXT -> Term
transText :: RENAMES -> TEXT -> Term
transText rn :: RENAMES
rn txt :: TEXT
txt = case TEXT
txt of
  ClBasic.Text phrs :: [PHRASE]
phrs _ ->
    let phrs' :: [PHRASE]
phrs' = (PHRASE -> Bool) -> [PHRASE] -> [PHRASE]
forall a. (a -> Bool) -> [a] -> [a]
filter PHRASE -> Bool
nonImport [PHRASE]
phrs
    in if [PHRASE] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PHRASE]
phrs' then Term
true
       else (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Term -> Term -> Term
binConj ((PHRASE -> Term) -> [PHRASE] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (RENAMES -> PHRASE -> Term
transPhrase RENAMES
rn) [PHRASE]
phrs')
  ClBasic.Named_text _ t :: TEXT
t _ -> RENAMES -> TEXT -> Term
transText RENAMES
rn TEXT
t
  where nonImport :: PHRASE -> Bool
nonImport p :: PHRASE
p = case PHRASE
p of
          ClBasic.Importation _ -> Bool
False
          _ -> Bool
True

transPhrase :: RENAMES -> ClBasic.PHRASE -> Term
transPhrase :: RENAMES -> PHRASE -> Term
transPhrase rn :: RENAMES
rn phr :: PHRASE
phr = case PHRASE
phr of
  ClBasic.Module _ -> String -> Term
forall a. HasCallStack => String -> a
error "transPhase: \"module\" found"
  ClBasic.Sentence s :: SENTENCE
s -> RENAMES -> SENTENCE -> Term
transSen RENAMES
rn SENTENCE
s
  ClBasic.Importation _ -> String -> Term
forall a. HasCallStack => String -> a
error "transPhase: \"import\" found"
  ClBasic.Comment_text _ t :: TEXT
t _ -> RENAMES -> TEXT -> Term
transText RENAMES
rn TEXT
t

transTerm :: RENAMES -> ClBasic.TERM -> Term
transTerm :: RENAMES -> TERM -> Term
transTerm rn :: RENAMES
rn trm :: TERM
trm = case TERM
trm of
  ClBasic.Name_term name :: Token
name -> VName -> Term
con (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ RENAMES -> String -> VName
rename RENAMES
rn (Token -> String
Id.tokStr Token
name)
  ClBasic.Funct_term op :: TERM
op args :: [TERM_SEQ]
args _ -> VName -> RENAMES -> TERM -> [TERM_SEQ] -> Term
applyTermSeq VName
funSymb RENAMES
rn TERM
op [TERM_SEQ]
args
  ClBasic.Comment_term t :: TERM
t _ _ -> RENAMES -> TERM -> Term
transTerm RENAMES
rn TERM
t
  ClBasic.That_term sen :: SENTENCE
sen _ -> Term -> Term -> Term
termAppl (VName -> Term
con VName
thatSymb) (RENAMES -> SENTENCE -> Term
transSen RENAMES
rn SENTENCE
sen)

transNameOrSeqmark :: ClBasic.NAME_OR_SEQMARK -> String
transNameOrSeqmark :: NAME_OR_SEQMARK -> String
transNameOrSeqmark ts :: NAME_OR_SEQMARK
ts = Token -> String
Id.tokStr (Token -> String) -> Token -> String
forall a b. (a -> b) -> a -> b
$ case NAME_OR_SEQMARK
ts of
  ClBasic.Name name :: Token
name -> Token
name
  ClBasic.SeqMark seqm :: Token
seqm -> Token
seqm

transTermSeq :: RENAMES -> ClBasic.TERM_SEQ -> Term
transTermSeq :: RENAMES -> TERM_SEQ -> Term
transTermSeq rn :: RENAMES
rn ts :: TERM_SEQ
ts = case TERM_SEQ
ts of
  ClBasic.Term_seq trm :: TERM
trm -> (Term -> Term -> Term
termAppl (Term -> Term -> Term) -> (Term -> Term) -> Term -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
termAppl (VName -> Term
conC VName
consV))
                          (RENAMES -> TERM -> Term
transTerm RENAMES
rn TERM
trm) (Continuity -> Term
nilPT Continuity
NotCont)
  ClBasic.Seq_marks seqm :: Token
seqm -> VName -> Term
con (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ RENAMES -> String -> VName
rename RENAMES
rn (Token -> String
Id.tokStr Token
seqm)

{- applicable for a non-empty argument list where only the last argument
(or none) is a seqmark -}
transArgsSimple :: RENAMES -> [ClBasic.TERM_SEQ] -> Maybe Term
transArgsSimple :: RENAMES -> [TERM_SEQ] -> Maybe Term
transArgsSimple rn :: RENAMES
rn tss :: [TERM_SEQ]
tss =
  (TERM_SEQ -> Maybe Term -> Maybe Term)
-> Maybe Term -> [TERM_SEQ] -> Maybe Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
  (\ ts :: TERM_SEQ
ts trm :: Maybe Term
trm ->
    do Term
trm' <- Maybe Term
trm
       case TERM_SEQ
ts of
         ClBasic.Term_seq clTrm :: TERM
clTrm ->
           Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term
termAppl (Term -> Term -> Term) -> (Term -> Term) -> Term -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
termAppl (VName -> Term
conC VName
consV)) (RENAMES -> TERM -> Term
transTerm RENAMES
rn TERM
clTrm) Term
trm'
         _ -> Maybe Term
forall a. Maybe a
Nothing)
  (Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ RENAMES -> TERM_SEQ -> Term
transTermSeq RENAMES
rn (TERM_SEQ -> Term) -> TERM_SEQ -> Term
forall a b. (a -> b) -> a -> b
$ [TERM_SEQ] -> TERM_SEQ
forall a. [a] -> a
last [TERM_SEQ]
tss)
  ([TERM_SEQ] -> [TERM_SEQ]
forall a. [a] -> [a]
init [TERM_SEQ]
tss)

transArgs :: RENAMES -> [ClBasic.TERM_SEQ] -> Term
transArgs :: RENAMES -> [TERM_SEQ] -> Term
transArgs rn :: RENAMES
rn tss :: [TERM_SEQ]
tss = case ([TERM_SEQ]
tss, RENAMES -> [TERM_SEQ] -> Maybe Term
transArgsSimple RENAMES
rn [TERM_SEQ]
tss) of
  ([], _) -> Continuity -> Term
nilPT Continuity
NotCont
  (_, Just trm :: Term
trm) -> Term
trm
  (_, Nothing) -> (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (Term -> Term -> Term
termAppl (Term -> Term -> Term) -> (Term -> Term) -> Term -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
termAppl (VName -> Term
con VName
appendV))
                  ((TERM_SEQ -> Term) -> [TERM_SEQ] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (RENAMES -> TERM_SEQ -> Term
transTermSeq RENAMES
rn) [TERM_SEQ]
tss)

applyTermSeq :: VName -> RENAMES -> ClBasic.TERM -> [ClBasic.TERM_SEQ] -> Term
applyTermSeq :: VName -> RENAMES -> TERM -> [TERM_SEQ] -> Term
applyTermSeq metaSymb :: VName
metaSymb rn :: RENAMES
rn clTrm :: TERM
clTrm clArgs :: [TERM_SEQ]
clArgs = VName -> Term -> Term -> Term
binVNameAppl VName
metaSymb Term
trm Term
args
  where trm :: Term
trm = RENAMES -> TERM -> Term
transTerm RENAMES
rn TERM
clTrm
        args :: Term
args = RENAMES -> [TERM_SEQ] -> Term
transArgs RENAMES
rn [TERM_SEQ]
clArgs

transSen :: RENAMES -> ClBasic.SENTENCE -> Term
transSen :: RENAMES -> SENTENCE -> Term
transSen rn :: RENAMES
rn sen :: SENTENCE
sen = case SENTENCE
sen of
  ClBasic.Bool_sent bs :: BOOL_SENT
bs _ -> case BOOL_SENT
bs of
    ClBasic.Negation s :: SENTENCE
s -> Term -> Term -> Term
termAppl Term
notOp (RENAMES -> SENTENCE -> Term
transSen RENAMES
rn SENTENCE
s)
    ClBasic.Junction j :: AndOr
j ss :: [SENTENCE]
ss ->
      if [SENTENCE] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SENTENCE]
ss then Term
true
      else (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (case AndOr
j of ClBasic.Conjunction -> Term -> Term -> Term
binConj
                             ClBasic.Disjunction -> Term -> Term -> Term
binDisj)
           ((SENTENCE -> Term) -> [SENTENCE] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (RENAMES -> SENTENCE -> Term
transSen RENAMES
rn) [SENTENCE]
ss)
    ClBasic.BinOp j :: ImplEq
j s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 ->
      (case ImplEq
j of ClBasic.Implication -> Term -> Term -> Term
binImpl
                 ClBasic.Biconditional -> Term -> Term -> Term
binEqv)
      (RENAMES -> SENTENCE -> Term
transSen RENAMES
rn SENTENCE
s1) (RENAMES -> SENTENCE -> Term
transSen RENAMES
rn SENTENCE
s2)
  ClBasic.Quant_sent q :: QUANT
q bs :: [NAME_OR_SEQMARK]
bs s :: SENTENCE
s _ -> (String -> Term -> Term) -> Term -> [String] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (RENAMES -> QUANT -> String -> Term -> Term
quantify RENAMES
rn' QUANT
q) (RENAMES -> SENTENCE -> Term
transSen RENAMES
rn' SENTENCE
s) [String]
varNames
    where rn' :: RENAMES
rn' = RENAMES -> [String] -> RENAMES
addRenames RENAMES
rn [String]
varNames
          varNames :: [String]
varNames = (NAME_OR_SEQMARK -> String) -> [NAME_OR_SEQMARK] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map NAME_OR_SEQMARK -> String
transNameOrSeqmark [NAME_OR_SEQMARK]
bs
  ClBasic.Atom_sent at :: ATOM
at _ -> case ATOM
at of
    ClBasic.Equation t1 :: TERM
t1 t2 :: TERM
t2 -> Term -> Term -> Term
binEq (RENAMES -> TERM -> Term
transTerm RENAMES
rn TERM
t1) (RENAMES -> TERM -> Term
transTerm RENAMES
rn TERM
t2)
    ClBasic.Atom p :: TERM
p args :: [TERM_SEQ]
args -> VName -> RENAMES -> TERM -> [TERM_SEQ] -> Term
applyTermSeq VName
relSymb RENAMES
rn TERM
p [TERM_SEQ]
args
  ClBasic.Comment_sent _ s :: SENTENCE
s _ -> RENAMES -> SENTENCE -> Term
transSen RENAMES
rn SENTENCE
s
  ClBasic.Irregular_sent s :: SENTENCE
s _ -> RENAMES -> SENTENCE -> Term
transSen RENAMES
rn SENTENCE
s