{- |
Module      :  ./ATC/Sml_cats.hs
Description :  conversions to and from old SML aterm format
Copyright   :  (c) Klaus Luettich and Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Grothendieck)

This module exports functions, that can convert an sml-CATS ATerm
   into the Haskell abstract syntax tree. So it contains all the
   necessary instances of ATermConvertible and a heuristic function
   that calculates the new lists of Pos out of Region tuples.

   the templates for the instances are automatically derived by
   DrIFT. But there were made many hand written changes.

   todo:
     - p_flag from pos-TERM is not considered jet!
-}


module ATC.Sml_cats ( ATermConvertibleSML
                    , from_sml_ATermString
                    , read_sml_ATerm
                    ) where

import Control.Monad

import Data.List (isPrefixOf)
import Data.Maybe

import qualified Data.Map as Map
-- better recompilation checking without 'import ATerm.Lib'
import ATerm.AbstractSyntax
import ATerm.ReadWrite

import Common.Id
import Common.AS_Annotation
import Common.LibName
import Common.IO

import Common.IRI (IRI, parseIRICurie, iriPos)

import CASL.AS_Basic_CASL

import CASL.Logic_CASL
import Logic.Grothendieck

import Syntax.AS_Structured
import Syntax.AS_Architecture
import Syntax.AS_Library

-- the following module provides the ability to parse the "unparsed-anno"
import Text.ParserCombinators.Parsec (parse)
import Common.AnnoParser (annotations, parseAnno)
import Common.Lexer (skip)
import Common.Utils (trimRight)

-- | cats creates latin1 files
read_sml_ATerm :: FilePath -> IO LIB_DEFN
read_sml_ATerm :: FilePath -> IO LIB_DEFN
read_sml_ATerm fn :: FilePath
fn = (FilePath -> LIB_DEFN) -> IO FilePath -> IO LIB_DEFN
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FilePath -> LIB_DEFN
forall a. ATermConvertibleSML a => FilePath -> a
from_sml_ATermString (IO FilePath -> IO LIB_DEFN) -> IO FilePath -> IO LIB_DEFN
forall a b. (a -> b) -> a -> b
$ Enc -> FilePath -> IO FilePath
readEncFile Enc
Latin1 FilePath
fn

-- --- Convertible class for sml -----------------------------------------

class ATermConvertibleSML t where
    from_sml_ShATerm :: ATermTable -> t
    from_sml_ShATermList :: ATermTable -> [t]

    -- default function ignores the annotation part
    from_sml_ShATermList = (ATermTable -> t) -> ATermTable -> [t]
forall t. (ATermTable -> t) -> ATermTable -> [t]
from_sml_ATermList ATermTable -> t
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm

from_sml_ATermList :: (ATermTable -> t) -> ATermTable -> [t]
from_sml_ATermList :: (ATermTable -> t) -> ATermTable -> [t]
from_sml_ATermList f :: ATermTable -> t
f at :: ATermTable
at = case ATermTable -> ShATerm
getATerm ATermTable
at of
   ShAList ats :: [Int]
ats _ -> (Int -> t) -> [Int] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map (ATermTable -> t
f (ATermTable -> t) -> (Int -> ATermTable) -> Int -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> ATermTable -> ATermTable)
-> ATermTable -> Int -> ATermTable
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> ATermTable -> ATermTable
getATermByIndex1 ATermTable
at) [Int]
ats
   aterm :: ShATerm
aterm -> FilePath -> ShATerm -> [t]
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "[a]" ShATerm
aterm

from_sml_ATermString :: ATermConvertibleSML a => String -> a
from_sml_ATermString :: FilePath -> a
from_sml_ATermString = ATermTable -> a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> a) -> (FilePath -> ATermTable) -> FilePath -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> ATermTable
readATerm

from_sml_ShATermError :: String -> ShATerm -> a
from_sml_ShATermError :: FilePath -> ShATerm -> a
from_sml_ShATermError t :: FilePath
t u :: ShATerm
u =
    FilePath -> a
forall a. HasCallStack => FilePath -> a
error ("Cannot convert Sml-ShATerm to " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
t FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ": " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
err)
    where err :: FilePath
err = case ShATerm
u of
                  ShAAppl s :: FilePath
s l :: [Int]
l _ -> "!ShAAppl " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "("
                                   FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show ([Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
l) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")"
                  ShAList _ _ -> "!ShAList"
                  _ -> "!ShAInt"

-- basic instances -----------------------------------------------
instance ATermConvertibleSML Bool where
    from_sml_ShATerm :: ATermTable -> Bool
from_sml_ShATerm att :: ATermTable
att = case ShATerm
at of
                       ShAAppl "true" [] _ -> Bool
True
                       ShAAppl "false" [] _ -> Bool
False
                       _ -> FilePath -> ShATerm -> Bool
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Bool" ShATerm
at
                      where at :: ShATerm
at = ATermTable -> ShATerm
getATerm ATermTable
att
-- for Integer derive : ATermConvertibleSML hand written!

instance ATermConvertibleSML Integer where
    from_sml_ShATerm :: ATermTable -> Integer
from_sml_ShATerm att :: ATermTable
att = case ATermTable -> ShATerm
getATerm ATermTable
att of
                           ShAInt x :: Integer
x _ -> Integer
x
                           at :: ShATerm
at -> FilePath -> ShATerm -> Integer
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Integer" ShATerm
at

instance ATermConvertibleSML Int where
    from_sml_ShATerm :: ATermTable -> Int
from_sml_ShATerm att :: ATermTable
att = Integer -> Int
integer2Int (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ ATermTable -> Integer
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm ATermTable
att

instance ATermConvertibleSML Char where
   from_sml_ShATerm :: ATermTable -> Char
from_sml_ShATerm att :: ATermTable
att = case ShATerm
at of
                      (ShAAppl s :: FilePath
s [] _) -> FilePath -> Char
str2Char FilePath
s
                      _ -> FilePath -> ShATerm -> Char
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Char" ShATerm
at
                      where at :: ShATerm
at = ATermTable -> ShATerm
getATerm ATermTable
att
   from_sml_ShATermList :: ATermTable -> FilePath
from_sml_ShATermList att :: ATermTable
att = case ShATerm
at of
                         (ShAAppl s :: FilePath
s [] _) -> FilePath -> FilePath
forall a. Read a => FilePath -> a
read FilePath
s
                         _ -> FilePath -> ShATerm -> FilePath
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "String" ShATerm
at
                       where at :: ShATerm
at = ATermTable -> ShATerm
getATerm ATermTable
att

instance (Ord a, ATermConvertibleSML a, ATermConvertibleSML b)
    => ATermConvertibleSML (Map.Map a b) where
    from_sml_ShATerm :: ATermTable -> Map a b
from_sml_ShATerm att :: ATermTable
att = [(a, b)] -> Map a b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(a, b)] -> Map a b) -> [(a, b)] -> Map a b
forall a b. (a -> b) -> a -> b
$ ATermTable -> [(a, b)]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm ATermTable
att

instance ATermConvertibleSML a => ATermConvertibleSML [a] where
    from_sml_ShATerm :: ATermTable -> [a]
from_sml_ShATerm = ATermTable -> [a]
forall a. ATermConvertibleSML a => ATermTable -> [a]
from_sml_ShATermList

instance (ATermConvertibleSML a, ATermConvertibleSML b)
    => ATermConvertibleSML (a, b) where
    from_sml_ShATerm :: ATermTable -> (a, b)
from_sml_ShATerm att :: ATermTable
att = case ShATerm
at of
                       (ShAAppl "" [x :: Int
x, y :: Int
y] _) -> (a
x', b
y')
                        where x' :: a
x' = ATermTable -> a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
x ATermTable
att)
                              y' :: b
y' = ATermTable -> b
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
y ATermTable
att)
                       _ -> FilePath -> ShATerm -> (a, b)
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "(a,b)" ShATerm
at
                      where at :: ShATerm
at = ATermTable -> ShATerm
getATerm ATermTable
att

instance (ATermConvertibleSML a, ATermConvertibleSML b, ATermConvertibleSML c)
    => ATermConvertibleSML (a, b, c) where
    from_sml_ShATerm :: ATermTable -> (a, b, c)
from_sml_ShATerm att :: ATermTable
att = case ShATerm
at of
                       (ShAAppl "" [a :: Int
a, b :: Int
b, c :: Int
c] _) -> (a
a', b
b', c
c')
                         where a' :: a
a' = ATermTable -> a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
a ATermTable
att)
                               b' :: b
b' = ATermTable -> b
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
b ATermTable
att)
                               c' :: c
c' = ATermTable -> c
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
c ATermTable
att)

                       _ -> FilePath -> ShATerm -> (a, b, c)
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "(a,b,c)" ShATerm
at
                      where at :: ShATerm
at = ATermTable -> ShATerm
getATerm ATermTable
att

instance (ATermConvertibleSML a, ATermConvertibleSML b,
          ATermConvertibleSML c, ATermConvertibleSML d)
    => ATermConvertibleSML (a, b, c, d) where
    from_sml_ShATerm :: ATermTable -> (a, b, c, d)
from_sml_ShATerm att :: ATermTable
att = case ShATerm
at of
                       (ShAAppl "" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _) -> (a
a', b
b', c
c', d
d')
                         where a' :: a
a' = ATermTable -> a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
a ATermTable
att)
                               b' :: b
b' = ATermTable -> b
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
b ATermTable
att)
                               c' :: c
c' = ATermTable -> c
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
c ATermTable
att)
                               d' :: d
d' = ATermTable -> d
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
d ATermTable
att)
                       _ -> FilePath -> ShATerm -> (a, b, c, d)
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "(a,b,c)" ShATerm
at
                      where at :: ShATerm
at = ATermTable -> ShATerm
getATerm ATermTable
att

-- --- instances of Id.hs ------------------------------------------------
instance ATermConvertibleSML Token where
    from_sml_ShATerm :: ATermTable -> Token
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "token" [ aa :: Int
aa ] _) ->
                FilePath -> Token
mkSimpleId (FilePath -> Token) -> FilePath -> Token
forall a b. (a -> b) -> a -> b
$ ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
            (ShAAppl "place" [] _) -> FilePath -> Token
mkSimpleId FilePath
Common.Id.place
            _ -> FilePath -> ShATerm -> Token
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Token" ShATerm
aterm
            where aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att

instance ATermConvertibleSML Id where
    from_sml_ShATerm :: ATermTable -> Id
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "compound-id" [ aa :: Int
aa, ab :: Int
ab ] _) -> -- TOKEN_OR_MIXFIX,[ID]
                let
                aa' :: [Token]
aa' = ATermTable -> [Token]
from_sml_ATermTokenTup (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [Id]
ab' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
nullRange
                in [Token] -> [Id] -> Range -> Id
Id [Token]
aa' [Id]
ab' Range
ac'
            (ShAAppl "simple-id" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Token]
aa' = ATermTable -> [Token]
from_sml_ATermTokenTup (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [a]
ab' = []
                ac' :: Range
ac' = Range
nullRange
                in [Token] -> [Id] -> Range -> Id
Id [Token]
aa' [Id]
forall a. [a]
ab' Range
ac'
            _ -> FilePath -> ShATerm -> Id
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Id" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att

from_sml_ATermTokenTup :: ATermTable -> [Token]
from_sml_ATermTokenTup :: ATermTable -> [Token]
from_sml_ATermTokenTup att :: ATermTable
att =
    case ShATerm
aterm of
       (ShAAppl "" [tops :: Int
tops, _, _] _) ->
           ATermTable -> [Token]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
tops ATermTable
att)
       _ -> FilePath -> ShATerm -> [Token]
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Token" ShATerm
aterm
    where aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att

-- --- instances of AS_Annotation.hs -------------------------------------
instance ATermConvertibleSML Annotation where
    from_sml_ShATerm :: ATermTable -> Annotation
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "comment-line" [ aa :: Int
aa ] _) ->
                let
                aa' :: FilePath
aa' = FilePath -> FilePath
trimRight (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in Annote_word -> Annote_text -> Range -> Annotation
Unparsed_anno Annote_word
Comment_start (FilePath -> Annote_text
Line_anno FilePath
aa') Range
ab'
            (ShAAppl "comment" [ aa :: Int
aa ] _) ->
                let
                aa' :: [FilePath]
aa' = FilePath -> [FilePath]
lines (ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att))
                ab' :: Range
ab' = Range
pos_l
                in Annote_word -> Annote_text -> Range -> Annotation
Unparsed_anno Annote_word
Comment_start ([FilePath] -> Annote_text
Group_anno [FilePath]
aa') Range
ab'
            (ShAAppl "unparsed-anno" [ aa :: Int
aa ] _) ->
                Range -> FilePath -> Annotation
parse_anno Range
pos_l
                   (ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att))
            (ShAAppl "annote-line" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: FilePath
aa' = ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: FilePath
ab' = ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in Annote_word -> Annote_text -> Range -> Annotation
Unparsed_anno (FilePath -> Annote_word
Annote_word FilePath
aa') (FilePath -> Annote_text
Line_anno FilePath
ab') Range
ac'
            (ShAAppl "annote-group" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: FilePath
aa' = ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [FilePath]
ab' = ATermTable -> [FilePath]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in Annote_word -> Annote_text -> Range -> Annotation
Unparsed_anno (FilePath -> Annote_word
Annote_word FilePath
aa') ([FilePath] -> Annote_text
Group_anno [FilePath]
ab') Range
ac'
            (ShAAppl "display-anno" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Annotation
ab' = Id -> Range -> FilePath -> Annotation
parse_disp_anno Id
aa' Range
pos_l
                      (FilePath -> FilePath
trimRight (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att))
                in Annotation
ab'
            (ShAAppl "string-anno" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in Id -> Id -> Range -> Annotation
String_anno Id
aa' Id
ab' Range
ac'
            (ShAAppl "list-anno" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Id
ac' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ad' :: Range
ad' = Range
pos_l
                in Id -> Id -> Id -> Range -> Annotation
List_anno Id
aa' Id
ab' Id
ac' Range
ad'
            (ShAAppl "number-anno" [ aa :: Int
aa ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in Id -> Range -> Annotation
Number_anno Id
aa' Range
ab'
            (ShAAppl "floating-anno" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in Id -> Id -> Range -> Annotation
Float_anno Id
aa' Id
ab' Range
ac'
            (ShAAppl "prec-anno" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac ] _) ->
                let
                aa' :: Bool
aa' = ATermTable -> Bool
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [Id]
ab' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: [Id]
ac' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ad' :: Range
ad' = Range
pos_l
                in PrecRel -> [Id] -> [Id] -> Range -> Annotation
Prec_anno (if Bool
aa' then PrecRel
Lower else PrecRel
BothDirections)
                    [Id]
ab' [Id]
ac' Range
ad'
            (ShAAppl "lassoc-anno" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in AssocEither -> [Id] -> Range -> Annotation
Assoc_anno AssocEither
ALeft [Id]
aa' Range
ab'
            (ShAAppl "rassoc-anno" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in AssocEither -> [Id] -> Range -> Annotation
Assoc_anno AssocEither
ARight [Id]
aa' Range
ab'
            (ShAAppl "label-anno" [ aa :: Int
aa ] _) ->
                let
                aa' :: [FilePath]
aa' = FilePath -> [FilePath]
lines (FilePath -> [FilePath]) -> FilePath -> [FilePath]
forall a b. (a -> b) -> a -> b
$ Id -> FilePath -> FilePath
showId
                      (ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> Id) -> ATermTable -> Id
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att) ""
                ab' :: Range
ab' = Range
pos_l
                in [FilePath] -> Range -> Annotation
Label [FilePath]
aa' Range
ab'
            (ShAAppl "implies" [] _) ->
                let
                aa' :: Range
aa' = Range
pos_l
                in Semantic_anno -> Range -> Annotation
Semantic_anno Semantic_anno
SA_implies Range
aa'
            (ShAAppl "definitional" [] _) ->
                let
                aa' :: Range
aa' = Range
pos_l
                in Semantic_anno -> Range -> Annotation
Semantic_anno Semantic_anno
SA_def Range
aa'
            (ShAAppl "conservative" [] _) ->
                let
                aa' :: Range
aa' = Range
pos_l
                in Semantic_anno -> Range -> Annotation
Semantic_anno Semantic_anno
SA_cons Range
aa'
            (ShAAppl "mono" [] _) ->
                Semantic_anno -> Range -> Annotation
Semantic_anno Semantic_anno
SA_mono Range
pos_l
            _ -> FilePath -> ShATerm -> Annotation
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Annotation" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-ANNO" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

{- - Well the following instance has to tie together things, that don't
- belong to each other. Because I can't declare instances for
- certain "Annoted types" -}
instance (ATermConvertibleSML a) => ATermConvertibleSML (Annoted a) where
    from_sml_ShATerm :: ATermTable -> Annoted a
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
         ShAAppl con :: FilePath
con as :: [Int]
as _ -> case FilePath
con of
               -- Basic Items (including sig_items)
                "pos-BASIC-ITEMS" ->
                      case ATermTable -> (a, [Annotation])
forall a. ATermConvertibleSML a => ATermTable -> (a, [Annotation])
from_sml_ATermAnnotedBasic_Items ATermTable
att of
                               (bi :: a
bi, las :: [Annotation]
las) -> a -> Range -> [Annotation] -> [Annotation] -> Annoted a
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted a
bi Range
nullRange [Annotation]
las []
               -- L_.* constuctors from SML
                "" -> a -> Range -> [Annotation] -> [Annotation] -> Annoted a
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted (ATermTable -> a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1
                                                        ([Int] -> Int
forall a. [a] -> a
head [Int]
as)
                                                        ATermTable
att))
                                             Range
nullRange
                                             []
                                             (Int -> ATermTable -> [Annotation]
toAnnoList ([Int] -> Int
forall a. [a] -> a
last [Int]
as) ATermTable
att)
                _ -> -- "No appropiate constructor for Annoted found"
                        a -> Annoted a
forall a. a -> Annoted a
emptyAnno (ATermTable -> a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm ATermTable
att)
         _ -> FilePath -> ShATerm -> Annoted a
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Annoted a" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att

{- -- functions to convert annoted stuff ---------------------------------
all these functions are called by instance ATermConvertibleSML Annoted a -}

from_sml_ATermAnnotedBasic_Items :: ATermConvertibleSML a =>
                               ATermTable -> (a, [Annotation])
from_sml_ATermAnnotedBasic_Items :: ATermTable -> (a, [Annotation])
from_sml_ATermAnnotedBasic_Items att :: ATermTable
att =
    if Bool
isSig_items then
       (ATermTable -> a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm ATermTable
att, [])
    else (ATermTable -> a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm ATermTable
att, [Annotation]
annoList)
    where isSig_items :: Bool
isSig_items =
              case ShATerm
aterm of
              ShAAppl _ as :: [Int]
as _ -> -- pos-BASIC-ITEMS
                    case ATermTable -> ShATerm
getATerm (ATermTable -> ShATerm) -> ATermTable -> ShATerm
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 ([Int] -> Int
forall a. [a] -> a
last [Int]
as) ATermTable
att of
                    (ShAAppl "sig-items" _ _) -> Bool
True
                    _ -> Bool
False
              _ -> FilePath -> ShATerm -> Bool
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "{SIG,BASIC}_items" ShATerm
aterm
          aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att
          annoList :: [Annotation]
annoList = case ATermTable -> ShATerm
getATerm ATermTable
att of
                     (ShAAppl _ as :: [Int]
as _) -> Int -> ATermTable -> [Annotation]
getAnnoList ([Int] -> Int
forall a. [a] -> a
last [Int]
as) ATermTable
att
                     _ -> FilePath -> [Annotation]
forall a. HasCallStack => FilePath -> a
error "Wrong ATerm structure: BASIC_ITEMS"

{- getAnnoList and toAnnoList are only working with an AIndex as first
argument is given. If getAnnoList is called every ShAAppl that starts _
with "pos-" is crossed without consideration. toAnnoList just calls
the [Annotation] conversion directly. -}

getAnnoList :: Int -> ATermTable -> [Annotation]
getAnnoList :: Int -> ATermTable -> [Annotation]
getAnnoList ai :: Int
ai att :: ATermTable
att = case ShATerm
at of
                     ShAAppl c :: FilePath
c as :: [Int]
as _ | FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "pos-" FilePath
c ->
                                    Int -> ATermTable -> [Annotation]
getAnnoList ([Int] -> Int
forall a. [a] -> a
last [Int]
as) ATermTable
att
                     ShAAppl _ as :: [Int]
as _ -> Int -> ATermTable -> [Annotation]
toAnnoList ([Int] -> Int
forall a. [a] -> a
last [Int]
as) ATermTable
att
                     _ -> FilePath -> [Annotation]
forall a. HasCallStack => FilePath -> a
error "wrong storage or missed 'pos-' contructor"
    where at :: ShATerm
at = ATermTable -> ShATerm
getATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ai ATermTable
att)

toAnnoList :: Int -> ATermTable -> [Annotation]
toAnnoList :: Int -> ATermTable -> [Annotation]
toAnnoList ai :: Int
ai att :: ATermTable
att = ATermTable -> [Annotation]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> [Annotation]) -> ATermTable -> [Annotation]
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ai ATermTable
att

parse_anno :: Range -> String -> Annotation
parse_anno :: Range -> FilePath -> Annotation
parse_anno _pos_l :: Range
_pos_l inp :: FilePath
inp =
    case Parsec FilePath () [Annotation]
-> FilePath -> FilePath -> Either ParseError [Annotation]
forall s t a.
Stream s Identity t =>
Parsec s () a -> FilePath -> s -> Either ParseError a
parse (CharParser () ()
forall st. CharParser st ()
skip CharParser () ()
-> Parsec FilePath () [Annotation]
-> Parsec FilePath () [Annotation]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parsec FilePath () [Annotation]
forall st. GenParser Char st [Annotation]
annotations) "" FilePath
inp of
       Right [x :: Annotation
x] -> Annotation
x
       _ -> FilePath -> Annotation
forall a. HasCallStack => FilePath -> a
error ("something strange happend to \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                             FilePath
inp FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\" during ATerm Conversion")

parse_disp_anno :: Id -> Range -> String -> Annotation
parse_disp_anno :: Id -> Range -> FilePath -> Annotation
parse_disp_anno i :: Id
i pos_l :: Range
pos_l inp :: FilePath
inp =
    case Annotation -> Pos -> Either ParseError Annotation
parseAnno (Annote_word -> Annote_text -> Range -> Annotation
Unparsed_anno (FilePath -> Annote_word
Annote_word "display")
                                         ([FilePath] -> Annote_text
Group_anno [FilePath
inp']) Range
pos_l) Pos
pos of
       Left err :: ParseError
err -> FilePath -> Annotation
forall a. HasCallStack => FilePath -> a
error (FilePath -> Annotation) -> FilePath -> Annotation
forall a b. (a -> b) -> a -> b
$ "internal parse error at " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
err
       Right x :: Annotation
x -> Annotation
x
    where
          pos :: Pos
pos = case Range -> [Pos]
rangeToList Range
pos_l of
                  [] -> FilePath -> Int -> Int -> Pos
newPos "" 0 0
                  h :: Pos
h : _ -> Pos
h
          inp' :: FilePath
inp' = Id -> FilePath -> FilePath
showId Id
i (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ ' ' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
s_inp
          s_inp :: FilePath
s_inp = case FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
inp of
                  rin :: FilePath
rin | "%)" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
rin -> FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
drop 2 FilePath
rin
                      | Bool
otherwise -> FilePath
inp

-- --- instances of AS_Basic_CASL.hs -------------------------------------
instance ATermConvertibleSML (BASIC_SPEC a b c) where
    from_sml_ShATerm :: ATermTable -> BASIC_SPEC a b c
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "basic-spec" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Annoted (BASIC_ITEMS a b c)]
aa' = ATermTable -> [Annoted (BASIC_ITEMS a b c)]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in [Annoted (BASIC_ITEMS a b c)] -> BASIC_SPEC a b c
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
CASL.AS_Basic_CASL.Basic_spec [Annoted (BASIC_ITEMS a b c)]
aa'
            _ -> FilePath -> ShATerm -> BASIC_SPEC a b c
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "BASIC_SPEC" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-BASIC-SPEC" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML (BASIC_ITEMS a b c) where
    from_sml_ShATerm :: ATermTable -> BASIC_ITEMS a b c
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "sig-items" [ aa :: Int
aa ] _) ->
                let
                aa' :: SIG_ITEMS b c
aa' = ATermTable -> SIG_ITEMS b c
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in SIG_ITEMS b c -> BASIC_ITEMS a b c
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items SIG_ITEMS b c
aa'
            (ShAAppl "free-datatype" [ aa :: Int
aa, _ ] _) ->
                let
                aa' :: [Annoted DATATYPE_DECL]
aa' = ATermTable -> [Annoted DATATYPE_DECL]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in SortsKind -> [Annoted DATATYPE_DECL] -> Range -> BASIC_ITEMS a b c
forall b s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> BASIC_ITEMS b s f
Free_datatype SortsKind
NonEmptySorts [Annoted DATATYPE_DECL]
aa' Range
ab'
            (ShAAppl "sort-gen" [ aa :: Int
aa, _ ] _) ->
                let
                aa' :: [Annoted (SIG_ITEMS b c)]
aa' = ATermTable -> [Annoted (SIG_ITEMS b c)]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in [Annoted (SIG_ITEMS b c)] -> Range -> BASIC_ITEMS a b c
forall b s f.
[Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
Sort_gen [Annoted (SIG_ITEMS b c)]
aa' Range
ab'
            (ShAAppl "var-items" [ aa :: Int
aa, _ ] _) ->
                let
                aa' :: [VAR_DECL]
aa' = ATermTable -> [VAR_DECL]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in [VAR_DECL] -> Range -> BASIC_ITEMS a b c
forall b s f. [VAR_DECL] -> Range -> BASIC_ITEMS b s f
Var_items [VAR_DECL]
aa' Range
ab'
            (ShAAppl "local-var-axioms" [ aa :: Int
aa, ab :: Int
ab, _ ] _) ->
                let
                aa' :: [VAR_DECL]
aa' = ATermTable -> [VAR_DECL]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [Annoted (FORMULA c)]
ab' = ATermTable -> [Annoted (FORMULA c)]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in [VAR_DECL] -> [Annoted (FORMULA c)] -> Range -> BASIC_ITEMS a b c
forall b s f.
[VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Local_var_axioms [VAR_DECL]
aa' [Annoted (FORMULA c)]
ab' Range
ac'
            (ShAAppl "axiom-items" [ aa :: Int
aa, _ ] _) ->
                let
                aa' :: [Annoted (FORMULA c)]
aa' = ATermTable -> [Annoted (FORMULA c)]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in [Annoted (FORMULA c)] -> Range -> BASIC_ITEMS a b c
forall b s f. [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Axiom_items [Annoted (FORMULA c)]
aa' Range
ab'
            _ -> FilePath -> ShATerm -> BASIC_ITEMS a b c
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "BASIC_ITEMS" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-BASIC-ITEMS" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML (SIG_ITEMS a b) where
    from_sml_ShATerm :: ATermTable -> SIG_ITEMS a b
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "sort-items" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                hd :: Annoted (SORT_ITEM b)
hd : tl :: [Annoted (SORT_ITEM b)]
tl = ATermTable -> [Annoted (SORT_ITEM b)]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                as :: [Annotation]
as = ATermTable -> [Annotation]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                aa'' :: [Annoted (SORT_ITEM b)]
aa'' = [Annotation] -> Annoted (SORT_ITEM b) -> Annoted (SORT_ITEM b)
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList [Annotation]
as Annoted (SORT_ITEM b)
hd Annoted (SORT_ITEM b)
-> [Annoted (SORT_ITEM b)] -> [Annoted (SORT_ITEM b)]
forall a. a -> [a] -> [a]
: [Annoted (SORT_ITEM b)]
tl
                ab' :: Range
ab' = Range
pos_l
                in SortsKind -> [Annoted (SORT_ITEM b)] -> Range -> SIG_ITEMS a b
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
NonEmptySorts [Annoted (SORT_ITEM b)]
aa'' Range
ab'
            (ShAAppl "op-items" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                hd :: Annoted (OP_ITEM b)
hd : tl :: [Annoted (OP_ITEM b)]
tl = ATermTable -> [Annoted (OP_ITEM b)]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                as :: [Annotation]
as = ATermTable -> [Annotation]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                aa'' :: [Annoted (OP_ITEM b)]
aa'' = [Annotation] -> Annoted (OP_ITEM b) -> Annoted (OP_ITEM b)
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList [Annotation]
as Annoted (OP_ITEM b)
hd Annoted (OP_ITEM b)
-> [Annoted (OP_ITEM b)] -> [Annoted (OP_ITEM b)]
forall a. a -> [a] -> [a]
: [Annoted (OP_ITEM b)]
tl
                ab' :: Range
ab' = Range
pos_l
                in [Annoted (OP_ITEM b)] -> Range -> SIG_ITEMS a b
forall s f. [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
Op_items [Annoted (OP_ITEM b)]
aa'' Range
ab'
            (ShAAppl "pred-items" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                hd :: Annoted (PRED_ITEM b)
hd : tl :: [Annoted (PRED_ITEM b)]
tl = ATermTable -> [Annoted (PRED_ITEM b)]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                as :: [Annotation]
as = ATermTable -> [Annotation]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                aa'' :: [Annoted (PRED_ITEM b)]
aa'' = [Annotation] -> Annoted (PRED_ITEM b) -> Annoted (PRED_ITEM b)
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList [Annotation]
as Annoted (PRED_ITEM b)
hd Annoted (PRED_ITEM b)
-> [Annoted (PRED_ITEM b)] -> [Annoted (PRED_ITEM b)]
forall a. a -> [a] -> [a]
: [Annoted (PRED_ITEM b)]
tl
                ab' :: Range
ab' = Range
pos_l
                in [Annoted (PRED_ITEM b)] -> Range -> SIG_ITEMS a b
forall s f. [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
Pred_items [Annoted (PRED_ITEM b)]
aa'' Range
ab'
            (ShAAppl "datatype-items" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                hd :: Annoted DATATYPE_DECL
hd : tl :: [Annoted DATATYPE_DECL]
tl = ATermTable -> [Annoted DATATYPE_DECL]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                as :: [Annotation]
as = ATermTable -> [Annotation]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                aa'' :: [Annoted DATATYPE_DECL]
aa'' = [Annotation] -> Annoted DATATYPE_DECL -> Annoted DATATYPE_DECL
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList [Annotation]
as Annoted DATATYPE_DECL
hd Annoted DATATYPE_DECL
-> [Annoted DATATYPE_DECL] -> [Annoted DATATYPE_DECL]
forall a. a -> [a] -> [a]
: [Annoted DATATYPE_DECL]
tl
                ab' :: Range
ab' = Range
pos_l
                in SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS a b
forall s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
Datatype_items SortsKind
NonEmptySorts [Annoted DATATYPE_DECL]
aa'' Range
ab'
            _ -> FilePath -> ShATerm -> SIG_ITEMS a b
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SIG_ITEMS" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SIG-ITEMS" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML (SORT_ITEM a) where
    from_sml_ShATerm :: ATermTable -> SORT_ITEM a
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "sort-decl" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in [Id] -> Range -> SORT_ITEM a
forall f. [Id] -> Range -> SORT_ITEM f
Sort_decl [Id]
aa' Range
ab'
            (ShAAppl "subsort-decl" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in [Id] -> Id -> Range -> SORT_ITEM a
forall f. [Id] -> Id -> Range -> SORT_ITEM f
Subsort_decl [Id]
aa' Id
ab' Range
ac'
            (ShAAppl "subsort-defn" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac, ad :: Int
ad, ae :: Int
ae ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Token
ab' = ATermTable -> Token
from_sml_ATermSIMPLE_ID (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Id
ac' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ad' :: Annoted (FORMULA a)
ad' = ATermTable -> Annoted (FORMULA a)
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ad ATermTable
att)
                as :: [Annotation]
as = Int -> ATermTable -> [Annotation]
toAnnoList Int
ae ATermTable
att
                ad'' :: Annoted (FORMULA a)
ad'' = [Annotation] -> Annoted (FORMULA a) -> Annoted (FORMULA a)
forall a. [Annotation] -> Annoted a -> Annoted a
addRAnnoList [Annotation]
as Annoted (FORMULA a)
ad'
                ae' :: Range
ae' = Range
pos_l
                in Id -> Token -> Id -> Annoted (FORMULA a) -> Range -> SORT_ITEM a
forall f.
Id -> Token -> Id -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
Subsort_defn Id
aa' Token
ab' Id
ac' Annoted (FORMULA a)
ad'' Range
ae'
            (ShAAppl "iso-decl" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in [Id] -> Range -> SORT_ITEM a
forall f. [Id] -> Range -> SORT_ITEM f
Iso_decl [Id]
aa' Range
ab'
            _ -> FilePath -> ShATerm -> SORT_ITEM a
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SORT_ITEM" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SORT-ITEM" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML (OP_ITEM a) where
    from_sml_ShATerm :: ATermTable -> OP_ITEM a
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "op-decl" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: OP_TYPE
ab' = ATermTable -> OP_TYPE
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: [OP_ATTR a]
ac' = ATermTable -> [OP_ATTR a]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ad' :: Range
ad' = Range
pos_l
                in [Id] -> OP_TYPE -> [OP_ATTR a] -> Range -> OP_ITEM a
forall f. [Id] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
Op_decl [Id]
aa' OP_TYPE
ab' [OP_ATTR a]
ac' Range
ad'
            (ShAAppl "op-defn" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac, ad :: Int
ad ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: OP_HEAD
ab' = ATermTable -> OP_HEAD
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Annoted (TERM a)
ac' = ATermTable -> Annoted (TERM a)
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                as :: [Annotation]
as = ATermTable -> [Annotation]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ad ATermTable
att)
                ac'' :: Annoted (TERM a)
ac'' = [Annotation] -> Annoted (TERM a) -> Annoted (TERM a)
forall a. [Annotation] -> Annoted a -> Annoted a
addRAnnoList [Annotation]
as Annoted (TERM a)
ac'
                ad' :: Range
ad' = Range
pos_l
                in Id -> OP_HEAD -> Annoted (TERM a) -> Range -> OP_ITEM a
forall f. Id -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
Op_defn Id
aa' OP_HEAD
ab' Annoted (TERM a)
ac'' Range
ad'
            _ -> FilePath -> ShATerm -> OP_ITEM a
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "OP_ITEM" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-OP-ITEM" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML OP_TYPE where
    from_sml_ShATerm :: ATermTable -> OP_TYPE
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "total-op-type" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                (aa' :: [Id]
aa', ps :: Range
ps) = ATermTable -> ([Id], Range)
from_sml_ATermSORTS (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range -> Range -> Range
insertPos Range
ps Range
pos_l
                in OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total [Id]
aa' Id
ab' Range
ac'
            (ShAAppl "partial-op-type" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                (aa' :: [Id]
aa', ps :: Range
ps) = ATermTable -> ([Id], Range)
from_sml_ATermSORTS (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range -> Range -> Range
insertPos Range
ps Range
pos_l
                in OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
aa' Id
ab' Range
ac'
            _ -> FilePath -> ShATerm -> OP_TYPE
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "OP_TYPE" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-OP-TYPE" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

-- -- a helper for the SML-datatype SORTS -------------------------------
from_sml_ATermSORTS :: ATermTable -> ([SORT], Range)
from_sml_ATermSORTS :: ATermTable -> ([Id], Range)
from_sml_ATermSORTS att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "sorts" [ aa :: Int
aa ] _) ->
                (ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att), Range
pos_l)
            _ -> FilePath -> ShATerm -> ([Id], Range)
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "([SORT],Range)" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SORTS" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML OP_HEAD where
    from_sml_ShATerm :: ATermTable -> OP_HEAD
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "total-op-head" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [VAR_DECL]
aa' = (ATermTable -> VAR_DECL) -> ATermTable -> [VAR_DECL]
forall t. (ATermTable -> t) -> ATermTable -> [t]
from_sml_ATermList ATermTable -> VAR_DECL
from_sml_ATermARG_DECL
                       (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in OpKind -> [VAR_DECL] -> Maybe Id -> Range -> OP_HEAD
Op_head OpKind
Total [VAR_DECL]
aa' (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
ab') Range
ac'
            (ShAAppl "partial-op-head" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [VAR_DECL]
aa' = (ATermTable -> VAR_DECL) -> ATermTable -> [VAR_DECL]
forall t. (ATermTable -> t) -> ATermTable -> [t]
from_sml_ATermList ATermTable -> VAR_DECL
from_sml_ATermARG_DECL
                       (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in OpKind -> [VAR_DECL] -> Maybe Id -> Range -> OP_HEAD
Op_head OpKind
Partial [VAR_DECL]
aa' (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
ab') Range
ac'
            _ -> FilePath -> ShATerm -> OP_HEAD
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "OP_HEAD" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-OP-HEAD" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

from_sml_ATermARG_DECL :: ATermTable -> VAR_DECL
from_sml_ATermARG_DECL :: ATermTable -> VAR_DECL
from_sml_ATermARG_DECL att :: ATermTable
att =
        case ShATerm
aterm of
-- (ShAAppl "arg-decl" [ ShAAppl "" [aa,ab] _ ] _)  ->
        (ShAAppl "" [aa :: Int
aa, ab :: Int
ab] _) ->
                let
                aa' :: [Token]
aa' = ATermTable -> [Token]
from_sml_ATermVARs (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in [Token] -> Id -> Range -> VAR_DECL
Var_decl [Token]
aa' Id
ab' Range
ac'
        _ -> FilePath -> ShATerm -> VAR_DECL
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "ARG_DECL" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = case ATermTable -> ShATerm
getATerm ATermTable
att' of
                    ShAAppl "arg-decl" [i :: Int
i] _ ->
                            ATermTable -> ShATerm
getATerm (ATermTable -> ShATerm) -> ATermTable -> ShATerm
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
i ATermTable
att
                    x :: ShATerm
x -> FilePath -> ShATerm -> ShATerm
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "arg-decl" ShATerm
x
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-ARG-DECL" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML (OP_ATTR a) where
    from_sml_ShATerm :: ATermTable -> OP_ATTR a
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "associative" [] _) ->
                let
                in OP_ATTR a
forall f. OP_ATTR f
Assoc_op_attr
            (ShAAppl "commutative" [] _) ->
                let
                in OP_ATTR a
forall f. OP_ATTR f
Comm_op_attr
            (ShAAppl "idempotent" [] _) ->
                let
                in OP_ATTR a
forall f. OP_ATTR f
Idem_op_attr
            (ShAAppl "unit-op-attr" [ aa :: Int
aa ] _) ->
                let
                aa' :: TERM a
aa' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in TERM a -> OP_ATTR a
forall f. TERM f -> OP_ATTR f
Unit_op_attr TERM a
aa'
            _ -> FilePath -> ShATerm -> OP_ATTR a
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "OP_ATTR" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-OP-ATTR" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML (PRED_ITEM a) where
    from_sml_ShATerm :: ATermTable -> PRED_ITEM a
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "pred-decl" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: PRED_TYPE
ab' = ATermTable -> PRED_TYPE
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in [Id] -> PRED_TYPE -> Range -> PRED_ITEM a
forall f. [Id] -> PRED_TYPE -> Range -> PRED_ITEM f
Pred_decl [Id]
aa' PRED_TYPE
ab' Range
ac'
            (ShAAppl "pred-defn" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac, _ ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: PRED_HEAD
ab' = ATermTable -> PRED_HEAD
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Annoted (FORMULA a)
ac' = ATermTable -> Annoted (FORMULA a)
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ad' :: Range
ad' = Range
pos_l
                in Id -> PRED_HEAD -> Annoted (FORMULA a) -> Range -> PRED_ITEM a
forall f.
Id -> PRED_HEAD -> Annoted (FORMULA f) -> Range -> PRED_ITEM f
Pred_defn Id
aa' PRED_HEAD
ab' Annoted (FORMULA a)
ac' Range
ad'
            _ -> FilePath -> ShATerm -> PRED_ITEM a
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "PRED_ITEM" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-PRED-ITEM" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML PRED_TYPE where
    from_sml_ShATerm :: ATermTable -> PRED_TYPE
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "pred-type" [ aa :: Int
aa ] _) ->
                let
                (aa' :: [Id]
aa', ps :: Range
ps) = ATermTable -> ([Id], Range)
from_sml_ATermSORTS (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range -> Range -> Range
insertPos Range
ps Range
pos_l
                in [Id] -> Range -> PRED_TYPE
Pred_type [Id]
aa' Range
ab'
            _ -> FilePath -> ShATerm -> PRED_TYPE
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "PRED_TYPE" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-PRED-TYPE" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML PRED_HEAD where
    from_sml_ShATerm :: ATermTable -> PRED_HEAD
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "pred-head" [ aa :: Int
aa ] _) ->
                let
                aa' :: [VAR_DECL]
aa' = (ATermTable -> VAR_DECL) -> ATermTable -> [VAR_DECL]
forall t. (ATermTable -> t) -> ATermTable -> [t]
from_sml_ATermList ATermTable -> VAR_DECL
from_sml_ATermARG_DECL
                       (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in [VAR_DECL] -> Range -> PRED_HEAD
Pred_head [VAR_DECL]
aa' Range
ab'
            _ -> FilePath -> ShATerm -> PRED_HEAD
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "PRED_HEAD" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-PRED-HEAD" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML DATATYPE_DECL where
    from_sml_ShATerm :: ATermTable -> DATATYPE_DECL
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "datatype-decl" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                abh :: Annoted ALTERNATIVE
abh : abt :: [Annoted ALTERNATIVE]
abt = ATermTable -> [Annoted ALTERNATIVE]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                as :: [Annotation]
as = ATermTable -> [Annotation]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ab'' :: [Annoted ALTERNATIVE]
ab'' = [Annotation] -> Annoted ALTERNATIVE -> Annoted ALTERNATIVE
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList [Annotation]
as Annoted ALTERNATIVE
abh Annoted ALTERNATIVE
-> [Annoted ALTERNATIVE] -> [Annoted ALTERNATIVE]
forall a. a -> [a] -> [a]
: [Annoted ALTERNATIVE]
abt
                ac' :: Range
ac' = Range
pos_l
                in Id -> [Annoted ALTERNATIVE] -> Range -> DATATYPE_DECL
Datatype_decl Id
aa' [Annoted ALTERNATIVE]
ab'' Range
ac'
            _ -> FilePath -> ShATerm -> DATATYPE_DECL
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "DATATYPE_DECL" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-DATATYPE-DECL" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML ALTERNATIVE where
    from_sml_ShATerm :: ATermTable -> ALTERNATIVE
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "total-construct" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [COMPONENTS]
ab' = ATermTable -> [COMPONENTS]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in OpKind -> Id -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
Total Id
aa' [COMPONENTS]
ab' Range
ac'
            (ShAAppl "partial-construct" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [COMPONENTS]
ab' = ATermTable -> [COMPONENTS]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in OpKind -> Id -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
Partial Id
aa' [COMPONENTS]
ab' Range
ac'
            (ShAAppl "subsort" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in [Id] -> Range -> ALTERNATIVE
Subsorts [Id]
aa' Range
ab'
            _ -> FilePath -> ShATerm -> ALTERNATIVE
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "ALTERNATIVE" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-ALTERNATIVE" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML COMPONENTS where
    from_sml_ShATerm :: ATermTable -> COMPONENTS
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "total-select" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in OpKind -> [Id] -> Id -> Range -> COMPONENTS
Cons_select OpKind
Total [Id]
aa' Id
ab' Range
ac'
            (ShAAppl "partial-select" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [Id]
aa' = ATermTable -> [Id]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in OpKind -> [Id] -> Id -> Range -> COMPONENTS
Cons_select OpKind
Partial [Id]
aa' Id
ab' Range
ac'
            (ShAAppl "sort-component" [ aa :: Int
aa ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in Id -> COMPONENTS
Sort Id
aa'
            _ -> FilePath -> ShATerm -> COMPONENTS
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "COMPONENTS" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-COMPONENTS" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML VAR_DECL where
    from_sml_ShATerm :: ATermTable -> VAR_DECL
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [Token]
aa' = ATermTable -> [Token]
from_sml_ATermVARs (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                in [Token] -> Id -> Range -> VAR_DECL
Var_decl [Token]
aa' Id
ab' Range
nullRange
            _ -> FilePath -> ShATerm -> VAR_DECL
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "VAR_DECL" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att

instance ATermConvertibleSML (FORMULA a) where
    from_sml_ShATerm :: ATermTable -> FORMULA a
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "quantification" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac ] _) ->
                let
                aa' :: QUANTIFIER
aa' = ATermTable -> QUANTIFIER
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                pq :: Range
pq = ATermTable -> Range
getPos (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [VAR_DECL]
ab' = ATermTable -> [VAR_DECL]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: FORMULA a
ac' = ATermTable -> FORMULA a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ad' :: Range
ad' = Range -> Range -> Range
insertPos Range
pq Range
pos_l
                in QUANTIFIER -> [VAR_DECL] -> FORMULA a -> Range -> FORMULA a
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
aa' [VAR_DECL]
ab' FORMULA a
ac' Range
ad'
            (ShAAppl "conjunction" [ aa :: Int
aa ] _) ->
                let
                aa' :: [FORMULA a]
aa' = ATermTable -> [FORMULA a]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in Junctor -> [FORMULA a] -> Range -> FORMULA a
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [FORMULA a]
aa' Range
ab'
            (ShAAppl "disjunction" [ aa :: Int
aa ] _) ->
                let
                aa' :: [FORMULA a]
aa' = ATermTable -> [FORMULA a]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in Junctor -> [FORMULA a] -> Range -> FORMULA a
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis [FORMULA a]
aa' Range
ab'
            (ShAAppl "implication" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: FORMULA a
aa' = ATermTable -> FORMULA a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: FORMULA a
ab' = ATermTable -> FORMULA a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in FORMULA a -> Relation -> FORMULA a -> Range -> FORMULA a
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA a
aa' Relation
Implication FORMULA a
ab' Range
ac'
            (ShAAppl "equivalence" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: FORMULA a
aa' = ATermTable -> FORMULA a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: FORMULA a
ab' = ATermTable -> FORMULA a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in FORMULA a -> Relation -> FORMULA a -> Range -> FORMULA a
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA a
aa' Relation
Equivalence FORMULA a
ab' Range
ac'
            (ShAAppl "negation" [ aa :: Int
aa ] _) ->
                let
                aa' :: FORMULA a
aa' = ATermTable -> FORMULA a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in FORMULA a -> Range -> FORMULA a
forall f. FORMULA f -> Range -> FORMULA f
Negation FORMULA a
aa' Range
ab'
            -- the following things are from SML-type ATOM
            (ShAAppl "atom" [i :: Int
i] _) ->
              case ATermTable -> ShATerm
getATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
i ATermTable
att') of
               (ShAAppl "ttrue" [] _) ->
                 let
                 aa' :: Range
aa' = Range
pos_l
                 in Bool -> Range -> FORMULA a
forall f. Bool -> Range -> FORMULA f
Atom Bool
True Range
aa'
               (ShAAppl "ffalse" [] _) ->
                 let
                 aa' :: Range
aa' = Range
pos_l
                 in Bool -> Range -> FORMULA a
forall f. Bool -> Range -> FORMULA f
Atom Bool
False Range
aa'
               (ShAAppl "predication" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                 let
                 aa' :: PRED_SYMB
aa' = ATermTable -> PRED_SYMB
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                 (ab' :: [TERM a]
ab', ps :: Range
ps) = ATermTable -> ([TERM a], Range)
forall a. ATermTable -> ([TERM a], Range)
from_sml_ATermTERMS (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                 ac' :: Range
ac' = Range -> Range -> Range
insertPos Range
ps Range
pos_l
                 in PRED_SYMB -> [TERM a] -> Range -> FORMULA a
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
aa' [TERM a]
forall a. [TERM a]
ab' Range
ac'
               (ShAAppl "definedness" [ aa :: Int
aa ] _) ->
                 let
                 aa' :: TERM a
aa' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                 ab' :: Range
ab' = Range
pos_l
                 in TERM a -> Range -> FORMULA a
forall f. TERM f -> Range -> FORMULA f
Definedness TERM a
aa' Range
ab'
               (ShAAppl "existl-equation" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                 let
                 aa' :: TERM a
aa' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                 ab' :: TERM a
ab' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                 ac' :: Range
ac' = Range
pos_l
                 in TERM a -> Equality -> TERM a -> Range -> FORMULA a
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM a
aa' Equality
Existl TERM a
ab' Range
ac'
               (ShAAppl "strong-equation" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                 let
                 aa' :: TERM a
aa' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                 ab' :: TERM a
ab' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                 ac' :: Range
ac' = Range
pos_l
                 in TERM a -> Equality -> TERM a -> Range -> FORMULA a
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM a
aa' Equality
Strong TERM a
ab' Range
ac'
               (ShAAppl "membership" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                 let
                 aa' :: TERM a
aa' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                 ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                 ac' :: Range
ac' = Range
pos_l
                 in TERM a -> Id -> Range -> FORMULA a
forall f. TERM f -> Id -> Range -> FORMULA f
Membership TERM a
aa' Id
ab' Range
ac'
               _ -> FilePath -> ShATerm -> FORMULA a
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "FORMULA" ShATerm
aterm
            _ -> FilePath -> ShATerm -> FORMULA a
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "FORMULA" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, _g_flag :: Bool
_g_flag, att' :: ATermTable
att') = FilePath -> ATermTable -> (Range, Bool, ATermTable)
skipPosFlag "pos-FORMULA" ATermTable
att

-- -- a helper for the SML-datatype TERMS -------------------------------
from_sml_ATermTERMS :: ATermTable -> ([TERM a], Range)
from_sml_ATermTERMS :: ATermTable -> ([TERM a], Range)
from_sml_ATermTERMS att :: ATermTable
att =
    case ShATerm
aterm of
             (ShAAppl "terms" [ aa :: Int
aa ] _) ->
                 (ATermTable -> [TERM a]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att), Range
pos_l)
             _ -> FilePath -> ShATerm -> ([TERM a], Range)
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "([TERM],Range)" ShATerm
aterm
    where aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
          (pos_l :: Range
pos_l, att' :: ATermTable
att') =
              case ATermTable -> ShATerm
getATerm ATermTable
att of
              (ShAAppl "pos-TERMS" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                       (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
              _ -> (Range
nullRange, ATermTable
att)

-- -- a helper for SIMPLE_IDs and IRIs ----------------------------------

from_sml_ATermSIMPLE_ID :: ATermTable -> SIMPLE_ID
from_sml_ATermSIMPLE_ID :: ATermTable -> Token
from_sml_ATermSIMPLE_ID att :: ATermTable
att =
    case ShATerm
aterm of
      (ShAAppl "" [ si :: Int
si, _ ] _) -> {- snd element is 'None'
                                  (CASL.grm:((WORDS,None))) -}
          let s :: FilePath
s = ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> FilePath) -> ATermTable -> FilePath
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
si ATermTable
att
          in FilePath -> Token
mkSimpleId FilePath
s
      _ -> FilePath -> ShATerm -> Token
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SIMPLE_ID" ShATerm
aterm
    where aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att

from_sml_ATermIRI :: ATermTable -> IRI
from_sml_ATermIRI :: ATermTable -> IRI
from_sml_ATermIRI att :: ATermTable
att =
    case ShATerm
aterm of
      (ShAAppl "" [ si :: Int
si, _ ] _) -> {- snd element is 'None'
                                  (CASL.grm:((WORDS,None))) -}
          let s :: FilePath
s = ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> FilePath) -> ATermTable -> FilePath
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
si ATermTable
att
          in IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> IRI
forall a. HasCallStack => FilePath -> a
error (FilePath -> IRI) -> FilePath -> IRI
forall a b. (a -> b) -> a -> b
$ "parsing error: not an IRI \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s
                                      FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\" \n(from_sml_ATermIRI)")
             (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe IRI
parseIRICurie FilePath
s
      _ -> FilePath -> ShATerm -> IRI
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "IRI" ShATerm
aterm
    where aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att

-- -- a helper for [VAR] -------------------------------------------------
from_sml_ATermVARs :: ATermTable -> [VAR]
from_sml_ATermVARs :: ATermTable -> [Token]
from_sml_ATermVARs att :: ATermTable
att = (ATermTable -> Token) -> [ATermTable] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map ATermTable -> Token
from_sml_ATermSIMPLE_ID [ATermTable]
att_list
    where att_list :: [ATermTable]
att_list = case ATermTable -> ShATerm
getATerm ATermTable
att of
                     ShAList l :: [Int]
l _ -> (Int -> ATermTable) -> [Int] -> [ATermTable]
forall a b. (a -> b) -> [a] -> [b]
map Int -> ATermTable
getAtt [Int]
l
                     _ -> FilePath -> ShATerm -> [ATermTable]
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "[VAR]" (ShATerm -> [ATermTable]) -> ShATerm -> [ATermTable]
forall a b. (a -> b) -> a -> b
$ ATermTable -> ShATerm
getATerm ATermTable
att
          getAtt :: Int -> ATermTable
getAtt ai :: Int
ai = Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ai ATermTable
att

instance ATermConvertibleSML QUANTIFIER where
    from_sml_ShATerm :: ATermTable -> QUANTIFIER
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "forall" [] _) ->
                let
                in QUANTIFIER
Universal
            (ShAAppl "exists" [] _) ->
                let
                in QUANTIFIER
Existential
            (ShAAppl "exists-uniquely" [] _) ->
                let
                in QUANTIFIER
Unique_existential
            _ -> FilePath -> ShATerm -> QUANTIFIER
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "QUANTIFIER" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-QUANTIFIER" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML PRED_SYMB where
    from_sml_ShATerm :: ATermTable -> PRED_SYMB
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            ShAAppl "pred-symb" [ aa :: Int
aa, ab :: Int
ab ] _ ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in case ATermTable -> ShATerm
getATerm (ATermTable -> ShATerm) -> ATermTable -> ShATerm
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att of
                   ShAAppl "None" [] _ -> Id -> PRED_SYMB
Pred_name Id
aa'
                   ShAAppl "Some" [ aab :: Int
aab ] _ ->
                     let aab' :: PRED_TYPE
aab' = ATermTable -> PRED_TYPE
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aab ATermTable
att)
                         ac' :: Range
ac' = Range
pos_l
                     in Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
aa' PRED_TYPE
aab' Range
ac'
                   _ -> FilePath -> ShATerm -> PRED_SYMB
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Option" ShATerm
aterm
            _ -> FilePath -> ShATerm -> PRED_SYMB
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "PRED_SYMB" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                ShAAppl "pos-PRED-SYMB" [reg_i :: Int
reg_i, item_i :: Int
item_i] _ ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML (TERM a) where
    from_sml_ShATerm :: ATermTable -> TERM a
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "var-or-const" [ aa :: Int
aa ] _) ->
                let
                aa' :: Token
aa' = ATermTable -> Token
from_sml_ATermSIMPLE_ID (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in Token -> TERM a
forall f. Token -> TERM f
varOrConst Token
aa'
            (ShAAppl "qual-var" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Token
aa' = ATermTable -> Token
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in Token -> Id -> Range -> TERM a
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
aa' Id
ab' Range
ac'
            (ShAAppl "application" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: OP_SYMB
aa' = ATermTable -> OP_SYMB
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                (ab' :: [TERM a]
ab', ps :: Range
ps) = ATermTable -> ([TERM a], Range)
forall a. ATermTable -> ([TERM a], Range)
from_sml_ATermTERMS (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range -> Range -> Range
insertPos Range
ps Range
pos_l
                in OP_SYMB -> [TERM a] -> Range -> TERM a
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
aa' [TERM a]
forall a. [TERM a]
ab' Range
ac'
            (ShAAppl "sorted-term" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: TERM a
aa' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in TERM a -> Id -> Range -> TERM a
forall f. TERM f -> Id -> Range -> TERM f
Sorted_term TERM a
aa' Id
ab' Range
ac'
            (ShAAppl "cast" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: TERM a
aa' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Id
ab' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in TERM a -> Id -> Range -> TERM a
forall f. TERM f -> Id -> Range -> TERM f
Cast TERM a
aa' Id
ab' Range
ac'
            (ShAAppl "conditional" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac ] _) ->
                let
                aa' :: TERM a
aa' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: FORMULA a
ab' = ATermTable -> FORMULA a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: TERM a
ac' = ATermTable -> TERM a
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ad' :: Range
ad' = Range
pos_l
                in TERM a -> FORMULA a -> TERM a -> Range -> TERM a
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM a
aa' FORMULA a
ab' TERM a
ac' Range
ad'
            _ -> FilePath -> ShATerm -> TERM a
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "TERM" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, _p_flag :: Bool
_p_flag, att' :: ATermTable
att') = FilePath -> ATermTable -> (Range, Bool, ATermTable)
skipPosFlag "pos-TERM" ATermTable
att

instance ATermConvertibleSML OP_SYMB where
    from_sml_ShATerm :: ATermTable -> OP_SYMB
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            ShAAppl "op-symb" [ aa :: Int
aa, ab :: Int
ab ] _ ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in case ATermTable -> ShATerm
getATerm (ATermTable -> ShATerm) -> ATermTable -> ShATerm
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att of
                   ShAAppl "None" [] _ -> Id -> OP_SYMB
Op_name Id
aa'
                   ShAAppl "Some" [ aab :: Int
aab ] _ ->
                     let aab' :: OP_TYPE
aab' = ATermTable -> OP_TYPE
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aab ATermTable
att)
                         ac' :: Range
ac' = Range
pos_l
                     in Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
aa' OP_TYPE
aab' Range
ac'
                   _ -> FilePath -> ShATerm -> OP_SYMB
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "Option" ShATerm
aterm
            _ -> FilePath -> ShATerm -> OP_SYMB
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "OP_SYMB" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-OP-SYMB" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML SYMB_ITEMS where
    from_sml_ShATerm :: ATermTable -> SYMB_ITEMS
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "symb-items" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: SYMB_KIND
aa' = ATermTable -> SYMB_KIND
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [SYMB]
ab' = ATermTable -> [SYMB]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in SYMB_KIND -> [SYMB] -> Range -> SYMB_ITEMS
Symb_items SYMB_KIND
aa' [SYMB]
ab' Range
ac'
            _ -> FilePath -> ShATerm -> SYMB_ITEMS
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SYMB_ITEMS" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SYMB-ITEMS" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML SYMB_MAP_ITEMS where
    from_sml_ShATerm :: ATermTable -> SYMB_MAP_ITEMS
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "symb-map-items" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: SYMB_KIND
aa' = ATermTable -> SYMB_KIND
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [SYMB_OR_MAP]
ab' = ATermTable -> [SYMB_OR_MAP]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in SYMB_KIND -> [SYMB_OR_MAP] -> Range -> SYMB_MAP_ITEMS
Symb_map_items SYMB_KIND
aa' [SYMB_OR_MAP]
ab' Range
ac'
            _ -> FilePath -> ShATerm -> SYMB_MAP_ITEMS
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SYMB_MAP_ITEMS" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SYMB-MAP-ITEMS" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML SYMB_KIND where
    from_sml_ShATerm :: ATermTable -> SYMB_KIND
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "implicitk" [] _) ->
                SYMB_KIND
Implicit
            (ShAAppl "sortsk" [] _) ->
                SYMB_KIND
Sorts_kind
            (ShAAppl "opsk" [] _) ->
                SYMB_KIND
Ops_kind
            (ShAAppl "predsk" [] _) ->
                SYMB_KIND
Preds_kind
            _ -> FilePath -> ShATerm -> SYMB_KIND
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SYMB_KIND" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SYMB-KIND" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML SYMB where
    from_sml_ShATerm :: ATermTable -> SYMB
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "symb-id" [ aa :: Int
aa ] _) ->
                let
                i :: Id
i = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                aa' :: Id
aa' = Range -> Id -> Id
setFstPos Range
pos_l Id
i
                in Id -> SYMB
Symb_id Id
aa'
            (ShAAppl "qual-id" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Id
aa' = ATermTable -> Id
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: TYPE
ab' = ATermTable -> TYPE
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in Id -> TYPE -> Range -> SYMB
Qual_id Id
aa' TYPE
ab' Range
ac'
            _ -> FilePath -> ShATerm -> SYMB
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SYMB" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SYMB" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML TYPE where
    from_sml_ShATerm :: ATermTable -> TYPE
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "op-symb-type" [ aa :: Int
aa ] _) ->
                let
                aa' :: OP_TYPE
aa' = ATermTable -> OP_TYPE
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in OP_TYPE -> TYPE
O_type OP_TYPE
aa'
            (ShAAppl "pred-symb-type" [ aa :: Int
aa ] _) ->
                let
                aa' :: PRED_TYPE
aa' = ATermTable -> PRED_TYPE
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in PRED_TYPE -> TYPE
P_type PRED_TYPE
aa'
            _ -> FilePath -> ShATerm -> TYPE
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "TYPE" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-TYPE" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML SYMB_OR_MAP where
    from_sml_ShATerm :: ATermTable -> SYMB_OR_MAP
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "symb" [ aa :: Int
aa ] _) ->
                let
                aa' :: SYMB
aa' = ATermTable -> SYMB
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in SYMB -> SYMB_OR_MAP
Symb SYMB
aa'
            (ShAAppl "symb-or-map" [ aa :: Int
aa ] _) ->
                let
                (aa' :: SYMB
aa', ab' :: SYMB
ab') = ATermTable -> (SYMB, SYMB)
from_sml_ATermSYMB_MAP (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in SYMB -> SYMB -> Range -> SYMB_OR_MAP
Symb_map SYMB
aa' SYMB
ab' Range
ac'
            _ -> FilePath -> ShATerm -> SYMB_OR_MAP
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SYMB_OR_MAP" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SYMB-OR-MAP" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

-- -- a helper for SYMB_MAP from SML -------------------------------------

from_sml_ATermSYMB_MAP :: ATermTable -> (SYMB, SYMB)
from_sml_ATermSYMB_MAP :: ATermTable -> (SYMB, SYMB)
from_sml_ATermSYMB_MAP att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "symb-map" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: SYMB
aa' = ATermTable -> SYMB
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: SYMB
ab' = ATermTable -> SYMB
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                in (SYMB
aa', SYMB
ab')
            _ -> FilePath -> ShATerm -> (SYMB, SYMB)
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "(SYMB,SYMB)" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-SYMB-MAP" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

-- --- instances of AS_Structured.hs -------------------------------------
instance ATermConvertibleSML SPEC where
    from_sml_ShATerm :: ATermTable -> SPEC
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "basic" [ aa :: Int
aa ] _) ->
                let
                aa' :: CASLBasicSpec
aa' = ATermTable -> CASLBasicSpec
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att) :: CASLBasicSpec
                aa'' :: G_basic_spec
aa'' = CASL -> CASLBasicSpec -> G_basic_spec
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> basic_spec -> G_basic_spec
G_basic_spec CASL
CASL CASLBasicSpec
aa'
                in SPEC -> Bool -> SPEC
group (G_basic_spec -> Range -> SPEC
Syntax.AS_Structured.Basic_spec G_basic_spec
aa''
                          Range
nullRange) Bool
group_flag
            (ShAAppl "translation" [ aa :: Int
aa, ab :: Int
ab, _ ] _) ->
                let
                aa' :: Annoted SPEC
aa' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: RENAMING
ab' = ATermTable -> RENAMING
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                in SPEC -> Bool -> SPEC
group (Annoted SPEC -> RENAMING -> SPEC
Translation Annoted SPEC
aa' RENAMING
ab') Bool
group_flag
            (ShAAppl "reduction" [ aa :: Int
aa, ab :: Int
ab, _ ] _) ->
                let
                aa' :: Annoted SPEC
aa' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: RESTRICTION
ab' = ATermTable -> RESTRICTION
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                in SPEC -> Bool -> SPEC
group (Annoted SPEC -> RESTRICTION -> SPEC
Reduction Annoted SPEC
aa' RESTRICTION
ab') Bool
group_flag
            (ShAAppl "union-spec" [ aa :: Int
aa ] _) ->
                let
                aa' :: [(Annoted SPEC, [Annotation])]
                aa' :: [(Annoted SPEC, [Annotation])]
aa' = ATermTable -> [(Annoted SPEC, [Annotation])]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in SPEC -> Bool -> SPEC
group ([Annoted SPEC] -> Range -> SPEC
Union ([(Annoted SPEC, [Annotation])] -> [Annoted SPEC]
forall a. [(Annoted a, [Annotation])] -> [Annoted a]
toAnnotedList [(Annoted SPEC, [Annotation])]
aa') Range
ab') Bool
group_flag
            (ShAAppl "extension" [ aa :: Int
aa ] _) ->
                let
                aa' :: [(Annoted SPEC, [Annotation])]
                aa' :: [(Annoted SPEC, [Annotation])]
aa' = ATermTable -> [(Annoted SPEC, [Annotation])]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in SPEC -> Bool -> SPEC
group ([Annoted SPEC] -> Range -> SPEC
Extension ([(Annoted SPEC, [Annotation])] -> [Annoted SPEC]
forall a. [(Annoted a, [Annotation])] -> [Annoted a]
toAnnotedList [(Annoted SPEC, [Annotation])]
aa') Range
ab') Bool
group_flag
            (ShAAppl "free-spec" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Annoted SPEC
aa' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                aa'' :: Annoted SPEC
aa'' = [Annotation] -> Annoted SPEC -> Annoted SPEC
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList (Int -> ATermTable -> [Annotation]
toAnnoList Int
ab ATermTable
att) Annoted SPEC
aa'
                ab' :: Range
ab' = Range
pos_l
                in SPEC -> Bool -> SPEC
group (Annoted SPEC -> Range -> SPEC
Free_spec Annoted SPEC
aa'' Range
ab') Bool
group_flag
            (ShAAppl "local-spec" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac, ad :: Int
ad ] _) ->
                let
                aa' :: Annoted SPEC
aa' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                sp1 :: Annoted SPEC
sp1 = [Annotation] -> Annoted SPEC -> Annoted SPEC
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList (Int -> ATermTable -> [Annotation]
toAnnoList Int
ab ATermTable
att) Annoted SPEC
aa'
                ac' :: Annoted SPEC
ac' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                sp2 :: Annoted SPEC
sp2 = [Annotation] -> Annoted SPEC -> Annoted SPEC
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList (Int -> ATermTable -> [Annotation]
toAnnoList Int
ad ATermTable
att) Annoted SPEC
ac'
                in SPEC -> Bool -> SPEC
group (Annoted SPEC -> Annoted SPEC -> Range -> SPEC
Local_spec Annoted SPEC
sp1 Annoted SPEC
sp2 Range
pos_l) Bool
group_flag
            (ShAAppl "closed-spec" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Annoted SPEC
aa' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                aa'' :: Annoted SPEC
aa'' = [Annotation] -> Annoted SPEC -> Annoted SPEC
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList (Int -> ATermTable -> [Annotation]
toAnnoList Int
ab ATermTable
att) Annoted SPEC
aa'
                ab' :: Range
ab' = Range
pos_l
                in SPEC -> Bool -> SPEC
group (Annoted SPEC -> Range -> SPEC
Closed_spec Annoted SPEC
aa'' Range
ab') Bool
group_flag
            (ShAAppl "spec-inst" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [Annoted FIT_ARG]
ab' = ATermTable -> [Annoted FIT_ARG]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                in IRI -> [Annoted FIT_ARG] -> Maybe IRI -> Range -> SPEC
Spec_inst IRI
aa' [Annoted FIT_ARG]
ab' Maybe IRI
forall a. Maybe a
Nothing Range
nullRange
            _ -> FilePath -> ShATerm -> SPEC
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "SPEC" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            group :: SPEC -> Bool -> SPEC
group s :: SPEC
s gf :: Bool
gf = if Bool
gf then Annoted SPEC -> Range -> SPEC
Group Annoted SPEC
s' Range
pos_l else SPEC
s
                where s' :: Annoted SPEC
s' = SPEC -> Annoted SPEC
forall a. a -> Annoted a
emptyAnno SPEC
s
            (pos_l :: Range
pos_l, group_flag :: Bool
group_flag, att' :: ATermTable
att') = FilePath -> ATermTable -> (Range, Bool, ATermTable)
skipPosFlag "pos-SPEC" ATermTable
att

-- - a helper function for [(Annoted a, [Annotation])] --------------------

toAnnotedList :: [(Annoted a, [Annotation])] -> [Annoted a]
toAnnotedList :: [(Annoted a, [Annotation])] -> [Annoted a]
toAnnotedList = ((Annoted a, [Annotation]) -> Annoted a)
-> [(Annoted a, [Annotation])] -> [Annoted a]
forall a b. (a -> b) -> [a] -> [b]
map (Annoted a, [Annotation]) -> Annoted a
forall a. (Annoted a, [Annotation]) -> Annoted a
merge
    where merge :: (Annoted a, [Annotation]) -> Annoted a
merge (ai :: Annoted a
ai, as :: [Annotation]
as) = Annoted a
ai { l_annos :: [Annotation]
l_annos = Annoted a -> [Annotation]
forall a. Annoted a -> [Annotation]
l_annos Annoted a
ai [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
as}

instance ATermConvertibleSML RENAMING where
    from_sml_ShATerm :: ATermTable -> RENAMING
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "renaming" [ aa :: Int
aa ] _) ->
              case ATermTable -> [SYMB_MAP_ITEMS]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att) of
              aa' :: [SYMB_MAP_ITEMS]
aa' -> let
                aa'' :: [G_mapping]
aa'' = if [SYMB_MAP_ITEMS] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SYMB_MAP_ITEMS]
aa' then []
                      else [G_symb_map_items_list -> G_mapping
G_symb_map (G_symb_map_items_list -> G_mapping)
-> G_symb_map_items_list -> G_mapping
forall a b. (a -> b) -> a -> b
$ CASL -> [SYMB_MAP_ITEMS] -> G_symb_map_items_list
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [symb_map_items] -> G_symb_map_items_list
G_symb_map_items_list CASL
CASL [SYMB_MAP_ITEMS]
aa']
                ab' :: Range
ab' = Range
pos_l
                in [G_mapping] -> Range -> RENAMING
Renaming [G_mapping]
aa'' Range
ab'
            _ -> FilePath -> ShATerm -> RENAMING
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "RENAMING" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-RENAMING" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML RESTRICTION where
    from_sml_ShATerm :: ATermTable -> RESTRICTION
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "hide" [ aa :: Int
aa ] _) ->
                let
                aa'' :: [G_hiding]
aa'' = case ATermTable -> [SYMB_ITEMS]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att) of
                      [] -> []
                      aa' :: [SYMB_ITEMS]
aa' -> [G_symb_items_list -> G_hiding
G_symb_list (G_symb_items_list -> G_hiding) -> G_symb_items_list -> G_hiding
forall a b. (a -> b) -> a -> b
$ CASL -> [SYMB_ITEMS] -> G_symb_items_list
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [symb_items] -> G_symb_items_list
G_symb_items_list CASL
CASL [SYMB_ITEMS]
aa']
                ab' :: Range
ab' = Range
pos_l
                in [G_hiding] -> Range -> RESTRICTION
Hidden [G_hiding]
aa'' Range
ab'
            (ShAAppl "reveal" [ aa :: Int
aa ] _) ->
                let
                aa' :: [SYMB_MAP_ITEMS]
aa' = ATermTable -> [SYMB_MAP_ITEMS]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                aa'' :: G_symb_map_items_list
aa'' = CASL -> [SYMB_MAP_ITEMS] -> G_symb_map_items_list
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [symb_map_items] -> G_symb_map_items_list
G_symb_map_items_list CASL
CASL [SYMB_MAP_ITEMS]
aa'
                ab' :: Range
ab' = Range
pos_l
                in G_symb_map_items_list -> Range -> RESTRICTION
Revealed G_symb_map_items_list
aa'' Range
ab'
            _ -> FilePath -> ShATerm -> RESTRICTION
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "RESTRICTION" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-RESTRICTION" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

{- !!! This will be done by the instance of LIB_ITEM !!!
instance ATermConvertibleSML SPEC_DEFN where
-}

instance ATermConvertibleSML GENERICITY where
    from_sml_ShATerm :: ATermTable -> GENERICITY
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "genericity" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: PARAMS
aa' = ATermTable -> PARAMS
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: IMPORTED
ab' = ATermTable -> IMPORTED
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in PARAMS -> IMPORTED -> Range -> GENERICITY
Genericity PARAMS
aa' IMPORTED
ab' Range
ac'
            _ -> FilePath -> ShATerm -> GENERICITY
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "GENERICITY" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-GENERICITY" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML PARAMS where
    from_sml_ShATerm :: ATermTable -> PARAMS
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "params" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Annoted SPEC]
aa' = ATermTable -> [Annoted SPEC]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in [Annoted SPEC] -> PARAMS
Params [Annoted SPEC]
aa'
            _ -> FilePath -> ShATerm -> PARAMS
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "PARAMS" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-PARAMS" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML IMPORTED where
    from_sml_ShATerm :: ATermTable -> IMPORTED
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "imports" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Annoted SPEC]
aa' = ATermTable -> [Annoted SPEC]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in [Annoted SPEC] -> IMPORTED
Imported [Annoted SPEC]
aa'
            _ -> FilePath -> ShATerm -> IMPORTED
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "IMPORTED" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-IMPORTS" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML FIT_ARG where
    from_sml_ShATerm :: ATermTable -> FIT_ARG
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "fit-spec" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Annoted SPEC
aa' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab'' :: [G_mapping]
ab'' = case ATermTable -> [SYMB_MAP_ITEMS]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att) of
                      [] -> []
                      ab' :: [SYMB_MAP_ITEMS]
ab' -> [G_symb_map_items_list -> G_mapping
G_symb_map (G_symb_map_items_list -> G_mapping)
-> G_symb_map_items_list -> G_mapping
forall a b. (a -> b) -> a -> b
$ CASL -> [SYMB_MAP_ITEMS] -> G_symb_map_items_list
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [symb_map_items] -> G_symb_map_items_list
G_symb_map_items_list CASL
CASL [SYMB_MAP_ITEMS]
ab']
                ac' :: Range
ac' = Range
pos_l
                in Annoted SPEC -> [G_mapping] -> Range -> FIT_ARG
Fit_spec Annoted SPEC
aa' [G_mapping]
ab'' Range
ac'
            (ShAAppl "fit-view" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [Annoted FIT_ARG]
ab' = ATermTable -> [Annoted FIT_ARG]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in IRI -> [Annoted FIT_ARG] -> Range -> FIT_ARG
Fit_view IRI
aa' [Annoted FIT_ARG]
ab' Range
ac'
            _ -> FilePath -> ShATerm -> FIT_ARG
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "FIT_ARG" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-FIT-ARG" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)
{- !!! This conversion is covered by the instance of LIB_ITEM !!!

instance ATermConvertibleSML VIEW_DEFN where
-}

instance ATermConvertibleSML VIEW_TYPE where
    from_sml_ShATerm :: ATermTable -> VIEW_TYPE
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "view-type" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Annoted SPEC
aa' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Annoted SPEC
ab' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in Annoted SPEC -> Annoted SPEC -> Range -> VIEW_TYPE
View_type Annoted SPEC
aa' Annoted SPEC
ab' Range
ac'
            _ -> FilePath -> ShATerm -> VIEW_TYPE
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "VIEW_TYPE" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-VIEW-TYPE" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

{- --- instances of AS_Architecture.hs -----------------------------------
!!! This conversion is covered by the instance of LIB_ITEM !!!
instance ATermConvertibleSML ARCH_SPEC_DEFN where
-}

instance ATermConvertibleSML ARCH_SPEC where
    from_sml_ShATerm :: ATermTable -> ARCH_SPEC
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "basic-arch-spec" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac ] _) ->
                let
                hd :: Annoted UNIT_DECL_DEFN
hd : tl :: [Annoted UNIT_DECL_DEFN]
tl = ATermTable -> [Annoted UNIT_DECL_DEFN]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Annoted UNIT_EXPRESSION
ab' = ATermTable -> Annoted UNIT_EXPRESSION
from_sml_ATermRESULT_UNIT (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                as :: [Annotation]
as = Int -> ATermTable -> [Annotation]
toAnnoList Int
ac ATermTable
att
                aa'' :: [Annoted UNIT_DECL_DEFN]
aa'' = [Annotation] -> Annoted UNIT_DECL_DEFN -> Annoted UNIT_DECL_DEFN
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList [Annotation]
as Annoted UNIT_DECL_DEFN
hd Annoted UNIT_DECL_DEFN
-> [Annoted UNIT_DECL_DEFN] -> [Annoted UNIT_DECL_DEFN]
forall a. a -> [a] -> [a]
: [Annoted UNIT_DECL_DEFN]
tl
                ac' :: Range
ac' = Range
pos_l
                in [Annoted UNIT_DECL_DEFN]
-> Annoted UNIT_EXPRESSION -> Range -> ARCH_SPEC
Basic_arch_spec [Annoted UNIT_DECL_DEFN]
aa'' Annoted UNIT_EXPRESSION
ab' Range
ac'
            (ShAAppl "named-arch-spec" [ aa :: Int
aa ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in IRI -> ARCH_SPEC
Arch_spec_name IRI
aa'
            _ -> FilePath -> ShATerm -> ARCH_SPEC
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "ARCH_SPEC" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-ARCH-SPEC" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

from_sml_ATermRESULT_UNIT :: ATermTable -> Annoted UNIT_EXPRESSION
from_sml_ATermRESULT_UNIT :: ATermTable -> Annoted UNIT_EXPRESSION
from_sml_ATermRESULT_UNIT att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "result-unit" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
-- aa' :: UNIT_EXPRESSION
                aa' :: UNIT_EXPRESSION
aa' = ATermTable -> UNIT_EXPRESSION
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                as :: [Annotation]
as = Int -> ATermTable -> [Annotation]
toAnnoList Int
ab ATermTable
att
                in UNIT_EXPRESSION
-> Range -> [Annotation] -> [Annotation] -> Annoted UNIT_EXPRESSION
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted UNIT_EXPRESSION
aa' Range
nullRange [Annotation]
as []
            _ -> FilePath -> ShATerm -> Annoted UNIT_EXPRESSION
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "RESULT-UNIT" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-RESULT-UNIT" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML UNIT_REF where
    from_sml_ShATerm :: ATermTable -> UNIT_REF
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "unit-decl-case" [ udl :: Int
udl ] _) ->
                let att1 :: ATermTable
att1 = Int -> ATermTable -> ATermTable
getATermByIndex1 Int
udl ATermTable
att
                    (ps :: Range
ps, att2 :: ATermTable
att2) = case ATermTable -> ShATerm
getATerm ATermTable
att1 of
                                  (ShAAppl "pos-UNIT-DECL" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                                      (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att,
                                       Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att1)
                                  _ -> (Range
nullRange, ATermTable
att1)
                    aterm2 :: ShATerm
aterm2 = ATermTable -> ShATerm
getATerm ATermTable
att2
                in case ShATerm
aterm2 of
                   ShAAppl "unit-decl" [aa :: Int
aa, ab :: Int
ab, _] _ ->
                      let aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (ATermTable -> IRI) -> ATermTable -> IRI
forall a b. (a -> b) -> a -> b
$
                               Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att
                          ab' :: REF_SPEC
ab' = ATermTable -> REF_SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                          ad' :: Range
ad' = Range
ps
                      in IRI -> REF_SPEC -> Range -> UNIT_REF
Unit_ref IRI
aa' REF_SPEC
ab' Range
ad'
                   _ -> FilePath -> ShATerm -> UNIT_REF
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_DECL" ShATerm
aterm2
            _ -> FilePath -> ShATerm -> UNIT_REF
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT-DECL-DEFN" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-UNIT-DECL-DEFN" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML UNIT_DECL_DEFN where
    from_sml_ShATerm :: ATermTable -> UNIT_DECL_DEFN
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "unit-decl-case" [ udl :: Int
udl ] _) ->
                let att1 :: ATermTable
att1 = Int -> ATermTable -> ATermTable
getATermByIndex1 Int
udl ATermTable
att
                    (ps :: Range
ps, att2 :: ATermTable
att2) = case ATermTable -> ShATerm
getATerm ATermTable
att1 of
                                  (ShAAppl "pos-UNIT-DECL" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                                      (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att,
                                       Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att1)
                                  _ -> (Range
nullRange, ATermTable
att1)
                    aterm2 :: ShATerm
aterm2 = ATermTable -> ShATerm
getATerm ATermTable
att2
                in case ShATerm
aterm2 of
                   ShAAppl "unit-decl" [aa :: Int
aa, ab :: Int
ab, ac :: Int
ac] _ ->
                    let aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (ATermTable -> IRI) -> ATermTable -> IRI
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att
                        ab' :: REF_SPEC
ab' = ATermTable -> REF_SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> REF_SPEC) -> ATermTable -> REF_SPEC
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att
                        ac' :: [Annoted UNIT_TERM]
ac' = ATermTable -> [Annoted UNIT_TERM]
from_sml_ATermUNIT_IMPORTS (ATermTable -> [Annoted UNIT_TERM])
-> ATermTable -> [Annoted UNIT_TERM]
forall a b. (a -> b) -> a -> b
$
                                         Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att
                        ad' :: Range
ad' = Range
ps
                    in IRI -> REF_SPEC -> [Annoted UNIT_TERM] -> Range -> UNIT_DECL_DEFN
Unit_decl IRI
aa' REF_SPEC
ab' [Annoted UNIT_TERM]
ac' Range
ad'
                   _ -> FilePath -> ShATerm -> UNIT_DECL_DEFN
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_DECL" ShATerm
aterm2
            (ShAAppl "unit-defn-case" [ udn :: Int
udn ] _) ->
                ATermTable -> UNIT_DECL_DEFN
from_sml_ATermUNIT_DEFN (ATermTable -> UNIT_DECL_DEFN) -> ATermTable -> UNIT_DECL_DEFN
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
udn ATermTable
att
            (ShAAppl "pos-UNIT-DEFN" _ _) ->
                ATermTable -> UNIT_DECL_DEFN
from_sml_ATermUNIT_DEFN ATermTable
att
            (ShAAppl "unit-defn" _ _) ->
                ATermTable -> UNIT_DECL_DEFN
from_sml_ATermUNIT_DEFN ATermTable
att
            _ -> FilePath -> ShATerm -> UNIT_DECL_DEFN
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT-DECL-DEFN" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-UNIT-DECL-DEFN" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

-- -- a helper for the SML-datatype UNIT_IMPORTS ------------------------

from_sml_ATermUNIT_IMPORTS :: ATermTable -> [Annoted UNIT_TERM]
from_sml_ATermUNIT_IMPORTS :: ATermTable -> [Annoted UNIT_TERM]
from_sml_ATermUNIT_IMPORTS att :: ATermTable
att =
    case ShATerm
aterm of
             (ShAAppl "unit-imports" [ aa :: Int
aa ] _) ->
                 ATermTable -> [Annoted UNIT_TERM]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> [Annoted UNIT_TERM])
-> ATermTable -> [Annoted UNIT_TERM]
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att
             _ -> FilePath -> ShATerm -> [Annoted UNIT_TERM]
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_IMPORTS" ShATerm
aterm
    where aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
          att' :: ATermTable
att' =
              case ATermTable -> ShATerm
getATerm ATermTable
att of
              (ShAAppl "pos-UNIT-IMPORTS" [_, item_i :: Int
item_i] _) ->
                  Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
              _ -> ATermTable
att

from_sml_ATermUNIT_DEFN :: ATermTable -> UNIT_DECL_DEFN
from_sml_ATermUNIT_DEFN :: ATermTable -> UNIT_DECL_DEFN
from_sml_ATermUNIT_DEFN att :: ATermTable
att =
    case ShATerm
aterm of
    ShAAppl "unit-defn" [aa :: Int
aa, ab :: Int
ab] _ ->
        let aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
            ab' :: UNIT_EXPRESSION
ab' = ATermTable -> UNIT_EXPRESSION
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
            ac' :: Range
ac' = Range
ps
        in IRI -> UNIT_EXPRESSION -> Range -> UNIT_DECL_DEFN
Unit_defn IRI
aa' UNIT_EXPRESSION
ab' Range
ac'
    _ -> FilePath -> ShATerm -> UNIT_DECL_DEFN
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_DEFN" ShATerm
aterm
    where aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
          (ps :: Range
ps, att' :: ATermTable
att') =
              case ATermTable -> ShATerm
getATerm ATermTable
att of
              (ShAAppl "pos-UNIT-DEFN" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                  (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
              _ -> (Range
nullRange, ATermTable
att)

{- !!! This conversion is covered by the instance of LIB_ITEM !!!
instance ATermConvertibleSML UNIT_SPEC_DEFN where
-}

instance ATermConvertibleSML UNIT_SPEC where
    from_sml_ShATerm :: ATermTable -> UNIT_SPEC
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "unit-type-case" [ aa :: Int
aa ] _) ->
                let
                (aa' :: [Annoted SPEC]
aa', ab' :: Annoted SPEC
ab') = ATermTable -> ([Annoted SPEC], Annoted SPEC)
from_sml_ATermUNIT_TYPE (ATermTable -> ([Annoted SPEC], Annoted SPEC))
-> ATermTable -> ([Annoted SPEC], Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att
                ac' :: Range
ac' = Range
pos_l
                in [Annoted SPEC] -> Annoted SPEC -> Range -> UNIT_SPEC
Unit_type [Annoted SPEC]
aa' Annoted SPEC
ab' Range
ac'
            (ShAAppl "spec-name-case" [ aa :: Int
aa ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in IRI -> UNIT_SPEC
Spec_name IRI
aa'
            (ShAAppl "closed" [ aa :: Int
aa ] _) ->
                let
                aa' :: UNIT_SPEC
aa' = ATermTable -> UNIT_SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in UNIT_SPEC -> Range -> UNIT_SPEC
Closed_unit_spec UNIT_SPEC
aa' Range
ab'
            _ -> FilePath -> ShATerm -> UNIT_SPEC
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_SPEC" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-UNIT-SPEC" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML REF_SPEC where
    from_sml_ShATerm :: ATermTable -> REF_SPEC
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "unit-type-case" [ aa :: Int
aa ] _) ->
                let
                (aa' :: [Annoted SPEC]
aa', ab' :: Annoted SPEC
ab') = ATermTable -> ([Annoted SPEC], Annoted SPEC)
from_sml_ATermUNIT_TYPE (ATermTable -> ([Annoted SPEC], Annoted SPEC))
-> ATermTable -> ([Annoted SPEC], Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att
                ac' :: Range
ac' = Range
pos_l
                in UNIT_SPEC -> REF_SPEC
Unit_spec (UNIT_SPEC -> REF_SPEC) -> UNIT_SPEC -> REF_SPEC
forall a b. (a -> b) -> a -> b
$ [Annoted SPEC] -> Annoted SPEC -> Range -> UNIT_SPEC
Unit_type [Annoted SPEC]
aa' Annoted SPEC
ab' Range
ac'
            (ShAAppl "spec-name-case" [ aa :: Int
aa ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                in (UNIT_SPEC -> REF_SPEC
Unit_spec (UNIT_SPEC -> REF_SPEC) -> UNIT_SPEC -> REF_SPEC
forall a b. (a -> b) -> a -> b
$ IRI -> UNIT_SPEC
Spec_name IRI
aa')
            (ShAAppl "arch-spec-case" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Annoted ARCH_SPEC
aa' = ATermTable -> Annoted ARCH_SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ps :: [Annotation]
ps = Int -> ATermTable -> [Annotation]
toAnnoList Int
ab ATermTable
att
                aa'' :: Annoted ARCH_SPEC
aa'' = [Annotation] -> Annoted ARCH_SPEC -> Annoted ARCH_SPEC
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList [Annotation]
ps Annoted ARCH_SPEC
aa'
                ab' :: Range
ab' = Range
pos_l
                aa''' :: Annoted ARCH_SPEC
aa''' = case Annoted ARCH_SPEC
aa'' of
                        (Annoted (Basic_arch_spec {}) _ _ _) ->
                            ARCH_SPEC -> Annoted ARCH_SPEC
forall a. a -> Annoted a
emptyAnno (Annoted ARCH_SPEC -> Range -> ARCH_SPEC
Group_arch_spec Annoted ARCH_SPEC
aa'' Range
ab')
                        _ -> Annoted ARCH_SPEC
aa''
                in Annoted ARCH_SPEC -> Range -> REF_SPEC
Arch_unit_spec Annoted ARCH_SPEC
aa''' Range
ab'
            (ShAAppl "closed" [ aa :: Int
aa ] _) ->
                let
                aa' :: UNIT_SPEC
aa' = ATermTable -> UNIT_SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in (UNIT_SPEC -> REF_SPEC
Unit_spec (UNIT_SPEC -> REF_SPEC) -> UNIT_SPEC -> REF_SPEC
forall a b. (a -> b) -> a -> b
$ UNIT_SPEC -> Range -> UNIT_SPEC
Closed_unit_spec UNIT_SPEC
aa' Range
ab')
            _ -> FilePath -> ShATerm -> REF_SPEC
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_SPEC" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-UNIT-SPEC" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

-- -- a helper for the SML-datatype UNIT_TYPE ----------------------------

from_sml_ATermUNIT_TYPE :: ATermTable -> ([Annoted SPEC], Annoted SPEC)
from_sml_ATermUNIT_TYPE :: ATermTable -> ([Annoted SPEC], Annoted SPEC)
from_sml_ATermUNIT_TYPE att :: ATermTable
att =
    case ShATerm
aterm of
             (ShAAppl "unit-type" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                 (ATermTable -> [Annoted SPEC]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> [Annoted SPEC]) -> ATermTable -> [Annoted SPEC]
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att,
                  ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> Annoted SPEC) -> ATermTable -> Annoted SPEC
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
             _ -> FilePath -> ShATerm -> ([Annoted SPEC], Annoted SPEC)
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_TYPE" ShATerm
aterm
    where aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
          att' :: ATermTable
att' =
              case ATermTable -> ShATerm
getATerm ATermTable
att of
              (ShAAppl "pos-UNIT-TYPE" [_, item_i :: Int
item_i] _) ->
                  Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
              _ -> ATermTable
att

instance ATermConvertibleSML UNIT_EXPRESSION where
    from_sml_ShATerm :: ATermTable -> UNIT_EXPRESSION
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "unit-expression" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [UNIT_BINDING]
aa' = ATermTable -> [UNIT_BINDING]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Annoted UNIT_TERM
ab' = ATermTable -> Annoted UNIT_TERM
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in [UNIT_BINDING] -> Annoted UNIT_TERM -> Range -> UNIT_EXPRESSION
Unit_expression [UNIT_BINDING]
aa' Annoted UNIT_TERM
ab' Range
ac'
            _ -> FilePath -> ShATerm -> UNIT_EXPRESSION
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_EXPRESSION" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-UNIT-EXPRESSION" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML UNIT_BINDING where
    from_sml_ShATerm :: ATermTable -> UNIT_BINDING
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "unit-binding" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: UNIT_SPEC
ab' = ATermTable -> UNIT_SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in IRI -> UNIT_SPEC -> Range -> UNIT_BINDING
Unit_binding IRI
aa' UNIT_SPEC
ab' Range
ac'
            _ -> FilePath -> ShATerm -> UNIT_BINDING
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_BINDING" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-UNIT-BINDING" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML UNIT_TERM where
    from_sml_ShATerm :: ATermTable -> UNIT_TERM
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "unit-reduction" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Annoted UNIT_TERM
aa' = ATermTable -> Annoted UNIT_TERM
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: RESTRICTION
ab' = ATermTable -> RESTRICTION
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                in UNIT_TERM -> Bool -> UNIT_TERM
group (Annoted UNIT_TERM -> RESTRICTION -> UNIT_TERM
Unit_reduction Annoted UNIT_TERM
aa' RESTRICTION
ab') Bool
group_flag
            (ShAAppl "unit-translation" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: Annoted UNIT_TERM
aa' = ATermTable -> Annoted UNIT_TERM
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: RENAMING
ab' = ATermTable -> RENAMING
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                in UNIT_TERM -> Bool -> UNIT_TERM
group (Annoted UNIT_TERM -> RENAMING -> UNIT_TERM
Unit_translation Annoted UNIT_TERM
aa' RENAMING
ab') Bool
group_flag
            (ShAAppl "amalgamation" [ aa :: Int
aa ] _) ->
                let
                aa' :: [Annoted UNIT_TERM]
aa' = ATermTable -> [Annoted UNIT_TERM]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in UNIT_TERM -> Bool -> UNIT_TERM
group ([Annoted UNIT_TERM] -> Range -> UNIT_TERM
Amalgamation [Annoted UNIT_TERM]
aa' Range
ab') Bool
group_flag
            (ShAAppl "local-unit" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: [Annoted UNIT_DECL_DEFN]
aa' = ATermTable -> [Annoted UNIT_DECL_DEFN]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Annoted UNIT_TERM
ab' = ATermTable -> Annoted UNIT_TERM
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in UNIT_TERM -> Bool -> UNIT_TERM
group ([Annoted UNIT_DECL_DEFN] -> Annoted UNIT_TERM -> Range -> UNIT_TERM
Local_unit [Annoted UNIT_DECL_DEFN]
aa' Annoted UNIT_TERM
ab' Range
ac') Bool
group_flag
            (ShAAppl "unit-appl" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [FIT_ARG_UNIT]
ab' = ATermTable -> [FIT_ARG_UNIT]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in UNIT_TERM -> Bool -> UNIT_TERM
group (IRI -> [FIT_ARG_UNIT] -> Range -> UNIT_TERM
Unit_appl IRI
aa' [FIT_ARG_UNIT]
ab' Range
ac') Bool
group_flag
            _ -> FilePath -> ShATerm -> UNIT_TERM
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "UNIT_TERM" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            group :: UNIT_TERM -> Bool -> UNIT_TERM
group ut :: UNIT_TERM
ut gf :: Bool
gf = if Bool
gf then Annoted UNIT_TERM -> Range -> UNIT_TERM
Group_unit_term Annoted UNIT_TERM
ut' Range
pos_l else UNIT_TERM
ut
                where ut' :: Annoted UNIT_TERM
ut' = UNIT_TERM -> Annoted UNIT_TERM
forall a. a -> Annoted a
emptyAnno UNIT_TERM
ut
            (pos_l :: Range
pos_l, group_flag :: Bool
group_flag, att' :: ATermTable
att') = FilePath -> ATermTable -> (Range, Bool, ATermTable)
skipPosFlag "pos-UNIT-TERM" ATermTable
att

instance ATermConvertibleSML FIT_ARG_UNIT where
    from_sml_ShATerm :: ATermTable -> FIT_ARG_UNIT
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "fit-arg-unit" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                case ATermTable -> Annoted UNIT_TERM
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att) of
                aa' :: Annoted UNIT_TERM
aa' -> case ATermTable -> [SYMB_MAP_ITEMS]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att) of
                    ab' :: [SYMB_MAP_ITEMS]
ab' -> Annoted UNIT_TERM -> [G_mapping] -> Range -> FIT_ARG_UNIT
Fit_arg_unit Annoted UNIT_TERM
aa' (if [SYMB_MAP_ITEMS] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SYMB_MAP_ITEMS]
ab' then [] else
                      [G_symb_map_items_list -> G_mapping
G_symb_map (G_symb_map_items_list -> G_mapping)
-> G_symb_map_items_list -> G_mapping
forall a b. (a -> b) -> a -> b
$ CASL -> [SYMB_MAP_ITEMS] -> G_symb_map_items_list
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [symb_map_items] -> G_symb_map_items_list
G_symb_map_items_list CASL
CASL [SYMB_MAP_ITEMS]
ab']) Range
pos_l
            _ -> FilePath -> ShATerm -> FIT_ARG_UNIT
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "FIT_ARG_UNIT" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-FIT-ARG-UNIT" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

-- --- instances of AS_LIbrary.hs ----------------------------------------
instance ATermConvertibleSML LIB_DEFN where
    from_sml_ShATerm :: ATermTable -> LIB_DEFN
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "lib-defn" [ aa :: Int
aa, ab :: Int
ab, ad :: Int
ad ] _) ->
                let
                aa' :: LibName
aa' = ATermTable -> LibName
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [Annoted LIB_ITEM]
ab' = ATermTable -> [Annoted LIB_ITEM]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                ad' :: [Annotation]
ad' = ATermTable -> [Annotation]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ad ATermTable
att)
                in LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn LibName
aa' [Annoted LIB_ITEM]
ab' Range
ac' [Annotation]
ad'
            _ -> FilePath -> ShATerm -> LIB_DEFN
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "LIB_DEFN" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-LIB-DEFN" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML LIB_ITEM where
    from_sml_ShATerm :: ATermTable -> LIB_ITEM
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "spec-defn" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac, ad :: Int
ad ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: GENERICITY
ab' = ATermTable -> GENERICITY
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Annoted SPEC
ac' = ATermTable -> Annoted SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                as :: [Annotation]
as = Int -> ATermTable -> [Annotation]
toAnnoList Int
ad ATermTable
att
                ac'' :: Annoted SPEC
ac'' = [Annotation] -> Annoted SPEC -> Annoted SPEC
forall a. [Annotation] -> Annoted a -> Annoted a
addLAnnoList [Annotation]
as Annoted SPEC
ac'
                ad' :: Range
ad' = Range
pos_l
                in IRI -> GENERICITY -> Annoted SPEC -> Range -> LIB_ITEM
Syntax.AS_Library.Spec_defn IRI
aa' GENERICITY
ab' Annoted SPEC
ac'' Range
ad'
            (ShAAppl "view-defn" [ aa :: Int
aa, ab :: Int
ab, ac :: Int
ac, ad :: Int
ad, _ ] _) ->
                let  -- the annotation list is lost !!!!
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: GENERICITY
ab' = ATermTable -> GENERICITY
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: VIEW_TYPE
ac' = ATermTable -> VIEW_TYPE
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ac ATermTable
att)
                ad'' :: [G_mapping]
ad'' = case ATermTable -> [SYMB_MAP_ITEMS]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ad ATermTable
att) of
                      [] -> []
                      ad' :: [SYMB_MAP_ITEMS]
ad' -> [G_symb_map_items_list -> G_mapping
G_symb_map (G_symb_map_items_list -> G_mapping)
-> G_symb_map_items_list -> G_mapping
forall a b. (a -> b) -> a -> b
$ CASL -> [SYMB_MAP_ITEMS] -> G_symb_map_items_list
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [symb_map_items] -> G_symb_map_items_list
G_symb_map_items_list CASL
CASL [SYMB_MAP_ITEMS]
ad']
                ae' :: Range
ae' = Range
pos_l
                in IRI -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range -> LIB_ITEM
Syntax.AS_Library.View_defn IRI
aa' GENERICITY
ab' VIEW_TYPE
ac' [G_mapping]
ad'' Range
ae'
            (ShAAppl "arch-spec-defn" [ aa :: Int
aa, ab :: Int
ab, _ ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Annoted ARCH_SPEC
ab' = ATermTable -> Annoted ARCH_SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in IRI -> Annoted ARCH_SPEC -> Range -> LIB_ITEM
Syntax.AS_Library.Arch_spec_defn IRI
aa' Annoted ARCH_SPEC
ab' Range
ac'
            (ShAAppl "unit-spec-defn" [ aa :: Int
aa, ab :: Int
ab, _ ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: UNIT_SPEC
ab' = ATermTable -> UNIT_SPEC
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in IRI -> UNIT_SPEC -> Range -> LIB_ITEM
Syntax.AS_Library.Unit_spec_defn IRI
aa' UNIT_SPEC
ab' Range
ac'
            (ShAAppl "download-items" [ aa :: Int
aa, ab :: Int
ab, _ ] _) ->
                let
                aa' :: LibName
aa' = ATermTable -> LibName
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: [ItemNameMap]
ab' = ATermTable -> [ItemNameMap]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                ac' :: Range
ac' = Range
pos_l
                in LibName -> DownloadItems -> Range -> LIB_ITEM
Syntax.AS_Library.Download_items LibName
aa' ([ItemNameMap] -> DownloadItems
ItemMaps [ItemNameMap]
ab') Range
ac'
            _ -> FilePath -> ShATerm -> LIB_ITEM
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "LIB_ITEM" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') = FilePath -> ATermTable -> (Range, ATermTable)
skipPos "pos-LIB-ITEM" ATermTable
att

-- -- helpers to skip nested "pos-"-constructors -----------------------
skipPos :: String -> ATermTable -> (Range, ATermTable)
skipPos :: FilePath -> ATermTable -> (Range, ATermTable)
skipPos mcon :: FilePath
mcon at :: ATermTable
at =
     case ATermTable -> ShATerm
getATerm ATermTable
at of
              ShAAppl con :: FilePath
con [reg_i :: Int
reg_i, item_i :: Int
item_i] _ | FilePath
mcon FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
con ->
                  if Bool
pCon then FilePath -> ATermTable -> (Range, ATermTable)
skipPos FilePath
mcon ATermTable
at'
                  else (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
at, ATermTable
at')
                      where pCon :: Bool
pCon = case ATermTable -> ShATerm
getATerm ATermTable
at' of
                                   ShAAppl con' :: FilePath
con' _ _ | FilePath
mcon FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
con' -> Bool
True
                                   _ -> Bool
False
                            at' :: ATermTable
at' = Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
at
              _ -> (Range
nullRange, ATermTable
at)

skipPosFlag :: String -> ATermTable -> (Range, Bool, ATermTable)
skipPosFlag :: FilePath -> ATermTable -> (Range, Bool, ATermTable)
skipPosFlag mcon :: FilePath
mcon att :: ATermTable
att =
    case ATermTable -> ShATerm
getATerm ATermTable
att of
    ShAAppl con :: FilePath
con [reg_i :: Int
reg_i, b_i :: Int
b_i, item_i :: Int
item_i] _ | FilePath
mcon FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
con ->
          if Bool
pCon then let (_r_pos_l :: Range
_r_pos_l, r_b :: Bool
r_b, r_at' :: ATermTable
r_at') = FilePath -> ATermTable -> (Range, Bool, ATermTable)
skipPosFlag FilePath
mcon ATermTable
at'
                       in (Range
pos_l, Bool
r_b Bool -> Bool -> Bool
|| Bool
b, ATermTable
r_at')
          else (Range
pos_l, Bool
b, ATermTable
at')
              where pCon :: Bool
pCon = case ATermTable -> ShATerm
getATerm ATermTable
at' of
                            ShAAppl con' :: FilePath
con' _ _ | FilePath
mcon FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
con' -> Bool
True
                            _ -> Bool
False
                    at' :: ATermTable
at' = Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                    pos_l :: Range
pos_l = Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att
                    b :: Bool
b = ATermTable -> Bool
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (ATermTable -> Bool) -> ATermTable -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
b_i ATermTable
att
    _ -> (Range
nullRange, Bool
False, ATermTable
att)

instance ATermConvertibleSML ItemNameMap where
    from_sml_ShATerm :: ATermTable -> ItemNameMap
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            ShAAppl "item-name" [aa :: Int
aa] _ ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (ATermTable -> IRI) -> ATermTable -> IRI
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att
                in IRI -> Maybe IRI -> ItemNameMap
ItemNameMap IRI
aa' Maybe IRI
forall a. Maybe a
Nothing
            ShAAppl "item-name-map" [aa :: Int
aa, ab :: Int
ab] _ ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
from_sml_ATermIRI (ATermTable -> IRI) -> ATermTable -> IRI
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att
                ab' :: IRI
ab' = ATermTable -> IRI
from_sml_ATermIRI (ATermTable -> IRI) -> ATermTable -> IRI
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att
                in IRI -> Maybe IRI -> ItemNameMap
ItemNameMap IRI
aa' (Maybe IRI -> ItemNameMap) -> Maybe IRI -> ItemNameMap
forall a b. (a -> b) -> a -> b
$ IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
ab'
            _ -> FilePath -> ShATerm -> ItemNameMap
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "ITEM_NAME_OR_MAP" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' = case ATermTable -> ShATerm
getATerm ATermTable
att of
                ShAAppl "pos-ITEM-NAME-OR-MAP" [_, item_i :: Int
item_i] _ ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

instance ATermConvertibleSML LibName where
    from_sml_ShATerm :: ATermTable -> LibName
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "versioned-lib" [ aa :: Int
aa, ab :: Int
ab ] _) ->
                let
                aa' :: IRI
aa' = ATermTable -> IRI
fromSmlShATermToLibId (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: VersionNumber
ab' = ATermTable -> VersionNumber
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
ab ATermTable
att)
                in IRI -> Maybe VersionNumber -> LibName
mkLibName IRI
aa' (Maybe VersionNumber -> LibName) -> Maybe VersionNumber -> LibName
forall a b. (a -> b) -> a -> b
$ VersionNumber -> Maybe VersionNumber
forall a. a -> Maybe a
Just VersionNumber
ab'
            (ShAAppl "lib" [ aa :: Int
aa ] _) ->
                IRI -> LibName
iriLibName (IRI -> LibName) -> (ATermTable -> IRI) -> ATermTable -> LibName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATermTable -> IRI
fromSmlShATermToLibId (ATermTable -> LibName) -> ATermTable -> LibName
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att
            _ -> FilePath -> ShATerm -> LibName
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "LibName" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            att' :: ATermTable
att' =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-LIB-NAME" [_, item_i :: Int
item_i] _) ->
                    Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att
                _ -> ATermTable
att

fromSmlShATermToLibId :: ATermTable -> IRI
fromSmlShATermToLibId :: ATermTable -> IRI
fromSmlShATermToLibId att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl str :: FilePath
str [ aa :: Int
aa ] _) | FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FilePath
str ["path-name", "url"] ->
                let
                aa' :: FilePath
aa' = ATermTable -> FilePath
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in (IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> IRI
forall a. HasCallStack => FilePath -> a
error "fromSmlShATermToLibId")
                   (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe IRI
parseIRICurie FilePath
aa') { iriPos :: Range
iriPos = Range
ab' }
            _ -> FilePath -> ShATerm -> IRI
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "LibId" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-LIB-ID" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)

instance ATermConvertibleSML VersionNumber where
    from_sml_ShATerm :: ATermTable -> VersionNumber
from_sml_ShATerm att :: ATermTable
att =
        case ShATerm
aterm of
            (ShAAppl "version" [ aa :: Int
aa ] _) ->
                let
                aa' :: [FilePath]
aa' = ATermTable -> [FilePath]
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm (Int -> ATermTable -> ATermTable
getATermByIndex1 Int
aa ATermTable
att)
                ab' :: Range
ab' = Range
pos_l
                in [FilePath] -> Range -> VersionNumber
VersionNumber [FilePath]
aa' Range
ab'
            _ -> FilePath -> ShATerm -> VersionNumber
forall a. FilePath -> ShATerm -> a
from_sml_ShATermError "VersionNumber" ShATerm
aterm
        where
            aterm :: ShATerm
aterm = ATermTable -> ShATerm
getATerm ATermTable
att'
            (pos_l :: Range
pos_l, att' :: ATermTable
att') =
                case ATermTable -> ShATerm
getATerm ATermTable
att of
                (ShAAppl "pos-VERSION" [reg_i :: Int
reg_i, item_i :: Int
item_i] _) ->
                    (Int -> ATermTable -> Range
posFromRegion Int
reg_i ATermTable
att, Int -> ATermTable -> ATermTable
getATermByIndex1 Int
item_i ATermTable
att)
                _ -> (Range
nullRange, ATermTable
att)
-- -----------------------------------------------------------------------

-- some helpers for Annoted things --------------------------------------
addLAnnoList :: [Annotation] -> Annoted a -> Annoted a
addLAnnoList :: [Annotation] -> Annoted a -> Annoted a
addLAnnoList as :: [Annotation]
as ani :: Annoted a
ani = Annoted a
ani {l_annos :: [Annotation]
l_annos = [Annotation]
as [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ Annoted a -> [Annotation]
forall a. Annoted a -> [Annotation]
l_annos Annoted a
ani }

addRAnnoList :: [Annotation] -> Annoted a -> Annoted a
addRAnnoList :: [Annotation] -> Annoted a -> Annoted a
addRAnnoList as :: [Annotation]
as ani :: Annoted a
ani = Annoted a
ani {r_annos :: [Annotation]
r_annos = Annoted a -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos Annoted a
ani [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
as }

-- - some helpers for Regions and Positions ------------------------------

posFromRegion :: Int -> ATermTable -> Range
posFromRegion :: Int -> ATermTable -> Range
posFromRegion reg :: Int
reg at :: ATermTable
at = [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ ((Int, Int) -> Pos) -> [(Int, Int)] -> [Pos]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int -> Pos) -> (Int, Int) -> Pos
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Int -> Int -> Pos) -> (Int, Int) -> Pos)
-> (Int -> Int -> Pos) -> (Int, Int) -> Pos
forall a b. (a -> b) -> a -> b
$ FilePath -> Int -> Int -> Pos
newPos "")
                             ([(Int, Int)] -> [Pos]) -> [(Int, Int)] -> [Pos]
forall a b. (a -> b) -> a -> b
$ Int -> ATermTable -> [(Int, Int)]
from_sml_ATerm_reg Int
reg ATermTable
at

getPos :: ATermTable -> Range
getPos :: ATermTable -> Range
getPos att :: ATermTable
att = case ATermTable -> ShATerm
getATerm ATermTable
att of
                ShAAppl _ (x :: Int
x : _) _ -> Int -> ATermTable -> Range
posFromRegion Int
x ATermTable
att
                _ -> Range
nullRange

-- converts an aterm region information to Range
from_sml_ATerm_reg :: Int -> ATermTable -> [(Int, Int)]
from_sml_ATerm_reg :: Int -> ATermTable -> [(Int, Int)]
from_sml_ATerm_reg reg_i :: Int
reg_i at :: ATermTable
at = [((Int, Int), (Int, Int)) -> (Int, Int)
forall a b. (a, b) -> a
fst ((Int, Int), (Int, Int))
r, ((Int, Int), (Int, Int)) -> (Int, Int)
forall a b. (a, b) -> b
snd ((Int, Int), (Int, Int))
r]
    where r :: ((Int, Int), (Int, Int)) -- Id.hs Region
          r :: ((Int, Int), (Int, Int))
r = ATermTable -> ((Int, Int), (Int, Int))
forall t. ATermConvertibleSML t => ATermTable -> t
from_sml_ShATerm ATermTable
r_at
          r_at :: ATermTable
r_at = Int -> ATermTable -> ATermTable
getATermByIndex1 Int
reg_i ATermTable
at

insertIM, insertPosAux :: [a] -> [a] -> [a]
insertIM :: [a] -> [a] -> [a]
insertIM ips :: [a]
ips ops :: [a]
ops | Int -> Bool
forall a. Integral a => a -> Bool
even (Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ops = let hl :: Int
hl = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ops Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 2
                                           (fp :: [a]
fp, lp :: [a]
lp) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
hl [a]
ops
                                       in [a]
fp [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ips [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
lp
                 | Bool
otherwise = FilePath -> [a]
forall a. HasCallStack => FilePath -> a
error
                               "wrong call: length of snd list must be even"
insertPosAux :: [a] -> [a] -> [a]
insertPosAux = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
insertIM

insertPos :: Range -> Range -> Range
insertPos :: Range -> Range -> Range
insertPos (Range l1 :: [Pos]
l1) (Range l2 :: [Pos]
l2) = [Pos] -> Range
Range ([Pos] -> [Pos] -> [Pos]
forall a. [a] -> [a] -> [a]
insertPosAux [Pos]
l1 [Pos]
l2)

setFstPos :: Range -> Id -> Id
setFstPos :: Range -> Id -> Id
setFstPos (Range (p :: Pos
p : _)) i :: Id
i = case Id
i of
                       Id tops :: [Token]
tops ids :: [Id]
ids pos_l :: Range
pos_l ->
                           [Token] -> [Id] -> Range -> Id
Id ([Token] -> [Token]
setFstPos' [Token]
tops) [Id]
ids Range
pos_l
    where setFstPos' :: [Token] -> [Token]
setFstPos' tops :: [Token]
tops = case [Token]
tops of
              [] -> []
              hd :: Token
hd : tl :: [Token]
tl -> Token
hd { tokPos :: Range
tokPos = [Pos] -> Range
Range [Pos
p] } Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
tl
setFstPos _ _ = FilePath -> Id
forall a. HasCallStack => FilePath -> a
error "wrong call: setFstPos"