-- editorconfig-checker-disable-file
{-# 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 ()

-- this should take a level and render levels as names
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 = ['α','β','γ','δ','ε','ζ','θ','ι','κ','ν','ξ','ο','π','ρ','σ','τ','υ','ϕ','χ','ψ','ω']
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)

-- I have put this here as it needs to be a .hs file so that it can be
-- imported in multiple places

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