- Timestamp:
- 24.09.2003 21:00:02 (6 years ago)
- Location:
- branches/raw-kinds/HasCASL
- Files:
-
- 11 modified
-
As.hs (modified) (4 diffs)
-
AsToLe.hs (modified) (3 diffs)
-
ClassAna.hs (modified) (2 diffs)
-
ClassDecl.hs (modified) (4 diffs)
-
DataAna.hs (modified) (1 diff)
-
Merge.hs (modified) (2 diffs)
-
PrintAs.hs (modified) (1 diff)
-
TypeAna.hs (modified) (8 diffs)
-
TypeCheck.hs (modified) (1 diff)
-
TypeDecl.hs (modified) (3 diffs)
-
VarDecl.hs (modified) (7 diffs)
Legend:
- Unmodified
- Added
- Removed
-
branches/raw-kinds/HasCASL/As.hs
r1701 r1722 18 18 19 19 import Common.Id 20 import Common.Keywords 20 21 import Common.AS_Annotation 22 import HasCASL.HToken 21 23 22 24 data BasicSpec = BasicSpec [Annoted BasicItem] … … 64 66 data Kind = Universe [Pos] 65 67 | MissingKind 66 | Downset (Maybe Token) Type RawKind [Pos]67 | ClassKind ClassId RawKind68 | Downset (Maybe Token) Type Kind [Pos] 69 | ClassKind ClassId Kind 68 70 | Intersection [Kind] [Pos] 69 71 | FunKind ExtKind Kind [Pos] … … 74 76 type RawKind = Kind 75 77 76 star ::Kind78 star, starPlus, funKind, prodKind :: RawKind 77 79 star = Universe [] 80 81 starPlus = ExtKind star CoVar [] 82 83 funKind = FunKind (ExtKind star ContraVar []) 84 (FunKind starPlus star []) [] 85 prodKind = FunKind starPlus (FunKind starPlus star []) [] 78 86 79 87 data TypeItem = TypeDecl [TypePattern] Kind [Pos] … … 119 127 120 128 data Arrow = FunArr| PFunArr | ContFunArr | PContFunArr 121 deriving (Show, Eq, Ord) 129 deriving (Eq, Ord) 130 131 instance Show Arrow where 132 show FunArr = funS 133 show PFunArr = pFun 134 show ContFunArr = contFun 135 show PContFunArr = pContFun 136 137 arrowId :: Arrow -> Id 138 arrowId a = Id (map mkSimpleId [place, show a, place]) [] [] 139 140 productId :: Id 141 productId = Id (map mkSimpleId [place, timesS, place]) [] [] 122 142 123 143 data Pred = IsIn ClassId [Type] -
branches/raw-kinds/HasCASL/AsToLe.hs
r1673 r1722 17 17 import Common.Lib.State 18 18 import qualified Common.Lib.Map as Map 19 import qualified Common.Lib.Set as Set20 19 import Common.Named 21 20 import Common.Result … … 28 27 import HasCASL.TypeCheck 29 28 import Data.Maybe 29 import Data.List 30 30 31 31 -- | basic analysis … … 49 49 diffClass :: ClassInfo -> ClassInfo -> Maybe ClassInfo 50 50 diffClass c1 c2 = 51 let diff = Set.difference (superClasses c1) (superClasses c2)52 in if Set.isEmptydiff51 let diff = classKinds c1 \\ classKinds c2 52 in if null diff 53 53 then Nothing 54 else Just c1 { superClasses = diff }54 else Just c1 { classKinds = diff } 55 55 56 56 -- | compute difference of type infos -
branches/raw-kinds/HasCASL/ClassAna.hs
r1701 r1722 39 39 case c of 40 40 Universe _ -> c 41 MissingKind -> error "rawKind "41 MissingKind -> error "rawKind1" 42 42 ClassKind _ rk -> rawKind rk 43 43 Downset _ _ rk _ -> rawKind rk 44 Intersection l _ -> 45 foldl1 ( \ k1 k2 -> 46 fromJust $ minKind True k1 k2) $ map rawKind l 44 Intersection l _ -> if null l then error "rawKind2" 45 else rawKind $ head l 47 46 FunKind e k ps -> FunKind (rawKind e) (rawKind k) ps 48 47 ExtKind k v ps -> ExtKind (rawKind k) v ps 49 50 51 48 52 49 checkIntersection :: RawKind -> [Kind] -> [Diagnosis] 53 50 checkIntersection _ [] = [] 54 51 checkIntersection k (f:r) = 55 let m = minKind True k (rawKind f) in 56 case m of 57 Nothing -> 52 case k == rawKind f of 53 False -> 58 54 Diag Error ("incompatible kind of: " ++ showPretty f "" 59 55 ++ "\n for raw kind: " ++ showPretty k "") 60 56 (posOf [f]) : checkIntersection k r 61 Just n -> checkIntersection nr57 True -> checkIntersection k r 62 58 63 eqRawKindDiag :: (PosItem a, PrettyPrint a) =>59 diffKindDiag :: (PosItem a, PrettyPrint a) => 64 60 a -> RawKind -> RawKind -> [Diagnosis] 65 eqRawKindDiag a k1 k2 = 66 if k1 == k2 then [] 67 else [ Diag Error 61 diffKindDiag a k1 k2 = 62 [ Diag Error 68 63 ("incompatible kind of: " ++ showPretty a "" ++ expected k1 k2) 69 64 $ posOf [a] ] … … 104 99 do let k3 = rawKind k1 105 100 k4 = rawKind k2 106 addDiags (eqRawKindDiag p k3 k4) 101 if k3 == k4 then return () 102 else addDiags $ diffKindDiag p k1 k2 -
branches/raw-kinds/HasCASL/ClassDecl.hs
r1673 r1722 15 15 import HasCASL.As 16 16 import qualified Common.Lib.Map as Map 17 import qualified Common.Lib.Set as Set18 17 import Common.Id 19 18 import HasCASL.Le … … 24 23 import HasCASL.ClassAna 25 24 import HasCASL.TypeAna 26 import HasCASL.Merge27 25 28 26 -- --------------------------------------------------------------------------- … … 33 31 anaClassDecls (ClassDecl cls k ps) = 34 32 do ak <- anaKind k 35 mapM_ (addClassDecl ak Set.empty Nothing) cls33 mapM_ (addClassDecl ak) cls 36 34 return $ ClassDecl cls ak ps 37 38 anaClassDecls (SubclassDecl _ _ (Downset _) _) = error "anaClassDecl"39 anaClassDecls (SubclassDecl cls k sc@(Intersection supcls ps) qs) =40 do ak <- anaKind k41 if Set.isEmpty supcls then42 do addDiags [Diag Warning43 "redundant universe class"44 $ headPos (ps ++ qs)]45 mapM_ (addClassDecl ak supcls Nothing) cls46 return $ SubclassDecl cls ak sc qs47 else let (hd, tl) = Set.deleteFindMin supcls in48 if Set.isEmpty tl then49 do e <- get50 mk <- anaClassId hd51 case mk of52 Nothing -> do53 put e54 addClassDecl ak tl Nothing hd55 addDiags [mkDiag Warning56 "implicit declaration of superclass" hd]57 Just sk -> checkKinds hd sk ak58 mapM_ (addClassDecl ak (Set.single hd) Nothing) cls59 return $ SubclassDecl cls ak sc qs60 else do (sk, newSc@(Intersection newSups _)) <- anaClass sc61 checkKinds hd sk ak62 mapM_ (addClassDecl ak newSups Nothing) cls63 return $ SubclassDecl cls ak newSc qs64 65 66 anaClassDecls (ClassDefn ci k ic ps) =67 do ak <- anaKind k68 (dk, newIc) <- anaClass ic69 checkKinds ci dk ak70 (newKind, _, mDefn) <- addClassDecl ak Set.empty (Just newIc) ci71 return $ case mDefn of72 Nothing -> ClassDecl [ci] newKind ps73 Just newDefn -> ClassDefn ci newKind newDefn ps74 75 anaClassDecls (DownsetDefn ci v t ps) =76 do mt <- anaStarType t77 (newKind, _, mDefn) <- addClassDecl star Set.empty (fmap Downset mt) ci78 return $ case mDefn of79 Nothing -> ClassDecl [ci] newKind ps80 Just newDefn -> case newDefn of81 Downset newT -> DownsetDefn ci v newT ps82 _ -> ClassDefn ci newKind newDefn ps83 35 84 36 -- --------------------------------------------------------------------------- … … 91 43 92 44 -- | store a class 93 addClassDecl :: Kind -> Set.Set ClassId -> Maybe Class94 -> ClassId -> State Env (Kind, Set.Set ClassId, Maybe Class)45 addClassDecl :: Kind -> ClassId 46 -> State Env () 95 47 -- check with merge 96 addClassDecl kind sups defnci =48 addClassDecl kind ci = 97 49 if showId ci "" == "Type" then 98 50 do addDiags [mkDiag Error 99 51 "illegal universe class declaration" ci] 100 return (kind, Set.empty, Nothing)101 52 else do 102 53 cMap <- gets classMap 103 54 case Map.lookup ci cMap of 104 55 Nothing -> do putClassMap $ Map.insert ci 105 newClassInfo { classKind = kind 106 , superClasses = sups 107 , classDefn = defn } cMap 108 return (kind, sups, defn) 56 ClassInfo { classKinds = [kind] } cMap 109 57 Just info -> do 110 addDiags [mkDiag Warning "redeclared class" ci] 111 let oldDefn = classDefn info 112 oldSups = superClasses info 113 oldKind = classKind info 114 (ds, newDefn) = case (oldDefn, defn) of 115 (Nothing, Nothing) -> ([], Nothing) 116 (Just _, Nothing) -> 117 ([mkDiag Error 118 "alias class cannot become a real class" ci] 119 , oldDefn) 120 (Nothing, Just _) -> 121 ([mkDiag Error 122 "class cannot become an alias class" ci] 123 , Nothing) 124 (Just d1, Just d2) -> 125 let Result es _ = merge d1 d2 in 126 (map (improveDiag ci) es, oldDefn) 127 checkKinds ci kind oldKind 128 addDiags ds 129 possSups <- getLegalSuperClasses ci oldSups sups 130 let newSups = case newDefn of Just _ -> Set.empty 131 Nothing -> possSups 132 putClassMap $ Map.insert ci info 133 { superClasses = newSups 134 , classDefn = newDefn } cMap 135 return (oldKind, newSups, newDefn) 58 let superClasses = classKinds info 59 checkKinds ci kind $ head superClasses 60 if kind `elem` superClasses then 61 addDiags [mkDiag Warning "redeclared class" ci] 62 else putClassMap $ Map.insert ci info 63 { classKinds = kind:superClasses } cMap 136 64 137 getLegalSuperClasses :: ClassId -> Set.Set ClassId 138 -> Set.Set ClassId -> State Env (Set.Set ClassId) 139 getLegalSuperClasses ci oldCs ses = 140 do ce <- gets classMap 141 let cs = Set.toList ses 142 scs = zip (map (allSuperClasses ce) cs) cs 143 (scycs, sOk) = partition ((ci `Set.member`) . fst) scs 144 defCs = map snd sOk 145 newCs = Set.fromList defCs `Set.union` oldCs 146 cycles = map snd scycs 147 dubs = filter (`Set.member` allSuperClasses ce ci) defCs 148 myDiag k s l = Diag k (s ++ " '" ++ showClassList l "'") 149 $ posOfId $ head l 150 in do if null cycles then return () 151 else addDiags [myDiag Error 152 "cyclic class relation via" cycles] 153 if null dubs then return () 154 else addDiags [myDiag Warning 155 "already known as super class" dubs] 156 return newCs 65 -- cycle check missing 157 66 158 67 showClassList :: [ClassId] -> ShowS 159 68 showClassList is = showParen (not $ isSingle is) 160 69 $ showSepList ("," ++) showId is 161 162 -- check with merge163 mergeDefns :: ClassId -> Class -> Class -> [Diagnosis]164 165 mergeDefns ci (Downset oldT) (Downset t) =166 if oldT == t then [] else wrongClassDecl ci167 168 mergeDefns ci (Intersection oldIs _) (Intersection is _) =169 if oldIs == is then []170 else wrongClassDecl ci171 172 mergeDefns ci _ _ = wrongClassDecl ci173 70 174 71 wrongClassDecl :: ClassId -> [Diagnosis] -
branches/raw-kinds/HasCASL/DataAna.hs
r1673 r1722 19 19 import Common.Result 20 20 import HasCASL.Le 21 import HasCASL.ClassAna22 21 import HasCASL.TypeAna 23 22 import Data.Maybe -
branches/raw-kinds/HasCASL/Merge.hs
r1673 r1722 71 71 72 72 instance Mergeable ClassInfo where 73 merge c1 c2 = do k <- merge (classKind c1) (classKind c2) 74 d <- merge (classDefn c1) (classDefn c2) 75 let s1 = superClasses c1 76 s2 = superClasses c2 77 if s1 == s2 then 78 return $ ClassInfo s1 k d 73 merge c1 c2 = if c1 == c2 then 74 return c1 79 75 else fail "merge: non-equal super classes" 80 76 … … 82 78 merge k1 k2 = if k1 == k2 then return k1 83 79 else fail "merge: non-equal kinds" 84 85 instance Mergeable Class where86 merge c1@(Downset t1) (Downset t2) =87 if t1 == t2 then return c188 else fail "inconsistent downset"89 merge c1@(Intersection i1 _) (Intersection i2 _) =90 if i1 == i2 then return c191 else fail "inconsistent intersection class"92 merge _ _ = fail "inconsistent class redefinition"93 80 94 81 mergeList :: Eq a => [a] -> [a] -> Result [a] -
branches/raw-kinds/HasCASL/PrintAs.hs
r1701 r1722 138 138 139 139 instance PrettyPrint Arrow where 140 printText0 _ FunArr = text funS 141 printText0 _ PFunArr = text pFun 142 printText0 _ ContFunArr = text contFun 143 printText0 _ PContFunArr = text pContFun 144 140 printText0 _ a = text $ show a 145 141 146 142 instance PrettyPrint Quantifier where -
branches/raw-kinds/HasCASL/TypeAna.hs
r1716 r1722 24 24 import Common.Result 25 25 import Common.Lib.State 26 import Common.PrettyPrint 26 27 27 28 -- -------------------------------------------------------------------------- … … 29 30 -- -------------------------------------------------------------------------- 30 31 31 anaKind :: Kind -> State Env (Maybe Kind) 32 anaKind k = 32 toKind :: Maybe Kind -> Kind 33 toKind mk = case mk of Nothing -> star 34 Just k -> k 35 36 anaKind :: Kind -> State Env Kind 37 anaKind k = fmap toKind (anaKindM k) 38 39 anaKindM :: Kind -> State Env (Maybe Kind) 40 anaKindM k = 33 41 case k of 34 42 Universe _ -> return (Just k) … … 40 48 Downset v newT rk ps 41 49 ClassKind ci _ -> anaClassId ci 42 Intersection ks ps -> do mks <- mapM anaKind ks50 Intersection ks ps -> do mks <- mapM anaKindM ks 43 51 let newKs = catMaybes mks 44 52 if null newKs then return Nothing … … 50 58 else do addDiags ds 51 59 return Nothing 52 FunKind k1 k2 ps -> do m1 <- anaKind k153 m2 <- anaKind k260 FunKind k1 k2 ps -> do m1 <- anaKindM k1 61 m2 <- anaKindM k2 54 62 return $ do k3 <- m1 55 63 k4 <- m2 56 64 return $ FunKind k3 k4 ps 57 ExtKind ek v ps -> do m <- anaKind ek65 ExtKind ek v ps -> do m <- anaKindM ek 58 66 return $ do nk <- m 59 67 return $ ExtKind nk v ps … … 197 205 case j of 198 206 ExtKind ek _ _ -> checkTypeRawKind t ek 199 _ -> do k <- inferRawKind t 200 addDiags (eqRawKindDiag t j k)207 _ -> do k <- inferRawKind t 208 if k == j then return () else addDiags $ diffKindDiag t j k 201 209 202 210 getIdRawKind :: Id -> State Env Kind … … 213 221 case Map.lookup i tk of 214 222 Nothing -> Nothing 215 Just (TypeInfo k l_ _) -> Just k223 Just (TypeInfo k _ _ _) -> Just k 216 224 217 225 -- --------------------------------------------------------------------------- … … 219 227 -- --------------------------------------------------------------------------- 220 228 221 inferKind :: Type -> State Env (Maybe Kind) 222 inferKind (TypeName i _ _) = getIdKind i 223 {- 224 inferKind (TypeAppl t1 t2) = 225 do mk1 <- inferKind t1 229 checkMaybeKinds :: (PosItem a, PrettyPrint a) => 230 a -> Maybe Kind -> Maybe Kind -> State Env (Maybe Kind) 231 checkMaybeKinds a mk1 mk2 = 232 case mk1 of 233 Nothing -> return mk2 234 Just k1 -> case mk2 of 235 Nothing -> return mk1 236 Just k2 -> 237 if lesserKind k1 k2 then return mk1 238 else if lesserKind k2 k1 then return mk2 239 else do addDiags $ diffKindDiag a k1 k2 240 return Nothing 241 242 checkFunKind :: Maybe Kind -> Type -> Type -> Kind -> State Env (Maybe Kind) 243 checkFunKind mk t1 t2 k1 = 244 case k1 of 245 FunKind fk ak _ -> do 246 mk2 <- inferKind (Just fk) t2 247 case mk2 of 248 Nothing -> return mk 249 Just _ -> checkMaybeKinds (TypeAppl t1 t2) mk (Just ak) 250 Intersection l ps -> do 251 ml <- mapM (checkFunKind mk t1 t2) l 252 let ks = catMaybes ml 253 return $ if null ks then Nothing else if isSingle ks then 254 Just $ head ks else Just $ Intersection ks ps 255 ClassKind _ k -> checkFunKind mk t1 t2 k 256 Downset _ _ k _ -> checkFunKind mk t1 t2 k 257 ExtKind k _ _ -> checkFunKind mk t1 t2 k 258 _ -> do addDiags [mkDiag Error 259 "expected higher order kind for type" t1] 260 return Nothing 261 262 inferKind :: Maybe Kind -> Type -> State Env (Maybe Kind) 263 inferKind mk (TypeName i _ _) = 264 do m <- getIdKind i 265 checkMaybeKinds i mk m 266 267 inferKind mk (TypeAppl t1 t2) = 268 do mk1 <- inferKind Nothing t1 226 269 case mk1 of 227 228 FunKind _ _ _ -> checkTypeKind t2 k1 229 Intersection 230 231 if ak lesserKind k1 then Just k2 232 else Nothing 233 Intersection ks _ -> 234 235 236 let l = concatMap ( \ fk -> 237 catMaybes ( \ ak -> 238 case fk of 239 FunKind k1 k2 _ -> if ak lesserKind k1 then Just k2 240 else Nothing 241 Intersection ks _ -> 242 243 244 do checkTypeKind t2 k1 245 return k2 246 _ -> do addDiags [mkDiag Error 247 "incompatible kind of type" t1] 248 return mk1 249 inferKind b (FunType t1 _ t2 _) = 250 do checkTypeKind t1 star 251 checkTypeKind t2 star 252 return star 253 inferKind b (ProductType ts _) = 254 do mapM_ ( \ t -> checkTypeKind t star) ts 255 return star 256 inferKind b (LazyType t _) = 257 do checkTypeKind t star 258 return star 259 inferKind b (TypeToken t) = getIdKind $ simpleIdToId t 260 inferKind b (KindedType t k _) = 261 do checkTypeKind t k 262 return k 263 inferKind b t = 270 Nothing -> return mk 271 Just k1 -> checkFunKind mk t1 t2 k1 272 273 inferKind mk (FunType t1 a t2 _) = 274 do let i = arrowId a 275 mfk <- getIdKind i 276 let fk = case mfk of Nothing -> funKind 277 Just k -> k 278 tn = TypeName i fk 0 279 inferKind mk (TypeAppl (TypeAppl tn t1) t2) 280 281 inferKind mk t@(ProductType ts _) = 282 if null ts then checkMaybeKinds t mk (Just star) 283 else do mpk <- getIdKind productId 284 let pk = case mpk of Nothing -> prodKind 285 Just k -> k 286 tn = TypeName productId pk 0 287 mkAppl [t1] = t1 288 mkAppl (t1:tr) = TypeAppl (TypeAppl tn t1) $ mkAppl tr 289 mkAppl [] = error "inferKind: mkAppl" 290 inferKind mk $ mkAppl ts 291 inferKind mk (LazyType t _) = 292 do inferKind mk t 293 inferKind mk (KindedType t k _) = 294 do mk2 <- inferKind (Just k) t 295 checkMaybeKinds t mk mk2 296 inferKind _ t = 264 297 do addDiags [mkDiag Error "unresolved type" t] 265 return star 266 267 checkTypeKind :: Type -> Kind -> State Env () 268 checkTypeKind t j = do k <- inferKind t 269 checkKinds t j k 270 271 -} 298 return Nothing 272 299 273 300 getIdKind :: Id -> State Env (Maybe Kind) … … 284 311 case Map.lookup i tk of 285 312 Nothing -> Nothing 286 Just (TypeInfo kl _ _) -> Just $313 Just (TypeInfo _ l _ _) -> Just $ 287 314 if isSingle l then head l else Intersection l [] 288 315 -
branches/raw-kinds/HasCASL/TypeCheck.hs
r1673 r1722 63 63 star, AliasTypeDefn $ simpleTypeScheme logicalType), 64 64 (simpleIdToId $ mkSimpleId "Pred", 65 KindApplstar star [],65 FunKind star star [], 66 66 AliasTypeDefn defType)] 67 67 -
branches/raw-kinds/HasCASL/TypeDecl.hs
r1673 r1722 156 156 do k <- anaKind kind 157 157 checkKinds pat star k 158 newDerivs <- case derivs of 159 Just c -> do (dk, newC) <- anaClass c 160 checkKinds newC star dk 161 return $ Just newC 162 Nothing -> return Nothing 163 let Result ds m = convertTypePattern pat 158 cs <- mapM anaClassId derivs 159 let jcs = catMaybes cs 160 mapM (checkKinds pat star) jcs 161 let newDerivs = foldr( \ ck l -> case ck of 162 ClassKind ci _ -> ci:l 163 _ -> l) [] jcs 164 Result ds m = convertTypePattern pat 164 165 addDiags ds 165 166 case m of … … 189 190 anaPseudoType mk (TypeScheme tArgs (q :=> ty) p) = 190 191 do k <- case mk of 191 Nothing -> return star192 Just j -> anaKind j192 Nothing -> return Nothing 193 Just j -> anaKindM j 193 194 tm <- gets typeMap -- save global variables 194 195 mapM_ anaTypeVarDecl tArgs … … 208 209 if null tArgs then k 209 210 else typeArgsListToKind (init tArgs) 210 ( KindAppl(( \ (TypeArg _ xk _ _) -> xk) $ last tArgs) k [])211 (FunKind (( \ (TypeArg _ xk _ _) -> xk) $ last tArgs) k []) 211 212 212 213 -- | convert mixfix type patterns to ids -
branches/raw-kinds/HasCASL/VarDecl.hs
r1673 r1722 17 17 import HasCASL.ClassAna 18 18 import qualified Common.Lib.Map as Map 19 import qualified Common.Lib.Set as Set20 19 import Common.Id 21 20 import HasCASL.Le … … 41 40 -- type args not yet considered for kind construction 42 41 addTypeId defn _ kind i = 43 do nk <- expandKind kind42 do let nk = rawKind kind 44 43 if placeCount i <= kindArity TopLevel nk then 45 44 do addTypeKind defn i kind … … 59 58 addSingleTypeKind d i k = 60 59 do tk <- gets typeMap 60 let rk = rawKind k 61 61 case Map.lookup i tk of 62 62 Nothing -> putTypeMap $ Map.insert i 63 (TypeInfo k [] [] d) tk63 (TypeInfo rk [k] [] d) tk 64 64 Just (TypeInfo ok ks sups defn) -> 65 -- check with merge 66 do checkKinds i k ok 67 if any (==k) (ok:ks) 68 then addDiags [mkDiag Warning 65 if rk == ok 66 then if k `elem` ks then 67 addDiags [mkDiag Warning 69 68 "redeclared type" i] 70 69 else putTypeMap $ Map.insert i 71 70 (TypeInfo ok 72 71 (k:ks) sups defn) tk 72 else addDiags $ diffKindDiag i ok k 73 73 74 74 -- | analyse a type argument … … 86 86 -- | compute arity from a 'Kind' 87 87 kindArity :: ApplMode -> Kind -> Int 88 kindArity m (KindAppl k1 k2 _) = 89 case m of 90 TopLevel -> kindArity OnlyArg k1 + 91 kindArity TopLevel k2 92 OnlyArg -> 1 93 kindArity m (ExtClass _ _ _) = case m of 94 TopLevel -> 0 95 OnlyArg -> 1 88 kindArity m k = 89 case k of 90 FunKind k1 k2 _ -> case m of 91 TopLevel -> kindArity OnlyArg k1 + 92 kindArity TopLevel k2 93 OnlyArg -> 1 94 Universe _ -> case m of 95 TopLevel -> 0 96 OnlyArg -> 1 97 ClassKind _ ck -> kindArity m ck 98 Downset _ _ dk _ -> kindArity m dk 99 Intersection (k1:_) _ -> kindArity m k1 100 ExtKind ek _ _ -> kindArity m ek 101 _ -> error "kindArity" 102 96 103 97 104 -- --------------------------------------------------------------------------- … … 146 153 anaTypeVarDecl t >>= (return . fmap GenTypeVarDecl) 147 154 148 convertTypeToClass :: Type -> State Env (Maybe Class)149 convertTypeToClass (TypeToken t) =150 if tokStr t == "Type" then return $ Just universe else do151 let ci = simpleIdToId t152 e <- get153 mk <- anaClassId ci154 case mk of155 Nothing -> do put e156 return Nothing157 _ -> return $ Just $ Intersection (Set.single ci) []158 convertTypeToClass (BracketType Parens ts ps) =159 do cs <- mapM convertTypeToClass ts160 if all isJust cs then161 return $ Just $ Intersection (Set.unions $ map iclass $162 catMaybes cs) ps163 else return Nothing164 165 convertTypeToClass _ =166 do return Nothing167 168 155 convertTypeToKind :: Type -> State Env (Maybe Kind) 169 156 convertTypeToKind (FunType t1 FunArr t2 ps) = … … 171 158 mk2 <- convertTypeToKind t2 172 159 case (mk1, mk2) of 173 (Just k1, Just k2) -> return $ Just $ KindAppl k1 k2 ps 160 (Just k1, Just k2) -> case k2 of 161 ExtKind _ _ _ -> return Nothing 162 _ -> return $ Just $ FunKind k1 k2 ps 174 163 _ -> return Nothing 175 164 165 convertTypeToKind (BracketType Parens [] _) = 166 return Nothing 176 167 convertTypeToKind (BracketType Parens [t] _) = 177 do convertTypeToKind t 178 168 convertTypeToKind t 169 convertTypeToKind (BracketType Parens ts ps) = 170 do cs <- mapM convertTypeToKind ts 171 if all isJust cs then 172 do let k:ks = catMaybes cs 173 rk = rawKind k 174 if all ((==rk) . rawKind) ks then 175 return $ Just $ Intersection (k:ks) ps 176 else return Nothing 177 else return Nothing 179 178 convertTypeToKind (MixfixType [t1, TypeToken t]) = 180 179 let s = tokStr t … … 185 184 in case v of 186 185 InVar -> do return Nothing 187 _ -> do mk1 <- convertTypeTo Classt1186 _ -> do mk1 <- convertTypeToKind t1 188 187 case mk1 of 189 Just k1 -> return $ Just $ Ext Classk1 v [tokPos t]188 Just k1 -> return $ Just $ ExtKind k1 v [tokPos t] 190 189 _ -> return Nothing 191 convertTypeToKind t = 192 do mc <- convertTypeToClass t 193 return $ fmap ( \ c -> ExtClass c InVar []) mc 190 convertTypeToKind(TypeToken t) = 191 if tokStr t == "Type" then return $ Just $ Universe [tokPos t] else do 192 let ci = simpleIdToId t 193 e <- get 194 mk <- anaClassId ci 195 case mk of 196 Nothing -> do put e 197 return Nothing 198 Just k -> return $ Just $ ClassKind ci k 199 convertTypeToKind _ = 200 do return Nothing 194 201 195 202 optAnaVarDecl :: VarDecl -> State Env (Maybe GenVarDecl)
