AsUtils.hs revision e76e6a43f51438215737d6fc176c89da05bb86da
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuCopyright : (c) Christian Maeder and Uni Bremen 2003
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuMaintainer : hets@tzi.de
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuStability : experimental
402ffc909b645ddb2d5c76343bf74a6cb33c6205Christian MaederPortability : portable
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu compute meaningful positions for various data types of the abstract syntax
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu-}
90d7cac36f60438bd35124e3389b5bce6d114b46Christian Maeder
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescumodule HasCASL.AsUtils where
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport HasCASL.As
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport HasCASL.PrintAs -- to reexport instances
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport Common.Id
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport Common.PrettyPrint
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu-- | extract bindings from an analysed pattern
392634badbe11a21c7825ee0e1ee132220a2539eMihai CodescuextractVars :: Pattern -> [VarDecl]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederextractVars pat =
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu case pat of
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu QualVar vd -> getVd vd
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu ApplTerm p1 p2 _ ->
5418aa59492005c2ca40436ab84c4029cd2922a5Christian Maeder extractVars p1 ++ extractVars p2
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski TupleTerm pats _ -> concatMap extractVars pats
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu TypedTerm p _ _ _ -> extractVars p
5418aa59492005c2ca40436ab84c4029cd2922a5Christian Maeder AsPattern v p2 _ -> getVd v ++ extractVars p2
5418aa59492005c2ca40436ab84c4029cd2922a5Christian Maeder ResolvedMixTerm _ pats _ -> concatMap extractVars pats
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu _ -> []
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu where getVd vd@(VarDecl v _ _ _) = if showId v "" == "_" then [] else [vd]
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu
3bc502518f75cd5a21aa2f608a31f50c19134db0Christian Maeder-- | construct term from id
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumkOpTerm :: Id -> TypeScheme -> Term
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumkOpTerm i sc = QualOp Op (InstOpId i [] []) sc []
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- | bind a term
7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai CodescumkForall :: [GenVarDecl] -> Term -> Term
7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai CodescumkForall vl f = if null vl then f else QuantifiedTerm Universal vl f []
7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu
7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu-- | construct application with curried arguments
7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai CodescumkApplTerm :: Term -> [Term] -> Term
7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai CodescumkApplTerm trm args = if null args then trm
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu else mkApplTerm (ApplTerm trm (head args) []) $ tail args
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- | get the type of a constructor with given curried argument types
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescugetConstrType :: Type -> Partiality -> [Type] -> Type
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetConstrType dt p ts = (case p of
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Total -> id
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Partial -> addPartiality ts) $
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu foldr ( \ c r -> FunType c FunArr r [] ) dt ts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- | make function arrow partial after some arguments
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescuaddPartiality :: [a] -> Type -> Type
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescuaddPartiality as t = case as of
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu [] -> LazyType t []
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu _ : rs -> case t of
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu FunType t1 a t2 ps -> if null rs then FunType t1 PFunArr t2 ps
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu else FunType t1 a (addPartiality rs t2) ps
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu _ -> error "addPartiality"
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- | get the partiality from a constructor type
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- with a given number of curried arguments
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescugetPartiality :: [a] -> Type -> Partiality
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescugetPartiality as t = case t of
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu KindedType ty _ _ -> getPartiality as ty
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu FunType _ a t2 _ -> case as of
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu [] -> Total
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu [_] -> case a of
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu PFunArr -> Partial
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu PContFunArr -> Partial
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu _ -> Total
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _:rs -> getPartiality rs t2
272a5a82588ab4115dac5eb81d43d74929e99ad7Till Mossakowski LazyType _ _ -> if null as then Partial else error "getPartiality"
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu _ -> Total
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- | compute the type given by the input
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescutypeIdToType :: Id -> [TypeArg] -> Kind -> Type
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescutypeIdToType i nAs k = let
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu fullKind = typeArgsListToKind nAs k
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu ti = TypeName i fullKind 0
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu mkType _ ty [] = ty
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu mkType n ty ((TypeArg ai ak _ _): rest) =
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu mkType (n-1) (TypeAppl ty (TypeName ai ak n)) rest
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu in mkType (-1) ti nAs
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- | extent a kind to expect further type arguments
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertypeArgsListToKind :: [TypeArg] -> Kind -> Kind
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescutypeArgsListToKind tArgs k =
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu if null tArgs then k
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else typeArgsListToKind (init tArgs)
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu (FunKind (( \ (TypeArg _ xk _ _) -> xk) $ last tArgs) k [])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | generate a comparison string
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuexpected :: PrettyPrint a => a -> a -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederexpected a b =
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu "\n expected: " ++ showPretty a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "\n found: " ++ showPretty b "\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuinstance PosItem Kind where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder get_pos = Just . posOfKind
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederposOfKind :: Kind -> Pos
142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescuposOfKind k =
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu case k of
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu MissingKind -> nullPos
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu ClassKind c _ -> posOfId c
142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Downset _ t _ ps -> firstPos [t] ps
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu Intersection ks ps -> firstPos ks ps
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu FunKind k1 _ ps -> firstPos [k1] ps
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu ExtKind ek _ ps -> firstPos [ek] ps
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski-- ---------------------------------------------------------------------
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski
803425dfe6a5da41b9cea480788980fa104545adMihai CodescuposOfVars :: Vars -> Pos
803425dfe6a5da41b9cea480788980fa104545adMihai CodescuposOfVars vr =
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu case vr of
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu Var v -> posOfId v
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder VarTuple vs ps -> firstPos vs ps
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
803425dfe6a5da41b9cea480788980fa104545adMihai Codescuinstance PosItem Vars where
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu get_pos = Just . posOfVars
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
803425dfe6a5da41b9cea480788980fa104545adMihai Codescuinstance PosItem TypePattern where
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu get_pos = Just . posOfTypePattern
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederposOfTypeArg :: TypeArg -> Pos
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederposOfTypeArg (TypeArg t _ _ ps) = firstPos [t] ps
b7f625188b6bf3d708b2a1b64a6cea7880708adbChristian Maeder
803425dfe6a5da41b9cea480788980fa104545adMihai Codescuinstance PosItem TypeArg where
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu get_pos = Just . posOfTypeArg
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu
803425dfe6a5da41b9cea480788980fa104545adMihai CodescuposOfTypePattern :: TypePattern -> Pos
803425dfe6a5da41b9cea480788980fa104545adMihai CodescuposOfTypePattern pat =
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu case pat of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder TypePattern t _ _ -> posOfId t
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu TypePatternToken t -> tokPos t
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu MixfixTypePattern ts -> posOf ts
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu BracketTypePattern _ ts ps -> firstPos ts ps
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu TypePatternArg (TypeArg t _ _ _) _ -> posOfId t
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu-- ---------------------------------------------------------------------
b7f625188b6bf3d708b2a1b64a6cea7880708adbChristian Maeder
b7f625188b6bf3d708b2a1b64a6cea7880708adbChristian Maederinstance PosItem TypeScheme where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder get_pos (TypeScheme tArgs _ ps) = Just $ firstPos tArgs ps
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
803425dfe6a5da41b9cea480788980fa104545adMihai Codescuinstance PosItem Type where
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu get_pos = Just . posOfType
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu
803425dfe6a5da41b9cea480788980fa104545adMihai CodescuposOfType :: Type -> Pos
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederposOfType ty =
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu case ty of
TypeName i _ _ -> posOfId i
TypeAppl t1 t2 -> posOf [t1, t2]
ExpandedType t1 t2 -> posOf [t1, t2]
TypeToken t -> tokPos t
BracketType _ ts ps -> firstPos ts ps
KindedType t _ ps -> firstPos [t] ps
MixfixType ts -> posOf ts
LazyType t ps -> firstPos [t] ps
ProductType ts ps -> firstPos ts ps
FunType t1 _ t2 ps -> firstPos [t1,t2] ps
-- ---------------------------------------------------------------------
instance PosItem Term where
get_pos = Just . posOfTerm
posOfTerm :: Term -> Pos
posOfTerm trm =
case trm of
QualVar v -> posOfVarDecl v
QualOp _ (InstOpId i _ ps) _ qs -> firstPos [i] (ps++qs)
ResolvedMixTerm i _ _ -> posOfId i
ApplTerm t1 t2 ps -> firstPos [t1, t2] ps
TupleTerm ts ps -> firstPos ts ps
TypedTerm t _ _ ps -> firstPos [t] ps
QuantifiedTerm _ _ t ps -> firstPos [t] ps
LambdaTerm _ _ t ps -> firstPos [t] ps
CaseTerm t _ ps -> firstPos [t] ps
LetTerm _ _ t ps -> firstPos [t] ps
TermToken t -> tokPos t
MixTypeTerm _ t ps -> firstPos [t] ps
MixfixTerm ts -> posOf ts
BracketTerm _ ts ps -> firstPos ts ps
AsPattern v _ ps -> firstPos [v] ps
-- ---------------------------------------------------------------------
posOfVarDecl :: VarDecl -> Pos
posOfVarDecl (VarDecl v _ _ ps) = firstPos [v] ps
instance PosItem VarDecl where
get_pos = Just . posOfVarDecl