{- |
Module      :  ./Adl/StatAna.hs
Description :  static ADL analysis
Copyright   :  (c) Stef Joosten, Christian Maeder DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

-}

module Adl.StatAna where

import Adl.As
import Adl.Sign

import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.Result
import Common.Lib.State
import qualified Common.Lib.Rel as Rel
import Common.Utils

import Control.Monad

import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe
import Data.List

basicAna :: (Context, Sign, GlobalAnnos)
  -> Result (Context, ExtSign Sign Symbol, [Named Sen])
basicAna :: (Context, Sign, GlobalAnnos)
-> Result (Context, ExtSign Sign Symbol, [Named Sen])
basicAna (Context m :: Maybe Token
m ps :: [PatElem]
ps, sig :: Sign
sig, _) =
  let (nps :: [PatElem]
nps, env :: Env
env) = State Env [PatElem] -> Env -> ([PatElem], Env)
forall s a. State s a -> s -> (a, s)
runState ((PatElem -> State Env PatElem) -> [PatElem] -> State Env [PatElem]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PatElem -> State Env PatElem
anaPatElem [PatElem]
ps) (Env -> ([PatElem], Env)) -> Env -> ([PatElem], Env)
forall a b. (a -> b) -> a -> b
$ Sign -> Env
toEnv Sign
sig
  in [Diagnosis]
-> Maybe (Context, ExtSign Sign Symbol, [Named Sen])
-> Result (Context, ExtSign Sign Symbol, [Named Sen])
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Diagnosis] -> [Diagnosis]
forall a. [a] -> [a]
reverse ([Diagnosis] -> [Diagnosis]) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ Env -> [Diagnosis]
msgs Env
env)
     (Maybe (Context, ExtSign Sign Symbol, [Named Sen])
 -> Result (Context, ExtSign Sign Symbol, [Named Sen]))
-> Maybe (Context, ExtSign Sign Symbol, [Named Sen])
-> Result (Context, ExtSign Sign Symbol, [Named Sen])
forall a b. (a -> b) -> a -> b
$ (Context, ExtSign Sign Symbol, [Named Sen])
-> Maybe (Context, ExtSign Sign Symbol, [Named Sen])
forall a. a -> Maybe a
Just (Maybe Token -> [PatElem] -> Context
Context Maybe Token
m [PatElem]
nps, Sign -> Set Symbol -> ExtSign Sign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign (Sign -> Sign
closeSign (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Env -> Sign
sign Env
env) (Set Symbol -> ExtSign Sign Symbol)
-> Set Symbol -> ExtSign Sign Symbol
forall a b. (a -> b) -> a -> b
$ Env -> Set Symbol
syms Env
env
            , [Named Sen] -> [Named Sen]
forall a. [a] -> [a]
reverse ([Named Sen] -> [Named Sen]) -> [Named Sen] -> [Named Sen]
forall a b. (a -> b) -> a -> b
$ Env -> [Named Sen]
sens Env
env)

data Env = Env
  { Env -> Sign
sign :: Sign
  , Env -> Set Symbol
syms :: Set.Set Symbol
  , Env -> [Named Sen]
sens :: [Named Sen]
  , Env -> [Diagnosis]
msgs :: [Diagnosis]
  }

toEnv :: Sign -> Env
toEnv :: Sign -> Env
toEnv s :: Sign
s = Env :: Sign -> Set Symbol -> [Named Sen] -> [Diagnosis] -> Env
Env { sign :: Sign
sign = Sign
s, syms :: Set Symbol
syms = Set Symbol
forall a. Set a
Set.empty, sens :: [Named Sen]
sens = [], msgs :: [Diagnosis]
msgs = [] }

addMsgs :: [Diagnosis] -> State Env ()
addMsgs :: [Diagnosis] -> State Env ()
addMsgs ds :: [Diagnosis]
ds = do
   Env
e <- State Env Env
forall s. State s s
get
   Env -> State Env ()
forall s. s -> State s ()
put Env
e { msgs :: [Diagnosis]
msgs = [Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ Env -> [Diagnosis]
msgs Env
e }

addSens :: [Named Sen] -> State Env ()
addSens :: [Named Sen] -> State Env ()
addSens ns :: [Named Sen]
ns = do
   Env
e <- State Env Env
forall s. State s s
get
   Env -> State Env ()
forall s. s -> State s ()
put Env
e { sens :: [Named Sen]
sens = [Named Sen]
ns [Named Sen] -> [Named Sen] -> [Named Sen]
forall a. [a] -> [a] -> [a]
++ Env -> [Named Sen]
sens Env
e }

addSyms :: Set.Set Symbol -> State Env ()
addSyms :: Set Symbol -> State Env ()
addSyms sys :: Set Symbol
sys = do
   Env
e <- State Env Env
forall s. State s s
get
   Env -> State Env ()
forall s. s -> State s ()
put Env
e { syms :: Set Symbol
syms = Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Symbol
sys (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Env -> Set Symbol
syms Env
e }

symsOf :: Relation -> Set.Set Symbol
symsOf :: Relation -> Set Symbol
symsOf r :: Relation
r = let
    y :: RelType
y = Relation -> RelType
relType Relation
r
    s :: Concept
s = RelType -> Concept
relSrc RelType
y
    t :: Concept
t = RelType -> Concept
relTrg RelType
y
    in [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
Set.fromList [Concept -> Symbol
Con Concept
s, Concept -> Symbol
Con Concept
t, Relation -> Symbol
Rel Relation
r]

addRel :: Relation -> State Env ()
addRel :: Relation -> State Env ()
addRel r :: Relation
r = do
   Env
e <- State Env Env
forall s. State s s
get
   let s :: Sign
s = Env -> Sign
sign Env
e
       m :: RelMap
m = Sign -> RelMap
rels Sign
s
       i :: Id
i = Token -> Id
simpleIdToId (Token -> Id) -> Token -> Id
forall a b. (a -> b) -> a -> b
$ Relation -> Token
decnm Relation
r
       l :: Set RelType
l = Set RelType -> Id -> RelMap -> Set RelType
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set RelType
forall a. Set a
Set.empty Id
i RelMap
m
       v :: RelType
v = Relation -> RelType
relType Relation
r
   Env -> State Env ()
forall s. s -> State s ()
put Env
e { sign :: Sign
sign = Sign
s { rels :: RelMap
rels = Id -> Set RelType -> RelMap -> RelMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i (RelType -> Set RelType -> Set RelType
forall a. Ord a => a -> Set a -> Set a
Set.insert RelType
v Set RelType
l) RelMap
m } }

addIsa :: Concept -> Concept -> State Env ()
addIsa :: Concept -> Concept -> State Env ()
addIsa c1 :: Concept
c1 c2 :: Concept
c2 = do
   Env
e <- State Env Env
forall s. State s s
get
   let s :: Sign
s = Env -> Sign
sign Env
e
       r :: Rel Concept
r = Sign -> Rel Concept
isas Sign
s
       sys :: Set Symbol
sys = Sign -> Set Symbol
symOf Sign
s
   if Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Concept -> Symbol
Con Concept
c1) Set Symbol
sys then
      if Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Concept -> Symbol
Con Concept
c2) Set Symbol
sys then
         if Concept
c1 Concept -> Concept -> Bool
forall a. Eq a => a -> a -> Bool
== Concept
c2 then [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Concept -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "no specialization" Concept
c1]
         else if Concept -> Concept -> Rel Concept -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path Concept
c2 Concept
c1 Rel Concept
r then
                  [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Concept -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "opposite ISA known" Concept
c1]
              else if Concept -> Concept -> Rel Concept -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path Concept
c1 Concept
c2 Rel Concept
r then
                       [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Concept -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "redeclared ISA" Concept
c1]
                   else Env -> State Env ()
forall s. s -> State s ()
put Env
e { sign :: Sign
sign = Sign
s { isas :: Rel Concept
isas = Concept -> Concept -> Rel Concept -> Rel Concept
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair Concept
c1 Concept
c2 Rel Concept
r }}
      else [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Concept -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown ISA" Concept
c2]
    else [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Concept -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown GEN" Concept
c1]

data TypedRule = TypedRule Rule RelType deriving Int -> TypedRule -> ShowS
[TypedRule] -> ShowS
TypedRule -> String
(Int -> TypedRule -> ShowS)
-> (TypedRule -> String)
-> ([TypedRule] -> ShowS)
-> Show TypedRule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypedRule] -> ShowS
$cshowList :: [TypedRule] -> ShowS
show :: TypedRule -> String
$cshow :: TypedRule -> String
showsPrec :: Int -> TypedRule -> ShowS
$cshowsPrec :: Int -> TypedRule -> ShowS
Show

instance Pretty TypedRule where
  pretty :: TypedRule -> Doc
pretty (TypedRule r :: Rule
r (RelType c1 :: Concept
c1 c2 :: Concept
c2)) =
    [Doc] -> Doc
fsep [Rule -> Doc
forall a. Pretty a => a -> Doc
pretty Rule
r Doc -> Doc -> Doc
<+> String -> Doc
text "::", Concept -> Doc
forall a. Pretty a => a -> Doc
pretty Concept
c1 Doc -> Doc -> Doc
<+> Doc
cross Doc -> Doc -> Doc
<+> Concept -> Doc
forall a. Pretty a => a -> Doc
pretty Concept
c2]

anaRule :: Rule -> State Env Rule
anaRule :: Rule -> State Env Rule
anaRule r :: Rule
r = do
  Sign
s <- (Env -> Sign) -> State Env Sign
forall s a. (s -> a) -> State s a
gets Env -> Sign
sign
  case Sign -> Rule -> [TypedRule]
typeRule Sign
s Rule
r of
    [] -> do
      [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Rule -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "no typing found" (Rule -> Diagnosis) -> Rule -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Sign -> Rule -> Rule
findTypeFailure Sign
s Rule
r]
      Rule -> State Env Rule
forall (m :: * -> *) a. Monad m => a -> m a
return Rule
r
    l :: [TypedRule]
l@(TypedRule e :: Rule
e (RelType c1 :: Concept
c1 c2 :: Concept
c2) : t :: [TypedRule]
t) -> do
      if [TypedRule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypedRule]
t then do
        case Concept
c1 of
          Anything -> [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Rule -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "source concept is anything" Rule
r]
          _ -> () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        case Concept
c2 of
          Anything -> [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Rule -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "target concept is anything" Rule
r]
          _ -> () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
          ([String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ "ambiguous typings found:"
            String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (TypedRule -> String) -> [TypedRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (TypedRule -> ShowS
forall a. Pretty a => a -> ShowS
`showDoc` "") [TypedRule]
l) (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Rule -> Range
forall a. GetRange a => a -> Range
getRangeSpan Rule
r]
      Rule -> State Env Rule
forall (m :: * -> *) a. Monad m => a -> m a
return Rule
e

findTypeFailure :: Sign -> Rule -> Rule
findTypeFailure :: Sign -> Rule -> Rule
findTypeFailure s :: Sign
s r :: Rule
r = case Rule
r of
  Tm _ -> Rule
r
  UnExp _ e :: Rule
e -> if [TypedRule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Sign -> Rule -> [TypedRule]
typeRule Sign
s Rule
e) then Sign -> Rule -> Rule
findTypeFailure Sign
s Rule
e else Rule
r
  MulExp o :: MulOp
o es :: [Rule]
es -> case [Rule]
es of
    [] -> String -> Rule
forall a. HasCallStack => String -> a
error "findTypeFailure"
    e :: Rule
e : t :: [Rule]
t | [TypedRule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Sign -> Rule -> [TypedRule]
typeRule Sign
s Rule
e) -> Sign -> Rule -> Rule
findTypeFailure Sign
s Rule
e
          | [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rule]
t -> Rule
e
          | Bool
otherwise -> let n :: Rule
n = MulOp -> [Rule] -> Rule
MulExp MulOp
o [Rule]
t in if [TypedRule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Sign -> Rule -> [TypedRule]
typeRule Sign
s Rule
n)
                                               then Sign -> Rule -> Rule
findTypeFailure Sign
s Rule
n else Rule
r

-- | analyze rule and return resolved one
typeRule :: Sign -> Rule -> [TypedRule]
typeRule :: Sign -> Rule -> [TypedRule]
typeRule s :: Sign
s rule :: Rule
rule =
  let m :: RelMap
m = Sign -> RelMap
rels Sign
s
      i :: Rel Concept
i = Sign -> Rel Concept
isas Sign
s
  in case Rule
rule of
   Tm (Sgn n :: Token
n ty :: RelType
ty@(RelType rs :: Concept
rs rt :: Concept
rt)) -> let str :: String
str = Token -> String
tokStr Token
n in
      if String
str String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "V" then [Rule -> RelType -> TypedRule
TypedRule Rule
rule RelType
ty] else
      if String
str String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "I" then case (Concept
rs, Concept
rt) of
        (Anything, Anything) ->
          (Concept -> TypedRule) -> [Concept] -> [TypedRule]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Concept
c -> let y :: RelType
y = Concept -> Concept -> RelType
RelType Concept
c Concept
c in Rule -> RelType -> TypedRule
TypedRule (Relation -> Rule
Tm (Relation -> Rule) -> Relation -> Rule
forall a b. (a -> b) -> a -> b
$ Token -> RelType -> Relation
Sgn Token
n RelType
y) RelType
y)
          ([Concept] -> [TypedRule])
-> (Set Concept -> [Concept]) -> Set Concept -> [TypedRule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Concept -> Concept -> Bool) -> [Concept] -> [Concept]
forall a. (a -> a -> Bool) -> [a] -> [a]
keepMins ((Concept -> Concept -> Bool) -> Concept -> Concept -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Concept -> Concept -> Bool) -> Concept -> Concept -> Bool)
-> (Concept -> Concept -> Bool) -> Concept -> Concept -> Bool
forall a b. (a -> b) -> a -> b
$ Rel Concept -> Concept -> Concept -> Bool
isSubConcept Rel Concept
i) ([Concept] -> [Concept])
-> (Set Concept -> [Concept]) -> Set Concept -> [Concept]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Concept -> [Concept]
forall a. Set a -> [a]
Set.toList (Set Concept -> [TypedRule]) -> Set Concept -> [TypedRule]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Concept
conceptsOf Sign
s
        _ -> case Rel Concept -> Concept -> Concept -> Maybe Concept
compatible Rel Concept
i Concept
rs Concept
rt of
          Just c :: Concept
c -> let y :: RelType
y = Concept -> Concept -> RelType
RelType Concept
c Concept
c in [Rule -> RelType -> TypedRule
TypedRule (Relation -> Rule
Tm (Relation -> Rule) -> Relation -> Rule
forall a b. (a -> b) -> a -> b
$ Token -> RelType -> Relation
Sgn Token
n RelType
y) RelType
y]
          Nothing -> []
      else (RelType -> [TypedRule] -> [TypedRule])
-> [TypedRule] -> Set RelType -> [TypedRule]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold
      (\ (RelType f :: Concept
f t :: Concept
t) l :: [TypedRule]
l -> Maybe TypedRule -> [TypedRule]
forall a. Maybe a -> [a]
maybeToList (do
              Concept
a <- Rel Concept -> Concept -> Concept -> Maybe Concept
compatible Rel Concept
i Concept
f Concept
rs
              Concept
b <- Rel Concept -> Concept -> Concept -> Maybe Concept
compatible Rel Concept
i Concept
t Concept
rt
              let y :: RelType
y = Concept -> Concept -> RelType
RelType Concept
a Concept
b
              TypedRule -> Maybe TypedRule
forall (m :: * -> *) a. Monad m => a -> m a
return (TypedRule -> Maybe TypedRule) -> TypedRule -> Maybe TypedRule
forall a b. (a -> b) -> a -> b
$ Rule -> RelType -> TypedRule
TypedRule (Relation -> Rule
Tm (Relation -> Rule) -> Relation -> Rule
forall a b. (a -> b) -> a -> b
$ Token -> RelType -> Relation
Sgn Token
n RelType
y) RelType
y) [TypedRule] -> [TypedRule] -> [TypedRule]
forall a. [a] -> [a] -> [a]
++ [TypedRule]
l) []
      (Set RelType -> [TypedRule]) -> Set RelType -> [TypedRule]
forall a b. (a -> b) -> a -> b
$ Set RelType -> Id -> RelMap -> Set RelType
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set RelType
forall a. Set a
Set.empty (Token -> Id
simpleIdToId Token
n) RelMap
m
   UnExp o :: UnOp
o r :: Rule
r -> (TypedRule -> [TypedRule]) -> [TypedRule] -> [TypedRule]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
     (\ (TypedRule e :: Rule
e t :: RelType
t@(RelType a :: Concept
a b :: Concept
b)) -> (RelType -> TypedRule) -> [RelType] -> [TypedRule]
forall a b. (a -> b) -> [a] -> [b]
map (Rule -> RelType -> TypedRule
TypedRule (Rule -> RelType -> TypedRule) -> Rule -> RelType -> TypedRule
forall a b. (a -> b) -> a -> b
$ UnOp -> Rule -> Rule
UnExp UnOp
o Rule
e)
          ([RelType] -> [TypedRule]) -> [RelType] -> [TypedRule]
forall a b. (a -> b) -> a -> b
$ case UnOp
o of
              Co -> [Concept -> Concept -> RelType
RelType Concept
b Concept
a]
              Cp -> [RelType
t]
              _ -> case Rel Concept -> Concept -> Concept -> Maybe Concept
compatible Rel Concept
i Concept
a Concept
b of
                     Nothing -> []
                     Just c :: Concept
c -> [Concept -> Concept -> RelType
RelType Concept
c Concept
c]
     ) ([TypedRule] -> [TypedRule]) -> [TypedRule] -> [TypedRule]
forall a b. (a -> b) -> a -> b
$ Sign -> Rule -> [TypedRule]
typeRule Sign
s Rule
r
   MulExp o :: MulOp
o es :: [Rule]
es -> case [Rule]
es of
     [] -> String -> [TypedRule]
forall a. HasCallStack => String -> a
error "typeRule"
     r :: Rule
r : t :: [Rule]
t -> if [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rule]
t then Sign -> Rule -> [TypedRule]
typeRule Sign
s Rule
r else
       let rs :: [TypedRule]
rs = Sign -> Rule -> [TypedRule]
typeRule Sign
s Rule
r
           ts :: [TypedRule]
ts = Sign -> Rule -> [TypedRule]
typeRule Sign
s (Rule -> [TypedRule]) -> Rule -> [TypedRule]
forall a b. (a -> b) -> a -> b
$ MulOp -> [Rule] -> Rule
MulExp MulOp
o [Rule]
t
       in
         [ Rule -> RelType -> TypedRule
TypedRule Rule
fe RelType
ty
         | TypedRule ne :: Rule
ne (RelType a :: Concept
a b :: Concept
b) <- [TypedRule]
rs
         , TypedRule re :: Rule
re (RelType p :: Concept
p q :: Concept
q) <- [TypedRule]
ts
         , let fe :: Rule
fe = case Rule
re of
                 MulExp op :: MulOp
op nt :: [Rule]
nt | MulOp
op MulOp -> MulOp -> Bool
forall a. Eq a => a -> a -> Bool
== MulOp
o -> MulOp -> [Rule] -> Rule
MulExp MulOp
o ([Rule] -> Rule) -> [Rule] -> Rule
forall a b. (a -> b) -> a -> b
$ Rule
ne Rule -> [Rule] -> [Rule]
forall a. a -> [a] -> [a]
: [Rule]
nt
                 _ -> MulOp -> [Rule] -> Rule
MulExp MulOp
o [Rule
ne, Rule
re]
         , let res :: Maybe RelType
res = if MulOp -> [MulOp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem MulOp
o [MulOp
Fc, MulOp
Fd] then
                 case Rel Concept -> Concept -> Concept -> Maybe Concept
compatible Rel Concept
i Concept
b Concept
p of
                         Nothing -> Maybe RelType
forall a. Maybe a
Nothing
                         Just _ -> RelType -> Maybe RelType
forall a. a -> Maybe a
Just (RelType -> Maybe RelType) -> RelType -> Maybe RelType
forall a b. (a -> b) -> a -> b
$ Concept -> Concept -> RelType
RelType Concept
a Concept
q
                 else do
                   Concept
na <- Rel Concept -> Concept -> Concept -> Maybe Concept
compatible Rel Concept
i Concept
a Concept
p
                   Concept
nb <- Rel Concept -> Concept -> Concept -> Maybe Concept
compatible Rel Concept
i Concept
b Concept
q
                   RelType -> Maybe RelType
forall (m :: * -> *) a. Monad m => a -> m a
return (RelType -> Maybe RelType) -> RelType -> Maybe RelType
forall a b. (a -> b) -> a -> b
$ Concept -> Concept -> RelType
RelType Concept
na Concept
nb
         , Just ty :: RelType
ty <- [Maybe RelType
res]]

compatible :: Rel.Rel Concept -> Concept -> Concept -> Maybe Concept
compatible :: Rel Concept -> Concept -> Concept -> Maybe Concept
compatible r :: Rel Concept
r c1 :: Concept
c1 c2 :: Concept
c2 = case () of
  _ | Rel Concept -> Concept -> Concept -> Bool
isSubConcept Rel Concept
r Concept
c1 Concept
c2 -> Concept -> Maybe Concept
forall a. a -> Maybe a
Just Concept
c1
    | Rel Concept -> Concept -> Concept -> Bool
isSubConcept Rel Concept
r Concept
c2 Concept
c1 -> Concept -> Maybe Concept
forall a. a -> Maybe a
Just Concept
c2
  _ -> Maybe Concept
forall a. Maybe a
Nothing

isSubConcept :: Rel.Rel Concept -> Concept -> Concept -> Bool
isSubConcept :: Rel Concept -> Concept -> Concept -> Bool
isSubConcept r :: Rel Concept
r c1 :: Concept
c1 c2 :: Concept
c2 = Concept
c1 Concept -> Concept -> Bool
forall a. Eq a => a -> a -> Bool
== Concept
c2 Bool -> Bool -> Bool
|| case Concept
c2 of
  Anything -> Bool
True
  _ -> Concept -> Concept -> Rel Concept -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path Concept
c1 Concept
c2 Rel Concept
r

anaAtts :: KeyAtt -> State Env KeyAtt
anaAtts :: KeyAtt -> State Env KeyAtt
anaAtts (KeyAtt m :: Maybe Token
m r :: Rule
r) = do
  Rule
n <- Rule -> State Env Rule
anaRule Rule
r
  KeyAtt -> State Env KeyAtt
forall (m :: * -> *) a. Monad m => a -> m a
return (KeyAtt -> State Env KeyAtt) -> KeyAtt -> State Env KeyAtt
forall a b. (a -> b) -> a -> b
$ Maybe Token -> Rule -> KeyAtt
KeyAtt Maybe Token
m Rule
n

conceptsOf :: Sign -> Set.Set Concept
conceptsOf :: Sign -> Set Concept
conceptsOf = (Symbol -> Set Concept -> Set Concept)
-> Set Concept -> Set Symbol -> Set Concept
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ sy :: Symbol
sy -> case Symbol
sy of
  Con c :: Concept
c -> Concept -> Set Concept -> Set Concept
forall a. Ord a => a -> Set a -> Set a
Set.insert Concept
c
  _ -> Set Concept -> Set Concept
forall a. a -> a
id) Set Concept
forall a. Set a
Set.empty (Set Symbol -> Set Concept)
-> (Sign -> Set Symbol) -> Sign -> Set Concept
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Symbol
symOf

anaObject :: Object -> State Env ()
anaObject :: Object -> State Env ()
anaObject (Object _ r :: Rule
r _ os :: [Object]
os) = do
  Rule -> State Env Rule
anaRule Rule
r
  (Object -> State Env ()) -> [Object] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Object -> State Env ()
anaObject (Object -> State Env ())
-> (Object -> Object) -> Object -> State Env ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ o :: Object
o -> Object
o { expr :: Rule
expr = MulOp -> [Rule] -> Rule
MulExp MulOp
Fc [Rule
r, Object -> Rule
expr Object
o]}) [Object]
os

anaPatElem :: PatElem -> State Env PatElem
anaPatElem :: PatElem -> State Env PatElem
anaPatElem pe :: PatElem
pe = case PatElem
pe of
    Pr h :: RuleHeader
h u :: Rule
u -> do
      Rule
nu <- Rule -> State Env Rule
anaRule Rule
u
      [Named Sen] -> State Env ()
addSens [case RuleHeader
h of
        Always -> String -> Sen -> Named Sen
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sen -> Named Sen) -> Sen -> Named Sen
forall a b. (a -> b) -> a -> b
$ Maybe RuleKind -> Rule -> Sen
Assertion Maybe RuleKind
forall a. Maybe a
Nothing Rule
nu
        RuleHeader k :: RuleKind
k t :: Token
t -> String -> Sen -> Named Sen
forall a s. a -> s -> SenAttr s a
makeNamed (Token -> String
forall a. Show a => a -> String
show Token
t) (Sen -> Named Sen) -> Sen -> Named Sen
forall a b. (a -> b) -> a -> b
$ Maybe RuleKind -> Rule -> Sen
Assertion (RuleKind -> Maybe RuleKind
forall a. a -> Maybe a
Just RuleKind
k) Rule
nu]
      PatElem -> State Env PatElem
forall (m :: * -> *) a. Monad m => a -> m a
return (PatElem -> State Env PatElem) -> PatElem -> State Env PatElem
forall a b. (a -> b) -> a -> b
$ RuleHeader -> Rule -> PatElem
Pr RuleHeader
h Rule
nu
    Pm qs :: [RangedProp]
qs d :: Relation
d@(Sgn _ ty :: RelType
ty@(RelType c1 :: Concept
c1 c2 :: Concept
c2)) b :: Bool
b -> do
      Relation -> State Env ()
addRel Relation
d
      let (nqs :: [RangedProp]
nqs, ws :: [RangedProp]
ws) = if Concept
c1 Concept -> Concept -> Bool
forall a. Eq a => a -> a -> Bool
== Concept
c2 then ([RangedProp]
qs, []) else
            (RangedProp -> Bool)
-> [RangedProp] -> ([RangedProp], [RangedProp])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Prop -> Prop -> Bool
forall a. Ord a => a -> a -> Bool
< Prop
Sym) (Prop -> Bool) -> (RangedProp -> Prop) -> RangedProp -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangedProp -> Prop
propProp) [RangedProp]
qs
      [Diagnosis] -> State Env ()
addMsgs ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (RangedProp -> Diagnosis) -> [RangedProp] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (DiagKind -> String -> RangedProp -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error (String -> RangedProp -> Diagnosis)
-> String -> RangedProp -> Diagnosis
forall a b. (a -> b) -> a -> b
$ "bad concepts "
                     String -> ShowS
forall a. [a] -> [a] -> [a]
++ RelType -> ShowS
forall a. Pretty a => a -> ShowS
showDoc RelType
ty " with property") [RangedProp]
ws
      [Named Sen] -> State Env ()
addSens ([Named Sen] -> State Env ()) -> [Named Sen] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (RangedProp -> Named Sen) -> [RangedProp] -> [Named Sen]
forall a b. (a -> b) -> [a] -> [b]
map (\ q :: RangedProp
q -> String -> Sen -> Named Sen
forall a s. a -> s -> SenAttr s a
makeNamed (Token -> String
forall a. Show a => a -> String
show (Relation -> Token
decnm Relation
d) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_"
                                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ Prop -> String
forall a. Show a => a -> String
showUp (RangedProp -> Prop
propProp RangedProp
q))
                    (Sen -> Named Sen) -> Sen -> Named Sen
forall a b. (a -> b) -> a -> b
$ Relation -> RangedProp -> Sen
DeclProp Relation
d RangedProp
q) [RangedProp]
nqs
      PatElem -> State Env PatElem
forall (m :: * -> *) a. Monad m => a -> m a
return (PatElem -> State Env PatElem) -> PatElem -> State Env PatElem
forall a b. (a -> b) -> a -> b
$ [RangedProp] -> Relation -> Bool -> PatElem
Pm [RangedProp]
nqs Relation
d Bool
b
    Pg c1 :: Concept
c1 c2 :: Concept
c2 -> do
      Concept -> Concept -> State Env ()
addIsa Concept
c1 Concept
c2
      PatElem -> State Env PatElem
forall (m :: * -> *) a. Monad m => a -> m a
return PatElem
pe
    Pk (KeyDef l :: Token
l c :: Concept
c atts :: [KeyAtt]
atts) -> do
       Set Concept
csyms <- (Env -> Set Concept) -> State Env (Set Concept)
forall s a. (s -> a) -> State s a
gets ((Env -> Set Concept) -> State Env (Set Concept))
-> (Env -> Set Concept) -> State Env (Set Concept)
forall a b. (a -> b) -> a -> b
$ Sign -> Set Concept
conceptsOf (Sign -> Set Concept) -> (Env -> Sign) -> Env -> Set Concept
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Sign
sign
       Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Concept -> Set Concept -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Concept
c Set Concept
csyms) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$
         [Diagnosis] -> State Env ()
addMsgs [DiagKind -> String -> Concept -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown KEY concept" Concept
c]
       [KeyAtt]
natts <- (KeyAtt -> State Env KeyAtt) -> [KeyAtt] -> State Env [KeyAtt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM KeyAtt -> State Env KeyAtt
anaAtts [KeyAtt]
atts
       PatElem -> State Env PatElem
forall (m :: * -> *) a. Monad m => a -> m a
return (PatElem -> State Env PatElem) -> PatElem -> State Env PatElem
forall a b. (a -> b) -> a -> b
$ KeyDef -> PatElem
Pk (KeyDef -> PatElem) -> KeyDef -> PatElem
forall a b. (a -> b) -> a -> b
$ Token -> Concept -> [KeyAtt] -> KeyDef
KeyDef Token
l Concept
c [KeyAtt]
natts
    Plug _ o :: Object
o -> do
      Object -> State Env ()
anaObject Object
o
      PatElem -> State Env PatElem
forall (m :: * -> *) a. Monad m => a -> m a
return PatElem
pe
    _ -> PatElem -> State Env PatElem
forall (m :: * -> *) a. Monad m => a -> m a
return PatElem
pe