{-# OPTIONS -w -O0 #-}
module LF.ATC_LF () where
import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation
import Common.Doc
import Common.Doc hiding (space)
import Common.DocUtils
import Common.Id
import Common.Keywords
import Common.Result
import Data.Data
import Data.List
import Data.Maybe
import Data.Maybe (isNothing, fromMaybe)
import LF.AS
import LF.Morphism
import LF.Sign
import qualified Data.Map as Map
import qualified Data.Set as Set
instance ShATermConvertible BASIC_SPEC where
toShATermAux att0 xv = case xv of
Basic_spec a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Basic_spec" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Basic_spec" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Basic_spec a') }
u -> fromShATermError "BASIC_SPEC" u
instance ShATermConvertible BASIC_ITEM where
toShATermAux att0 xv = case xv of
Decl a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Decl" [a'] []) att1
Form a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Form" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Decl" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Decl a') }
ShAAppl "Form" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Form a') }
u -> fromShATermError "BASIC_ITEM" u
instance ShATermConvertible SYMB_ITEMS where
toShATermAux att0 xv = case xv of
Symb_items a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Symb_items" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Symb_items" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Symb_items a') }
u -> fromShATermError "SYMB_ITEMS" u
instance ShATermConvertible SYMB_MAP_ITEMS where
toShATermAux att0 xv = case xv of
Symb_map_items a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Symb_map_items" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Symb_map_items" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Symb_map_items a') }
u -> fromShATermError "SYMB_MAP_ITEMS" u
instance ShATermConvertible SYMB_OR_MAP where
toShATermAux att0 xv = case xv of
Symb a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Symb" [a'] []) att1
Symb_map a b -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "Symb_map" [a', b'] []) att2
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Symb" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Symb a') }
ShAAppl "Symb_map" [a, b] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
(att2, Symb_map a' b') }}
u -> fromShATermError "SYMB_OR_MAP" u
instance ShATermConvertible Morphism where
toShATermAux att0 xv = case xv of
Morphism a b c d e f g -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
(att4, d') <- toShATerm' att3 d
(att5, e') <- toShATerm' att4 e
(att6, f') <- toShATerm' att5 f
(att7, g') <- toShATerm' att6 g
return $ addATerm (ShAAppl "Morphism" [a', b', c', d', e', f',
g'] []) att7
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Morphism" [a, b, c, d, e, f, g] _ ->
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') ->
case fromShATerm' e att4 of
{ (att5, e') ->
case fromShATerm' f att5 of
{ (att6, f') ->
case fromShATerm' g att6 of
{ (att7, g') ->
(att7, Morphism a' b' c' d' e' f' g') }}}}}}}
u -> fromShATermError "Morphism" u
instance ShATermConvertible MorphType where
toShATermAux att0 xv = case xv of
Definitional -> return $ addATerm (ShAAppl "Definitional" [] []) att0
Postulated -> return $ addATerm (ShAAppl "Postulated" [] []) att0
Unknown -> return $ addATerm (ShAAppl "Unknown" [] []) att0
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Definitional" [] _ -> (att0, Definitional)
ShAAppl "Postulated" [] _ -> (att0, Postulated)
ShAAppl "Unknown" [] _ -> (att0, Unknown)
u -> fromShATermError "MorphType" u
instance ShATermConvertible Symbol where
toShATermAux att0 xv = case xv of
Symbol a b c -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
return $ addATerm (ShAAppl "Symbol" [a', b', c'] []) att3
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Symbol" [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, Symbol a' b' c') }}}
u -> fromShATermError "Symbol" u
instance ShATermConvertible EXP where
toShATermAux att0 xv = case xv of
Type -> return $ addATerm (ShAAppl "Type" [] []) att0
Var a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Var" [a'] []) att1
Const a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Const" [a'] []) att1
Appl a b -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "Appl" [a', b'] []) att2
Func a b -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "Func" [a', b'] []) att2
Pi a b -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "Pi" [a', b'] []) att2
Lamb a b -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "Lamb" [a', b'] []) att2
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Type" [] _ -> (att0, Type)
ShAAppl "Var" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Var a') }
ShAAppl "Const" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Const a') }
ShAAppl "Appl" [a, b] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
(att2, Appl a' b') }}
ShAAppl "Func" [a, b] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
(att2, Func a' b') }}
ShAAppl "Pi" [a, b] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
(att2, Pi a' b') }}
ShAAppl "Lamb" [a, b] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
(att2, Lamb a' b') }}
u -> fromShATermError "EXP" u
instance ShATermConvertible DEF where
toShATermAux att0 xv = case xv of
Def a b c -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
return $ addATerm (ShAAppl "Def" [a', b', c'] []) att3
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Def" [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, Def a' b' c') }}}
u -> fromShATermError "DEF" u
instance ShATermConvertible Sign where
toShATermAux att0 xv = case xv of
Sign a b c -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
return $ addATerm (ShAAppl "Sign" [a', b', c'] []) att3
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Sign" [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, Sign a' b' c') }}}
u -> fromShATermError "Sign" u