{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module Fpl.ATC_Fpl () where
import ATerm.Lib
import CASL.AS_Basic_CASL
import CASL.ATC_CASL
import CASL.Formula
import CASL.OpItem
import CASL.Sign
import CASL.SortItem
import CASL.ToDoc
import Common.AS_Annotation
import Common.AnnoState
import Common.Doc
import Common.Doc as Doc
import Common.DocUtils
import Common.Id
import Common.Json.Instances
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token hiding (innerList)
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.List
import Data.List (delete)
import Data.Maybe (isNothing)
import Data.Ord
import Fpl.As
import Fpl.Sign
import GHC.Generics(Generic)
import Text.ParserCombinators.Parsec
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
instance ShATermConvertible Fpl.As.FplExt where
toShATermAux :: ATermTable -> FplExt -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FplExt
xv = case FplExt
xv of
FplSortItems a :: [Annoted FplSortItem]
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted FplSortItem] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted FplSortItem]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "FplSortItems" [Int
a', Int
b'] []) ATermTable
att2
FplOpItems a :: [Annoted FplOpItem]
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted FplOpItem] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted FplOpItem]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "FplOpItems" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, FplExt)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "FplSortItems" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, [Annoted FplSortItem])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Annoted FplSortItem]
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [Annoted FplSortItem] -> Range -> FplExt
FplSortItems [Annoted FplSortItem]
a' Range
b') }}
ShAAppl "FplOpItems" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, [Annoted FplOpItem])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Annoted FplOpItem]
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [Annoted FplOpItem] -> Range -> FplExt
FplOpItems [Annoted FplOpItem]
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FplExt)
forall a. String -> ShATerm -> a
fromShATermError "Fpl.As.FplExt" ShATerm
u
instance ShATermConvertible Fpl.As.FplSortItem where
toShATermAux :: ATermTable -> FplSortItem -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FplSortItem
xv = case FplSortItem
xv of
FreeType a :: DATATYPE_DECL
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DATATYPE_DECL -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DATATYPE_DECL
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "FreeType" [Int
a'] []) ATermTable
att1
CaslSortItem a :: SORT_ITEM TermExt
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT_ITEM TermExt -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT_ITEM TermExt
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CaslSortItem" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, FplSortItem)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "FreeType" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, DATATYPE_DECL)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: DATATYPE_DECL
a') ->
(ATermTable
att1, DATATYPE_DECL -> FplSortItem
FreeType DATATYPE_DECL
a') }
ShAAppl "CaslSortItem" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, SORT_ITEM TermExt)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SORT_ITEM TermExt
a') ->
(ATermTable
att1, SORT_ITEM TermExt -> FplSortItem
CaslSortItem SORT_ITEM TermExt
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FplSortItem)
forall a. String -> ShATerm -> a
fromShATermError "Fpl.As.FplSortItem" ShATerm
u
instance ShATermConvertible Fpl.As.FplOpItem where
toShATermAux :: ATermTable -> FplOpItem -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FplOpItem
xv = case FplOpItem
xv of
FunOp a :: FunDef
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FunDef -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FunDef
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "FunOp" [Int
a'] []) ATermTable
att1
CaslOpItem a :: OP_ITEM TermExt
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OP_ITEM TermExt -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OP_ITEM TermExt
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CaslOpItem" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, FplOpItem)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "FunOp" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, FunDef)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: FunDef
a') ->
(ATermTable
att1, FunDef -> FplOpItem
FunOp FunDef
a') }
ShAAppl "CaslOpItem" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, OP_ITEM TermExt)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: OP_ITEM TermExt
a') ->
(ATermTable
att1, OP_ITEM TermExt -> FplOpItem
CaslOpItem OP_ITEM TermExt
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FplOpItem)
forall a. String -> ShATerm -> a
fromShATermError "Fpl.As.FplOpItem" ShATerm
u
instance ShATermConvertible Fpl.As.FunDef where
toShATermAux :: ATermTable -> FunDef -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FunDef
xv = case FunDef
xv of
FunDef a :: OP_NAME
a b :: OP_HEAD
b c :: Annoted FplTerm
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OP_NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OP_NAME
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> OP_HEAD -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 OP_HEAD
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Annoted FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Annoted FplTerm
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "FunDef" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, FunDef)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "FunDef" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, OP_NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: OP_NAME
a') ->
case Int -> ATermTable -> (ATermTable, OP_HEAD)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: OP_HEAD
b') ->
case Int -> ATermTable -> (ATermTable, Annoted FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Annoted FplTerm
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, OP_NAME -> OP_HEAD -> Annoted FplTerm -> Range -> FunDef
FunDef OP_NAME
a' OP_HEAD
b' Annoted FplTerm
c' Range
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FunDef)
forall a. String -> ShATerm -> a
fromShATermError "Fpl.As.FunDef" ShATerm
u
instance ShATermConvertible Fpl.As.TermExt where
toShATermAux :: ATermTable -> TermExt -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TermExt
xv = case TermExt
xv of
FixDef a :: FunDef
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FunDef -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FunDef
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "FixDef" [Int
a'] []) ATermTable
att1
Case a :: FplTerm
a b :: [(FplTerm, FplTerm)]
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FplTerm
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [(FplTerm, FplTerm)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [(FplTerm, FplTerm)]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Case" [Int
a', Int
b', Int
c'] []) ATermTable
att3
Let a :: FunDef
a b :: FplTerm
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FunDef -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FunDef
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FplTerm
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Let" [Int
a', Int
b', Int
c'] []) ATermTable
att3
IfThenElse a :: FplTerm
a b :: FplTerm
b c :: FplTerm
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FplTerm
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FplTerm
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FplTerm
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "IfThenElse" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
EqTerm a :: FplTerm
a b :: FplTerm
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FplTerm
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FplTerm
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "EqTerm" [Int
a', Int
b', Int
c'] []) ATermTable
att3
BoolTerm a :: FplTerm
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FplTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FplTerm
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "BoolTerm" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TermExt)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "FixDef" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, FunDef)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: FunDef
a') ->
(ATermTable
att1, FunDef -> TermExt
FixDef FunDef
a') }
ShAAppl "Case" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: FplTerm
a') ->
case Int -> ATermTable -> (ATermTable, [(FplTerm, FplTerm)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [(FplTerm, FplTerm)]
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, FplTerm -> [(FplTerm, FplTerm)] -> Range -> TermExt
Case FplTerm
a' [(FplTerm, FplTerm)]
b' Range
c') }}}
ShAAppl "Let" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, FunDef)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: FunDef
a') ->
case Int -> ATermTable -> (ATermTable, FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: FplTerm
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, FunDef -> FplTerm -> Range -> TermExt
Let FunDef
a' FplTerm
b' Range
c') }}}
ShAAppl "IfThenElse" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: FplTerm
a') ->
case Int -> ATermTable -> (ATermTable, FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: FplTerm
b') ->
case Int -> ATermTable -> (ATermTable, FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: FplTerm
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, FplTerm -> FplTerm -> FplTerm -> Range -> TermExt
IfThenElse FplTerm
a' FplTerm
b' FplTerm
c' Range
d') }}}}
ShAAppl "EqTerm" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: FplTerm
a') ->
case Int -> ATermTable -> (ATermTable, FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: FplTerm
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, FplTerm -> FplTerm -> Range -> TermExt
EqTerm FplTerm
a' FplTerm
b' Range
c') }}}
ShAAppl "BoolTerm" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, FplTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: FplTerm
a') ->
(ATermTable
att1, FplTerm -> TermExt
BoolTerm FplTerm
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TermExt)
forall a. String -> ShATerm -> a
fromShATermError "Fpl.As.TermExt" ShATerm
u
deriving instance GHC.Generics.Generic Fpl.As.FplExt
instance Data.Aeson.ToJSON Fpl.As.FplExt where
instance Data.Aeson.FromJSON Fpl.As.FplExt where
deriving instance GHC.Generics.Generic Fpl.As.FplSortItem
instance Data.Aeson.ToJSON Fpl.As.FplSortItem where
instance Data.Aeson.FromJSON Fpl.As.FplSortItem where
deriving instance GHC.Generics.Generic Fpl.As.FplOpItem
instance Data.Aeson.ToJSON Fpl.As.FplOpItem where
instance Data.Aeson.FromJSON Fpl.As.FplOpItem where
deriving instance GHC.Generics.Generic Fpl.As.FunDef
instance Data.Aeson.ToJSON Fpl.As.FunDef where
instance Data.Aeson.FromJSON Fpl.As.FunDef where
deriving instance GHC.Generics.Generic Fpl.As.TermExt
instance Data.Aeson.ToJSON Fpl.As.TermExt where
instance Data.Aeson.FromJSON Fpl.As.TermExt where
deriving instance GHC.Generics.Generic Fpl.Sign.SignExt
instance Data.Aeson.ToJSON Fpl.Sign.SignExt where
instance Data.Aeson.FromJSON Fpl.Sign.SignExt where
instance ShATermConvertible Fpl.Sign.SignExt where
toShATermAux :: ATermTable -> SignExt -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SignExt
xv = case SignExt
xv of
SignExt a :: OpMap
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpMap
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SignExt" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, SignExt)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SignExt" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, OpMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: OpMap
a') ->
(ATermTable
att1, OpMap -> SignExt
SignExt OpMap
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SignExt)
forall a. String -> ShATerm -> a
fromShATermError "Fpl.Sign.SignExt" ShATerm
u