module BaseStruct2Alfa{-(transModule,modPath)-} where
import TiDecorate(DeclsUseType,TiPat(..),drop_use)
import TiPrelude(prelFlip,prelOtherwise,prelTrue)
import PNT(PNT(..))
import TypedIds(IdTy(ConstrOf,Class),ConInfo(..),TypeInfo(..))
import UniqueNames as UN(PN(..),Orig(..),orig)
import HasBaseName
import NameMaps
import NameMapsDecorate
import QualNames(unqual,getQualified)
import BaseSyntax hiding (extend)
import Syntax(kstar,kpred,kprop)
import HsConstants(mod_Prelude)
import PrettyPrint
import qualified UAbstract as U
import qualified AbstractOps as U
import qualified UMatch as U
import qualified USubstitute as U
import qualified UFree as U
--import qualified DrawOptions as U(defaultArgOptions,HasName(..),ArgOptions(..))
--import qualified DrawOptionsPrinter as U(printIdOptions)
import EnvM hiding (inEnv)
import MUtils
import TI hiding (TI,getEnv,inst,tapp,sch,inEnv,extend,restrict,tupleT,conName)
--import TiT(kcCheck)
--import RemovePatBinds(remPatBinds')
--import RemoveIrrefPatsBase(removeIrrefPats)
import Lift(lift)
import TiHsName
import USCC(decls)
import PFE0(moduleInfoPath) -- grr
--import Char(isUpper)
import Maybe(fromMaybe,listToMaybe,fromJust)
import List(nub,partition,(\\),sort)
import Monad(join,mplus{-,unless-})
--import Fudgets(ctrace)
default(Int)
type DEnv = DeclsType NName
type DEnv' = DeclsUseType NName
type Env = ([ModuleName],DEnv) -- to keep track of which module is being translated
type Ctx = [Typing NName (Pred NName)]
--type NName = PN HsName
type NName = PNT
---
modPath m = moduleInfoPath m++".alfa"
class Trans src dst | src->dst where
trans :: src->EnvM Env dst
transTyped :: Maybe (HsTypeI NName) -> src -> EnvM Env dst
-- Defined at least one of trans and transTyped!
trans = transTyped Nothing
transTyped _ = trans
instance Trans src dst => Trans (Maybe src) (Maybe dst) where
transTyped t (Just e) = Just # transTyped t e
transTyped t Nothing = return Nothing
ltrans xs = mapM trans xs
--instance Trans [HsImportDeclI i] [U.Decl] where
-- trans is = return [] -- not implemented yet
instance (Trans ds1 [U.Def],
--MapNames (Bool,NName) ds1 NName ds2,
AccNames NName ds1,
MapNames NName ds0 NName ds1)
=> Trans (HsModuleI m i1 ds0) U.Module where
trans m = transModule m # getEnv
packageSynonym (PlainModule newm) (PlainModule oldm) = -- !!!
[U.decl' [U.defA $
U.Package (U.Var (transMName newm),(U.ctx [],
U.PackageInst (un (transMName oldm))))]]
joinModuleNames [m] = m
joinModuleNames ms = PlainModule . concat $ sort [s|PlainModule s<-ms] -- !!!
uPackage n ds = U.defA $ U.Package (n,(U.ctx [],U.PackageDef ds))
uPack n ds = uPackage n (decls ds)
transModule hsmodule (mo0,denv) =
U.Module (map include origMods++
[U.decl' [uPackage (U.Var m)
(map openUnqual (unqualNames ns)++
decls (withEnv env (trans ds2)))]]
)
where
PlainModule m = transM (joinModuleNames mo0) -- !!!
mo = map transM mo0
HsModule src _ e is ds0 =
{-remPatBinds' bind_names . removeIrrefPats arg_names $-} hsmodule
{-
where
--arg_names, bind_names :: [PNT]
arg_names = [ localVal ("arg" ++ show n) | n <- [1..]]
bind_names = [ localVal ("bind" ++ show n) | n <- [1..]]
-}
env = (mo,denv)
ds2 = {-mapNames snd-} ds1
ds1 = transNames mo ds0
ns = --map snd $
filter notcon $ {- nubBy eqSrc $ -} accNames (:) ds1 []
--notcon = fst
notcon (PNT _ (ConstrOf {}) _) = False
notcon _ = True
origMods = nub [m|PNT (PN _ (G m _ _)) _ _<-ns,m `notElem` mo0]
include m = U.ImportDecl (U.Import (modPath m))
unqualNames ns =
collectByFst [(m,n)|PNT (PN (UnQual n) (G m _ _)) _ _<-ns,m `notElem` mo0]
openUnqual (PlainModule m,ns) = -- !!!
U.decl' [U.defA (U.Open (un (transMName m),map oa (nub ns)))]
oa = oav . U.Var . transName
oav' v = U.OpenArg [] v Nothing
oav v = oav' v Nothing
mapPNT f (PNT i idty p) = PNT (f i) idty p
transNames self = mapNames2 TopLevel (varf,conf)
where
varf (role,ClassOrTypeNames) = mapPNT (u . tvar)
varf (role,ValueNames) = mapPNT (u . var)
conf (role,ClassOrTypeNames) = mapPNT (u . tcon)
conf (role,ValueNames) = mapPNT (u . vcon)
-- Packages can't refer to themselves...
u (PN (Qual m n) o) | m `elem` self = PN (UnQual n) o
u x = x
-- var (PN (UnQual x) o@(I m _)) = PN (Qual (transM m) x) o -- instances
var (PN (UnQual x) o@(D n _)) = PN (UnQual (x++show n)) o -- type vars
var (PN (UnQual x) o@(Sn _ s)) = PN (UnQual (x{-++sh s-})) o
-- where sh (SrcLoc f 0 0) = ""
-- sh (SrcLoc f r c) = "_"++show r++"_"++show c
var (PN (Qual _ _) o@(G m n _)) = PN (Qual (transM m) (transName n)) o
var v@(PN q o) =
if v==prelVal "super"
then localVal "super" -- hack
else PN (transQ q) o
tvar (PN (UnQual x) o@(D n _)) = PN (UnQual (x++show n)) o -- generated type var
tvar (PN (UnQual x) o@(UN.S s)) = PN (UnQual (x++"_")) o -- source type var
vcon (PN _ o@(G m n _)) = PN (UnQual (transConName n)) o
vcon c = c
tcon (PN (Qual _ _) o@(G m n _)) = PN (Qual (transM m) (transTCon n)) o
tcon (PN (UnQual _) o@(G m n _)) = PN (UnQual (transTCon n)) o
transTCon n =
case n of
"[]" -> "List"
_ -> transName n
transQ (UnQual x) = UnQual (transName x)
transQ (Qual m n) = Qual (transM m) (transName n)
transConName n = case n of
"[]" -> "Nil"
":" -> "Cons" -- Hmm. Alfa Library convension
_ -> transName n
inPrelude this = transM mod_Prelude `elem` this
transM (PlainModule m) = PlainModule (transMName m)
transM (MainModule m) = PlainModule (transMName "Main") -- !!!
transMName m = "Module_"++dots2uscore m
transName n =
case n of
"Type" -> "Type_" -- reserved identifier
"sig" -> "sig_"
"use" -> "use_"
"." -> ".." -- reserved operator
"()" -> "Unit"
'(':s -> "Tuple"++show (length s) -- tuples!
_ -> n
transD ds = decls # trans ds
{-
instance Trans Ctx [U.Def] where trans = ltrans
instance Trans (Typing NName (Pred NName)) U.Def where
trans (d:>:t) = do t' <- trans t
d' <- transVar d
return $ valdef d' ([],t') U.ePreMetaVar
-}
inModDEnv f = inModEnv (apSnd f)
extend env = inModDEnv (env+++)
extendFrom ds = extend (drop_use (envFrom ds))
extendTyvars = extendTyvars' . mapFst HsVar
extendTyvars' vs = inModDEnv (\(ks,ts)->(map tyvar vs++ks,ts))
where tyvar (v,k) = v:>:(k,Tyvar)
restrict vs = inModDEnv (\(ks,ts)->(ks,[a|a@(x:>:_)<-ts,x `notElem` vs]))
restrictFrom ps = restrict (patternVars ps)
scope ps ds = restrictFrom ps . extendFrom ds
instance (Printable e,Printable p,Printable ds,Printable t,Printable ctx,
FreeNames NName ctx,
Printable tp,DefinedNames NName tp,DefinedNames NName t,
FreeNames NName t,KindCheck NName t Kind,Types NName t,
FreeNames NName tp,Trans p U.Pat,
HasId NName p, DefinedNames NName p, AccNames NName p,
KindCheck NName tp Kind,Types NName tp,
HasId NName e,Trans e U.Exp,Trans ds [U.Def], EnvFrom ds DEnv',
Trans t U.Exp,Trans ctx [U.Exp],Trans tp U.Exp) =>
Trans (DI NName e p ds t ctx tp) [U.Def] where
trans d = trans' d =<< getMEnv
where
trans' d this =
case d of
HsTypeDecl s tp t -> tPs tp $ typeD # tlhs tp <# trans t
HsNewTypeDecl s ctx tp cd drv -> tPs tp $ dataD # tlhs tp <# ltrans [cd]
HsDataDecl s ctx tp cds drv -> tPs tp $ dataD # tlhs tp <# ltrans cds
HsClassDecl s ctx tp _ ds -> pPs tp $ classD ds =<< tlhs tp
HsInstDecl s optn c tp ds -> iPs c tp $ instDecl s optn c tp ds
-- HsDefaultDecl s t -> return (hsDefaultDecl s t)
HsTypeSig s nms c tp -> return [] -- just looks ugly...
HsFunBind s matches -> transMatches matches
HsPatBind s p rhs ds -> transPatBind p rhs ds
-- HsInfixDecl s fixity names -> return (hsInfixDecl s fixity names)
HsPrimitiveTypeDecl s ctx tp -> tPs tp $ primTypeD # tlhs tp
HsPrimitiveBind s i t -> primValueD i t
_ -> return [commentdef d]
where
pPs = kPs kpred
tPs = kPs kstar
kPs k lhs m =
do vks <- runKc k (freeTyvars lhs) lhs
extendTyvars' vks m
iPs ctx lhs m =
do vks <- runKc kpred (freeTyvars (ctx,lhs)) lhs
extendTyvars' vks (m [(v,k)|(HsVar v,k)<-vks])
tlhs tp = do (qn, ts) <- U.flatApp' # trans tp
let HsCon n = definedType tp
n' = U.Var (getQualified (getBaseName n))
k <- kinfo tp
return (n,n',k,[x|U.EVar x<-ts])
kinfo tp = do (k,i) <- knd (definedType tp)
k' <- trans k
return (k',i)
-- A hack to be able to use special syntax when defining types in the Prelude:
--unqual (U.EVar n) = n
--unqual (U.EProj (U.EVar (U.Var m)) (U.Label s)) = U.Var s
typeD (_,n,(k,_),xs) t = [valdef n (args xs k) t]
dataD lhs@(_,n,(k,_),xs) cs =
if inPrelude this && reusePreludeFromAlfa n
then primTypeD lhs
else [valdef n (args xs k) (U.ESum cs)]
where
reusePreludeFromAlfa n =
n `elem` map U.Var ["Unit","Bool","List"]
--methodnames ms = ltrans [n|HsVar n<-ns]
-- where ns:>:_ =unzipTyped ms
methodnames ms = [U.Var ("method_"++show i)|i<-[1..length ms]]
classD ds (n,n'@(U.Var nstr),(k,TI.Class ctx vs fdeps ms0),_) =
do let ss=zipWith superMethod [1..] ctx
ms=ss++ms0
vs' <- ltrans (tdom vs)
ms' <- ltrans ms
let ns' = methodnames ms
ds' <- trans{-D-} ds -- default methods
let tsig = args vs' k
cn = {-projSelf-} (U.EVar n')
c = U.app cn (map U.EVar vs')
mds <- concatMapM (methodDecl c ns' vs') (zip ns' ms)
return $ valdef n' (args vs' k) (sig ns' ms'):
defaultMethods ds'++
mds
where
d = U.Var "d"
(cvs,_) = U.flatFun k
{-
defaultMethods ds' =
U.defA $ U.Package (pkg,(U.ctx [],U.PackageDef ds'))
where pkg = U.Var ("default__"++nstr)
-}
defaultMethods = map (U.mapDefB defaultMethod)
defaultMethod (U.Value (U.Var name,rhs)) =
U.Value (U.Var (defaultName name),rhs)
defaultMethod (U.Binding (U.Var name,rhs)) =
U.Binding (U.Var (defaultName name),rhs)
defaultMethod d = d -- comments...
methodDecl c ns' vs' (n',HsVar m:>:s) =
do (gs,qt) <- kcScheme m s
gs' <- ltrans gs
qt' <- extendTyvars gs (trans qt)
let ps = zip vs' cvs++gs'++[(d,c)]
m' <- transUnqualVar m
return $ hide m' ps ++
[valdef m' (ps,([],qt'))
(sigproj ns' n' (map (U.EVar . fst) gs'))
]
superMethod i supercl =
HsVar (superName n i):>:mono supercl
sigproj ns' m' gs' =
U.app (U.EProj (U.EVar d) (var2lbl m')) gs'
dataproj ns' m' gs' =
U.ECase (U.EVar d) [U.Branch (inst,(ns',U.app (U.EVar m') gs'))]
sig ns ms = U.ESig (zipWith method ns ms)
where
method n (U.SigField x t) = U.SigField (var2lbl n) t
sig2data _ ms =
U.ESum [U.Constr (inst,(U.ctx [(lbl2var x,t)|U.SigField x t<-ms],[]))]
inst = U.Con "instance"
primTypeD (_,n,(k,_),xs) =
[if inPrelude this
then preludePrimImportD n
else postulate n (args xs k)]
preludePrimImportD n =preludePrimImportD' n Nothing
preludePrimImportAsD n = preludePrimImportD' n . Just
preludePrimImportD' n as =
U.changeProps (const [U.Public]) $
U.defA (U.Open (pb,[oav' n as]))
where
pb = un "PreludeFromAlfa"
--instDecl s Nothing ctx tp ds vks = undefined
instDecl s (Just n) ctx tp ds vks =
do ctx' <- trans ctx
vks' <- ltrans vks
t <- trans tp
--ds' <- transD ds
ds' <- trans ds
ns <- do (k,TI.Class super _ _ ms) <- kinfo tp
let ns=[n|HsVar n:>:_<-ms]
HsCon c=definedType tp
ss=map (superName c) [1..length super]
ltrans (ss++ns)
let mns = methodnames ns
n' <- trans n
let dicts = xargs ctx'
actx = vks'++dicts
targs = map (U.EVar . fst) vks'
return $
--hide n' vks' ++
[valdef n' (actx,([],t)) (str targs dicts (zip ns mns) ds')]
where
str targs dicts ns2mns ds =
U.EStr (decls (map (U.mapDefB (rename.adjust)) (bindings ds)))
where
adjust (U.Binding (n,e)) = U.Binding (n,adjustmethod e targs dicts)
adjust d = d
rename (U.Value (name,rhs)) = U.Value (mname name,rhs)
rename (U.Binding (name,rhs)) = U.Binding (mname name,rhs)
rename d = d -- comments...
mname n = fromJust (lookup n ns2mns)
{-
str2con targs dicts ns ds = U.app (U.ECon inst) (map conarg ns)
where
conarg n = fromMaybe undef (lookup n ds')
ds' = [(n,adjustmethod e targs dicts)|
U.DefA _ (U.Binding (n,e))<-bindings ds]
-}
adjustmethod e = substds . uapply e
--useDefault (U.Var n) = un (defaultName n)
--undef = U.ePreMetaVar
--undef = eUndefined `uApp` U.ePreMetaVar
bindings = U.rmTypeSign . map (U.mapDefB preserve)
where
preserve d =
case d of
U.Value (name,(ctx@(U.Ctx _ (_:_)),e,t)) | needType e ->
U.Value (name,(ctx,eTyped e t,t))
_ -> d
needType (U.ECase {}) = True
needType _ = False -- sig and data can't occur in instance decls
ifHasType v d m = ifM (inEnv (HsVar v)) m (return [commentdef d])
transMatches ms@(HsMatch _ n _ _ _:_) =
ifHasType n ms $
do sch@(gs,cs:=>t) <- schk (HsVar n)
extendTyvars gs $ do
cs' <- ltrans cs
(xs,rhs) <- umatch this (matchcons ms) # ltrans ms
(targs,tres) <- U.flatFun # trans t
--this <- getMEnv
tctx <- ltrans gs
let (ctx,(xs',tres')) = args' xs (cs'++targs) tres
cnt = length gs+length cs'
n' <- transUnqualVar n
return $
--commentdef sch:
hide' n' cnt++[valdef n' (tctx++ctx,(xs',tres')) rhs]
transPatBind = transVarBind . fromJust' . isVar
fromJust' = fromMaybe (error "Hs2Alfa.hs: pattern bindings not supported")
transVarBind qv rhs ds =
ifHasType qv d $
do v <- transUnqualVar qv
(gs,[]:=>t) <- schk (HsVar qv)
tvs <- ltrans gs
extendTyvars gs $ do
t' <- trans t
extendFrom ds $ do
rhs' <- transR ds rhs
return $ hide v gs ++ [valdef v (tvs, ([],t')) rhs']
primValueD qv t =
do v <- transUnqualVar qv
if inPrelude this
then return [preludePrimImportD v]
else do (gs,[]:=>t) <- schk (HsVar qv)
tvs <- ltrans gs
extendTyvars gs $ do
t' <- trans t
return $ hide v gs ++ [postulate v (tvs, ([], t'))]
commentdef d = U.defA $ U.CommentDef (comment (pp d))
args xs t = uncurry (args' xs) (U.flatFun t)
args' [] ts tres = ([],([],U.eFuns ts tres))
args' (x:xs) (t:ts) tres = apFst ((x,t):) (args' xs ts tres)
args' xs [] tres = ([],(xs,tres))
{- This was used in an attempt to put type and class declarations inside
packages, where auxiliary functions could be put as well without creating
name clashes. But packages can't be recursive so it didn't work.
-}
--packdef v lhs rhs = uPackage v (decls [valdef self lhs rhs])
--self = U.Var "T"
--projSelf e = U.EProj e (U.Label "T")
valdef v (ctx,(xs, t)) rhs =
U.defA $ U.Value (v,(U.ctx ctx,U.uAbsExp xs (rmtannot rhs),t))
rmtannot (U.ETyped e t) = e
rmtannot e = e
typeOf (U.ETyped e t) = Just t
typeOf _ = Nothing
postulate v (ctx,(xs, t)) = U.defA $ U.Axiom (v,(U.ctx ctx,U.uAbsExp xs t))
--typedef v ctx rhs = U.defA $ U.Type (v,(U.ctx ctx,rhs))
eTyped e@(U.ETyped _ _) t = e
eTyped e t = U.ETyped e t
instance (HasId NName e,Trans e U.Exp,Trans p U.Pat,DefinedNames NName p,
Trans ds [U.Def],EnvFrom ds DEnv')
=> Trans (HsMatchI NName e p ds) U.Rule where
trans (HsMatch s _ ps rhs ds) =
(,) # ltrans ps <# (scope ps ds $ transR ds rhs)
transR ds e = eLet # transD ds <# trans e
instance Trans t U.Exp => Trans (HsConDeclI NName t c) U.Constructor where
-- Existential quantification is ignored!!! (Impredicativity problem)
trans (HsConDecl s _ _ n as) = constr # transCon n <# mapM (trans.unbang) as
where
constr n as = U.Constr (nilHack n,(args as,[]))
unbang bt = accBangType const bt ()
args = U.ctx . xargs
nilHack (U.Con "List") = U.Con "Nil"
nilHack c = c
trans (HsRecDecl s _ _ n fs) = constr # transCon n <# concatMapM transFields fs
where
transFields (fs,bt) = fields # mapM trans fs <# trans (unbang bt)
where fields fs t = [(f,t)|f<-fs]
constr n as = U.Constr (n,(U.ctx as,[]))
xargs = zipWith arg [1..]
where arg i t = (U.Var ("x"++show i),t)
instance (HasId NName e,Trans e U.Exp) => Trans (HsRhs e) U.Exp where
transTyped t (HsBody e) = transTyped t e
transTyped t (HsGuard gs) = transGuards gs =<< trans t
where
-- this is a quick hack!!!
transGuards [] t =
do this <- getMEnv
return (eUndefined this `uApp` opt "result type in guarded rhs" t) -- a failed guard
transGuards ((_,g,e):gs) t =
if isTrue g
then trans e
else eIf t # trans g <# trans e <# transGuards gs t
isTrue = maybe False isTrueId . isId
isTrueId x = x `elem` [prelTrue,prelOtherwise]
instance Trans (Assump NName) U.SigPart where
trans (HsVar x:>:t) = U.SigField # transLbl x <# trans t
instance Trans (Scheme NName) U.Exp where
trans s =
do (vs,qt) <- kcScheme "?" s
U.piExp # ltrans vs <# extendTyvars vs (trans qt)
instance Trans t U.Exp => Trans (Qual NName t) U.Exp where
trans (ctx:=>t) = U.eFuns # ltrans ctx <# trans t
instance Trans (HsTypeI NName) U.Exp where trans (Typ t) = trans t
instance Trans NName U.Var where trans x = U.Var # (flip transId x # getMEnv)
transEVar x = inst x
{-
do b <- inEnv x
if b
then do Forall vs (ctx:=>_) <- sch x -- monomorphic recursive call
unless (null vs && null ctx) $
error $"missing type annotation for "++show x
x' <- inst x
vs' <- map U.EVar # ltrans vs
return $ U.app x' (vs'++replicate (length ctx) U.ePreMetaVar)
else inst x -- lambda bound variable
-}
-- Constructors don't need type arguments, but they need to be applied
-- to the right number of values.
transECon c sc ts =
con # inst c <# trans (specialize sc ts)
where
con c t =
eTyped (U.absExp (zipWith (U.:-) ps ts) (U.app c (map U.EVar ps))) t
where
(ts,tr) = U.flatFun t
ps = [U.Var ("conarg"++show n)|n<-[1..length ts]]
specialize (Forall _ gs qt) ts = apply (TI.S (zip (tdom gs) ts)) qt
instance (Printable t,KindCheck NName t Kind,Trans t U.Exp,Types NName t)
=> Trans (TI NName t) U.Exp where
trans t =
case t of
HsTyFun x y -> U.eFun # trans x <# trans y
-- HsTyTuple ts -> U.app . tupleT (length ts) # getMEnv <# ltrans ts
HsTyApp f x -> trans f `tapp` trans x
HsTyVar nm -> do b <- inTEnv (HsVar nm)
if b
then do (k,_) <- knd (HsVar nm)
if k==kprop
then U.EApp (un "predT") # inst (HsVar nm)
else inst (HsVar nm)
else return (missing "type variable not in scope")
HsTyCon nm -> instTcon nm
HsTyForall vs ps t1 ->
do vks <- runKc kstar (map HsVar vs) t1
let vks' = [(v,k)|(HsVar v,k)<-vks] -- grr
U.piExp # ltrans vks' <# extendTyvars' vks (trans t1) -- ps !!!
--ePis vs t = foldr ePi t vs
--ePi (v,k) = U.EPi (v U.:- k)
{-
tupleT n this = uqn (tupleName n)
where
prel = transM mod_Prelude
uqn = if this==prel then un else qn prel
-}
tupleName n = "Tuple"++show (n::Int)
instance Trans Kind U.Exp where
trans (K k) =
case k of
Kstar -> return eStar
Kfun k1 k2 -> U.eFun # trans k1 <# trans k2
Kpred -> return eClass
Kprop -> return ePropKind
consE = U.ECon cons
nilE = U.ECon nil
cons = U.Con "Cons"
nil = U.Con "Nil"
{-
type Pat0 = (U.Con,[U.Var])
instance Trans HsPat Pat0 where
trans (Pat p) =
case p of
HsPId (HsCon c) -> return (transCon c,[])
HsPApp c ps -> return (transCon c,transPVars ps)
HsPList [] -> return (nil,[])
-}
instance Trans (TiPat NName) U.Pat where
trans (Pat p) = trans p
trans (TiPSpec (HsVar v) _ []) = U.PVar # transUnqualVar v
trans (TiPSpec (HsCon c) _ _) = con0P c
trans (TiPTyped p t) = transTyped (Just t) p
trans (TiPApp p1 p2) = papp # trans p1 <# trans p2
where
papp (U.PCon c ps) p = U.PCon c (ps++[p])
papp _ _ = U.PVar noname -- !!!
trans p = --error $ "Not implemented yet: "++pp p
return $ U.PVar noname -- !!!
transTyped t (Pat e) = transTyped t e
transTyped _ e = trans e
-- ...
instance (Printable p,Trans p U.Pat) => Trans (PI NName p) U.Pat where
trans p =
case p of
HsPId (HsCon c) -> con0P c
HsPId (HsVar v) -> U.PVar # transUnqualVar v
HsPApp c ps -> U.PCon # transCon c <# ltrans ps
HsPList s ps -> foldr consP nilP # ltrans ps
HsPTuple s ps -> U.PCon (tupleCon (length ps)) # ltrans ps
HsPInfixApp p1 c p2 -> U.PCon # transCon c <# ltrans [p1,p2]
HsPParen p -> trans p
HsPAsPat v p -> U.PAs # trans v <# trans p
HsPWildCard -> return $ U.PVar noname
HsPIrrPat p -> trans p -- !!
_ -> --error $ "Not implemented yet: "++pp p
return $ U.PVar noname -- !!!
noname = U.Var "__" -- "_" is reserved in Agda nowadays
nilP = U.PCon nil []
consP p1 p2 = U.PCon cons [p1,p2]
con0P c = flip U.PCon [] # transCon c
tupleCon = U.Con . tupleName
--rmtrans e = rmtannot # trans e
rmltrans es = map rmtannot # ltrans es
ptrans (TiPTyped p t) = (,) # trans p <# trans t
lptrans = mapM ptrans
optTransTyped t e = maybe e (eTyped e) # trans t
{-
checkChar x c =
if c<toEnum 0 || c>toEnum 255
then error$ "Unsupported char"++show (fromEnum c)++" in "++show x
else c
-}
checkChar _ c = toEnum (fromEnum c `mod` 256) -- hmm
instance (HasId NName e,Trans e U.Exp,
--AccNames NName p,DefinedNames NName p,HasId NName p,Trans p U.Pat,
Trans ds [U.Def],EnvFrom ds DEnv')
=> Trans (EI NName e (TiPat NName) ds c t) U.Exp where
transTyped t e =
optTransTyped t =<<
case e of
HsId x -> transEVar x
HsLit _ (HsChar c) -> return (U.EChar (checkChar c c))
HsLit _ (HsString s) -> return (U.EString (map (checkChar s) s))
--HsLit _ (HsString s) -> return (U.EString "") -- for a performance test
HsLit _ (HsInt i) -> return (U.EInt i)
HsLit _ (HsFrac x) -> return (U.ERat x)
HsLit _ _ -> return (missing "unimplemented type of literal")
HsInfixApp x op z -> inst op `tapp` trans x `tapp` trans z
HsApp x y -> trans x `tapp` trans y
-- HsNegApp x -> inst prelNegate `tapp` tc x
HsLambda ps e -> do this <- getMEnv
eLambda this (patscons ps) # lptrans ps <# restrictFrom ps (trans e)
HsLet ds e -> eLet # transD ds <# extendFrom ds (trans e)
HsIf x y z -> eIf # trans t <# trans x <# trans y <# trans z
HsCase e alts -> do this <- getMEnv
eCase this (altcons alts) # trans t <# trans e <# ltrans alts
-- HsDo stmts -> tcStmts stmts
HsTuple es -> U.app (U.ECon (tupleCon (length es))) #rmltrans es
HsList es -> foldr (U.app2 consE) nilE # rmltrans es
HsParen e -> trans e
HsLeftSection x op -> inst op `tapp` trans x
HsRightSection op y -> inst pqFlip `tapp` inst op `tapp` trans y
-- HsRecConstr s n fields -> recConstr n fields
-- HsRecUpdate e upds ->
-- HsEnumFrom x -> inst prelEnumFrom `tapp` tc x
-- HsEnumFromTo x y -> inst prelEnumFromTo `tapp` tc x `tapp` tc y
-- HsEnumFromThen x y -> inst prelEnumFromThen `tapp` tc x `tapp` tc y
-- HsEnumFromThenTo x y z ->
-- inst prelEnumFromThenTo `tapp` tc x `tapp` tc y `tapp` tc z
-- HsListComp stmts -> emap hsListComp # tcLComp stmts
-- HsExpTypeSig s e c t -> tcExpTypeSig s e c t
-- Unimplemented things are turned into metavariables:
_ -> return $ missing "unimplemented form of expression"
where
{- recConstr c fs =
case fieldsOf c of
Nothing -> return $ missing bad
Just fns -> do c' <- inst (HsCon c)
let args = map (pick [(orig fn,e)|HsField fn e<-fs]) fns
args' <- mapM (mtrans bad) args
return (U.app c' args')
bad = "bad record construction?"
fieldsOf (PNT c (ConstrOf _ tinfo) _) =
fmap (map orig) . join . listToMaybe $
[conFields ci|ci<-constructors tinfo,orig (conName ci)==orig c]
fieldsOf (PNT c (TypedIds.Class ms) _) = Just (map orig ms)
fieldsOf _ = Nothing -- Not a constructor ?!
pick = flip lookup
-}
pqFlip = mapHsIdent oqual prelFlip
oqual (PNT (PN _ o@(G m n _)) t s) = PNT (PN (Qual m n) o) t s
oqual n = n
mtrans s Nothing = return $ missing s
mtrans s (Just e) = trans e
instance (Trans i1 i2,Trans e1 e2) => Trans (HsFieldI i1 e1) (i2,e2) where
trans (HsField i e) = (,) # trans i <# trans e
instance Trans [HsTypeI NName] [U.Exp] where trans = ltrans
instance (Trans a1 a2,Trans b1 b2) => Trans (a1,b1) (a2,b2) where
trans = trans >#< trans
instance (HasId NName e,Trans e U.Exp,Trans p U.Pat,DefinedNames NName p,
Trans ds [U.Def],EnvFrom ds DEnv')
=> Trans (HsAlt e p ds) U.Rule
where
trans (HsAlt s p rhs ds) =
do p' <- trans p
scope p ds $ do
rhs' <- transR ds rhs
return ([p'], rhs')
sets xs = [(x,eStar)|x<-xs]
--sets xs = [(x,U.ePreMetaVar)|x<-xs]
instTcon c = {-projSelf # -} inst (HsVar c)
inst x = flip inst' x # getMEnv
inst' this (HsCon x) = U.ECon (transCon' this x)
inst' this (HsVar n) = case getBaseName (n::NName) of
UnQual x -> un x
Qual mo x -> qn mo x
qn (PlainModule m) x = U.EProj (un m) (U.Label x)
un = U.EVar . U.Var
--evar = U.EVar . U.Var
{-
transPVar p = transVar (fromJust' . isVar $ p)
where fromJust' = fromMaybe (error "BaseStruct2Alfa.hs: patterns in lambdas are not supported")
transPVars ps = mapM transPVar ps
-}
-- This is used to translate identifiers appearing where only unqualified names
-- are legal, but the abstract syntax allows qualified names
transUnqualVar = transVar . unqual
transCon x = flip transCon' x # getMEnv
transVar x = flip transVar' x # getMEnv
var2lbl (U.Var x) = U.Label x
lbl2var (U.Label x) = U.Var x
transLbl x = var2lbl # transUnqualVar x
transVar' this = U.Var . transId this
transCon' this = U.Con . transId this
--lbl = U.Label # transId
transId this n = transId' this (getBaseName (n::NName))
transId' this (UnQual x) = x
transId' this (Qual mo@(PlainModule m) x) = -- !!!
if mo `elem` this
then x
else m{-++"_"-}++x
--Hmm. Qualified names in definitions won't work...
--Just output something rather than failing immediately.
eClass = un "Class" -- for readability
eStar = un "Star" -- for readability
--eStar = U.eSet -- avoids dependency on nonstd predefined things in Alfa
ePropKind = un "PropKind" -- for readability
eUndefined this =
if inPrelude this
then un "undefined"
else qn (transM mod_Prelude) "undefined"
eLet [] e = e
eLet (U.Decl _ []:ds) e = eLet ds e
eLet ds e = U.ELet ds e -- problem if e is case or sig or ...
eCase this css t e rules = optTyped t (U.subst e v ecase)
where ([v],ecase) = umatch this css rules
optTyped = maybe id (flip eTyped)
eLambda this css tps e0 =
if all uIsVar ps
then U.absExp [x U.:-t|(U.PVar x,t)<-tps] e0
else U.absExp [v U.:-t|(v,t)<-zip vs ts] (f ecase)
where
(ps,ts) = unzip tps
(vs,ecase) = umatch this css [(ps,e)]
(e,f) = case e0 of
U.ETyped e t -> (e,flip eTyped t)
_ -> (e0,id)
altcons alts = patscons [ p | HsAlt s p rhs ds<-alts]
matchcons ms = patscons [ p | HsMatch s _ ps rhs ds<-ms,p<-ps]
-- This can fail if a pattern contains constructors from different types
-- but with the same unqualified name...
patscons = transCons . accCons
where
transCons = (listcons:).map (mapFst con)
con (PN c o) = U.Con (transConName c)
listcons = [(U.Con "Nil",0),(U.Con "Cons",2)]
--tr x = ctrace "cons" x x
accCons ps = accNames con ps []
where
con (PNT c (ConstrOf _ tinfo) _) css =
if cs `elem` css
then css
else cs:css
where cs = tinfo2cs tinfo
con _ css = css
tinfo2cs tinfo = [(c,n)|ConInfo{conName=c,conArity=n}<-constructors tinfo]
eIf t cnd thn els = eIfTyped (opt "result type for if" t') cnd thn els
where t' = t `mplus` typeOf thn `mplus` typeOf els
eIfTyped t cnd thn els = U.app (un "if_then_else") [t,cnd,thn,els]
--eIf cnd thn els = U.ECase cnd [b "True" thn,b "False" els]
-- where b c e = U.Branch (U.Con c,([],e))
umatch this css rules =
case rules of
[(ps,e)] | all uIsVar ps -> ([x|U.PVar x<-ps],e) -- to preserve var names
_ -> U.exhaustiveMatch'' css [] rules undef
where
undef = eUndefined this `uApp` missing "potential pattern match failure"
uIsVar (U.PVar _) = True
uIsVar _ = False
m1 `tapp` m2 = uApp # m1 <# m2
e1 `uApp` e2 =
case e1 of
-- Agda doesn't like applied meta variables:
U.EMeta _ -> e1
U.EAnnot a (U.EMeta _) -> e1
-- Agda doesn't like beta redexes:
U.ETyped (U.EAbs (x U.:-_) e1') (U.EPi _ t) -> U.subst e2 x e1' `eTyped` t
U.EAbs x e1' -> uLet x e2 e1'
--U.ETyped e1' (U.EPi _ t) -> (e1' `uApp` e2) `eTyped` t
_ -> U.EApp e1 e2
where
-- Avoid code duplication, if possible without name capture
-- (there are no non-recursive declarations in Agda)
uLet (x U.:-t) e2 e1 =
if x `elem` U.free e2
then U.subst e2 x e1
else U.ELet [U.decl' [valdef x (([],([],t))) e2]] e1
getDEnv = snd # getEnv
getMEnv = fst # getEnv
Since the type checker doesn't provide kind information for type variables in type schemes, we do a local kind inference on the type scheme. I am not quite sure this is enough to always get the right kinds...
schk x = kcScheme x =<< sch x
schak x = akcScheme x =<< sch x
kcScheme _ (Forall _ vs qt) = return ([(v,k)|v:>:k<-vs],qt)
akcScheme _ (Forall as vs qt) = return ([(v,k)|v:>:k<-as++vs],qt)
{-
kcScheme x (Forall [] qt) = return ([],qt) -- shortcut
kcScheme x (Forall vs qt) =
do vks <- runKc' x kstar (map HsVar (tdom vs)) qt
return ([(v,k)|(HsVar v,k)<-vks],qt)
--}
--runKcStar = runKc kstar
runKc = runKc' ""
runKc' s k vs qt =
do kenv <- fst # getDEnv
vkts <- lift (errorContext (pp (s,vs,qt,k)) $
extendkts kenv $ kgeneraliseSloppy $
do bs <- kintro vs
bs' <- kintro (map HsVar (tv qt)\\vs) -- hmm
k' <- extendkts (bs++bs') $ kc qt
let _ = k' `asTypeOf` k
return bs)
return [(v,k)|v:>:(k,_)<-vkts]
sch x = lookupts x . snd # getDEnv
knd x = lookupts x . fst # getDEnv
inEnv x = (elem x . map tfst . snd) # getDEnv
inTEnv v = (elem v . map tfst . fst) # getDEnv
tfst (x:>:_) = x
lookupts x [] = error ("Not in scope:"++show x)
lookupts x ((y:>:t):ts) = if x==y then t else lookupts x ts
eCmnt = U.eComment . comment
comment s = "{- "++s++" -}"
annot s = "{-# Alfa "++s++" #-}"
missing s = eCmnt s U.ePreMetaVar
opt = fromMaybe . missing
hide v = hide' v . length
hide' (U.Var v) cnt =
if cnt>0
then [U.defA $ U.CommentDef $ annot s]
else []
where
s = --U.printIdOptions (U.name v,(U.defaultArgOptions v){U.hideCnt=cnt})
"var "++show v++" hide "++show cnt
---}
uapply e [] = e
uapply (U.EAbs (x U.:-_) e) (a:as) = uapply (U.subst a x e) as
uapply e as = U.app e as -- hmm
substds e [] = e
substds e@(U.EAbs p@(x U.:-t) b) ds =
case partition (sameT t) ds of
((d,_):ds1,ds2) -> substds (U.subst (U.EVar d) x b) (ds1++ds2)
([],ds2) -> U.EAbs p (substds b ds2) -- assume p is a type parameter
-- _ -> U.eComment (comment $ "Something went wrong here: dictionary argument type mismatch: "++show t) e -- Hmm
where
sameT t (_,t') = t==t'
substds e _ = U.eComment (comment "Something went wrong here: too many dictionary arguments?") e -- Hmm