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.
- p_flag from pos-TERM is not considered jet!
-- better recompilation checking without 'import
ATerm.Lib'
-- the following module provides the ability to parse the "unparsed-anno"
-- | cats creates latin1 files
read_sml_ATerm :: FilePath -> IO LIB_DEFN
read_sml_ATerm fn = readEncFile Latin1 fn >>= return . from_sml_ATermString
----- 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 s = (\ a -> from_sml_ShATerm a) (readATerm s)
from_sml_ShATermError :: String -> ShATerm -> a
from_sml_ShATermError t u =
error ("Cannot convert Sml-ShATerm to " ++ t ++ ": "++ err)
ShAAppl s l _ -> "!ShAAppl " ++ s ++ "("
++ show (length l) ++ ")"
ShAList _ _ -> "!ShAList"
-- basic instances -----------------------------------------------
instance ATermConvertibleSML Bool where
from_sml_ShATerm att = case at of
ShAAppl "true" [] _ -> True
ShAAppl "false" [] _ -> False
_ -> from_sml_ShATermError "Bool" at
-- for Integer derive : ATermConvertibleSML hand written!
instance ATermConvertibleSML Integer where
from_sml_ShATerm att = case getATerm att of
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
from_sml_ShATermList att = case at of
(ShAAppl s [] _) -> read s
_ -> from_sml_ShATermError "String" at
instance (Ord a, ATermConvertibleSML a, ATermConvertibleSML b)
=> ATermConvertibleSML (
Map.Map a b) where
instance ATermConvertibleSML a => ATermConvertibleSML [a] where
from_sml_ShATerm att = from_sml_ShATermList att
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
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
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
----- instances of
Id.hs ------------------------------------------------
instance ATermConvertibleSML Token where
(ShAAppl "token" [ aa ] _) ->
mkSimpleId $ from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "Token" aterm
where aterm = getATerm att
instance ATermConvertibleSML Id where
(ShAAppl "compound-id" [ aa,ab ] _) -> -- TOKEN_OR_MIXFIX,[ID]
aa' = from_sml_ATermTokenTup (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
(ShAAppl "simple-id" [ aa ] _) ->
aa' = from_sml_ATermTokenTup (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "Id" aterm
from_sml_ATermTokenTup :: ATermTable -> [Token]
from_sml_ATermTokenTup att =
(ShAAppl "" [tops,_,_] _) ->
from_sml_ShATerm (getATermByIndex1 tops att)
_ -> from_sml_ShATermError "Token" aterm
where aterm = getATerm att
instance ATermConvertibleSML Annotation where
(ShAAppl "comment-line" [ aa ] _) ->
aa' = trimRight $ from_sml_ShATerm (getATermByIndex1 aa att)
in (Unparsed_anno Comment_start (Line_anno aa') ab')
(ShAAppl "comment" [ aa ] _) ->
aa' = lines (from_sml_ShATerm (getATermByIndex1 aa att))
in (Unparsed_anno Comment_start (Group_anno aa') ab')
(ShAAppl "unparsed-anno" [ aa ] _) ->
(from_sml_ShATerm (getATermByIndex1 aa att))
(ShAAppl "annote-line" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Unparsed_anno (Annote_word aa') (Line_anno ab') ac')
(ShAAppl "annote-group" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Unparsed_anno (Annote_word aa') (Group_anno ab') ac')
(ShAAppl "display-anno" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = parse_disp_anno aa' (pos_l)
(trimRight $ from_sml_ShATerm (getATermByIndex1 ab att))
(ShAAppl "string-anno" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (String_anno aa' ab' ac')
(ShAAppl "list-anno" [ aa,ab,ac ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = from_sml_ShATerm (getATermByIndex1 ac att)
in (List_anno aa' ab' ac' ad')
(ShAAppl "number-anno" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "floating-anno" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Float_anno aa' ab' ac')
(ShAAppl "prec-anno" [ aa,ab,ac ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = from_sml_ShATerm (getATermByIndex1 ac att)
in (Prec_anno (if aa' then Lower else BothDirections)
(ShAAppl "lassoc-anno" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in (Assoc_anno ALeft aa' ab')
(ShAAppl "rassoc-anno" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in (Assoc_anno ARight aa' ab')
(ShAAppl "label-anno" [ aa ] _) ->
(from_sml_ShATerm $ getATermByIndex1 aa att) ""
(ShAAppl "implies" [] _) ->
in (Semantic_anno SA_implies aa')
(ShAAppl "definitional" [] _) ->
in (Semantic_anno SA_def aa')
(ShAAppl "conservative" [] _) ->
in (Semantic_anno SA_cons aa')
Semantic_anno SA_mono (pos_l)
_ -> from_sml_ShATermError "Annotation" aterm
(ShAAppl "pos-ANNO" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i 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
-- Basic Items (including sig_items)
case from_sml_ATermAnnotedBasic_Items att of
(bi, las) -> Annoted bi nullRange las []
-- L_.* constuctors from SML
"" -> Annoted (from_sml_ShATerm (getATermByIndex1
(toAnnoList (last as) att)
_ -> -- "No appropiate constructor for Annoted found"
Annoted (from_sml_ShATerm att)
_ -> from_sml_ShATermError "Annoted a" aterm
---- 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 =
((from_sml_ShATerm att),[])
else ((from_sml_ShATerm att),annoList)
(ShAAppl _ as _)-> -- pos-BASIC-ITEMS
case getATerm $ getATermByIndex1 (last as) att of
(ShAAppl "sig-items" _ _) -> True
_ -> from_sml_ShATermError "{SIG,BASIC}_items" aterm
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
case parse (skip >> annotations) "" inp of
_ -> 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
pos = case rangeToList pos_l of
inp' = showId i $ ' ' : s_inp
s_inp = case reverse inp of
rin | "%)" `isPrefixOf` rin -> reverse $ drop 2 rin
instance ATermConvertibleSML (BASIC_SPEC a b c) where
(ShAAppl "basic-spec" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "BASIC_SPEC" aterm
(ShAAppl "pos-BASIC-SPEC" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML (BASIC_ITEMS a b c) where
(ShAAppl "sig-items" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "free-datatype" [ aa,_ ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in (Free_datatype NonEmptySorts aa' ab')
(ShAAppl "sort-gen" [ aa,_ ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "var-items" [ aa,_ ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "local-var-axioms" [ aa,ab,_ ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Local_var_axioms aa' ab' ac')
(ShAAppl "axiom-items" [ aa,_ ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "BASIC_ITEMS" aterm
(ShAAppl "pos-BASIC-ITEMS" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML (SIG_ITEMS a b) where
(ShAAppl "sort-items" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
as = from_sml_ShATerm (getATermByIndex1 ab att)
aa'' = (addLAnnoList as $ head aa'):(tail aa')
in (Sort_items NonEmptySorts aa'' ab')
(ShAAppl "op-items" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
as = from_sml_ShATerm (getATermByIndex1 ab att)
aa'' = (addLAnnoList as $ head aa'):(tail aa')
(ShAAppl "pred-items" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
as = from_sml_ShATerm (getATermByIndex1 ab att)
aa'' = (addLAnnoList as $ head aa'):(tail aa')
(ShAAppl "datatype-items" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
as = from_sml_ShATerm (getATermByIndex1 ab att)
aa'' = (addLAnnoList as $ head aa'):(tail aa')
in (Datatype_items NonEmptySorts aa'' ab')
_ -> from_sml_ShATermError "SIG_ITEMS" aterm
(ShAAppl "pos-SIG-ITEMS" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML (SORT_ITEM a) where
(ShAAppl "sort-decl" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "subsort-decl" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Subsort_decl aa' ab' ac')
(ShAAppl "subsort-defn" [ aa,ab,ac,ad,ae ] _) ->
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)
ad''= addRAnnoList as ad'
in (Subsort_defn aa' ab' ac' ad'' ae')
(ShAAppl "iso-decl" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "SORT_ITEM" aterm
(ShAAppl "pos-SORT-ITEM" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML (OP_ITEM a) where
(ShAAppl "op-decl" [ aa,ab,ac ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = from_sml_ShATerm (getATermByIndex1 ac att)
in (Op_decl aa' ab' ac' ad')
(ShAAppl "op-defn" [ aa,ab,ac,ad ] _) ->
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'
in (Op_defn aa' ab' ac'' ad')
_ -> from_sml_ShATermError "OP_ITEM" aterm
(ShAAppl "pos-OP-ITEM" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML OP_TYPE where
(ShAAppl "total-op-type" [ aa,ab ] _) ->
(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 ] _) ->
(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
(ShAAppl "pos-OP-TYPE" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
---- a helper for the SML-datatype SORTS -------------------------------
from_sml_ATermSORTS :: ATermTable -> ([SORT],Range)
from_sml_ATermSORTS att =
(ShAAppl "sorts" [ aa ] _) ->
(from_sml_ShATerm (getATermByIndex1 aa att),pos_l)
_ -> from_sml_ShATermError "([SORT],Range)" aterm
(ShAAppl "pos-SORTS" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML OP_HEAD where
(ShAAppl "total-op-head" [ aa,ab ] _) ->
aa' = from_sml_ATermList from_sml_ATermARG_DECL
(getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Op_head Total aa' (Just ab') ac')
(ShAAppl "partial-op-head" [ aa,ab ] _) ->
aa' = from_sml_ATermList from_sml_ATermARG_DECL
(getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Op_head Partial aa' (Just ab') ac')
_ -> from_sml_ShATermError "OP_HEAD" aterm
(ShAAppl "pos-OP-HEAD" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
from_sml_ATermARG_DECL :: ATermTable -> VAR_DECL
from_sml_ATermARG_DECL att =
-- (ShAAppl "arg-decl" [ ShAAppl "" [aa,ab] _ ] _) ->
(ShAAppl "" [aa,ab] _) ->
aa' = from_sml_ATermVARs (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Var_decl aa' ab' ac')
_ -> from_sml_ShATermError "ARG_DECL" aterm
aterm = case getATerm att' of
ShAAppl "arg-decl" [i] _ ->
getATerm $ getATermByIndex1 i att
x -> from_sml_ShATermError "arg-decl" x
(ShAAppl "pos-ARG-DECL" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML (OP_ATTR a) where
(ShAAppl "associative" [ ] _) ->
(ShAAppl "commutative" [ ] _) ->
(ShAAppl "idempotent" [ ] _) ->
(ShAAppl "unit-op-attr" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "OP_ATTR" aterm
(ShAAppl "pos-OP-ATTR" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML (PRED_ITEM a) where
(ShAAppl "pred-decl" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Pred_decl aa' ab' ac')
(ShAAppl "pred-defn" [ aa,ab,ac,_ ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = from_sml_ShATerm (getATermByIndex1 ac att)
in (Pred_defn aa' ab' ac' ad')
_ -> from_sml_ShATermError "PRED_ITEM" aterm
(ShAAppl "pos-PRED-ITEM" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML PRED_TYPE where
(ShAAppl "pred-type" [ aa ] _) ->
(aa',ps) = from_sml_ATermSORTS (getATermByIndex1 aa att)
ab' = insertPos ps $ pos_l
_ -> from_sml_ShATermError "PRED_TYPE" aterm
(ShAAppl "pos-PRED-TYPE" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML PRED_HEAD where
(ShAAppl "pred-head" [ aa ] _) ->
aa' = from_sml_ATermList from_sml_ATermARG_DECL
(getATermByIndex1 aa att)
_ -> from_sml_ShATermError "PRED_HEAD" aterm
(ShAAppl "pos-PRED-HEAD" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML DATATYPE_DECL where
(ShAAppl "datatype-decl" [ aa,ab,ac ] _) ->
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
in (Datatype_decl aa' ab'' ac')
_ -> from_sml_ShATermError "DATATYPE_DECL" aterm
(ShAAppl "pos-DATATYPE-DECL" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML ALTERNATIVE where
(ShAAppl "total-construct" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Alt_construct Total aa' ab' ac')
(ShAAppl "partial-construct" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Alt_construct Partial aa' ab' ac')
(ShAAppl "subsort" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "ALTERNATIVE" aterm
(ShAAppl "pos-ALTERNATIVE" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML COMPONENTS where
(ShAAppl "total-select" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Cons_select Total aa' ab' ac')
(ShAAppl "partial-select" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Cons_select Partial aa' ab' ac')
(ShAAppl "sort-component" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "COMPONENTS" aterm
(ShAAppl "pos-COMPONENTS" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML VAR_DECL where
(ShAAppl "" [ aa,ab ] _) ->
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
instance ATermConvertibleSML (FORMULA a) where
(ShAAppl "quantification" [ aa,ab,ac ] _) ->
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 ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "disjunction" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "implication" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Implication aa' ab' True ac')
(ShAAppl "equivalence" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Equivalence aa' ab' ac')
(ShAAppl "negation" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
-- the following things are from SML-type ATOM
(ShAAppl "atom" [i] _) ->
case getATerm (getATermByIndex1 i att') of
(ShAAppl "ttrue" [] _) ->
(ShAAppl "ffalse" [] _) ->
(ShAAppl "predication" [ aa,ab ] _) ->
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 ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "existl-equation" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Existl_equation aa' ab' ac')
(ShAAppl "strong-equation" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Strong_equation aa' ab' ac')
(ShAAppl "membership" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Membership aa' ab' ac')
_ -> from_sml_ShATermError "FORMULA" aterm
_ -> from_sml_ShATermError "FORMULA" aterm
(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 =
(ShAAppl "terms" [ aa ] _) ->
(from_sml_ShATerm (getATermByIndex1 aa att),pos_l)
_ -> from_sml_ShATermError "([TERM],Range)" aterm
where aterm = getATerm att'
(ShAAppl "pos-TERMS" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
---- a helper for SIMPLE_IDs and IRIs ----------------------------------
from_sml_ATermSIMPLE_ID :: ATermTable -> SIMPLE_ID
from_sml_ATermSIMPLE_ID att =
(ShAAppl "" [ si, _ ] _) -> -- snd element is 'None'
let s = from_sml_ShATerm $ getATermByIndex1 si att
_ -> from_sml_ShATermError "SIMPLE_ID" aterm
where aterm = getATerm att
from_sml_ATermIRI :: ATermTable -> IRI
(ShAAppl "" [ si, _ ] _) -> -- snd element is 'None'
let s = from_sml_ShATerm $ getATermByIndex1 si att
in case parseIRICurie s of
Nothing -> error $ "parsing error: not an IRI \"" ++ s
++ "\" \n(from_sml_ATermIRI)"
_ -> 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
(ShAAppl "forall" [ ] _) ->
(ShAAppl "exists" [ ] _) ->
(ShAAppl "exists-uniquely" [ ] _) ->
_ -> from_sml_ShATermError "QUANTIFIER" aterm
(ShAAppl "pos-QUANTIFIER" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML PRED_SYMB where
(ShAAppl "pred-symb" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in case getATerm $ getATermByIndex1 ab att of
ShAAppl "Some" [ aab ] _ ->
let aab' = from_sml_ShATerm (getATermByIndex1 aab att)
in (Qual_pred_name aa' aab' ac')
_ -> from_sml_ShATermError "Option" aterm
_ -> from_sml_ShATermError "PRED_SYMB" aterm
(ShAAppl "pos-PRED-SYMB" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML (TERM a) where
(ShAAppl "var-or-const" [ aa ] _) ->
aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)
(ShAAppl "qual-var" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Qual_var aa' ab' ac')
(ShAAppl "application" [ aa,ab ] _) ->
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 ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Sorted_term aa' ab' ac')
(ShAAppl "cast" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
(ShAAppl "conditional" [ aa,ab,ac ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = from_sml_ShATerm (getATermByIndex1 ac att)
in (Conditional aa' ab' ac' ad')
_ -> from_sml_ShATermError "TERM" aterm
(pos_l,_p_flag,att') = skipPosFlag "pos-TERM" att
instance ATermConvertibleSML OP_SYMB where
(ShAAppl "op-symb" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in case getATerm $ getATermByIndex1 ab att of
ShAAppl "Some" [ aab ] _ ->
let aab' = from_sml_ShATerm (getATermByIndex1 aab att)
in (Qual_op_name aa' aab' ac')
_ -> from_sml_ShATermError "Option" aterm
_ -> from_sml_ShATermError "OP_SYMB" aterm
(ShAAppl "pos-OP-SYMB" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML SYMB_ITEMS where
(ShAAppl "symb-items" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Symb_items aa' ab' ac')
_ -> from_sml_ShATermError "SYMB_ITEMS" aterm
(ShAAppl "pos-SYMB-ITEMS" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML SYMB_MAP_ITEMS where
(ShAAppl "symb-map-items" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Symb_map_items aa' ab' ac')
_ -> from_sml_ShATermError "SYMB_MAP_ITEMS" aterm
(ShAAppl "pos-SYMB-MAP-ITEMS" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML SYMB_KIND where
(ShAAppl "implicitk" [ ] _) ->
(ShAAppl "sortsk" [ ] _) ->
(ShAAppl "opsk" [ ] _) ->
(ShAAppl "predsk" [ ] _) ->
_ -> from_sml_ShATermError "SYMB_KIND" aterm
(ShAAppl "pos-SYMB-KIND" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML SYMB where
(ShAAppl "symb-id" [ aa ] _) ->
i = from_sml_ShATerm (getATermByIndex1 aa att)
aa' = setFstPos (pos_l) i
(ShAAppl "qual-id" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
_ -> from_sml_ShATermError "SYMB" aterm
(ShAAppl "pos-SYMB" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML TYPE where
(ShAAppl "op-symb-type" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "pred-symb-type" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "TYPE" aterm
(ShAAppl "pos-TYPE" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML SYMB_OR_MAP where
(ShAAppl "symb" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "symb-or-map" [ aa ] _) ->
(aa',ab') = from_sml_ATermSYMB_MAP (getATermByIndex1 aa att)
in (Symb_map aa' ab' ac')
_ -> from_sml_ShATermError "SYMB_OR_MAP" aterm
(ShAAppl "pos-SYMB-OR-MAP" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
---- a helper for SYMB_MAP from SML -------------------------------------
from_sml_ATermSYMB_MAP :: ATermTable -> (SYMB,SYMB)
from_sml_ATermSYMB_MAP att =
(ShAAppl "symb-map" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
_ -> from_sml_ShATermError "(SYMB,SYMB)" aterm
(ShAAppl "pos-SYMB-MAP" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML SPEC where
(ShAAppl "basic" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
aa'' = G_basic_spec CASL aa'
(ShAAppl "translation" [ aa,ab,_ ] _) ->
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,_ ] _) ->
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 ] _) ->
aa' :: [(Annoted SPEC,[Annotation])]
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in group (Union (toAnnotedList aa') ab') group_flag
(ShAAppl "extension" [ aa ] _) ->
aa' :: [(Annoted SPEC,[Annotation])]
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in group (Extension (toAnnotedList aa') ab') group_flag
(ShAAppl "free-spec" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
aa''= addLAnnoList (toAnnoList ab att) aa'
in group (Free_spec aa'' ab') group_flag
(ShAAppl "local-spec" [ aa,ab,ac,ad ] _) ->
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 ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
aa''= addLAnnoList (toAnnoList ab att) aa'
in group (Closed_spec aa'' ab') group_flag
(ShAAppl "spec-inst" [ aa,ab ] _) ->
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
group s gf = if gf then (Group s' pos_l) else s
where s' = Annoted s nullRange [] []
(pos_l,group_flag,att') = skipPosFlag "pos-SPEC" att
--- a helper function for [(Annoted a, [Annotation])] --------------------
toAnnotedList :: [(Annoted a,[Annotation])] -> [Annoted a]
toAnnotedList xs = map merge xs
where merge (ai,as) = ai { l_annos = (l_annos ai) ++ as}
instance ATermConvertibleSML RENAMING where
(ShAAppl "renaming" [ aa ] _) ->
case from_sml_ShATerm (getATermByIndex1 aa att) of
aa''= if null aa' then []
else [G_symb_map $ G_symb_map_items_list CASL aa']
_ -> from_sml_ShATermError "RENAMING" aterm
(ShAAppl "pos-RENAMING" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML RESTRICTION where
(ShAAppl "hide" [ aa ] _) ->
aa''= case from_sml_ShATerm (getATermByIndex1 aa att) of
aa' -> [G_symb_list $ G_symb_items_list CASL aa']
(ShAAppl "reveal" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
aa''= G_symb_map_items_list CASL aa'
_ -> from_sml_ShATermError "RESTRICTION" aterm
(ShAAppl "pos-RESTRICTION" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
{- !!! This will be done by the instance of LIB_ITEM !!!
instance ATermConvertibleSML SPEC_DEFN where
instance ATermConvertibleSML GENERICITY where
(ShAAppl "genericity" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Genericity aa' ab' ac')
_ -> from_sml_ShATermError "GENERICITY" aterm
(ShAAppl "pos-GENERICITY" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML PARAMS where
(ShAAppl "params" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "PARAMS" aterm
(ShAAppl "pos-PARAMS" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML IMPORTED where
(ShAAppl "imports" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "IMPORTED" aterm
(ShAAppl "pos-IMPORTS" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML FIT_ARG where
(ShAAppl "fit-spec" [ aa,ab ] _) ->
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']
in (Fit_spec aa' ab'' ac')
(ShAAppl "fit-view" [ aa,ab ] _) ->
aa' = from_sml_ATermIRI (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Fit_view aa' ab' ac')
_ -> from_sml_ShATermError "FIT_ARG" aterm
(ShAAppl "pos-FIT-ARG" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
{- !!! This conversion is covered by the instance of LIB_ITEM !!!
instance ATermConvertibleSML VIEW_DEFN where
instance ATermConvertibleSML VIEW_TYPE where
(ShAAppl "view-type" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (View_type aa' ab' ac')
_ -> from_sml_ShATermError "VIEW_TYPE" aterm
(ShAAppl "pos-VIEW-TYPE" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
{- !!! This conversion is covered by the instance of LIB_ITEM !!!
instance ATermConvertibleSML ARCH_SPEC_DEFN where
instance ATermConvertibleSML ARCH_SPEC where
(ShAAppl "basic-arch-spec" [ aa,ab,ac ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ATermRESULT_UNIT (getATermByIndex1 ab att)
aa''= (addLAnnoList as $ head aa'):tail aa'
in (Basic_arch_spec aa'' ab' ac')
(ShAAppl "named-arch-spec" [ aa ] _) ->
aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "ARCH_SPEC" aterm
(ShAAppl "pos-ARCH-SPEC" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
from_sml_ATermRESULT_UNIT :: ATermTable -> (Annoted UNIT_EXPRESSION)
from_sml_ATermRESULT_UNIT att =
(ShAAppl "result-unit" [ aa,ab ] _) ->
-- aa' :: UNIT_EXPRESSION
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in (Annoted aa' nullRange as [])
_ -> from_sml_ShATermError "RESULT-UNIT" aterm
(ShAAppl "pos-RESULT-UNIT" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML UNIT_REF where
(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)
ShAAppl "unit-decl" [aa,ab,_] _ ->
let aa' = from_sml_ATermSIMPLE_ID $
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Unit_ref aa' ab' ad')
_ -> from_sml_ShATermError "UNIT_DECL" aterm2
_ -> from_sml_ShATermError "UNIT-DECL-DEFN" aterm
(ShAAppl "pos-UNIT-DECL-DEFN" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML UNIT_DECL_DEFN where
(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)
ShAAppl "unit-decl" [aa,ab,ac] _ ->
let aa' = from_sml_ATermSIMPLE_ID $ getATermByIndex1 aa att
ab' = from_sml_ShATerm $ getATermByIndex1 ab att
ac' = from_sml_ATermUNIT_IMPORTS $
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
(ShAAppl "pos-UNIT-DECL-DEFN" [_,item_i] _) ->
getATermByIndex1 item_i att
---- a helper for the SML-datatype UNIT_IMPORTS ------------------------
from_sml_ATermUNIT_IMPORTS :: ATermTable -> [Annoted UNIT_TERM]
from_sml_ATermUNIT_IMPORTS att =
(ShAAppl "unit-imports" [ aa ] _) ->
from_sml_ShATerm $ getATermByIndex1 aa att
_ -> from_sml_ShATermError "UNIT_IMPORTS" aterm
where aterm = getATerm att'
(ShAAppl "pos-UNIT-IMPORTS" [_,item_i] _) ->
getATermByIndex1 item_i att
from_sml_ATermUNIT_DEFN :: ATermTable -> UNIT_DECL_DEFN
from_sml_ATermUNIT_DEFN att =
ShAAppl "unit-defn" [aa,ab] _ ->
let aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Unit_defn aa' ab' ac')
_ -> from_sml_ShATermError "UNIT_DEFN" aterm
where aterm = getATerm att'
(ShAAppl "pos-UNIT-DEFN" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
{- !!! This conversion is covered by the instance of LIB_ITEM !!!
instance ATermConvertibleSML UNIT_SPEC_DEFN where
instance ATermConvertibleSML UNIT_SPEC where
(ShAAppl "unit-type-case" [ aa ] _) ->
(aa',ab') = from_sml_ATermUNIT_TYPE $ getATermByIndex1 aa att
in (Unit_type aa' ab' ac')
(ShAAppl "spec-name-case" [ aa ] _) ->
aa' = from_sml_ATermIRI (getATermByIndex1 aa att)
(ShAAppl "closed" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in (Closed_unit_spec aa' ab')
_ -> from_sml_ShATermError "UNIT_SPEC" aterm
(ShAAppl "pos-UNIT-SPEC" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML REF_SPEC where
(ShAAppl "unit-type-case" [ aa ] _) ->
(aa',ab') = from_sml_ATermUNIT_TYPE $ getATermByIndex1 aa att
in Unit_spec $ Unit_type aa' ab' ac'
(ShAAppl "spec-name-case" [ aa ] _) ->
aa' = from_sml_ATermIRI (getATermByIndex1 aa att)
in (Unit_spec $ Spec_name aa')
(ShAAppl "arch-spec-case" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
aa'' = addLAnnoList ps aa'
(Annoted (Basic_arch_spec _ _ _) _ _ _) ->
Annoted (Group_arch_spec aa'' ab') nullRange [][]
in (Arch_unit_spec aa''' ab')
(ShAAppl "closed" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in (Unit_spec $ Closed_unit_spec aa' ab')
_ -> from_sml_ShATermError "UNIT_SPEC" aterm
(ShAAppl "pos-UNIT-SPEC" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
---- a helper for the SML-datatype UNIT_TYPE ----------------------------
from_sml_ATermUNIT_TYPE :: ATermTable -> ([Annoted SPEC],(Annoted SPEC))
from_sml_ATermUNIT_TYPE att =
(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'
(ShAAppl "pos-UNIT-TYPE" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML UNIT_EXPRESSION where
(ShAAppl "unit-expression" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Unit_expression aa' ab' ac')
_ -> from_sml_ShATermError "UNIT_EXPRESSION" aterm
(ShAAppl "pos-UNIT-EXPRESSION" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML UNIT_BINDING where
(ShAAppl "unit-binding" [ aa,ab ] _) ->
aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (Unit_binding aa' ab' ac')
_ -> from_sml_ShATermError "UNIT_BINDING" aterm
(ShAAppl "pos-UNIT-BINDING" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML UNIT_TERM where
(ShAAppl "unit-reduction" [ aa,ab ] _) ->
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 ] _) ->
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 ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in group (Amalgamation aa' ab') group_flag
(ShAAppl "local-unit" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in group (Local_unit aa' ab' ac') group_flag
(ShAAppl "unit-appl" [ aa,ab ] _) ->
aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in group (Unit_appl aa' ab' ac') group_flag
_ -> from_sml_ShATermError "UNIT_TERM" aterm
group ut gf = if gf then (Group_unit_term ut' pos_l) else ut
where ut' = Annoted ut nullRange [] []
(pos_l,group_flag,att') = skipPosFlag "pos-UNIT-TERM" att
instance ATermConvertibleSML FIT_ARG_UNIT where
(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
(ShAAppl "pos-FIT-ARG-UNIT" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
----- instances of
AS_LIbrary.hs ----------------------------------------
instance ATermConvertibleSML LIB_DEFN where
(ShAAppl "lib-defn" [ aa,ab,ad ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ad' = from_sml_ShATerm (getATermByIndex1 ad att)
in (Lib_defn aa' ab' ac' ad')
_ -> from_sml_ShATermError "LIB_DEFN" aterm
(ShAAppl "pos-LIB-DEFN" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
instance ATermConvertibleSML LIB_ITEM where
(ShAAppl "spec-defn" [ aa,ab,ac,ad ] _) ->
aa' = from_sml_ATermIRI (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
ac' = from_sml_ShATerm (getATermByIndex1 ac att)
ac''= addLAnnoList as ac'
(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']
(ShAAppl "arch-spec-defn" [ aa,ab,_ ] _) ->
aa' = from_sml_ATermSIMPLE_ID (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
(ShAAppl "unit-spec-defn" [ aa,ab,_ ] _) ->
aa' = from_sml_ATermIRI (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
(ShAAppl "download-items" [ aa,ab,_ ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
_ -> from_sml_ShATermError "LIB_ITEM" aterm
(pos_l,att') = skipPos "pos-LIB-ITEM" att
---- helpers to skip nested "pos-"-constructors -----------------------
skipPos :: String -> ATermTable -> (Range,ATermTable)
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
at' = getATermByIndex1 item_i at
skipPosFlag :: String -> ATermTable -> (Range,Bool,ATermTable)
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')
where pCon = case getATerm at' of
ShAAppl con' _ _ | mcon == con' -> True
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
ShAAppl "item-name" [aa] _ ->
aa' = from_sml_ATermIRI $ getATermByIndex1 aa att
in ItemNameMap aa' Nothing
ShAAppl "item-name-map" [aa, ab] _ ->
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
att' = case getATerm att of
ShAAppl "pos-ITEM-NAME-OR-MAP" [_, item_i] _ ->
getATermByIndex1 item_i att
instance ATermConvertibleSML LibName where
(ShAAppl "versioned-lib" [ aa,ab ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
ab' = from_sml_ShATerm (getATermByIndex1 ab att)
in (LibName aa' $ Just ab')
(ShAAppl "lib" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
_ -> from_sml_ShATermError "LibName" aterm
(ShAAppl "pos-LIB-NAME" [_,item_i] _) ->
getATermByIndex1 item_i att
instance ATermConvertibleSML LibId where
(ShAAppl "url" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
(ShAAppl "path-name" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in (IndirectLink aa' ab' "" noTime)
_ -> from_sml_ShATermError "LibName" aterm
(ShAAppl "pos-LIB-ID" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
-- nothing special implemented, since not used for CASL
instance ATermConvertibleSML IRI where
from_sml_ShATerm _ = nullIRI
instance ATermConvertibleSML VersionNumber where
(ShAAppl "version" [ aa ] _) ->
aa' = from_sml_ShATerm (getATermByIndex1 aa att)
in (VersionNumber aa' ab')
_ -> from_sml_ShATermError "VersionNumber" aterm
(ShAAppl "pos-VERSION" [reg_i,item_i] _) ->
(posFromRegion reg_i att,getATermByIndex1 item_i att)
-------------------------------------------------------------------------
-- some helpers for Annoted things --------------------------------------
addLAnnoList :: [Annotation] -> Annoted a -> Annoted a
addLAnnoList as ani = ani {l_annos = as ++ (l_annos ani) }
addRAnnoList :: [Annotation] -> Annoted a -> Annoted a
addRAnnoList as ani = ani {r_annos = (r_annos ani) ++ as }
--- some helpers for Regions and Positions ------------------------------
posFromRegion :: Int -> ATermTable -> Range
posFromRegion reg at = Range $ map ( \ (l, c) -> newPos "" l c )
$ from_sml_ATerm_reg reg at
getPos :: ATermTable -> Range
getPos att = case getATerm att of
ShAAppl _ (x:_) _ -> posFromRegion x att
-- 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
"wrong call: length of snd list must be even"
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 (setFstPos' tops) ids pos_l
where setFstPos' tops | null tops = []
| otherwise = (ftop):(tail tops)
where ftop = (head tops) { tokPos = Range [p] }
setFstPos _ _ = error "wrong call: setFstPos"