hets/CommonLogic/Analysis.hs

	Analysis.hs revision 1da120eb84c9d3ed16f64d6defd9bc30569dc45b
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen{- |
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenModule      :  $Header$
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenDescription :  Basic analysis for common logic
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenCopyright   :  (c) Eugen Kuksa, Karl Luc, Uni Bremen 2010
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenLicense     :  GPLv2 or higher, see LICENSE.txt
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenMaintainer  :  eugenk@informatik.uni-bremen.de
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenStability   :  experimental
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenPortability :  portable
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenBasic and static analysis for common logic
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen-}
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenmodule CommonLogic.Analysis
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    ( basicCommonLogicAnalysis
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    , negForm
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    , symsOfTextMeta
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    , mkStatSymbItems
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    , mkStatSymbMapItem
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    , inducedFromMorphism
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    , inducedFromToMorphism
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    )
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    where
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
f60e98b33646e7a3317553e13bac591a98ce41c0Lukasz Skalskiimport Common.ExtSign
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersenimport Common.Result as Result
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenimport Common.GlobalAnnotations
39d8db043b599a7382f94bfc904d5e108af438bdLennart Poetteringimport qualified Common.AS_Annotation as AS_Anno
4e945a6f7971fd7d1f6b2c62ee3afdaff3c95ce4Lennart Poetteringimport Common.Id as Id
4e945a6f7971fd7d1f6b2c62ee3afdaff3c95ce4Lennart Poetteringimport Common.IRI (parseIRIReference)
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenimport Common.DocUtils
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersenimport CommonLogic.Symbol as Symbol
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersenimport qualified CommonLogic.AS_CommonLogic as AS
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersenimport CommonLogic.Morphism as Morphism
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenimport CommonLogic.Sign as Sign
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenimport CommonLogic.ExpandCurie
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenimport qualified Data.Set as Set
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenimport qualified Data.Map as Map
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenimport qualified Common.Lib.MapSet as MapSet
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersenimport qualified Data.List as List
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersendata DIAG_FORM = DiagForm
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering    {
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen        formula :: AS_Anno.Named AS.TEXT_META,
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen      diagnosis :: Result.Diagnosis
a5a807e63a50314e190e9166d8a453cd8dd258e3Zbigniew Jędrzejewski-Szmek    }
a5a807e63a50314e190e9166d8a453cd8dd258e3Zbigniew Jędrzejewski-Szmek
cc56fafeebf814ef035e549115cf1850e6473fa5WaLyong Cho-- | retrieves the signature out of a basic spec
a5a807e63a50314e190e9166d8a453cd8dd258e3Zbigniew Jędrzejewski-SzmekmakeSig :: AS.BASIC_SPEC -> Sign.Sign -> Sign.Sign
da927ba997d68401563b927f92e6e40e021a8e5cMichal SchmidtmakeSig (AS.Basic_spec spec) sig = List.foldl retrieveBasicItem sig spec
a5a807e63a50314e190e9166d8a453cd8dd258e3Zbigniew Jędrzejewski-Szmek
a5a807e63a50314e190e9166d8a453cd8dd258e3Zbigniew Jędrzejewski-SzmekretrieveBasicItem :: Sign.Sign -> AS_Anno.Annoted AS.BASIC_ITEMS -> Sign.Sign
a5a807e63a50314e190e9166d8a453cd8dd258e3Zbigniew Jędrzejewski-SzmekretrieveBasicItem sig x = case AS_Anno.item x of
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersen                            AS.Axiom_items xs -> List.foldl retrieveSign sig xs
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersen
da927ba997d68401563b927f92e6e40e021a8e5cMichal SchmidtretrieveSign :: Sign.Sign -> AS_Anno.Annoted AS.TEXT_META -> Sign.Sign
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart PoetteringretrieveSign sig (AS_Anno.Annoted tm _ _ _) =
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersen  Sign.unite (Sign.unite sig $ nondiscItems $ AS.nondiscourseNames tm)
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersen             (propsOfFormula $ AS.getText tm)
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
682265d5e2157882861b0091c6b81fa92699b72aTom GundersennondiscItems :: Maybe (Set.Set AS.NAME) -> Sign.Sign
682265d5e2157882861b0091c6b81fa92699b72aTom GundersennondiscItems s = case s of
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt  Nothing -> Sign.emptySig
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering  Just ns -> Sign.emptySig {Sign.nondiscourseNames = Set.map Id.simpleIdToId ns}
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersen
682265d5e2157882861b0091c6b81fa92699b72aTom Gundersen-- | retrieve sentences
682265d5e2157882861b0091c6b81fa92699b72aTom GundersenmakeFormulas :: AS.BASIC_SPEC -> Sign.Sign -> [DIAG_FORM]
682265d5e2157882861b0091c6b81fa92699b72aTom GundersenmakeFormulas (AS.Basic_spec bspec) sig =
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering  List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
b9e7a9d870ac41d4db954edd52a1f5dd7d153389Lennart PoetteringretrieveFormulaItem :: [DIAG_FORM] -> AS_Anno.Annoted AS.BASIC_ITEMS
b9e7a9d870ac41d4db954edd52a1f5dd7d153389Lennart Poettering                       -> Sign.Sign -> [DIAG_FORM]
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenretrieveFormulaItem axs x sig =
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen   case AS_Anno.item x of
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt      AS.Axiom_items ax ->
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering          List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersendata NUM_FORM = NumForm
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering    {
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering      nfformula :: AS_Anno.Annoted AS.TEXT_META
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt    , nfnum :: Int
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen    }
edc501d4674dadc304d45a7e1c5b69e207eb8cd4Lennart Poettering
edc501d4674dadc304d45a7e1c5b69e207eb8cd4Lennart PoetteringnumberFormulae :: [AS_Anno.Annoted AS.TEXT_META] -> Int -> [NUM_FORM]
da927ba997d68401563b927f92e6e40e021a8e5cMichal SchmidtnumberFormulae [] _ = []
edc501d4674dadc304d45a7e1c5b69e207eb8cd4Lennart PoetteringnumberFormulae (x : xs) i =
edc501d4674dadc304d45a7e1c5b69e207eb8cd4Lennart Poettering  if null $ AS_Anno.getRLabel x
edc501d4674dadc304d45a7e1c5b69e207eb8cd4Lennart Poettering  then NumForm {nfformula = x, nfnum = i} : numberFormulae xs (i + 1)
4e945a6f7971fd7d1f6b2c62ee3afdaff3c95ce4Lennart Poettering  else NumForm {nfformula = x, nfnum = 0} : numberFormulae xs i
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart PoetteringaddFormula :: [DIAG_FORM]
4e945a6f7971fd7d1f6b2c62ee3afdaff3c95ce4Lennart Poettering           -> NUM_FORM
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt           -> Sign.Sign
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen           -> [DIAG_FORM]
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenaddFormula formulae nf _ = formulae ++
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen                          [DiagForm {
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen                             formula = makeNamed (setTextIRI f) i
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen                           , diagnosis = Result.Diag
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen                           {
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen                             Result.diagKind = Result.Hint
da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt                           , Result.diagString = "All fine"
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering                           , Result.diagPos = lnum
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen                           }
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen                         }]
96e6e394431dcc1db52847be311e2c8e61d7a9d6Lennart Poettering    where
96e6e394431dcc1db52847be311e2c8e61d7a9d6Lennart Poettering      f = nfformula nf
74b2466e14a1961bf3ac0e8a60cfaceec705bd59Lennart Poettering      i = nfnum nf
af4ec4309e8f82aad87a8d574785c12f8763d5f8Lennart Poettering      lnum = AS_Anno.opt_pos f
b37d45c9ab5f645502695e47d268af1a54216e0eTom Gundersen
af4ec4309e8f82aad87a8d574785c12f8763d5f8Lennart Poettering-- | generates a named formula
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenmakeNamed :: AS_Anno.Annoted AS.TEXT_META -> Int
091a364c802e34a58f3260c9cb5db9b75c62215cTom Gundersen             -> AS_Anno.Named AS.TEXT_META
091a364c802e34a58f3260c9cb5db9b75c62215cTom GundersenmakeNamed f i =
  (AS_Anno.makeNamed (
      if null label
        then case text of
                AS.Named_text n _ _ -> Id.tokStr n
                _ ->  "Ax_" ++ show i
        else label
    ) $ AS_Anno.item f)
  { AS_Anno.isAxiom = not isTheorem }
   where
      text = AS.getText $ AS_Anno.item f
      label = AS_Anno.getRLabel f
      annos = AS_Anno.r_annos f
      isImplies = any AS_Anno.isImplies annos
      isImplied = any AS_Anno.isImplied annos
      isTheorem = isImplies || isImplied

setTextIRI :: AS_Anno.Annoted AS.TEXT_META -> AS_Anno.Annoted AS.TEXT_META
setTextIRI atm@(AS_Anno.Annoted{ AS_Anno.item = tm }) =
  let mi = case AS.getText tm of
            AS.Named_text n _ _ -> parseIRIReference $ init $ tail $ Id.tokStr n
            _ -> Nothing
  in  atm { AS_Anno.item = tm { AS.textIri = mi } }

-- | Retrives the signature of a sentence
propsOfFormula :: AS.TEXT -> Sign.Sign
propsOfFormula (AS.Named_text _ txt _) = propsOfFormula txt
propsOfFormula (AS.Text phrs _) = Sign.uniteL $ map propsOfPhrase phrs

propsOfPhrase :: AS.PHRASE -> Sign.Sign
propsOfPhrase (AS.Module m) = propsOfModule m
propsOfPhrase (AS.Sentence s) = propsOfSentence s
propsOfPhrase (AS.Comment_text _ txt _) = propsOfFormula txt
propsOfPhrase (AS.Importation _) = Sign.emptySig

propsOfModule :: AS.MODULE -> Sign.Sign
propsOfModule m = case m of
  (AS.Mod n txt _) -> Sign.unite (propsOfFormula txt) $ nameToSign n
  (AS.Mod_ex n exs txt _) -> Sign.unite (propsOfFormula txt)
      $ Sign.uniteL $ nameToSign n : map nameToSign exs
  where nameToSign x = Sign.emptySig {
            Sign.discourseNames = Set.singleton $ Id.simpleIdToId x
          }

propsOfSentence :: AS.SENTENCE -> Sign.Sign
propsOfSentence (AS.Atom_sent form _) = case form of
    AS.Equation term1 term2 -> Sign.unite (propsOfTerm term1)
      (propsOfTerm term2)
    AS.Atom term ts -> Sign.unite (propsOfTerm term)
      (uniteMap propsOfTermSeq ts)
propsOfSentence (AS.Quant_sent qs _) = case qs of
    AS.Universal xs s -> Sign.sigDiff (propsOfSentence s)
                                      (uniteMap propsOfNames xs)
    AS.Existential xs s -> Sign.sigDiff (propsOfSentence s)
                                        (uniteMap propsOfNames xs)
propsOfSentence (AS.Bool_sent bs _) = case bs of
    AS.Conjunction xs -> uniteMap propsOfSentence xs
    AS.Disjunction xs -> uniteMap propsOfSentence xs
    AS.Negation x -> propsOfSentence x
    AS.Implication s1 s2 -> Sign.unite (propsOfSentence s1) (propsOfSentence s2)
    AS.Biconditional s1 s2 -> Sign.unite (propsOfSentence s1) (propsOfSentence s2)
propsOfSentence (AS.Comment_sent _ s _) = propsOfSentence s
propsOfSentence (AS.Irregular_sent s _) = propsOfSentence s

propsOfTerm :: AS.TERM -> Sign.Sign
propsOfTerm term = case term of
    AS.Name_term x -> Sign.emptySig {
            Sign.discourseNames = Set.singleton $ Id.simpleIdToId x
          }
    AS.Funct_term t ts _ -> Sign.unite (propsOfTerm t)
                                       (uniteMap propsOfTermSeq ts)
    AS.Comment_term t _ _ -> propsOfTerm t -- fix

propsOfNames :: AS.NAME_OR_SEQMARK -> Sign.Sign
propsOfNames (AS.Name x) = Sign.emptySig {
            Sign.discourseNames = Set.singleton $ Id.simpleIdToId x
          }
propsOfNames (AS.SeqMark x) = Sign.emptySig {
            Sign.sequenceMarkers = Set.singleton $ Id.simpleIdToId x
          }

propsOfTermSeq :: AS.TERM_SEQ -> Sign.Sign
propsOfTermSeq s = case s of
    AS.Term_seq term -> propsOfTerm term
    AS.Seq_marks x -> Sign.emptySig {
            Sign.sequenceMarkers = Set.singleton $ Id.simpleIdToId x
          }

uniteMap :: (a -> Sign.Sign) -> [a] -> Sign
uniteMap p = List.foldl (\ sig -> Sign.unite sig . p)
   Sign.emptySig

-- | Common Logic static analysis
basicCommonLogicAnalysis :: (AS.BASIC_SPEC, Sign.Sign, GlobalAnnos)
  -> Result (AS.BASIC_SPEC,
             ExtSign Sign.Sign Symbol.Symbol,
             [AS_Anno.Named AS.TEXT_META])
basicCommonLogicAnalysis (bs', sig, ga) =
   Result.Result [] $ if exErrs then Nothing else
     Just (bs, ExtSign sigItems newSyms, sentences)
    where
      bs = expandCurieBS (prefix_map ga) bs'
      sigItems = makeSig bs sig
      newSyms = Set.map Symbol.Symbol
                  $ Set.difference (Sign.allItems sigItems) $ Sign.allItems sig
      bsform = makeFormulas bs sigItems
  -- [DIAG_FORM] signature and list of sentences
      sentences = map formula bsform
  -- Annoted Sentences (Ax_), numbering, DiagError
      exErrs = False

-- | creates a morphism from a symbol map
inducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                    -> Sign.Sign
                    -> Result.Result Morphism.Morphism
inducedFromMorphism m s = let
  p = Map.mapKeys symName $ Map.map symName m
  t = Sign.emptySig { discourseNames = Set.map (applyMap p) $ discourseNames s
                    , nondiscourseNames = Set.map (applyMap p) $ nondiscourseNames s
                    , sequenceMarkers = Set.map (applyMap p) $ sequenceMarkers s
                    }
  in return $ mkMorphism s t p

splitFragment :: Id -> (String, String)
splitFragment = span (/= '#') . show

inducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                    -> ExtSign Sign.Sign Symbol.Symbol
                    -> ExtSign Sign.Sign Symbol.Symbol
                    -> Result.Result Morphism.Morphism
inducedFromToMorphism m (ExtSign s sys) (ExtSign t ty) = let
  tsy = Set.fold (\ r -> let (q, f) = splitFragment $ symName r
          in MapSet.insert f q) MapSet.empty ty
  p = Set.fold (\ sy -> let n = symName sy in case Map.lookup sy m of
         Just r -> Map.insert n $ symName r
         Nothing -> if Set.member sy ty then id else
           let (_, f) = splitFragment n
           in case Set.toList $ MapSet.lookup f tsy of
                [q] -> Map.insert n $ simpleIdToId
                    $ mkSimpleId $ q ++ f
                _ -> id) Map.empty sys
  t2 = Sign.emptySig
       { discourseNames = Set.map (applyMap p) $ discourseNames s
       , nondiscourseNames = Set.map (applyMap p) $ nondiscourseNames s
       , sequenceMarkers = Set.map (applyMap p) $ sequenceMarkers s
       }
  in if isSubSigOf t2 t then return $ mkMorphism s t p else
        fail $ "cannot map symbols from\n" ++ showDoc (sigDiff t2 t) "\nto\n"
          ++ showDoc t ""

-- | negate sentence (text) - propagates negation to sentences
negForm :: AS.TEXT_META -> AS.TEXT_META
negForm tm = tm { AS.getText = negForm_txt $ AS.getText tm }

negForm_txt :: AS.TEXT -> AS.TEXT
negForm_txt t = case t of
  AS.Text phrs r -> AS.Text (map negForm_phr phrs) r
  AS.Named_text n txt r -> AS.Named_text n (negForm_txt txt) r

-- negate phrase - propagates negation to sentences
negForm_phr :: AS.PHRASE -> AS.PHRASE
negForm_phr phr = case phr of
  AS.Module m -> AS.Module $ negForm_mod m
  AS.Sentence s -> AS.Sentence $ negForm_sen s
  AS.Comment_text c t r -> AS.Comment_text c (negForm_txt t) r
  x -> x

-- negate module - propagates negation to sentences
negForm_mod ::AS.MODULE -> AS.MODULE
negForm_mod m = case m of
  AS.Mod n t r -> AS.Mod n (negForm_txt t) r
  AS.Mod_ex n exs t r -> AS.Mod_ex n exs (negForm_txt t) r

-- negate sentence
negForm_sen :: AS.SENTENCE -> AS.SENTENCE
negForm_sen f = case f of
  AS.Quant_sent _ r -> AS.Bool_sent (AS.Negation f) r
  AS.Bool_sent bs r -> case bs of
    AS.Negation s -> s
    _ -> AS.Bool_sent (AS.Negation f) r
  _ -> AS.Bool_sent (AS.Negation f) Id.nullRange

-- | Static analysis for symbol maps
mkStatSymbMapItem :: [AS.SYMB_MAP_ITEMS]
                  -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
mkStatSymbMapItem xs =
    Result.Result
    {
      Result.diags = []
    , Result.maybeResult = Just $
                           foldl
                           (
                            \ smap x ->
                                case x of
                                  AS.Symb_map_items sitem _ ->
                                       Map.union smap $ statSymbMapItem sitem
                           )
                           Map.empty
                           xs
    }

statSymbMapItem :: [AS.SYMB_OR_MAP] -> Map.Map Symbol.Symbol Symbol.Symbol
statSymbMapItem =
    foldl
    (
     \ mmap x ->
         case x of
           AS.Symb sym -> Map.insert (nosToSymbol sym) (nosToSymbol sym) mmap
           AS.Symb_mapN s1 s2 _
             -> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
           AS.Symb_mapS s1 s2 _
             -> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
    )
    Map.empty

-- | Retrieve raw symbols
mkStatSymbItems :: [AS.SYMB_ITEMS] -> Result.Result [Symbol.Symbol]
mkStatSymbItems a = Result.Result
                    {
                      Result.diags = []
                    , Result.maybeResult = Just $ statSymbItems a
                    }

statSymbItems :: [AS.SYMB_ITEMS] -> [Symbol.Symbol]
statSymbItems = concatMap symbItemsToSymbol

symbItemsToSymbol :: AS.SYMB_ITEMS -> [Symbol.Symbol]
symbItemsToSymbol (AS.Symb_items syms _) = map nosToSymbol syms

nosToSymbol :: AS.NAME_OR_SEQMARK -> Symbol.Symbol
nosToSymbol nos = case nos of
  AS.Name tok -> symbToSymbol tok
  AS.SeqMark tok -> symbToSymbol tok

symbToSymbol :: Id.Token -> Symbol.Symbol
symbToSymbol tok = Symbol.Symbol{Symbol.symName = Id.simpleIdToId tok}

-- | retrieves all symbols from the text
symsOfTextMeta :: AS.TEXT_META -> [Symbol.Symbol]
symsOfTextMeta tm =
  Set.toList $ Symbol.symOf $ retrieveSign Sign.emptySig $ AS_Anno.emptyAnno tm