{- |
Module      :  ./HasCASL/AsToLe.hs
Description :  final static analysis
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

conversion from As to Le
-}

module HasCASL.AsToLe where

import HasCASL.As
import HasCASL.Le
import HasCASL.ClassAna
import HasCASL.VarDecl
import HasCASL.Unify
import HasCASL.OpDecl
import HasCASL.TypeAna
import HasCASL.TypeDecl
import HasCASL.Builtin
import HasCASL.PrintLe
import HasCASL.Merge

import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Id
import Common.Result
import Common.ExtSign
import Common.Prec
import Common.Lib.State

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

-- * extract predicate ids from As for mixfix analysis

type Ids = Set.Set Id

unite :: [Ids] -> Ids
unite :: [Ids] -> Ids
unite = [Ids] -> Ids
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions

idsOfBasicSpec :: BasicSpec -> Ids
idsOfBasicSpec :: BasicSpec -> Ids
idsOfBasicSpec (BasicSpec l :: [Annoted BasicItem]
l) = [Ids] -> Ids
unite ([Ids] -> Ids) -> [Ids] -> Ids
forall a b. (a -> b) -> a -> b
$ (Annoted BasicItem -> Ids) -> [Annoted BasicItem] -> [Ids]
forall a b. (a -> b) -> [a] -> [b]
map (BasicItem -> Ids
idsOfBasicItem (BasicItem -> Ids)
-> (Annoted BasicItem -> BasicItem) -> Annoted BasicItem -> Ids
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BasicItem -> BasicItem
forall a. Annoted a -> a
item) [Annoted BasicItem]
l

idsOfBasicItem :: BasicItem -> Ids
idsOfBasicItem :: BasicItem -> Ids
idsOfBasicItem bi :: BasicItem
bi = case BasicItem
bi of
    SigItems i :: SigItems
i -> SigItems -> Ids
idsOfSigItems SigItems
i
    ClassItems _ l :: [Annoted ClassItem]
l _ -> [Ids] -> Ids
unite ([Ids] -> Ids) -> [Ids] -> Ids
forall a b. (a -> b) -> a -> b
$ (Annoted ClassItem -> Ids) -> [Annoted ClassItem] -> [Ids]
forall a b. (a -> b) -> [a] -> [b]
map (ClassItem -> Ids
idsOfClassItem (ClassItem -> Ids)
-> (Annoted ClassItem -> ClassItem) -> Annoted ClassItem -> Ids
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted ClassItem -> ClassItem
forall a. Annoted a -> a
item) [Annoted ClassItem]
l
    GenItems l :: [Annoted SigItems]
l _ -> [Ids] -> Ids
unite ([Ids] -> Ids) -> [Ids] -> Ids
forall a b. (a -> b) -> a -> b
$ (Annoted SigItems -> Ids) -> [Annoted SigItems] -> [Ids]
forall a b. (a -> b) -> [a] -> [b]
map (SigItems -> Ids
idsOfSigItems (SigItems -> Ids)
-> (Annoted SigItems -> SigItems) -> Annoted SigItems -> Ids
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SigItems -> SigItems
forall a. Annoted a -> a
item) [Annoted SigItems]
l
    Internal l :: [Annoted BasicItem]
l _ -> [Ids] -> Ids
unite ([Ids] -> Ids) -> [Ids] -> Ids
forall a b. (a -> b) -> a -> b
$ (Annoted BasicItem -> Ids) -> [Annoted BasicItem] -> [Ids]
forall a b. (a -> b) -> [a] -> [b]
map (BasicItem -> Ids
idsOfBasicItem (BasicItem -> Ids)
-> (Annoted BasicItem -> BasicItem) -> Annoted BasicItem -> Ids
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BasicItem -> BasicItem
forall a. Annoted a -> a
item) [Annoted BasicItem]
l
    _ -> Ids
forall a. Set a
Set.empty

idsOfClassItem :: ClassItem -> Ids
idsOfClassItem :: ClassItem -> Ids
idsOfClassItem (ClassItem _ l :: [Annoted BasicItem]
l _) = [Ids] -> Ids
unite ([Ids] -> Ids) -> [Ids] -> Ids
forall a b. (a -> b) -> a -> b
$ (Annoted BasicItem -> Ids) -> [Annoted BasicItem] -> [Ids]
forall a b. (a -> b) -> [a] -> [b]
map (BasicItem -> Ids
idsOfBasicItem (BasicItem -> Ids)
-> (Annoted BasicItem -> BasicItem) -> Annoted BasicItem -> Ids
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BasicItem -> BasicItem
forall a. Annoted a -> a
item) [Annoted BasicItem]
l

idsOfSigItems :: SigItems -> Ids
idsOfSigItems :: SigItems -> Ids
idsOfSigItems si :: SigItems
si = case SigItems
si of
    TypeItems {} -> Ids
forall a. Set a
Set.empty
    OpItems b :: OpBrand
b l :: [Annoted OpItem]
l _ -> [Ids] -> Ids
unite ([Ids] -> Ids) -> [Ids] -> Ids
forall a b. (a -> b) -> a -> b
$ (Annoted OpItem -> Ids) -> [Annoted OpItem] -> [Ids]
forall a b. (a -> b) -> [a] -> [b]
map (OpBrand -> OpItem -> Ids
idsOfOpItem OpBrand
b (OpItem -> Ids)
-> (Annoted OpItem -> OpItem) -> Annoted OpItem -> Ids
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted OpItem -> OpItem
forall a. Annoted a -> a
item) [Annoted OpItem]
l

idsOfOpItem :: OpBrand -> OpItem -> Ids
idsOfOpItem :: OpBrand -> OpItem -> Ids
idsOfOpItem b :: OpBrand
b oi :: OpItem
oi = let
    stripCompound :: PolyId -> Id
stripCompound (PolyId (Id ts :: [Token]
ts _ ps :: Range
ps) _ _) = [Token] -> [Id] -> Range -> Id
Id [Token]
ts [] Range
ps
    getPolyId :: PolyId -> Id
getPolyId (PolyId i :: Id
i _ _) = Id
i
    in case OpItem
oi of
    OpDecl os :: [PolyId]
os _ _ _ -> case OpBrand
b of
        Pred -> Ids -> Ids -> Ids
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([Id] -> Ids
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Ids) -> [Id] -> Ids
forall a b. (a -> b) -> a -> b
$ (PolyId -> Id) -> [PolyId] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map PolyId -> Id
getPolyId [PolyId]
os) (Ids -> Ids) -> Ids -> Ids
forall a b. (a -> b) -> a -> b
$ [Id] -> Ids
forall a. Ord a => [a] -> Set a
Set.fromList
                ([Id] -> Ids) -> [Id] -> Ids
forall a b. (a -> b) -> a -> b
$ (PolyId -> Id) -> [PolyId] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map PolyId -> Id
stripCompound [PolyId]
os
        _ -> Ids
forall a. Set a
Set.empty
    OpDefn p :: PolyId
p _ _ _ _ -> case OpBrand
b of
        Pred -> [Id] -> Ids
forall a. Ord a => [a] -> Set a
Set.fromList [PolyId -> Id
getPolyId PolyId
p, PolyId -> Id
stripCompound PolyId
p]
        _ -> Ids
forall a. Set a
Set.empty

-- * basic analysis

-- | basic analysis
basicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->
                 Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])
basicAnalysis :: (BasicSpec, Env, GlobalAnnos)
-> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])
basicAnalysis (b :: BasicSpec
b, e :: Env
e, ga :: GlobalAnnos
ga) =
    let (nb :: BasicSpec
nb, ne :: Env
ne) = State Env BasicSpec -> Env -> (BasicSpec, Env)
forall s a. State s a -> s -> (a, s)
runState (GlobalAnnos -> BasicSpec -> State Env BasicSpec
anaBasicSpec GlobalAnnos
ga BasicSpec
b) Env
e
        in [Diagnosis]
-> Maybe (BasicSpec, ExtSign Env Symbol, [Named Sentence])
-> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])
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]
envDiags Env
ne) (Maybe (BasicSpec, ExtSign Env Symbol, [Named Sentence])
 -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]))
-> Maybe (BasicSpec, ExtSign Env Symbol, [Named Sentence])
-> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])
forall a b. (a -> b) -> a -> b
$
           (BasicSpec, ExtSign Env Symbol, [Named Sentence])
-> Maybe (BasicSpec, ExtSign Env Symbol, [Named Sentence])
forall a. a -> Maybe a
Just (BasicSpec
nb, Env -> Set Symbol -> ExtSign Env Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign (Env -> Env
cleanEnv Env
ne) (Set Symbol -> ExtSign Env Symbol)
-> Set Symbol -> ExtSign Env Symbol
forall a b. (a -> b) -> a -> b
$ Env -> Set Symbol
declSymbs Env
ne,
                 [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a]
reverse ([Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ Env -> [Named Sentence]
sentences Env
ne)

-- | is the first argument a subsignature of the second?
isSubEnv :: Env -> Env -> Bool
isSubEnv :: Env -> Env -> Bool
isSubEnv e1 :: Env
e1 e2 :: Env
e2 =
  let c2 :: ClassMap
c2 = Env -> ClassMap
classMap Env
e2
      cm :: ClassMap
cm = ClassMap -> ClassMap
addCpoMap ClassMap
c2
      t2 :: TypeMap
t2 = Env -> TypeMap
typeMap Env
e2
      tm :: TypeMap
tm = ClassMap -> TypeMap -> TypeMap
addUnit ClassMap
cm TypeMap
t2
      expTy :: OpInfo -> TypeScheme
expTy = TypeMap -> TypeScheme -> TypeScheme
expand TypeMap
tm (TypeScheme -> TypeScheme)
-> (OpInfo -> TypeScheme) -> OpInfo -> TypeScheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
opType
  in (ClassInfo -> ClassInfo -> Bool) -> ClassMap -> ClassMap -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy (\ (ClassInfo _ k1 :: Set Kind
k1) (ClassInfo _ k2 :: Set Kind
k2) ->
       Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$ (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter
         (\ k :: Kind
k -> Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$ (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Kind -> Kind -> Bool) -> Kind -> Kind -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm) Kind
k) Set Kind
k2) Set Kind
k1)
     (Env -> ClassMap
classMap Env
e1) ClassMap
c2
     Bool -> Bool -> Bool
&& (TypeInfo -> TypeInfo -> Bool) -> TypeMap -> TypeMap -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy (\ ti1 :: TypeInfo
ti1 ti2 :: TypeInfo
ti2 -> let
        k1 :: Set Kind
k1 = TypeInfo -> Set Kind
otherTypeKinds TypeInfo
ti1
        k2 :: Set Kind
k2 = TypeInfo -> Set Kind
otherTypeKinds TypeInfo
ti2
        in Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$ (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ k :: Kind
k -> Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$
                  (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Kind -> Kind -> Bool) -> Kind -> Kind -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm) Kind
k) Set Kind
k2) Set Kind
k1)
     (Env -> TypeMap
typeMap Env
e1) (Env -> TypeMap
typeMap Env
e2)
     Bool -> Bool -> Bool
&& (Set OpInfo -> Set OpInfo -> Bool)
-> Map Id (Set OpInfo) -> Map Id (Set OpInfo) -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy (\ s1 :: Set OpInfo
s1 s2 :: Set OpInfo
s2 ->
         (OpInfo -> Bool) -> [OpInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ t :: OpInfo
t -> (OpInfo -> Bool) -> [OpInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool
instScheme TypeMap
tm 1 (OpInfo -> TypeScheme
expTy OpInfo
t) (TypeScheme -> Bool) -> (OpInfo -> TypeScheme) -> OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
expTy)
             ([OpInfo] -> Bool) -> [OpInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
s2)
         ([OpInfo] -> Bool) -> [OpInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
s1) (Env -> Map Id (Set OpInfo)
assumps Env
e1) (Env -> Map Id (Set OpInfo)
assumps Env
e2)

-- | compute difference of signatures
diffEnv :: Env -> Env -> Env
diffEnv :: Env -> Env -> Env
diffEnv e1 :: Env
e1 e2 :: Env
e2 = let
    tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
e2
    cm :: ClassMap
cm = ClassMap -> ClassMap -> ClassMap
diffClassMap (Env -> ClassMap
classMap Env
e1) (ClassMap -> ClassMap) -> ClassMap -> ClassMap
forall a b. (a -> b) -> a -> b
$ Env -> ClassMap
classMap Env
e2
    acm :: ClassMap
acm = ClassMap -> ClassMap -> ClassMap
addClassMap (Env -> ClassMap
classMap Env
e1) (ClassMap -> ClassMap) -> ClassMap -> ClassMap
forall a b. (a -> b) -> a -> b
$ Env -> ClassMap
classMap Env
e2
    in Env
initialEnv
       { classMap :: ClassMap
classMap = ClassMap
cm
       , typeMap :: TypeMap
typeMap = ClassMap -> TypeMap -> TypeMap -> TypeMap
diffTypeMap ClassMap
acm (Env -> TypeMap
typeMap Env
e1) TypeMap
tm
       , assumps :: Map Id (Set OpInfo)
assumps = (Set OpInfo -> Set OpInfo -> Maybe (Set OpInfo))
-> Map Id (Set OpInfo)
-> Map Id (Set OpInfo)
-> Map Id (Set OpInfo)
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith Set OpInfo -> Set OpInfo -> Maybe (Set OpInfo)
diffAss (Env -> Map Id (Set OpInfo)
assumps Env
e1) (Map Id (Set OpInfo) -> Map Id (Set OpInfo))
-> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e2
       , binders :: Map Id Id
binders = (Id -> Id -> Maybe Id) -> Map Id Id -> Map Id Id -> Map Id Id
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith
           (\ i1 :: Id
i1 i2 :: Id
i2 -> if Id
i1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
i2 then Maybe Id
forall a. Maybe a
Nothing else Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i1)
           (Env -> Map Id Id
binders Env
e1) (Map Id Id -> Map Id Id) -> Map Id Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ Env -> Map Id Id
binders Env
e2 }

-- | compute difference of operations
diffAss :: Set.Set OpInfo -> Set.Set OpInfo
        -> Maybe (Set.Set OpInfo)
diffAss :: Set OpInfo -> Set OpInfo -> Maybe (Set OpInfo)
diffAss s1 :: Set OpInfo
s1 s2 :: Set OpInfo
s2 =
    let s3 :: Set OpInfo
s3 = Set OpInfo -> Set OpInfo -> Set OpInfo
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set OpInfo
s1 Set OpInfo
s2 in
        if Set OpInfo -> Bool
forall a. Set a -> Bool
Set.null Set OpInfo
s3 then Maybe (Set OpInfo)
forall a. Maybe a
Nothing else Set OpInfo -> Maybe (Set OpInfo)
forall a. a -> Maybe a
Just Set OpInfo
s3

-- | clean up finally accumulated environment
cleanEnv :: Env -> Env
cleanEnv :: Env -> Env
cleanEnv e :: Env
e = Env -> Env
delPreDefs Env
initialEnv
             { classMap :: ClassMap
classMap = Env -> ClassMap
classMap Env
e
             , typeMap :: TypeMap
typeMap = Env -> TypeMap
typeMap Env
e
             , assumps :: Map Id (Set OpInfo)
assumps = Env -> Map Id (Set OpInfo)
assumps Env
e
             , binders :: Map Id Id
binders = Env -> Map Id Id
binders Env
e }

-- | analyse basic spec
anaBasicSpec :: GlobalAnnos -> BasicSpec -> State Env BasicSpec
anaBasicSpec :: GlobalAnnos -> BasicSpec -> State Env BasicSpec
anaBasicSpec ga :: GlobalAnnos
ga b :: BasicSpec
b@(BasicSpec l :: [Annoted BasicItem]
l) = do
    Env
e <- State Env Env
forall s. State s s
get
    let newAs :: Map Id (Set OpInfo)
newAs = Env -> Map Id (Set OpInfo)
assumps Env
e
        preds :: Ids
preds = Map Id (Set OpInfo) -> Ids
forall k a. Map k a -> Set k
Map.keysSet (Map Id (Set OpInfo) -> Ids) -> Map Id (Set OpInfo) -> Ids
forall a b. (a -> b) -> a -> b
$ (Set OpInfo -> Bool) -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool) -> (Set OpInfo -> Bool) -> Set OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set OpInfo -> Bool
forall a. Set a -> Bool
Set.null (Set OpInfo -> Bool)
-> (Set OpInfo -> Set OpInfo) -> Set OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpInfo -> Bool) -> Set OpInfo -> Set OpInfo
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ( \ oi :: OpInfo
oi ->
                                 case OpInfo -> OpDefn
opDefn OpInfo
oi of
                                 NoOpDefn Pred -> Bool
True
                                 Definition Pred _ -> Bool
True
                                 _ -> Bool
False)) Map Id (Set OpInfo)
newAs
        newPreds :: Ids
newPreds = BasicSpec -> Ids
idsOfBasicSpec BasicSpec
b
        rels :: Ids
rels = Ids -> Ids -> Ids
forall a. Ord a => Set a -> Set a -> Set a
Set.union Ids
preds Ids
newPreds
        newGa :: GlobalAnnos
newGa = GlobalAnnos -> GlobalAnnos
addBuiltins GlobalAnnos
ga
        precs :: PrecMap
precs = Rel Id -> PrecMap
mkPrecIntMap (Rel Id -> PrecMap) -> Rel Id -> PrecMap
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Rel Id
prec_annos GlobalAnnos
newGa
        Result _ (Just ne :: Env
ne) = Env -> Env -> Result Env
merge Env
preEnv Env
e
    Env -> State Env ()
forall s. s -> State s ()
put Env
ne { preIds :: (PrecMap, Ids)
preIds = (PrecMap
precs, Ids
rels), globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
newGa }
    [Annoted BasicItem]
ul <- (BasicItem -> State Env BasicItem)
-> [Annoted BasicItem] -> State Env [Annoted BasicItem]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM BasicItem -> State Env BasicItem
anaBasicItem [Annoted BasicItem]
l
    BasicSpec -> State Env BasicSpec
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicSpec -> State Env BasicSpec)
-> BasicSpec -> State Env BasicSpec
forall a b. (a -> b) -> a -> b
$ [Annoted BasicItem] -> BasicSpec
BasicSpec [Annoted BasicItem]
ul

-- | analyse basic item
anaBasicItem :: BasicItem -> State Env BasicItem
anaBasicItem :: BasicItem -> State Env BasicItem
anaBasicItem bi :: BasicItem
bi = case BasicItem
bi of
    SigItems i :: SigItems
i -> (SigItems -> BasicItem)
-> State Env SigItems -> State Env BasicItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SigItems -> BasicItem
SigItems (State Env SigItems -> State Env BasicItem)
-> State Env SigItems -> State Env BasicItem
forall a b. (a -> b) -> a -> b
$ GenKind -> SigItems -> State Env SigItems
anaSigItems GenKind
Loose SigItems
i
    ClassItems inst :: Instance
inst l :: [Annoted ClassItem]
l ps :: Range
ps -> do
       [Annoted ClassItem]
ul <- (ClassItem -> State Env ClassItem)
-> [Annoted ClassItem] -> State Env [Annoted ClassItem]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Instance -> ClassItem -> State Env ClassItem
anaClassItem Instance
inst) [Annoted ClassItem]
l
       BasicItem -> State Env BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> State Env BasicItem)
-> BasicItem -> State Env BasicItem
forall a b. (a -> b) -> a -> b
$ Instance -> [Annoted ClassItem] -> Range -> BasicItem
ClassItems Instance
inst [Annoted ClassItem]
ul Range
ps
    GenVarItems l :: [GenVarDecl]
l ps :: Range
ps -> do
       [Maybe GenVarDecl]
ul <- (GenVarDecl -> State Env (Maybe GenVarDecl))
-> [GenVarDecl] -> State Env [Maybe GenVarDecl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> GenVarDecl -> State Env (Maybe GenVarDecl)
anaddGenVarDecl Bool
True) [GenVarDecl]
l
       BasicItem -> State Env BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> State Env BasicItem)
-> BasicItem -> State Env BasicItem
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Range -> BasicItem
GenVarItems ([Maybe GenVarDecl] -> [GenVarDecl]
forall a. [Maybe a] -> [a]
catMaybes [Maybe GenVarDecl]
ul) Range
ps
    ProgItems l :: [Annoted ProgEq]
l ps :: Range
ps -> do
       [Annoted ProgEq]
ul <- (Annoted ProgEq -> State Env (Maybe ProgEq))
-> [Annoted ProgEq] -> State Env [Annoted ProgEq]
forall (m :: * -> *) a b.
Monad m =>
(Annoted a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]
mapAnMaybe Annoted ProgEq -> State Env (Maybe ProgEq)
anaProgEq [Annoted ProgEq]
l
       BasicItem -> State Env BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> State Env BasicItem)
-> BasicItem -> State Env BasicItem
forall a b. (a -> b) -> a -> b
$ [Annoted ProgEq] -> Range -> BasicItem
ProgItems [Annoted ProgEq]
ul Range
ps
    FreeDatatype l :: [Annoted DatatypeDecl]
l ps :: Range
ps -> do
       [Annoted DatatypeDecl]
al <- (Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl))
-> [Annoted DatatypeDecl] -> State Env [Annoted DatatypeDecl]
forall (m :: * -> *) a b.
Monad m =>
(Annoted a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]
mapAnMaybe Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
ana1Datatype [Annoted DatatypeDecl]
l
       [DataPat]
tys <- (Annoted DatatypeDecl -> State Env DataPat)
-> [Annoted DatatypeDecl] -> State Env [DataPat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (DatatypeDecl -> State Env DataPat
dataPatToType (DatatypeDecl -> State Env DataPat)
-> (Annoted DatatypeDecl -> DatatypeDecl)
-> Annoted DatatypeDecl
-> State Env DataPat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted DatatypeDecl -> DatatypeDecl
forall a. Annoted a -> a
item) [Annoted DatatypeDecl]
al
       [Annoted DatatypeDecl]
ul <- (Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl))
-> [Annoted DatatypeDecl] -> State Env [Annoted DatatypeDecl]
forall (m :: * -> *) a b.
Monad m =>
(Annoted a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]
mapAnMaybe (GenKind
-> [DataPat]
-> Annoted DatatypeDecl
-> State Env (Maybe DatatypeDecl)
anaDatatype GenKind
Free [DataPat]
tys) [Annoted DatatypeDecl]
al
       [DataPat] -> State Env ()
addDataSen [DataPat]
tys
       BasicItem -> State Env BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> State Env BasicItem)
-> BasicItem -> State Env BasicItem
forall a b. (a -> b) -> a -> b
$ [Annoted DatatypeDecl] -> Range -> BasicItem
FreeDatatype [Annoted DatatypeDecl]
ul Range
ps
    GenItems l :: [Annoted SigItems]
l ps :: Range
ps -> do
       [Annoted SigItems]
ul <- (SigItems -> State Env SigItems)
-> [Annoted SigItems] -> State Env [Annoted SigItems]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (GenKind -> SigItems -> State Env SigItems
anaSigItems GenKind
Generated) [Annoted SigItems]
l
       BasicItem -> State Env BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> State Env BasicItem)
-> BasicItem -> State Env BasicItem
forall a b. (a -> b) -> a -> b
$ [Annoted SigItems] -> Range -> BasicItem
GenItems [Annoted SigItems]
ul Range
ps
    AxiomItems decls :: [GenVarDecl]
decls fs :: [Annoted Term]
fs ps :: Range
ps -> do
       LocalTypeVars
tm <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars -- save type map
       Map Id VarDefn
vs <- (Env -> Map Id VarDefn) -> State Env (Map Id VarDefn)
forall s a. (s -> a) -> State s a
gets Env -> Map Id VarDefn
localVars -- save vars
       [Maybe GenVarDecl]
ds <- (GenVarDecl -> State Env (Maybe GenVarDecl))
-> [GenVarDecl] -> State Env [Maybe GenVarDecl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> GenVarDecl -> State Env (Maybe GenVarDecl)
anaddGenVarDecl Bool
True) [GenVarDecl]
decls
       [Maybe (Annoted Term, Annoted Term)]
ts <- (Annoted Term -> State Env (Maybe (Annoted Term, Annoted Term)))
-> [Annoted Term] -> State Env [Maybe (Annoted Term, Annoted Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Annoted Term -> State Env (Maybe (Annoted Term, Annoted Term))
anaFormula [Annoted Term]
fs
       Env
e <- State Env Env
forall s. State s s
get
       Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs -- restore
       LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tm -- restore
       let newFs :: [(Annoted Term, Annoted Term)]
newFs = [Maybe (Annoted Term, Annoted Term)]
-> [(Annoted Term, Annoted Term)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Annoted Term, Annoted Term)]
ts
           newDs :: [GenVarDecl]
newDs = [Maybe GenVarDecl] -> [GenVarDecl]
forall a. [Maybe a] -> [a]
catMaybes [Maybe GenVarDecl]
ds
           sens :: [Named Sentence]
sens = ((Annoted Term, Annoted Term) -> Named Sentence)
-> [(Annoted Term, Annoted Term)] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (_, f :: Annoted Term
f) -> Annoted Sentence -> Named Sentence
forall a. Annoted a -> Named a
makeNamedSen (Annoted Sentence -> Named Sentence)
-> Annoted Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Sentence -> Annoted Term -> Annoted Sentence
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted (Term -> Sentence
Formula
                                (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Range -> Term
mkEnvForall Env
e (Annoted Term -> Term
forall a. Annoted a -> a
item Annoted Term
f) Range
ps) Annoted Term
f) [(Annoted Term, Annoted Term)]
newFs
       [Named Sentence] -> State Env ()
appendSentences [Named Sentence]
sens
       BasicItem -> State Env BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> State Env BasicItem)
-> BasicItem -> State Env BasicItem
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> [Annoted Term] -> Range -> BasicItem
AxiomItems [GenVarDecl]
newDs (((Annoted Term, Annoted Term) -> Annoted Term)
-> [(Annoted Term, Annoted Term)] -> [Annoted Term]
forall a b. (a -> b) -> [a] -> [b]
map (Annoted Term, Annoted Term) -> Annoted Term
forall a b. (a, b) -> a
fst [(Annoted Term, Annoted Term)]
newFs) Range
ps
    Internal l :: [Annoted BasicItem]
l ps :: Range
ps -> do
       [Annoted BasicItem]
ul <- (BasicItem -> State Env BasicItem)
-> [Annoted BasicItem] -> State Env [Annoted BasicItem]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM BasicItem -> State Env BasicItem
anaBasicItem [Annoted BasicItem]
l
       BasicItem -> State Env BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> State Env BasicItem)
-> BasicItem -> State Env BasicItem
forall a b. (a -> b) -> a -> b
$ [Annoted BasicItem] -> Range -> BasicItem
Internal [Annoted BasicItem]
ul Range
ps

-- | analyse sig items
anaSigItems :: GenKind -> SigItems -> State Env SigItems
anaSigItems :: GenKind -> SigItems -> State Env SigItems
anaSigItems gk :: GenKind
gk si :: SigItems
si = case SigItems
si of
    TypeItems inst :: Instance
inst l :: [Annoted TypeItem]
l ps :: Range
ps -> do
       [Annoted TypeItem]
ul <- GenKind -> [Annoted TypeItem] -> State Env [Annoted TypeItem]
anaTypeItems GenKind
gk [Annoted TypeItem]
l
       SigItems -> State Env SigItems
forall (m :: * -> *) a. Monad m => a -> m a
return (SigItems -> State Env SigItems) -> SigItems -> State Env SigItems
forall a b. (a -> b) -> a -> b
$ Instance -> [Annoted TypeItem] -> Range -> SigItems
TypeItems Instance
inst [Annoted TypeItem]
ul Range
ps
    OpItems b :: OpBrand
b l :: [Annoted OpItem]
l ps :: Range
ps -> do
       [Annoted (Maybe OpItem)]
ul <- (Annoted OpItem -> State Env (Annoted (Maybe OpItem)))
-> [Annoted OpItem] -> State Env [Annoted (Maybe OpItem)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (OpBrand -> Annoted OpItem -> State Env (Annoted (Maybe OpItem))
anaOpItem OpBrand
b) [Annoted OpItem]
l
       let al :: [Annoted OpItem]
al = (Annoted (Maybe OpItem) -> [Annoted OpItem] -> [Annoted OpItem])
-> [Annoted OpItem] -> [Annoted (Maybe OpItem)] -> [Annoted OpItem]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ i :: Annoted (Maybe OpItem)
i -> case Annoted (Maybe OpItem) -> Maybe OpItem
forall a. Annoted a -> a
item Annoted (Maybe OpItem)
i of
                    Nothing -> [Annoted OpItem] -> [Annoted OpItem]
forall a. a -> a
id
                    Just v :: OpItem
v -> (OpItem -> Annoted (Maybe OpItem) -> Annoted OpItem
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted OpItem
v Annoted (Maybe OpItem)
i Annoted OpItem -> [Annoted OpItem] -> [Annoted OpItem]
forall a. a -> [a] -> [a]
:)) [] [Annoted (Maybe OpItem)]
ul
       SigItems -> State Env SigItems
forall (m :: * -> *) a. Monad m => a -> m a
return (SigItems -> State Env SigItems) -> SigItems -> State Env SigItems
forall a b. (a -> b) -> a -> b
$ OpBrand -> [Annoted OpItem] -> Range -> SigItems
OpItems OpBrand
b [Annoted OpItem]
al Range
ps

-- | analyse a class item
anaClassItem :: Instance -> ClassItem -> State Env ClassItem
anaClassItem :: Instance -> ClassItem -> State Env ClassItem
anaClassItem _ (ClassItem d :: ClassDecl
d l :: [Annoted BasicItem]
l ps :: Range
ps) = do
       ClassDecl
cd <- ClassDecl -> State Env ClassDecl
anaClassDecls ClassDecl
d
       [Annoted BasicItem]
ul <- (BasicItem -> State Env BasicItem)
-> [Annoted BasicItem] -> State Env [Annoted BasicItem]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM BasicItem -> State Env BasicItem
anaBasicItem [Annoted BasicItem]
l
       ClassItem -> State Env ClassItem
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassItem -> State Env ClassItem)
-> ClassItem -> State Env ClassItem
forall a b. (a -> b) -> a -> b
$ ClassDecl -> [Annoted BasicItem] -> Range -> ClassItem
ClassItem ClassDecl
cd [Annoted BasicItem]
ul Range
ps