{- |
Module      :  ./DFOL/Analysis_DFOL.hs
Description :  Static analysis for first-order logic with dependent types (DFOL)
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module DFOL.Analysis_DFOL
  (
    basicAnalysis         -- static analysis of basic specifications
  , symbAnalysis          -- static analysis for symbols lists
  , symbMapAnalysis       -- static analysis for symbol map lists
   ) where

import DFOL.Utils
import DFOL.AS_DFOL
import DFOL.Sign
import DFOL.Symbol

import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import qualified Common.Result as Result
import qualified Common.AS_Annotation as Anno

import qualified Data.Set as Set
import qualified Data.Map as Map

-- BASIC SPEC ANALYSIS
basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->
   Result.Result (BASIC_SPEC, ExtSign Sign Symbol, [Anno.Named FORMULA])
basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
basicAnalysis (bs :: BASIC_SPEC
bs, sig :: Sign
sig, _) =
   if Bool
errs
      then [Diagnosis]
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diag Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. Maybe a
Nothing
      else [Diagnosis]
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a b. (a -> b) -> a -> b
$ (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. a -> Maybe a
Just (BASIC_SPEC
bs, Sign -> Set Symbol -> ExtSign Sign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign
newSig Set Symbol
declaredSyms, [Named FORMULA]
formulae)
   where Diagn diag1 :: [Diagnosis]
diag1 newSig :: Sign
newSig = BASIC_SPEC -> Sign -> DIAGN Sign
makeSig BASIC_SPEC
bs Sign
sig
         Diagn diag2 :: [Diagnosis]
diag2 formulae :: [Named FORMULA]
formulae = BASIC_SPEC -> Sign -> DIAGN [Named FORMULA]
makeFormulas BASIC_SPEC
bs Sign
newSig
         declaredSyms :: Set Symbol
declaredSyms = (NAME -> Symbol) -> Set NAME -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map NAME -> Symbol
Symbol
                         (Set NAME -> Set Symbol) -> Set NAME -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set NAME
getSymbols Sign
newSig) (Sign -> Set NAME
getSymbols Sign
sig)
         diag :: [Diagnosis]
diag = [Diagnosis]
diag1 [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
diag2
         errs :: Bool
errs = [Diagnosis] -> Bool
Result.hasErrors [Diagnosis]
diag

{- SIGNATURES
make a new signature out of a basic spec and an input signature -}
makeSig :: BASIC_SPEC -> Sign -> DIAGN Sign
makeSig :: BASIC_SPEC -> Sign -> DIAGN Sign
makeSig (Basic_spec items :: [Annoted BASIC_ITEM]
items) = [Annoted BASIC_ITEM] -> Sign -> DIAGN Sign
addItemsToSig [Annoted BASIC_ITEM]
items

-- adds a list of annotated basic items to an input signature
addItemsToSig :: [Anno.Annoted BASIC_ITEM] -> Sign -> DIAGN Sign
addItemsToSig :: [Annoted BASIC_ITEM] -> Sign -> DIAGN Sign
addItemsToSig [] sig :: Sign
sig = [Diagnosis] -> Sign -> DIAGN Sign
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] Sign
sig
addItemsToSig (i :: Annoted BASIC_ITEM
i : is :: [Annoted BASIC_ITEM]
is) sig :: Sign
sig =
   case Annoted BASIC_ITEM
i of
        (Anno.Annoted (Axiom_item _) _ _ _) -> [Annoted BASIC_ITEM] -> Sign -> DIAGN Sign
addItemsToSig [Annoted BASIC_ITEM]
is Sign
sig
        (Anno.Annoted (Decl_item d :: DECL
d) _ _ _) ->
             if [Diagnosis] -> Bool
Result.hasErrors [Diagnosis]
diag
                then [Diagnosis] -> Sign -> DIAGN Sign
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [Diagnosis]
diag Sign
sig
                else [Annoted BASIC_ITEM] -> Sign -> DIAGN Sign
addItemsToSig [Annoted BASIC_ITEM]
is Sign
newSig
             where Diagn diag :: [Diagnosis]
diag newSig :: Sign
newSig = DECL -> Sign -> DIAGN Sign
addDeclToSig DECL
d Sign
sig

-- adds a declaration to an existing signature
addDeclToSig :: DECL -> Sign -> DIAGN Sign
addDeclToSig :: DECL -> Sign -> DIAGN Sign
addDeclToSig dec :: DECL
dec sig :: Sign
sig = if Bool
valid
                          then [Diagnosis] -> Sign -> DIAGN Sign
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] (Sign -> DIAGN Sign) -> Sign -> DIAGN Sign
forall a b. (a -> b) -> a -> b
$ DECL -> Sign -> Sign
addSymbolDecl DECL
dec Sign
sig
                          else [Diagnosis] -> Sign -> DIAGN Sign
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [Diagnosis]
diag Sign
sig
                       where Diagn diag :: [Diagnosis]
diag valid :: Bool
valid = DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidDecl DECL
dec Sign
sig CONTEXT
emptyContext

{- FORMULAS
make a list of formulas for the given signature out of a basic spec -}
makeFormulas :: BASIC_SPEC -> Sign -> DIAGN [Anno.Named FORMULA]
makeFormulas :: BASIC_SPEC -> Sign -> DIAGN [Named FORMULA]
makeFormulas (Basic_spec items :: [Annoted BASIC_ITEM]
items) = [Annoted BASIC_ITEM] -> Int -> Sign -> DIAGN [Named FORMULA]
makeFormulasFromItems [Annoted BASIC_ITEM]
items 0

-- make a list of named formulas out of a list of annotated items
makeFormulasFromItems :: [Anno.Annoted BASIC_ITEM] -> Int
                         -> Sign -> DIAGN [Anno.Named FORMULA]
makeFormulasFromItems :: [Annoted BASIC_ITEM] -> Int -> Sign -> DIAGN [Named FORMULA]
makeFormulasFromItems [] _ _ = [Diagnosis] -> [Named FORMULA] -> DIAGN [Named FORMULA]
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] []
makeFormulasFromItems (i :: Annoted BASIC_ITEM
i : is :: [Annoted BASIC_ITEM]
is) num :: Int
num sig :: Sign
sig =
    case Annoted BASIC_ITEM
i of
         (Anno.Annoted (Decl_item _) _ _ _) -> [Annoted BASIC_ITEM] -> Int -> Sign -> DIAGN [Named FORMULA]
makeFormulasFromItems [Annoted BASIC_ITEM]
is Int
num Sign
sig
         (Anno.Annoted (Axiom_item a :: FORMULA
a) _ _ annos :: [Annotation]
annos) ->
           case Maybe (Named FORMULA)
fM of
                Just f :: Named FORMULA
f ->
                   let Diagn diagL :: [Diagnosis]
diagL fs :: [Named FORMULA]
fs = [Annoted BASIC_ITEM] -> Int -> Sign -> DIAGN [Named FORMULA]
makeFormulasFromItems [Annoted BASIC_ITEM]
is Int
newNum Sign
sig
                       in [Diagnosis] -> [Named FORMULA] -> DIAGN [Named FORMULA]
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [Diagnosis]
diagL (Named FORMULA
f Named FORMULA -> [Named FORMULA] -> [Named FORMULA]
forall a. a -> [a] -> [a]
: [Named FORMULA]
fs)
                Nothing ->
                   let Diagn diagL :: [Diagnosis]
diagL fs :: [Named FORMULA]
fs = [Annoted BASIC_ITEM] -> Int -> Sign -> DIAGN [Named FORMULA]
makeFormulasFromItems [Annoted BASIC_ITEM]
is Int
num Sign
sig
                       in [Diagnosis] -> [Named FORMULA] -> DIAGN [Named FORMULA]
forall a. [Diagnosis] -> a -> DIAGN a
Diagn ([Diagnosis]
diag [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
diagL) [Named FORMULA]
fs
           where Result.Result diag :: [Diagnosis]
diag fM :: Maybe (Named FORMULA)
fM = FORMULA -> String -> [Annotation] -> Sign -> Result (Named FORMULA)
makeNamedFormula FORMULA
a String
nam [Annotation]
annos Sign
sig
                 label :: String
label = Annoted BASIC_ITEM -> String
forall a. Annoted a -> String
Anno.getRLabel Annoted BASIC_ITEM
i
                 nam :: String
nam = if String
label String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then "Ax_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
num else String
label
                 newNum :: Int
newNum = if String
label String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then Int
num Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else Int
num

-- make a named formula
makeNamedFormula :: FORMULA -> String -> [Anno.Annotation]
                    -> Sign -> Result.Result (Anno.Named FORMULA)
makeNamedFormula :: FORMULA -> String -> [Annotation] -> Sign -> Result (Named FORMULA)
makeNamedFormula f :: FORMULA
f nam :: String
nam annos :: [Annotation]
annos sig :: Sign
sig =
    if Bool
valid
       then [Diagnosis] -> Maybe (Named FORMULA) -> Result (Named FORMULA)
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe (Named FORMULA) -> Result (Named FORMULA))
-> Maybe (Named FORMULA) -> Result (Named FORMULA)
forall a b. (a -> b) -> a -> b
$ Named FORMULA -> Maybe (Named FORMULA)
forall a. a -> Maybe a
Just Named FORMULA
namedF
       else [Diagnosis] -> Maybe (Named FORMULA) -> Result (Named FORMULA)
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diag Maybe (Named FORMULA)
forall a. Maybe a
Nothing
    where Diagn diag :: [Diagnosis]
diag valid :: Bool
valid = FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
f Sign
sig CONTEXT
emptyContext
          namedF :: Named FORMULA
namedF = (String -> FORMULA -> Named FORMULA
forall a s. a -> s -> SenAttr s a
Anno.makeNamed String
nam FORMULA
f) {isAxiom :: Bool
Anno.isAxiom = Bool -> Bool
not Bool
isTheorem}
          isImplies :: Bool
isImplies = (Annotation -> Bool) -> [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Annotation -> Bool
Anno.isImplies [Annotation]
annos
          isImplied :: Bool
isImplied = (Annotation -> Bool) -> [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Annotation -> Bool
Anno.isImplied [Annotation]
annos
          isTheorem :: Bool
isTheorem = Bool
isImplies Bool -> Bool -> Bool
|| Bool
isImplied

-- determines whether a formula is valid w.r.t. a signature and a context
isValidFormula :: FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula :: FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula T _ _ = [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] Bool
True
isValidFormula F _ _ = [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] Bool
True
isValidFormula (Pred t :: TERM
t) sig :: Sign
sig cont :: CONTEXT
cont = TERM -> TYPE -> Sign -> CONTEXT -> DIAGN Bool
hasType TERM
t TYPE
Form Sign
sig CONTEXT
cont
isValidFormula (Equality term1 :: TERM
term1 term2 :: TERM
term2) sig :: Sign
sig cont :: CONTEXT
cont =
    case Maybe TYPE
type1M of
         Nothing -> [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [Diagnosis]
diag1 Bool
False
         Just type1 :: TYPE
type1 -> case TYPE
type1 of
                            Univ _ -> TERM -> TYPE -> Sign -> CONTEXT -> DIAGN Bool
hasType TERM
term2 TYPE
type1 Sign
sig CONTEXT
cont
                            _ -> [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [TERM -> TYPE -> CONTEXT -> Diagnosis
noDiscourseTermError TERM
term1 TYPE
type1 CONTEXT
cont]
                                       Bool
False
    where Result.Result diag1 :: [Diagnosis]
diag1 type1M :: Maybe TYPE
type1M = TERM -> Sign -> CONTEXT -> Result TYPE
getTermType TERM
term1 Sign
sig CONTEXT
cont
isValidFormula (Negation f :: FORMULA
f) sig :: Sign
sig cont :: CONTEXT
cont = FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
f Sign
sig CONTEXT
cont
isValidFormula (Conjunction fs :: [FORMULA]
fs) sig :: Sign
sig cont :: CONTEXT
cont =
   [DIAGN Bool] -> DIAGN Bool
andD ([DIAGN Bool] -> DIAGN Bool) -> [DIAGN Bool] -> DIAGN Bool
forall a b. (a -> b) -> a -> b
$ (FORMULA -> DIAGN Bool) -> [FORMULA] -> [DIAGN Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: FORMULA
f -> FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
f Sign
sig CONTEXT
cont) [FORMULA]
fs
isValidFormula (Disjunction fs :: [FORMULA]
fs) sig :: Sign
sig cont :: CONTEXT
cont =
   [DIAGN Bool] -> DIAGN Bool
andD ([DIAGN Bool] -> DIAGN Bool) -> [DIAGN Bool] -> DIAGN Bool
forall a b. (a -> b) -> a -> b
$ (FORMULA -> DIAGN Bool) -> [FORMULA] -> [DIAGN Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: FORMULA
f -> FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
f Sign
sig CONTEXT
cont) [FORMULA]
fs
isValidFormula (Implication f :: FORMULA
f g :: FORMULA
g) sig :: Sign
sig cont :: CONTEXT
cont =
   [DIAGN Bool] -> DIAGN Bool
andD [FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
f Sign
sig CONTEXT
cont, FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
g Sign
sig CONTEXT
cont]
isValidFormula (Equivalence f :: FORMULA
f g :: FORMULA
g) sig :: Sign
sig cont :: CONTEXT
cont =
   [DIAGN Bool] -> DIAGN Bool
andD [FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
f Sign
sig CONTEXT
cont, FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
g Sign
sig CONTEXT
cont]
isValidFormula (Forall [] f :: FORMULA
f) sig :: Sign
sig cont :: CONTEXT
cont = FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
f Sign
sig CONTEXT
cont
isValidFormula (Forall (d :: DECL
d : ds :: [DECL]
ds) f :: FORMULA
f) sig :: Sign
sig cont :: CONTEXT
cont =
   [DIAGN Bool] -> DIAGN Bool
andD [DIAGN Bool
validDecl, DIAGN Bool
validFormula]
   where validDecl :: DIAGN Bool
validDecl = DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidVarDecl DECL
d Sign
sig CONTEXT
cont
         validFormula :: DIAGN Bool
validFormula = FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula ([DECL] -> FORMULA -> FORMULA
Forall [DECL]
ds FORMULA
f) Sign
sig (DECL -> CONTEXT -> CONTEXT
addVarDecl DECL
d CONTEXT
cont)
isValidFormula (Exists [] f :: FORMULA
f) sig :: Sign
sig cont :: CONTEXT
cont = FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula FORMULA
f Sign
sig CONTEXT
cont
isValidFormula (Exists (d :: DECL
d : ds :: [DECL]
ds) f :: FORMULA
f) sig :: Sign
sig cont :: CONTEXT
cont =
   [DIAGN Bool] -> DIAGN Bool
andD [DIAGN Bool
validDecl, DIAGN Bool
validFormula]
   where validDecl :: DIAGN Bool
validDecl = DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidVarDecl DECL
d Sign
sig CONTEXT
cont
         validFormula :: DIAGN Bool
validFormula = FORMULA -> Sign -> CONTEXT -> DIAGN Bool
isValidFormula ([DECL] -> FORMULA -> FORMULA
Exists [DECL]
ds FORMULA
f) Sign
sig (DECL -> CONTEXT -> CONTEXT
addVarDecl DECL
d CONTEXT
cont)

{- SYMBOL LIST AND MAP ANALYSIS
creates a symbol map out of a list of symbol map items -}
symbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result.Result (Map.Map Symbol Symbol)
symbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result (Map Symbol Symbol)
symbMapAnalysis xs :: [SYMB_MAP_ITEMS]
xs = [Diagnosis]
-> Maybe (Map Symbol Symbol) -> Result (Map Symbol Symbol)
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result []
     (Maybe (Map Symbol Symbol) -> Result (Map Symbol Symbol))
-> Maybe (Map Symbol Symbol) -> Result (Map Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ Map Symbol Symbol -> Maybe (Map Symbol Symbol)
forall a. a -> Maybe a
Just (Map Symbol Symbol -> Maybe (Map Symbol Symbol))
-> Map Symbol Symbol -> Maybe (Map Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ (Map Symbol Symbol -> SYMB_MAP_ITEMS -> Map Symbol Symbol)
-> Map Symbol Symbol -> [SYMB_MAP_ITEMS] -> Map Symbol Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map Symbol Symbol
m x :: SYMB_MAP_ITEMS
x -> Map Symbol Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Symbol Symbol
m (SYMB_MAP_ITEMS -> Map Symbol Symbol
makeSymbMap SYMB_MAP_ITEMS
x)) Map Symbol Symbol
forall k a. Map k a
Map.empty [SYMB_MAP_ITEMS]
xs

-- creates a symbol map out of symbol map items
makeSymbMap :: SYMB_MAP_ITEMS -> Map.Map Symbol Symbol
makeSymbMap :: SYMB_MAP_ITEMS -> Map Symbol Symbol
makeSymbMap (Symb_map_items xs :: [SYMB_OR_MAP]
xs) =
   (Map Symbol Symbol -> SYMB_OR_MAP -> Map Symbol Symbol)
-> Map Symbol Symbol -> [SYMB_OR_MAP] -> Map Symbol Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map Symbol Symbol
m x :: SYMB_OR_MAP
x -> case SYMB_OR_MAP
x of
                        Symb s :: NAME
s -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (NAME -> Symbol
Symbol NAME
s) (NAME -> Symbol
Symbol NAME
s) Map Symbol Symbol
m
                        Symb_map s1 :: NAME
s1 s2 :: NAME
s2 -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (NAME -> Symbol
Symbol NAME
s1) (NAME -> Symbol
Symbol NAME
s2) Map Symbol Symbol
m
         )
         Map Symbol Symbol
forall k a. Map k a
Map.empty
         [SYMB_OR_MAP]
xs

-- creates a symbol list out of a list of symbol items
symbAnalysis :: [SYMB_ITEMS] -> Result.Result [Symbol]
symbAnalysis :: [SYMB_ITEMS] -> Result [Symbol]
symbAnalysis xs :: [SYMB_ITEMS]
xs = [Diagnosis] -> Maybe [Symbol] -> Result [Symbol]
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe [Symbol] -> Result [Symbol])
-> Maybe [Symbol] -> Result [Symbol]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> Maybe [Symbol]
forall a. a -> Maybe a
Just ([Symbol] -> Maybe [Symbol]) -> [Symbol] -> Maybe [Symbol]
forall a b. (a -> b) -> a -> b
$ (SYMB_ITEMS -> [Symbol]) -> [SYMB_ITEMS] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SYMB_ITEMS -> [Symbol]
makeSymbols [SYMB_ITEMS]
xs

-- creates a symbol list out of symbol item
makeSymbols :: SYMB_ITEMS -> [Symbol]
makeSymbols :: SYMB_ITEMS -> [Symbol]
makeSymbols (Symb_items symbs :: [NAME]
symbs) = (NAME -> Symbol) -> [NAME] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map NAME -> Symbol
Symbol [NAME]
symbs

-- ERROR MESSAGES
noDiscourseTermError :: TERM -> TYPE -> CONTEXT -> Result.Diagnosis
noDiscourseTermError :: TERM -> TYPE -> CONTEXT -> Diagnosis
noDiscourseTermError term :: TERM
term t :: TYPE
t cont :: CONTEXT
cont =
  Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
    { diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
    , diagString :: String
Result.diagString = "Term " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TERM -> Doc
forall a. Pretty a => a -> Doc
pretty TERM
term)
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " has the non-discourse type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t)
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " in the context " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (CONTEXT -> Doc
forall a. Pretty a => a -> Doc
pretty CONTEXT
cont)
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and hence cannot be used in an equality."
    , diagPos :: Range
Result.diagPos = Range
nullRange
    }