AsUtils.hs revision 9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
5ba323da9f037264b4a356085e844889aedeac23Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian MaederMaintainer : maeder@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederutility functions and computations of meaningful positions for
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder various data types of the abstract syntax
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder-}
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule HasCASL.AsUtils where
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport HasCASL.As
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport HasCASL.PrintAs()
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport Common.Id
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Common.PrettyPrint
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport qualified Common.Lib.Set as Set
af621d0066770895fd79562728e93099c8c52060Christian Maeder
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder{- | decompose an 'ApplTerm' into an application of an operation and a
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder list of arguments -}
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaedergetAppl :: Term -> Maybe (Id, TypeScheme, [Term])
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedergetAppl = thrdM reverse . getRevAppl
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder thrdM :: (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder thrdM f = fmap ( \ (a, b, c) -> (a, b, f c))
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder getRevAppl :: Term -> Maybe (Id, TypeScheme, [Term])
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder getRevAppl t = case t of
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder TypedTerm trm q _ _ -> case q of
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder InType -> Nothing
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder _ -> getRevAppl trm
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder QualOp _ (InstOpId i _ _) sc _ -> Just (i, sc, [])
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder QualVar (VarDecl v ty _ _) -> Just (v, simpleTypeScheme ty, [])
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder ApplTerm t1 t2 _ -> thrdM (t2:) $ getRevAppl t1
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder _ -> Nothing
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder-- | extract bindings from an analysed pattern
024621f43239cfe9629e35d35a8669fad7acbba2Christian MaederextractVars :: Pattern -> [VarDecl]
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederextractVars pat =
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder case pat of
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder QualVar vd -> getVd vd
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder ApplTerm p1 p2 _ ->
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder extractVars p1 ++ extractVars p2
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder TupleTerm pats _ -> concatMap extractVars pats
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder TypedTerm p _ _ _ -> extractVars p
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder AsPattern v p2 _ -> getVd v ++ extractVars p2
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder ResolvedMixTerm _ pats _ -> concatMap extractVars pats
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder _ -> []
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder where getVd vd@(VarDecl v _ _ _) = if showId v "" == "_" then [] else [vd]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | construct term from id
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermkOpTerm :: Id -> TypeScheme -> Term
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermkOpTerm i sc = QualOp Op (InstOpId i [] []) sc []
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | bind a term
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedermkForall :: [GenVarDecl] -> Term -> Term
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedermkForall vl f = if null vl then f else QuantifiedTerm Universal vl f []
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | construct application with curried arguments
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedermkApplTerm :: Term -> [Term] -> Term
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermkApplTerm = foldl ( \ t a -> ApplTerm t a [])
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | make function arrow partial after some arguments
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederaddPartiality :: [a] -> Type -> Type
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederaddPartiality args t = case args of
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder [] -> LazyType t []
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder _ : rs -> case t of
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder FunType t1 a t2 ps -> if null rs then FunType t1 PFunArr t2 ps
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder else FunType t1 a (addPartiality rs t2) ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder _ -> error "addPartiality"
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | convert a type argument to a type
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedertypeArgToType :: TypeArg -> Type
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedertypeArgToType (TypeArg i _ rk c _ _) = TypeName i rk c
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder{- | convert a parameterized type identifier with a result raw kind
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder to a type application -}
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederpatToType :: TypeId -> [TypeArg] -> RawKind -> Type
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederpatToType i args rk = mkTypeAppl
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder (TypeName i (typeArgsListToRawKind True args rk) 0)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder $ map typeArgToType args
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | create the (raw if True) kind from type arguments
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedertypeArgsListToRawKind :: Bool -> [TypeArg] -> Kind -> Kind
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedertypeArgsListToRawKind b tArgs = mkFunKind $
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder map ( \ (TypeArg _ ak rk _ _ _) -> if b then rk else toKind ak) tArgs
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder
986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian Maeder-- | create the kind from type arguments
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaedertypeArgsListToKind :: [TypeArg] -> Kind -> Kind
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaedertypeArgsListToKind = typeArgsListToRawKind False
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder-- | get the type of a constructor with given curried argument types
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaedergetConstrType :: Type -> Partiality -> [Type] -> Type
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaedergetConstrType rty p ts = (case p of
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder Total -> id
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder Partial -> addPartiality ts) $
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder foldr ( \ c r -> FunType c FunArr r [] )
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder rty ts
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | get the type of a selector given the data type as first arguemnt
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedergetSelType :: Type -> Partiality -> Type -> Type
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedergetSelType dt p rt = (case p of
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder Partial -> addPartiality [dt]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Total -> id) (FunType dt FunArr rt [])
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder-- | get the type of a constructor for printing (kinds may be wrong)
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian MaedercreateConstrType :: Id -> [TypeArg] -> RawKind -> Partiality -> [Type] -> Type
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaedercreateConstrType i is rk =
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder getConstrType (patToType i is rk)
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- | get the type variable
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaedergetTypeVar :: TypeArg -> Id
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedergetTypeVar(TypeArg v _ _ _ _ _) = v
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder-- | construct application left-associative
ad187062b0009820118c1b773a232e29b879a2faChristian MaedermkTypeAppl :: Type -> [Type] -> Type
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaedermkTypeAppl = foldl ( \ c a -> TypeAppl c a)
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder-- | get the kind of an analyzed type variable
ad187062b0009820118c1b773a232e29b879a2faChristian MaedertoKind :: VarKind -> Kind
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaedertoKind vk = case vk of
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder VarKind k -> k
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder Downset t -> case t of
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder KindedType _ k _ -> k
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder _ -> error "toKind: Downset"
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder MissingKind -> error "toKind: Missing"
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder-- | generate a comparison string
ad187062b0009820118c1b773a232e29b879a2faChristian Maederexpected :: PrettyPrint a => a -> a -> String
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederexpected a b =
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder "\n expected: " ++ showPretty a
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder "\n found: " ++ showPretty b "\n"
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder-- * compute better positions
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederposOfVars :: Vars -> [Pos]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederposOfVars vr =
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder case vr of
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Var v -> posOfId v
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder VarTuple _ ps -> ps
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
8485da94b57d8b5135ee685b55c982b037ed4140Christian MaederposOfTypeArg :: TypeArg -> [Pos]
8485da94b57d8b5135ee685b55c982b037ed4140Christian MaederposOfTypeArg (TypeArg t _ _ _ _ ps) = firstPos [t] ps
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder
e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederposOfTypePattern :: TypePattern -> [Pos]
e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederposOfTypePattern pat =
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder case pat of
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder TypePattern t _ _ -> posOfId t
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder TypePatternToken t -> tokPos t
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder MixfixTypePattern ts -> posOf ts
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder BracketTypePattern _ ts ps -> firstPos ts ps
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder TypePatternArg (TypeArg t _ _ _ _ _) _ -> posOfId t
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaederposOfType :: Type -> [Pos]
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederposOfType ty =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder case ty of
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder TypeName i _ _ -> posOfId i
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder TypeAppl t1 t2 -> concatMap posOfType [t1, t2]
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ExpandedType t1 t2 -> concatMap posOfType [t1, t2]
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder TypeToken t -> tokPos t
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder BracketType _ ts ps -> concatMap posOfType ts ++ ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder KindedType t _ ps -> posOfType t ++ ps
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder MixfixType ts -> concatMap posOfType ts
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder LazyType t ps -> posOfType t ++ ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder ProductType ts ps -> concatMap posOfType ts ++ ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder FunType t1 _ t2 ps -> concatMap posOfType [t1, t2] ++ ps
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederposOfTerm :: Term -> [Pos]
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederposOfTerm trm =
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder case trm of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder QualVar v -> posOfVarDecl v
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder QualOp _ (InstOpId i _ ps) _ qs -> firstPos [i] (ps++qs)
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder ResolvedMixTerm i _ _ -> posOfId i
f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian Maeder ApplTerm t1 t2 ps -> firstPos [t1, t2] ps
c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder TupleTerm ts ps -> firstPos ts ps
fce77b2785912d1abbcc3680088b235f534bdeffChristian Maeder TypedTerm t _ _ ps -> firstPos [t] ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder QuantifiedTerm _ _ t ps -> firstPos [t] ps
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder LambdaTerm _ _ t ps -> firstPos [t] ps
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder CaseTerm t _ ps -> firstPos [t] ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder LetTerm _ _ t ps -> firstPos [t] ps
ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder TermToken t -> tokPos t
039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder MixTypeTerm _ t ps -> firstPos [t] ps
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder MixfixTerm ts -> posOf ts
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder BracketTerm _ ts ps -> firstPos ts ps
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder AsPattern v _ ps -> firstPos [v] ps
039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder
ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian MaederposOfVarDecl :: VarDecl -> [Pos]
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian MaederposOfVarDecl (VarDecl v _ _ ps) = firstPos [v] ps
7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder
021d7137df04ec1834911d99d90243a092841cedChristian Maederinstance PosItem a => PosItem [a] where
021d7137df04ec1834911d99d90243a092841cedChristian Maeder get_pos = concatMap get_pos
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederinstance PosItem a => PosItem (a, b) where
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder get_pos (a, _) = get_pos a
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederinstance PosItem a => PosItem (Set.Set a) where
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder get_pos = get_pos . Set.toList
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder