Cross Reference: /hets/HasCASL/DataAna.hs
DataAna.hs revision 3f69b6948966979163bdfe8331c38833d5d90ecd
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz{- |
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzModule : $Header$
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzMaintainer : Christian.Maeder@dfki.de
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzStability : provisional
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzPortability : portable
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzanalyse alternatives of data types
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-}
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzmodule HasCASL.DataAna where
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Data.Maybe
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport qualified Data.Map as Map
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport qualified Data.Set as Set
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Id
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Result
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.AS_Annotation
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.As
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.Le
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.TypeAna
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.AsUtils
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.Builtin
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.Unify
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-- | description of polymorphic data types
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzdata DataPat = DataPat Id [TypeArg] RawKind Type
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-- * creating selector equations
fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavumkSelId :: Range -> String -> Int -> Int -> Id
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavumkSelId p str n m = mkId
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu [Token (str ++ "_" ++ show n ++ "_" ++ show m) p]
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavumkSelVar :: Int -> Int -> Type -> VarDecl
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumkSelVar n m ty = VarDecl (mkSelId (getRange ty) "x" n m) ty Other nullRange
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu
239330cd665aac95fcf9cf95449594c96667cbc2Robert SavugenTuple :: Int -> Int -> [Selector] -> [VarDecl]
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavugenTuple _ _ [] = []
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavugenTuple n m (Select _ ty _ : sels) =
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu mkSelVar n m ty : genTuple n (m + 1) sels
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavugenSelVars :: Int -> [[Selector]] -> [[VarDecl]]
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavugenSelVars _ [] = []
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavugenSelVars n (ts:sels) =
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu genTuple n 1 ts : genSelVars (n + 1) sels
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumakeSelTupleEqs :: DataPat -> Term -> Int -> Int -> [Selector] -> [Named Term]
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavumakeSelTupleEqs dt@(DataPat _ tArgs _ rt) ct n m (Select mi ty p : sels) =
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu let sc = TypeScheme tArgs (getSelType rt p ty) nullRange in
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (case mi of
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Just i -> let
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu vt = QualVar $ mkSelVar n m ty
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu eq = mkEqTerm eqId nullRange
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (mkApplTerm (mkOpTerm i sc) [ct]) vt
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu in [makeNamed ("ga_select_" ++ show i) eq]
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu _ -> [])
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ++ makeSelTupleEqs dt ct n (m + 1) sels
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumakeSelTupleEqs _ _ _ _ [] = []
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavumakeSelEqs :: DataPat -> Term -> Int -> [[Selector]] -> [Named Term]
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumakeSelEqs dt ct n (sel:sels) =
3051a3502f027f3d7bb750a1d7a6b1b43cdd2a86Robert Savu makeSelTupleEqs dt ct n 1 sel
3051a3502f027f3d7bb750a1d7a6b1b43cdd2a86Robert Savu ++ makeSelEqs dt ct (n + 1) sels
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumakeSelEqs _ _ _ _ = []
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumakeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumakeAltSelEqs dt@(DataPat _ args _ rt) (Construct mc ts p sels) =
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu case mc of
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Nothing -> []
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Just c -> let sc = TypeScheme args (getFunType rt p ts) nullRange
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu newSc = sc
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu vars = genSelVars 1 sels
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ars = map ( \ vs -> mkTupleTerm (map QualVar vs) nullRange)
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu vars
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ct = mkApplTerm (mkOpTerm c newSc) ars
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu in map (mapNamed (mkForall (map GenTypeVarDecl args
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ++ map GenVarDecl (concat vars))))
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu $ makeSelEqs dt ct 1 sels
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumakeDataSelEqs :: DataEntry -> Type -> [Named Sentence]
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavumakeDataSelEqs (DataEntry _ i _ args rk alts) rt =
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu map (mapNamed Formula) $
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu concatMap (makeAltSelEqs $ DataPat i args rk rt) alts
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- * analysis of alternatives
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
69b1e90bbb27ce2dd365628c07c0f03a3ae97b26Robert SavuanaAlts :: [DataPat] -> DataPat -> [Alternative] -> TypeEnv -> Result [AltDefn]
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuanaAlts tys dt alts te =
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu do l <- mapM (anaAlt tys dt te) alts
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Result (checkUniqueness $ catMaybes $
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu map ( \ (Construct i _ _ _) -> i) l) $ Just ()
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu return l
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
69b1e90bbb27ce2dd365628c07c0f03a3ae97b26Robert SavuanaAlt :: [DataPat] -> DataPat -> TypeEnv -> Alternative
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu -> Result AltDefn
239330cd665aac95fcf9cf95449594c96667cbc2Robert SavuanaAlt _ _ te (Subtype ts _) =
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu do l <- mapM ( \ t -> anaStarTypeM t te) ts
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu return $ Construct Nothing (map snd l) Partial []
239330cd665aac95fcf9cf95449594c96667cbc2Robert SavuanaAlt tys dt te (Constructor i cs p _) =
239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu do newCs <- mapM (anaComps tys dt te) cs
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu let sels = map snd newCs
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Result (checkUniqueness $ catMaybes $
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu map ( \ (Select s _ _) -> s ) $ concat sels) $ Just ()
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu return $ Construct (Just i) (map fst newCs) p sels
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuanaComps :: [DataPat] -> DataPat -> TypeEnv -> [Component]
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz -> Result (Type, [Selector])
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuanaComps tys rt te cs =
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz do newCs <- mapM (anaComp tys rt te) cs
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz return (mkProductType $ map fst newCs, map snd newCs)
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst SchulzanaComp :: [DataPat] -> DataPat -> TypeEnv -> Component
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz -> Result (Type, Selector)
anaComp tys rt te (Selector s p t _ _) =
do ct <- anaCompType tys rt t te
return (ct, Select (Just s) ct p)
anaComp tys rt te (NoSelector t) =
do ct <- anaCompType tys rt t te
return (ct, Select Nothing ct Partial)
anaCompType :: [DataPat] -> DataPat -> Type -> TypeEnv -> Result Type
anaCompType tys (DataPat _ tArgs _ _) t te = do
(_, ct) <- anaStarTypeM t te
let ds = unboundTypevars True tArgs ct
if null ds then return () else Result ds Nothing
mapM (checkMonomorphRecursion ct te) tys
return $ generalize tArgs ct
checkMonomorphRecursion :: Type -> TypeEnv -> DataPat -> Result ()
checkMonomorphRecursion t te (DataPat i _ _ rt) =
case filter (\ ty -> not (lesserType te ty rt || lesserType te rt ty))
$ findSubTypes (typeMap te) i t of
[] -> return ()
ty : _ -> Result [Diag Error ("illegal polymorphic recursion"
++ expected rt ty) $ getRange ty] Nothing
findSubTypes :: TypeMap -> TypeId -> Type -> [Type]
findSubTypes tm i t = case getTypeAppl t of
(TypeName j _ _, args) -> if relatedTypeIds tm i j then [t]
else concatMap (findSubTypes tm i) args
(topTy, args) -> concatMap (findSubTypes tm i) $ topTy : args
relatedTypeIds :: TypeMap -> TypeId -> TypeId -> Bool
relatedTypeIds tm i1 i2 =
not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
allRelIds :: TypeMap -> TypeId -> Set.Set TypeId
allRelIds tm i = Set.union (superIds tm i) $ subIds tm i
subIds :: TypeMap -> Id -> Set.Set Id
subIds tm i = foldr ( \ j s ->
if Set.member i $ superIds tm j then
Set.insert j s else s) Set.empty $ Map.keys tm