{- |

Module : $Header: /repository/HetCATS/Comorphisms/Hs2HOLCF.hs,v 1.42 2007/05/25 10:49:58 paolot Exp $

Description : theory translation for the embedding comorphism from Haskell to Isabelle

Copyright : (c) Paolo Torrini and Till Mossakowski and Uni Bremen 2004-2005

License : GPLv2 or higher, see LICENSE.txt

Maintainer : paolot@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (depends on programatica using MPTC)

theory translation for the embedding comorphism from Haskell to Isabelle.

-}

module Comorphisms.Hs2HOLCF (transTheory) where

import qualified Data.Map as Map

import Data.Maybe (catMaybes, fromMaybe)

import Common.Utils (number)

import Common.Result

import Common.AS_Annotation

import Comorphisms.Hs2HOLCFaux

-- Haskell

import Haskell.HatAna as HatAna

-- Programatica

import NewPrettyPrint (pp)

import TypedIds

import TiTypes

import PNT

import UniqueNames

import TiPropDecorate

import PropSyntaxStruct

import HsDeclStruct

import HsGuardsStruct

import TiDecorate

-- Isabelle

import Isabelle.IsaSign as IsaSign

import Isabelle.IsaConsts

import Debug.Trace

-- ---------------------------- Top level function ------------------------

transTheory :: Continuity -> Bool -> HatAna.Sign -> [Named PrDecl]

-> Result (IsaSign.Sign, [Named IsaSign.Sentence])

transTheory c m sign sens = do

sign' <- transSignature c m sign

(sign'', sens'') <- transSentencesI c sign' (map sentence sens)

return (sign'', concatMap (\ (t, l) ->

map (\ (r, ars) -> makeNamed ""

$ Instance t (map snd ars) [r] [] $ toIsaProof DotDot) l)

(filter (not . flip elem

["unitT", "intT", "integerT", "charT", "ratT"] . fst)

$ Map.toList $ arities $ tsig sign'') ++ sens'')

{- ---------------------------- Theory translation ------------------------

Relevant theories in Programatica: base/Ti/TiClasses (for

tcTopDecls); property/parse2/Parse/PropPosSyntax (def of HsDecl) -}

data TSt a = TSt (ISign -> Result (a, ISign))

instance Monad TSt

where

return x = TSt (\ w -> return (x, w))

(TSt f) >>= g = TSt (\ w -> do

(d, z) <- f w

let (TSt q) = g d in q z)

transSentencesI :: Continuity -> ISign -> [PrDecl]

-> Result (IsaSign.Sign, [Named IsaSign.Sentence])

transSentencesI c sign ls = let TSt f = transSentences c ls

in do (a, b) <- f sign

return (ff b, a)

where ff x = x {constTab = Map.filter (/= noTypeT) $ constTab x}

-- -----------------------------------------------------------------

transSentences :: Continuity -> [PrDecl]

-> TSt [Named IsaSign.Sentence]

transSentences c ls = do

xx0 <- mapM (transSentence c FunDef) ls

let xs = [[s] | [s] <- xx0, notDummy s]

yys <- insFixpoints c xs

zz0 <- mapM (transSentence c InstDef) ls

let zz1 = removeEL zz0

zz2 <- insFixpoints c zz1

let zz3 = filter notDummy (yys ++ zz2)

return $ filter (\ x -> extAxType x /= noTypeT) zz3

notDummy :: Named Sentence -> Bool

notDummy s = case sentence s of

ConstDef (IsaEq t _) -> t /= xDummy

RecDef _ _ _ [] -> False

RecDef _ _ _ (IsaEq t _ : _) -> t /= xDummy

_ -> True

transSentence :: Continuity -> ExpRole -> PrDecl

-> TSt [Named IsaSign.Sentence]

transSentence c a (TiPropDecorate.Dec d) =

case d of

PropSyntaxStruct.Base p -> case (a, p) of

(FunDef, HsDeclStruct.HsFunBind _ ws) -> do

k <- transMMatch c ws

return [k]

(FunDef, HsPatBind _ q (HsBody e) _) -> do

k <- transCProp FunDef c q e

case k of

Just k' -> return [k']

Nothing -> return []

(InstDef, HsInstDecl _ _ _ t (TiPropDecorate.Decs ds _)) -> do

k <- mapM (transIMatch c t)

[y | TiPropDecorate.Dec (PropSyntaxStruct.Base

(HsDeclStruct.HsFunBind _ [y])) <- ds]

w <-

mapM (uncurry $ transCProp InstDef c) [(q, e) |

TiPropDecorate.Dec (PropSyntaxStruct.Base

(HsDeclStruct.HsPatBind _ q (HsBody e) _)) <- ds]

return $ catMaybes $ k ++ w

_ -> return []

_ -> return []

{- ------------ main functions for sentence translation -------------------

------------------- inserts fixpoints ---------------------------------- -}

insFixpoints :: Continuity -> [[Named IsaSign.Sentence]]

-> TSt [Named IsaSign.Sentence]

insFixpoints c xs = TSt $ \ ssg ->

let ws = [[s] | s <- concat xs]

ys = fixMRec c ws

ac = newConstTab c ys

nc = Map.union (constTab ssg) ac

nssg = ssg {constTab = nc}

in return (ys, nssg)

-- ------------------------- constants -----------------------------------

constTabM :: TSt ConstTab

constTabM = TSt $ \ sign -> return (constTab sign, sign)

transCProp :: ExpRole -> Continuity

-> PrPat -> PrExp

-> TSt (Maybe (Named Sentence))

transCProp j a p e = do

cs <- constTabM

case transPatBindX True a cs p e of

Just (x, y) -> let k = fst $ extTBody x

in case getTermName k of

Nothing -> trace (show p) $ error "Hs2HOLCF.transCProp1"

Just nm -> case j of

InstDef -> case p of

TiPSpec (HsVar r) _ _ -> case extClass r of

Just c -> case e of

(TiPropDecorate.Exp (HsApp

(TiPropDecorate.TiSpec _ _ (g : _)) _)) ->

transInstEx a nm (mkVName nm)

(IsaClass c) (transType a [] g)

(typ $ termType x) [] y

_ -> trace (show p) $ error "Hs2HOLCF.transCProp2"

_ -> trace ("\n ER000: " ++ show j) $

trace ("\n ER111: " ++ show p) $

trace ("\n ER222: " ++ show e) $

error "Hs2HOLCF.transCProp3"

_ -> error "Hs2HOLCF.transCProp4"

FunDef -> return $ Just $ makeNamed nm $ ConstDef $ IsaEq x y

_ -> trace ("\n PAT: " ++ show p) $

trace ("\n EXP: " ++ show e) $

error "Hs2HOLCF.transCProp5"

{- ---------------- translate pattern matching definitions ---------------

Main function. transMultiDef translate the expressions,

formCaseExp builds the case expression. -}

transMMatch :: Show ds => Continuity

-> [HsDeclStruct.HsMatchI PNT PrExp PrPat ds]

-> TSt (Named Sentence)

transMMatch c ds = TSt $ \ sign -> case ds of

[] -> error "Hs2HOLCF.transMMatch"

a : _ -> let

cs = constTab sign

(a1, a2) = extInfo c cs a

df = mkVName $ showIsaName a1

y = fromMaybe noTypeT $ Map.lookup df cs

ls = map (snd . extInfo c cs) ds

in case ls of

[] -> error "Hs2HOLCF.transMMatch 2"

[(ps, tx)] -> let

qs = wrapWild $ map (transPat c cs) ps

in mkkSent c df y qs tx sign

_ -> let

ww = transMultiDef c cs ls

tx = formCaseExp c ww

qs = map (mkVs "qX" . snd) $

zip (fst a2) [(1 :: Int) ..]

in mkkSent c df y qs tx sign

where

extInfo c' cs' m = case m of

HsDeclStruct.HsMatch _ nm ps (HsGuardsStruct.HsBody x) _ ->

(nm, (elimDic ps, transExp c' cs' x))

HsDeclStruct.HsMatch _ nm ps (HsGuardsStruct.HsGuard xs) _ ->

let ys = [(transExp c' cs' x1, transExp c' cs' x2)

| (_, x1, x2) <- xs]

k = buildIfs c' ys

ps' = elimDic ps

in (nm, (ps', k))

mkkSent c' df' y' qs' tx' sign' = return

(makeSentence FunDef c' (IsaSign.orig df') y' df' qs' tx', sign')

wrapWild ls = map wrapW $ number ls

wrapW (a, n) = case a of

Free x -> case new x of

"wildcX" -> Free $ mkVName ("wildcX" ++ show n)

_ -> a

_ -> a

elimDic :: [PrPat] -> [PrPat]

elimDic ls = case ls of

[] -> []

x : xs -> let r = elimDic xs in case x of

TiDecorate.Pat (HsPId (HsVar _)) -> r

_ -> x : r

{- ----------------------- translates instances --------------------------

translates method definitions -}

transIMatch :: (Show ds) => Continuity -> HsType

-> HsDeclStruct.HsMatchI PNT PrExp PrPat ds

-> TSt (Maybe (Named Sentence))

transIMatch a t s = do

ct <- constTabM

case s of

HsDeclStruct.HsMatch _ nm ps (HsGuardsStruct.HsBody ex) _ ->

let nam = showIsaName nm

df = mkVName $ showIsaName nm

tx = transExp a ct ex

qs = map (transPat a ct) ps

gt = getInstType t -- instatiating type

x = transType a [] gt -- instatiating type

c = transClass $ getInstClass t

-- instantiated class

in transInstEx a nam df c x noTypeT qs tx

_ -> error "Hs2HOLCF, transIMatch"

transInstEx :: Continuity -> String -> VName ->

IsaClass -> IsaType -> IsaType ->

[IsaTerm] -> IsaTerm -> TSt (Maybe (Named Sentence))

transInstEx a nam df c@(IsaClass k) x x2 qs tx = TSt $

if and [enElem nam mthEq]

then \ sig -> return (Nothing, sig)

else

\ sign ->

let ct = constTab sign

xx = typeId x

w = fromMaybe [] $ Map.lookup xx (arities $ tsig sign)

-- all arities of inst. type

cs = fromMaybe [] $ Map.lookup c (Map.fromList w)

-- selects the arity for the inst. class

xdf = new df

ndf = if enElem nam aweLits

then xdf ++ "_" ++ xx

else xx ++ "_" ++ xdf

pdf = if enElem nam aweLits

then mkVName ndf else df

nsg = if enElem nam ["return"]

then addMonOpDecs sign xx

else sign

mty | enElem nam ["return"] = returnType xx

| enElem nam [">>="] = bindType xx

| enElem nam ["fail", ">>"] = noTypeT

| enElem nam mthAll = mthTy a k nam

| otherwise = fromMaybe x2 $ Map.lookup df ct

-- abstract method type

nty = instTyp mty c x cs

{- in mty, replaces the variable of class c with type x,

constraining variables in x with cs -}

tst = makeSentence InstDef a ndf nty pdf qs tx

in return (Just tst, nsg)

instTyp :: IsaType -> IsaClass -> IsaType -> [(IsaType, Sort)] -> IsaType

instTyp t c x cs = repVarClass t c (constrVarClass x cs)

{- ------------------ theory trans auxiliaries ------------------------

------------------ transMMatch auxs ------------------------------- -}

buildIfs :: Continuity -> [(IsaTerm, IsaTerm)] -> IsaTerm

buildIfs c xs = case xs of

[] -> bottomPT c

(y1, y2) : ys -> case getTermName y1 of

Just "otherwise" -> y2

_ -> If y1 y2 (buildIfs c ys) c

makeSentence :: ExpRole -> Continuity -> String -> IsaType ->

VName -> [IsaPattern] -> IsaTerm -> Named Sentence

makeSentence k a d y df ps tx =

makeNamed d $ ConstDef (if tx == xDummy

then IsaEq xDummy xDummy

else let w = ( case k of

InstDef -> dispMN y

FunDef -> hideNN y )

in IsaEq (Const df w) $ termMAbs a ps tx)

-- ----------------- transIMatch auxs ---------------------------------

returnType :: String -> IsaType

returnType t = let

v = TFree "a" holType

x = IsaSign.Type t holType [v]

in IsaSign.Type "=>" holType [v, x]

bindType :: String -> IsaType

bindType t = let

va = TFree "a" holType

vb = TFree "b" holType

xa = IsaSign.Type t holType [va]

xb = IsaSign.Type t holType [vb]

f = IsaSign.Type "=>" holType [va, xb]

g = IsaSign.Type "=>" holType [f, xb]

in IsaSign.Type "=>" holType [xa, g]

addMonOpDecs :: ISign -> String -> ISign

addMonOpDecs sign xx = let

nrt = returnType xx

nbd = bindType xx

jrt = mkVName $ "return_" ++ xx

jbd = mkVName $ "mbind_" ++ xx

qqs = Map.fromList [(jrt, nrt), (jbd, nbd)]

nc = Map.union (constTab sign) qqs

in sign {constTab = nc}

extHead :: IsaType -> IsaType

extHead t = case t of

IsaSign.Type "=>" _ [_, b] -> extHead b

_ -> t

{- ------------- other theory trans auxs ----------------------------------

annotated translation function.

Each parameter pattern - IsaPattern - associated

with datatype information - [(String,Int)]

case variable name - IsaTerm

parameter name before translation - String -}

transMultiDef :: Continuity -> ConstTab -> [([PrPat], IsaTerm)]

-> [([([(String, Int)], ((IsaTerm, String), IsaPattern))], IsaTerm)]

transMultiDef c sign ls =

let

ws = csAris [fst w | w <- ls]

ks = [([newInfo v | v <- xs], y) | (xs, y) <- ls]

ss = map standizeVars ks

in [(zipNE ws rs, s) | (rs, s) <- ss]

where

newInfo f = (snd $ extCI f, transPat c sign f)

zipNE ws rs = case ws of

[] -> []

hd : xs -> (case hd of

[] -> []

_ -> if null rs then error "Hs2HOLCF, zipNE"

else [(hd, head rs)]) ++ zipNE xs (tail rs)

{- Extract datatype information from a list of patterned parameter lists.

Returns the list of constructors and arities for parameter datatypes. -}

csAris :: [[PrPat]] -> [[(String, Int)]]

csAris ws = let

ls = removeEL ws

in case ls of

[] -> []

m : _ -> case m of

[] -> []

_ : _ -> extCL (map head ls) : csAris [tail a | a <- ls]

{- Standardizes parameter names from all the expressions.

Associates a case variable name. -}

standizeVars :: ([(String, IsaPattern)], IsaTerm)

-> ([((IsaTerm, String), IsaPattern)], IsaTerm)

standizeVars k' = let

mkqXVs = mkVs "qX"

stdVars (cs, sd) i = case cs of

[] -> ([], sd)

(a, b) : as -> let

na = sbVs (b, i)

nk = renVars na [b] sd

(ls, y) = stdVars (as, nk) (i + 1)

in (((mkqXVs i, a), na) : ls, y)

sbVs a = case a of

(Free _, b) -> mkqXVs b

(f, _) -> f

in stdVars k' 1

mkVs :: String -> Int -> IsaTerm

mkVs str n = Free (mkVName $ str ++ show n)

-- Forms the nested case expression, using trCase.

formCaseExp :: Continuity ->

[([([(String, Int)], ((IsaTerm, String), IsaPattern))], IsaTerm)]

-> IsaTerm

formCaseExp ct ls =

case ls of

[] -> error "Hs2HOLCF.formCaseExp"

m : _ -> case fst m of

[] -> snd m

h : _ -> let

k1s = map fst ls

xs = map head (filter (/= []) k1s)

xxs = remove_duplicates [((snd $ fst $ snd x, snd $ snd x),

[(us, t) | (u : us, t) <- ls, u == x] ++

[(us, t) | ((_, (_, Free _)) : us, t) <- ls]) | x <- xs]

ws = remove_duplicates

[((a, b), formCaseExp ct c) | ((a, b), c) <- xxs]

in makeCase (fst $ fst $ snd h) $ map (\ z -> trCase ct z ws) (fst h)

where

makeCase = Case

{- ---------------------- TERM translation --------------------------------

---------------------- Patterns ---------------------------------------- -}

transPat :: Continuity -> ConstTab -> PrPat -> IsaPattern

transPat a c t = let

a' = if a == IsCont True then IsCont False else a

in fromMaybe xDummy $ transMPat a' c t

transMPat :: Continuity -> ConstTab -> PrPat -> Maybe IsaPattern

transMPat = transMPatX False

transMPatX :: Bool ->

Continuity -> ConstTab -> PrPat -> Maybe IsaPattern

transMPatX bx a' cs t = let

tInt = IsaSign.Type "int" holType []

a = if a' == IsCont True then IsCont False else a'

in case t of

TiDecorate.Pat p -> case p of

HsPLit _ (HsInt n) -> return $ liftExp a (show n) tInt

HsPList _ xs -> do

ws <- mapM (transMPatX bx a cs) xs

return $ foldr (termBAppl a $ consPT a) (nilPT a) ws

_ -> transP a (mkVName . showIsaName) (transMPat a cs) p

TiDecorate.TiPSpec w lt bb -> case w of

HsVar x -> case showIsaName x of

"errorH" -> Just $ bottomPT a

_ -> transHV bx a x bb lt

HsCon x -> transCN a x

TiDecorate.TiPTyped x _ -> transMPat a cs x

TiDecorate.TiPApp w z -> do w1 <- transMPat a cs w

z1 <- transMPat a cs z

return $ termMAppl a w1 [z1]

transP :: IsaName i => Continuity -> (i -> VName) ->

(p -> Maybe IsaPattern) -> PI i p -> Maybe IsaPattern

transP a trId trP p =

case mapPI3 trId trP p of

Just (HsPId (HsVar _)) -> return $ conDouble "DIC"

Just (HsPTuple _ xs) -> return $ Tuplex xs a

Just (HsPParen x) -> return x

Just HsPWildCard -> return $ Free $ mkVName "wildcX"

_ -> Nothing

-- ------------------------ Terms --------------------------------------

transExp :: Continuity -> ConstTab -> PrExp -> IsaTerm

transExp a c t = fromMaybe xDummy $ transMExp a c t

transMExp :: Continuity -> ConstTab -> PrExp -> Maybe IsaTerm

transMExp a cs t = let

tInt = IsaSign.Type "int" holType []

tRat = IsaSign.Type "Rat" holType []

in case t of

(TiPropDecorate.Exp e) -> case e of

HsLit _ (HsInt n) -> return $ liftExp a (show n) tInt

HsLit _ (HsFloatPrim n) -> return $ liftExp a (show n) tRat

HsLit _ (HsString n) -> return $ liftStr a (show n)

HsList xs -> do

ws <- mapM (transMExp a cs) xs

return $ foldr (termBAppl a $ consPT a) (nilPT a) ws

HsLet (TiPropDecorate.Decs ds _) k -> do

w <- mapM (transPatBind False a cs) ds

z <- transMExp a cs k

return $ Let w z

HsCase e' as -> do

e1 <- transMExp a cs e'

bs <- transCases a cs (map extPE as)

return $ Case e1 bs

_ -> transE a (mkVName . showIsaName) (transMExp a cs)

(transMPat a cs) e

TiPropDecorate.TiSpec w st bb -> case w of

HsVar x -> case showIsaName x of

"errorH" -> Just $ bottomPT a

_ -> transHV False a x bb st

HsCon x -> transCN a x

TiPropDecorate.TiTyped x _ -> transMExp a cs x

transE :: Continuity -> (PNT -> VName) -> (e -> Maybe IsaTerm)

-> (p -> Maybe IsaPattern) -> EI PNT e p j h k -> Maybe IsaTerm

transE c trId trE trP e =

case mapEI5 trId trE trP e of

Just (HsId (HsVar _)) -> return $ conDouble "DIC"

Just (HsApp x y) -> return $ if x == bottomPT c

then x

else termMAppl c x [y]

Just (HsLambda ps x) -> return $ termMAbs c ps x

Just (HsIf x y z) -> return $ If x y z c

Just (HsTuple xs) -> return $ Tuplex xs c

Just (HsParen x) -> return x

_ -> Nothing

-- --------------------- TERM auxs ----------------------------------------

liftExp :: Continuity -> String -> Typ -> IsaTerm

liftExp c n t = case c of

IsCont _ -> App (conDouble "Def")

(Const (mkVName n) $ hideNN t) NotCont

NotCont -> Const (mkVName n) $ hideNN t

liftStr :: Continuity -> String -> IsaTerm

liftStr a n = let

st = Const (mkVName n) noType

in case a of

NotCont -> st

IsCont _ -> termAppl liftString st

transCases :: Continuity -> ConstTab ->

[(TiPat PNT, TiPropDecorate.TiExp PNT)] -> Maybe [(IsaTerm, IsaTerm)]

transCases r cs ks = case ks of

[] -> return []

_ : _ -> let

cnn = extCL $ map fst ks -- (cons, arity) list for the case value.

ys = [((snd $ extCI f, transPat r cs f), transExp r cs g)

| (f, g) <- ks] -- (cons, (ptn, exp)) list.

in if null cnn then trace ("\n CASES: " ++ show ks) $

error "Hs2HOLCF.transCases"

else return $ map (\ h -> trCase r h ys) cnn

extPE :: HsGuardsStruct.HsAlt (TiPropDecorate.TiExp PNT) (TiPat PNT)

(TiPropDecorate.TiDecls PNT) -> (TiPat PNT, TiPropDecorate.TiExp PNT)

extPE k = case k of

HsAlt _ p (HsBody e) _ -> (p, e)

_ -> error "HsHOLCF.extPE"

extCL :: [TiPat PNT] -> [(String, Int)]

extCL ks = case ks of -- ((cons, arity) list, cons).

[] -> []

x : xs -> let p = (fst $ extCI x)

in if p /= [] then p else extCL xs

extCI :: TiPat PNT -> ([(String, Int)], String)

extCI k = case k of

TiPSpec (HsCon (PNT z (ConstrOf _ x) _)) _ _ ->

([(gBN $ conName w, conArity w) | w <- constructors x], pp z)

TiPSpec (HsVar (PNT z _ _)) _ _ -> ([], pp z)

TiPApp m _ -> extCI m

TiDecorate.Pat u -> case u of

HsPWildCard -> ([], "wildcX")

HsPParen p -> extCI p

HsPLit _ (HsString "") -> ([], "emptyString")

_ -> ([], pp u)

TiPTyped p _ -> ([], pp p)

_ -> error "H2HOLCF.extCI"

where

gBN (UniqueNames.PN q _) = q

trCase :: Continuity -> (String, Int) ->

[((String, IsaPattern), IsaTerm)] -> (IsaTerm, IsaTerm)

trCase r' h ys = let

r = case r' of

IsCont _ -> IsCont False

_ -> r'

in case ys of

[] -> case r of

IsCont _ -> (buildPat r h, bottomPT r)

NotCont -> error "Hs2HOLCF.trCase"

((a, b), c) : as | a == fst h -> repVsCPt b c (snd h) -- snd h :: Int

| take 6 a == "wildcX" -> (buildPat r h, c)

| otherwise -> trCase r h as

where

mkpXVs = mkVs "pX"

repVsCPt a b n = case a of

IsaSign.Const _ _ -> (a, b)

IsaSign.App x y@(IsaSign.Free _) z' -> let

nv = mkpXVs n

nr = renVars nv [y] b

st = repVsCPt x nr (n - 1)

nf = termMAppl z' (fst st) [nv]

ns = renVars nv [y] $ snd st

in (nf, ns)

_ -> trace ("\n print A: " ++ show a) $

trace ("\n print B: " ++ show b) $

error "Hs2HOLCF.repVsCPt"

buildPat s (x, n) = let

hh = string2iterm s x Nothing

k = Const (mkVName $ showIsaName x) noTypeC

j = fromMaybe k hh

sk = termMAppl s j $ reverse $ map mkpXVs [1 .. n]

in sk

extClass :: PNT -> Maybe String

extClass p = case p of

PNT _ (MethodOf (PN x _) _ _) _ -> Just x

_ -> Nothing

transPatBindX :: Bool ->

Continuity -> ConstTab -> PrPat -> PrExp -> Maybe (IsaTerm, IsaTerm)

transPatBindX b a cs p e = do

x <- transMPatX b a cs p

y <- transMExp a cs e

return (x, y)

transPatBind :: Bool ->

Continuity -> ConstTab -> PrDecl -> Maybe (IsaTerm, IsaTerm)

transPatBind b a cs s = case s of

TiPropDecorate.Dec (PropSyntaxStruct.Base

(HsDeclStruct.HsPatBind _ p (HsGuardsStruct.HsBody e) _)) ->

transPatBindX b a cs p e

_ -> error "HsHOLCF.transPatBind"

transCN :: Continuity -> PNT -> Maybe IsaTerm

transCN c x = let

k = pp x

y = showIsaName x

w = Const (mkVName y) $ Hide noTypeT TCon (extArity x)

zz = string2iterm c k Nothing

in return $ fromMaybe w zz

extArity :: PNT -> Maybe Int

extArity p = case p of

(PNT z (ConstrOf _ x) _) -> let

y = pp z

ls = [(gBN $ conName w, conArity w) | w <- constructors x]

ns = Map.fromList ls

in Map.lookup y ns

_ -> Nothing

where

gBN (UniqueNames.PN q _) = q

transHV :: Bool -> Continuity -> PNT -> [HsType] ->

HsScheme -> Maybe IsaTerm

transHV _ a x lt tt = let

qq = pp x

n = showIsaName x

xt = fromMaybe noTypeT $ transMScheme a tt

kt = fromMaybe noTypeT $ case lt of

r : _ -> transMType a [] r

_ -> Nothing

zt = replaceTyVar kt xt

dx = case x of

PNT (PN _ (UniqueNames.G {})) _ _ ->

mkConstV n (hideNN zt)

PNT (PN _ (UniqueNames.S _)) _ _ -> mkFree n

PNT (PN _ (UniqueNames.Sn _ _)) _ _ -> mkFree n

_ -> error "Hs2HOLCF.transHV"

rt = fromMaybe dx $ string2iterm a qq (Just lt)

in return rt

string2iterm :: Continuity -> String ->

Maybe [HsType] -> Maybe IsaTerm

string2iterm a qq ls =

case showIsaName qq of

"()" -> return $ unitPT a

"(,)" -> return $ pairPT a

"True" -> return $ truePT a

"False" -> return $ falsePT a

"conjH" -> return $ andPT a

"disjH" -> return $ orPT a

"notH" -> return $ notPT a

":" -> return $ consPT a

"[]" -> return $ nilPT a

"Nothing" -> return $ nothingPT a

"Just" -> return $ justPT a

"fstH" -> return $ fstPT a

"sndH" -> return $ sndPT a

"headH" -> return $ headPT a

"tailH" -> return $ tailPT a

"Left" -> return $ leftPT a

"Right" -> return $ rightPT a

"return" -> return $ mkTyConst a ls "return"

"mbind" -> return $ mkTyConst a ls "mbind"

"mbbind" -> return $ mkTyConst a ls "mbbind"

_ -> Nothing

where

mkTyConst aa tt s = let

ndf = case tt of

Just (x : _) -> let

w = typeId $ extHead $ transType aa [] x

in s ++ "_" ++ w

_ -> s

in Const (mkVName ndf) noType

-- --------------------- TERM trans recursive schemes ---------------------

mapEI5 :: (i1 -> i2) -> (e1 -> Maybe e2) -> (p1 -> Maybe p2)

-> EI i1 e1 p1 d t c -> Maybe (EI i2 e2 p2 d t c)

mapEI5 vf ef pf ex =

case ex of

HsId n -> return $ HsId (mapHsIdent2 vf vf n)

HsApp x y -> do a <- ef x

b <- ef y

return $ HsApp a b

HsLambda ps e -> do xs <- mapM pf ps

y <- ef e

return $ HsLambda xs y

HsIf x y z -> do a <- ef x

b <- ef y

c <- ef z

return $ HsIf a b c

HsTuple xs -> do zs <- mapM ef xs

return $ HsTuple zs

HsParen x -> do a <- ef x

return $ HsParen a

HsList xs -> do ys <- mapM ef xs

return $ HsList ys

_ -> Nothing

mapPI3 :: (i1 -> i2) -> (p1 -> Maybe p2) -> PI i1 p1 -> Maybe (PI i2 p2)

mapPI3 vf pf pat =

case pat of

HsPId n -> return $ HsPId (mapHsIdent2 vf vf n)

HsPLit s l -> return $ HsPLit s l

HsPTuple s ps -> do bs <- mapM pf ps

return $ HsPTuple s bs

HsPParen p -> do h <- pf p

return $ HsPParen h

HsPWildCard -> return HsPWildCard

HsPList s ps -> do qs <- mapM pf ps

return $ HsPList s qs

HsPApp nm ps -> do qs <- mapM pf ps

return $ HsPApp (vf nm) qs

HsPSucc s n l -> return $ HsPSucc s (vf n) l

_ -> Nothing

{- -----------------------------------------------------------------------

---------------------- SIGNATURE translation --------------------------

----------------------------------------------------------------------- -}

transSignature :: Continuity -> Bool -> HatAna.Sign -> Result IsaSign.Sign

transSignature c m sign = let

tys = HatAna.types sign

vals = HatAna.values sign

xx = getDomainTab c vals

nsig = IsaSign.emptySign

{ baseSig = case (c, m) of

(IsCont _, False) -> HsHOLCF_thy

(NotCont, False) -> HsHOL_thy

(IsCont _, True) -> MHsHOLCF_thy

(NotCont, True) -> MHsHOL_thy,

tsig = emptyTypeSig

{

classrel = getClassrel c tys,

abbrs = getAbbrs c tys,

arities = getArities c xx (HatAna.instances sign)

},

constTab = getConstTab c vals,

domainTab = xx

}

in Result [] $ Just nsig

{- ---------------------------- TYPE translation -------------------------

signature translation takes after one to Stratego, relies

on Isabelle.Translation to solve naming conflicts. -}

transType :: Continuity -> [HsType] -> HsType -> IsaType

transType a c t = fromMaybe noTypeT $ transMType a c t

transMType :: Continuity -> [HsType] -> HsType -> Maybe IsaType

transMType a c (Typ t) = transT a

(transIdV a c) (transIdC a) (transMType a c) t

transT :: Show d => Continuity -> (PNT -> Maybe IsaType)

-> (PNT -> Maybe IsaType) -> (d -> Maybe IsaType)

-> TI PNT d -> Maybe IsaType

transT c trIdV trIdC trT t =

case mapTI3 trIdV trIdC trT t of

Just (HsTyFun t1 t2) -> return (case c of

IsCont _ -> mkContFun t1 t2

NotCont -> mkFunType t1 t2)

Just (HsTyApp t1 t2) ->

case t1 of

IsaSign.Type name s args -> -- better resolve nested HsTyApp first

return $ IsaSign.Type name s $ args ++ [t2]

_ -> Nothing

Just (HsTyVar a) -> return a

Just (HsTyCon k) -> return k

_ -> Nothing

getSort :: Continuity -> [HsType] -> PNT -> IsaSort

getSort r c t = case c of

[] -> case r of

IsCont _ -> dom

NotCont -> holType

(x@(Typ (HsTyApp _ _))) : cs -> let

a = getInstType x

b = getInstClass x

d = getLitName a

s = getSort r cs t

k = transClass b

u = showIsaName d

v = showIsaName t

in if u == v then k : s else s

_ : cs -> getSort r cs t

transIdV :: Continuity -> [HsType] -> PNT -> Maybe IsaType

transIdV a c t = return $ TFree (showIsaName t) (getSort a c t)

transIdC :: Continuity -> PNT -> Maybe IsaType

transIdC c t = case t of

PNT _ (TypedIds.Class _ _) _ -> Nothing

_ -> return $ let

tfs = transFields c t

srt = case c of

IsCont _ -> dom

NotCont -> holType

in

case UniqueNames.orig t of

UniqueNames.G (PlainModule m) n _ ->

IsaSign.Type (transTN c m n) srt tfs

UniqueNames.G (MainModule m) n _ ->

IsaSign.Type (transPath m n) srt tfs

_ -> IsaSign.Type (showIsaName t) srt tfs

transFields :: Continuity -> PNT -> [IsaType]

transFields c t = let

srt = case c of

IsCont _ -> dom

NotCont -> holType

in case t of

PNT _ (TypedIds.Type q) _ ->

[TFree (showIsaS x) srt | (PN x _) <- TypedIds.fields q]

PNT _ (TypedIds.FieldOf _ q) _ ->

[TFree (showIsaS x) srt | (PN x _) <- TypedIds.fields q]

_ -> []

mapTI3 :: (Show i1, Show i2, Show t1, Show t2) =>

(i1 -> Maybe i2) -> (i1 -> Maybe i2) -> (t1 -> Maybe t2)

-> TI i1 t1 -> Maybe (TI i2 t2)

mapTI3 vf cf tf hty = case hty of

HsTyFun x y -> do a <- tf x

b <- tf y

return $ HsTyFun a b

HsTyApp f x -> do a <- tf f

b <- tf x

return $ HsTyApp a b

HsTyVar nm -> do a <- vf nm

return $ HsTyVar a

HsTyCon nm -> do a <- cf nm

return $ HsTyCon a

_ -> Nothing

-- ---------------------------- Class translation ------------------------

transClass :: HsType -> IsaClass

transClass x = case x of

Typ (HsTyCon c) -> IsaClass (showIsaName c)

Typ _ -> trace ("\n CLASS: " ++ show x) $

error "Hs2HOLCF.transClass"

{- ------------------------ SIGN fields translation -----------------------

------------------------ translation for ConstTab ---------------------- -}

getConstTab :: Continuity -> VaMap -> ConstTab

getConstTab c = Map.map fst . Map.filter ((== IsaVal) . snd)

. getAConstTab c

getAConstTab :: Continuity -> VaMap -> AConstTab

getAConstTab c =

liftMapByListD Map.toList Map.fromList (mkVName . showIsaName . fst)

(\ (x, y) -> (transMScheme c y, getValInfo x)) nothingFiOut

getValInfo :: HsId -> IsaVT

getValInfo n = case n of

HsCon _ -> IsaConst

_ -> IsaVal

transMScheme :: Continuity -> HsScheme -> Maybe IsaType

transMScheme a s = case s of

Forall _ _ (c TiTypes.:=> t) -> transMType a c t

-- ---------------------- translation of domaintab -----------------------

getDomainTab :: Continuity -> VaMap -> DomainTab

getDomainTab c f = let

ls = remove_duplicates

[getDomainEntry (getAConstTab c f) x |

x <- Map.keys f, checkTyCons x]

in getDepDoms ls

getDomainEntry :: AConstTab -> HsId -> [DomainEntry]

getDomainEntry ctab t = case t of

HsCon (PNT _ (TypedIds.ConstrOf _ d) _) ->

[(getDomType ctab (mkVName $ showIsaName t),

[(b, getFieldTypes ctab b)

| b <- [ mkVName $ showIsaName c

| PN c _ <- map conName (constructors d)]])]

_ -> []

-- -------------------- translation for Classrel (from KEnv) ------------

getClassrel :: Continuity -> TyMap -> Classrel

getClassrel c = liftMapByList Map.toList Map.fromList

(IsaClass . showIsaName) (transClassInfo c)

transClassInfo :: Continuity -> (Kind, HsTypeInfo) -> ClassDecl

transClassInfo c p = case snd p of

TiTypes.Class {} ->

(remove_duplicates $ case c of

IsCont _ -> dom

NotCont -> holType

++ map transClass (extClassInfo $ snd p), [], [])

_ -> ([], [], [])

-- ----------------- translation of Abbrs (from KEnv) --------------------

getAbbrs :: Continuity -> TyMap -> Abbrs

getAbbrs c = Map.foldWithKey (\ k v -> case v of

Nothing -> id

Just p -> Map.insert k p) Map.empty

. liftMapByList Map.toList Map.fromList

(showTyNm c) (transAbbrsInfo c)

where showTyNm w t = case t of

HsCon x -> case transIdC w x of

Just (IsaSign.Type n _ _) -> n

_ -> showIsaName t

_ -> showIsaName t

transAbbrsInfo :: Continuity -> (Kind, HsTypeInfo) ->

Maybe ([TName], IsaType)

transAbbrsInfo c p = case snd p of

TiTypes.Synonym _ _ -> let (x, y) = extAbbrsInfo (snd p) in

Just (map showIsaName x, transType c [] y)

_ -> Nothing

-- -------------------- translation of arities ---------------------------

getArities :: Continuity -> DomainTab -> HsInstances -> IsaSign.Arities

getArities c dt db = Map.fromList (groupInst $ getTypeInsts c dt db)

getTypeInsts :: Continuity -> DomainTab -> HsInstances -> [IsaTypeInsts]

getTypeInsts c dt db =

[(typeId $ transType c [] $ getMainInstType x,

[transInst c x]) | x <- db]

++ [(u, [(IsaClass "Eq", [])]) | [(IsaSign.Type u _ [], _)] <- dt]

transInst :: Continuity -> HsInstance ->

(IsaClass, [(IsaType, [IsaClass])])

transInst c i = let (x, y) = prepInst i

w = case c of

IsCont _ -> pcpo

NotCont -> isaTerm

in (transClass x,

[(transType c [] a, w : map transClass b) | (a, b) <- y])

-- ------------------------------------------------------------------------