{-# OPTIONS -w -O0 #-}
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.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token hiding (innerList)
import Data.Data
import Data.List
import Data.List (delete)
import Data.Maybe (isNothing)
import Data.Ord
import Fpl.As
import Fpl.Sign
import Text.ParserCombinators.Parsec
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
instance ShATermConvertible TermExt where
toShATermAux att0 xv = case xv of
FixDef a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "FixDef" [a'] []) att1
Case a b c -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
return $ addATerm (ShAAppl "Case" [a', b', c'] []) att3
Let a b c -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
return $ addATerm (ShAAppl "Let" [a', b', c'] []) att3
IfThenElse a b c d -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
(att4, d') <- toShATerm' att3 d
return $ addATerm (ShAAppl "IfThenElse" [a', b', c', d'] []) att4
EqTerm a b c -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
return $ addATerm (ShAAppl "EqTerm" [a', b', c'] []) att3
BoolTerm a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "BoolTerm" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "FixDef" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, FixDef a') }
ShAAppl "Case" [a, b, c] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
case fromShATerm' c att2 of
{ (att3, c') ->
(att3, Case a' b' c') }}}
ShAAppl "Let" [a, b, c] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
case fromShATerm' c att2 of
{ (att3, c') ->
(att3, Let a' b' c') }}}
ShAAppl "IfThenElse" [a, b, c, d] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
case fromShATerm' c att2 of
{ (att3, c') ->
case fromShATerm' d att3 of
{ (att4, d') ->
(att4, IfThenElse a' b' c' d') }}}}
ShAAppl "EqTerm" [a, b, c] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
case fromShATerm' c att2 of
{ (att3, c') ->
(att3, EqTerm a' b' c') }}}
ShAAppl "BoolTerm" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, BoolTerm a') }
u -> fromShATermError "TermExt" u
instance ShATermConvertible FunDef where
toShATermAux att0 xv = case xv of
FunDef a b c d -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
(att4, d') <- toShATerm' att3 d
return $ addATerm (ShAAppl "FunDef" [a', b', c', d'] []) att4
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "FunDef" [a, b, c, d] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
case fromShATerm' c att2 of
{ (att3, c') ->
case fromShATerm' d att3 of
{ (att4, d') ->
(att4, FunDef a' b' c' d') }}}}
u -> fromShATermError "FunDef" u
instance ShATermConvertible FplOpItem where
toShATermAux att0 xv = case xv of
FunOp a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "FunOp" [a'] []) att1
CaslOpItem a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "CaslOpItem" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "FunOp" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, FunOp a') }
ShAAppl "CaslOpItem" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, CaslOpItem a') }
u -> fromShATermError "FplOpItem" u
instance ShATermConvertible FplSortItem where
toShATermAux att0 xv = case xv of
FreeType a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "FreeType" [a'] []) att1
CaslSortItem a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "CaslSortItem" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "FreeType" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, FreeType a') }
ShAAppl "CaslSortItem" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, CaslSortItem a') }
u -> fromShATermError "FplSortItem" u
instance ShATermConvertible FplExt where
toShATermAux att0 xv = case xv of
FplSortItems a b -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "FplSortItems" [a', b'] []) att2
FplOpItems a b -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "FplOpItems" [a', b'] []) att2
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "FplSortItems" [a, b] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
(att2, FplSortItems a' b') }}
ShAAppl "FplOpItems" [a, b] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
(att2, FplOpItems a' b') }}
u -> fromShATermError "FplExt" u
instance ShATermConvertible SignExt where
toShATermAux att0 xv = case xv of
SignExt a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "SignExt" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "SignExt" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, SignExt a') }
u -> fromShATermError "SignExt" u