{-# LANGUAGE TemplateHaskell #-}
module Language.SOAS.FreeFoilConfig where

import qualified Language.SOAS.Syntax.Abs    as Raw
import           Control.Monad.Free.Foil.TH.MkFreeFoil

intToVarIdent :: Int -> Raw.VarIdent
intToVarIdent :: Int -> VarIdent
intToVarIdent Int
i = String -> VarIdent
Raw.VarIdent (String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)

rawVar :: Raw.VarIdent -> Raw.Term' a
rawVar :: forall a. VarIdent -> Term' a
rawVar = a -> VarIdent -> Term' a
forall a. a -> VarIdent -> Term' a
Raw.Var (String -> a
forall a. HasCallStack => String -> a
error String
"trying to access an erased annotation")

rawTypeVar :: Raw.VarIdent -> Raw.Type' a
rawTypeVar :: forall a. VarIdent -> Type' a
rawTypeVar = a -> VarIdent -> Type' a
forall a. a -> VarIdent -> Type' a
Raw.TypeVar (String -> a
forall a. HasCallStack => String -> a
error String
"trying to access an erased annotation")

rawScopedTerm :: Raw.Term' a -> Raw.ScopedTerm' a
rawScopedTerm :: forall a. Term' a -> ScopedTerm' a
rawScopedTerm = a -> Term' a -> ScopedTerm' a
forall a. a -> Term' a -> ScopedTerm' a
Raw.ScopedTerm (String -> a
forall a. HasCallStack => String -> a
error String
"trying to access an erased annotation")

rawScopedType :: Raw.Type' a -> Raw.ScopedType' a
rawScopedType :: forall a. Type' a -> ScopedType' a
rawScopedType = a -> Type' a -> ScopedType' a
forall a. a -> Type' a -> ScopedType' a
Raw.ScopedType (String -> a
forall a. HasCallStack => String -> a
error String
"trying to access an erased annotation")

rawScopeToTerm :: Raw.ScopedTerm' a -> Raw.Term' a
rawScopeToTerm :: forall a. ScopedTerm' a -> Term' a
rawScopeToTerm (Raw.ScopedTerm a
_loc Term' a
term) = Term' a
term

rawScopeToType :: Raw.ScopedType' a -> Raw.Type' a
rawScopeToType :: forall a. ScopedType' a -> Type' a
rawScopeToType (Raw.ScopedType a
_loc Type' a
type_) = Type' a
type_

soasConfig :: FreeFoilConfig
soasConfig :: FreeFoilConfig
soasConfig = FreeFoilConfig
  { rawQuantifiedNames :: [Name]
rawQuantifiedNames =
      [ ''Raw.Subst'
      , ''Raw.MetaVarTyping'
      , ''Raw.OpTyping'
      , ''Raw.Constraint'
      , ''Raw.VarTyping'
      , ''Raw.TermTyping'
      ]
  , freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilTermConfigs =
      [ FreeFoilTermConfig
          { rawIdentName :: Name
rawIdentName = ''Raw.VarIdent
          , rawTermName :: Name
rawTermName = ''Raw.Term'
          , rawBindingName :: Name
rawBindingName = ''Raw.Binders'
          , rawScopeName :: Name
rawScopeName = ''Raw.ScopedTerm'
          , rawVarConName :: Name
rawVarConName = 'Raw.Var
          , rawSubTermNames :: [Name]
rawSubTermNames = [ ''Raw.OpArg' ]
          , rawSubScopeNames :: [Name]
rawSubScopeNames = []
          , intToRawIdentName :: Name
intToRawIdentName = 'intToVarIdent
          , rawVarIdentToTermName :: Name
rawVarIdentToTermName = 'rawVar
          , rawTermToScopeName :: Name
rawTermToScopeName = 'rawScopedTerm
          , rawScopeToTermName :: Name
rawScopeToTermName = 'rawScopeToTerm
          }
      , FreeFoilTermConfig
          { rawIdentName :: Name
rawIdentName = ''Raw.VarIdent
          , rawTermName :: Name
rawTermName = ''Raw.Type'
          , rawBindingName :: Name
rawBindingName = ''Raw.TypeBinders'
          , rawScopeName :: Name
rawScopeName = ''Raw.ScopedType'
          , rawVarConName :: Name
rawVarConName = 'Raw.TypeVar
          , rawSubTermNames :: [Name]
rawSubTermNames = [ ''Raw.OpArgTyping' ]
          , rawSubScopeNames :: [Name]
rawSubScopeNames = [ ''Raw.ScopedOpArgTyping' ]
          , intToRawIdentName :: Name
intToRawIdentName = 'intToVarIdent
          , rawVarIdentToTermName :: Name
rawVarIdentToTermName = 'rawTypeVar
          , rawTermToScopeName :: Name
rawTermToScopeName = 'rawScopedType
          , rawScopeToTermName :: Name
rawScopeToTermName = 'rawScopeToType
          } ]
  , freeFoilNameModifier :: String -> String
freeFoilNameModifier = String -> String
forall a. a -> a
id
  , freeFoilScopeNameModifier :: String -> String
freeFoilScopeNameModifier = (String
"Scoped" String -> String -> String
forall a. [a] -> [a] -> [a]
++ )
  , freeFoilConNameModifier :: String -> String
freeFoilConNameModifier = String -> String
forall a. a -> a
id
  , freeFoilConvertFromName :: String -> String
freeFoilConvertFromName = (String
"from" String -> String -> String
forall a. [a] -> [a] -> [a]
++ )
  , freeFoilConvertToName :: String -> String
freeFoilConvertToName = (String
"to" String -> String -> String
forall a. [a] -> [a] -> [a]
++ )
  , signatureNameModifier :: String -> String
signatureNameModifier = (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Sig")
  }