Hs2HOLCF.hs revision 13ed13e06a5dd4aad12044ed7e7503cbe7f62990
18c2aff776a775d34a4c9893a4c72e0434d68e36artemModule : $Header$
18c2aff776a775d34a4c9893a4c72e0434d68e36artemCopyright : (c) Paolo Torrini and Till Mossakowski and Uni Bremen 2004-2005
18c2aff776a775d34a4c9893a4c72e0434d68e36artemLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
18c2aff776a775d34a4c9893a4c72e0434d68e36artemMaintainer : paolot@tzi.de
18c2aff776a775d34a4c9893a4c72e0434d68e36artemStability : provisional
18c2aff776a775d34a4c9893a4c72e0434d68e36artemPortability : non-portable (imports Logic.Logic)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemThe embedding comorphism from Haskell to Isabelle-HOLCF.
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport qualified Common.Lib.Map as Map
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Common.Result as Result
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Comorphisms.Hs2HOLCFaux as Hs2HOLCFaux
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Haskell.HatParser as HatParser hiding (HsType)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Haskell.HatAna as HatAna
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- Programatica
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsTypeStruct
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsKindStruct
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsTypeMaps
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsName
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsIdent
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TypedIds
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport OrigTiMonad
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TiTypes
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TiKinds
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TiInstanceDB -- as TiInst
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TiTEnv
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TiKEnv
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TiEnvFM
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport PosName
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport UniqueNames
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport PropSyntaxRec
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsExpStruct
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsPatStruct
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsExpMaps
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsPatMaps
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport SyntaxRec
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TiPropDecorate
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport PropSyntaxStruct
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsDeclStruct
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport HsGuardsStruct
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport TiDecorate
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Isabelle.IsaSign as IsaSign
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Isabelle.IsaConsts as IsaConsts
18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Isabelle.Translate as Translate
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------ Top level function ------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransTheory ::
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HatAna.Sign -> [Named PrDecl] -> Result (IsaSign.Sign, [Named IsaSign.Sentence])
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransTheory sign sens = do
18c2aff776a775d34a4c9893a4c72e0434d68e36artem sign' <- transSignature sign
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (sign'',sens'') <- -- trace (show $ arities $ tsig sign') $
18c2aff776a775d34a4c9893a4c72e0434d68e36artem transSentences sign' (map sentence sens)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return (sign'', sens'')
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------ Theory translation -------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artem{- Relevant theories in Programatica: base/Ti/TiClasses (for
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtcTopDecls); property/parse2/Parse/PropPosSyntax (def of HsDecl). -}
18c2aff776a775d34a4c9893a4c72e0434d68e36artemdata ExpRole = FunDef | InstDef
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransSentences ::
18c2aff776a775d34a4c9893a4c72e0434d68e36artem IsaSign.Sign -> [PrDecl] -> Result (IsaSign.Sign, [Named IsaSign.Sentence])
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransSentences sign ls = do xx <- mapM (transSentence sign FunDef) ls
18c2aff776a775d34a4c9893a4c72e0434d68e36artem xs <- return [[s] | [s] <- xx, extAxType s /= noType]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem ys <- -- trace ("\n" ++ (show xs)) $
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ fixMRec xs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem zz <- mapM (transSentence sign InstDef) ls
18c2aff776a775d34a4c9893a4c72e0434d68e36artem zw <- return $ concat zz
18c2aff776a775d34a4c9893a4c72e0434d68e36artem zs <- return [s | s <- zw, extAxType s /= noType]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return (sign, ys ++ zs)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransSentence :: IsaSign.Sign -> ExpRole -> PrDecl -> Result [Named IsaSign.Sentence]
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransSentence sign a (TiPropDecorate.Dec d) = case d of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem PropSyntaxStruct.Base p -> case (a,p) of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (FunDef, HsDeclStruct.HsFunBind _ [x]) -> do
18c2aff776a775d34a4c9893a4c72e0434d68e36artem k <- transMatch sign x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (InstDef, HsInstDecl _ _ _ t (TiPropDecorate.Decs ds _)) -> do
18c2aff776a775d34a4c9893a4c72e0434d68e36artem q <- mapM (transIMatch sign t)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem [y | TiPropDecorate.Dec (PropSyntaxStruct.Base (HsDeclStruct.HsFunBind _ [y])) <- ds]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> return []
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> return []
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmakeSentence :: String -> ConstTab -> IsaType -> VName -> [PrPat] -> IsaTerm -> Named Sentence
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmakeSentence d cs y df ps tx =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem if tx == xDummy then NamedSen d True False $ ConstDef $ IsaEq xDummy $ xDummy
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else NamedSen d True False $ ConstDef $
18c2aff776a775d34a4c9893a4c72e0434d68e36artem IsaEq (Const df y) $ termMAbs IsCont (map (transPat cs) ps) tx
18c2aff776a775d34a4c9893a4c72e0434d68e36artem--------------------------- translation of sentences --------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artem---------------------------- function definitions ---------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMatch :: IsaSign.Sign -> HsDeclStruct.HsMatchI PNT PrExp PrPat ds
18c2aff776a775d34a4c9893a4c72e0434d68e36artem -> Result (Named Sentence)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMatch sign t = case (t, constTab sign) of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (HsDeclStruct.HsMatch _ nm ps (HsGuardsStruct.HsBody x) _,
18c2aff776a775d34a4c9893a4c72e0434d68e36artem let df = mkVName $ showIsaName nm
18c2aff776a775d34a4c9893a4c72e0434d68e36artem tx = transExp cs x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem y = maybe (noType) id $ Map.lookup df cs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem in return $ makeSentence (IsaSign.orig df) cs y df ps tx
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> fail "Haskell2IsabelleHOLCF.transMatch, case not supported"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------- translates instances ---------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransIMatch :: IsaSign.Sign -> HsType -> HsDeclStruct.HsMatchI PNT PrExp PrPat ds
18c2aff776a775d34a4c9893a4c72e0434d68e36artem -> Result (Named Sentence)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransIMatch sign t s
18c2aff776a775d34a4c9893a4c72e0434d68e36artem = case (s, constTab sign) of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (HsDeclStruct.HsMatch _ nm ps (HsGuardsStruct.HsBody ex) _,
18c2aff776a775d34a4c9893a4c72e0434d68e36artem let tx = transExp ct ex
18c2aff776a775d34a4c9893a4c72e0434d68e36artem df = mkVName $ showIsaName nm
18c2aff776a775d34a4c9893a4c72e0434d68e36artem c = transClass $ getInstClass t -- instantiated class
18c2aff776a775d34a4c9893a4c72e0434d68e36artem x = transType [] $ getInstType t -- instatiating type
18c2aff776a775d34a4c9893a4c72e0434d68e36artem w = maybe [] id $ Map.lookup (typeId x) (arities $ tsig sign) -- all arities of inst. type
18c2aff776a775d34a4c9893a4c72e0434d68e36artem cs = maybe [] id $ Map.lookup c (Map.fromList w) -- selects the arity for the inst. class
18c2aff776a775d34a4c9893a4c72e0434d68e36artem ndf = typeId x ++ "_" ++ IsaSign.orig df
18c2aff776a775d34a4c9893a4c72e0434d68e36artem ty = maybe (noType) id $ Map.lookup df ct -- abstract method type
18c2aff776a775d34a4c9893a4c72e0434d68e36artem nty = repVarClass ty c (constrVarClass x cs) -- in ty, replaces the variable of class c with type x, constraining variables in x with cs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem in return $ makeSentence ndf ct nty df ps tx
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> fail "Haskell2IsabelleHOLCF.transIMatch, case not supported"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------ Signature translation -----------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransSignature sign = Result [] $ Just $ IsaSign.emptySign
18c2aff776a775d34a4c9893a4c72e0434d68e36artem { baseSig = HsHOLCF_thy,
18c2aff776a775d34a4c9893a4c72e0434d68e36artem tsig = emptyTypeSig
18c2aff776a775d34a4c9893a4c72e0434d68e36artem classrel = getClassrel (HatAna.types sign),
18c2aff776a775d34a4c9893a4c72e0434d68e36artem abbrs = getAbbrs (HatAna.types sign),
18c2aff776a775d34a4c9893a4c72e0434d68e36artem arities = -- trace (show (HatAna.instances sign)) $
18c2aff776a775d34a4c9893a4c72e0434d68e36artem getArities (HatAna.instances sign)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem constTab = getConstTab (HatAna.values sign),
18c2aff776a775d34a4c9893a4c72e0434d68e36artem domainTab = getDomainTab (HatAna.values sign)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------ translation of types -------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artem{- This signature translation takes after the one to Stratego, and relies on
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Isabelle.Translation to solve naming conflicts. -}
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransType :: [HsType] -> HsType -> IsaType
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransType c t = maybe noType id $ transMType IsCont c t
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMType :: Continuity -> [HsType] -> HsType -> Maybe IsaType
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMType a c (Typ t) = transT (transIdV a c) transIdC (transMType a c) t
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransT :: Show d => (PNT -> Maybe IsaType) -> (PNT -> Maybe IsaType) -> (d -> Maybe IsaType) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsTypeStruct.TI PNT d -> Maybe IsaType
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransT trIdV trIdC trT t =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem case mapTI3 trIdV trIdC trT t of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsTyFun t1 t2) -> return $ IsaSign.mkContFun t1 t2
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsTyApp t1 t2) -> return $ IsaSign.typeAppl t1 [t2]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsTyVar a) -> return a
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsTyCon k) -> return k
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- _ -> not_supported "Type" t
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetSort :: Continuity -> [HsType] -> PNT -> IsaSort
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetSort r c t = case c of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem [] -> case r of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem NotCont -> [isaTerm]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem x:cs -> let a = getInstType x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem b = getInstClass x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem d = getLitName a
18c2aff776a775d34a4c9893a4c72e0434d68e36artem s = getSort r cs t
18c2aff776a775d34a4c9893a4c72e0434d68e36artem k = transClass b
18c2aff776a775d34a4c9893a4c72e0434d68e36artem u = showIsaName d
18c2aff776a775d34a4c9893a4c72e0434d68e36artem v = showIsaName t
18c2aff776a775d34a4c9893a4c72e0434d68e36artem in if u == v then k:s else s
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- in if u == v && k /= IsaClass "Eq" && k /= IsaClass "Ord" then k:s else s
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransIdV :: Continuity -> [HsType] -> PNT -> Maybe IsaType
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransIdV a c t = return $ TFree (showIsaName t) (getSort a c t)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransIdC :: PNT -> Maybe IsaType
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransIdC t = case t of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem PNT _ (TypedIds.Class _ _) _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> return $ let tfs = transFields t
18c2aff776a775d34a4c9893a4c72e0434d68e36artem UniqueNames.G (PlainModule m) n _ ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem UniqueNames.G (MainModule m) n _ ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransFields :: PNT -> [IsaType]
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransFields t = case t of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem PNT _ (TypedIds.Type q) _ ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem [TFree (showIsaS x) IsaSign.dom | (PN x _) <- TypedIds.fields q]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem PNT _ (TypedIds.FieldOf _ q) _ ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem [TFree (showIsaS x) IsaSign.dom | (PN x _) <- TypedIds.fields q]
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmapTI3 :: (i1 -> Maybe i2) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (i1 -> Maybe i2) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (t1 -> Maybe t2) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TI i1 t1 -> Maybe (TI i2 t2)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmapTI3 vf cf tf ty = case ty of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsTyFun x y -> do a <- tf x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsTyFun a b
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsTyApp f x -> do a <- tf f
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsTyApp a b
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsTyVar nm -> do a <- vf nm
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsTyVar a
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsTyCon nm -> do a <- cf nm
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsTyCon a
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsTyForall xs ps t -> HsTyForall (map vf xs) (map tf ps) (tf t)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- error :: forall a. [Char] -> a
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- not_supported :: (Show t, Show i) => String -> HsTypeStruct.TI i t -> a
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- not_supported s x = error $ s++" Haskell2IsabelleHOLCF.transT, type not supported: "++show x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------ Class translation ------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmkIsaClass :: CName -> IsaClass
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmkIsaClass n = IsaClass n
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransClass :: HsType -> IsaClass
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransClass x = case x of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Typ (HsTyCon c) -> IsaClass (showIsaName c)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Typ _ -> error "Hs2HOLCF.transClass"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- need check of parameters?
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------- Kind translation ------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemkindTrans :: Kind -> IsaKind
18c2aff776a775d34a4c9893a4c72e0434d68e36artemkindTrans x = case x of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem K (HsKindStruct.Kfun a b) -> IsaSign.Kfun (kindTrans a) (kindTrans b)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> error "error, Hs2HOLCF.kindTrans,"
18c2aff776a775d34a4c9893a4c72e0434d68e36artemkindExTrans :: Kind -> IsaExKind
18c2aff776a775d34a4c9893a4c72e0434d68e36artemkindExTrans x = case x of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem K (HsKindStruct.Kfun a b) -> IKind (IsaSign.Kfun (kindTrans a) (kindTrans b))
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> error "Hs2HOLCF.kindExTrans, kind variables not supported"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------- SIGN fields translation ---------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------- translation for ConstTab --------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetConstTab :: VaMap -> ConstTab
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetConstTab f = Map.map fst (Map.filter (\x -> (snd x) == IsaVal) (getAConstTab f))
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetAConstTab :: VaMap -> AConstTab
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetAConstTab f =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem liftMapByListD Map.toList Map.fromList (mkVName . showIsaName . fst)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (\y -> (transMScheme IsCont $ snd y, getValInfo $ fst y)) nothingFiOut f
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetValInfo :: HsId -> IsaVT
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetValInfo n = case n of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsCon _ -> IsaConst
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> IsaVal
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMScheme :: Continuity -> HsScheme -> Maybe IsaType
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMScheme a s = case s of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Forall _ _ (c TiTypes.:=> t) -> transMType a c t
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransScheme :: HsScheme -> IsaType
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransScheme s = maybe (error "HsHOLCF, transScheme") id $ transMScheme IsCont s
18c2aff776a775d34a4c9893a4c72e0434d68e36artem----------------------------- translation for Classrel (from KEnv) -----------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetClassrel :: TyMap -> IsaSign.Classrel
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetClassrel f =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem liftMapByList Map.toList Map.fromList (mkIsaClass . showIsaName) transClassInfo f
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransClassInfo :: (Kind, HsTypeInfo) -> Maybe [IsaClass]
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransClassInfo p = case snd p of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TiTypes.Class _ _ _ _ -> Just (map transClass (extClassInfo $ snd p))
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------- translation of Abbrs (from KEnv) -----------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetAbbrs :: TyMap -> IsaSign.Abbrs
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetAbbrs f = let
18c2aff776a775d34a4c9893a4c72e0434d68e36artem mf = liftMapByList Map.toList Map.fromList showIsaName transAbbrsInfo f
18c2aff776a775d34a4c9893a4c72e0434d68e36artem nf = Map.filter (\x -> case x of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just _ -> True
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Nothing -> False) mf
18c2aff776a775d34a4c9893a4c72e0434d68e36artem in Map.map (\x -> maybe ([],noType) id x) nf
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransAbbrsInfo :: (Kind, HsTypeInfo) -> Maybe ([TName], IsaType)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransAbbrsInfo p = case (snd p) of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TiTypes.Synonym _ _ -> let x = extAbbrsInfo (snd p) in
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ (map showIsaName (fst x), transType [] (snd x))
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artem---------------------------- translation of arities --------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetArities :: HsInstances -> IsaSign.Arities
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetArities db = -- trace (show $ getTypeInsts db) $ trace (show db) $
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Map.fromList (groupInst $ getTypeInsts db) -- \$ getIsaInsts db
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetTypeInsts :: HsInstances -> [IsaTypeInsts]
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetTypeInsts db = [(typeId $ transType [] $ getMainInstType x, [transInst x]) | x <- db]
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransInst :: HsInstance -> (IsaClass, [(IsaType, [IsaClass])])
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransInst i = let x = prepInst i in
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (transClass $ fst x, reverse [(transType [] a, map transClass b) | (a,b) <- snd x])
18c2aff776a775d34a4c9893a4c72e0434d68e36artem------------------------------ translation of domaintab ---------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetDomainTab :: VaMap -> IsaSign.DomainTab
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetDomainTab f =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem getDepDoms $ remove_duplicates
18c2aff776a775d34a4c9893a4c72e0434d68e36artem [getDomainEntry (getAConstTab f) x | x <- Map.keys f, checkTyCons x]
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetDomainEntry :: AConstTab -> HsId -> [IsaSign.DomainEntry]
18c2aff776a775d34a4c9893a4c72e0434d68e36artemgetDomainEntry ctab t = case t of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsCon (PNT _ (TypedIds.ConstrOf _ d) _) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem [(getDomType ctab (mkVName $ showIsaName t), [(b, getFieldTypes ctab b)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem | b <- [ mkVName $ showIsaName c
18c2aff776a775d34a4c9893a4c72e0434d68e36artem | PN c _ <- map conName (constructors d)]])]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem--------------------------------- Term translation -------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-------------------------------------------- term and patterns ------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransExp :: ConstTab -> PrExp -> IsaTerm
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransExp c t = maybe xDummy id $ transMExp IsCont c t
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransPat :: ConstTab -> PrPat -> IsaPattern
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransPat c t = maybe xDummy id $ transMPat IsCont c t
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMExp :: Continuity -> ConstTab -> PrExp -> Maybe IsaTerm
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMExp a cs t = case t of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (TiPropDecorate.Exp e) -> case e of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsLit _ (HsInt n) -> return $
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Const (mkVName $ "(Def (" ++ show n ++ "::int))")
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (IsaSign.Type "dInt" [] [])
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsList xs -> return $ case xs of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem [] -> conDouble "lNil"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> error "Hs2HOLCF, transMExp, unsupported list notation"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsLet (TiPropDecorate.Decs ds _) k -> do
18c2aff776a775d34a4c9893a4c72e0434d68e36artem w <- mapM (transPatBind a cs) ds
18c2aff776a775d34a4c9893a4c72e0434d68e36artem z <- transMExp a cs k
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ Let w z -- (transE showIsaName (transExp cs) (transPat cs) e)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsCase e as -> do bs <- mapM (transCases a cs) as
18c2aff776a775d34a4c9893a4c72e0434d68e36artem e1 <- transMExp a cs e
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ Case e1 bs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> transE (mkVName . showIsaName) (transMExp a cs) (transMPat a cs) e
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TiPropDecorate.TiSpec w s _ -> case w of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsVar x -> transHV a s x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsCon x -> transCN s x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TiPropDecorate.TiTyped x _ -> transMExp a cs x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artem transCases r cs k = case k of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsAlt _ p (HsBody e) _ -> do a <- transMPat r cs p
18c2aff776a775d34a4c9893a4c72e0434d68e36artem b <- transMExp r cs e
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ (a,b)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> error "HsHOLCF, transCases"
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransPatBind :: Continuity -> ConstTab -> PrDecl -> Maybe (IsaTerm,IsaTerm)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransPatBind a cs s = case s of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (HsDeclStruct.HsPatBind _ p (HsGuardsStruct.HsBody e) _)) -> do
18c2aff776a775d34a4c9893a4c72e0434d68e36artem x <- transMPat a cs p
18c2aff776a775d34a4c9893a4c72e0434d68e36artem y <- transMExp a cs e
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return (x, y)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> error "HsHOLCF, transPatBind"
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMPat :: Continuity -> ConstTab -> PrPat -> Maybe IsaPattern
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransMPat a cs t = case t of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TiDecorate.Pat p -> case p of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPList _ xs -> return $ case xs of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem [] -> conDouble "lNil"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> error "Hs2HOLCF, transMPat, unsupported list notation"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> transP a (mkVName . showIsaName) (transMPat a cs) p
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TiDecorate.TiPSpec w s _ -> case w of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsVar x -> transHV a s x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsCon x -> transCN s x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TiDecorate.TiPTyped x _ -> transMPat a cs x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem TiDecorate.TiPApp w z -> do w1 <- transMPat a cs w
18c2aff776a775d34a4c9893a4c72e0434d68e36artem z1 <- transMPat a cs z
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ (App w1 z1 a)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- _ -> error "oh so funny" -- return $ Bottom
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransE :: (PNT -> VName) -> (e -> Maybe IsaTerm) -> (p -> Maybe IsaPattern) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (HsExpStruct.EI PNT e p j h k) -> Maybe IsaTerm
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransE trId trE trP e =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem case (mapEI5 trId trE trP e) of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsId (HsVar _)) -> return $ conDouble "DIC"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsApp x y) -> return $ termMAppl IsCont x [y]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsLambda ps x) -> return $ termMAbs IsCont ps x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsIf x y z) -> return $ If x y z IsCont
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsTuple xs) -> return $ Tuplex xs IsCont
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsParen x) -> return $ Paren x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing -- Const "dummy" noType
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- _ -> error "Haskell2IsabelleHOLCF.transE, not supported"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsId (HsCon c) -> Const c noType
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsId (HsVar "==") -> Const "Eq" noType
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsLet ds e -> Let (map transPatBind ds) (transExp e)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsCase e ds -> Case e ds
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransP :: IsaName i => Continuity -> (i -> VName) -> (p -> Maybe IsaPattern) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (HsPatStruct.PI i p) -> Maybe IsaPattern
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransP a trId trP p =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem case mapPI3 trId trP p of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsPId (HsVar _)) -> return $ conDouble "DIC"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsPTuple _ xs) -> return $ Tuplex xs a
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just (HsPParen x) -> return $ Paren x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Just HsPWildCard -> return $ Wildcard
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing -- error "Haskell2IsabelleHOLCF.transP, not supported"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPList ps -> plist ps
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPId (HsCon c) -> Const c noType
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPLit _ lit -> litPat (transL lit) -- new
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPApp c ps -> App x y IsCont
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPAsPat x p -> AsPattern (x,p)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPIrrPat p -> twiddlePat p
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransCN :: HsScheme -> PNT -> Maybe IsaTerm
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransCN s x = let
18c2aff776a775d34a4c9893a4c72e0434d68e36artem y = showIsaName x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem z = transScheme s
18c2aff776a775d34a4c9893a4c72e0434d68e36artem f w = Const (mkVName w) z
18c2aff776a775d34a4c9893a4c72e0434d68e36artem in return $
18c2aff776a775d34a4c9893a4c72e0434d68e36artem if elem pcpo (typeSort z) then case pp x of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "True" -> f "TT"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "False" -> f "FF"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem ":" -> f "lCons"
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransHV :: Continuity -> HsScheme -> PNT -> Maybe IsaTerm
18c2aff776a775d34a4c9893a4c72e0434d68e36artemtransHV a s x = let
18c2aff776a775d34a4c9893a4c72e0434d68e36artem n = showIsaName x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem k = maybe (error "Hs2HOLCF, transHV") id $ transMScheme a s
18c2aff776a775d34a4c9893a4c72e0434d68e36artem tag = elem pcpo (typeSort k)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem mkConst w = Const (mkVName w) k
18c2aff776a775d34a4c9893a4c72e0434d68e36artem mkFree w = Free (mkVName w) k
18c2aff776a775d34a4c9893a4c72e0434d68e36artem mFree w = Free (mkVName w) noType
18c2aff776a775d34a4c9893a4c72e0434d68e36artem flist = [mFree "x", mFree "y"]
18c2aff776a775d34a4c9893a4c72e0434d68e36artem in if qq == "error" then Nothing else return $
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "==" -> if tag == False then mkConst eq
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (termMAbs IsCont flist
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (termLift $ termMAppl NotCont (mkConst eq)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "&&" -> if tag == False then mkConst conj
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else mkConst "trand"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "||" -> if tag == False then mkConst disj
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else mkConst "tror"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "+" -> if tag == False then mkConst "op +"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else funFliftbin $ mkConst "op +"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "-" -> if tag == False then mkConst "op -"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else funFliftbin $ mkConst "op -"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "*" -> if tag == False then mkConst "op *"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else funFliftbin $ mkConst "op *"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "head" -> if tag == False then mkConst "hd"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else mkConst "lHd"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem "tail" -> if tag == False then mkConst "tl"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else mkConst "lTl"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem ":" -> if tag == False then mkConst "op #"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem else mkConst "lCons"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> case x of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem PNT (PN _ (UniqueNames.G _ _ _)) _ _ -> mkConst n
18c2aff776a775d34a4c9893a4c72e0434d68e36artem PNT (PN _ (UniqueNames.S _)) _ _ -> mkFree n
18c2aff776a775d34a4c9893a4c72e0434d68e36artem PNT (PN _ (UniqueNames.Sn _ _)) _ _ -> mkFree n
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> error "Haskell2IsabelleHOLCF, transHV"
18c2aff776a775d34a4c9893a4c72e0434d68e36artem---------------------------------- auxiliary ------------------------------------------------
18c2aff776a775d34a4c9893a4c72e0434d68e36artemclass IsaName i => TransFunction i j k where
18c2aff776a775d34a4c9893a4c72e0434d68e36artem transFun :: (j i) -> k
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmapEI5 :: (i1 -> i2) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (e1 -> Maybe e2) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (p1 -> Maybe p2) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem EI i1 e1 p1 d t c ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem Maybe (EI i2 e2 p2 d t c)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmapEI5 vf ef pf exp =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem case exp of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsId n -> return $ HsId (HsIdent.mapHsIdent2 vf vf n)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsApp x y -> do a <- ef x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsApp a b
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsLambda ps e -> do xs <- mapM pf ps
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsLambda xs y
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsIf x y z -> do a <- ef x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsIf a b c
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsTuple xs -> do zs <- mapM ef xs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsTuple zs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsParen x -> do a <- ef x
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsParen a
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsList xs -> do ys <- mapM ef xs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsList ys
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsLit s l -> HsLit s l
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsCase e as -> do f <- ef e
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- bs <- map (mapA ef pf) as
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- return $ HsCase f bs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- mapA f g k = case k of HsAlt _ p (HsBody e) _ ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsLit s l -> HsLit s l
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsInfixApp x op z -> HsInfixApp (ef x) (mapHsIdent2 vf cf op) (ef z)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsNegApp s x -> HsNegApp s (ef x)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsLet ds e -> HsLet (df ds) (ef e)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsCase e alts -> HsCase (ef e) (map (mapAlt ef pf df) alts)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsDo stmts -> HsDo (mStmt stmts)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsLeftSection x op -> HsLeftSection (ef x) (mapHsIdent2 vf cf op)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsRightSection op y -> HsRightSection (mapHsIdent2 vf cf op) (ef y)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsRecConstr s n upds -> HsRecConstr s (cf n) (mapFieldsI vf ef upds)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsRecUpdate s e upds -> HsRecUpdate s (ef e) (mapFieldsI vf ef upds)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsEnumFrom x -> HsEnumFrom (ef x)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsEnumFromTo x y -> HsEnumFromTo (ef x) (ef y)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsEnumFromThen x y -> HsEnumFromThen (ef x) (ef y)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsEnumFromThenTo x y z -> HsEnumFromThenTo (ef x) (ef y) (ef z)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsListComp stmts -> HsListComp (mStmt stmts)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsExpTypeSig s e c t -> HsExpTypeSig s (ef e) (ctxf c) (tf t)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsAsPat n e -> HsAsPat (vf n) (ef e) -- pattern only
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsWildCard -> HsWildCard -- ditto
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsIrrPat e -> HsIrrPat (ef e) -- ditto
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- mStmt = mapStmt ef pf df
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmapPI3 :: (i1 -> i2) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem (p1 -> Maybe p2) ->
18c2aff776a775d34a4c9893a4c72e0434d68e36artem PI i1 p1 -> Maybe (PI i2 p2)
18c2aff776a775d34a4c9893a4c72e0434d68e36artemmapPI3 vf pf pat =
18c2aff776a775d34a4c9893a4c72e0434d68e36artem case pat of
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPId n -> return $ HsPId (HsIdent.mapHsIdent2 vf vf n)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPLit s l -> return $ HsPLit s l
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPTuple s ps -> do bs <- mapM pf ps
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsPTuple s bs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPParen p -> do h <- pf p
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsPParen h
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPWildCard -> return $ HsPWildCard
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPList s ps -> do qs <- mapM pf ps
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsPList s qs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPApp nm ps -> do qs <- mapM pf ps
18c2aff776a775d34a4c9893a4c72e0434d68e36artem return $ HsPApp (vf nm) qs
18c2aff776a775d34a4c9893a4c72e0434d68e36artem HsPSucc s n l -> return $ HsPSucc s (vf n) l
18c2aff776a775d34a4c9893a4c72e0434d68e36artem _ -> Nothing
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPNeg s l -> HsPNeg s l
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPNeg s l -> HsPNeg s l
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPSucc s n l -> HsPSucc s (vf n) l
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPInfixApp x op y -> HsPInfixApp (pf x) (cf op) (pf y)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPApp nm ps -> HsPApp (cf nm) (map pf ps)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPList s ps -> HsPList s (map pf ps)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPRec nm fields -> HsPRec (cf nm) (mapFieldsI vf pf fields)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPAsPat nm p -> HsPAsPat (vf nm) (pf p)
18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- HsPIrrPat p -> HsPIrrPat (pf p)