collect symbols

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9117 cec4b9c1-7d33-0410-9eda-942365e851bb
spechub · Nov 1, 2007 · d976ba4 · d976ba4
1 parent 4eaf4dc
commit d976ba4
Show file tree

Hide file tree

Showing 7 changed files with 69 additions and 49 deletions.
diff --git a/HasCASL/AsToLe.hs b/HasCASL/AsToLe.hs
@@ -86,7 +86,8 @@ basicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->
 basicAnalysis (b, e, ga) =
     let (nb, ne) = runState (anaBasicSpec ga b) e
         in Result (reverse $ envDiags ne) $
-           Just (nb, mkExtSign (cleanEnv ne), reverse $ sentences ne)
+           Just (nb, ExtSign (cleanEnv ne) $ declSymbs ne,
+                 reverse $ sentences ne)
 
 -- | is the signature empty?
 isEmptyEnv :: Env -> Bool

diff --git a/HasCASL/AsUtils.hs b/HasCASL/AsUtils.hs
@@ -149,12 +149,16 @@ isProductIdWithArgs (Id ts cs _) m = let n = length ts in
 mapKindV :: (Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
 mapKindV g f k = case k of
     ClassKind a -> ClassKind $ f a
-    FunKind v a b r -> FunKind (g v) (mapKind f a) (mapKind f b) r
+    FunKind v a b r -> FunKind (g v) (mapKindV g f a) (mapKindV g f b) r
 
 -- | map a kind and keep variance the same
 mapKind :: (a -> b) -> AnyKind a -> AnyKind b
 mapKind = mapKindV id
 
+-- | ignore variances of raw kinds
+inVarRawKind :: RawKind -> RawKind
+inVarRawKind = mapKindV (const InVar) id
+
 -- | compute raw kind (if class ids or no higher kinds)
 toRaw :: Kind -> RawKind
 toRaw = mapKind $ const ()
@@ -189,8 +193,7 @@ mkLazyType t = TypeAppl lazyTypeConstr t
 
 -- | function type
 mkFunArrType :: Type -> Arrow -> Type -> Type
-mkFunArrType t1 a t2 =
-    mkTypeAppl (toFunType a) [t1, t2]
+mkFunArrType t1 a t2 = mkTypeAppl (toFunType a) [t1, t2]
 
 mkFunArrTypeWithRange :: Range -> Type -> Arrow -> Type -> Type
 mkFunArrTypeWithRange r t1 a t2 =

diff --git a/HasCASL/ClassAna.hs b/HasCASL/ClassAna.hs
@@ -150,25 +150,30 @@ addClassDecl rk kind ci =
     if ci == universeId then
        addDiags [mkDiag Warning "void universe class declaration" ci]
     else do
-       cm <- gets classMap
-       tm <- gets typeMap
-       tvs <- gets localTypeVars
+       e <- get
+       let cm = classMap e
+           tm = typeMap e
+           tvs = localTypeVars e
        case Map.lookup ci tm of
          Just _ -> addDiags [mkDiag Error "class name already a type" ci]
          Nothing -> case Map.lookup ci tvs of
              Just _ -> addDiags
                  [mkDiag Error "class name already a type variable" ci]
              Nothing -> case Map.lookup ci cm of
-                 Nothing -> putClassMap $ Map.insert ci
+                 Nothing -> do
+                   addSymbol $ idToClassSymbol e ci rk
+                   putClassMap $ Map.insert ci
                      (ClassInfo rk $ Set.singleton kind) cm
                  Just (ClassInfo ork superClasses) ->
                    let ds = checkKinds ci rk ork in
                    if null ds then
                      if cyclicClassId cm ci kind then
                         addDiags [mkDiag Error "cyclic class" ci]
-                     else if newKind cm kind superClasses then do
-                        addDiags [mkDiag Hint "refined class" ci]
-                        putClassMap $ Map.insert ci
-                          (ClassInfo ork $ addNewKind cm kind superClasses) cm
-                     else addDiags [mkDiag Warning "unchanged class" ci]
+                     else do
+                       addSymbol $ idToClassSymbol e ci ork
+                       if newKind cm kind superClasses then do
+                         addDiags [mkDiag Hint "refined class" ci]
+                         putClassMap $ Map.insert ci
+                           (ClassInfo ork $ addNewKind cm kind superClasses) cm
+                        else addDiags [mkDiag Warning "unchanged class" ci]
                    else addDiags ds
diff --git a/HasCASL/Le.hs b/HasCASL/Le.hs
@@ -164,6 +164,7 @@ data Env = Env
     , assumps :: Assumps
     , localVars :: Map.Map Id VarDefn
     , sentences :: [Named Sentence]
+    , declSymbs :: Set.Set Symbol
     , envDiags :: [Diagnosis]
     , preIds :: (PrecMap, Set.Set Id)
     , globAnnos :: GlobalAnnos
@@ -183,6 +184,7 @@ initialEnv = Env
     , assumps = Map.empty
     , localVars = Map.empty
     , sentences = []
+    , declSymbs = Set.empty
     , envDiags = []
     , preIds = (emptyPrecMap, Set.empty)
     , globAnnos = emptyGlobalAnnos
@@ -239,6 +241,12 @@ fromResult f = do
    addDiags ds
    return mr
 
+-- | add the symbol to the state
+addSymbol :: Symbol -> State.State Env ()
+addSymbol sy = do
+    e <- State.get
+    State.put e { declSymbs = Set.insert sy $ declSymbs e }
+
 -- | store local type variables
 putLocalTypeVars :: LocalTypeVars -> State.State Env ()
 putLocalTypeVars tvs = do
@@ -314,11 +322,11 @@ type SymbolSet = Set.Set Symbol
 
 -- | create a type symbol
 idToTypeSymbol :: Env -> Id -> RawKind -> Symbol
-idToTypeSymbol e idt k = Symbol idt (TypeAsItemType k) e
+idToTypeSymbol e idt k = Symbol idt (TypeAsItemType $ inVarRawKind k) e
 
 -- | create a class symbol
 idToClassSymbol :: Env -> Id -> RawKind -> Symbol
-idToClassSymbol e idt k = Symbol idt (ClassAsItemType k) e
+idToClassSymbol e idt k = Symbol idt (ClassAsItemType $ inVarRawKind k) e
 
 -- | create an operation symbol
 idToOpSymbol :: Env -> Id -> TypeScheme -> Symbol

diff --git a/HasCASL/RawSym.hs b/HasCASL/RawSym.hs
@@ -88,10 +88,12 @@ anaSymbolType t = do
     case t of
         ClassAsItemType k -> do
             let Result ds (Just rk) = anaKindM k cm
-            return $ if null ds then Just $ ClassAsItemType rk else Nothing
+            return $ if null ds then Just $ ClassAsItemType
+                   $ inVarRawKind rk else Nothing
         TypeAsItemType k -> do
             let Result ds (Just rk) = anaKindM k cm
-            return $ if null ds then Just $ TypeAsItemType rk else Nothing
+            return $ if null ds then Just $ TypeAsItemType
+                   $ inVarRawKind rk else Nothing
         OpAsItemType sc -> do
             asc <- anaTypeScheme sc
             return $ fmap OpAsItemType asc

diff --git a/HasCASL/Unify.hs b/HasCASL/Unify.hs
@@ -113,7 +113,7 @@ eps :: Subst
 eps = Map.empty
 
 flatKind :: Type -> RawKind
-flatKind = mapKindV (const InVar) id . rawKindOfType
+flatKind = inVarRawKind . rawKindOfType
 
 noAbs :: Type -> Bool
 noAbs t = case t of

diff --git a/HasCASL/VarDecl.hs b/HasCASL/VarDecl.hs
@@ -117,37 +117,37 @@ isLiberalKind cm ok k = case ok of
 -- | store type as is (warn on redeclared types)
 addTypeKind :: Bool -> TypeDefn -> Id -> RawKind -> Kind
             -> State Env Bool
-addTypeKind warn d i rk k =
-    do tm <- gets typeMap
-       cm <- gets classMap
-       case Map.lookup i tm of
-           Nothing -> do
-               putTypeMap $ Map.insert i (TypeInfo rk (Set.singleton k)
-                                          Set.empty d) tm
-               return True
-           Just (TypeInfo ok oldks sups dfn) -> case isLiberalKind cm ok k of
-                 Just nk -> do
-                   let isNewInst = newKind cm nk oldks
-                       insts = if isNewInst then addNewKind cm nk oldks
-                               else oldks
-                       Result ds mDef = mergeTypeDefn dfn d
-                       Result es mk = minRawKind (show i) ok rk
-                   if warn && not isNewInst && case (dfn, d) of
-                                 (PreDatatype, DatatypeDefn _) -> False
-                                 _ -> True then
-                       addDiags [mkDiag Hint "redeclared type" i]
-                       else return ()
-                   case (mDef, mk) of
-                       (Just newDefn, Just r) -> do
-                           putTypeMap $ Map.insert i
-                               (TypeInfo r insts sups newDefn) tm
-                           return True
-                       _ -> do
-                           addDiags $ map (improveDiag i) $ es ++ ds
-                           return False
-                 Nothing -> do
-                    addDiags $ diffKindDiag i ok rk
-                    return False
+addTypeKind warn d i rk k = do
+  e <- get
+  let tm = typeMap e
+      cm = classMap e
+  case Map.lookup i tm of
+    Nothing -> do
+      addSymbol $ idToTypeSymbol e i rk
+      putTypeMap $ Map.insert i (TypeInfo rk (Set.singleton k) Set.empty d) tm
+      return True
+    Just (TypeInfo ok oldks sups dfn) -> case isLiberalKind cm ok k of
+      Just nk -> do
+        let isNewInst = newKind cm nk oldks
+            insts = if isNewInst then addNewKind cm nk oldks else oldks
+            Result ds mDef = mergeTypeDefn dfn d
+            Result es mk = minRawKind (show i) ok rk
+        if warn && not isNewInst && case (dfn, d) of
+           (PreDatatype, DatatypeDefn _) -> False
+           _ -> True
+          then addDiags [mkDiag Hint "redeclared type" i]
+          else return ()
+        case (mDef, mk) of
+          (Just newDefn, Just r) -> do
+            addSymbol $ idToTypeSymbol e i r
+            putTypeMap $ Map.insert i (TypeInfo r insts sups newDefn) tm
+            return True
+          _ -> do
+            addDiags $ map (improveDiag i) $ es ++ ds
+            return False
+      Nothing -> do
+        addDiags $ diffKindDiag i ok rk
+        return False
 
 nonUniqueKind :: (PosItem a, Pretty a) => Set.Set Kind -> a ->
                  (Kind -> State Env (Maybe b)) -> State Env (Maybe b)
@@ -260,6 +260,7 @@ addOpId i oldSc attrs dfn = do
     case mo of
       Nothing -> return False
       Just oi -> do
+        addSymbol $ idToOpSymbol e i $ opType oi
         putAssumps $ Map.insert i (Set.insert oi r) as
         return True