{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ExtendedDefaultRules #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}

module Embedder.Atmo.ToIsabelle where

import Control.Arrow (second)
import safe Embedder.Isabelle.Syntax as Isa
    ( Theory(..),
      DatatypeConstructor(..), Decl(..),
      Term(..), Typ(..), TypSig(..), TName, Pttrn(..))
import safe Embedder.Atmo.Syntax as A
    ( FreeProgram, Module (..),
      TypeSynonym(..), DataDefn(..), Defn(..),
      Exp(..), Ty(..), Poly(..),
      DataCon(..), Pat (..), PatBind (..), FunBinding (..), RecDefn (..))
import ReWire.Orphans ()
import ReWire.Error (AstError, MonadError, failAt)
import Embedder.Atmo.Types (flattenSig, nilTy, pairTy, TypeAnnotated (..))
import Embedder.Atmo.Util(isPrim, flattenLam)

import System.FilePath(takeBaseName)
import Data.Char (isDigit)
import Data.List (isPrefixOf)
import qualified Data.Text as T (Text, pack, splitOn, map, filter, null, head, last)
import Data.Graph (Graph, Vertex, Tree (..))
import Embedder.Atmo.DependencyGraph (Declaration (..), sortFreeProgram)
import Embedder.Atmo.FlattenMonadTrans (transMonadT)
import Data.Text (Text)


---------- Todos/Questions --------------
-- TODO: Implement Case translation in the Isabelle ReWire session (targets/isabelle/thys) [and modify this translation to suit]
-- TODO: Implement translation of Builtins/Prims (hopefully can be ported over from the Source translation)
-- TODO: Readability concerns?

---------- ================================================= ----------

-- Translating Programs

{- data Theory = Theory
  { thyName :: T.Text
  , imports :: [Text]
  , decls :: [Decl] } -}

-- | The rewire-user library modules, by theory name. Their Isabelle
--   semantics is the hand-written session (targets\/isabelle\/thys, imported
--   as @ReWire.Atmo@), so embedding them would emit theories nothing
--   imports. Matched against the theory name rather than the output path,
--   which @-o@ overrides.
rewireUserMods :: [Text]
rewireUserMods :: [Text]
rewireUserMods = [Text
"ReWire",Text
"Bits",Text
"BitWord",Text
"Finite",Text
"FiniteComp"
                 ,Text
"Monad",Text
"Prelude",Text
"Vectors",Text
"Primitives"]

embedModule :: (MonadError AstError m) => FilePath -> A.Module -> m (Maybe Isa.Theory)
embedModule :: forall (m :: * -> *).
MonadError AstError m =>
[Char] -> Module -> m (Maybe Theory)
embedModule [Char]
filename Module
mod = do
    let thyname :: Text
thyname = [Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
takeBaseName [Char]
filename
    if Text
thyname Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
rewireUserMods
      then Maybe Theory -> m (Maybe Theory)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Theory
forall a. Maybe a
Nothing
      else do
            (decls,_graph,_tree) <- Module -> m ([Decl], Graph, [Tree Vertex])
forall (m :: * -> *).
MonadError AstError m =>
Module -> m ([Decl], Graph, [Tree Vertex])
tModule Module
mod
            return $ Just $ Theory thyname ["Main","ReWire.Atmo"] decls

embedFreeProgram :: (MonadError AstError m) => FilePath -> A.FreeProgram -> m Isa.Theory
embedFreeProgram :: forall (m :: * -> *).
MonadError AstError m =>
[Char] -> FreeProgram -> m Theory
embedFreeProgram [Char]
filename FreeProgram
prog = do
    let thyname :: Text
thyname = [Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
takeBaseName [Char]
filename
    (decls,_graph,_tree) <- FreeProgram -> m ([Decl], Graph, [Tree Vertex])
forall (m :: * -> *).
MonadError AstError m =>
FreeProgram -> m ([Decl], Graph, [Tree Vertex])
tFreeProgram FreeProgram
prog
    return $ Theory thyname ["Main","ReWire.Atmo"] decls


{- type FreeProgram = ([DataDefn], [RecDefn], [TypeSynonym], [Defn]) -}
tFreeProgram :: (MonadError AstError m) => A.FreeProgram -> m ([Isa.Decl], Graph, [Tree Vertex] )
tFreeProgram :: forall (m :: * -> *).
MonadError AstError m =>
FreeProgram -> m ([Decl], Graph, [Tree Vertex])
tFreeProgram ([DataDefn]
data_defs, [RecDefn]
rec_defs, [TypeSynonym]
type_syns, [Defn]
definitions) =
      let ddfs :: [DataDefn]
ddfs = (DataDefn -> Bool) -> [DataDefn] -> [DataDefn]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (DataDefn -> Bool) -> DataDefn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
forall a. Show a => a -> Bool
isReWire (Text -> Bool) -> (DataDefn -> Text) -> DataDefn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDefn -> Text
dataName) [DataDefn]
data_defs
          tsyns :: [TypeSynonym]
tsyns = (TypeSynonym -> Bool) -> [TypeSynonym] -> [TypeSynonym]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TypeSynonym -> Bool) -> TypeSynonym -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
forall a. Show a => a -> Bool
isReWire (Text -> Bool) -> (TypeSynonym -> Text) -> TypeSynonym -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSynonym -> Text
typeSynName) [TypeSynonym]
type_syns
          defs :: [Defn]
defs = (Defn -> Bool) -> [Defn] -> [Defn]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Defn -> Bool) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
forall a. Show a => a -> Bool
isReWire (Text -> Bool) -> (Defn -> Text) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Text
defnName) [Defn]
definitions
          fprog :: FreeProgram
fprog = ([DataDefn]
ddfs,[RecDefn]
rec_defs,[TypeSynonym]
tsyns,[Defn]
defs)
          ([Declaration]
decls,Graph
graph,[Tree Vertex]
tree) = FreeProgram -> ([Declaration], Graph, [Tree Vertex])
sortFreeProgram FreeProgram
fprog
      in do
            decls' <- (Declaration -> m Decl) -> [Declaration] -> m [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 Declaration -> m Decl
forall (m :: * -> *).
MonadError AstError m =>
Declaration -> m Decl
tDeclaration [Declaration]
decls
            return (decls', graph, tree)

tModule :: (MonadError AstError m) => A.Module -> m ([Isa.Decl], Graph, [Tree Vertex] )
tModule :: forall (m :: * -> *).
MonadError AstError m =>
Module -> m ([Decl], Graph, [Tree Vertex])
tModule (A.Module [DataDefn]
data_defs [RecDefn]
rec_defs [TypeSynonym]
type_syns [Defn]
definitions) =
      let ddfs :: [DataDefn]
ddfs = (DataDefn -> Bool) -> [DataDefn] -> [DataDefn]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (DataDefn -> Bool) -> DataDefn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
forall a. Show a => a -> Bool
isReWire (Text -> Bool) -> (DataDefn -> Text) -> DataDefn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDefn -> Text
dataName) [DataDefn]
data_defs
          tsyns :: [TypeSynonym]
tsyns = (TypeSynonym -> Bool) -> [TypeSynonym] -> [TypeSynonym]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TypeSynonym -> Bool) -> TypeSynonym -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
forall a. Show a => a -> Bool
isReWire (Text -> Bool) -> (TypeSynonym -> Text) -> TypeSynonym -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSynonym -> Text
typeSynName) [TypeSynonym]
type_syns
          defs :: [Defn]
defs = (Defn -> Bool) -> [Defn] -> [Defn]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Defn -> Bool) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
forall a. Show a => a -> Bool
isReWire (Text -> Bool) -> (Defn -> Text) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Text
defnName) [Defn]
definitions
          fprog :: FreeProgram
fprog = ([DataDefn]
ddfs,[RecDefn]
rec_defs,[TypeSynonym]
tsyns,[Defn]
defs)
          ([Declaration]
decls,Graph
graph,[Tree Vertex]
tree) = FreeProgram -> ([Declaration], Graph, [Tree Vertex])
sortFreeProgram FreeProgram
fprog
      in do
            decls' <- (Declaration -> m Decl) -> [Declaration] -> m [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 Declaration -> m Decl
forall (m :: * -> *).
MonadError AstError m =>
Declaration -> m Decl
tDeclaration [Declaration]
decls
            return (decls', graph, tree)

---------- ================================================= ----------

-- Translating Declarations

tDeclaration :: (MonadError AstError m) => Declaration -> m Isa.Decl
tDeclaration :: forall (m :: * -> *).
MonadError AstError m =>
Declaration -> m Decl
tDeclaration = \ case
     DDecl DataDefn
d -> DataDefn -> m Decl
forall (m :: * -> *). Monad m => DataDefn -> m Decl
tDataDefn DataDefn
d
     TDecl TypeSynonym
d -> TypeSynonym -> m Decl
forall (m :: * -> *). Monad m => TypeSynonym -> m Decl
tTypeSynonym TypeSynonym
d
     FDecl Defn
d -> Defn -> m Decl
forall (m :: * -> *). MonadError AstError m => Defn -> m Decl
tDefn Defn
d
     RDecl [Defn]
ds -> [Defn] -> m Decl
forall (m :: * -> *). MonadError AstError m => [Defn] -> m Decl
tRDefns [Defn]
ds
     RecDecl RecDefn
d -> RecDefn -> m Decl
forall (m :: * -> *). Monad m => RecDefn -> m Decl
tRecDefn RecDefn
d




tTypeSynonym :: Monad m => A.TypeSynonym -> m Isa.Decl
tTypeSynonym :: forall (m :: * -> *). Monad m => TypeSynonym -> m Decl
tTypeSynonym (A.TypeSynonym Annote
_a Text
name Poly
poly) = do
     (tvs, t) <- Poly -> m ([Text], Typ)
forall (m :: * -> *). Monad m => Poly -> m ([Text], Typ)
tPoly Poly
poly
     return $ Isa.TypeSynonym (tGlobal name) tvs t


tDefn :: (MonadError AstError m) => A.Defn -> m Isa.Decl
tDefn :: forall (m :: * -> *). MonadError AstError m => Defn -> m Decl
tDefn =  \ case
   Defn Annote
a Text
_name Poly
_poly Maybe DefnAttr
_defnattr [] -> Annote -> Text -> m Decl
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
a Text
"should not have empty definitions"
   Defn Annote
_a Text
name Poly
poly Maybe DefnAttr
_defnattr [A.FunBinding Annote
_ [] Exp
rhs] -> do
                  (_tvs,tsig) <- Poly -> m ([Text], TypSig)
forall (m :: * -> *). Monad m => Poly -> m ([Text], TypSig)
tPolySig Poly
poly
                  let e = Exp
rhs
                  e' <- tExp e
                  return $ Isa.Definition (tGlobal name) tsig [] e'
   d :: Defn
d@(Defn Annote
_ Text
_ Poly
_ Maybe DefnAttr
_ (FunBinding
_ : [FunBinding]
_)) -> do
                  fun <- Defn -> m (Text, TypSig, [([Pttrn], Term)])
forall (m :: * -> *).
MonadError AstError m =>
Defn -> m (Text, TypSig, [([Pttrn], Term)])
tFun Defn
d
                  return $ Isa.Fun [fun]


tFunBinding :: (MonadError AstError m) => A.FunBinding -> m ([Pttrn], Term)
tFunBinding :: forall (m :: * -> *).
MonadError AstError m =>
FunBinding -> m ([Pttrn], Term)
tFunBinding (A.FunBinding Annote
_ [Pat]
ps Exp
e) = do
      e' <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e
      let ps' = (Pat -> Pttrn) -> [Pat] -> [Pttrn]
forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pttrn
tPat [Pat]
ps
      return (ps',e')


tFun :: (MonadError AstError m) => A.Defn -> m (T.Text, TypSig, [([Pttrn], Term)])
tFun :: forall (m :: * -> *).
MonadError AstError m =>
Defn -> m (Text, TypSig, [([Pttrn], Term)])
tFun (Defn Annote
_a Text
name Poly
poly Maybe DefnAttr
_defnattr [FunBinding]
fbs) = do
                  (_tvs,tsig) <- Poly -> m ([Text], TypSig)
forall (m :: * -> *). Monad m => Poly -> m ([Text], TypSig)
tPolySig Poly
poly
                  fbs' <- mapM tFunBinding fbs
                  return (tGlobal name, tsig, fbs')


tRDefns :: (MonadError AstError m) => [A.Defn] -> m Isa.Decl
tRDefns :: forall (m :: * -> *). MonadError AstError m => [Defn] -> m Decl
tRDefns [Defn]
ds = do
            fs <- (Defn -> m (Text, TypSig, [([Pttrn], Term)]))
-> [Defn] -> m [(Text, TypSig, [([Pttrn], Term)])]
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 Defn -> m (Text, TypSig, [([Pttrn], Term)])
forall (m :: * -> *).
MonadError AstError m =>
Defn -> m (Text, TypSig, [([Pttrn], Term)])
tFun [Defn]
ds
            return $ Isa.Fun fs

tDataDefn :: Monad m => A.DataDefn -> m Isa.Decl
tDataDefn :: forall (m :: * -> *). Monad m => DataDefn -> m Decl
tDataDefn (DataDefn Annote
_a Text
name [Text]
_tvs cons :: [DataCon]
cons@(A.DataCon Annote
_ Text
_ Poly
p:[DataCon]
_)) = do
      constrs <- (DataCon -> m DatatypeConstructor)
-> [DataCon] -> m [DatatypeConstructor]
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 DataCon -> m DatatypeConstructor
forall (m :: * -> *). Monad m => DataCon -> m DatatypeConstructor
tDataCon [DataCon]
cons
      (tvs,_t) <- tPoly p
      return $ Datatype (tGlobal name) tvs constrs
tDataDefn (DataDefn Annote
_ Text
name [Text]
tvs []) = Decl -> m Decl
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> m Decl) -> Decl -> m Decl
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> [DatatypeConstructor] -> Decl
Datatype (Text -> Text
tGlobal Text
name) ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Text
tLocal [Text]
tvs) []

tRecDefn :: Monad m => A.RecDefn -> m Isa.Decl
tRecDefn :: forall (m :: * -> *). Monad m => RecDefn -> m Decl
tRecDefn (RecDefn Annote
_ Text
name [Text]
tvs Poly
_poly [(Text, Ty)]
fields) =
  Decl -> m Decl
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> m Decl) -> Decl -> m Decl
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> [(Text, Typ)] -> Decl
Isa.Record (Text -> Text
tGlobal Text
name) ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Text
tLocal [Text]
tvs) (((Text, Ty) -> (Text, Typ)) -> [(Text, Ty)] -> [(Text, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map ((Ty -> Typ) -> (Text, Ty) -> (Text, Typ)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Ty -> Typ
tType) [(Text, Ty)]
fields)


tDataCon :: Monad m => A.DataCon -> m Isa.DatatypeConstructor
tDataCon :: forall (m :: * -> *). Monad m => DataCon -> m DatatypeConstructor
tDataCon (A.DataCon Annote
_a Text
name Poly
poly) = do
      (_tvs, TypSig ts _cod) <- Poly -> m ([Text], TypSig)
forall (m :: * -> *). Monad m => Poly -> m ([Text], TypSig)
tPolySig Poly
poly  -- TODO: Might need to use the codomain and tvs to rename args variables
      return $ DatatypeConstructor (tGlobal name) ts


---------- ================================================= ----------

--- Translating Types

tType :: A.Ty -> Isa.Typ
tType :: Ty -> Typ
tType (Ty -> Ty
flattenTyTuple (Ty -> Ty) -> (Ty -> Ty) -> Ty -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> Ty
transMonadT -> Ty
t') = case Ty -> (Ty, [Ty])
flattenTy Ty
t' of
        (TyBuiltin Annote
_a TyBuiltin
tb,[Ty]
ts) -> TyBuiltin -> [Typ] -> Typ
Isa.TBuiltin TyBuiltin
tb ((Ty -> Typ) -> [Ty] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Ty -> Typ
tType [Ty]
ts)
        (TyCon Annote
_a Text
name,[Ty]
ts) -> Text -> [Typ] -> Typ
Isa.Type (Text -> Text
tGlobal Text
name) ((Ty -> Typ) -> [Ty] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Ty -> Typ
tType [Ty]
ts)
        (TyVar Annote
_a Text
name, []) -> Text -> Typ
Isa.TVar (Text -> Text
tLocal Text
name)
        (TyVar Annote
_a Text
name, ts :: [Ty]
ts@(Ty
_:[Ty]
_)) -> Text -> [Typ] -> Typ
Isa.Type (Text -> Text
tLocal Text
name) ((Ty -> Typ) -> [Ty] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Ty -> Typ
tType [Ty]
ts)
        (TyNat Annote
_a Natural
n, []) -> Vertex -> Typ
Isa.TNum (Natural -> Vertex
forall a. Enum a => a -> Vertex
fromEnum Natural
n)
        (TyNat Annote
a Natural
_, Ty
_:[Ty]
_) -> [Char] -> Typ
forall a. HasCallStack => [Char] -> a
error ([Char] -> Typ) -> [Char] -> Typ
forall a b. (a -> b) -> a -> b
$ [Char]
"ERROR: shouldn't apply type numerals" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Annote -> [Char]
forall a. Show a => a -> [Char]
show Annote
a
        (TyApp {},[Ty]
_) -> [Char] -> Typ
forall a. HasCallStack => [Char] -> a
error [Char]
"ERROR: shouldn't have an application after flattening"
        (TyTuple {},[Ty]
_) -> [Char] -> Typ
forall a. HasCallStack => [Char] -> a
error [Char]
"ERROR: shouldn't have a type tuple after flattening"


tTypeSig :: A.Ty -> Isa.TypSig
tTypeSig :: Ty -> TypSig
tTypeSig Ty
t = let ([Ty]
args,Ty
cod) = Ty -> ([Ty], Ty)
flattenSig Ty
t
             in [Typ] -> Typ -> TypSig
TypSig ((Ty -> Typ) -> [Ty] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Ty -> Typ
tType [Ty]
args) (Ty -> Typ
tType Ty
cod)

tPoly :: Monad m => A.Poly -> m ([TName], Isa.Typ)
tPoly :: forall (m :: * -> *). Monad m => Poly -> m ([Text], Typ)
tPoly (Poly [Text]
tvs Ty
t) = ([Text], Typ) -> m ([Text], Typ)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Text
tLocal [Text]
tvs, Ty -> Typ
tType Ty
t)

tPolySig :: Monad m => A.Poly -> m ([TName], Isa.TypSig)
tPolySig :: forall (m :: * -> *). Monad m => Poly -> m ([Text], TypSig)
tPolySig (Poly [Text]
tvs Ty
t) = ([Text], TypSig) -> m ([Text], TypSig)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Text
tLocal [Text]
tvs, Ty -> TypSig
tTypeSig Ty
t)


-- | translates (t1,t2,t3,t4) to (t1,(t2,(t3,t4))))
flattenTyTuple :: A.Ty -> A.Ty
flattenTyTuple :: Ty -> Ty
flattenTyTuple (TyTuple Annote
_ []) = Ty
nilTy
flattenTyTuple (TyTuple Annote
a ts :: [Ty]
ts@(Ty
_:[Ty]
_)) =
      (Ty -> Ty -> Ty) -> [Ty] -> Ty
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (Annote -> Ty -> Ty -> Ty
pairTy Annote
a) [Ty]
ts
flattenTyTuple Ty
t = Ty
t

flattenTy :: A.Ty -> (A.Ty,[A.Ty])
flattenTy :: Ty -> (Ty, [Ty])
flattenTy (TyApp Annote
_ Ty
t [Ty]
ts) = (Ty
t', [Ty]
ts' [Ty] -> [Ty] -> [Ty]
forall a. [a] -> [a] -> [a]
++ [Ty]
ts)
       where (Ty
t',[Ty]
ts') = Ty -> (Ty, [Ty])
flattenTy Ty
t
flattenTy Ty
t = (Ty
t,[])


---------- ================================================= ----------

--- Translating Expressions

tExp :: Monad m => A.Exp -> m Isa.Term
tExp :: forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e | Just Poly
pt <- Exp -> Maybe Poly
forall a. TypeAnnotated a => a -> Maybe Poly
tyAnn Exp
e = do
      e' <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp (Maybe Poly -> Exp -> Exp
forall a. TypeAnnotated a => Maybe Poly -> a -> a
setTyAnn Maybe Poly
forall a. Maybe a
Nothing Exp
e)
      (_ts,pt') <- tPoly pt
      return $ Isa.TypAnnTerm e' pt'
tExp (A.Tuple Annote
_ Maybe Poly
_ Maybe Ty
_ [Exp]
es) = do
      es' <- (Exp -> m Term) -> [Exp] -> m [Term]
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 Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp [Exp]
es
      return $ Isa.Tuplex es'
tExp (A.App Annote
_ Maybe Poly
_ Maybe Ty
_ Exp
e [Exp]
es) = do
      rator <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e
      rands <- mapM tExp es
      return $ Isa.App rator rands
tExp lam :: Exp
lam@(A.Lam {}) = do
      (names,e) <- Exp -> m ([Text], Exp)
forall (m :: * -> *). Monad m => Exp -> m ([Text], Exp)
flattenLam Exp
lam
      e' <- tExp e
      return $ Isa.Abs (map tLocal names) e'
tExp (A.Var     Annote
_ Maybe Poly
_mp Maybe Ty
_mt Text
name) = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Text -> Term
Free (Text -> Term) -> Text -> Term
forall a b. (a -> b) -> a -> b
$ Text -> Text
tLocal Text
name
tExp (A.Con     Annote
_ Maybe Poly
_mp Maybe Ty
_mt Text
name) = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Text -> Term
Free (Text -> Term) -> Text -> Term
forall a b. (a -> b) -> a -> b
$ Text -> Text
tGlobal Text
name
tExp c :: Exp
c@(A.Case    {}) = do
      let (Exp
e',[(Pat, Exp)]
bs') = Exp -> (Exp, [(Pat, Exp)])
flattenCase Exp
c
      e'' <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e'
      bs'' <- mapM tCase bs'
      return $ Isa.Case e'' bs''
tExp (A.RWUser Annote
_ Maybe Poly
_mp Maybe Ty
_mt RWUserOp
b) = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ RWUserOp -> Term
Isa.Prim RWUserOp
b
tExp (A.LitInt  Annote
_ Maybe Poly
_mp     Integer
i) = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Integer -> Term
Isa.LitNum (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
i)
tExp (A.LitStr  Annote
_ Maybe Poly
_mp     Text
s) = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Text -> Term
Isa.LitString Text
s
tExp (A.LitVec  Annote
_ Maybe Poly
_mp Maybe Ty
_mt [Exp]
es) = do
      es' <- (Exp -> m Term) -> [Exp] -> m [Term]
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 Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp [Exp]
es
      return $ Isa.LitVec es'
tExp (A.LitList Annote
_ Maybe Poly
_mp Maybe Ty
_mt [Exp]
es) = do
      es' <- (Exp -> m Term) -> [Exp] -> m [Term]
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 Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp [Exp]
es
      return $ Isa.List es'
tExp (A.If Annote
_ Maybe Poly
_mp Maybe Ty
_mt Exp
t Exp
c Exp
a) = do
      t' <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
t
      c' <- tExp c
      a' <- tExp a
      return $ Isa.If t' c' a'
tExp (A.Let Annote
_ Maybe Poly
_mp Maybe Ty
_mt [PatBind]
bs Exp
e) = do
      e' <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e
      bs' <- mapM tPatBind bs
      return $ Isa.Let bs' e'
tExp (A.RecVal Annote
_ Maybe Poly
_ Maybe Ty
_ [(Text, Exp)]
fields) = do
  fields' <- ((Text, Exp) -> m (Text, Term))
-> [(Text, Exp)] -> m [(Text, Term)]
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 (\(Text
f, Exp
e) -> (Text
f,) (Term -> (Text, Term)) -> m Term -> m (Text, Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e) [(Text, Exp)]
fields
  return $ Isa.RecordVal fields'
tExp (A.RecUpd Annote
_ Maybe Poly
_ Maybe Ty
_ Exp
base [(Text, Exp)]
updates) = do
  base' <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
base
  updates' <- mapM (\(Text
f, Exp
e) -> (Text
f,) (Term -> (Text, Term)) -> m Term -> m (Text, Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e) updates
  return $ Isa.RecordUpdate base' updates'
tExp (A.RecSel Annote
_ Maybe Poly
_ Maybe Ty
_ Text
field Exp
rec) = Text -> Term -> Term
Isa.RecordSel Text
field (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
rec



-- Patterns and Case

tPat :: Pat -> Pttrn
tPat :: Pat -> Pttrn
tPat = \ case
      (PatCon Annote
_a Maybe Poly
_mp Maybe Ty
mt Text
name [Pat]
ps) -> Text -> Maybe Typ -> [Pttrn] -> Pttrn
PttrnCon (Text -> Text
tGlobal Text
name) ((Ty -> Typ) -> Maybe Ty -> Maybe Typ
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ty -> Typ
tType Maybe Ty
mt) ((Pat -> Pttrn) -> [Pat] -> [Pttrn]
forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pttrn
tPat [Pat]
ps)
      (PatVar Annote
_a Maybe Poly
_mp Maybe Ty
mt Text
name) -> Text -> Maybe Typ -> Pttrn
PttrnVar (Text -> Text
tLocal Text
name) ((Ty -> Typ) -> Maybe Ty -> Maybe Typ
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ty -> Typ
tType Maybe Ty
mt)
      (PatWildCard Annote
_a Maybe Poly
_mp Maybe Ty
mt) -> Maybe Typ -> Pttrn
PttrnWildCard ((Ty -> Typ) -> Maybe Ty -> Maybe Typ
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ty -> Typ
tType Maybe Ty
mt)
      (PatTuple Annote
_a Maybe Poly
_mp Maybe Ty
mt [Pat]
ps) -> Maybe Typ -> [Pttrn] -> Pttrn
PttrnTuple ((Ty -> Typ) -> Maybe Ty -> Maybe Typ
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ty -> Typ
tType Maybe Ty
mt) ((Pat -> Pttrn) -> [Pat] -> [Pttrn]
forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pttrn
tPat [Pat]
ps)
      (PatAs Annote
_a Maybe Poly
_mp Maybe Ty
mt Text
n Pat
p)   -> Maybe Typ -> Pttrn -> Text -> Pttrn
PttrnAs ((Ty -> Typ) -> Maybe Ty -> Maybe Typ
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ty -> Typ
tType Maybe Ty
mt) (Pat -> Pttrn
tPat Pat
p) (Text -> Text
tLocal Text
n)
      (A.PatRec Annote
_ Maybe Poly
_ Maybe Ty
mt [(Text, Pat)]
fields) -> Maybe Typ -> [(Text, Pttrn)] -> Pttrn
PttrnRecord ((Ty -> Typ) -> Maybe Ty -> Maybe Typ
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ty -> Typ
tType Maybe Ty
mt) (((Text, Pat) -> (Text, Pttrn)) -> [(Text, Pat)] -> [(Text, Pttrn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Pat -> Pttrn) -> (Text, Pat) -> (Text, Pttrn)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Pat -> Pttrn
tPat) [(Text, Pat)]
fields)

tPatBind :: (Monad m) => PatBind -> m (Isa.Pttrn, Isa.Term)
tPatBind :: forall (m :: * -> *). Monad m => PatBind -> m (Pttrn, Term)
tPatBind (A.PatBind Pat
p Exp
e) = do
      let p' :: Pttrn
p' = Pat -> Pttrn
tPat Pat
p
      e' <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e
      return (p',e')

-- | Case Annote !(Maybe Poly) !(Maybe Ty) !Exp ![PatBind]
flattenCase :: A.Exp -> (A.Exp, [(Pat,Exp)])
flattenCase :: Exp -> (Exp, [(Pat, Exp)])
flattenCase (A.Case Annote
_ Maybe Poly
_ Maybe Ty
_ Exp
e [PatBind]
pbs) = (Exp
e,(PatBind -> (Pat, Exp)) -> [PatBind] -> [(Pat, Exp)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (A.PatBind Pat
p Exp
e') -> (Pat
p,Exp
e')) [PatBind]
pbs)
flattenCase Exp
_ = [Char] -> (Exp, [(Pat, Exp)])
forall a. HasCallStack => [Char] -> a
error [Char]
"flattenCase: should prevent this case"

tCase :: Monad m => (Pat,Exp) -> m (Pttrn,Term)
tCase :: forall (m :: * -> *). Monad m => (Pat, Exp) -> m (Pttrn, Term)
tCase (Pat
p,Exp
e) = do
      e' <- Exp -> m Term
forall (m :: * -> *). Monad m => Exp -> m Term
tExp Exp
e
      let p' = Pat -> Pttrn
tPat Pat
p
      return (p', e')

---------- ================================================= ----------

--- Translating Names

tGlobal :: T.Text -> T.Text
tGlobal :: Text -> Text
tGlobal = Text -> Text
filterName (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
getBaseName
 -- could modify getBaseName to try to handle namespaces/imports

tLocal :: T.Text -> T.Text
tLocal :: Text -> Text
tLocal = Text -> Text
filterName (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
getBaseName

getBaseName :: T.Text -> T.Text
getBaseName :: Text -> Text
getBaseName Text
s = [Text] -> Text
forall a. HasCallStack => [a] -> a
last (HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
T.splitOn Text
"." Text
s)

filterName :: T.Text -> T.Text
filterName :: Text -> Text
filterName = Text -> Text
leadingTrailingEmpty
             (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
removePunc
             (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
handleQualified
      where
      handleQualified :: T.Text -> T.Text
      handleQualified :: Text -> Text
handleQualified = (Char -> Char) -> Text -> Text
T.map (\ Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'.' then Char
'_' else Char
c)
      removePunc :: T.Text -> T.Text
      removePunc :: Text -> Text
removePunc = (Char -> Bool) -> Text -> Text
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'$')
      leadingTrailingEmpty :: T.Text -> T.Text
      leadingTrailingEmpty :: Text -> Text
leadingTrailingEmpty Text
s | Text -> Bool
T.null Text
s = Text
"null"
                             | Char -> Bool
isDigit (HasCallStack => Text -> Char
Text -> Char
T.head Text
s) = Text
"a" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s
                             | Text
s Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"_" = Text
s
                             | HasCallStack => Text -> Char
Text -> Char
T.last Text
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' = Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"a"
                             | HasCallStack => Text -> Char
Text -> Char
T.head Text
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' = Text
"a" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s
                             | Bool
otherwise = Text
s


isReWire :: Show a => a -> Bool
isReWire :: forall a. Show a => a -> Bool
isReWire a
a = [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf [Char]
"ReWire." (a -> [Char]
forall a. Show a => a -> [Char]
show a
a) Bool -> Bool -> Bool
|| a -> Bool
forall a. Show a => a -> Bool
isPrim a
a