AsUtils.hs revision 97018cf5fa25b494adffd7e9b4e87320dae6bf47
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt{- |
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntModule : $Header$
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntCopyright : (c) Christian Maeder and Uni Bremen 2003
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntMaintainer : maeder@tzi.de
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntStability : experimental
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntPortability : portable
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt utility functions and computations of meaningful positions for
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt various data types of the abstract syntax
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-}
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntmodule HasCASL.AsUtils where
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.As
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.PrintAs()
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.Id
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.PrettyPrint
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport qualified Common.Lib.Set as Set
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | recursively substitute type names within a type
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntrename :: (TypeId -> Kind -> Int -> Type) -> Type -> Type
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntrename m t = case t of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeName i k n -> m i k n
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeAppl t1 t2 -> TypeAppl (rename m t1) (rename m t2)
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ExpandedType t1 t2 -> ExpandedType (rename m t1) (rename m t2)
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeToken _ -> t
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt BracketType b l ps ->
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt BracketType b (map (rename m) l) ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt KindedType tk k ps ->
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt KindedType (rename m tk) k ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt MixfixType l -> MixfixType $ map (rename m) l
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt LazyType tl ps -> LazyType (rename m tl) ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ProductType l ps -> ProductType (map (rename m) l) ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt FunType t1 a t2 ps -> FunType (rename m t1) a (rename m t2) ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt{- | decompose an 'ApplTerm' into an application of an operation and a
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt list of arguments -}
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntgetAppl :: Term -> Maybe (Id, TypeScheme, [Term])
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntgetAppl = thrdM reverse . getAppl2
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt where
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt thrdM :: (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt thrdM f = fmap ( \ (a, b, c) -> (a, b, f c))
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt getAppl2 :: Term -> Maybe (Id, TypeScheme, [Term])
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt getAppl2 t = case t of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypedTerm trm q _ _ -> case q of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt InType -> Nothing
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> getAppl2 trm
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt QualOp _ (InstOpId i _ _) sc _ -> Just (i, sc, [])
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt QualVar (VarDecl v ty _ _) -> Just (v, simpleTypeScheme ty, [])
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ApplTerm t1 t2 _ -> thrdM (t2:) $ getAppl2 t1
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> Nothing
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | extract bindings from an analysed pattern
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntextractVars :: Pattern -> [VarDecl]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntextractVars pat =
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case pat of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt QualVar vd -> getVd vd
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ApplTerm p1 p2 _ ->
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt extractVars p1 ++ extractVars p2
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TupleTerm pats _ -> concatMap extractVars pats
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypedTerm p _ _ _ -> extractVars p
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt AsPattern v p2 _ -> getVd v ++ extractVars p2
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ResolvedMixTerm _ pats _ -> concatMap extractVars pats
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> []
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt where getVd vd@(VarDecl v _ _ _) = if showId v "" == "_" then [] else [vd]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | construct term from id
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntmkOpTerm :: Id -> TypeScheme -> Term
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntmkOpTerm i sc = QualOp Op (InstOpId i [] []) sc []
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | bind a term
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntmkForall :: [GenVarDecl] -> Term -> Term
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntmkForall vl f = if null vl then f else QuantifiedTerm Universal vl f []
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | construct application with curried arguments
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntmkApplTerm :: Term -> [Term] -> Term
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntmkApplTerm trm args = if null args then trm
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else mkApplTerm (ApplTerm trm (head args) []) $ tail args
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | get the type of a constructor with given curried argument types
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntgetConstrType :: DataPat -> Partiality -> [Type] -> Type
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntgetConstrType dt p ts = (case p of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Total -> id
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Partial -> addPartiality ts) $
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt foldr ( \ c r -> FunType c FunArr r [] )
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt (typeIdToType dt) ts
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | make function arrow partial after some arguments
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntaddPartiality :: [a] -> Type -> Type
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntaddPartiality as t = case as of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt [] -> LazyType t []
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ : rs -> case t of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt FunType t1 a t2 ps -> if null rs then FunType t1 PFunArr t2 ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else FunType t1 a (addPartiality rs t2) ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> error "addPartiality"
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | get the partiality from a constructor type
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- with a given number of curried arguments
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntgetPartiality :: [a] -> Type -> Partiality
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntgetPartiality as t = case t of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt KindedType ty _ _ -> getPartiality as ty
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt FunType _ a t2 _ -> case as of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt [] -> Total
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt [_] -> case a of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt PFunArr -> Partial
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt PContFunArr -> Partial
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> Total
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _:rs -> getPartiality rs t2
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt LazyType _ _ -> if null as then Partial else error "getPartiality"
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> Total
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunttype DataPat = (Id, [TypeArg], Kind)
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | compute the type given by the input
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HunttypeIdToType :: DataPat -> Type
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HunttypeIdToType (i, nAs, k) = let
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt fullKind = typeArgsListToKind nAs k
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ti = TypeName i fullKind 0
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mkType _ ty [] = ty
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mkType n ty ((TypeArg ai ak _ _): rest) =
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mkType (n-1) (TypeAppl ty (TypeName ai ak n)) rest
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt in mkType (-1) ti nAs
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | extent a kind to expect further type arguments
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HunttypeArgsListToKind :: [TypeArg] -> Kind -> Kind
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HunttypeArgsListToKind tArgs k =
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt if null tArgs then k
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else typeArgsListToKind (init tArgs)
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt (FunKind (( \ (TypeArg _ xk _ _) -> xk) $ last tArgs) k [])
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | generate a comparison string
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntexpected :: PrettyPrint a => a -> a -> String
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntexpected a b =
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt "\n expected: " ++ showPretty a
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt "\n found: " ++ showPretty b "\n"
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- ---------------------------------------------------------------------
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfKind :: Kind -> [Pos]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfKind k = case k of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt MissingKind -> []
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ClassKind c _ -> posOfId c
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> get_pos k
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfVars :: Vars -> [Pos]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfVars vr =
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case vr of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Var v -> posOfId v
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt VarTuple _ ps -> ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfTypeArg :: TypeArg -> [Pos]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfTypeArg (TypeArg t _ _ ps) = firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfTypePattern :: TypePattern -> [Pos]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfTypePattern pat =
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case pat of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypePattern t _ _ -> posOfId t
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypePatternToken t -> tokPos t
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt MixfixTypePattern ts -> posOf ts
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt BracketTypePattern _ ts ps -> firstPos ts ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypePatternArg (TypeArg t _ _ _) _ -> posOfId t
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfType :: Type -> [Pos]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfType ty =
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case ty of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeName i _ _ -> posOfId i
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeAppl t1 t2 -> posOf [t1, t2]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ExpandedType t1 t2 -> posOf [t1, t2]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeToken t -> tokPos t
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt BracketType _ ts ps -> firstPos ts ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt KindedType t _ ps -> firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt MixfixType ts -> posOf ts
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt LazyType t ps -> firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ProductType ts ps -> firstPos ts ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt FunType t1 _ t2 ps -> firstPos [t1,t2] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfTerm :: Term -> [Pos]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfTerm trm =
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case trm of
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt QualVar v -> posOfVarDecl v
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt QualOp _ (InstOpId i _ ps) _ qs -> firstPos [i] (ps++qs)
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ResolvedMixTerm i _ _ -> posOfId i
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ApplTerm t1 t2 ps -> firstPos [t1, t2] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TupleTerm ts ps -> firstPos ts ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypedTerm t _ _ ps -> firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt QuantifiedTerm _ _ t ps -> firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt LambdaTerm _ _ t ps -> firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt CaseTerm t _ ps -> firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt LetTerm _ _ t ps -> firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TermToken t -> tokPos t
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt MixTypeTerm _ t ps -> firstPos [t] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt MixfixTerm ts -> posOf ts
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt BracketTerm _ ts ps -> firstPos ts ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt AsPattern v _ ps -> firstPos [v] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfVarDecl :: VarDecl -> [Pos]
b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntposOfVarDecl (VarDecl v _ _ ps) = firstPos [v] ps
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntinstance PosItem a => PosItem [a] where
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt get_pos = concatMap get_pos
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntinstance PosItem a => PosItem (a, b) where
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt get_pos (a, _) = get_pos a
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntinstance PosItem a => PosItem (Set.Set a) where
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt get_pos = get_pos . Set.toList
b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt