8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- --------------------------------------------------------------------------

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova HetCATS/CASL/Static.hs

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova $Id$

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova Authors: Pascal Schmidt

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina Sojakova Year: 2002

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu-----------------------------------------------------------------------------

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova SUMMARY

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova This modules provides static analysis for the BASIC_SPEC datatype

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova found in AS_Basic_CASL

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-----------------------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova TODO

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova datatypes

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Speicherzugriffsfehler bei Analyse von

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sort Nat

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova preds even: Nat

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova deshalb gibt basic_analysis erstmal nur triviale Werte zur�ck

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-------------------------------------------------------------------------- -}

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova-----------------------------------------------------------------------------

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova-- Export declarations

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-----------------------------------------------------------------------------

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovamodule CASL.Static {-( basicAnalysis, statSymbMapItems, statSymbItems,

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova symbolToRaw, idToRaw, symOf, symmapOf, matches,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova isSubSig, symName )-} where

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova------------------------------------------------------------------------------

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- Imports from other modules

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Data.Maybe

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Control.Monad(foldM) -- instead of foldResult

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Lib.Map hiding (map, filter)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Prelude hiding (lookup)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Common.Lib.Set as Set

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Common.Id

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.AS_Annotation

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.GlobalAnnotations

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.GlobalAnnotationsFunctions

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport CASL.AS_Basic_CASL

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.Sign

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Result

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.Latin

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Utils

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Logic.Logic ( EndoMap )

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova------------------------------------------------------------------------------

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova--

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- Datatypes

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova--

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova------------------------------------------------------------------------------

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovatype Filename = String

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovadata GlobalVars = Global { global :: [VarDecl] }

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova deriving (Eq,Show)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovadata NamedSentence = NamedSen { senName :: String,

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova sentence :: Sentence }

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova deriving (Eq,Show)

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovadata Sentences = Sentences { sentences :: [NamedSentence] }

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova deriving (Eq,Show)

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovadata LocalEnv = Env { getName :: Filename,

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder getGA :: GlobalAnnos,

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova getSign :: Sign,

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder getPsi :: Sentences,

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova getGlobal :: GlobalVars }

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova deriving Show

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata SigLocalEnv = SigEnv { localEnv :: LocalEnv,

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova selectors :: [Annoted OpItem],

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova w :: Map Symbol [Symbol],

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova flag :: Bool }

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovadata Annotations = Annotations { annosOptPos :: [Pos],

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder annosLeft, annosRight :: [Annotation] }

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakovatype ExtPos = (Pos, TokenKind)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova--

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- Helper functions

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova--

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder-- helper functions on datatypes

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder------------------------------------------------------------------------------

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatoAnnotations :: Annoted a -> Annotations

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatoAnnotations a = Annotations (opt_pos a) (l_annos a) (r_annos a)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatoAnnoted :: a ->Annotations -> Annoted a

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatoAnnoted a (Annotations x y z) = Annoted a x y z

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatoSigLocalEnv :: LocalEnv -> SigLocalEnv

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatoSigLocalEnv env = SigEnv env [] empty False

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyGlobal :: GlobalVars

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyGlobal = Global []

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptySentences :: Sentences

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptySentences = Sentences []

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyLocalEnv :: LocalEnv

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyLocalEnv =

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova Env "empty" emptyGlobalAnnos emptySign emptySentences emptyGlobal

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyExtPos :: ExtPos

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyExtPos = (nullPos, Key)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyAnnotations :: Annotations

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyAnnotations = Annotations [] [] []

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaflattenSentences :: Sentences -> [(String, Sentence)]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaflattenSentences sens = map (\x -> (senName x,sentence x)) (sentences sens)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaaddNamedSentences :: Sentences -> [NamedSentence] -> Sentences

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaaddNamedSentences (Sentences s) l = Sentences (setAdd s l)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovamyShowList :: Show a => [a] -> String

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovamyShowList [] = "[]"

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovamyShowList [h] = "'" ++ show h ++ "'"

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovamyShowList (h:t) = "'" ++ (show h) ++ "', " ++ (myShowList t)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyFilename :: Filename

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyFilename = ""

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovacloneAnnos :: Annoted a -> b -> Annoted b

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovacloneAnnos a b = a { item = b }

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

12d9bff7c82145a8b68bfb8553688172655c926eKristina SojakovalabelAnno :: String -> b -> Annoted b

12d9bff7c82145a8b68bfb8553688172655c926eKristina SojakovalabelAnno name itm = Annoted itm [] [] [Label [name] []]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovanoAnnos :: a -> Annoted a

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovanoAnnos itm = toAnnoted itm emptyAnnotations

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaemptyAnnos :: Annoted ()

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovaemptyAnnos = noAnnos ()

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovaannoFilter :: Annotation -> Maybe Annotation

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovaannoFilter x = case x of Label _ _ -> Just x;

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova _ -> Nothing

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovacloneAnnoFormula :: Annoted a -> b -> Annoted b

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovacloneAnnoFormula a b = Annoted b [] (mapMaybe annoFilter $ l_annos a)

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder (mapMaybe annoFilter $ r_annos a)

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovamergeAnnos :: Annoted a -> Annoted b -> Annoted b

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovamergeAnnos a b = b { opt_pos = setAdd (opt_pos a) (opt_pos b),

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova l_annos = setAdd (l_annos a) (l_annos b),

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova r_annos = setAdd (r_annos a) (r_annos b) }

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova------------------------------------------------------------------------------

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- special functions to generate token lists from Pos lists

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova------------------------------------------------------------------------------

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovatoExtPos :: Maybe ExtPos -> [Pos] -> ([Pos] -> [TokenKind]) -> [ExtPos]

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovatoExtPos pref p f = let

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova tokens = (zip p (f p))

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova in

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova case pref of Nothing -> tokens

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova Just ep -> ep:tokens

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedertokPos_sort_decl :: [Pos] -> [TokenKind]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatokPos_sort_decl l = replicate (length l) Comma

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatokPos_subsort_decl :: [Pos] -> [TokenKind]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatokPos_subsort_decl [] = []

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovatokPos_subsort_decl (_:t) = (replicate (length t) Comma) ++ [Less]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovatokPos_subsort_defn :: [Pos] -> [TokenKind]

b470a3e54a4289b4189906e41f0c04578c85619dKristina SojakovatokPos_subsort_defn _ = [Equal,Key,Colon,Comma,Key]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovatokPos_iso_decl :: [Pos] -> [TokenKind]

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovatokPos_iso_decl l = replicate (length l) Colon

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_SORT_ITEM :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_SORT_ITEM [] = []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_SORT_ITEM (_:t) = Key:(replicate (length t) Semi)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovatokPos_pred_decl :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_pred_decl [] = []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_pred_decl (_:t) = (replicate (length t) Comma) ++ [Colon]

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_VAR_DECL :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_VAR_DECL = tokPos_pred_decl

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_pred_defn :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_pred_defn _ = [Key]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_ARG_DECL :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_ARG_DECL = tokPos_pred_decl

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovatokPos_ARG_DECL_list :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_ARG_DECL_list [] = []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_ARG_DECL_list [_] = []

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovatokPos_ARG_DECL_list (_:(_:t)) = (Key:(replicate (length t) Semi)) ++ [Key]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_PRED_ITEM :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_PRED_ITEM = tokPos_SORT_ITEM

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovatokPos_VAR_ITEM :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_VAR_ITEM = tokPos_SORT_ITEM

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_local_var_axioms :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_local_var_axioms [] = []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_local_var_axioms (_:t) = Key:(replicate (length t) Key)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovatokPos_axiom_items :: [Pos] -> [TokenKind]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_axiom_items = tokPos_local_var_axioms

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_select :: [Pos] -> [TokenKind]

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovatokPos_select = tokPos_pred_decl

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovatokPos_construct :: [Pos] -> [TokenKind]

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovatokPos_construct = tokPos_SORT_ITEM

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatokPos_subsorts :: [Pos] -> [TokenKind]

a3a6b6ebe9c2d1dc3554e44779dc7361a90e7617Kristina SojakovatokPos_subsorts [] = []

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovatokPos_subsorts (_:t) = Key:(replicate (length t) Comma)

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovatokPos_DATATYPE_DECL :: [Pos] -> [TokenKind]

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovatokPos_DATATYPE_DECL l = replicate (length l) Key

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedertokPos_datatype_items :: [Pos] -> [TokenKind]

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovatokPos_datatype_items = tokPos_SORT_ITEM

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovatokPos_OP_ITEM :: [Pos] -> [TokenKind]

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovatokPos_OP_ITEM = tokPos_SORT_ITEM

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova------------------------------------------------------------------------------

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- functions to generate labels

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova------------------------------------------------------------------------------

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovasomeLabel :: String -> Annoted a -> String

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovasomeLabel def x =

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova let

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova labels = filter (\y -> case y of (Label _ _) -> True;

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova _ -> False)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova ((l_annos x)++(r_annos x))

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova in

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova case labels of ((Label s _):_) -> concat s;

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova _ -> def

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedertoLabel :: Show a => a -> String

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovatoLabel x = toASCII $ show x

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- conversion from simple to compound datatypes

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoListPos :: ExtPos -> ListPos

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoListPos (pos,tok) = ListPos tok pos

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoItemPos :: Filename -> ExtPos -> ItemPos

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoItemPos name (pos,tok) = ItemPos name tok [pos]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovafromItemPos :: ItemPos -> ExtPos

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovafromItemPos (ItemPos _ kind []) = (nullPos,kind)

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederfromItemPos (ItemPos _ kind l) = (head l,kind)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedertoVarDecl :: SortId -> ExtPos -> VAR -> VarDecl

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoVarDecl sort pos var = VarDecl var sort (toListPos pos)

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoVarDecls :: SortId -> [ExtPos] -> [VAR] -> [VarDecl]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoVarDecls sort p v = map (uncurry (toVarDecl sort))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (zip (extendList emptyExtPos v p) v)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatypeToVarDecl :: OpType -> [VarDecl]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatypeToVarDecl t = map (\(s,v) -> VarDecl v s (ListPos Key nullPos))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ zip (opArgs t) $ map mkSimpleId $ map (\x -> "x" ++ x)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ map show $ [1..(length $ opArgs t)]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedertoVarId :: VarDecl -> Term

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoVarId v = VarId (simpleIdToId $ varId v) (varSort v) Inferred []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaopToApplSentence :: OpItem -> [NamedSentence]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaopToApplSentence itm =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova name = case (opId itm) of Id [Token n _] [] [] -> n;

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova _ -> ""

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova optype = opType itm

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova vars = typeToVarDecl optype

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova terms = map toVarId vars

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova res = opRes optype

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder [NamedSen name

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (Axiom (noAnnos (AxiomDecl vars (ElemTest (OpAppl (opId itm) optype terms

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder Inferred []) res []) [])))]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoGenItems :: [OpItem] -> [Pos] -> NamedSentence

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoGenItems ops pos = NamedSen ""

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (GenItems (map (\x -> Symbol (opId x)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (OpAsItemType (opType x))) ops) pos)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoFunKind :: Bool -> FunKind

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoFunKind False = Partial

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoFunKind _ = Total

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasortToSymbol :: SortId -> Symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasortToSymbol s = Symbol s CASL.Sign.Sort

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederopTypeIdToSymbol :: OpType -> Id -> Symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaopTypeIdToSymbol typ idt = Symbol idt (OpAsItemType typ)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoNamedSentence :: [VarDecl] -> String -> Annoted Formula -> NamedSentence

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoNamedSentence vars str f =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova NamedSen str

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (Axiom (cloneAnnos f (AxiomDecl vars (item f) [])))

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- foldTwo: foldResult function over two lists

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- makes sure second list is at least as long as the first

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- add a default element if not

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- foldPos: same for foldl

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova------------------------------------------------------------------------------

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaextendList :: b -> [a] -> [b] -> [b]

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaextendList def a b = if ((length b) < (length a)) then

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova b ++ replicate ((length a)-(length b)) def

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova else b

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovafoldTwo :: a -> c -> (a -> b -> c -> Result a) -> [b] -> [c] -> Result a

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovafoldTwo state def f a b = foldM (\st (x, y) -> f st x y) state

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova (zip a (extendList def a b))

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovafoldlTwo :: c -> (a -> b -> c -> a) -> a -> [b] -> [c] -> a

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovafoldlTwo def f ini a b = foldl (\st (x, y) -> f st x y) ini

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (zip a (extendList def a b))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovafoldPos :: (Sign -> a -> ExtPos -> Sign) -> Sign -> [a] -> [ExtPos] -> Sign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovafoldPos f sigma a pos = foldlTwo emptyExtPos f sigma a pos

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovachainPos :: b -> (b -> a -> ExtPos -> Result b) -> [a] -> [ExtPos] -> [Pos]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -> ([Pos] -> [TokenKind]) -> Result b

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovachainPos env f items positions addPos toStrFun =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova foldTwo env emptyExtPos f items (positions ++ (zip addPos (toStrFun addPos)))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- element test and selector functions for SigItem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova------------------------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasElem :: Sign -> (Id -> SigItem -> Bool) -> Id -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasElem sigma f idt =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova res = lookup idt (getMap sigma)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova if (isJust res) then

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova or $ map (f idt) (fromJust res)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova False

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetElem :: Sign -> (Id -> SigItem -> Bool) -> Id -> Maybe SigItem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetElem sigma f idt =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova if (hasElem sigma f idt) then

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just (head $ filter (f idt) $ fromJust $ lookup idt $ getMap sigma)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigSortItem :: Id -> SigItem -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigSortItem idt (ASortItem s) = (sortId $ item s)==idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigSortItem _ _ = False

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigOpItem :: Id -> SigItem -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigOpItem idt (AnOpItem o) = (opId $ item o)==idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigOpItem _ _ = False

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigPredItem :: Id -> SigItem -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigPredItem idt (APredItem p) = (predId $ item p)==idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisSigPredItem _ _ = False

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoSortItem :: Maybe SigItem -> Maybe (Annoted SortItem)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoSortItem (Just (ASortItem s)) = Just s

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoSortItem _ = Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoOpItem :: Maybe SigItem -> Maybe (Annoted OpItem)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoOpItem (Just (AnOpItem o)) = Just o

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoOpItem _ = Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoPredItem :: Maybe SigItem -> Maybe (Annoted PredItem)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatoPredItem (Just (APredItem p)) = Just p

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovatoPredItem _ = Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasSort :: Sign -> SortId -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasSort sigma idt = hasElem sigma isSigSortItem idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasOp :: Sign -> Id -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasOp sigma idt = hasElem sigma isSigOpItem idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasPred :: Sign -> Id -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasPred sigma idt = hasElem sigma isSigPredItem idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalookupSort :: Sign -> SortId -> Maybe (Annoted SortItem)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalookupSort sigma idt = toSortItem $ getElem sigma isSigSortItem idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalookupOp :: Sign -> Id -> Maybe (Annoted OpItem)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalookupOp sigma idt = toOpItem $ getElem sigma isSigOpItem idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalookupPred :: Sign -> Id -> Maybe (Annoted PredItem)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalookupPred sigma idt = toPredItem $ getElem sigma isSigPredItem idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetSort :: Sign -> SortId -> Annoted SortItem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetSort sigma idt = fromJust $ lookupSort sigma idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetOp :: Sign -> Id -> Annoted OpItem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetOp sigma idt = fromJust $ lookupOp sigma idt

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovagetPred :: Sign -> Id -> Annoted PredItem

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovagetPred sigma idt = fromJust $ lookupPred sigma idt

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova------------------------------------------------------------------------------

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova-- update function for SigItem in Sign

7caaddef0ccffd5528a7cde7cb0b7161250f4e59Kristina Sojakova------------------------------------------------------------------------------

7caaddef0ccffd5528a7cde7cb0b7161250f4e59Kristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovaupdateSigItem :: Sign -> Id -> SigItem -> Sign

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovaupdateSigItem sigma idt itm =

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova let

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova res = lookup idt $ getMap sigma

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova new = if (isNothing res) then

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova [itm]

else

[ x | x<-(fromJust res), x /= itm ] ++ [itm]

in

sigma { getMap = insert idt new (getMap sigma)}

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

-- functions for SortItem generation and modification

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

addSuper :: SortRels -> Bool -> [SortId] -> SortRels

addSuper rels _ [] = rels

addSuper rels direct (idt:allid) =

if direct then

rels { supersorts = setAddOne (supersorts rels) idt,

allsupersrts = setAdd (allsupersrts rels) (idt:allid) }

else

rels { allsupersrts = setAdd (allsupersrts rels) (idt:allid) }

addSub :: SortRels -> Bool -> [SortId] -> SortRels

addSub rels _ [] = rels

addSub rels direct (idt:allid) =

if direct then

rels { subsorts = setAddOne (subsorts rels) idt,

allsubsrts = setAdd (allsubsrts rels) (idt:allid) }

else

rels { allsubsrts = setAdd (allsubsrts rels) (idt:allid) }

addSubsort :: SortId -> Sign -> SortId -> Sign

addSubsort super sigma sub =

let

subItem = getSort sigma sub

allSubs = allsubsrts $ sortRels $ item subItem

superItem = getSort sigma super

allSupers = allsupersrts $ sortRels $ item superItem

newSub = ASortItem (subItem { item = (item subItem)

{ sortRels =

addSuper (sortRels $ item subItem) True (super:allSupers)}})

newSuper = ASortItem (superItem { item = (item superItem)

{ sortRels =

addSub (sortRels $ item superItem) True (sub:allSubs) }})

withSub = updateSigItem (updateSigItem sigma sub newSub) super newSuper

iterSuper = foldl (addSubsorts (sub:allSubs)) withSub allSupers

in

foldl (addSupersorts (super:allSupers)) iterSuper allSubs

addSubsorts :: [SortId] -> Sign -> SortId -> Sign

addSubsorts subs sigma super =

let

res = getSort sigma super

new = res { item = (item res)

{ sortRels =

addSub (sortRels $ item res) False subs } }

in

updateSigItem sigma super (ASortItem new)

addSupersorts :: [SortId] -> Sign -> SortId -> Sign

addSupersorts supers sigma sub =

let

res = getSort sigma sub

new = res { item = (item res)

{ sortRels =

addSuper (sortRels $ item res) False supers } }

in

updateSigItem sigma sub (ASortItem new)

addIsoSubsorting :: [SortId] -> Sign -> SortId -> Sign

addIsoSubsorting sorts sigma sort =

let

others = [ x | x<-sorts, x/=sort ]

res = getSort sigma sort

old = sortRels $ item res

new = old { subsorts = setAdd (subsorts old) others,

supersorts = setAdd (supersorts old) others,

allsubsrts = setAdd (allsubsrts old) others,

allsupersrts = setAdd (allsupersrts old) others }

ext = (item res) { sortRels = new }

in

updateSigItem sigma sort (ASortItem (res { item = ext }))

updateSortItem :: Filename -> Annoted a -> Maybe SortDefn -> Sign -> SortId

-> ExtPos -> Sign

updateSortItem name ann defn sigma idt kwpos =

let

res = lookupSort sigma idt

pos = toItemPos name kwpos

new = if (isJust res) then

let

itm = fromJust res

old = item itm

in

mergeAnnos itm (cloneAnnos ann

old { sortDef = case defn of Nothing -> sortDef old;

x -> x,

sortPos = pos,

altSorts = (altSorts old) ++ [sortPos old] })

else

cloneAnnos ann (SortItem idt emptySortRels defn pos [])

in

updateSigItem sigma idt (ASortItem new)

updateSortDefn :: Sign -> SortId -> Maybe SortDefn -> Sign

updateSortDefn sigma idt defn =

let

res = getSort sigma idt

new = res { item = (item res) { sortDef = defn } }

in

updateSigItem sigma idt (ASortItem new)

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

-- PredItem generation

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

updatePredItem :: Filename -> Annoted PRED_ITEM -> PredType -> Maybe PredDefn

-> Sign -> Id -> ExtPos -> Sign

updatePredItem name ann typ defn sigma idt pos =

let

res = lookupPred sigma idt

ppos = toItemPos name pos

new = if (isJust res) then

let

old = fromJust res

itm = item old

in

mergeAnnos old (cloneAnnos ann

itm { predDefn = case defn of Nothing -> predDefn itm;

Just x -> Just x,

predPos = ppos,

altPreds = (altPreds itm) ++ [predPos itm] })

else

cloneAnnos ann (PredItem idt typ defn ppos [])

in

updateSigItem sigma idt (APredItem new)

updatePredDefn :: Sign -> Id -> Maybe PredDefn -> Sign

updatePredDefn sigma idt defn =

let

res = getPred sigma idt

new = res { item = (item res) { predDefn = defn } }

in

updateSigItem sigma idt (APredItem new)

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

-- OpItem generation

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

updateOpItem :: Filename -> Annoted a -> OpType -> Maybe OpDefn -> [OpAttr]

-> Sign -> Id -> ExtPos -> Sign

updateOpItem name ann typ defn attr sigma idt pos =

let

res = lookupOp sigma idt

opos = toItemPos name pos

new = if (isJust res) then

let

old = fromJust res

itm = item old

in

mergeAnnos old (cloneAnnos ann

itm { opDefn = case defn of Nothing -> opDefn itm;

x -> x,

opAttrs = setAdd (opAttrs itm) attr,

opPos = opos,

altOps = (altOps itm) ++ [opPos itm] })

else

cloneAnnos ann (OpItem idt typ attr defn opos [])

in

updateSigItem sigma idt (AnOpItem new)

updateOpItems :: Filename -> Sign -> [Annoted OpItem] -> Sign

updateOpItems _ sigma [] = sigma

updateOpItems fn sigma

(ann@(Annoted (OpItem idt typ attr defn pos _) _ _ _):t) =

updateOpItems fn (updateOpItem fn ann typ defn attr sigma idt

(fromItemPos pos)) t

mergeOpDefn :: Maybe OpDefn -> OpDefn -> OpDefn

mergeOpDefn Nothing x = x

mergeOpDefn (Just y) x =

case x of OpDef _ _ _ -> x

Constr _ -> x

Select l1 s -> (case y of Select l2 _ -> Select (setAdd l1 l2) s

_ -> x)

updateOpDefn :: Sign -> Id -> OpDefn -> Sign

updateOpDefn sigma idt defn =

let

res = getOp sigma idt

new = res { item = (item res) { opDefn = Just (mergeOpDefn

(opDefn $ item res) defn) } }

in

updateSigItem sigma idt (AnOpItem new)

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

--

-- Static Analysis

-- BASIC-SPEC

--

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

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

-- FORMULA

-- FIXME, dummy implementation

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

ana_FORMULA :: LocalEnv -> Annoted FORMULA -> Result (Annoted Formula)

ana_FORMULA _ f = return (cloneAnnoFormula f (TrueAtom []))

ana_no_anno_FORMULA :: LocalEnv -> Annoted FORMULA -> Result Formula

ana_no_anno_FORMULA sigma f = ana_FORMULA sigma f >>= (return . item)

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

-- SORT-DECL

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

ana_sort_decl :: LocalEnv -> Annoted SORT_ITEM -> [SortId] -> [ExtPos]

-> Result LocalEnv

ana_sort_decl sigma _itm s _pos =

return sigma { getSign = foldPos (updateSortItem (getName sigma) _itm

Nothing) (getSign sigma) s _pos }

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

-- SUBSORT-DECL

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

checkSubsDistinctSuper :: Pos -> [SortId] -> SortId -> Result ()

checkSubsDistinctSuper _pos s_n s =

if (s `notElem` s_n) then

return ()

else

fatal_error "subsort not distinct from supersort" _pos

ana_subsort_decl :: LocalEnv -> Annoted SORT_ITEM -> Maybe SortDefn -> [SortId]

-> SortId -> [ExtPos] -> Result LocalEnv

ana_subsort_decl sigma _itm _defn s_n s _pos =

do checkSubsDistinctSuper (fst $ head _pos) s_n s

let _delta = foldPos (updateSortItem (getName sigma) _itm _defn)

(getSign sigma) (s:s_n) _pos

let embedRel = foldl (addSubsort s) _delta s_n

return sigma { getSign = embedRel }

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

-- SUBSORT-DEFN

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

subsortLabel :: SortId -> SortId -> String

subsortLabel s s' = "ga_subsort_defn_" ++ (toLabel s) ++ "_"

++ (toLabel s') ++ "_"

checkSortExists :: LocalEnv -> Pos -> SortId -> Result ()

checkSortExists sigma _pos s' =

if ((getSign sigma) `hasSort` s') then

return ()

else

fatal_error ("sort '"++(show s')++"' is not declared") _pos

ana_subsort_defn :: LocalEnv -> Annoted SORT_ITEM -> SortId -> VAR -> SortId

-> Annoted FORMULA -> [ExtPos] -> Result LocalEnv

ana_subsort_defn sigma _itm s v s' f _pos =

let

_colpos = head $ drop 3 _pos

f' = cloneAnnoFormula f (Quantification Universal [(Var_decl [v] s'

[fst _colpos])] (Equivalence (item f) (Membership

(Simple_id v) s []) []) [])

in

do checkSortExists sigma (fst $ head _pos) s'

_f <- ana_no_anno_FORMULA sigma f

let _defn = SubsortDefn (toVarDecl s' _colpos v) _f

(map fst $ tail _pos)

delta <- ana_subsort_decl sigma _itm (Just _defn) [s] s' _pos

_f' <- ana_FORMULA delta { getGlobal = emptyGlobal } f'

let phi = toNamedSentence [] (someLabel (subsortLabel s s') f) _f'

return delta { getPsi = addNamedSentences (getPsi delta) [phi] }

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

-- ISO-DECL

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

checkAllUnique :: Pos -> [SortId] -> Result ()

checkAllUnique _pos s_n =

if (allUnique s_n) then

return ()

else

fatal_error ("multiple occurences of sort(s): "

++ (myShowList $ notUnique s_n)) _pos

checkGreaterOrEqualTwo :: Pos -> [SortId] -> Result ()

checkGreaterOrEqualTwo _pos s_n =

if ((length s_n)>=2) then

return ()

else

fatal_error "single sort in isomorphism decl" _pos

ana_iso_decl :: LocalEnv -> Annoted SORT_ITEM -> [SortId] -> [ExtPos]

-> Result LocalEnv

ana_iso_decl sigma _itm s_n _pos =

do checkAllUnique (fst $ head _pos) s_n

checkGreaterOrEqualTwo (fst $ head _pos) s_n

let _delta = foldPos (updateSortItem (getName sigma) _itm Nothing)

(getSign sigma) s_n _pos

let embedRel = foldl (addIsoSubsorting s_n) _delta s_n

return sigma { getSign = embedRel }

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

-- SORT-ITEM

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

ana_SORT_ITEM :: LocalEnv -> Annoted SORT_ITEM -> ExtPos -> Result LocalEnv

ana_SORT_ITEM sigma _itm _pos =

case (item _itm) of

(Sort_decl s_n _p)

-> ana_sort_decl sigma _itm s_n

(toExtPos (Just _pos) _p tokPos_sort_decl)

(Subsort_decl s_n s _p)

-> ana_subsort_decl sigma _itm Nothing s_n s

(toExtPos (Just _pos) _p tokPos_subsort_decl)

(Subsort_defn s v s' f _p)

-> ana_subsort_defn sigma _itm s v s' f

(toExtPos (Just _pos) _p tokPos_subsort_defn)

(Iso_decl s_n _p)

-> ana_iso_decl sigma _itm s_n

(toExtPos (Just _pos) _p tokPos_iso_decl)

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

-- PRED-DECL

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

ana_PRED_TYPE' :: LocalEnv -> PredType -> PRED_TYPE -> ExtPos

-> Result PredType

ana_PRED_TYPE' _ w' (Pred_type [] _) _pos = return w'

ana_PRED_TYPE' sigma w' (Pred_type (s_n:_t) _) _pos =

do checkSortExists sigma (fst _pos) s_n

ana_PRED_TYPE' sigma (w'++[s_n]) (Pred_type _t []) _pos

ana_PRED_TYPE :: LocalEnv -> PRED_TYPE -> ExtPos -> Result PredType

ana_PRED_TYPE sigma _t _pos = ana_PRED_TYPE' sigma [] _t _pos

ana_pred_decl :: LocalEnv -> Annoted PRED_ITEM -> [PRED_NAME] -> PRED_TYPE

-> [ExtPos] -> Result LocalEnv

ana_pred_decl sigma _itm p_n _t _pos =

do w' <- ana_PRED_TYPE sigma _t (head _pos)

let delta = foldPos (updatePredItem (getName sigma) _itm w' Nothing)

(getSign sigma) p_n _pos

return sigma { getSign = delta }

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

-- PRED-DEFN

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

predDefnLabel :: PRED_NAME -> [VarDecl] -> String

predDefnLabel n v = "ga_pred_defn_" ++ (toLabel n) ++ "_" ++

(concat $ map (\x -> toLabel (varId x) ++ "_") v)

checkVarsUnique :: [VAR] -> Pos -> Result ()

checkVarsUnique x_n _pos =

if (allUnique x_n) then

return ()

else

fatal_error ("variables not unique in arg-decl: (" ++

(myShowList $ notUnique x_n) ++ ")") _pos

ana_ARG_DECL :: LocalEnv -> [VAR] -> SortId -> [ExtPos]

-> Result ([VAR],SortId)

ana_ARG_DECL sigma x_n s _pos =

do checkSortExists sigma (fst $ last _pos) s

checkVarsUnique x_n (fst $ head _pos)

return (x_n,s)

checkQualVarsUnique :: Pos -> [VarDecl] -> [VarDecl] -> Result ()

checkQualVarsUnique _pos a b =

if (allUnique (a++b)) then

return ()

else

fatal_error "overlapping variable names" _pos

ana_ARG_DECL_list' :: LocalEnv -> ([VarDecl],[SortId]) -> [ARG_DECL]

-> Result ([VarDecl],[SortId])

ana_ARG_DECL_list' _ (x_s_n,w') [] = return (x_s_n,w')

ana_ARG_DECL_list' sigma (x_s_n,w') ((Arg_decl _v _s _pos):_t) =

do let _extPos = zip _pos (tokPos_ARG_DECL _pos)

(x_n,s) <- ana_ARG_DECL sigma _v _s _extPos

let _qual = toVarDecls s _extPos x_n

checkQualVarsUnique (head _pos) x_s_n _qual

ana_ARG_DECL_list' sigma (x_s_n ++ _qual,w' ++ [s]) _t

ana_ARG_DECL_list :: LocalEnv -> [ARG_DECL] -> Result ([VarDecl],[SortId])

ana_ARG_DECL_list sigma _ad = ana_ARG_DECL_list' sigma ([],[]) _ad

ana_pred_defn :: LocalEnv -> Annoted PRED_ITEM -> PRED_NAME -> PRED_HEAD

-> Annoted FORMULA -> [ExtPos] -> Result LocalEnv

ana_pred_defn sigma _ann p (Pred_head _ad _pos') _f _pos =

do (_x_s_n,w') <- ana_ARG_DECL_list sigma _ad

let _delta' = updatePredItem (getName sigma) _ann w' Nothing

(getSign sigma) p (head _pos)

phi <- ana_no_anno_FORMULA (sigma { getSign = _delta',

getGlobal = Global _x_s_n }) _f

let _defn = PredDef _x_s_n phi (_pos' ++ [(fst $ last _pos)])

let delta = updatePredDefn _delta' p (Just _defn)

return sigma { getSign = delta,

getPsi = addNamedSentences (getPsi sigma)

[toNamedSentence [] (someLabel

(predDefnLabel p (_x_s_n)) _f)

(cloneAnnos _f (Quantified Forall _x_s_n

(Connect EquivOp [PredAppl p w'

(map toVarId _x_s_n) Inferred [],phi]

[])[]))] }

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

-- PRED-ITEM

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

ana_PRED_ITEM :: LocalEnv -> Annoted PRED_ITEM -> ExtPos -> Result LocalEnv

ana_PRED_ITEM sigma _itm _pos =

case (item _itm) of

(Pred_decl p_n _t _p) -> ana_pred_decl sigma _itm p_n _t

(toExtPos (Just _pos) _p tokPos_pred_decl)

(Pred_defn p _h _f _p) -> ana_pred_defn sigma _itm p _h _f

(toExtPos (Just _pos) _p tokPos_pred_defn)

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

-- OP-ITEMS

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

ana_OP_ITEM :: LocalEnv -> Annoted OP_ITEM -> ExtPos -> Result LocalEnv

ana_OP_ITEM sigma _itm _pos =

return sigma

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

-- DATATYPE-ITEMS

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

sig_COMPONENTS :: COMPONENTS -> [SortId]

sig_COMPONENTS (Total_select f_n s' _) = replicate (length f_n) s'

sig_COMPONENTS (Partial_select f_n s' _) = replicate (length f_n) s'

sig_COMPONENTS (CASL.AS_Basic_CASL.Sort s' ) = [s']

sig_COMPONENTS_list :: [COMPONENTS] -> [SortId]

sig_COMPONENTS_list l = concat $ map sig_COMPONENTS l

sig_ALTERNATIVE :: SortId -> Sign -> ALTERNATIVE -> Sign

sig_ALTERNATIVE s sigma (Total_construct f components_list _) =

updateOpItem emptyFilename emptyAnnos

(OpType Total (sig_COMPONENTS_list components_list) s)

Nothing [] sigma f emptyExtPos

sig_ALTERNATIVE s sigma (Partial_construct f components_list _) =

updateOpItem emptyFilename emptyAnnos

(OpType Partial (sig_COMPONENTS_list components_list) s)

Nothing [] sigma f emptyExtPos

sig_ALTERNATIVE _ sigma (Subsorts _ _) = sigma

sig_ALTERNATIVE_list :: Sign -> SortId -> [ALTERNATIVE] -> Sign

sig_ALTERNATIVE_list sigma s l = foldl (sig_ALTERNATIVE s) sigma l

sig_DATATYPE_DECL :: Sign -> DATATYPE_DECL -> Sign

sig_DATATYPE_DECL sigma (Datatype_decl s alternative_list _) =

updateSortItem emptyFilename emptyAnnos Nothing

(sig_ALTERNATIVE_list sigma s (map item alternative_list))

s emptyExtPos

ana_select :: Annotations -> SortId -> Id -> OpType

-> (SigLocalEnv, [Component]) -> [Id] -> SortId -> [Pos]

-> FunKind -> ExtPos -> (SigLocalEnv, [Component])

ana_select ann s f ws (sigma,c) f_n s' pos kind top_pos =

let

optype = OpType kind [opRes ws] s'

in

(sigma { selectors = (selectors sigma) ++

(map (\(x,p) -> toAnnoted

(OpItem x optype []

(Just (Select [opTypeIdToSymbol ws f]

(idToSortSymbol s)))

(toItemPos (getName $ localEnv sigma) p)

[]) ann)

(zip f_n (toExtPos Nothing pos

tokPos_select))) },

c ++ (map (\x -> Component (Just x) optype

(Just (toListPos top_pos))) f_n));

ana_COMPONENTS :: Annotations -> SortId -> Id -> OpType

-> (SigLocalEnv, [Component]) -> COMPONENTS -> ExtPos

-> Result (SigLocalEnv, [Component])

ana_COMPONENTS ann s f ws (sigma,c) components top_pos =

return

(case components of

Total_select f_n s' pos

-> ana_select ann s f ws (sigma,c) f_n s' pos Total top_pos

Partial_select f_n s' pos

-> ana_select ann s f ws (sigma,c) f_n s' pos Partial top_pos

CASL.AS_Basic_CASL.Sort s'

-> (sigma,c ++ [Component Nothing (OpType Total [s'] s)

(Just (toListPos top_pos))]))

ana_subsort :: Annoted ALTERNATIVE -> (SigLocalEnv, [Annoted Alternative])

-> SortId -> ExtPos

-> Result (SigLocalEnv, [Annoted Alternative])

ana_subsort ann (sigma,alternatives) s_n pos =

do checkSortExists (localEnv sigma) (fst pos) s_n

return (sigma { flag = True },

alternatives ++ [cloneAnnos ann (Subsort s_n (toListPos pos))])

ana_construct :: Annoted ALTERNATIVE

-> Sign -> SortId -> (SigLocalEnv, [Annoted Alternative])

-> Id -> [COMPONENTS] -> [Pos] -> ExtPos

-> Result (SigLocalEnv, [Annoted Alternative])

ana_construct ann sigma' s (sigma,alternatives) f components pos top_pos =

let

ws = opType $ item $ getOp sigma' f

annos = toAnnotations ann

in

do (delta,c) <- chainPos (sigma,[]) (ana_COMPONENTS annos s f ws)

components [top_pos] pos tokPos_construct

return (delta { localEnv = (localEnv delta)

{ getSign = updateOpItem (getName $ localEnv delta)

ann ws

(Just (Constr

(idToSortSymbol s)))

[]

(getSign $ localEnv delta)

f top_pos } },

alternatives ++ [toAnnoted (Construct f ws c pos) annos])

ana_ALTERNATIVE :: Sign -> SortId -> (SigLocalEnv, [Annoted Alternative])

-> Annoted ALTERNATIVE -> ExtPos

-> Result (SigLocalEnv, [Annoted Alternative])

ana_ALTERNATIVE sigma' s (sigma,alternatives) alternative top_pos =

case (item alternative) of

Total_construct f components pos

-> ana_construct alternative sigma' s (sigma,alternatives) f

components pos top_pos

Partial_construct f components pos

-> ana_construct alternative sigma' s (sigma,alternatives) f

components pos top_pos

Subsorts sorts pos

-> chainPos (sigma,alternatives) (ana_subsort alternative) sorts

[top_pos] pos tokPos_subsorts

ana_ALTERNATIVE_list :: Sign -> SortId -> SigLocalEnv -> [Annoted ALTERNATIVE]

-> ExtPos -> [Pos] ->

Result (SigLocalEnv, [Annoted Alternative])

ana_ALTERNATIVE_list sigma' s sigma alternative_list top_pos pos =

chainPos (sigma,[]) (ana_ALTERNATIVE sigma' s) alternative_list [top_pos]

pos tokPos_DATATYPE_DECL

ana_DATATYPE_DECL :: Sign -> SigLocalEnv -> Annoted DATATYPE_DECL

-> ExtPos -> Result SigLocalEnv

ana_DATATYPE_DECL sigma' sigma decl@(Annoted (Datatype_decl s alternative_list

pos) _ _ _) top_pos =

do (delta,alternatives) <- ana_ALTERNATIVE_list sigma' s sigma

alternative_list top_pos pos

let embedRel = mapMaybe (\x -> case x of Subsort sort _ -> Just sort;

_ -> Nothing)

(map item alternatives)

let defn = let

gen_items = concat $ map (\(x,y) -> x:y)

(toList $ w delta)

in

Datatype alternatives Loose gen_items pos

return delta { localEnv = (localEnv delta)

{ getSign = foldl (addSubsort s)

(updateSortItem (getName $ localEnv sigma)

decl (Just defn)

(getSign $ localEnv delta)

s top_pos)

embedRel } }

ana_datatype_items :: SigLocalEnv -> [Annoted DATATYPE_DECL] -> [Pos] ->

Result SigLocalEnv

ana_datatype_items sigma datatype_decl_list pos =

let

sigma' = foldl sig_DATATYPE_DECL (getSign $ localEnv sigma)

(map item datatype_decl_list)

in

chainPos sigma (ana_DATATYPE_DECL sigma') datatype_decl_list [] pos

tokPos_datatype_items

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

-- SIG-ITEMS

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

ana_SIG_ITEMS :: SigLocalEnv -> SIG_ITEMS -> Result SigLocalEnv

ana_SIG_ITEMS sigma (Sort_items sort_items loc_pos) =

chainPos (localEnv sigma) ana_SORT_ITEM sort_items [] loc_pos

tokPos_SORT_ITEM >>= return . toSigLocalEnv

ana_SIG_ITEMS sigma (Op_items op_items loc_pos) =

chainPos (localEnv sigma) ana_OP_ITEM op_items [] loc_pos

tokPos_OP_ITEM >>= return . toSigLocalEnv

ana_SIG_ITEMS sigma (Pred_items pred_items loc_pos) =

chainPos (localEnv sigma) ana_PRED_ITEM pred_items [] loc_pos

tokPos_PRED_ITEM >>= return . toSigLocalEnv

ana_SIG_ITEMS sigma (Datatype_items datatype_items loc_pos) =

ana_datatype_items sigma datatype_items loc_pos

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

-- VAR-DECL

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

ana_VAR_DECL :: LocalEnv -> VAR_DECL -> ExtPos -> Result LocalEnv

ana_VAR_DECL sigma (Var_decl x_n s _pos') _pos =

do checkSortExists sigma (fst _pos) s

let _extPos = toExtPos Nothing _pos' tokPos_VAR_DECL

let _decls = toVarDecls s _extPos x_n

return sigma { getGlobal = Global (setAdd (global $ getGlobal sigma)

_decls) }

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

-- VAR-ITEMS

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

ana_VAR_ITEMS :: LocalEnv -> [VAR_DECL] -> [Pos] -> Result LocalEnv

ana_VAR_ITEMS sigma _v _pos =

chainPos sigma ana_VAR_DECL _v [] _pos tokPos_VAR_ITEM

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

-- LOCAL-VAR-AXIOMS

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

ana_local_var_axioms' :: LocalEnv -> Annoted FORMULA -> ExtPos ->

Result LocalEnv

ana_local_var_axioms' sigma _f _pos =

do _phi <- ana_FORMULA sigma _f

let _phi' = toNamedSentence (global $ getGlobal sigma)

(someLabel "" _phi) _phi

return sigma { getPsi = addNamedSentences (getPsi sigma) [_phi'] }

ana_local_var_axioms :: LocalEnv -> [VAR_DECL] -> [Pos] ->

[Annoted FORMULA] -> [Pos] -> Result LocalEnv

ana_local_var_axioms sigma _v _vpos _f _apos =

do _delta <- ana_VAR_ITEMS sigma _v _vpos

chainPos _delta ana_local_var_axioms' _f [] _apos tokPos_local_var_axioms

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

-- AXIOM-ITEMS

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

ana_axiom_items :: LocalEnv -> [Annoted FORMULA] -> [Pos] -> Result LocalEnv

ana_axiom_items sigma _f _pos =

chainPos sigma ana_local_var_axioms' _f [] _pos tokPos_axiom_items

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

-- SORT-GEN

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

checkSortsExist :: Sign -> Pos -> Result ()

checkSortsExist sigma _pos =

let

_sorts = filter (\x -> case x of ASortItem _ -> True;

_ -> False)

(concat $ map snd $ toList $ getMap sigma)

in

if (null _sorts) then

fatal_error "sort-gen did not declare any sorts" _pos

else

return ()

ana_sort_gen :: LocalEnv -> [Annoted SIG_ITEMS] -> [Pos] -> Result LocalEnv

ana_sort_gen sigma _si _pos =

return sigma

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

-- BASIC-ITEMS

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

ana_BASIC_ITEMS :: LocalEnv -> Annoted BASIC_ITEMS -> Result LocalEnv

ana_BASIC_ITEMS sigma _itm =

case (item _itm) of

(Sig_items sig_items )

-> do sigma' <- ana_SIG_ITEMS (toSigLocalEnv sigma) sig_items

return (localEnv sigma')

{ getSign = updateOpItems (getName $ localEnv sigma')

(getSign $ localEnv sigma')

(selectors sigma') }

(Free_datatype _free_types _pos)

-> return sigma

(Sort_gen sig_items pos)

-> ana_sort_gen sigma sig_items pos

(Var_items var_items pos)

-> ana_VAR_ITEMS sigma var_items pos

(Local_var_axioms vars formulas pos)

-> ana_local_var_axioms sigma vars ((head pos):

(take ((length vars)-1) pos))

formulas (drop (length vars) pos)

(Axiom_items formulas pos)

-> ana_axiom_items sigma formulas pos

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

-- BASIC-SPEC

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

ana_BASIC_SPEC :: LocalEnv -> BASIC_SPEC -> Result LocalEnv

ana_BASIC_SPEC sigma (Basic_spec l) = foldM ana_BASIC_ITEMS sigma l

basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos)

-> Result (Sign,Sign,[(String,Sentence)])

basicAnalysis (spec,sigma,ga) = return(emptySign,emptySign,[])

{-

do env <- ana_BASIC_SPEC

(Env "unknown" ga sigma emptySentences emptyGlobal) spec

let sigma' = getSign env

let delta = signDiff sigma' sigma

return (delta, sigma', flattenSentences $ getPsi env)

-}

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

--

-- Static Analysis

-- Signature computations

--

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

-- FIXME

--

signDiff :: Sign -> Sign -> Sign

signDiff a b = emptySign {getMap = getMap a `difference` getMap b }

checkItem :: Sign -> (Id,SigItem) -> Bool

checkItem sigma (idt,si) =

let

res = lookup idt $ getMap sigma

items = if (isJust res) then

fromJust res

else

[]

in

si `elem` items

unfoldSigItems :: (Id, [SigItem]) -> [(Id, SigItem)]

unfoldSigItems (_,[]) = []

unfoldSigItems (idt,h:t) = (idt,h):(unfoldSigItems (idt,t))

isSubSig :: Sign -> Sign -> Bool

isSubSig sub super =

and $ map (checkItem super) $ concat $ map unfoldSigItems

$ toList $ getMap sub

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

--

-- Static Analysis

-- Symbol functions

--

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

symbTypeToKind :: SymbType -> Kind

symbTypeToKind (OpAsItemType _) = FunKind

symbTypeToKind (PredType _) = PredKind

symbTypeToKind (CASL.Sign.Sort) = SortKind

symbolToRaw :: Symbol -> RawSymbol

symbolToRaw (Symbol idt typ) = AKindedId (symbTypeToKind typ) idt

idToRaw :: Id -> RawSymbol

idToRaw x = AnID x

sigItemToSymbol :: SigItem -> Symbol

sigItemToSymbol (ASortItem s) = Symbol (sortId $ item s) CASL.Sign.Sort

sigItemToSymbol (AnOpItem o) = Symbol (opId $ item o)

(OpAsItemType (opType $ item o))

sigItemToSymbol (APredItem p) = Symbol (predId $ item p)

(PredType (predType $ item p))

symOf :: Sign -> Set.Set Symbol

symOf sigma = Set.fromList $ map sigItemToSymbol

$ concat $ elems $ getMap sigma

idToSortSymbol :: Id -> Symbol

idToSortSymbol idt = Symbol idt CASL.Sign.Sort

idToOpSymbol :: Id -> OpType -> Symbol

idToOpSymbol idt typ = Symbol idt (OpAsItemType typ)

idToPredSymbol :: Id -> PredType -> Symbol

idToPredSymbol idt typ = Symbol idt (PredType typ)

funMapEntryToSymbol :: Sign -> (Id,[(OpType,Id,Bool)]) -> [(Symbol,Symbol)]

funMapEntryToSymbol _ (_,[]) = []

funMapEntryToSymbol sigma (idt,(typ,newId,_):t) =

let

origType = opType $ item $ getOp sigma idt

in

(idToOpSymbol idt origType,idToOpSymbol newId typ):

(funMapEntryToSymbol sigma (idt,t))

predMapEntryToSymbol :: Sign -> (Id,[(PredType,Id)]) -> [(Symbol,Symbol)]

predMapEntryToSymbol _ (_,[]) = []

predMapEntryToSymbol sigma (idt,(typ,newId):t) =

let

origType = predType $ item $ getPred sigma idt

in

(idToPredSymbol idt origType,idToPredSymbol newId typ):

(predMapEntryToSymbol sigma (idt,t))

symmapOf :: Morphism -> EndoMap Symbol

symmapOf (Morphism src _ sorts funs preds) =

let

sortMap = fromList $ zip (map idToSortSymbol $ keys sorts)

(map idToSortSymbol $ elems sorts)

funMap = fromList $ concat $ map (funMapEntryToSymbol src)

(toList funs)

predMap = fromList $ concat $ map (predMapEntryToSymbol src)

(toList preds)

in

foldl union empty [sortMap,funMap,predMap]

matches :: Symbol -> RawSymbol -> Bool

matches x (ASymbol y) = x==y

matches (Symbol idt _) (AnID di) = idt==di

matches (Symbol idt CASL.Sign.Sort) (AKindedId SortKind di) = idt==di

matches (Symbol idt (OpAsItemType _)) (AKindedId FunKind di) = idt==di

matches (Symbol idt (PredType _)) (AKindedId PredKind di) = idt==di

matches _ _ = False

symName :: Symbol -> Id

symName (Symbol idt _) = idt

statSymbMapItems :: [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol)

statSymbMapItems sl = return (fromList $ concat $ map s1 sl)

where

s1 (Symb_map_items kind l _) = map (symbOrMapToRaw kind) l

symbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> (RawSymbol,RawSymbol)

symbOrMapToRaw k (Symb s) = (symbToRaw k s,symbToRaw k s)

symbOrMapToRaw k (Symb_map s t _) = (symbToRaw k s,symbToRaw k t)

statSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]

statSymbItems sl =

return (concat (map s1 sl))

where s1 (Symb_items kind l _) = map (symbToRaw kind) l

symbToRaw :: SYMB_KIND -> SYMB -> RawSymbol

symbToRaw k (Symb_id idt) = symbKindToRaw k idt

symbToRaw k (Qual_id idt _ _) = symbKindToRaw k idt

symbKindToRaw :: SYMB_KIND -> Id -> RawSymbol

symbKindToRaw Implicit idt = AnID idt

symbKindToRaw (Sorts_kind) idt = AKindedId SortKind idt

symbKindToRaw (Ops_kind) idt = AKindedId FunKind idt

symbKindToRaw (Preds_kind) idt = AKindedId PredKind idt

typeToRaw :: SYMB_KIND -> TYPE -> Id -> RawSymbol

typeToRaw _ (O_type _) idt = AKindedId FunKind idt

typeToRaw _ (P_type _) idt = AKindedId PredKind idt

typeToRaw k (A_type _) idt = symbKindToRaw k idt

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

-- THE END

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