Sml_cats.hs revision 3d3889e0cefcdce9b3f43c53aaa201943ac2e895
55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{- |
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : conversions to and from old SML aterm format
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaCopyright : (c) Klaus Luettich and Uni Bremen 2002-2004
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian MaederMaintainer : Christian.Maeder@dfki.de
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaStability : provisional
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederPortability : non-portable (imports Logic.Grothendieck)
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaThis module exports functions, that can convert an sml-CATS ATerm
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea into the Haskell abstract syntax tree. So it contains all the
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea necessary instances of ATermConvertible and a heuristic function
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea that calculates the new lists of Pos out of Region tuples.
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea the templates for the instances are automatically derived by
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea DrIFT. But there were made many hand written changes.
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder
e73f8ff81464981f9ba296a65a459364c0c3c486Codruta Girlea todo:
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea - p_flag from pos-TERM is not considered jet!
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea-}
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcu
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girleamodule ATC.Sml_cats ( ATermConvertibleSML
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder , from_sml_ATermString
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea , read_sml_ATerm
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder ) where
cb5be4f31df88b8137ef3cabf4e8b0ddec52f351Christian Maeder
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederimport Control.Monad
fd1c864a3dec70aa22ecb2bc85816ec8251c6decCodruta Girlea
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederimport Data.List (isPrefixOf)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederimport Data.Maybe
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder
fd1c864a3dec70aa22ecb2bc85816ec8251c6decCodruta Girleaimport qualified Data.Map as Map
c578c3805234bc223ab96f7d1892d3c73518ee94Christian Maeder-- better recompilation checking without 'import ATerm.Lib'
cb5be4f31df88b8137ef3cabf4e8b0ddec52f351Christian Maederimport ATerm.AbstractSyntax
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girleaimport ATerm.ReadWrite
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea
b5fc3c116b803863fe86b55bb75b164d4029c696Christian Maederimport Common.Id
1445ecc2d9c5c298117a0e7ea2c5accde351d07eChristian Maederimport Common.AS_Annotation
1445ecc2d9c5c298117a0e7ea2c5accde351d07eChristian Maederimport Common.LibName
b5fc3c116b803863fe86b55bb75b164d4029c696Christian Maederimport Common.IO
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleaimport Common.IRI (IRI, parseIRICurie)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport CASL.AS_Basic_CASL
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport CASL.Logic_CASL
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Logic.Grothendieck
a641f28dd33a3b94a9f28f9515ec50ea1b879fe4Christian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Syntax.AS_Structured
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Syntax.AS_Architecture
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleaimport Syntax.AS_Library
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea-- the following module provides the ability to parse the "unparsed-anno"
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleaimport Text.ParserCombinators.Parsec (parse)
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleaimport Common.AnnoParser (annotations, parseAnno)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Common.Lexer (skip)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Common.Utils (trimRight)
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowski-- | cats creates latin1 files
cb5be4f31df88b8137ef3cabf4e8b0ddec52f351Christian Maederread_sml_ATerm :: FilePath -> IO LIB_DEFN
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederread_sml_ATerm fn = liftM from_sml_ATermString $ readEncFile Latin1 fn
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder-- --- Convertible class for sml -----------------------------------------
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleaclass ATermConvertibleSML t where
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea from_sml_ShATerm :: ATermTable -> t
246cef3345515dc289e03fda4b04b1500db3ff6aChristian Maeder from_sml_ShATermList :: ATermTable -> [t]
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder -- default function ignores the annotation part
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder from_sml_ShATermList = from_sml_ATermList from_sml_ShATerm
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maederfrom_sml_ATermList :: (ATermTable -> t) -> ATermTable -> [t]
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maederfrom_sml_ATermList f at = case getATerm at of
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder ShAList ats _ -> map (f . flip getATermByIndex1 at) ats
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder aterm -> from_sml_ShATermError "[a]" aterm
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder
3e0ed56e973aeef92177e50f7272cafa7eb96fbeChristian Maederfrom_sml_ATermString :: ATermConvertibleSML a => String -> a
c578c3805234bc223ab96f7d1892d3c73518ee94Christian Maederfrom_sml_ATermString = from_sml_ShATerm . readATerm
29d8536ce8b1f05e6efd0b7d40e5c15cec3943c7Christian Maeder
29d8536ce8b1f05e6efd0b7d40e5c15cec3943c7Christian Maederfrom_sml_ShATermError :: String -> ShATerm -> a
d20b265a2765e843986ceed6bf0055582981bf0fChristian Maederfrom_sml_ShATermError t u =
1445ecc2d9c5c298117a0e7ea2c5accde351d07eChristian Maeder error ("Cannot convert Sml-ShATerm to " ++ t ++ ": " ++ err)
1445ecc2d9c5c298117a0e7ea2c5accde351d07eChristian Maeder where err = case u of
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder ShAAppl s l _ -> "!ShAAppl " ++ s ++ "("
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder ++ show (length l) ++ ")"
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder ShAList _ _ -> "!ShAList"
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder _ -> "!ShAInt"
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder-- basic instances -----------------------------------------------
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance ATermConvertibleSML Bool where
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder from_sml_ShATerm att = case at of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ShAAppl "true" [] _ -> True
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder ShAAppl "false" [] _ -> False
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder _ -> from_sml_ShATermError "Bool" at
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder where at = getATerm att
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder-- for Integer derive : ATermConvertibleSML hand written!
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance ATermConvertibleSML Integer where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder from_sml_ShATerm att = case getATerm att of
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder ShAInt x _ -> x
98ca12832943f9b8e6edd28bc59716a2f7798899Christian Maeder at -> from_sml_ShATermError "Integer" at
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederinstance ATermConvertibleSML Int where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder from_sml_ShATerm att = integer2Int $ from_sml_ShATerm att
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maederinstance ATermConvertibleSML Char where
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder from_sml_ShATerm att = case at of
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder (ShAAppl s [] _) -> str2Char s
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder _ -> from_sml_ShATermError "Char" at
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder where at = getATerm att
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder from_sml_ShATermList att = case at of
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder (ShAAppl s [] _) -> read s
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder _ -> from_sml_ShATermError "String" at
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder where at = getATerm att
417437c97b9f3ef102275ebd1e3d015b52ef6201Christian Maeder
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maederinstance (Ord a, ATermConvertibleSML a, ATermConvertibleSML b)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder => ATermConvertibleSML (Map.Map a b) where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder from_sml_ShATerm att = Map.fromList $ from_sml_ShATerm att
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance ATermConvertibleSML a => ATermConvertibleSML [a] where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder from_sml_ShATerm = from_sml_ShATermList
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance (ATermConvertibleSML a, ATermConvertibleSML b)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder => ATermConvertibleSML (a, b) where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder from_sml_ShATerm att = case at of
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcu (ShAAppl "" [x, y] _) -> (x', y')
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder where x' = from_sml_ShATerm (getATermByIndex1 x att)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder y' = from_sml_ShATerm (getATermByIndex1 y att)
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcu _ -> from_sml_ShATermError "(a,b)" at
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder where at = getATerm att
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcuinstance (ATermConvertibleSML a, ATermConvertibleSML b, ATermConvertibleSML c)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder => ATermConvertibleSML (a, b, c) where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder from_sml_ShATerm att = case at of
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcu (ShAAppl "" [a, b, c] _) -> (a', b', c')
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder where a' = from_sml_ShATerm (getATermByIndex1 a att)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder b' = from_sml_ShATerm (getATermByIndex1 b att)
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcu c' = from_sml_ShATerm (getATermByIndex1 c att)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder _ -> from_sml_ShATermError "(a,b,c)" at
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcu where at = getATerm att
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance (ATermConvertibleSML a, ATermConvertibleSML b,
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcu ATermConvertibleSML c, ATermConvertibleSML d)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder => ATermConvertibleSML (a, b, c, d) where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder from_sml_ShATerm att = case at of
9e4febfd2eb81ca73c9b6a6a3c40017e6fb99390Mihaela Turcu (ShAAppl "" [a, b, c, d] _) -> (a', b', c', d')
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder where a' = from_sml_ShATerm (getATermByIndex1 a att)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder b' = from_sml_ShATerm (getATermByIndex1 b att)
c' = from_sml_ShATerm (getATermByIndex1 c att)
d' = from_sml_ShATerm (getATermByIndex1 d att)
_ -> from_sml_ShATermError "(a,b,c)" at
where at = getATerm att
-- --- instances of Id.hs ------------------------------------------------
instance ATermConvertibleSML Token where
from_sml_ShATerm att =
case aterm of
(ShAAppl "token" [ aa ] _) ->
mkSimpleId $ from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "place" [] _) -> mkSimpleId Common.Id.place
_ -> from_sml_ShATermError "Token" aterm
where aterm = getATerm att
instance ATermConvertibleSML Id where
from_sml_ShATerm att =
case aterm of
(ShAAppl "compound-id" [ aa, ab ] _) -> -- TOKEN_OR_MIXFIX,[ID]
let
aa' = from_sml_ATermTokenTup (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = nullRange
in Id aa' ab' ac'
(ShAAppl "simple-id" [ aa ] _) ->
let
aa' = from_sml_ATermTokenTup (getATermByIndex1 aa att)
ab' = []
ac' = nullRange
in Id aa' ab' ac'
_ -> from_sml_ShATermError "Id" aterm
where
aterm = getATerm att
from_sml_ATermTokenTup :: ATermTable -> [Token]
from_sml_ATermTokenTup att =
case aterm of
(ShAAppl "" [tops, _, _] _) ->
from_sml_ShATerm (getATermByIndex1 tops att)
_ -> from_sml_ShATermError "Token" aterm
where aterm = getATerm att
-- --- instances of AS_Annotation.hs -------------------------------------
instance ATermConvertibleSML Annotation where
from_sml_ShATerm att =
case aterm of
(ShAAppl "comment-line" [ aa ] _) ->
let
aa' = trimRight $ from_sml_ShATerm (getATermByIndex1 aa att)
ab' = pos_l
in Unparsed_anno Comment_start (Line_anno aa') ab'
(ShAAppl "comment" [ aa ] _) ->
let
aa' = lines (from_sml_ShATerm (getATermByIndex1 aa att))
ab' = pos_l
in Unparsed_anno Comment_start (Group_anno aa') ab'
(ShAAppl "unparsed-anno" [ aa ] _) ->
parse_anno pos_l
(from_sml_ShATerm (getATermByIndex1 aa att))
(ShAAppl "annote-line" [ aa, ab ] _) ->
let
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = pos_l
in Unparsed_anno (Annote_word aa') (Line_anno ab') ac'
(ShAAppl "annote-group" [ aa, ab ] _) ->
let
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = pos_l
in Unparsed_anno (Annote_word aa') (Group_anno ab') ac'
(ShAAppl "display-anno" [ aa, ab ] _) ->
let
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = parse_disp_anno aa' pos_l
(trimRight $ from_sml_ShATerm (getATermByIndex1 ab att))
in ab'
(ShAAppl "string-anno" [ aa, ab ] _) ->
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"
emptyAnno (from_sml_ShATerm att)
_ -> 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
hd : tl = from_sml_ShATerm (getATermByIndex1 aa att)
as = from_sml_ShATerm (getATermByIndex1 ab att)
aa'' = addLAnnoList as hd : tl
ab' = pos_l
in Sort_items NonEmptySorts aa'' ab'
(ShAAppl "op-items" [ aa, ab ] _) ->
let
hd : tl = from_sml_ShATerm (getATermByIndex1 aa att)
as = from_sml_ShATerm (getATermByIndex1 ab att)
aa'' = addLAnnoList as hd : tl
ab' = pos_l
in Op_items aa'' ab'
(ShAAppl "pred-items" [ aa, ab ] _) ->
let
hd : tl = from_sml_ShATerm (getATermByIndex1 aa att)
as = from_sml_ShATerm (getATermByIndex1 ab att)
aa'' = addLAnnoList as hd : tl
ab' = pos_l
in Pred_items aa'' ab'
(ShAAppl "datatype-items" [ aa, ab ] _) ->
let
hd : tl = from_sml_ShATerm (getATermByIndex1 aa att)
as = from_sml_ShATerm (getATermByIndex1 ab att)
aa'' = addLAnnoList as hd : tl
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_ATermList from_sml_ATermARG_DECL
(getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = pos_l
in Op_head Total aa' (Just ab') ac'
(ShAAppl "partial-op-head" [ aa, ab ] _) ->
let
aa' = from_sml_ATermList from_sml_ATermARG_DECL
(getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = pos_l
in Op_head Partial aa' (Just 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)
from_sml_ATermARG_DECL :: ATermTable -> VAR_DECL
from_sml_ATermARG_DECL 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 Var_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_ATermList from_sml_ATermARG_DECL
(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)
abh : abt = from_sml_ShATerm (getATermByIndex1 ab att)
as = from_sml_ShATerm (getATermByIndex1 ac att)
ab'' = addLAnnoList as abh : abt
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 Junction Con aa' ab'
(ShAAppl "disjunction" [ aa ] _) ->
let
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = pos_l
in Junction Dis 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 Relation aa' Implication ab' ac'
(ShAAppl "equivalence" [ aa, ab ] _) ->
let
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = pos_l
in Relation aa' Equivalence 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 Atom True aa'
(ShAAppl "ffalse" [] _) ->
let
aa' = pos_l
in Atom False 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 Equation aa' Existl 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 Equation aa' Strong 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 and IRIs ----------------------------------
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
from_sml_ATermIRI :: ATermTable -> IRI
from_sml_ATermIRI att =
case aterm of
(ShAAppl "" [ si, _ ] _) -> {- snd element is 'None'
(CASL.grm:((WORDS,None))) -}
let s = from_sml_ShATerm $ getATermByIndex1 si att
in fromMaybe (error $ "parsing error: not an IRI \"" ++ s
++ "\" \n(from_sml_ATermIRI)")
$ parseIRICurie s
_ -> from_sml_ShATermError "IRI" 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_ATermIRI (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' = emptyAnno s
(pos_l, group_flag, att') = skipPosFlag "pos-SPEC" att
-- - a helper function for [(Annoted a, [Annotation])] --------------------
toAnnotedList :: [(Annoted a, [Annotation])] -> [Annoted a]
toAnnotedList = map merge
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_ATermIRI (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
hd : tl = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ATermRESULT_UNIT (getATermByIndex1 ab att)
as = toAnnoList ac att
aa'' = addLAnnoList as hd : tl
ac' = pos_l
in Basic_arch_spec aa'' ab' ac'
(ShAAppl "named-arch-spec" [ aa ] _) ->
let
aa' = from_sml_ATermIRI (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_ATermIRI $
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_ATermIRI $ 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_ATermIRI (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_ATermIRI (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_ATermIRI (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 {}) _ _ _) ->
emptyAnno (Group_arch_spec aa'' ab')
_ -> 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_ATermIRI (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_ATermIRI (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' = emptyAnno ut
(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_ATermIRI (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_ATermIRI (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_ATermIRI (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_ATermIRI (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' (ItemMaps 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 ItemNameMap where
from_sml_ShATerm att =
case aterm of
ShAAppl "item-name" [aa] _ ->
let
aa' = from_sml_ATermIRI $ getATermByIndex1 aa att
in ItemNameMap aa' Nothing
ShAAppl "item-name-map" [aa, ab] _ ->
let
aa' = from_sml_ATermIRI $ getATermByIndex1 aa att
ab' = from_sml_ATermIRI $ getATermByIndex1 ab att
in ItemNameMap aa' $ Just ab'
_ -> from_sml_ShATermError "ITEM_NAME_OR_MAP" aterm
where
aterm = getATerm att'
att' = case getATerm att of
ShAAppl "pos-ITEM-NAME-OR-MAP" [_, item_i] _ ->
getATermByIndex1 item_i att
_ -> att
instance ATermConvertibleSML LibName where
from_sml_ShATerm att =
case aterm of
(ShAAppl "versioned-lib" [ aa, ab ] _) ->
let
(aa', r) = fromSmlShATermToLibId (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (LibName aa' r Nothing $ Just ab')
(ShAAppl "lib" [ aa ] _) ->
let (aa', r) = fromSmlShATermToLibId (getATermByIndex1 aa att)
in LibName aa' r Nothing 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
fromSmlShATermToLibId :: ATermTable -> (IRI, Range)
fromSmlShATermToLibId att =
case aterm of
(ShAAppl str [ aa ] _) | elem str ["path-name", "url"] ->
let
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = pos_l
in (fromMaybe (error "fromSmlShATermToLibId")
$ parseIRICurie aa', ab')
_ -> from_sml_ShATermError "LibId" 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 (uncurry $ newPos "")
$ 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 = case tops of
[] -> []
hd : tl -> hd { tokPos = Range [p] } : tl
setFstPos _ _ = error "wrong call: setFstPos"