hets/HasCASL/AsUtils.hs

	AsUtils.hs revision ce7653c9c71e23bf04a5ec0ca5cb600c3738a909
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule      :  $Header$
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederCopyright   :  (c) Christian Maeder and Uni Bremen 2003
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer  :  maeder@tzi.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability   :  experimental
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability :  portable
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederutility functions and computations of meaningful positions for
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder   various data types of the abstract syntax
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder-}
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maedermodule HasCASL.AsUtils where
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport HasCASL.As
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport HasCASL.PrintAs()
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Common.Id
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.PrettyPrint
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Common.Lib.Set as Set
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder-- | recursively substitute type names within a type
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederrename :: (TypeId -> Kind -> Int -> Type) -> Type -> Type
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederrename m t = case t of
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder           TypeName i k n -> m i k n
62925f4a144f45b5ed1e7c841f891d13f51e553dChristian Maeder           TypeAppl t1 t2 -> TypeAppl (rename m t1) (rename m t2)
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder           ExpandedType t1 t2 -> ExpandedType (rename m t1) (rename m t2)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder           TypeToken _ -> t
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder           BracketType b l ps ->
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder               BracketType b (map (rename m) l) ps
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder           KindedType tk k ps ->
d17834302eaa101395b4b806cd73670fd864445fChristian Maeder               KindedType (rename m tk) k ps
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder           MixfixType l -> MixfixType $ map (rename m) l
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder           LazyType tl ps -> LazyType (rename m tl) ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder           ProductType l ps -> ProductType (map (rename m) l) ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder           FunType t1 a t2 ps -> FunType (rename m t1) a (rename m t2) ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder{- | decompose an 'ApplTerm' into an application of an operation and a
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder     list of arguments -}
836e72a3c413366ba9801726f3b249c7791cb9caChristian MaedergetAppl :: Term -> Maybe (Id, TypeScheme, [Term])
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaedergetAppl = thrdM reverse . getAppl2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    thrdM :: (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    thrdM f = fmap ( \ (a, b, c) -> (a, b, f c))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    getAppl2 :: Term -> Maybe (Id, TypeScheme, [Term])
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    getAppl2 t = case t of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder        TypedTerm trm q _ _ -> case q of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder            InType -> Nothing
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder            _ -> getAppl2 trm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder        QualOp _ (InstOpId i _ _) sc _ -> Just (i, sc, [])
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder        QualVar (VarDecl v ty _ _) -> Just (v, simpleTypeScheme ty, [])
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder        ApplTerm t1 t2 _ -> thrdM (t2:) $ getAppl2 t1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder        _ -> Nothing
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | extract bindings from an analysed pattern
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederextractVars :: Pattern -> [VarDecl]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederextractVars pat =
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder    case pat of
fa45d098e1c9d468f128be9505eb7e5b2705b304Christian Maeder    QualVar vd -> getVd vd
25612a7b3ce708909298d5426406592473880a20Christian Maeder    ApplTerm p1 p2 _ ->
0b75edd800cef1a3b695f24df39d13f1ceace257Christian Maeder         extractVars p1 ++ extractVars p2
0b75edd800cef1a3b695f24df39d13f1ceace257Christian Maeder    TupleTerm pats _ -> concatMap extractVars pats
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder    TypedTerm p _ _ _ -> extractVars p
18b709ce961d68328da768318dcc70067f066d86Christian Maeder    AsPattern v p2 _ -> getVd v ++ extractVars p2
18b709ce961d68328da768318dcc70067f066d86Christian Maeder    ResolvedMixTerm _ pats _ -> concatMap extractVars pats
18b709ce961d68328da768318dcc70067f066d86Christian Maeder    _ -> []
18b709ce961d68328da768318dcc70067f066d86Christian Maeder    where getVd vd@(VarDecl v _ _ _) = if showId v "" == "_" then [] else [vd]
18b709ce961d68328da768318dcc70067f066d86Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | construct term from id
18b709ce961d68328da768318dcc70067f066d86Christian MaedermkOpTerm :: Id -> TypeScheme -> Term
18b709ce961d68328da768318dcc70067f066d86Christian MaedermkOpTerm i sc = QualOp Op (InstOpId i [] []) sc []
18b709ce961d68328da768318dcc70067f066d86Christian Maeder
b814fecd0a2dbdeae62402903783d08e4206b4d2Christian Maeder-- | bind a term
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermkForall :: [GenVarDecl] -> Term -> Term
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedermkForall vl f = if null vl then f else QuantifiedTerm Universal vl f []
18b709ce961d68328da768318dcc70067f066d86Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | construct application with curried arguments
18b709ce961d68328da768318dcc70067f066d86Christian MaedermkApplTerm :: Term -> [Term] -> Term
9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaedermkApplTerm = foldl ( \ t a -> ApplTerm t a [])
18b709ce961d68328da768318dcc70067f066d86Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | make function arrow partial after some arguments
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederaddPartiality :: [a] -> Type -> Type
9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederaddPartiality as t = case as of
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder        [] -> LazyType t []
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder        _ : rs -> case t of
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder           FunType t1 a t2 ps -> if null rs then FunType t1 PFunArr t2 ps
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder               else FunType t1 a (addPartiality rs t2) ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder           _ -> error "addPartiality"
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder-- | get the partiality from a constructor type
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder-- with a given number of curried arguments
797f811e57952d59e73b8cd03b667eef276db972Christian MaedergetPartiality :: [a] -> Type -> Partiality
797f811e57952d59e73b8cd03b667eef276db972Christian MaedergetPartiality as t = case t of
18b709ce961d68328da768318dcc70067f066d86Christian Maeder   KindedType ty _ _ -> getPartiality as ty
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski   FunType _ a t2 _ -> case as of
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder     [] -> Total
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder     [_] -> case a of
18b709ce961d68328da768318dcc70067f066d86Christian Maeder            PFunArr  -> Partial
18b709ce961d68328da768318dcc70067f066d86Christian Maeder            PContFunArr -> Partial
18b709ce961d68328da768318dcc70067f066d86Christian Maeder            _ -> Total
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder     _:rs -> getPartiality rs t2
3f7009c892b16d172314abbba83d663fa0d87a65Christian Maeder   LazyType _ _ -> if null as then Partial else error "getPartiality"
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder   _ -> Total
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maedertype DataPat = (Id, [TypeArg], Kind)
22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder
22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder-- | get the type of a constructor with given curried argument types
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedergetConstrType :: DataPat -> Partiality -> [Type] -> Type
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedergetConstrType dt p ts = (case p of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder     Total -> id
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder     Partial -> addPartiality ts) $
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder                       foldr ( \ c r -> FunType c FunArr r [] )
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski                             (typeIdToType dt) ts
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | compute the type given by the input
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedertypeIdToType :: DataPat -> Type
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedertypeIdToType (i, nAs, k) = let
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    fullKind = typeArgsListToKind nAs k
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    ti = TypeName i fullKind 0
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    mkType _ ty [] = ty
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder    mkType n ty (TypeArg ai ak _ _ : rest) =
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder        mkType (n-1) (TypeAppl ty (TypeName ai (toKind ak) n)) rest
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder    in mkType (-1) ti nAs
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder-- | extent a kind to expect further type arguments
9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaedertypeArgsListToKind :: [TypeArg] -> Kind -> Kind
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedertypeArgsListToKind tArgs k =
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder    if null tArgs then k
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder       else typeArgsListToKind (init tArgs)
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder            (FunKind (( \ (TypeArg _ xk _ _) -> toKind xk) $ last tArgs) k [])
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedertoKind :: VarKind -> Kind
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian MaedertoKind vk = case vk of
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder    VarKind k -> k
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder    Downset t -> case t of
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder        KindedType _ k _ -> k
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder        _ -> error "toKind: Downset"
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder    MissingKind -> error "toKind: Missing"
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder-- | generate a comparison string
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederexpected :: PrettyPrint a => a -> a -> String
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maederexpected a b =
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder    "\n  expected: " ++ showPretty a
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder    "\n     found: " ++ showPretty b "\n"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- ---------------------------------------------------------------------
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederposOfVars :: Vars -> [Pos]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederposOfVars vr =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    case vr of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    Var v -> posOfId v
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    VarTuple _ ps -> ps
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian MaederposOfTypeArg :: TypeArg -> [Pos]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederposOfTypeArg (TypeArg t _ _ ps) = firstPos [t] ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian MaederposOfTypePattern :: TypePattern -> [Pos]
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian MaederposOfTypePattern pat =
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder    case pat of
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder    TypePattern t _ _ -> posOfId t
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder    TypePatternToken t -> tokPos t
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder    MixfixTypePattern ts -> posOf ts
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder    BracketTypePattern _ ts ps -> firstPos ts ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    TypePatternArg (TypeArg t _ _ _) _ -> posOfId t
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian MaederposOfType :: Type -> [Pos]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederposOfType ty =
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder    case ty of
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder    TypeName i _ _ -> posOfId i
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder    TypeAppl t1 t2 -> concatMap posOfType [t1, t2]
    ExpandedType t1 t2 -> concatMap posOfType [t1, t2]
    TypeToken t -> tokPos t
    BracketType _ ts ps -> concatMap posOfType ts ++ ps
    KindedType t _ ps -> posOfType t ++ ps
    MixfixType ts -> concatMap posOfType ts
    LazyType t ps -> posOfType t ++ ps
    ProductType ts ps -> concatMap posOfType ts ++ ps
    FunType t1 _ t2 ps -> concatMap posOfType [t1, t2] ++ ps

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 a => PosItem [a] where
    get_pos = concatMap get_pos

instance PosItem a => PosItem (a, b) where
    get_pos (a, _) = get_pos a

instance PosItem a => PosItem (Set.Set a) where
    get_pos = get_pos . Set.toList