{- |
Module      :  ./CASL/ToTIP.hs
Description :  represent CASL in TIP format
Copyright   :  (c) Tom Kranz 2022
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :
Stability   :  experimental
Portability : 

translations from CASL specs to TIP format

This module provides functions for expressing CASL signatures in
  TIP declarations and converting single sentences to declarations.
-}
module CASL.ToTIP where

import TIP.AbsTIP
import TIP.Utils

import qualified CASL.Sign as CS
import CASL.AS_Basic_CASL
import CASL.Utils (codeOutUniqueExtF)
import CASL.Induction (inductionSentence)
import Common.DocUtils
import Common.Id (mkId)
import Common.AS_Annotation
import qualified Common.Lib.MapSet as MapSet

import qualified Data.Set as Set
import Data.Maybe (mapMaybe)
import Data.List (intercalate)

tipSign :: (CS.CASLSign, [Named CASLFORMULA]) -> [Decl]
tipSign :: (CASLSign, [Named CASLFORMULA]) -> [Decl]
tipSign (sig :: CASLSign
sig, thry :: [Named CASLFORMULA]
thry) =
  (SORT -> Decl) -> [SORT] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Decl
declareSort (Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
CS.sortSet CASLSign
sig) Set SORT
freeTypes))
  [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ ([(DatatypeName, Datatype)] -> [Decl]
declareData ([(DatatypeName, Datatype)] -> [Decl])
-> [(DatatypeName, Datatype)] -> [Decl]
forall a b. (a -> b) -> a -> b
$ ((SORT, [OP_SYMB]) -> (DatatypeName, Datatype))
-> [(SORT, [OP_SYMB])] -> [(DatatypeName, Datatype)]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, [OP_SYMB]) -> (DatatypeName, Datatype)
tipDatatype ([(SORT, [OP_SYMB])] -> [(DatatypeName, Datatype)])
-> [(SORT, [OP_SYMB])] -> [(DatatypeName, Datatype)]
forall a b. (a -> b) -> a -> b
$ [[(SORT, [OP_SYMB])]] -> [(SORT, [OP_SYMB])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(SORT, [OP_SYMB])]]
fTAC)
  [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ ((SORT, PredType) -> Decl) -> [(SORT, PredType)] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, PredType) -> Decl
declarePred (MapSet SORT PredType -> [(SORT, PredType)]
forall a b. MapSet a b -> [(a, b)]
MapSet.toPairList (CASLSign -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
CS.predMap CASLSign
sig))
  [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ ((SORT, OpType) -> Decl) -> [(SORT, OpType)] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, OpType) -> Decl
declareOp (((SORT, OpType) -> Bool) -> [(SORT, OpType)] -> [(SORT, OpType)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((((SORT, OpType) -> Set (SORT, OpType) -> Bool)
-> Set (SORT, OpType) -> (SORT, OpType) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (SORT, OpType) -> Set (SORT, OpType) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember) Set (SORT, OpType)
constructors) ([(SORT, OpType)] -> [(SORT, OpType)])
-> [(SORT, OpType)] -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ MapSet SORT OpType -> [(SORT, OpType)]
forall a b. MapSet a b -> [(a, b)]
MapSet.toPairList (CASLSign -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
CS.opMap CASLSign
sig))
    where 
      fTAC :: [[(SORT, [OP_SYMB])]]
fTAC = [Named CASLFORMULA] -> [[(SORT, [OP_SYMB])]]
forall f. [Named (FORMULA f)] -> [[(SORT, [OP_SYMB])]]
freeTypesAndCons [Named CASLFORMULA]
thry
      constructors :: Set (SORT, OpType)
constructors = [(SORT, OpType)] -> Set (SORT, OpType)
forall a. Ord a => [a] -> Set a
Set.fromList ([(SORT, OpType)] -> Set (SORT, OpType))
-> [(SORT, OpType)] -> Set (SORT, OpType)
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> (SORT, OpType)) -> [OP_SYMB] -> [(SORT, OpType)]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> (SORT, OpType)
fromOP_SYMBtoOpMapPair ([OP_SYMB] -> [(SORT, OpType)]) -> [OP_SYMB] -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ ((SORT, [OP_SYMB]) -> [OP_SYMB])
-> [(SORT, [OP_SYMB])] -> [OP_SYMB]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SORT, [OP_SYMB]) -> [OP_SYMB]
forall a b. (a, b) -> b
snd ([(SORT, [OP_SYMB])] -> [OP_SYMB])
-> [(SORT, [OP_SYMB])] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ [[(SORT, [OP_SYMB])]] -> [(SORT, [OP_SYMB])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(SORT, [OP_SYMB])]]
fTAC
      freeTypes :: Set SORT
freeTypes = [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList ([SORT] -> Set SORT) -> [SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ ((SORT, [OP_SYMB]) -> SORT) -> [(SORT, [OP_SYMB])] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, [OP_SYMB]) -> SORT
forall a b. (a, b) -> a
fst ([(SORT, [OP_SYMB])] -> [SORT]) -> [(SORT, [OP_SYMB])] -> [SORT]
forall a b. (a -> b) -> a -> b
$ [[(SORT, [OP_SYMB])]] -> [(SORT, [OP_SYMB])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(SORT, [OP_SYMB])]]
fTAC

fromOP_SYMBtoOpMapPair :: OP_SYMB -> (OP_NAME,CS.OpType)
fromOP_SYMBtoOpMapPair :: OP_SYMB -> (SORT, OpType)
fromOP_SYMBtoOpMapPair (Qual_op_name n :: SORT
n ty :: OP_TYPE
ty _) = (SORT
n, OP_TYPE -> OpType
CS.toOpType OP_TYPE
ty)
fromOP_SYMBtoOpMapPair o :: OP_SYMB
o = [Char] -> (SORT, OpType)
forall a. HasCallStack => [Char] -> a
error ("CASL.ToTIP.fromOP_SYMBtoOpMapPair" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Doc -> [Char]
forall a. Show a => a -> [Char]
show(Doc -> [Char]) -> (OP_SYMB -> Doc) -> OP_SYMB -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.OP_SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty) OP_SYMB
o)

tipAxiom :: Named CASLFORMULA -> Decl
tipAxiom :: Named CASLFORMULA -> Decl
tipAxiom f :: Named CASLFORMULA
f = 
  Assertion -> [Attr] -> Expr -> Decl
Formula Assertion
Assert [([Char], Maybe [Char]) -> Attr
toAttr ("axiom",[Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> [Char]
forall s a. SenAttr s a -> a
senAttr Named CASLFORMULA
f)] (Expr -> Decl) -> Expr -> Decl
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Expr
tipFORMULA (CASLFORMULA -> Expr) -> CASLFORMULA -> Expr
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
f

tipFORMULA :: CASLFORMULA -> Expr
tipFORMULA :: CASLFORMULA -> Expr
tipFORMULA = Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA Set (SORT, PredType)
forall a. Set a
Set.empty

tipSOFORMULA :: Set.Set (PRED_NAME,CS.PredType) -> CASLFORMULA -> Expr
tipSOFORMULA :: Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds f :: CASLFORMULA
f@(Quantification Unique_existential _ _ _) = Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA Set (SORT, PredType)
qPreds (CASLFORMULA -> Expr) -> CASLFORMULA -> Expr
forall a b. (a -> b) -> a -> b
$ (() -> ()) -> (() -> ()) -> CASLFORMULA -> CASLFORMULA
forall f. (f -> f) -> (f -> f) -> FORMULA f -> FORMULA f
codeOutUniqueExtF () -> ()
forall a. a -> a
id () -> ()
forall a. a -> a
id CASLFORMULA
f
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds (Quantification q :: QUANTIFIER
q vds :: [VAR_DECL]
vds f :: CASLFORMULA
f _) = Binder -> [Binding] -> Expr -> Expr
Binder (QUANTIFIER -> Binder
tipQUANTIFIER QUANTIFIER
q) ((VAR_DECL -> [Binding]) -> [VAR_DECL] -> [Binding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VAR_DECL -> [Binding]
tipVAR_DECL [VAR_DECL]
vds) (Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA Set (SORT, PredType)
qPreds CASLFORMULA
f)
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds (Junction j :: Junctor
j fs :: [CASLFORMULA]
fs _) = Head -> [Expr] -> Expr
App (Junctor -> Head
tipJunctor Junctor
j) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (CASLFORMULA -> Expr) -> [CASLFORMULA] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA Set (SORT, PredType)
qPreds) [CASLFORMULA]
fs
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds (Relation lhs :: CASLFORMULA
lhs r :: Relation
r rhs :: CASLFORMULA
rhs _) = Head -> [Expr] -> Expr
App (Relation -> Head
tipRelation Relation
r) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (CASLFORMULA -> Expr) -> [CASLFORMULA] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA Set (SORT, PredType)
qPreds) [CASLFORMULA
lhs, CASLFORMULA
rhs]
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds (Negation f :: CASLFORMULA
f _) = Head -> [Expr] -> Expr
App Head
Not [Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA Set (SORT, PredType)
qPreds CASLFORMULA
f]
tipSOFORMULA _Preds :: Set (SORT, PredType)
_Preds (Atom b :: Bool
b _) = Lit -> Expr
Lit (if Bool
b then Lit
LitTrue else Lit
LitFalse)
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds (Predication p :: PRED_SYMB
p@(Qual_pred_name pName :: SORT
pName pType :: PRED_TYPE
pType@(Pred_type pSorts :: [SORT]
pSorts _) _) ts :: [TERM ()]
ts _)
  | (SORT
pName,PRED_TYPE -> PredType
CS.toPredType PRED_TYPE
pType) (SORT, PredType) -> Set (SORT, PredType) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (SORT, PredType)
qPreds = Head -> [Expr] -> Expr
App Head
At (PolySymbol -> Expr
Var (Symbol -> PolySymbol
NoAs (Symbol -> PolySymbol) -> Symbol -> PolySymbol
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT -> Symbol
tipPredVAR [SORT]
pSorts SORT
pName) Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: (TERM () -> Expr) -> [TERM ()] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Set (SORT, PredType) -> TERM () -> Expr
tipSOTERM Set (SORT, PredType)
qPreds) [TERM ()]
ts)
  | Bool
otherwise = Head -> [Expr] -> Expr
App (PolySymbol -> Head
Const (PolySymbol -> Head) -> PolySymbol -> Head
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> PolySymbol
tipPRED_SYMB PRED_SYMB
p) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (TERM () -> Expr) -> [TERM ()] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Set (SORT, PredType) -> TERM () -> Expr
tipSOTERM Set (SORT, PredType)
qPreds) [TERM ()]
ts
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds (Equation lhs :: TERM ()
lhs Strong rhs :: TERM ()
rhs _) = Head -> [Expr] -> Expr
App Head
Equal ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (TERM () -> Expr) -> [TERM ()] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Set (SORT, PredType) -> TERM () -> Expr
tipSOTERM Set (SORT, PredType)
qPreds) [TERM ()
lhs, TERM ()
rhs] 
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds (Sort_gen_ax cs :: [Constraint]
cs _) = Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA Set (SORT, PredType)
qPreds (CASLFORMULA -> Expr) -> CASLFORMULA -> Expr
forall a b. (a -> b) -> a -> b
$ [Constraint] -> CASLFORMULA
forall f. FormExtension f => [Constraint] -> FORMULA f
inductionSentence [Constraint]
cs
tipSOFORMULA qPreds :: Set (SORT, PredType)
qPreds (QuantPred pName :: SORT
pName pType :: PRED_TYPE
pType f :: CASLFORMULA
f) =
  let pT :: PredType
pT = PRED_TYPE -> PredType
CS.toPredType PRED_TYPE
pType in
      Binder -> [Binding] -> Expr -> Expr
Binder Binder
Forall (SORT -> PredType -> [Binding]
tipPredVAR_DECL SORT
pName PredType
pT) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA ((SORT, PredType) -> Set (SORT, PredType) -> Set (SORT, PredType)
forall a. Ord a => a -> Set a -> Set a
Set.insert (SORT
pName,PredType
pT) Set (SORT, PredType)
qPreds) CASLFORMULA
f
tipSOFORMULA _Preds :: Set (SORT, PredType)
_Preds f :: CASLFORMULA
f = [Char] -> Expr
forall a. HasCallStack => [Char] -> a
error ("CASL.ToTIP.tipSOFORMULA" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Doc -> [Char]
forall a. Show a => a -> [Char]
show(Doc -> [Char]) -> (CASLFORMULA -> Doc) -> CASLFORMULA -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CASLFORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty) CASLFORMULA
f)
--(Definedness (TERM f) Range)
--(Membership (TERM f) SORT Range)
--(Mixfix_formula (TERM f))
--(Unparsed_formula String Range)
--(QuantOp OP_NAME OP_TYPE (FORMULA f))
--(ExtFORMULA f)

tipSOTERM :: Set.Set (PRED_NAME,CS.PredType) -> TERM () -> Expr
tipSOTERM :: Set (SORT, PredType) -> TERM () -> Expr
tipSOTERM _Preds :: Set (SORT, PredType)
_Preds (Qual_var v :: VAR
v s :: SORT
s _) = PolySymbol -> Expr
Var (PolySymbol -> Expr) -> PolySymbol -> Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> PolySymbol
NoAs (SORT -> VAR -> Symbol
tipVAR SORT
s VAR
v)
tipSOTERM qPreds :: Set (SORT, PredType)
qPreds (Sorted_term t :: TERM ()
t _ _) = Set (SORT, PredType) -> TERM () -> Expr
tipSOTERM Set (SORT, PredType)
qPreds TERM ()
t
tipSOTERM qPreds :: Set (SORT, PredType)
qPreds (Application op :: OP_SYMB
op ts :: [TERM ()]
ts _) = Head -> [Expr] -> Expr
App (PolySymbol -> Head
Const (PolySymbol -> Head) -> PolySymbol -> Head
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> PolySymbol
tipOP_SYMB OP_SYMB
op) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (TERM () -> Expr) -> [TERM ()] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Set (SORT, PredType) -> TERM () -> Expr
tipSOTERM Set (SORT, PredType)
qPreds) [TERM ()]
ts
tipSOTERM qPreds :: Set (SORT, PredType)
qPreds (Conditional t :: TERM ()
t c :: CASLFORMULA
c f :: TERM ()
f _) = Head -> [Expr] -> Expr
App Head
IfThenElse [Set (SORT, PredType) -> CASLFORMULA -> Expr
tipSOFORMULA Set (SORT, PredType)
qPreds CASLFORMULA
c, Set (SORT, PredType) -> TERM () -> Expr
tipSOTERM Set (SORT, PredType)
qPreds TERM ()
t, Set (SORT, PredType) -> TERM () -> Expr
tipSOTERM Set (SORT, PredType)
qPreds TERM ()
f]
tipSOTERM _Preds :: Set (SORT, PredType)
_Preds t :: TERM ()
t = [Char] -> Expr
forall a. HasCallStack => [Char] -> a
error ("CASL.ToTIP.tipSOTERM" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Doc -> [Char]
forall a. Show a => a -> [Char]
show(Doc -> [Char]) -> (TERM () -> Doc) -> TERM () -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty) TERM ()
t)

tipOP_SYMB :: OP_SYMB -> PolySymbol
tipOP_SYMB :: OP_SYMB -> PolySymbol
tipOP_SYMB (Qual_op_name n :: SORT
n ot :: OP_TYPE
ot _) = Symbol -> PolySymbol
NoAs (Symbol -> PolySymbol) -> Symbol -> PolySymbol
forall a b. (a -> b) -> a -> b
$ SORT -> [SORT] -> SORT -> Symbol
tipOP_NAME (OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
ot) (OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
ot) SORT
n
tipOP_SYMB o :: OP_SYMB
o = [Char] -> PolySymbol
forall a. HasCallStack => [Char] -> a
error ("CASL.ToTIP.tipOP_SYMB" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Doc -> [Char]
forall a. Show a => a -> [Char]
show(Doc -> [Char]) -> (OP_SYMB -> Doc) -> OP_SYMB -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.OP_SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty) OP_SYMB
o)

tipOP_NAME :: SORT -> [SORT] -> OP_NAME -> Symbol
tipOP_NAME :: SORT -> [SORT] -> SORT -> Symbol
tipOP_NAME = [Char] -> Maybe SORT -> [SORT] -> SORT -> Symbol
forall a. Show a => [Char] -> Maybe SORT -> [SORT] -> a -> Symbol
qualNameToSymbol "f" (Maybe SORT -> [SORT] -> SORT -> Symbol)
-> (SORT -> Maybe SORT) -> SORT -> [SORT] -> SORT -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Maybe SORT
forall a. a -> Maybe a
Just

tipPRED_SYMB :: PRED_SYMB -> PolySymbol
tipPRED_SYMB :: PRED_SYMB -> PolySymbol
tipPRED_SYMB (Qual_pred_name n :: SORT
n (Pred_type as :: [SORT]
as _) _) = Symbol -> PolySymbol
NoAs (Symbol -> PolySymbol) -> Symbol -> PolySymbol
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT -> Symbol
tipPRED_NAME [SORT]
as SORT
n
tipPRED_SYMB p :: PRED_SYMB
p = [Char] -> PolySymbol
forall a. HasCallStack => [Char] -> a
error ("CASL.ToTIP.tipPRED_SYMB" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Doc -> [Char]
forall a. Show a => a -> [Char]
show(Doc -> [Char]) -> (PRED_SYMB -> Doc) -> PRED_SYMB -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PRED_SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty) PRED_SYMB
p)

tipPRED_NAME :: [SORT] -> PRED_NAME -> Symbol
tipPRED_NAME :: [SORT] -> SORT -> Symbol
tipPRED_NAME = [Char] -> Maybe SORT -> [SORT] -> SORT -> Symbol
forall a. Show a => [Char] -> Maybe SORT -> [SORT] -> a -> Symbol
qualNameToSymbol "p" Maybe SORT
forall a. Maybe a
Nothing

tipProfile :: [SORT] -> Maybe SORT -> String
tipProfile :: [SORT] -> Maybe SORT -> [Char]
tipProfile as :: [SORT]
as r :: Maybe SORT
r = let addArrow :: [Char] -> [Char]
addArrow = if [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
as then [Char] -> [Char]
forall a. a -> a
id else ("->"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) in
  [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate "*" ((SORT -> [Char]) -> [SORT] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> [Char]
forall a. Show a => a -> [Char]
show [SORT]
as) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> (SORT -> [Char]) -> Maybe SORT -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" ([Char] -> [Char]
addArrow([Char] -> [Char]) -> (SORT -> [Char]) -> SORT -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.SORT -> [Char]
forall a. Show a => a -> [Char]
show) Maybe SORT
r

tipRelation :: Relation -> Head
tipRelation :: Relation -> Head
tipRelation Equivalence = Head
Equal
tipRelation _ = Head
Implies

tipJunctor :: Junctor -> Head
tipJunctor :: Junctor -> Head
tipJunctor Con = Head
And
tipJunctor Dis = Head
Or

tipQUANTIFIER :: QUANTIFIER -> Binder
tipQUANTIFIER :: QUANTIFIER -> Binder
tipQUANTIFIER Universal = Binder
Forall
tipQUANTIFIER Existential = Binder
Exists
tipQUANTIFIER Unique_existential = [Char] -> Binder
forall a. HasCallStack => [Char] -> a
error "CASL.ToTIP.tipQUANTIFIER: Unique_existential should have been coded out before getting here."

tipPredVAR_DECL :: PRED_NAME -> CS.PredType -> [Binding]
tipPredVAR_DECL :: SORT -> PredType -> [Binding]
tipPredVAR_DECL pN :: SORT
pN pT :: PredType
pT = let pS :: [SORT]
pS = PredType -> [SORT]
CS.predArgs PredType
pT in
  [Symbol -> Type -> Binding
Binding ([SORT] -> SORT -> Symbol
tipPredVAR [SORT]
pS SORT
pN) (Type -> Binding) -> Type -> Binding
forall a b. (a -> b) -> a -> b
$
    [Type] -> Type
ArrowTy ((SORT -> Type) -> [SORT] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Type
TyVar (Symbol -> Type) -> (SORT -> Symbol) -> SORT -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Symbol
tipSORT) [SORT]
pS [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
BoolTy])]

tipPredVAR :: [SORT] -> PRED_NAME -> Symbol
tipPredVAR :: [SORT] -> SORT -> Symbol
tipPredVAR = [Char] -> Maybe SORT -> [SORT] -> SORT -> Symbol
forall a. Show a => [Char] -> Maybe SORT -> [SORT] -> a -> Symbol
qualNameToSymbol "P" Maybe SORT
forall a. Maybe a
Nothing

tipVAR_DECL :: VAR_DECL -> [Binding]
tipVAR_DECL :: VAR_DECL -> [Binding]
tipVAR_DECL (Var_decl vars :: [VAR]
vars sort :: SORT
sort _) = (VAR -> Binding) -> [VAR] -> [Binding]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: VAR
v -> Symbol -> Type -> Binding
Binding (SORT -> VAR -> Symbol
tipVAR SORT
sort VAR
v) (Symbol -> Type
TyVar (Symbol -> Type) -> Symbol -> Type
forall a b. (a -> b) -> a -> b
$ SORT -> Symbol
tipSORT SORT
sort)) [VAR]
vars

tipVAR :: SORT -> VAR -> Symbol
tipVAR :: SORT -> VAR -> Symbol
tipVAR s :: SORT
s = [Char] -> Maybe SORT -> [SORT] -> SORT -> Symbol
forall a. Show a => [Char] -> Maybe SORT -> [SORT] -> a -> Symbol
qualNameToSymbol "F" (SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
s) [] (SORT -> Symbol) -> (VAR -> SORT) -> VAR -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR] -> SORT
mkId ([VAR] -> SORT) -> (VAR -> [VAR]) -> VAR -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR -> [VAR] -> [VAR]
forall a. a -> [a] -> [a]
: [])

tipSORT :: SORT -> Symbol
tipSORT :: SORT -> Symbol
tipSORT = [Char] -> Maybe SORT -> [SORT] -> SORT -> Symbol
forall a. Show a => [Char] -> Maybe SORT -> [SORT] -> a -> Symbol
qualNameToSymbol "s" Maybe SORT
forall a. Maybe a
Nothing []

qualNameToSymbol :: Show a => String -> Maybe SORT -> [SORT] -> a -> Symbol
qualNameToSymbol :: [Char] -> Maybe SORT -> [SORT] -> a -> Symbol
qualNameToSymbol prefix :: [Char]
prefix resSort :: Maybe SORT
resSort argSorts :: [SORT]
argSorts i :: a
i =
  [Char] -> Symbol
toSymbol ([Char]
prefix [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SORT] -> Maybe SORT -> [Char]
tipProfile [SORT]
argSorts Maybe SORT
resSort [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i)

tipDatatype :: (SORT, [OP_SYMB]) -> (DatatypeName, Datatype)
tipDatatype :: (SORT, [OP_SYMB]) -> (DatatypeName, Datatype)
tipDatatype (s :: SORT
s,cs :: [OP_SYMB]
cs) =
  ( AttrSymbol -> Integer -> DatatypeName
DatatypeName (Symbol -> [Attr] -> AttrSymbol
AttrSymbol (SORT -> Symbol
tipSORT SORT
s) []) 0
  , InnerDatatype -> Datatype
DatatypeMono (InnerDatatype -> Datatype) -> InnerDatatype -> Datatype
forall a b. (a -> b) -> a -> b
$ [Constructor] -> InnerDatatype
InnerDatatype ([Constructor] -> InnerDatatype) -> [Constructor] -> InnerDatatype
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> Constructor) -> [OP_SYMB] -> [Constructor]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> Constructor
tipConstructor [OP_SYMB]
cs)

tipConstructor :: OP_SYMB -> Constructor
tipConstructor :: OP_SYMB -> Constructor
tipConstructor (Qual_op_name n :: SORT
n ts :: OP_TYPE
ts _) =
  let as :: [SORT]
as = OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
ts; r :: SORT
r = OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
ts; s :: Symbol
s = SORT -> [SORT] -> SORT -> Symbol
tipOP_NAME SORT
r [SORT]
as SORT
n in
      AttrSymbol -> [Binding] -> Constructor
Constructor (Symbol -> [Attr] -> AttrSymbol
AttrSymbol Symbol
s []) ([Binding] -> Constructor) -> [Binding] -> Constructor
forall a b. (a -> b) -> a -> b
$
        ((SORT, Integer) -> Binding) -> [(SORT, Integer)] -> [Binding]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> (SORT, Integer) -> Binding
tipSelector Symbol
s) ([SORT] -> [Integer] -> [(SORT, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SORT]
as [1..])
tipConstructor o :: OP_SYMB
o = [Char] -> Constructor
forall a. HasCallStack => [Char] -> a
error ("CASL.ToTIP.tipConstructor" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Doc -> [Char]
forall a. Show a => a -> [Char]
show(Doc -> [Char]) -> (OP_SYMB -> Doc) -> OP_SYMB -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.OP_SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty) OP_SYMB
o)

tipSelector :: Symbol -> (SORT,Integer) -> Binding
tipSelector :: Symbol -> (SORT, Integer) -> Binding
tipSelector s :: Symbol
s (r :: SORT
r,i :: Integer
i) =
  Symbol -> Type -> Binding
Binding ([Char] -> Maybe SORT -> [SORT] -> Doc -> Symbol
forall a. Show a => [Char] -> Maybe SORT -> [SORT] -> a -> Symbol
qualNameToSymbol ('i' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
i) Maybe SORT
forall a. Maybe a
Nothing [] (Doc -> Symbol) -> Doc -> Symbol
forall a b. (a -> b) -> a -> b
$
    [Char] -> Doc
forall a. Pretty a => a -> Doc
pretty (Symbol -> [Char]
fromSymbol Symbol
s)) (Symbol -> Type
TyVar (Symbol -> Type) -> Symbol -> Type
forall a b. (a -> b) -> a -> b
$ SORT -> Symbol
tipSORT SORT
r)

freeTypesAndCons :: [Named (FORMULA f)] -> [[(SORT, [OP_SYMB])]]
freeTypesAndCons :: [Named (FORMULA f)] -> [[(SORT, [OP_SYMB])]]
freeTypesAndCons = (Named (FORMULA f) -> Maybe [(SORT, [OP_SYMB])])
-> [Named (FORMULA f)] -> [[(SORT, [OP_SYMB])]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Named (FORMULA f) -> Maybe [(SORT, [OP_SYMB])])
 -> [Named (FORMULA f)] -> [[(SORT, [OP_SYMB])]])
-> (Named (FORMULA f) -> Maybe [(SORT, [OP_SYMB])])
-> [Named (FORMULA f)]
-> [[(SORT, [OP_SYMB])]]
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Maybe [(SORT, [OP_SYMB])]
forall f. FORMULA f -> Maybe [(SORT, [OP_SYMB])]
justFTAC (FORMULA f -> Maybe [(SORT, [OP_SYMB])])
-> (Named (FORMULA f) -> FORMULA f)
-> Named (FORMULA f)
-> Maybe [(SORT, [OP_SYMB])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence
  where
    justFTAC :: FORMULA f -> Maybe [(SORT, [OP_SYMB])]
justFTAC (Sort_gen_ax cs :: [Constraint]
cs True) = [(SORT, [OP_SYMB])] -> Maybe [(SORT, [OP_SYMB])]
forall a. a -> Maybe a
Just ([(SORT, [OP_SYMB])] -> Maybe [(SORT, [OP_SYMB])])
-> [(SORT, [OP_SYMB])] -> Maybe [(SORT, [OP_SYMB])]
forall a b. (a -> b) -> a -> b
$ [Constraint] -> [(SORT, [OP_SYMB])]
recoverSortGen [Constraint]
cs
    justFTAC _ = Maybe [(SORT, [OP_SYMB])]
forall a. Maybe a
Nothing

declareSort :: SORT -> Decl
declareSort :: SORT -> Decl
declareSort s :: SORT
s = AttrSymbol -> Integer -> Decl
DeclareSort (Symbol -> [Attr] -> AttrSymbol
AttrSymbol (SORT -> Symbol
tipSORT SORT
s) []) 0

declareOp :: (OP_NAME, CS.OpType) -> Decl
declareOp :: (SORT, OpType) -> Decl
declareOp (o :: SORT
o, ot :: OpType
ot)
  | [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
as
  = AttrSymbol -> ConstType -> Decl
DeclareConst AttrSymbol
symbol (ConstType -> Decl) -> ConstType -> Decl
forall a b. (a -> b) -> a -> b
$ Type -> ConstType
ConstTypeMono Type
ty
  | Bool
otherwise
  = AttrSymbol -> FunType -> Decl
DeclareFun AttrSymbol
symbol (FunType -> Decl) -> FunType -> Decl
forall a b. (a -> b) -> a -> b
$ InnerFunType -> FunType
FunTypeMono (InnerFunType -> FunType) -> InnerFunType -> FunType
forall a b. (a -> b) -> a -> b
$ [Type] -> Type -> InnerFunType
InnerFunType ((SORT -> Type) -> [SORT] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Type
TyVar (Symbol -> Type) -> (SORT -> Symbol) -> SORT -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Symbol
tipSORT) [SORT]
as) Type
ty
    where as :: [SORT]
as = OpType -> [SORT]
CS.opArgs OpType
ot
          r :: SORT
r = OpType -> SORT
CS.opRes OpType
ot
          symbol :: AttrSymbol
symbol = Symbol -> [Attr] -> AttrSymbol
AttrSymbol (SORT -> [SORT] -> SORT -> Symbol
tipOP_NAME SORT
r [SORT]
as SORT
o) []
          ty :: Type
ty = Symbol -> Type
TyVar (Symbol -> Type) -> Symbol -> Type
forall a b. (a -> b) -> a -> b
$ SORT -> Symbol
tipSORT SORT
r

declarePred :: (PRED_NAME, CS.PredType) -> Decl
declarePred :: (SORT, PredType) -> Decl
declarePred (p :: SORT
p, pt :: PredType
pt)
  | [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
as
  = AttrSymbol -> ConstType -> Decl
DeclareConst AttrSymbol
symbol (ConstType -> Decl) -> ConstType -> Decl
forall a b. (a -> b) -> a -> b
$ Type -> ConstType
ConstTypeMono Type
BoolTy
  | Bool
otherwise
  = AttrSymbol -> FunType -> Decl
DeclareFun AttrSymbol
symbol (FunType -> Decl) -> FunType -> Decl
forall a b. (a -> b) -> a -> b
$ InnerFunType -> FunType
FunTypeMono (InnerFunType -> FunType) -> InnerFunType -> FunType
forall a b. (a -> b) -> a -> b
$ [Type] -> Type -> InnerFunType
InnerFunType ((SORT -> Type) -> [SORT] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Type
TyVar (Symbol -> Type) -> (SORT -> Symbol) -> SORT -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Symbol
tipSORT) [SORT]
as) Type
BoolTy
    where as :: [SORT]
as = PredType -> [SORT]
CS.predArgs PredType
pt
          symbol :: AttrSymbol
symbol = Symbol -> [Attr] -> AttrSymbol
AttrSymbol ([SORT] -> SORT -> Symbol
tipPRED_NAME [SORT]
as SORT
p) []