module ToHaskell where

{- type-directed extraction of Haskell programs with a lot of unsafeCoerce

Examples:
---------

MiniAgda

  data Vec (A : Set) : Nat -> Set
  { vnil  : Vec A zero
  ; vcons : [n : Nat] -> (head : A) -> (tail : Vec A n) -> Vec A (suc n)
  }

  fun length : [A : Set] -> [n : Nat] -> Vec A n -> <n : Nat>
  { length .A .zero    (vnil A)         = zero
  ; length .A .(suc n) (vcons A n a as) = suc (length A n as)
  }

Haskell

  {-# LANGUAGE NoImplicitPrelude #-}
  module Main where
  import qualified Text.Show as Show

  data Vec (a :: *)
    = Vec_vnil
    | Vec_vcons { vec_head :: a , vec_tail :: Vec a }
      deriving Show.Show

  length :: forall a. Vec a -> Nat
  length  Vec_vnil        = Nat_zero
  length (Vec_vcons a as) = Nat_suc (length as)

Components:
-----------

Translation from MiniAgda identifiers to Haskell identifiers

-}

import Prelude hiding (null)

import Data.Char

#if !MIN_VERSION_base(4,8,0)
import Control.Applicative ((<$>), (<*>))
#endif
import Control.Monad
import Control.Monad.Except (ExceptT, runExceptT)
import Control.Monad.Reader (ReaderT, runReaderT)
import Control.Monad.State  (StateT, evalStateT)

import qualified Data.Traversable as Trav

import qualified Language.Haskell.Exts.Syntax as Hs

import Polarity
import Abstract
import Extract
import qualified HsSyntax as H
import TraceError
import Util

-- translation monad

type Translate = StateT TState (ReaderT TContext (ExceptT TraceError IO))

{- no longer needed with mtl-2
instance Applicative Translate where
  pure      = return
  mf <*> ma = do { f <- mf; a <- ma; return (f a) }
-}

data TState = TState

initSt :: TState
initSt :: TState
initSt = TState
TState

data TContext = TContext

initCxt :: TContext
initCxt :: TContext
initCxt = TContext
TContext

runTranslate :: Translate a -> IO (Either TraceError a)
runTranslate :: forall a. Translate a -> IO (Either TraceError a)
runTranslate Translate a
t = ExceptT TraceError IO a -> IO (Either TraceError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ReaderT TContext (ExceptT TraceError IO) a
-> TContext -> ExceptT TraceError IO a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Translate a -> TState -> ReaderT TContext (ExceptT TraceError IO) a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Translate a
t TState
initSt) TContext
initCxt)

-- translation

translateModule :: [EDeclaration] -> Translate (H.Module)
translateModule :: [EDeclaration] -> Translate Module
translateModule [EDeclaration]
ds = do
  hs <- [EDeclaration] -> Translate [Decl]
translateDecls [EDeclaration]
ds
  return $ H.mkModule hs

translateDecls :: [EDeclaration] -> Translate [H.Decl]
translateDecls :: [EDeclaration] -> Translate [Decl]
translateDecls [EDeclaration]
ds = [[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Decl]] -> [Decl])
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) [[Decl]]
-> Translate [Decl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EDeclaration -> Translate [Decl])
-> [EDeclaration]
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) [[Decl]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM EDeclaration -> Translate [Decl]
translateDecl [EDeclaration]
ds

translateDecl :: EDeclaration -> Translate [H.Decl]
translateDecl :: EDeclaration -> Translate [Decl]
translateDecl EDeclaration
d =
  case EDeclaration
d of
    MutualDecl Bool
_ [EDeclaration]
ds -> [EDeclaration] -> Translate [Decl]
translateDecls [EDeclaration]
ds
    OverrideDecl{} -> String -> Translate [Decl]
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> Translate [Decl]) -> String -> Translate [Decl]
forall a b. (a -> b) -> a -> b
$ String
"translateDecls internal error: overrides impossible"
    MutualFunDecl Bool
_ Co
_ [Fun]
funs -> [Fun] -> Translate [Decl]
translateFuns [Fun]
funs
    FunDecl Co
_ Fun
fun -> Fun -> Translate [Decl]
translateFun Fun
fun
    LetDecl Bool
_ Name
x Telescope
tel (Just FKind
t) FKind
e | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel -> Name -> FKind -> FKind -> Translate [Decl]
translateLet Name
x FKind
t FKind
e
    DataDecl Name
n Sized
_ Co
_ [Pol]
_ Telescope
tel FKind
fkind [Constructor]
cs [Name]
_ -> Name -> Telescope -> FKind -> [Constructor] -> Translate [Decl]
translateDataDecl Name
n Telescope
tel FKind
fkind [Constructor]
cs

translateFuns :: [Fun] -> Translate [H.Decl]
translateFuns :: [Fun] -> Translate [Decl]
translateFuns [Fun]
funs = [[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Decl]] -> [Decl])
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) [[Decl]]
-> Translate [Decl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Fun -> Translate [Decl])
-> [Fun]
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) [[Decl]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Fun -> Translate [Decl]
translateFun [Fun]
funs

translateFun :: Fun -> Translate [H.Decl]
translateFun :: Fun -> Translate [Decl]
translateFun (Fun ts :: TypeSig
ts@(TypeSig Name
n FKind
t) Name
n' Arity
ar [Clause]
cls) = do
  ts@(Hs.TypeSig _ [n] t) <- TypeSig -> Translate Decl
translateTypeSig TypeSig
ts
  cls <- concat <$> mapM (translateClause n) cls
  return [ts, H.hFunBind cls]

translateLet :: Name -> Type -> FExpr -> Translate [H.Decl]
translateLet :: Name -> FKind -> FKind -> Translate [Decl]
translateLet Name
n FKind
t FKind
e
  | Name -> Bool
isEtaAlias Name
n = [Decl] -> Translate [Decl]
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []  -- skip internal decls
  | Bool
otherwise = do
      ts <- TypeSig -> Translate Decl
translateTypeSig (TypeSig -> Translate Decl) -> TypeSig -> Translate Decl
forall a b. (a -> b) -> a -> b
$ Name -> FKind -> TypeSig
forall a. Name -> a -> TySig a
TypeSig Name
n FKind
t
      e  <- translateExpr e
      n  <- hsName (DefId LetK $ QName n)
      return [ ts, H.mkLet n e ]

translateTypeSig :: TypeSig -> Translate H.Decl
translateTypeSig :: TypeSig -> Translate Decl
translateTypeSig (TypeSig Name
n FKind
t) = do
  n <- DefId -> Translate (Name ())
hsName (IdKind -> QName -> DefId
DefId IdKind
LetK (QName -> DefId) -> QName -> DefId
forall a b. (a -> b) -> a -> b
$ Name -> QName
QName Name
n)
  t <- translateType t
  return $ H.mkTypeSig n t

translateDataDecl :: Name -> FTelescope -> FKind -> [FConstructor] -> Translate [H.Decl]
translateDataDecl :: Name -> Telescope -> FKind -> [Constructor] -> Translate [Decl]
translateDataDecl Name
n Telescope
tel FKind
k [Constructor]
cs = do
  n   <- DefId -> Translate (Name ())
hsName (IdKind -> QName -> DefId
DefId IdKind
DatK (QName -> DefId) -> QName -> DefId
forall a b. (a -> b) -> a -> b
$ Name -> QName
QName Name
n)
  tel <- translateTelescope tel
  let k' = FKind -> Type ()
translateKind FKind
k
  cs  <- mapM translateConstructor cs
  return [H.mkDataDecl n tel k' cs]

translateConstructor :: FConstructor -> Translate H.GadtDecl
translateConstructor :: Constructor
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) GadtDecl
translateConstructor (Constructor QName
n ParamPats
pars FKind
t) = do
  n  <- DefId -> Translate (Name ())
hsName (IdKind -> QName -> DefId
DefId (ConK -> IdKind
ConK ConK
Cons) QName
n)
  t' <- translateType t
  return $ H.mkConDecl n t'

translateClause :: H.Name -> Clause -> Translate [H.Match]
translateClause :: Name ()
-> Clause
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) [Match]
translateClause Name ()
n (Clause TeleVal
_ [Pattern]
ps (Just FKind
rhs)) = do
  ps <- (Pattern
 -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat)
-> [Pattern]
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) [Pat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Pattern
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat
translatePattern [Pattern]
ps
  rhs <- translateExpr rhs
  return [H.mkClause n ps rhs]

translateTelescope :: FTelescope -> Translate [H.TyVarBind]
translateTelescope :: Telescope -> Translate [TyVarBind]
translateTelescope (Telescope [TBind]
tel) = (TBind
 -> StateT
      TState (ReaderT TContext (ExceptT TraceError IO)) TyVarBind)
-> [TBind] -> Translate [TyVarBind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TBind
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) TyVarBind
translateTBind [TBind]
tel'
  -- throw away erasure marks
  where tel' :: [TBind]
tel' = (TBind -> Bool) -> [TBind] -> [TBind]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ TBind
tb -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dec -> Bool) -> Dec -> Bool
forall a b. (a -> b) -> a -> b
$ Dom FKind -> Dec
forall a. Dom a -> Dec
decor (Dom FKind -> Dec) -> Dom FKind -> Dec
forall a b. (a -> b) -> a -> b
$ TBind -> Dom FKind
forall a. TBinding a -> Dom a
boundDom TBind
tb) [TBind]
tel

translateTBind :: TBind -> Translate H.TyVarBind
translateTBind :: TBind
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) TyVarBind
translateTBind (TBind Name
x Dom FKind
dom) = do
  x <- Name -> Translate (Name ())
hsVarName Name
x
  return $ H.hKindedVar x $ translateKind (typ dom)

translateKind :: FKind -> H.Kind
translateKind :: FKind -> Type ()
translateKind FKind
k =
  case FKind
k of
    FKind
k | FKind
k FKind -> FKind -> Bool
forall a. Eq a => a -> a -> Bool
== FKind
star -> Type ()
H.hKindStar
    Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k' | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dom FKind -> Dec
forall a. Dom a -> Dec
decor Dom FKind
dom) -> FKind -> Type ()
translateKind FKind
k'
    Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k' ->
      FKind -> Type ()
translateKind (Dom FKind -> FKind
forall a. Dom a -> a
typ Dom FKind
dom) Type () -> Type () -> Type ()
`H.mkKindFun` FKind -> Type ()
translateKind FKind
k'

translateType :: FType -> Translate H.Type
translateType :: FKind -> Translate (Type ())
translateType FKind
t =
  case FKind
t of

    FKind
Irr -> Type () -> Translate (Type ())
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type () -> Translate (Type ())) -> Type () -> Translate (Type ())
forall a b. (a -> b) -> a -> b
$ Type ()
H.unit_tycon

    Quant PiSigma
piSig (TBind Name
_ Dom FKind
dom) FKind
b | Bool -> Bool
not (Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dom FKind -> Dec
forall a. Dom a -> Dec
decor Dom FKind
dom)) ->
      PiSigma -> Type () -> Type () -> Type ()
H.mkTyPiSig PiSigma
piSig (Type () -> Type () -> Type ())
-> Translate (Type ())
-> StateT
     TState
     (ReaderT TContext (ExceptT TraceError IO))
     (Type () -> Type ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FKind -> Translate (Type ())
translateType (Dom FKind -> FKind
forall a. Dom a -> a
typ Dom FKind
dom) StateT
  TState
  (ReaderT TContext (ExceptT TraceError IO))
  (Type () -> Type ())
-> Translate (Type ()) -> Translate (Type ())
forall a b.
StateT TState (ReaderT TContext (ExceptT TraceError IO)) (a -> b)
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FKind -> Translate (Type ())
translateType FKind
b

    Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
b | Dom FKind -> FKind
forall a. Dom a -> a
typ Dom FKind
dom FKind -> FKind -> Bool
forall a. Eq a => a -> a -> Bool
== FKind
Irr -> FKind -> Translate (Type ())
translateType FKind
b

    Quant PiSigma
Pi (TBind Name
x Dom FKind
dom) FKind
b -> do
      x <- Name -> Translate (Name ())
hsVarName Name
x
      let k = FKind -> Type ()
translateKind (Dom FKind -> FKind
forall a. Dom a -> a
typ Dom FKind
dom)
      -- todo: add x to context
      t <- translateType b
      return $ H.mkForall x k t

    App FKind
f FKind
a -> Type () -> Type () -> Type ()
H.mkTyApp (Type () -> Type () -> Type ())
-> Translate (Type ())
-> StateT
     TState
     (ReaderT TContext (ExceptT TraceError IO))
     (Type () -> Type ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FKind -> Translate (Type ())
translateType FKind
f StateT
  TState
  (ReaderT TContext (ExceptT TraceError IO))
  (Type () -> Type ())
-> Translate (Type ()) -> Translate (Type ())
forall a b.
StateT TState (ReaderT TContext (ExceptT TraceError IO)) (a -> b)
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FKind -> Translate (Type ())
translateType FKind
a

    Def d :: DefId
d@(DefId IdKind
DatK QName
n) -> (QName () -> Type ()
H.hTyCon (QName () -> Type ())
-> (Name () -> QName ()) -> Name () -> Type ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name () -> QName ()
H.hUnQual) (Name () -> Type ()) -> Translate (Name ()) -> Translate (Type ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefId -> Translate (Name ())
hsName DefId
d

    Var Name
x -> Name () -> Type ()
H.hTyVar (Name () -> Type ()) -> Translate (Name ()) -> Translate (Type ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Translate (Name ())
hsVarName Name
x

    FKind
_ -> Type () -> Translate (Type ())
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Type ()
H.unit_tycon

{- TODO:
    _ -> throwErrorMsg $ "no Haskell representation for type " ++ show t
 -}

translateExpr :: FExpr -> Translate H.Exp
translateExpr :: FKind -> Translate Exp
translateExpr FKind
e =
  case FKind
e of

    Var Name
x -> Name () -> Exp
H.mkVar (Name () -> Exp) -> Translate (Name ()) -> Translate Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Translate (Name ())
hsVarName Name
x

    -- constructors
    Def f :: DefId
f@(DefId (ConK{}) QName
n) -> Name () -> Exp
H.mkCon (Name () -> Exp) -> Translate (Name ()) -> Translate Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefId -> Translate (Name ())
hsName DefId
f

    -- function identifiers
    Def f :: DefId
f@(DefId IdKind
_ QName
n) -> Name () -> Exp
H.mkVar (Name () -> Exp) -> Translate (Name ()) -> Translate Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefId -> Translate (Name ())
hsName DefId
f

    -- discard type arguments
    App FKind
f FKind
e0 -> do
      f <- FKind -> Translate Exp
translateExpr FKind
f
      let (er, e) = isErasedExpr e0
      if er then return f else H.mkApp f <$> translateExpr e

    -- discard type lambdas
    Lam Dec
dec Name
y FKind
e -> do
      y <- Name -> Translate (Name ())
hsVarName Name
y
      e <- translateExpr e
      return $ if erased dec then e else H.mkLam y e

    LLet (TBind Name
x Dom (Maybe FKind)
dom) Telescope
tel FKind
e1 FKind
e2 | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel-> do
      x  <- Name -> Translate (Name ())
hsVarName Name
x
      e2 <- translateExpr e2
      if erased (decor dom) then return e2 else do
        t  <- Trav.mapM translateType (typ dom)
        e1 <- translateExpr e1
        return $ H.mkLLet x t e1 e2

    Pair FKind
e1 FKind
e2 -> Exp -> Exp -> Exp
H.mkPair (Exp -> Exp -> Exp)
-> Translate Exp
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) (Exp -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FKind -> Translate Exp
translateExpr FKind
e1 StateT
  TState (ReaderT TContext (ExceptT TraceError IO)) (Exp -> Exp)
-> Translate Exp -> Translate Exp
forall a b.
StateT TState (ReaderT TContext (ExceptT TraceError IO)) (a -> b)
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FKind -> Translate Exp
translateExpr FKind
e2

    -- TODO

    Ann (Tagged [Tag
Cast] FKind
e) -> Exp -> Exp
H.mkCast (Exp -> Exp) -> Translate Exp -> Translate Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FKind -> Translate Exp
translateExpr FKind
e

    FKind
_ -> Exp -> Translate Exp
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> Translate Exp) -> Exp -> Translate Exp
forall a b. (a -> b) -> a -> b
$ () -> Exp
forall l. l -> Exp l
Hs.unit_con ()

translatePattern :: Pattern -> Translate H.Pat
translatePattern :: Pattern
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat
translatePattern Pattern
p =
  case Pattern
p of
    VarP Name
y       -> Name () -> Pat
H.hPVar (Name () -> Pat)
-> Translate (Name ())
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Translate (Name ())
hsVarName Name
y
    PairP Pattern
p1 Pattern
p2  -> Boxed -> [Pat] -> Pat
H.hPTuple Boxed
Hs.Boxed ([Pat] -> Pat)
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) [Pat]
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern
 -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat)
-> [Pattern]
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) [Pat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Pattern
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat
translatePattern [Pattern
p1,Pattern
p2]
    ConP PatternInfo
pi QName
n [Pattern]
ps ->
       QName () -> [Pat] -> Pat
H.hPApp (QName () -> [Pat] -> Pat)
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) (QName ())
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) ([Pat] -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name () -> QName ()
H.hUnQual (Name () -> QName ())
-> Translate (Name ())
-> StateT
     TState (ReaderT TContext (ExceptT TraceError IO)) (QName ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefId -> Translate (Name ())
hsName (IdKind -> QName -> DefId
DefId (ConK -> IdKind
ConK (ConK -> IdKind) -> ConK -> IdKind
forall a b. (a -> b) -> a -> b
$ PatternInfo -> ConK
coPat PatternInfo
pi) QName
n))
               StateT
  TState (ReaderT TContext (ExceptT TraceError IO)) ([Pat] -> Pat)
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) [Pat]
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat
forall a b.
StateT TState (ReaderT TContext (ExceptT TraceError IO)) (a -> b)
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Pattern
 -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat)
-> [Pattern]
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) [Pat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Pattern
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) Pat
translatePattern [Pattern]
ps

{-
Name translation

  data names        : check capitalization, identity translation
  constructor names : prefix with Dataname_
  destructor names  : ditto
  type-valued lets  : check capitalization, identity
  type-valued funs  : reject!
  lets              : check lowercase
  funs/cofuns       : check lowercase
-}

hsVarName :: Name -> Translate H.Name
hsVarName :: Name -> Translate (Name ())
hsVarName Name
x = Name () -> Translate (Name ())
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name () -> Translate (Name ())) -> Name () -> Translate (Name ())
forall a b. (a -> b) -> a -> b
$ String -> Name ()
H.hIdent (String -> Name ()) -> String -> Name ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
x

hsName :: DefId -> Translate H.Name
hsName :: DefId -> Translate (Name ())
hsName DefId
id = String -> Translate (Name ()) -> Translate (Name ())
forall (m :: * -> *) a.
MonadError TraceError m =>
String -> m a -> m a
enter (String
"error translating identifier " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DefId -> String
forall a. Show a => a -> String
show DefId
id) (Translate (Name ()) -> Translate (Name ()))
-> Translate (Name ()) -> Translate (Name ())
forall a b. (a -> b) -> a -> b
$
  case DefId
id of
  (DefId IdKind
DatK (QName Name
x)) -> do
    let n :: String
n = Name -> String
suggestion Name
x
    Bool
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) ()
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Char -> Bool
isUpper (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
forall a. HasCallStack => [a] -> a
head String
n) (StateT TState (ReaderT TContext (ExceptT TraceError IO)) ()
 -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) ())
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) ()
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) ()
forall a b. (a -> b) -> a -> b
$
      String
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) ()
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String
 -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) ())
-> String
-> StateT TState (ReaderT TContext (ExceptT TraceError IO)) ()
forall a b. (a -> b) -> a -> b
$ String
"data names need to be capitalized"
    Name () -> Translate (Name ())
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name () -> Translate (Name ())) -> Name () -> Translate (Name ())
forall a b. (a -> b) -> a -> b
$ String -> Name ()
H.hIdent String
n
  (DefId (ConK ConK
co) (Qual Name
d Name
x)) -> do
    let n :: String
n = Name -> String
suggestion Name
x
        m :: String
m = Name -> String
suggestion Name
d
    Name () -> Translate (Name ())
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name () -> Translate (Name ())) -> Name () -> Translate (Name ())
forall a b. (a -> b) -> a -> b
$ String -> Name ()
H.hIdent (String -> Name ()) -> String -> Name ()
forall a b. (a -> b) -> a -> b
$ String
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n
    -- dataName <- getDataName x
    -- return $ H.hIdent $ dataName ++ "_" ++ n
  -- lets, funs, cofuns. TODO: type-valued funs!
--   (DefId Let ('_':n)) | -> return $ H.hIdent n
  (DefId IdKind
_ QName
x) -> do
    let n :: String
n = Name -> String
suggestion (Name -> String) -> Name -> String
forall a b. (a -> b) -> a -> b
$ QName -> Name
unqual QName
x
{- ignore for now
     unless (isLower $ head n) $
       throwErrorMsg $ "function names need to start with a lowercase letter"
 -}
    Name () -> Translate (Name ())
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name () -> Translate (Name ())) -> Name () -> Translate (Name ())
forall a b. (a -> b) -> a -> b
$ String -> Name ()
H.hIdent String
n

-- getDataName constructorName = return dataNamec
getDataName :: Name -> Translate String
getDataName :: Name -> Translate String
getDataName Name
n = String -> Translate String
forall a.
a -> StateT TState (ReaderT TContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"DATA"