{- |
Module : ./ATC/Sml_cats.hs
Description : conversions to and from old SML aterm format
Copyright : (c) Klaus Luettich and Uni Bremen 2002-2004
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : non-portable (imports Logic.Grothendieck)
This module exports functions, that can convert an sml-CATS ATerm
into the Haskell abstract syntax tree. So it contains all the
necessary instances of ATermConvertible and a heuristic function
that calculates the new lists of Pos out of Region tuples.
the templates for the instances are automatically derived by
DrIFT. But there were made many hand written changes.
todo:
- p_flag from pos-TERM is not considered jet!
-}
module ATC.Sml_cats ( ATermConvertibleSML
, from_sml_ATermString
, read_sml_ATerm
) where
import Control.Monad
import Data.List (isPrefixOf)
import Data.Maybe
import qualified Data.Map as Map
-- better recompilation checking without 'import ATerm.Lib'
import ATerm.AbstractSyntax
import ATerm.ReadWrite
import Common.Id
import Common.AS_Annotation
import Common.LibName
import Common.IO
import Common.IRI (IRI, parseIRICurie, iriPos)
import CASL.AS_Basic_CASL
import CASL.Logic_CASL
import Logic.Grothendieck
import Syntax.AS_Structured
import Syntax.AS_Architecture
import Syntax.AS_Library
-- the following module provides the ability to parse the "unparsed-anno"
import Text.ParserCombinators.Parsec (parse)
import Common.AnnoParser (annotations, parseAnno)
import Common.Lexer (skip)
import Common.Utils (trimRight)
-- | cats creates latin1 files
read_sml_ATerm :: FilePath -> IO LIB_DEFN
read_sml_ATerm fn = liftM from_sml_ATermString $ readEncFile Latin1 fn
-- --- Convertible class for sml -----------------------------------------
class ATermConvertibleSML t where
from_sml_ShATerm :: ATermTable -> t
from_sml_ShATermList :: ATermTable -> [t]
-- default function ignores the annotation part
from_sml_ShATermList = from_sml_ATermList from_sml_ShATerm
from_sml_ATermList :: (ATermTable -> t) -> ATermTable -> [t]
from_sml_ATermList f at = case getATerm at of
ShAList ats _ -> map (f . flip getATermByIndex1 at) ats
aterm -> from_sml_ShATermError "[a]" aterm
from_sml_ATermString :: ATermConvertibleSML a => String -> a
from_sml_ATermString = from_sml_ShATerm . readATerm
from_sml_ShATermError :: String -> ShATerm -> a
from_sml_ShATermError t u =
error ("Cannot convert Sml-ShATerm to " ++ t ++ ": " ++ err)
where err = case u of
ShAAppl s l _ -> "!ShAAppl " ++ s ++ "("
++ show (length l) ++ ")"
ShAList _ _ -> "!ShAList"
_ -> "!ShAInt"
-- basic instances -----------------------------------------------
instance ATermConvertibleSML Bool where
from_sml_ShATerm att = case at of
ShAAppl "true" [] _ -> True
ShAAppl "false" [] _ -> False
_ -> from_sml_ShATermError "Bool" at
where at = getATerm att
-- for Integer derive : ATermConvertibleSML hand written!
instance ATermConvertibleSML Integer where
from_sml_ShATerm att = case getATerm att of
ShAInt x _ -> x
at -> from_sml_ShATermError "Integer" at
instance ATermConvertibleSML Int where
from_sml_ShATerm att = integer2Int $ from_sml_ShATerm att
instance ATermConvertibleSML Char where
from_sml_ShATerm att = case at of
(ShAAppl s [] _) -> str2Char s
_ -> from_sml_ShATermError "Char" at
where at = getATerm att
from_sml_ShATermList att = case at of
(ShAAppl s [] _) -> read s
_ -> from_sml_ShATermError "String" at
where at = getATerm att
instance (Ord a, ATermConvertibleSML a, ATermConvertibleSML b)
=> ATermConvertibleSML (Map.Map a b) where
from_sml_ShATerm att = Map.fromList $ from_sml_ShATerm att
instance ATermConvertibleSML a => ATermConvertibleSML [a] where
from_sml_ShATerm = from_sml_ShATermList
instance (ATermConvertibleSML a, ATermConvertibleSML b)
=> ATermConvertibleSML (a, b) where
from_sml_ShATerm att = case at of
(ShAAppl "" [x, y] _) -> (x', y')
where x' = from_sml_ShATerm (getATermByIndex1 x att)
y' = from_sml_ShATerm (getATermByIndex1 y att)
_ -> from_sml_ShATermError "(a,b)" at
where at = getATerm att
instance (ATermConvertibleSML a, ATermConvertibleSML b, ATermConvertibleSML c)
=> ATermConvertibleSML (a, b, c) where
from_sml_ShATerm att = case at of
(ShAAppl "" [a, b, c] _) -> (a', b', c')
where a' = from_sml_ShATerm (getATermByIndex1 a att)
b' = from_sml_ShATerm (getATermByIndex1 b att)
c' = from_sml_ShATerm (getATermByIndex1 c att)
_ -> from_sml_ShATermError "(a,b,c)" at
where at = getATerm att
instance (ATermConvertibleSML a, ATermConvertibleSML b,
ATermConvertibleSML c, ATermConvertibleSML d)
=> ATermConvertibleSML (a, b, c, d) where
from_sml_ShATerm att = case at of
(ShAAppl "" [a, b, c, d] _) -> (a', b', c', d')
where a' = from_sml_ShATerm (getATermByIndex1 a att)
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)
_ -> 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' Nothing 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' = fromSmlShATermToLibId (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in mkLibName aa' $ Just ab'
(ShAAppl "lib" [ aa ] _) ->
iriLibName . fromSmlShATermToLibId $ getATermByIndex1 aa att
_ -> 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
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') { iriPos = 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"