content: 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
  