{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Raw where
import Data.ByteString as BS hiding (map)
import Data.Text qualified as T
import PlutusCore
import PlutusCore.Data hiding (Constr)
import PlutusCore.DeBruijn
import PlutusCore.Default
import PlutusCore.Parser
import PlutusCore.Pretty
import Data.Either
import PlutusCore.Error (ParserErrorBundle)
data KIND = Star | Sharp | Arrow KIND KIND
deriving Int -> KIND -> ShowS
[KIND] -> ShowS
KIND -> String
(Int -> KIND -> ShowS)
-> (KIND -> String) -> ([KIND] -> ShowS) -> Show KIND
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> KIND -> ShowS
showsPrec :: Int -> KIND -> ShowS
$cshow :: KIND -> String
show :: KIND -> String
$cshowList :: [KIND] -> ShowS
showList :: [KIND] -> ShowS
Show
data RType = RTyVar Integer
| RTyFun RType RType
| RTyPi KIND RType
| RTyLambda KIND RType
| RTyApp RType RType
| RTyCon RTyCon
| RTyMu RType RType
| RTySOP [[RType]]
deriving Int -> RType -> ShowS
[RType] -> ShowS
RType -> String
(Int -> RType -> ShowS)
-> (RType -> String) -> ([RType] -> ShowS) -> Show RType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RType -> ShowS
showsPrec :: Int -> RType -> ShowS
$cshow :: RType -> String
show :: RType -> String
$cshowList :: [RType] -> ShowS
showList :: [RType] -> ShowS
Show
data AtomicTyCon = ATyConInt
| ATyConBS
| ATyConStr
| ATyConUnit
| ATyConBool
| ATyConData
| ATyConBLS12_381_G1_Element
| ATyConBLS12_381_G2_Element
| ATyConBLS12_381_MlResult
deriving Int -> AtomicTyCon -> ShowS
[AtomicTyCon] -> ShowS
AtomicTyCon -> String
(Int -> AtomicTyCon -> ShowS)
-> (AtomicTyCon -> String)
-> ([AtomicTyCon] -> ShowS)
-> Show AtomicTyCon
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AtomicTyCon -> ShowS
showsPrec :: Int -> AtomicTyCon -> ShowS
$cshow :: AtomicTyCon -> String
show :: AtomicTyCon -> String
$cshowList :: [AtomicTyCon] -> ShowS
showList :: [AtomicTyCon] -> ShowS
Show
data RTyCon = RTyConAtom AtomicTyCon
| RTyConList
| RTyConPair
deriving Int -> RTyCon -> ShowS
[RTyCon] -> ShowS
RTyCon -> String
(Int -> RTyCon -> ShowS)
-> (RTyCon -> String) -> ([RTyCon] -> ShowS) -> Show RTyCon
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RTyCon -> ShowS
showsPrec :: Int -> RTyCon -> ShowS
$cshow :: RTyCon -> String
show :: RTyCon -> String
$cshowList :: [RTyCon] -> ShowS
showList :: [RTyCon] -> ShowS
Show
data RTerm = RVar Integer
| RTLambda KIND RTerm
| RTApp RTerm RType
| RLambda RType RTerm
| RApp RTerm RTerm
| RCon (Some (ValueOf DefaultUni))
| RError RType
| RBuiltin DefaultFun
| RWrap RType RType RTerm
| RUnWrap RTerm
| RConstr RType Integer [RTerm]
| RCase RType RTerm [RTerm]
deriving Int -> RTerm -> ShowS
[RTerm] -> ShowS
RTerm -> String
(Int -> RTerm -> ShowS)
-> (RTerm -> String) -> ([RTerm] -> ShowS) -> Show RTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RTerm -> ShowS
showsPrec :: Int -> RTerm -> ShowS
$cshow :: RTerm -> String
show :: RTerm -> String
$cshowList :: [RTerm] -> ShowS
showList :: [RTerm] -> ShowS
Show
unIndex :: Index -> Integer
unIndex :: Index -> Integer
unIndex (Index Word64
n) = Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger Word64
n
convP :: Program NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
convP :: forall a.
Program NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
-> RTerm
convP (Program a
_ Version
_ Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t) = Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t
convK :: Kind a -> KIND
convK :: forall a. Kind a -> KIND
convK (Type a
_) = KIND
Star
convK (KindArrow a
_ Kind a
k Kind a
k') = KIND -> KIND -> KIND
Arrow (Kind a -> KIND
forall a. Kind a -> KIND
convK Kind a
k) (Kind a -> KIND
forall a. Kind a -> KIND
convK Kind a
k')
convT :: Type NamedTyDeBruijn DefaultUni a -> RType
convT :: forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT (TyVar a
_ (NamedTyDeBruijn NamedDeBruijn
x)) = Integer -> RType
RTyVar (Index -> Integer
unIndex (NamedDeBruijn -> Index
ndbnIndex NamedDeBruijn
x))
convT (TyFun a
_ Type NamedTyDeBruijn DefaultUni a
_A Type NamedTyDeBruijn DefaultUni a
_B) = RType -> RType -> RType
RTyFun (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A) (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_B)
convT (TyForall a
_ NamedTyDeBruijn
_ Kind a
_K Type NamedTyDeBruijn DefaultUni a
_A) = KIND -> RType -> RType
RTyPi (Kind a -> KIND
forall a. Kind a -> KIND
convK Kind a
_K) (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A)
convT (TyLam a
_ NamedTyDeBruijn
_ Kind a
_K Type NamedTyDeBruijn DefaultUni a
_A) = KIND -> RType -> RType
RTyLambda (Kind a -> KIND
forall a. Kind a -> KIND
convK Kind a
_K) (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A)
convT (TyApp a
_ Type NamedTyDeBruijn DefaultUni a
_A Type NamedTyDeBruijn DefaultUni a
_B) = RType -> RType -> RType
RTyApp (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A) (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_B)
convT (TyBuiltin a
ann (SomeTypeIn (DefaultUniApply DefaultUni (Esc f)
f DefaultUni (Esc a1)
x))) =
RType -> RType -> RType
RTyApp (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT (a -> SomeTypeIn DefaultUni -> Type NamedTyDeBruijn DefaultUni a
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin a
ann (DefaultUni (Esc f) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc f)
f)))
(Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT (a -> SomeTypeIn DefaultUni -> Type NamedTyDeBruijn DefaultUni a
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin a
ann (DefaultUni (Esc a1) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc a1)
x)))
convT (TyBuiltin a
_ SomeTypeIn DefaultUni
someUni) = SomeTypeIn DefaultUni -> RType
convTyCon SomeTypeIn DefaultUni
someUni
convT (TyIFix a
_ Type NamedTyDeBruijn DefaultUni a
a Type NamedTyDeBruijn DefaultUni a
b) = RType -> RType -> RType
RTyMu (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
a) (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
b)
convT (TySOP a
_ [[Type NamedTyDeBruijn DefaultUni a]]
xss) = [[RType]] -> RType
RTySOP (([Type NamedTyDeBruijn DefaultUni a] -> [RType])
-> [[Type NamedTyDeBruijn DefaultUni a]] -> [[RType]]
forall a b. (a -> b) -> [a] -> [b]
map ((Type NamedTyDeBruijn DefaultUni a -> RType)
-> [Type NamedTyDeBruijn DefaultUni a] -> [RType]
forall a b. (a -> b) -> [a] -> [b]
map Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT) [[Type NamedTyDeBruijn DefaultUni a]]
xss)
convTyCon :: SomeTypeIn DefaultUni -> RType
convTyCon :: SomeTypeIn DefaultUni -> RType
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniInteger) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConInt)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniByteString) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConBS)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniString) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConStr)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniBool) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConBool)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniUnit) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConUnit)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniData) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConData)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConBLS12_381_G1_Element)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConBLS12_381_G2_Element)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult) = RTyCon -> RType
RTyCon (AtomicTyCon -> RTyCon
RTyConAtom AtomicTyCon
ATyConBLS12_381_MlResult)
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniProtoList) = RTyCon -> RType
RTyCon RTyCon
RTyConList
convTyCon (SomeTypeIn DefaultUni (Esc a)
DefaultUniProtoPair) = RTyCon -> RType
RTyCon RTyCon
RTyConPair
convTyCon (SomeTypeIn (DefaultUniApply DefaultUni (Esc f)
_ DefaultUni (Esc a1)
_)) = String -> RType
forall a. HasCallStack => String -> a
error String
"unsupported builtin type application"
conv :: Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv :: forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv (Var a
_ NamedDeBruijn
x) = Integer -> RTerm
RVar (Index -> Integer
unIndex (NamedDeBruijn -> Index
ndbnIndex NamedDeBruijn
x))
conv (TyAbs a
_ NamedTyDeBruijn
_ Kind a
_K Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t) = KIND -> RTerm -> RTerm
RTLambda (Kind a -> KIND
forall a. Kind a -> KIND
convK Kind a
_K) (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t)
conv (TyInst a
_ Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t Type NamedTyDeBruijn DefaultUni a
_A) = RTerm -> RType -> RTerm
RTApp (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t) (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A)
conv (LamAbs a
_ NamedDeBruijn
_ Type NamedTyDeBruijn DefaultUni a
_A Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t) = RType -> RTerm -> RTerm
RLambda (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A) (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t)
conv (Apply a
_ Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
u) = RTerm -> RTerm -> RTerm
RApp (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t) (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
u)
conv (Builtin a
_ DefaultFun
b) = DefaultFun -> RTerm
RBuiltin DefaultFun
b
conv (Constant a
_ Some (ValueOf DefaultUni)
c) = Some (ValueOf DefaultUni) -> RTerm
RCon Some (ValueOf DefaultUni)
c
conv (Unwrap a
_ Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t) = RTerm -> RTerm
RUnWrap (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t)
conv (IWrap a
_ Type NamedTyDeBruijn DefaultUni a
ty1 Type NamedTyDeBruijn DefaultUni a
ty2 Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t) = RType -> RType -> RTerm -> RTerm
RWrap (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
ty1) (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
ty2) (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
t)
conv (Error a
_ Type NamedTyDeBruijn DefaultUni a
_A) = RType -> RTerm
RError (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A)
conv (Constr a
_ Type NamedTyDeBruijn DefaultUni a
_A Word64
i [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a]
cs) = RType -> Integer -> [RTerm] -> RTerm
RConstr (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A) (Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger Word64
i) ((Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
-> RTerm)
-> [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a]
-> [RTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a]
cs)
conv (Case a
_ Type NamedTyDeBruijn DefaultUni a
_A Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
arg [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a]
cs) = RType -> RTerm -> [RTerm] -> RTerm
RCase (Type NamedTyDeBruijn DefaultUni a -> RType
forall a. Type NamedTyDeBruijn DefaultUni a -> RType
convT Type NamedTyDeBruijn DefaultUni a
_A) (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
arg) ((Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
-> RTerm)
-> [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a]
-> [RTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
conv [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a]
cs)
varTm :: Int -> NamedDeBruijn
varTm :: Int -> NamedDeBruijn
varTm Int
i = Text -> Index -> NamedDeBruijn
NamedDeBruijn (String -> Text
T.pack [String
tmnames String -> Int -> Char
forall a. HasCallStack => [a] -> Int -> a
!! Int
i]) Index
deBruijnInitIndex
varTy :: Int -> NamedDeBruijn
varTy :: Int -> NamedDeBruijn
varTy Int
i = Text -> Index -> NamedDeBruijn
NamedDeBruijn (String -> Text
T.pack [String
tynames String -> Int -> Char
forall a. HasCallStack => [a] -> Int -> a
!! Int
i]) Index
deBruijnInitIndex
unconvK :: KIND -> Kind ()
unconvK :: KIND -> Kind ()
unconvK (Arrow KIND
k KIND
k') = () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (KIND -> Kind ()
unconvK KIND
k) (KIND -> Kind ()
unconvK KIND
k')
unconvK KIND
_ = () -> Kind ()
forall ann. ann -> Kind ann
Type ()
unconvT :: Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT :: Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i (RTyVar Integer
x) =
() -> NamedTyDeBruijn -> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () (NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (Text -> Index -> NamedDeBruijn
NamedDeBruijn (String -> Text
T.pack [String
tynames String -> Int -> Char
forall a. HasCallStack => [a] -> Int -> a
!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
x)]) (Word64 -> Index
Index (Integer -> Word64
forall a. Num a => Integer -> a
fromInteger Integer
x))))
unconvT Int
i (RTyFun RType
t RType
u) = ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
t) (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
u)
unconvT Int
i (RTyPi KIND
k RType
t) =
()
-> NamedTyDeBruijn
-> Kind ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () (NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (Int -> NamedDeBruijn
varTy Int
i)) (KIND -> Kind ()
unconvK KIND
k) (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) RType
t)
unconvT Int
i (RTyLambda KIND
k RType
t) = ()
-> NamedTyDeBruijn
-> Kind ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () (NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (Int -> NamedDeBruijn
varTy Int
i)) (KIND -> Kind ()
unconvK KIND
k) (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) RType
t)
unconvT Int
i (RTyApp RType
t RType
u) = ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
t) (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
u)
unconvT Int
i (RTyCon RTyCon
c) = () -> SomeTypeIn DefaultUni -> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin () (RTyCon -> SomeTypeIn DefaultUni
unconvTyCon RTyCon
c)
unconvT Int
i (RTyMu RType
t RType
u) = ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
t) (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
u)
unconvT Int
i (RTySOP [[RType]]
xss) = ()
-> [[Type NamedTyDeBruijn DefaultUni ()]]
-> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP () (([RType] -> [Type NamedTyDeBruijn DefaultUni ()])
-> [[RType]] -> [[Type NamedTyDeBruijn DefaultUni ()]]
forall a b. (a -> b) -> [a] -> [b]
map ((RType -> Type NamedTyDeBruijn DefaultUni ())
-> [RType] -> [Type NamedTyDeBruijn DefaultUni ()]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i)) [[RType]]
xss)
unconvTyCon :: RTyCon -> SomeTypeIn DefaultUni
unconvTyCon :: RTyCon -> SomeTypeIn DefaultUni
unconvTyCon (RTyConAtom AtomicTyCon
ATyConInt) = DefaultUni (Esc Integer) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Integer)
DefaultUniInteger
unconvTyCon (RTyConAtom AtomicTyCon
ATyConBS) = DefaultUni (Esc ByteString) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc ByteString)
DefaultUniByteString
unconvTyCon (RTyConAtom AtomicTyCon
ATyConStr) = DefaultUni (Esc Text) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Text)
DefaultUniString
unconvTyCon (RTyConAtom AtomicTyCon
ATyConBool) = DefaultUni (Esc Bool) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Bool)
DefaultUniBool
unconvTyCon (RTyConAtom AtomicTyCon
ATyConUnit) = DefaultUni (Esc ()) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc ())
DefaultUniUnit
unconvTyCon (RTyConAtom AtomicTyCon
ATyConData) = DefaultUni (Esc Data) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Data)
DefaultUniData
unconvTyCon (RTyConAtom AtomicTyCon
ATyConBLS12_381_G1_Element)
= DefaultUni (Esc Element) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Element)
DefaultUniBLS12_381_G1_Element
unconvTyCon (RTyConAtom AtomicTyCon
ATyConBLS12_381_G2_Element)
= DefaultUni (Esc Element) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Element)
DefaultUniBLS12_381_G2_Element
unconvTyCon (RTyConAtom AtomicTyCon
ATyConBLS12_381_MlResult)
= DefaultUni (Esc MlResult) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc MlResult)
DefaultUniBLS12_381_MlResult
unconvTyCon RTyCon
RTyConList = DefaultUni (Esc []) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc [])
DefaultUniProtoList
unconvTyCon RTyCon
RTyConPair = DefaultUni (Esc (,)) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc (,))
DefaultUniProtoPair
tmnames :: String
tmnames = [Char
'a' .. Char
'z']
tynames :: String
tynames = [Char
'A' .. Char
'Z']
unconv :: Int -> RTerm -> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv :: Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i (RVar Integer
x) =
()
-> NamedDeBruijn
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () (Text -> Index -> NamedDeBruijn
NamedDeBruijn (String -> Text
T.pack [String
tmnames String -> Int -> Char
forall a. HasCallStack => [a] -> Int -> a
!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
x )]) (Word64 -> Index
Index (Integer -> Word64
forall a. Num a => Integer -> a
fromInteger Integer
x)))
unconv Int
i (RTLambda KIND
k RTerm
tm) = ()
-> NamedTyDeBruijn
-> Kind ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () (NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (Int -> NamedDeBruijn
varTy Int
i)) (KIND -> Kind ()
unconvK KIND
k) (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) RTerm
tm)
unconv Int
i (RTApp RTerm
t RType
ty) = ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i RTerm
t) (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
ty)
unconv Int
i (RLambda RType
ty RTerm
tm) = ()
-> NamedDeBruijn
-> Type NamedTyDeBruijn DefaultUni ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () (Int -> NamedDeBruijn
varTm Int
i) (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) RType
ty) (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) RTerm
tm)
unconv Int
i (RApp RTerm
t RTerm
u) = ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i RTerm
t) (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i RTerm
u)
unconv Int
i (RCon Some (ValueOf DefaultUni)
c) = ()
-> Some (ValueOf DefaultUni)
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant () Some (ValueOf DefaultUni)
c
unconv Int
i (RError RType
ty) = ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error () (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
ty)
unconv Int
i (RBuiltin DefaultFun
b) = ()
-> DefaultFun
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
b
unconv Int
i (RWrap RType
tyA RType
tyB RTerm
t) = ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap () (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
tyA) (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
tyB) (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i RTerm
t)
unconv Int
i (RUnWrap RTerm
t) = ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap () (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i RTerm
t)
unconv Int
i (RConstr RType
ty Integer
j [RTerm]
cs) = ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Word64
-> [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr () (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
ty) (Integer -> Word64
forall a. Num a => Integer -> a
fromInteger Integer
j) ((RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> [RTerm]
-> [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i) [RTerm]
cs)
unconv Int
i (RCase RType
ty RTerm
arg [RTerm]
cs) = ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case () (Int -> RType -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
i RType
ty) (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i RTerm
arg) ((RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> [RTerm]
-> [Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int
-> RTerm
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
i) [RTerm]
cs)
data ERROR = TypeError T.Text
| ParseError ParserErrorBundle
| ScopeError ScopeError
| RuntimeError RuntimeError
| JsonError T.Text
deriving Int -> ERROR -> ShowS
[ERROR] -> ShowS
ERROR -> String
(Int -> ERROR -> ShowS)
-> (ERROR -> String) -> ([ERROR] -> ShowS) -> Show ERROR
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ERROR -> ShowS
showsPrec :: Int -> ERROR -> ShowS
$cshow :: ERROR -> String
show :: ERROR -> String
$cshowList :: [ERROR] -> ShowS
showList :: [ERROR] -> ShowS
Show
data ScopeError = DeBError|FreeVariableError FreeVariableError deriving Int -> ScopeError -> ShowS
[ScopeError] -> ShowS
ScopeError -> String
(Int -> ScopeError -> ShowS)
-> (ScopeError -> String)
-> ([ScopeError] -> ShowS)
-> Show ScopeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeError -> ShowS
showsPrec :: Int -> ScopeError -> ShowS
$cshow :: ScopeError -> String
show :: ScopeError -> String
$cshowList :: [ScopeError] -> ShowS
showList :: [ScopeError] -> ShowS
Show
data RuntimeError = GasError | UserError | RuntimeTypeError deriving Int -> RuntimeError -> ShowS
[RuntimeError] -> ShowS
RuntimeError -> String
(Int -> RuntimeError -> ShowS)
-> (RuntimeError -> String)
-> ([RuntimeError] -> ShowS)
-> Show RuntimeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuntimeError -> ShowS
showsPrec :: Int -> RuntimeError -> ShowS
$cshow :: RuntimeError -> String
show :: RuntimeError -> String
$cshowList :: [RuntimeError] -> ShowS
showList :: [RuntimeError] -> ShowS
Show