hets/HasCASL/Morphism.hs

	Morphism.hs revision 7221c71b38c871ce66eee4537cb681d468308dfb
967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule      :  $Header$
967e5f3c25249c779575864692935627004d3f9eChristian MaederCopyright   :  (c) Christian Maeder and Uni Bremen 2002-2003
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer  :  hets@tzi.de
967e5f3c25249c779575864692935627004d3f9eChristian MaederStability   :  provisional
62599a910de0701b0f9461e534a43d5900131c55Christian MaederPortability :  non-portable (deriving Typeable)
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaederMorphism on 'Env' (as for CASL)
967e5f3c25249c779575864692935627004d3f9eChristian Maeder-}
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maedermodule HasCASL.Morphism where
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport HasCASL.Le
997c56f3bc74a703043010978e5013fdb074d659Christian Maederimport HasCASL.HToken
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport HasCASL.As
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maederimport HasCASL.AsToLe
997c56f3bc74a703043010978e5013fdb074d659Christian Maederimport HasCASL.PrintAs
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maederimport HasCASL.PrintLe
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maederimport HasCASL.Unify
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport HasCASL.Merge
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport HasCASL.Symbol
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport Common.Id
997c56f3bc74a703043010978e5013fdb074d659Christian Maederimport Common.Keywords
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport Common.Result
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiimport Common.PrettyPrint
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiimport Common.Lib.Pretty
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maederimport Common.Lib.State
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport qualified Common.Lib.Map as Map
997c56f3bc74a703043010978e5013fdb074d659Christian Maederimport qualified Common.Lib.Set as Set
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maederimport Data.Dynamic
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederdata SymbolType = OpAsItemType TypeScheme
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder        | TypeAsItemType Kind
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder        | ClassAsItemType Kind
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder          deriving (Show, Eq, Ord)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
997c56f3bc74a703043010978e5013fdb074d659Christian Maederinstance PrettyPrint SymbolType where
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder    printText0 ga t = case t of
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder      OpAsItemType sc -> printText0 ga sc
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder      TypeAsItemType k -> printText0 ga k
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder      ClassAsItemType k -> printText0 ga k
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederinstance Ord TypeScheme where
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    sc1 <= sc2 = let (t1, c) = runState (freshInst sc1) 1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             t2 = evalState (freshInst sc2) c
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             v1 = varsOf t1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             v2 = varsOf t2
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                 in case compare (length v1) $ length v2 of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder            LT -> True
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder            EQ -> t1 <= subst (Map.fromList $
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                zipWith (\ v (TypeArg i k _ _) ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                     (v, TypeName i k 1)) v1 v2) t2
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder            GT -> False
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederdata Symbol = Symbol {symName :: Id, symbType :: SymbolType}
62599a910de0701b0f9461e534a43d5900131c55Christian Maeder          deriving (Show, Eq, Ord, Typeable)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederdata RawSymbol = ASymbol Symbol | AnID Id | AKindedId SymbKind Id
62599a910de0701b0f9461e534a43d5900131c55Christian Maeder                 deriving (Show, Eq, Ord, Typeable)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maedertype SymbolMap = Map.Map Symbol Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToTypeSymbol :: Id -> Kind -> Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToTypeSymbol idt k = Symbol idt $ TypeAsItemType k
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToOpSymbol :: Id -> TypeScheme -> Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederidToOpSymbol idt typ = Symbol idt $ OpAsItemType typ
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederidToRaw :: Id -> RawSymbol
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederidToRaw x = AnID x
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbTypeToKind :: SymbolType -> SymbKind
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymbTypeToKind (OpAsItemType _)    = SK_op
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymbTypeToKind (TypeAsItemType _)  = SK_type
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymbTypeToKind (ClassAsItemType _) = SK_class
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbolToRaw :: Symbol -> RawSymbol
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymbolToRaw sym = ASymbol sym
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder-- symbolToRaw (Symbol idt typ) = AKindedId (symbTypeToKind typ) idt
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder
997c56f3bc74a703043010978e5013fdb074d659Christian MaedersymOf :: Env -> Set.Set Symbol
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedersymOf sigma =
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder    let classes = Map.foldWithKey ( \ i ks s ->
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder            Set.insert (Symbol i $ ClassAsItemType $
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder                    Intersection (classKinds ks) []) s)
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder          Set.empty $ classMap sigma
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder    types = Map.foldWithKey ( \ i ti s ->
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder            Set.insert (Symbol i $ TypeAsItemType $
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder                    typeKind ti) s)
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder        classes $ typeMap sigma
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder        ops = Map.foldWithKey ( \ i ts s0 ->
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder              foldr ( \ t s1 ->
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder              Set.insert (Symbol i $ OpAsItemType $
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder                      opType t) s1) s0 $ opInfos ts)
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder          types $ assumps sigma
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder    in ops
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbMapItems :: [SymbMapItems] -> Result (Map.Map RawSymbol RawSymbol)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbMapItems sl =  return (Map.fromList $ concat $ map s1 sl)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder  where
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder  s1 (SymbMapItems kind l _ _) = map (symbOrMapToRaw kind) l
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbOrMapToRaw :: SymbKind -> SymbOrMap -> (RawSymbol,RawSymbol)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbOrMapToRaw k (SymbOrMap s mt _) =
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder    (symbToRaw k s,
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder     symbToRaw k $ case mt of Nothing -> s
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder                              Just t -> t)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbItems :: [SymbItems] -> Result [RawSymbol]
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederstatSymbItems sl =
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder  return (concat (map s1 sl))
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder  where s1 (SymbItems kind l _ _) = map (symbToRaw kind) l
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbToRaw :: SymbKind -> Symb -> RawSymbol
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbToRaw k (Symb idt _ _)     = symbKindToRaw k idt
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbKindToRaw :: SymbKind -> Id -> RawSymbol
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbKindToRaw Implicit     idt = AnID idt
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedersymbKindToRaw sk idt = AKindedId sk idt
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedermatchSymb :: Symbol -> RawSymbol -> Bool
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb x                               (ASymbol y)            =  x==y
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt _)                  (AnID di)              = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt (TypeAsItemType _)) (AKindedId SK_type di) = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt (TypeAsItemType _)) (AKindedId SK_sort di) = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt (OpAsItemType _))   (AKindedId SK_op di)   = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb (Symbol idt (OpAsItemType _))   (AKindedId SK_pred di) = idt==di
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermatchSymb _                               _                      = False
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederrawSymName :: RawSymbol -> Id
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederrawSymName (ASymbol sym) = symName sym
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederrawSymName (AnID i) = i
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederrawSymName (AKindedId _ i) = i
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maedertype IdMap = Map.Map Id Id
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapType :: IdMap -> Type -> Type
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- include classIdMap later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapType m t = case t of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder       TypeName i k n ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder           if n == 0 then
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder          case Map.lookup i m of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder          Just j -> TypeName j k 0
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder          _ -> t
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder           else t
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder       TypeAppl t1 t2 ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder           TypeAppl (mapType m t1) (mapType m t2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder       TypeToken _ -> t
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder       BracketType b l ps ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder           BracketType b (map (mapType m) l) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder       KindedType tk k ps ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder           KindedType (mapType m tk) k ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder       MixfixType l -> MixfixType $ map (mapType m) l
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder       LazyType tl ps -> LazyType (mapType m tl) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder       ProductType l ps -> ProductType (map (mapType m) l) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder           FunType t1 a t2 ps -> FunType (mapType m t1) a (mapType m t2) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme :: IdMap -> TypeScheme -> TypeScheme
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- rename clashing type arguments later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme m (TypeScheme args (q :=> t) ps) =
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    TypeScheme args (q :=> mapType m t) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maedertype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> Maybe (Id, TypeScheme)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapFunSym tm fm (i, sc) = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  (newI, _sc1) <- Map.lookup (i, sc) fm
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  let sc2 = mapTypeScheme tm sc
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder      -- unify sc2 with sc1 later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  return (newI, sc2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maederdata Morphism = Morphism { msource :: Env
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             , mtarget :: Env
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             , classIdMap :: IdMap  -- ignore
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             , typeIdMap :: IdMap
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                         , funMap :: FunMap }
62599a910de0701b0f9461e534a43d5900131c55Christian Maeder                         deriving (Eq, Show, Typeable)
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaedermkMorphism :: Env -> Env -> Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaederideMor :: Env -> Morphism
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederideMor e = (mkMorphism e e)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder       { typeIdMap = Map.foldWithKey ( \ i _ m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder                Map.insert i i m) Map.empty $ typeMap e
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder       , funMap = Map.foldWithKey ( \ i ts m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder              foldr ( \ t m2 -> let v = (i, opType t) in
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder                  Map.insert v v m2) m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder                    $ opInfos ts) Map.empty
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder                                        $ assumps e
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder       }
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor :: Morphism -> Morphism -> Maybe Morphism
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor m1 m2 =
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder  if mtarget m1 == msource m2 then Just
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder      (mkMorphism (msource m1) (mtarget m2))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder      { typeIdMap = Map.map ( \ i -> Map.findWithDefault i i $ typeIdMap m2)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder                 $ typeIdMap m1
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder      , funMap = Map.foldWithKey ( \ (i1, sc1) (i2, sc2) m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder               Map.insert (i1, sc1)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder               (Map.findWithDefault (i2, sc2) (i2, sc2) $
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder            funMap m2) m) Map.empty $ funMap m1
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder      }
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder   else Nothing
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederisSubEnv :: Env -> Env -> Bool
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederisSubEnv e1 e2 = diffEnv e1 e2 == initialEnv
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiinclusionMor :: Env -> Env -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinclusionMor e1 e2 =
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder  if isSubEnv e1 e2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder     then return (embedMorphism e1 e2)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder     else pplain_error (embedMorphism initialEnv initialEnv)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder          (ptext "Attempt to construct inclusion between non-subsignatures:"
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder           $$ ptext "Singature 1:" $$ printText e1
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder           $$ ptext "Singature 2:" $$ printText e2)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder           nullPos
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederembedMorphism :: Env -> Env -> Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederembedMorphism a b =
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    (mkMorphism a b)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    { typeIdMap = foldr (\x -> Map.insert x x) Map.empty
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                $ Map.keys $ typeMap a
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    , funMap = Map.foldWithKey
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                 ( \ i (OpInfos ts) m -> foldr
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                      (\ oi -> let t = opType oi in
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                   Map.insert (i,t) (i, t)) m ts)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                 Map.empty $ assumps a
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    }
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedersymbMapToMorphism :: Env -> Env -> SymbolMap -> Result Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedersymbMapToMorphism sigma1 sigma2 smap = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  type_map1 <- Map.foldWithKey myIdMap (return Map.empty) $ typeMap sigma1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  fun_map1 <- Map.foldWithKey myAsMap (return Map.empty) $ assumps sigma1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  return (mkMorphism sigma1 sigma2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder     { typeIdMap = type_map1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder     , funMap = fun_map1}
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  where
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  myIdMap i k m = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    m1 <- m
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    sym <- maybeToResult nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             ("symbMapToMorphism - Could not map sort "++showId i "")
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             $ Map.lookup (Symbol { symName = i
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                  , symbType = TypeAsItemType
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                               $ typeKind k}) smap
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    return (Map.insert i (symName sym) m1)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  myAsMap i (OpInfos ots) m = foldr (insFun i) m ots
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder  insFun i ot m = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    m1 <- m
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    sym <- maybeToResult nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             ("symbMapToMorphism - Could not map op "++showId i "")
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder             $ Map.lookup (Symbol { symName = i
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder                  , symbType = OpAsItemType $ opType ot}) smap
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    k <- case symbType sym of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder        OpAsItemType sc -> return sc
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder        _ -> plain_error (opType ot)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder              ("symbMapToMorphism - Wrong result symbol type for op"
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder               ++showId i "") nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder    return (Map.insert (i, opType ot) (symName sym,k) m1)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv :: Env -> Bool
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv _ = True -- maybe a closure test?
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalMor :: Morphism -> Bool
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederlegalMor m = let s = msource m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         t = mtarget m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         ts = typeIdMap m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         fs = funMap m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         in
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         all (`elem` (Map.keys $ typeMap s))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder          (Map.keys ts)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         && all (`elem` (Map.keys $ typeMap t))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder        (Map.elems ts)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         && all ((`elem` (Map.keys $ assumps s)) . fst)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder        (Map.keys fs)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         && all ((`elem` (Map.keys $ assumps t)) . fst)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder        (Map.elems fs)
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermorphismUnion m1 m2 =
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder    do s <- merge (msource m1) $ msource m2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder       t <- merge (mtarget m1) $ mtarget m2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder       return (mkMorphism s t)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder          { typeIdMap = Map.union (typeIdMap m1) $ typeIdMap m2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder          , funMap = Map.union (funMap m1) $ funMap m2 }
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
997c56f3bc74a703043010978e5013fdb074d659Christian MaedermorphismToSymbMap :: Morphism -> Map.Map Symbol Symbol
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermorphismToSymbMap mor =
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder  let
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder    tm = typeMap $ msource mor
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder    typeSymMap =
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder      Map.foldWithKey
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         ( \ s1 s2 m -> let k = typeKind $
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder                            Map.findWithDefault starTypeInfo s1 tm
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder       in Map.insert (idToTypeSymbol s1 k) (idToTypeSymbol s2 k) m)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         Map.empty $
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         typeIdMap mor
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder   in Map.foldWithKey
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         ( \ (id1,t1) (id2,t2) m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder             Map.insert (idToOpSymbol id1 t1)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder                        (idToOpSymbol id2 t2) m)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder         typeSymMap $ funMap mor
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- | Check if two OpTypes are equal except from totality or partiality
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedercompatibleOpTypes :: TypeScheme -> TypeScheme -> Bool
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedercompatibleOpTypes = isUnifiable Map.empty 0
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- Some quick and dirty instances
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiinstance PrettyPrint Morphism where
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder  printText0 _ga s = text (show s)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint Symbol where
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder  printText0 ga s = text (case symbType s of
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder              OpAsItemType _ -> opS
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder              TypeAsItemType _ -> typeS
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder              ClassAsItemType _ -> classS) <+>
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder                    printText0 ga (symName s) <+> text colonS <+>
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder            printText0 ga (symbType s)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint RawSymbol where
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder  printText0 _ga s = text (show s)