AsToLe.hs revision b56389e736838ac2fe7b105a8a2d0963a2374e99
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
$Id$
Authors: Christian Maeder
Year: 2002
-}
module HasCASL.AsToLe where
import Common.AS_Annotation
import HasCASL.As
import HasCASL.ClassAna
import HasCASL.ClassDecl
import Common.Id
import qualified Common.Lib.Set as Set
import HasCASL.Le
import Common.Lexer
import Data.Maybe
import Control.Monad
import Common.Lib.State
import HasCASL.OpDecl
import Common.Result
import Common.PrettyPrint
import HasCASL.PrintAs
import HasCASL.TypeDecl
import HasCASL.MixAna
import HasCASL.Reader
----------------------------------------------------------------------------
-- analysis
-----------------------------------------------------------------------------
logicalType :: Type
logicalType = TypeName (simpleIdToId (mkSimpleId "logical")) star 0
missingAna :: PrettyPrint a => a -> [Pos] -> State Env ()
missingAna t ps = appendDiags [Diag FatalError
("no analysis yet for: " ++ showPretty t "")
$ if null ps then nullPos else head ps]
anaBasicSpec :: BasicSpec -> State Env ()
anaBasicSpec (BasicSpec l) = mapM_ anaBasicItem $ map item l
anaBasicItem :: BasicItem -> State Env ()
anaBasicItem (SigItems i) = anaSigItems Loose i
anaBasicItem (ClassItems inst l _) = mapM_ (anaAnnotedClassItem inst) l
anaBasicItem (GenVarItems l _) = mapM_ anaGenVarDecl l
anaBasicItem t@(ProgItems _ p) = missingAna t p
anaBasicItem (FreeDatatype l _) = mapM_ (anaDatatype Free Plain) $ map item l
anaBasicItem (GenItems l _) = mapM_ (anaSigItems Generated) $ map item l
anaBasicItem (AxiomItems decls fs _) =
do tm <- gets typeMap -- save type map
as <- gets assumps -- save vars
mapM_ anaGenVarDecl decls
ds <- mapM (( \ (TermFormula t) -> resolveTermWithType
(Just logicalType) t ) . item) fs
appendDiags $ concatMap diags ds
putTypeMap tm -- restore
putAssumps as -- restore
-- store the formulae
anaSigItems :: GenKind -> SigItems -> State Env ()
anaSigItems gk (TypeItems inst l _) = mapM_ (anaTypeItem gk inst) $ map item l
anaSigItems _ (OpItems l _) = mapM_ anaOpItem $ map item l
anaSigItems _ l@(PredItems _ p) = missingAna l p
----------------------------------------------------------------------------
-- GenVarDecl
-----------------------------------------------------------------------------
anaGenVarDecl :: GenVarDecl -> State Env ()
anaGenVarDecl(GenVarDecl v) = optAnaVarDecl v
anaGenVarDecl(GenTypeVarDecl t) = anaTypeVarDecl t
convertTypeToClass :: Type -> ReadR ClassMap Class
convertTypeToClass (TypeToken t) =
if tokStr t == "Type" then return universe else do
let ci = simpleIdToId t
mapReadR ( \ (Result _ m) ->
case m of
Just _ -> Result [] (Just $ Intersection
(Set.single ci) [])
Nothing -> Result
[mkDiag Hint "not a class" ci] Nothing )
$ anaClassId ci
convertTypeToClass (BracketType Parens ts ps) =
do cs <- mapM convertTypeToClass ts
return $ Intersection (Set.unions $ map iclass cs) ps
convertTypeToClass t = lift $ Result [mkDiag Hint "not a class" t] Nothing
convertTypeToKind :: Type -> ReadR ClassMap Kind
convertTypeToKind (FunType t1 FunArr t2 ps) =
do k1 <- convertTypeToKind t1
k2 <- convertTypeToKind t2
return $ KindAppl k1 k2 ps
convertTypeToKind (BracketType Parens [t] _) =
do k <- convertTypeToKind t
return $ k
convertTypeToKind (MixfixType [t1, TypeToken t]) =
let s = tokStr t
v = case s of
"+" -> CoVar
"-" -> ContraVar
_ -> InVar
in case v of
InVar -> lift $ Result [] Nothing
_ -> do k1 <- convertTypeToClass t1
return $ ExtClass k1 v [tokPos t]
convertTypeToKind t =
do c <- convertTypeToClass t
return $ ExtClass c InVar []
optAnaVarDecl, anaVarDecl :: VarDecl -> State Env ()
optAnaVarDecl vd@(VarDecl v t s q) =
if isSimpleId v then
do mc <- toMaybeState classMap $ convertTypeToKind t
case mc of
Just c -> anaTypeVarDecl(TypeArg v c s q)
Nothing -> anaVarDecl vd
else anaVarDecl vd
anaVarDecl(VarDecl v oldT _ _) =
do (k, t) <- anaTypeS (star, oldT)
checkKindsS v star k
addOpId v (simpleTypeScheme t) [] VarDefn
-- ----------------------------------------------------------------------------
-- ClassItem
-- ----------------------------------------------------------------------------
anaAnnotedClassItem :: Instance -> Annoted ClassItem -> State Env ()
anaAnnotedClassItem _ aci =
let ClassItem d l _ = item aci in
do anaClassDecls d
mapM_ anaBasicItem $ map item l