hets/HasCASL/Merge.hs

	Merge.hs revision f42bcc750a9a02cb4f753b70679f9aacf1b338d7


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance{- |
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceModule      :  $Header$
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceDescription :  union of signature parts
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceCopyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceMaintainer  :  Christian.Maeder@dfki.de
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceStability   :  experimental
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancePortability :  portable
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
68ace74bf7cd65cb7eb7e19ffe373520fc520e0cFelix Gabriel Mancemerging parts of local environment
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance-}
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mancemodule HasCASL.Merge
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    ( merge
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    , mergeTypeDefn
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    , mergeOpInfo
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    , addUnit
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    ) where
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Common.Id
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Common.DocUtils
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Common.Result
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport HasCASL.As
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport HasCASL.Le
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport HasCASL.AsUtils
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport HasCASL.PrintLe
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport HasCASL.ClassAna
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport HasCASL.TypeAna
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport HasCASL.Builtin
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport HasCASL.MapTerm
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport qualified Data.Map as Map
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport qualified Data.Set as Set
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Control.Monad(foldM)
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Manceimport Data.List
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance
f6f50c832e59d06ae11bbfcf94d0df87313c844eFelix Gabriel MancemergeTypeInfo :: ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
f6f50c832e59d06ae11bbfcf94d0df87313c844eFelix Gabriel MancemergeTypeInfo cm t1 t2 = do
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    let o = keepMinKinds cm [otherTypeKinds t1, otherTypeKinds t2]
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        s = Set.union (superTypes t1) $ superTypes t2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    k <- minRawKind "type raw kind" (typeKind t1) $ typeKind t2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    return $ TypeInfo k o s d
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel MancemergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancemergeTypeDefn d1 d2 = case (d1, d2) of
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (_, DatatypeDefn _) -> return d2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (PreDatatype, _) -> fail "expected data type definition"
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (_, PreDatatype) -> return d1
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (NoTypeDefn, _) -> return d2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (_, NoTypeDefn) -> return d1
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (AliasTypeDefn s1, AliasTypeDefn s2) -> do
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        s <- mergeAlias s1 s2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        return $ AliasTypeDefn s
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (_, _) -> mergeA "TypeDefn" d1 d2
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel MancemergeAlias :: Type -> Type -> Result Type
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel MancemergeAlias s1 s2 = if eqStrippedType s1 s2 then return s1 else
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    fail $ "wrong type" ++ expected s1 s2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancemergeOpBrand :: OpBrand -> OpBrand -> OpBrand
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancemergeOpBrand b1 b2 = case (b1, b2) of
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (Pred, _) -> Pred
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (_, Pred) -> Pred
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (Op, _) -> Op
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (_, Op) -> Op
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    _ -> Fun
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancemergeOpDefn :: OpDefn -> OpDefn -> Result OpDefn
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel MancemergeOpDefn d1 d2 = case (d1, d2) of
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (NoOpDefn b1, NoOpDefn b2) -> do
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        let b = mergeOpBrand b1 b2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        return $ NoOpDefn b
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (SelectData c1 s, SelectData c2 _) -> do
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        let c = Set.union c1 c2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        return $ SelectData c s
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (Definition b1 e1, Definition b2 e2) -> do
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        d <- mergeTerm Hint e1 e2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        let b = mergeOpBrand b1 b2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        return $ Definition b d
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (NoOpDefn b1, Definition b2 e2) -> do
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        let b = mergeOpBrand b1 b2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        return $ Definition b e2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (Definition b1 e1, NoOpDefn b2) -> do
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        let b = mergeOpBrand b1 b2
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder        return $ Definition b e1
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (ConstructData _, SelectData _ _) ->
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        fail "illegal selector as constructor redefinition"
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (SelectData _ _, ConstructData _) ->
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance        fail "illegal constructor as selector redefinition"
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (ConstructData _, _) -> return d1
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (_, ConstructData _) -> return d2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (SelectData _ _, _) -> return d1
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance    (_, SelectData _ _) -> return d2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceaddUnit :: ClassMap -> TypeMap -> TypeMap
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceaddUnit cm = maybe (error "addUnit") id . maybeResult . mergeTypeMap cm bTypes
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancemergeOpInfos :: Set.Set OpInfo -> Set.Set OpInfo -> Result (Set.Set OpInfo)
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel MancemergeOpInfos s1 s2 = if Set.null s1 then return s2 else do
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance    let (o, os) = Set.deleteFindMin s1
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance        (es, us) = Set.partition ((opType o ==) . opType) s2
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance    s <- mergeOpInfos os us
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance    r <- foldM mergeOpInfo o $ Set.toList es
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance    return $ Set.insert r s
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel MancemergeOpInfo :: OpInfo -> OpInfo -> Result OpInfo
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel MancemergeOpInfo o1 o2 = do
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance    let as = Set.union (opAttrs o1) $ opAttrs o2
    d <- mergeOpDefn (opDefn o1) $ opDefn o2
    return $ OpInfo (opType o1) as d

mergeTypeMap :: ClassMap -> TypeMap -> TypeMap -> Result TypeMap
mergeTypeMap cm = mergeMap $ mergeTypeInfo cm

merge :: Env -> Env -> Result Env
merge e1 e2 = do
    cMap <- mergeMap mergeClassInfo (classMap e1) $ classMap e2
    let clMap = Map.map (\ ci -> ci { classKinds =
                          keepMinKinds cMap [classKinds ci] }) cMap
    tMap <- mergeTypeMap clMap (typeMap e1) $ typeMap e2
    let tAs = filterAliases tMap
    as <- mergeMap mergeOpInfos (assumps e1) $ assumps e2
    bs <- mergeMap (\ i1 i2 -> if i1 == i2 then return i1 else
                    fail "conflicting operation for binder syntax")
         (binders e1) $ binders e2
    return initialEnv
      { classMap = clMap
      , typeMap = tMap
      , assumps = Map.map (Set.map $ mapOpInfo (id, expandAliases tAs)) $ as
      , binders = bs }

mergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
mergeA str t1 t2 = if t1 == t2 then return t1 else
    fail ("different " ++ str ++ expected t1 t2)

mergeTerm :: DiagKind -> Term -> Term -> Result Term
mergeTerm k t1 t2 = if t1 == t2 then return t1 else
  Result [Diag k ("different terms" ++ expected t1 t2) $ getRange t2] $ Just t2