added a fix for ticket #412

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8513 cec4b9c1-7d33-0410-9eda-942365e851bb

HasCASL/AsToLe.hs

@@ -100,7 +100,7 @@ diffEnv e1 e2 = let
     in initialEnv
        { classMap = cm
        , typeMap = diffTypeMap cm (typeMap e1) tm
-       , assumps = Map.differenceWith (diffAss (filterAliases tm)
+       , assumps = Map.differenceWith (diffAss cm (filterAliases tm)
                          $ addUnit cm tm) (assumps e1) $ assumps e2
        }
 
@@ -109,17 +109,17 @@ diffClass :: ClassInfo -> ClassInfo -> Maybe ClassInfo
 diffClass _ _ = Nothing
 
 -- | compute difference of overloaded operations
-diffAss :: TypeMap -> TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
+diffAss :: ClassMap -> TypeMap -> TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
         -> Maybe (Set.Set OpInfo)
-diffAss tAs tm s1 s2 =
-    let s3 = diffOps tAs tm s1 s2 in
+diffAss cm tAs tm s1 s2 =
+    let s3 = diffOps cm tAs tm s1 s2 in
         if Set.null s3 then Nothing else Just s3
 
-diffOps :: TypeMap -> TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
+diffOps :: ClassMap -> TypeMap -> TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
         -> Set.Set OpInfo
-diffOps tAs tm s1 s2 = if Set.null s1 then s1 else
+diffOps cm tAs tm s1 s2 = if Set.null s1 then s1 else
     let (o, os) = Set.deleteFindMin s1
-        rs = diffOps tAs tm os s2
+        rs = diffOps cm tAs tm os s2
         n = mapOpInfo (id, expandAliases tAs) o
     in if Set.null $ Set.filter
            (instScheme tm 1 (opType n) . expand tAs . opType) s2

HasCASL/Merge.hs

@@ -127,22 +127,26 @@ mergeOpInfos :: ClassMap -> TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
              -> Result (Set.Set OpInfo)
 mergeOpInfos cm tm s1 s2 = do
   nt <- mergeTypeMap cm bTypes tm
-  mergeOps nt s1 s2
+  mergeOps cm nt s1 s2
 
-mergeOps :: TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
+mergeOps :: ClassMap -> TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
          -> Result (Set.Set OpInfo)
-mergeOps tm s1 s2 = if Set.null s1 then return s2 else do
+mergeOps cm tm s1 s2 = if Set.null s1 then return s2 else do
     let (o, os) = Set.deleteFindMin s1
         (es, us) = Set.partition (isUnifiable tm 1 (opType o) . opType) s2
-    s <- mergeOps tm os us
-    r <- foldM (mergeOpInfo tm) o $ Set.toList es
+    s <- mergeOps cm tm os us
+    r <- foldM (mergeOpInfo cm tm) o $ Set.toList es
     return $ Set.insert r s
 
-mergeOpInfo ::  TypeMap -> OpInfo -> OpInfo -> Result OpInfo
-mergeOpInfo tm o1 o2 = do
-    let s1 = opType o1
-        s2 = opType o2
-    sc <- if instScheme tm 1 s2 s1 then return s1
+mergeOpInfo :: ClassMap -> TypeMap -> OpInfo -> OpInfo -> Result OpInfo
+mergeOpInfo cm tm o1 o2 = do
+    let s1@(TypeScheme args1 ty1 _) = opType o1
+        s2@(TypeScheme args2 ty2 _) = opType o2
+    sc <- if ty1 == ty2 then
+              if specializedScheme cm args2 args1 then return s1
+              else if specializedScheme cm args1 args2 then return s2
+              else fail "equal type schemes with uncomparable constraints"
+          else if instScheme tm 1 s2 s1 then return s1
           else if instScheme tm 1 s1 s2 then return s2
                else fail "overlapping but incompatible type schemes"
     let as = Set.union (opAttrs o1) $ opAttrs o2

HasCASL/Unify.hs

@@ -16,6 +16,7 @@ module HasCASL.Unify where
 import HasCASL.As
 import HasCASL.AsUtils
 import HasCASL.PrintAs ()
+import HasCASL.ClassAna
 import HasCASL.TypeAna
 import HasCASL.Le
 
@@ -46,6 +47,14 @@ isUnifiable tm c = asSchemes c (unify tm)
 instScheme :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool
 instScheme tm c = asSchemes c (subsume tm)
 
+specializedScheme :: ClassMap -> [TypeArg] -> [TypeArg] -> Bool
+specializedScheme cm args1 args2 =
+    length args1 == length args2 && and
+        (zipWith (\ (TypeArg _ v1 vk1 _ _ _ _) (TypeArg _ v2 vk2 _ _ _ _) ->
+             (v1 == v2 || v1 == InVar) && case (vk1, vk2) of
+              (VarKind k1, VarKind k2) -> lesserKind cm k1 k2
+              _ -> vk1 == vk2) args1 args2)
+
 -- | lift 'State' Int to 'State' Env
 toEnvState :: State Int a -> State Env a
 toEnvState p =

HasCASL/VarDecl.hs

@@ -228,7 +228,8 @@ addOpId i oldSc attrs dfn =
        e <- get
        let as = assumps e
            tm = typeMap e
-           TypeScheme _ ty _ = sc
+           cm = classMap e
+           TypeScheme args1 ty _ = sc
            ds = if placeCount i > 1 then
                 let (fty, fargs) = getTypeAppl ty in
                    if length fargs == 2 &&
@@ -245,15 +246,22 @@ addOpId i oldSc attrs dfn =
            (l, r) = partitionOpId e i sc
            oInfo = OpInfo sc attrs dfn
        if null ds then
-               do let Result es mo = foldM (mergeOpInfo tm) oInfo
+               do let Result es mo = foldM (mergeOpInfo cm tm) oInfo
                                      $ Set.toList l
                   addDiags $ map (improveDiag i) es
                   if i `elem` map fst bList then addDiags [mkDiag Warning
                       "ignoring declaration for builtin identifier" i]
                       else case Set.toList l of
                         [] -> return ()
-                        [x] | opType x == sc -> addDiags [mkDiag Hint
-                           "repeated declaration of" i]
+                        [OpInfo {opType = TypeScheme args2 ty2 _}]
+                            | ty2 == ty -> addDiags [mkDiag Hint
+                           ((if args1 == args2 then "repeated" else
+                            if specializedScheme cm args2 args1
+                               then "more general" else
+                            if specializedScheme cm args1 args2 then
+                                "ignored specialized" else "uncomparable")
+                            ++ " declaration of '"
+                                   ++ showId i "' with type") ty]
                         _ -> addDiags [mkDiag Warning
                            "overlapping declaration of" i]
                   case mo of

HasCASL/test/AsPattern.hascasl.output

@@ -8,4 +8,4 @@ f : a -> a %(op)%
 %% Sentences -------------------------------------------------------------
 program f (v @ _ : a) : a = v %(pe_f)%
 %% Diagnostics -----------------------------------------------------------
-### Hint 5.9, repeated declaration of 'f'
+### Hint 3.8-3.13, repeated declaration of 'f' with type 'a -> a'

HasCASL/test/BasicSpec.hascasl.output

@@ -145,7 +145,7 @@ true
 ### Hint 11.19, refined class 'a'
 ### Hint 16.7, not a class 's'
 ### Hint 18.15, rebound variable 'x'
-### Hint 18.9, repeated declaration of 'tt'
+### Hint 15.11, repeated declaration of 'tt' with type 's ->? Unit'
 *** Error 20.12, unexpected mixfix token: res
 ### Hint 21.6, rebound variable 'x'
 ### Hint 21.6, rebound variable 'x'
@@ -200,10 +200,10 @@ true
 ### Hint 45.8, rebound variable 'x'
 ### Hint 45.16, not a class 't'
 ### Hint 57.11, redeclared type 's'
-### Hint 62.64, repeated declaration of 'sel2'
-### Hint 62.77, repeated declaration of 'sel1'
-### Hint 64.65, repeated declaration of 'sel2'
-### Hint 64.78, repeated declaration of 'sel1'
+### Hint 62.11-62.70, repeated declaration of 'sel2' with type 'Data3 ->? Data2'
+### Hint 62.11-63.1, repeated declaration of 'sel1' with type 'Data3 ->? Data1'
+### Hint 64.11-64.71, repeated declaration of 'sel2' with type 'Data4 ->? Data2'
+### Hint 64.11-64.84, repeated declaration of 'sel1' with type 'Data4 ->? Data1'
 ### Hint 66.22, not a class 's'
 ### Hint 66.21, rebound variable 'x'
 ### Hint 66.25, no type found for 'e'

HasCASL/test/BoundedOrd.hascasl

@@ -39,3 +39,10 @@ type  instance Unit: Ord
 type  instance ?a: Ord
 vars  x, y: ?a
 . x <= y <=> def x() => x() <= y()
+
+class Cpo < Ord 
+var a : Cpo
+op    __<=__ : Pred (a * a)
+
+var x:?a
+. x <=[?a] x 

HasCASL/test/BoundedOrd.hascasl.output

@@ -22,8 +22,7 @@ vars  a : DiscreteOrd; x, y : a
 . x <= y <=> x = y;
 class Num
 vars  a : Ord; b : Num
-ops   min : a * a ->? a;
-      min : b * b ->? b
+op    min : a * a ->? a
 vars  a : Ord; b : Ord
 op    __<=__ : Pred ((a ->? b) * (a ->? b))
 type instance a ->? b : Ord
@@ -32,8 +31,14 @@ type instance Unit : Ord
 type instance ? a : Ord
 vars  x, y : ? a
 . x <= y <=> def x () => x () <= y ();
+class Cpo < Ord
+var   a : Cpo
+op    __<=__ : Pred (a * a)
+var   x : ? a
+. x <=[? a] x;
 %% Classes ---------------------------------------------------------------
 BoundedOrd < Ord
+Cpo < Ord
 DiscreteOrd < Ord
 Num < Type
 Ord < Type
@@ -42,12 +47,12 @@ Ord < Type
 __*__ : +Ord -> +Ord -> Ord
 __->?__ : -Ord -> +Ord -> Ord
 %% Type Variables --------------------------------------------------------
-a  : Ord %(var_164)%
+a  : Cpo %(var_205)%
 b  : Ord %(var_165)%
 %% Assumptions -----------------------------------------------------------
 __<=__ : forall a : Ord . Pred (a * a) %(op)%
 bot : forall b : BoundedOrd . b %(op)%
-min : forall b : Num . b * b ->? b %(op)%
+min : forall a : Ord . a * a ->? a %(op)%
 top : forall b : BoundedOrd . b %(op)%
 %% Variables -------------------------------------------------------------
 v : b
@@ -66,13 +71,14 @@ v <= top
 x <= y <=> x = y
 () <= ()
 x <= y <=> def x () => x () <= y ()
+x <= x
 %% Diagnostics -----------------------------------------------------------
 ### Hint 2.7, is type variable 'a'
 ### Hint 2.16, not a class 'a'
 ### Hint 8.7, is type variable 'a'
 ### Hint 8.7, rebound type variable 'a'
 ### Hint 8.15, is type variable 'b'
-### Hint 9.9, repeated declaration of '__<=__'
+### Hint 9.16-9.22, repeated declaration of '__<=__' with type 'Pred (a * a)'
 ### Hint 11.8, not a class 'a'
 ### Hint 11.7, rebound variable 'x'
 ### Hint 11.11, not a class 'a'
@@ -103,7 +109,9 @@ x <= y <=> def x () => x () <= y ()
   expected: {Ord}
      found: {Num}
 
-### Warning 30.7, overlapping declaration of 'min'
+*** Error 30.7, equal type schemes with uncomparable constraints of 'min'
+
+### Hint 30.12, uncomparable declaration of 'min' with type 'b * b ->? b'
 ### Hint 32.7, is type variable 'a'
 ### Hint 32.7, rebound type variable 'a'
 ### Hint 32.15, is type variable 'b'
@@ -129,3 +137,13 @@ x <= y <=> def x () => x () <= y ()
   typename 'a' (40.14)
   is not unifiable with type 'Unit ->? _v204' (41.32)
 
+### Hint 44.5, is type variable 'a'
+### Hint 44.5, rebound type variable 'a'
+### Hint 45.16-45.27, no kind found for 'a'
+  expected: {Ord}
+     found: {Type}
+
+### Hint 45.16-45.22, ignored specialized declaration of '__<=__' with type 'Pred (a * a)'
+### Hint 47.6, not a kind '? a'
+### Hint 47.5, rebound variable 'x'
+### Hint 48.7-48.10, is type list '[? a]'

HasCASL/test/Pair.hascasl.output

@@ -45,4 +45,4 @@ program (g : Pair _v25 _v27_b ->? _v25)
         ((op Pair : forall a : Type; b : Type . a * b -> Pair a b) (a, b))
         = a'
  are uninstantiated type variables '[_v25, _v27_b]'
-### Hint 8.9, repeated declaration of 'g'
+### Hint 6.8-6.15, repeated declaration of 'g' with type 'Pair a b ->? a'

HasCASL/test/PatternEq.hascasl.output

@@ -37,13 +37,13 @@ program (var b : s) : s = a %(pe_b)%
 program b = a %(pe_b)%
 c = (snd (x, y) as t) %(def_c)%
 %% Diagnostics -----------------------------------------------------------
-### Hint 3.9, repeated declaration of 'snd'
-### Hint 5.10, repeated declaration of 'snd'
-### Hint 6.10, repeated declaration of 'snd'
-### Hint 7.10, repeated declaration of 'snd'
-### Hint 10.9, repeated declaration of 'snd'
-### Hint 12.9, repeated declaration of 'snd'
+### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
+### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
+### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
+### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
+### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
+### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
 *** Error 14.11-14.18, illegal toplevel pattern '((var x : s), (var y : s))'
 ### Warning 17.10, illegal lhs pattern '(var b : s)'
-### Hint 18.4, repeated declaration of 'b'
-### Hint 19.9, repeated declaration of 'b'
+### Hint 18.8, repeated declaration of 'b' with type 's'
+### Hint 18.8, repeated declaration of 'b' with type 's'

HasCASL/test/PetriSystemCategory.hascasl.output

@@ -304,7 +304,7 @@ def (op __o__ : HomSys * HomSys ->? HomSys) (h2, h1)
 ### Hint 62.7, rebound type variable 'S'
 ### Hint 62.10, is type variable 'V'
 ### Hint 62.10, rebound type variable 'V'
-### Hint 67.10, repeated declaration of '__intersection__'
+### Hint 20.18-67.60, repeated declaration of '__intersection__' with type 'MultiSet Elem * MultiSet Elem -> MultiSet Elem'
 ### Hint 72.23, not a kind 'MultiSet P'
 ### Hint 73.26, not a kind 'MultiSet P'
 ### Hint 72.45, rejected 'Unit < Nat' of '((var p1 : MultiSet P),

HasCASL/test/Prelude.hascasl.output

@@ -219,9 +219,9 @@ free type bool ::= false | true %(ga_bool)%
 *** Error 31.6-31.12, illegal type pattern '__ * __ * __'
 ### Hint 40.7, not a class 's'
 ### Hint 42.16, rebound variable 'x'
-### Hint 42.9, repeated declaration of 'def'
+### Hint 39.14-39.19, repeated declaration of 'def' with type 'Pred s'
 ### Hint 44.15, rebound variable 'x'
-### Hint 44.9, repeated declaration of 'tt'
+### Hint 39.14-39.19, repeated declaration of 'tt' with type 'Pred s'
 *** Error 46.11, unexpected mixfix token: und
 ### Hint 50.8, redeclared type '__->__'
 ### Hint 52.8, redeclared type '__->__'
@@ -358,7 +358,7 @@ free type bool ::= false | true %(ga_bool)%
 *** Error 143.3-143.22, no typing for 'all \ x : p . bottom <<= x'
 ### Hint 148.6, is type variable 'f'
 ### Hint 150.15-150.17, is type list '[f]'
-### Hint 150.12, repeated declaration of '__<<=__'
+### Hint 119.16, repeated declaration of '__<<=__' with type 'c * c ->? Unit'
 ### Hint 153.5, is type variable 'c'
 ### Hint 153.5, rebound type variable 'c'
 ### Hint 153.8, is type variable 'd'
@@ -414,7 +414,7 @@ free type bool ::= false | true %(ga_bool)%
 ### Hint 186.16, rebound variable 'g'
 ### Hint 186.10, rebound variable 'f'
 ### Hint 186.16, rebound variable 'g'
-### Hint 186.12, repeated declaration of '__<<=__'
+### Hint 119.16, repeated declaration of '__<<=__' with type 'c * c ->? Unit'
 ### Hint 192.3, no type found for 'all'
 ### Hint 192.3, untypable term (with type: _v456 ->? Unit)
    'all'