918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce{- |

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo SorceModule : $Header$

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo SorceDescription : conversions to and from old SML aterm format

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo SorceCopyright : (c) Klaus Luettich and Uni Bremen 2002-2004

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo SorceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo SorceMaintainer : Christian.Maeder@dfki.de

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo SorceStability : provisional

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo SorcePortability : non-portable (imports Logic.Grothendieck)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo SorceThis module exports functions, that can convert an sml-CATS ATerm

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce into the Haskell abstract syntax tree. So it contains all the

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce necessary instances of ATermConvertible and a heuristic function

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce that calculates the new lists of Pos out of Region tuples.

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce the templates for the instances are automatically derived by

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce DrIFT. But there were made many hand written changes.

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce todo:

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce - p_flag from pos-TERM is not considered jet!

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce-}

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnikmodule ATC.Sml_cats ( ATermConvertibleSML

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik , from_sml_ATermString

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik , read_sml_ATerm

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik ) where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport Data.List (isPrefixOf)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport qualified Data.Map as Map

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce-- better recompilation checking without 'import ATerm.Lib'

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport ATerm.AbstractSyntax

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport ATerm.ReadWrite

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jhaimport Common.Id

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jhaimport Common.AS_Annotation

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport Common.LibName

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport CASL.AS_Basic_CASL

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport CASL.Logic_CASL

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport Logic.Grothendieck

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport Syntax.AS_Structured

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport Syntax.AS_Architecture

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport Syntax.AS_Library

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce-- the following module provides the ability to parse the "unparsed-anno"

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceimport Text.ParserCombinators.Parsec (parse)

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jhaimport Common.AnnoParser (annotations, parseAnno)

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jhaimport Common.Lexer (skip)

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce-- |

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce-- like the chomp from Perl

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce-- but this chomp removes trailing newlines AND trailing spaces if any

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorcechomp :: String -> String

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorcechomp = reverse . chomp' . reverse

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where chomp' [] = []

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha chomp' xs@(x:xs') | x == '\n' || x == ' ' = chomp' xs'

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha | otherwise = xs

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceread_sml_ATerm :: FilePath -> IO LIB_DEFN

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceread_sml_ATerm fn = readFile fn >>= return . from_sml_ATermString

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce----- Convertible class for sml -----------------------------------------

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceclass ATermConvertibleSML t where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm :: ATermTable -> t

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATermList :: ATermTable -> [t]

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce -- default function ignores the annotation part

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATermList at =

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce case aterm of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ShAList ats _ -> map cnvrt ats

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "[a]" aterm

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where aterm = getATerm at

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce cnvrt i = from_sml_ShATerm (getATermByIndex1 i at)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorcefrom_sml_ATermString :: ATermConvertibleSML a => String -> a

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jhafrom_sml_ATermString s = (\ a -> from_sml_ShATerm a) (readATerm s)

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jhafrom_sml_ShATermError :: String -> ShATerm -> a

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorcefrom_sml_ShATermError t u =

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce error ("Cannot convert Sml-ShATerm to " ++ t ++ ": "++ err)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where err = case u of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ShAAppl s l _ -> "!ShAAppl " ++ s ++ "("

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ++ show (length l) ++ ")"

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ShAList _ _ -> "!ShAList"

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> "!ShAInt"

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce-- basic instances -----------------------------------------------

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance ATermConvertibleSML Bool where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att = case at of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ShAAppl "true" [] _ -> True

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ShAAppl "false" [] _ -> False

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "Bool" at

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where at = getATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce-- for Integer derive : ATermConvertibleSML hand written!

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance ATermConvertibleSML Integer where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att = case getATerm att of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ShAInt x _ -> x

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce at -> from_sml_ShATermError "Integer" at

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance ATermConvertibleSML Int where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att = integer2Int $ from_sml_ShATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance ATermConvertibleSML Char where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att = case at of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl s [] _) -> str2Char s

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "Char" at

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where at = getATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATermList att = case at of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl s [] _) -> read s

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "String" at

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where at = getATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance (Ord a, ATermConvertibleSML a, ATermConvertibleSML b)

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik => ATermConvertibleSML (Map.Map a b) where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att = Map.fromList $ from_sml_ShATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance ATermConvertibleSML a => ATermConvertibleSML [a] where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att = from_sml_ShATermList att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance (ATermConvertibleSML a,ATermConvertibleSML b)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce => ATermConvertibleSML (a,b) where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att = case at of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "" [x,y] _) -> (x',y')

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where x' = from_sml_ShATerm (getATermByIndex1 x att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce y' = from_sml_ShATerm (getATermByIndex1 y att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "(a,b)" at

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where at = getATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jhainstance (ATermConvertibleSML a, ATermConvertibleSML b, ATermConvertibleSML c)

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha => ATermConvertibleSML (a,b,c) where

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha from_sml_ShATerm att = case at of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "" [a,b,c] _) -> (a',b',c')

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where a' = from_sml_ShATerm (getATermByIndex1 a att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce b' = from_sml_ShATerm (getATermByIndex1 b att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce c' = from_sml_ShATerm (getATermByIndex1 c att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "(a,b,c)" at

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where at = getATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance (ATermConvertibleSML a, ATermConvertibleSML b,

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ATermConvertibleSML c, ATermConvertibleSML d)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce => ATermConvertibleSML (a,b,c,d) where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att = case at of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "" [a,b,c,d] _) -> (a',b',c',d')

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where a' = from_sml_ShATerm (getATermByIndex1 a att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce b' = from_sml_ShATerm (getATermByIndex1 b att)

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik c' = from_sml_ShATerm (getATermByIndex1 c att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce d' = from_sml_ShATerm (getATermByIndex1 d att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "(a,b,c)" at

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where at = getATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik----- instances of Id.hs ------------------------------------------------

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance ATermConvertibleSML Token where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att =

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce case aterm of

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik (ShAAppl "token" [ aa ] _) ->

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce mkSimpleId $ from_sml_ShATerm (getATermByIndex1 aa att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "place" [] _) -> mkSimpleId $ Common.Id.place

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "Token" aterm

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where aterm = getATerm att

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance ATermConvertibleSML Id where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att =

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce case aterm of

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik (ShAAppl "compound-id" [ aa,ab ] _) -> -- TOKEN_OR_MIXFIX,[ID]

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce let

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce aa' = from_sml_ATermTokenTup (getATermByIndex1 aa att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ab' = from_sml_ShATerm (getATermByIndex1 ab att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ac' = nullRange

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce in (Id aa' ab' ac')

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik (ShAAppl "simple-id" [ aa ] _) ->

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce let

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik aa' = from_sml_ATermTokenTup (getATermByIndex1 aa att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ab' = []

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ac' = nullRange

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce in (Id aa' ab' ac')

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce _ -> from_sml_ShATermError "Id" aterm

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce aterm = getATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorcefrom_sml_ATermTokenTup :: ATermTable -> [Token]

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnikfrom_sml_ATermTokenTup att =

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce case aterm of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "" [tops,_,_] _) ->

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha from_sml_ShATerm (getATermByIndex1 tops att)

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha _ -> from_sml_ShATermError "Token" aterm

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha where aterm = getATerm att

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce----- instances of AS_Annotation.hs -------------------------------------

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorceinstance ATermConvertibleSML Annotation where

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce from_sml_ShATerm att =

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce case aterm of

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "comment-line" [ aa ] _) ->

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik let

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce aa' = chomp $ from_sml_ShATerm (getATermByIndex1 aa att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ab' = pos_l

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce in (Unparsed_anno Comment_start (Line_anno aa') ab')

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "comment" [ aa ] _) ->

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce let

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce aa' = lines (from_sml_ShATerm (getATermByIndex1 aa att))

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ab' = pos_l

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce in (Unparsed_anno Comment_start (Group_anno aa') ab')

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "unparsed-anno" [ aa ] _) ->

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik parse_anno (pos_l)

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik (from_sml_ShATerm (getATermByIndex1 aa att))

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik (ShAAppl "annote-line" [ aa,ab ] _) ->

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik let

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik aa' = from_sml_ShATerm (getATermByIndex1 aa att)

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik ab' = from_sml_ShATerm (getATermByIndex1 ab att)

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik ac' = pos_l

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik in (Unparsed_anno (Annote_word aa') (Line_anno ab') ac')

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik (ShAAppl "annote-group" [ aa,ab ] _) ->

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik let

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik aa' = from_sml_ShATerm (getATermByIndex1 aa att)

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik ab' = from_sml_ShATerm (getATermByIndex1 ab att)

9acfb09f7969a69f58bd45c856b01700541853caLukas Slebodnik ac' = pos_l

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce in (Unparsed_anno (Annote_word aa') (Group_anno ab') ac')

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "display-anno" [ aa,ab ] _) ->

439f664bfb0cbed7e85ebd68647deed7414598d4Pallavi Jha let

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce aa' = from_sml_ShATerm (getATermByIndex1 aa att)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce ab' = parse_disp_anno aa' (pos_l)

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (chomp $ from_sml_ShATerm (getATermByIndex1 ab att))

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce in ab'

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce (ShAAppl "string-anno" [ aa,ab ] _) ->

918b2a5a91f1c551d48f4bffed2a28c36fdb4be1Simo Sorce let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (String_anno aa' ab' ac')

(ShAAppl "list-anno" [ aa,ab,ac ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

ad' = pos_l

in (List_anno aa' ab' ac' ad')

(ShAAppl "number-anno" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Number_anno aa' ab')

(ShAAppl "floating-anno" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Float_anno aa' ab' ac')

(ShAAppl "prec-anno" [ aa,ab,ac ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

ad' = pos_l

in (Prec_anno (if aa' then Lower else BothDirections)

ab' ac' ad')

(ShAAppl "lassoc-anno" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Assoc_anno ALeft aa' ab')

(ShAAppl "rassoc-anno" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Assoc_anno ARight aa' ab')

(ShAAppl "label-anno" [ aa ] _) ->

let

aa' = lines $ showId

(from_sml_ShATerm $ getATermByIndex1 aa att) ""

ab' = pos_l

in (Label aa' ab')

(ShAAppl "implies" [] _) ->

let

aa' = pos_l

in (Semantic_anno SA_implies aa')

(ShAAppl "definitional" [] _) ->

let

aa' = pos_l

in (Semantic_anno SA_def aa')

(ShAAppl "conservative" [] _) ->

let

aa' = pos_l

in (Semantic_anno SA_cons aa')

(ShAAppl "mono" [] _) ->

Semantic_anno SA_mono (pos_l)

_ -> from_sml_ShATermError "Annotation" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-ANNO" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,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 att =

case aterm of

(ShAAppl con as _) ->

(case con of

-- Basic Items (including sig_items)

"pos-BASIC-ITEMS" ->

case from_sml_ATermAnnotedBasic_Items att of

(bi, las) -> Annoted bi nullRange las []

-- L_.* constuctors from SML

"" -> Annoted (from_sml_ShATerm (getATermByIndex1

(head as)

att))

nullRange

[]

(toAnnoList (last as) att)

_ -> -- "No appropiate constructor for Annoted found"

Annoted (from_sml_ShATerm att)

nullRange

[]

[]

)

_ -> from_sml_ShATermError "Annoted a" aterm

where

aterm = getATerm 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 att =

if isSig_items then

((from_sml_ShATerm att),[])

else ((from_sml_ShATerm att),annoList)

where isSig_items =

case aterm of

(ShAAppl _ as _)-> -- pos-BASIC-ITEMS

case getATerm $ getATermByIndex1 (last as) att of

(ShAAppl "sig-items" _ _) -> True

_ -> False

_ -> from_sml_ShATermError "{SIG,BASIC}_items" aterm

aterm = getATerm att

annoList = case getATerm att of

(ShAAppl _ as _) -> getAnnoList (last as) att

_ -> 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 ai att = case at of

ShAAppl c as _ | isPrefixOf "pos-" c ->

getAnnoList (last as) att

ShAAppl _ as _ -> toAnnoList (last as) att

_ -> error "wrong storage or missed 'pos-' contructor"

where at = getATerm (getATermByIndex1 ai att)

toAnnoList :: Int -> ATermTable -> [Annotation]

toAnnoList ai att = from_sml_ShATerm $ getATermByIndex1 ai att

parse_anno :: Range -> String -> Annotation

parse_anno _pos_l inp =

case parse (skip >> annotations) "" inp of

Right [x] -> x

_ -> error ("something strange happend to \"" ++

inp ++ "\" during ATerm Conversion")

parse_disp_anno :: Id -> Range -> String -> Annotation

parse_disp_anno i pos_l inp =

case parseAnno (Unparsed_anno (Annote_word "display")

(Group_anno [inp']) pos_l) pos of

Left err -> error $ "internal parse error at " ++ show err

Right x -> x

where

pos = case rangeToList pos_l of

[] -> newPos "" 0 0

h : _ -> h

inp' = showId i $ ' ' : s_inp

s_inp = case reverse inp of

rin | "%)" `isPrefixOf` rin -> reverse $ drop 2 rin

| otherwise -> inp

----- instances of AS_Basic_CASL.hs -------------------------------------

instance ATermConvertibleSML (BASIC_SPEC a b c) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "basic-spec" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (CASL.AS_Basic_CASL.Basic_spec aa')

_ -> from_sml_ShATermError "BASIC_SPEC" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-BASIC-SPEC" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML (BASIC_ITEMS a b c) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "sig-items" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (Sig_items aa')

(ShAAppl "free-datatype" [ aa,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Free_datatype NonEmptySorts aa' ab')

(ShAAppl "sort-gen" [ aa,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Sort_gen aa' ab')

(ShAAppl "var-items" [ aa,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Var_items aa' ab')

(ShAAppl "local-var-axioms" [ aa,ab,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Local_var_axioms aa' ab' ac')

(ShAAppl "axiom-items" [ aa,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Axiom_items aa' ab')

_ -> from_sml_ShATermError "BASIC_ITEMS" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-BASIC-ITEMS" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML (SIG_ITEMS a b) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "sort-items" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

as = from_sml_ShATerm (getATermByIndex1 ab att)

aa'' = (addLAnnoList as $ head aa'):(tail aa')

ab' = pos_l

in (Sort_items NonEmptySorts aa'' ab')

(ShAAppl "op-items" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

as = from_sml_ShATerm (getATermByIndex1 ab att)

aa'' = (addLAnnoList as $ head aa'):(tail aa')

ab' = pos_l

in (Op_items aa'' ab')

(ShAAppl "pred-items" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

as = from_sml_ShATerm (getATermByIndex1 ab att)

aa'' = (addLAnnoList as $ head aa'):(tail aa')

ab' = pos_l

in (Pred_items aa'' ab')

(ShAAppl "datatype-items" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

as = from_sml_ShATerm (getATermByIndex1 ab att)

aa'' = (addLAnnoList as $ head aa'):(tail aa')

ab' = pos_l

in (Datatype_items NonEmptySorts aa'' ab')

_ -> from_sml_ShATermError "SIG_ITEMS" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-SIG-ITEMS" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML (SORT_ITEM a) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "sort-decl" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Sort_decl aa' ab')

(ShAAppl "subsort-decl" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Subsort_decl aa' ab' ac')

(ShAAppl "subsort-defn" [ aa,ab,ac,ad,ae ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ATermSIMPLE_ID (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

ad' = from_sml_ShATerm (getATermByIndex1 ad att)

as = toAnnoList ae att

ad''= addRAnnoList as ad'

ae' = pos_l

in (Subsort_defn aa' ab' ac' ad'' ae')

(ShAAppl "iso-decl" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Iso_decl aa' ab')

_ -> from_sml_ShATermError "SORT_ITEM" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-SORT-ITEM" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML (OP_ITEM a) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "op-decl" [ aa,ab,ac ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

ad' = pos_l

in (Op_decl aa' ab' ac' ad')

(ShAAppl "op-defn" [ aa,ab,ac,ad ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

as = from_sml_ShATerm (getATermByIndex1 ad att)

ac''= addRAnnoList as ac'

ad' = pos_l

in (Op_defn aa' ab' ac'' ad')

_ -> from_sml_ShATermError "OP_ITEM" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-OP-ITEM" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML OP_TYPE where

from_sml_ShATerm att =

case aterm of

(ShAAppl "total-op-type" [ aa,ab ] _) ->

let

(aa',ps) = from_sml_ATermSORTS (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = insertPos ps $ pos_l

in (Op_type Total aa' ab' ac')

(ShAAppl "partial-op-type" [ aa,ab ] _) ->

let

(aa',ps) = from_sml_ATermSORTS (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = insertPos ps $ pos_l

in (Op_type Partial aa' ab' ac')

_ -> from_sml_ShATermError "OP_TYPE" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-OP-TYPE" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

---- a helper for the SML-datatype SORTS -------------------------------

from_sml_ATermSORTS :: ATermTable -> ([SORT],Range)

from_sml_ATermSORTS att =

case aterm of

(ShAAppl "sorts" [ aa ] _) ->

(from_sml_ShATerm (getATermByIndex1 aa att),pos_l)

_ -> from_sml_ShATermError "([SORT],Range)" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-SORTS" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML OP_HEAD where

from_sml_ShATerm att =

case aterm of

(ShAAppl "total-op-head" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Op_head Total aa' ab' ac')

(ShAAppl "partial-op-head" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Op_head Partial aa' ab' ac')

_ -> from_sml_ShATermError "OP_HEAD" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-OP-HEAD" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML ARG_DECL where

from_sml_ShATerm att =

case aterm of

-- (ShAAppl "arg-decl" [ ShAAppl "" [aa,ab] _ ] _) ->

(ShAAppl "" [aa,ab] _) ->

let

aa' = from_sml_ATermVARs (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Arg_decl aa' ab' ac')

_ -> from_sml_ShATermError "ARG_DECL" aterm

where

aterm = case getATerm att' of

ShAAppl "arg-decl" [i] _ ->

getATerm $ getATermByIndex1 i att

x -> from_sml_ShATermError "arg-decl" x

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-ARG-DECL" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML (OP_ATTR a) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "associative" [ ] _) ->

let

in Assoc_op_attr

(ShAAppl "commutative" [ ] _) ->

let

in Comm_op_attr

(ShAAppl "idempotent" [ ] _) ->

let

in Idem_op_attr

(ShAAppl "unit-op-attr" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (Unit_op_attr aa')

_ -> from_sml_ShATermError "OP_ATTR" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-OP-ATTR" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML (PRED_ITEM a) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "pred-decl" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Pred_decl aa' ab' ac')

(ShAAppl "pred-defn" [ aa,ab,ac,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

ad' = pos_l

in (Pred_defn aa' ab' ac' ad')

_ -> from_sml_ShATermError "PRED_ITEM" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-PRED-ITEM" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML PRED_TYPE where

from_sml_ShATerm att =

case aterm of

(ShAAppl "pred-type" [ aa ] _) ->

let

(aa',ps) = from_sml_ATermSORTS (getATermByIndex1 aa att)

ab' = insertPos ps $ pos_l

in (Pred_type aa' ab')

_ -> from_sml_ShATermError "PRED_TYPE" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-PRED-TYPE" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML PRED_HEAD where

from_sml_ShATerm att =

case aterm of

(ShAAppl "pred-head" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Pred_head aa' ab')

_ -> from_sml_ShATermError "PRED_HEAD" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-PRED-HEAD" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML DATATYPE_DECL where

from_sml_ShATerm att =

case aterm of

(ShAAppl "datatype-decl" [ aa,ab,ac ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

as = from_sml_ShATerm (getATermByIndex1 ac att)

ab''= (addLAnnoList as $ head ab'):(tail ab')

ac' = pos_l

in (Datatype_decl aa' ab'' ac')

_ -> from_sml_ShATermError "DATATYPE_DECL" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-DATATYPE-DECL" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML ALTERNATIVE where

from_sml_ShATerm att =

case aterm of

(ShAAppl "total-construct" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Alt_construct Total aa' ab' ac')

(ShAAppl "partial-construct" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Alt_construct Partial aa' ab' ac')

(ShAAppl "subsort" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Subsorts aa' ab')

_ -> from_sml_ShATermError "ALTERNATIVE" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-ALTERNATIVE" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML COMPONENTS where

from_sml_ShATerm att =

case aterm of

(ShAAppl "total-select" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Cons_select Total aa' ab' ac')

(ShAAppl "partial-select" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Cons_select Partial aa' ab' ac')

(ShAAppl "sort-component" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (Sort aa')

_ -> from_sml_ShATermError "COMPONENTS" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-COMPONENTS" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML VAR_DECL where

from_sml_ShATerm att =

case aterm of

(ShAAppl "" [ aa,ab ] _) ->

let

aa' = from_sml_ATermVARs (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

in (Var_decl aa' ab' nullRange)

_ -> from_sml_ShATermError "VAR_DECL" aterm

where

aterm = getATerm att

instance ATermConvertibleSML (FORMULA a) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "quantification" [ aa,ab,ac ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

pq = getPos (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

ad' = insertPos pq $ pos_l

in (Quantification aa' ab' ac' ad')

(ShAAppl "conjunction" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Conjunction aa' ab')

(ShAAppl "disjunction" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Disjunction aa' ab')

(ShAAppl "implication" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Implication aa' ab' True ac')

(ShAAppl "equivalence" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Equivalence aa' ab' ac')

(ShAAppl "negation" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Negation aa' ab')

-- the following things are from SML-type ATOM

(ShAAppl "atom" [i] _) ->

case getATerm (getATermByIndex1 i att') of

(ShAAppl "ttrue" [] _) ->

let

aa' = pos_l

in (True_atom aa')

(ShAAppl "ffalse" [] _) ->

let

aa' = pos_l

in (False_atom aa')

(ShAAppl "predication" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

(ab',ps) = from_sml_ATermTERMS (getATermByIndex1 ab att)

ac' = insertPos ps $ pos_l

in (Predication aa' ab' ac')

(ShAAppl "definedness" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Definedness aa' ab')

(ShAAppl "existl-equation" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Existl_equation aa' ab' ac')

(ShAAppl "strong-equation" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Strong_equation aa' ab' ac')

(ShAAppl "membership" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Membership aa' ab' ac')

_ -> from_sml_ShATermError "FORMULA" aterm

_ -> from_sml_ShATermError "FORMULA" aterm

where

aterm = getATerm att'

(pos_l,_g_flag,att') = skipPosFlag "pos-FORMULA" att

---- a helper for the SML-datatype TERMS -------------------------------

from_sml_ATermTERMS :: ATermTable -> ([TERM a],Range)

from_sml_ATermTERMS att =

case aterm of

(ShAAppl "terms" [ aa ] _) ->

(from_sml_ShATerm (getATermByIndex1 aa att),pos_l)

_ -> from_sml_ShATermError "([TERM],Range)" aterm

where aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-TERMS" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

---- a helper for SIMPLE_IDs --------------------------------------------

from_sml_ATermSIMPLE_ID :: ATermTable -> SIMPLE_ID

from_sml_ATermSIMPLE_ID att =

case aterm of

(ShAAppl "" [ si, _ ] _) -> -- snd element is 'None'

-- (CASL.grm:((WORDS,None)))

let s = from_sml_ShATerm $ getATermByIndex1 si att

in mkSimpleId s

_ -> from_sml_ShATermError "SIMPLE_ID" aterm

where aterm = getATerm att

---- a helper for [VAR] -------------------------------------------------

from_sml_ATermVARs :: ATermTable -> [VAR]

from_sml_ATermVARs att = map from_sml_ATermSIMPLE_ID att_list

where att_list = case getATerm att of

ShAList l _-> map getAtt l

_ -> from_sml_ShATermError "[VAR]" $ getATerm att

getAtt ai = getATermByIndex1 ai att

instance ATermConvertibleSML QUANTIFIER where

from_sml_ShATerm att =

case aterm of

(ShAAppl "forall" [ ] _) ->

let

in Universal

(ShAAppl "exists" [ ] _) ->

let

in Existential

(ShAAppl "exists-uniquely" [ ] _) ->

let

in Unique_existential

_ -> from_sml_ShATermError "QUANTIFIER" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-QUANTIFIER" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML PRED_SYMB where

from_sml_ShATerm att =

case aterm of

(ShAAppl "pred-symb" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in case getATerm $ getATermByIndex1 ab att of

ShAAppl "None" [] _ ->

(Pred_name aa')

ShAAppl "Some" [ aab ] _ ->

let aab' = from_sml_ShATerm (getATermByIndex1 aab att)

ac' = pos_l

in (Qual_pred_name aa' aab' ac')

_ -> from_sml_ShATermError "Option" aterm

_ -> from_sml_ShATermError "PRED_SYMB" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-PRED-SYMB" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML (TERM a) where

from_sml_ShATerm att =

case aterm of

(ShAAppl "var-or-const" [ aa ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

in varOrConst aa'

(ShAAppl "qual-var" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Qual_var aa' ab' ac')

(ShAAppl "application" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

(ab',ps) = from_sml_ATermTERMS (getATermByIndex1 ab att)

ac' = insertPos ps $ pos_l

in (Application aa' ab' ac')

(ShAAppl "sorted-term" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Sorted_term aa' ab' ac')

(ShAAppl "cast" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Cast aa' ab' ac')

(ShAAppl "conditional" [ aa,ab,ac ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

ad' = pos_l

in (Conditional aa' ab' ac' ad')

_ -> from_sml_ShATermError "TERM" aterm

where

aterm = getATerm att'

(pos_l,_p_flag,att') = skipPosFlag "pos-TERM" att

instance ATermConvertibleSML OP_SYMB where

from_sml_ShATerm att =

case aterm of

(ShAAppl "op-symb" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in case getATerm $ getATermByIndex1 ab att of

ShAAppl "None" [] _ ->

(Op_name aa')

ShAAppl "Some" [ aab ] _ ->

let aab' = from_sml_ShATerm (getATermByIndex1 aab att)

ac' = pos_l

in (Qual_op_name aa' aab' ac')

_ -> from_sml_ShATermError "Option" aterm

_ -> from_sml_ShATermError "OP_SYMB" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-OP-SYMB" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML SYMB_ITEMS where

from_sml_ShATerm att =

case aterm of

(ShAAppl "symb-items" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Symb_items aa' ab' ac')

_ -> from_sml_ShATermError "SYMB_ITEMS" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-SYMB-ITEMS" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML SYMB_MAP_ITEMS where

from_sml_ShATerm att =

case aterm of

(ShAAppl "symb-map-items" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Symb_map_items aa' ab' ac')

_ -> from_sml_ShATermError "SYMB_MAP_ITEMS" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-SYMB-MAP-ITEMS" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML SYMB_KIND where

from_sml_ShATerm att =

case aterm of

(ShAAppl "implicitk" [ ] _) ->

Implicit

(ShAAppl "sortsk" [ ] _) ->

Sorts_kind

(ShAAppl "opsk" [ ] _) ->

Ops_kind

(ShAAppl "predsk" [ ] _) ->

Preds_kind

_ -> from_sml_ShATermError "SYMB_KIND" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-SYMB-KIND" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML SYMB where

from_sml_ShATerm att =

case aterm of

(ShAAppl "symb-id" [ aa ] _) ->

let

i = from_sml_ShATerm (getATermByIndex1 aa att)

aa' = setFstPos (pos_l) i

in (Symb_id aa')

(ShAAppl "qual-id" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Qual_id aa' ab' ac')

_ -> from_sml_ShATermError "SYMB" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-SYMB" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML TYPE where

from_sml_ShATerm att =

case aterm of

(ShAAppl "op-symb-type" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (O_type aa')

(ShAAppl "pred-symb-type" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (P_type aa')

_ -> from_sml_ShATermError "TYPE" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-TYPE" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML SYMB_OR_MAP where

from_sml_ShATerm att =

case aterm of

(ShAAppl "symb" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (Symb aa')

(ShAAppl "symb-or-map" [ aa ] _) ->

let

(aa',ab') = from_sml_ATermSYMB_MAP (getATermByIndex1 aa att)

ac' = pos_l

in (Symb_map aa' ab' ac')

_ -> from_sml_ShATermError "SYMB_OR_MAP" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-SYMB-OR-MAP" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

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

from_sml_ATermSYMB_MAP :: ATermTable -> (SYMB,SYMB)

from_sml_ATermSYMB_MAP att =

case aterm of

(ShAAppl "symb-map" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

in (aa',ab')

_ -> from_sml_ShATermError "(SYMB,SYMB)" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-SYMB-MAP" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

----- instances of AS_Structured.hs -------------------------------------

instance ATermConvertibleSML SPEC where

from_sml_ShATerm att =

case aterm of

(ShAAppl "basic" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

aa'' = G_basic_spec CASL aa'

in group (Syntax.AS_Structured.Basic_spec aa''

nullRange) group_flag

(ShAAppl "translation" [ aa,ab,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

in group (Translation aa' ab') group_flag

(ShAAppl "reduction" [ aa,ab,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

in group (Reduction aa' ab') group_flag

(ShAAppl "union-spec" [ aa ] _) ->

let

aa' :: [(Annoted SPEC,[Annotation])]

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in group (Union (toAnnotedList aa') ab') group_flag

(ShAAppl "extension" [ aa ] _) ->

let

aa' :: [(Annoted SPEC,[Annotation])]

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in group (Extension (toAnnotedList aa') ab') group_flag

(ShAAppl "free-spec" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

aa''= addLAnnoList (toAnnoList ab att) aa'

ab' = pos_l

in group (Free_spec aa'' ab') group_flag

(ShAAppl "local-spec" [ aa,ab,ac,ad ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

sp1 = addLAnnoList (toAnnoList ab att) aa'

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

sp2 = addLAnnoList (toAnnoList ad att) ac'

in group (Local_spec sp1 sp2 pos_l) group_flag

(ShAAppl "closed-spec" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

aa''= addLAnnoList (toAnnoList ab att) aa'

ab' = pos_l

in group (Closed_spec aa'' ab') group_flag

(ShAAppl "spec-inst" [ aa,ab ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

in (Spec_inst aa' ab' nullRange)

_ -> from_sml_ShATermError "SPEC" aterm

where

aterm = getATerm att'

group s gf = if gf then (Group s' pos_l) else s

where s' = Annoted s nullRange [] []

(pos_l,group_flag,att') = skipPosFlag "pos-SPEC" att

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

toAnnotedList :: [(Annoted a,[Annotation])] -> [Annoted a]

toAnnotedList xs = map merge xs

where merge (ai,as) = ai { l_annos = (l_annos ai) ++ as}

instance ATermConvertibleSML RENAMING where

from_sml_ShATerm att =

case aterm of

(ShAAppl "renaming" [ aa ] _) ->

case from_sml_ShATerm (getATermByIndex1 aa att) of

aa' -> let

aa''= if null aa' then []

else [G_symb_map $ G_symb_map_items_list CASL aa']

ab' = pos_l

in (Renaming aa'' ab')

_ -> from_sml_ShATermError "RENAMING" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-RENAMING" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML RESTRICTION where

from_sml_ShATerm att =

case aterm of

(ShAAppl "hide" [ aa ] _) ->

let

aa''= case from_sml_ShATerm (getATermByIndex1 aa att) of

[] -> []

aa' -> [G_symb_list $ G_symb_items_list CASL aa']

ab' = pos_l

in (Hidden aa'' ab')

(ShAAppl "reveal" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

aa''= G_symb_map_items_list CASL aa'

ab' = pos_l

in (Revealed aa'' ab')

_ -> from_sml_ShATermError "RESTRICTION" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-RESTRICTION" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

{- !!! This will be done by the instance of LIB_ITEM !!!

instance ATermConvertibleSML SPEC_DEFN where

-}

instance ATermConvertibleSML GENERICITY where

from_sml_ShATerm att =

case aterm of

(ShAAppl "genericity" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Genericity aa' ab' ac')

_ -> from_sml_ShATermError "GENERICITY" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-GENERICITY" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML PARAMS where

from_sml_ShATerm att =

case aterm of

(ShAAppl "params" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (Params aa')

_ -> from_sml_ShATermError "PARAMS" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-PARAMS" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML IMPORTED where

from_sml_ShATerm att =

case aterm of

(ShAAppl "imports" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (Imported aa')

_ -> from_sml_ShATermError "IMPORTED" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-IMPORTS" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML FIT_ARG where

from_sml_ShATerm att =

case aterm of

(ShAAppl "fit-spec" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab''= case from_sml_ShATerm (getATermByIndex1 ab att) of

[] -> []

ab' -> [G_symb_map $ G_symb_map_items_list CASL ab']

ac' = pos_l

in (Fit_spec aa' ab'' ac')

(ShAAppl "fit-view" [ aa,ab ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Fit_view aa' ab' ac')

_ -> from_sml_ShATermError "FIT_ARG" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-FIT-ARG" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

{- !!! This conversion is covered by the instance of LIB_ITEM !!!

instance ATermConvertibleSML VIEW_DEFN where

-}

instance ATermConvertibleSML VIEW_TYPE where

from_sml_ShATerm att =

case aterm of

(ShAAppl "view-type" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (View_type aa' ab' ac')

_ -> from_sml_ShATermError "VIEW_TYPE" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-VIEW-TYPE" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,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 att =

case aterm of

(ShAAppl "basic-arch-spec" [ aa,ab,ac ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ATermRESULT_UNIT (getATermByIndex1 ab att)

as = toAnnoList ac att

aa''= (addLAnnoList as $ head aa'):tail aa'

ac' = pos_l

in (Basic_arch_spec aa'' ab' ac')

(ShAAppl "named-arch-spec" [ aa ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

in (Arch_spec_name aa')

_ -> from_sml_ShATermError "ARCH_SPEC" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-ARCH-SPEC" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

from_sml_ATermRESULT_UNIT :: ATermTable -> (Annoted UNIT_EXPRESSION)

from_sml_ATermRESULT_UNIT att =

case aterm of

(ShAAppl "result-unit" [ aa,ab ] _) ->

let

-- aa' :: UNIT_EXPRESSION

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

as = toAnnoList ab att

in (Annoted aa' nullRange as [])

_ -> from_sml_ShATermError "RESULT-UNIT" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-RESULT-UNIT" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML UNIT_REF where

from_sml_ShATerm att =

case aterm of

(ShAAppl "unit-decl-case" [ udl ] _) ->

let att1 = getATermByIndex1 udl att

(ps,att2) = case getATerm att1 of

(ShAAppl "pos-UNIT-DECL" [reg_i,item_i] _) ->

(posFromRegion reg_i att,

getATermByIndex1 item_i att1)

_ -> (nullRange,att1)

aterm2 = getATerm att2

in case aterm2 of

ShAAppl "unit-decl" [aa,ab,_] _ ->

let aa' = from_sml_ATermSIMPLE_ID $

getATermByIndex1 aa att

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ad' = ps

in (Unit_ref aa' ab' ad')

_ -> from_sml_ShATermError "UNIT_DECL" aterm2

_ -> from_sml_ShATermError "UNIT-DECL-DEFN" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-UNIT-DECL-DEFN" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML UNIT_DECL_DEFN where

from_sml_ShATerm att =

case aterm of

(ShAAppl "unit-decl-case" [ udl ] _) ->

let att1 = getATermByIndex1 udl att

(ps,att2) = case getATerm att1 of

(ShAAppl "pos-UNIT-DECL" [reg_i,item_i] _) ->

(posFromRegion reg_i att,

getATermByIndex1 item_i att1)

_ -> (nullRange,att1)

aterm2 = getATerm att2

in case aterm2 of

ShAAppl "unit-decl" [aa,ab,ac] _ ->

let aa' = from_sml_ATermSIMPLE_ID $ getATermByIndex1 aa att

ab' = from_sml_ShATerm $ getATermByIndex1 ab att

ac' = from_sml_ATermUNIT_IMPORTS $

getATermByIndex1 ac att

ad' = ps

in Unit_decl aa' ab' ac' ad'

_ -> from_sml_ShATermError "UNIT_DECL" aterm2

(ShAAppl "unit-defn-case" [ udn ] _) ->

from_sml_ATermUNIT_DEFN $ getATermByIndex1 udn att

(ShAAppl "pos-UNIT-DEFN" _ _) ->

from_sml_ATermUNIT_DEFN att

(ShAAppl "unit-defn" _ _) ->

from_sml_ATermUNIT_DEFN att

_ -> from_sml_ShATermError "UNIT-DECL-DEFN" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-UNIT-DECL-DEFN" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

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

from_sml_ATermUNIT_IMPORTS :: ATermTable -> [Annoted UNIT_TERM]

from_sml_ATermUNIT_IMPORTS att =

case aterm of

(ShAAppl "unit-imports" [ aa ] _) ->

from_sml_ShATerm $ getATermByIndex1 aa att

_ -> from_sml_ShATermError "UNIT_IMPORTS" aterm

where aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-UNIT-IMPORTS" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

from_sml_ATermUNIT_DEFN :: ATermTable -> UNIT_DECL_DEFN

from_sml_ATermUNIT_DEFN att =

case aterm of

ShAAppl "unit-defn" [aa,ab] _ ->

let aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = ps

in (Unit_defn aa' ab' ac')

_ -> from_sml_ShATermError "UNIT_DEFN" aterm

where aterm = getATerm att'

(ps,att') =

case getATerm att of

(ShAAppl "pos-UNIT-DEFN" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,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 att =

case aterm of

(ShAAppl "unit-type-case" [ aa ] _) ->

let

(aa',ab') = from_sml_ATermUNIT_TYPE $ getATermByIndex1 aa att

ac' = pos_l

in (Unit_type aa' ab' ac')

(ShAAppl "spec-name-case" [ aa ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

in (Spec_name aa')

(ShAAppl "closed" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Closed_unit_spec aa' ab')

_ -> from_sml_ShATermError "UNIT_SPEC" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-UNIT-SPEC" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML REF_SPEC where

from_sml_ShATerm att =

case aterm of

(ShAAppl "unit-type-case" [ aa ] _) ->

let

(aa',ab') = from_sml_ATermUNIT_TYPE $ getATermByIndex1 aa att

ac' = pos_l

in Unit_spec $ Unit_type aa' ab' ac'

(ShAAppl "spec-name-case" [ aa ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

in (Unit_spec $ Spec_name aa')

(ShAAppl "arch-spec-case" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ps = toAnnoList ab att

aa'' = addLAnnoList ps aa'

ab' = pos_l

aa''' = case aa'' of

(Annoted (Basic_arch_spec _ _ _) _ _ _) ->

Annoted (Group_arch_spec aa'' ab') nullRange [][]

_ -> aa''

in (Arch_unit_spec aa''' ab')

(ShAAppl "closed" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (Unit_spec $ Closed_unit_spec aa' ab')

_ -> from_sml_ShATermError "UNIT_SPEC" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-UNIT-SPEC" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

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

from_sml_ATermUNIT_TYPE :: ATermTable -> ([Annoted SPEC],(Annoted SPEC))

from_sml_ATermUNIT_TYPE att =

case aterm of

(ShAAppl "unit-type" [ aa,ab ] _) ->

(from_sml_ShATerm $ getATermByIndex1 aa att,

from_sml_ShATerm $ getATermByIndex1 ab att)

_ -> from_sml_ShATermError "UNIT_TYPE" aterm

where aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-UNIT-TYPE" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML UNIT_EXPRESSION where

from_sml_ShATerm att =

case aterm of

(ShAAppl "unit-expression" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Unit_expression aa' ab' ac')

_ -> from_sml_ShATermError "UNIT_EXPRESSION" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-UNIT-EXPRESSION" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML UNIT_BINDING where

from_sml_ShATerm att =

case aterm of

(ShAAppl "unit-binding" [ aa,ab ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Unit_binding aa' ab' ac')

_ -> from_sml_ShATermError "UNIT_BINDING" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-UNIT-BINDING" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML UNIT_TERM where

from_sml_ShATerm att =

case aterm of

(ShAAppl "unit-reduction" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

in group (Unit_reduction aa' ab') group_flag

(ShAAppl "unit-translation" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

in group (Unit_translation aa' ab') group_flag

(ShAAppl "amalgamation" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in group (Amalgamation aa' ab') group_flag

(ShAAppl "local-unit" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in group (Local_unit aa' ab' ac') group_flag

(ShAAppl "unit-appl" [ aa,ab ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in group (Unit_appl aa' ab' ac') group_flag

_ -> from_sml_ShATermError "UNIT_TERM" aterm

where

aterm = getATerm att'

group ut gf = if gf then (Group_unit_term ut' pos_l) else ut

where ut' = Annoted ut nullRange [] []

(pos_l,group_flag,att') = skipPosFlag "pos-UNIT-TERM" att

instance ATermConvertibleSML FIT_ARG_UNIT where

from_sml_ShATerm att =

case aterm of

(ShAAppl "fit-arg-unit" [ aa,ab ] _) ->

case from_sml_ShATerm (getATermByIndex1 aa att) of

aa' -> case from_sml_ShATerm (getATermByIndex1 ab att) of

ab' -> Fit_arg_unit aa' (if null ab' then [] else

[G_symb_map $ G_symb_map_items_list CASL ab']) $ pos_l

_ -> from_sml_ShATermError "FIT_ARG_UNIT" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-FIT-ARG-UNIT" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

----- instances of AS_LIbrary.hs ----------------------------------------

instance ATermConvertibleSML LIB_DEFN where

from_sml_ShATerm att =

case aterm of

(ShAAppl "lib-defn" [ aa,ab,ad ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

ad' = from_sml_ShATerm (getATermByIndex1 ad att)

in (Lib_defn aa' ab' ac' ad')

_ -> from_sml_ShATermError "LIB_DEFN" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-LIB-DEFN" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML LIB_ITEM where

from_sml_ShATerm att =

case aterm of

(ShAAppl "spec-defn" [ aa,ab,ac,ad ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

as = toAnnoList ad att

ac''= addLAnnoList as ac'

ad' = pos_l

in Syntax.AS_Library.Spec_defn aa' ab' ac'' ad'

(ShAAppl "view-defn" [ aa,ab,ac,ad,_ ] _) ->

let -- the annotation list is lost !!!!

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = from_sml_ShATerm (getATermByIndex1 ac att)

ad''= case from_sml_ShATerm (getATermByIndex1 ad att) of

[] -> []

ad' -> [G_symb_map $ G_symb_map_items_list CASL ad']

ae' = pos_l

in (Syntax.AS_Library.View_defn aa' ab' ac' ad'' ae')

(ShAAppl "arch-spec-defn" [ aa,ab,_ ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Syntax.AS_Library.Arch_spec_defn aa' ab' ac')

(ShAAppl "unit-spec-defn" [ aa,ab,_ ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Syntax.AS_Library.Unit_spec_defn aa' ab' ac')

(ShAAppl "download-items" [ aa,ab,_ ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

ac' = pos_l

in (Syntax.AS_Library.Download_items aa' ab' ac')

_ -> from_sml_ShATermError "LIB_ITEM" aterm

where

aterm = getATerm att'

(pos_l,att') = skipPos "pos-LIB-ITEM" att

---- helpers to skip nested "pos-"-constructors -----------------------

skipPos :: String -> ATermTable -> (Range,ATermTable)

skipPos mcon at =

case getATerm at of

ShAAppl con [reg_i,item_i] _ | mcon == con ->

if pCon then skipPos mcon at'

else (posFromRegion (reg_i) at, at')

where pCon = case getATerm at' of

ShAAppl con' _ _ | mcon == con' -> True

_ -> False

at' = getATermByIndex1 item_i at

_ -> (nullRange,at)

skipPosFlag :: String -> ATermTable -> (Range,Bool,ATermTable)

skipPosFlag mcon att =

case getATerm att of

ShAAppl con [reg_i,b_i,item_i] _ | mcon == con ->

if pCon then let (_r_pos_l,r_b,r_at') = skipPosFlag mcon at'

in (pos_l,r_b || b,r_at')

else (pos_l,b,at')

where pCon = case getATerm at' of

ShAAppl con' _ _ | mcon == con' -> True

_ -> False

at' = getATermByIndex1 item_i att

pos_l = posFromRegion reg_i att

b = from_sml_ShATerm $ getATermByIndex1 b_i att

_ -> (nullRange,False,att)

instance ATermConvertibleSML ITEM_NAME_OR_MAP where

from_sml_ShATerm att =

case aterm of

(ShAAppl "item-name" [ aa ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

in (Item_name aa')

(ShAAppl "item-name-map" [ aa,ab ] _) ->

let

aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)

ab' = from_sml_ATermSIMPLE_ID (getATermByIndex1 ab att)

ac' = pos_l

in (Item_name_map aa' ab' ac')

_ -> from_sml_ShATermError "ITEM_NAME_OR_MAP" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-ITEM-NAME-OR-MAP" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML LibName where

from_sml_ShATerm att =

case aterm of

(ShAAppl "versioned-lib" [ aa,ab ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = from_sml_ShATerm (getATermByIndex1 ab att)

in (LibName aa' $ Just ab')

(ShAAppl "lib" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

in (LibName aa' Nothing)

_ -> from_sml_ShATermError "LibName" aterm

where

aterm = getATerm att'

att' =

case getATerm att of

(ShAAppl "pos-LIB-NAME" [_,item_i] _) ->

getATermByIndex1 item_i att

_ -> att

instance ATermConvertibleSML LibId where

from_sml_ShATerm att =

case aterm of

(ShAAppl "url" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (DirectLink aa' ab')

(ShAAppl "path-name" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (IndirectLink aa' ab' "" noTime)

_ -> from_sml_ShATermError "LibName" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-LIB-ID" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

instance ATermConvertibleSML VersionNumber where

from_sml_ShATerm att =

case aterm of

(ShAAppl "version" [ aa ] _) ->

let

aa' = from_sml_ShATerm (getATermByIndex1 aa att)

ab' = pos_l

in (VersionNumber aa' ab')

_ -> from_sml_ShATermError "VersionNumber" aterm

where

aterm = getATerm att'

(pos_l,att') =

case getATerm att of

(ShAAppl "pos-VERSION" [reg_i,item_i] _) ->

(posFromRegion reg_i att,getATermByIndex1 item_i att)

_ -> (nullRange,att)

-------------------------------------------------------------------------

-- some helpers for Annoted things --------------------------------------

addLAnnoList :: [Annotation] -> Annoted a -> Annoted a

addLAnnoList as ani = ani {l_annos = as ++ (l_annos ani) }

addRAnnoList :: [Annotation] -> Annoted a -> Annoted a

addRAnnoList as ani = ani {r_annos = (r_annos ani) ++ as }

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

posFromRegion :: Int -> ATermTable -> Range

posFromRegion reg at = Range $ map ( \ (l, c) -> newPos "" l c )

$ from_sml_ATerm_reg reg at

getPos :: ATermTable -> Range

getPos att = case getATerm att of

ShAAppl _ (x:_) _ -> posFromRegion x att

_ -> nullRange

-- converts an aterm region information to Range

from_sml_ATerm_reg :: Int -> ATermTable -> [(Int,Int)]

from_sml_ATerm_reg reg_i at = [fst r,snd r]

where r :: ((Int,Int),(Int,Int)) -- Id.hs Region

r = from_sml_ShATerm r_at

r_at = getATermByIndex1 reg_i at

insertIM, insertPosAux :: [a] -> [a] -> [a]

insertIM ips ops | even $ length ops = let hl = (length ops) `div` 2

(fp,lp) = splitAt hl ops

in fp ++ ips ++ lp

| otherwise = error

"wrong call: length of snd list must be even"

insertPosAux = insertIM

insertPos :: Range -> Range -> Range

insertPos (Range l1) (Range l2) = Range (insertPosAux l1 l2)

setFstPos :: Range -> Id -> Id

setFstPos (Range (p:_)) i = case i of

Id tops ids pos_l ->

Id (setFstPos' tops) ids pos_l

where setFstPos' tops | null tops = []

| otherwise = (ftop):(tail tops)

where ftop = (head tops) { tokPos = Range [p] }

setFstPos _ _ = error "wrong call: setFstPos"