{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
module Untyped where
import PlutusCore.Data hiding (Constr)
import PlutusCore.Default
import UntypedPlutusCore
import Data.ByteString as BS hiding (map)
import Data.Text as T hiding (map)
import Data.Word (Word64)
import GHC.Exts (IsList (..))
import Universe
data UTerm = UVar Integer
| ULambda UTerm
| UApp UTerm UTerm
| UCon (Some (ValueOf DefaultUni))
| UError
| UBuiltin DefaultFun
| UDelay UTerm
| UForce UTerm
| UConstr Integer [UTerm]
| UCase UTerm [UTerm]
deriving Int -> UTerm -> ShowS
[UTerm] -> ShowS
UTerm -> String
(Int -> UTerm -> ShowS)
-> (UTerm -> String) -> ([UTerm] -> ShowS) -> Show UTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UTerm -> ShowS
showsPrec :: Int -> UTerm -> ShowS
$cshow :: UTerm -> String
show :: UTerm -> String
$cshowList :: [UTerm] -> ShowS
showList :: [UTerm] -> 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 NamedDeBruijn DefaultUni DefaultFun a -> UTerm
convP :: forall a. Program NamedDeBruijn DefaultUni DefaultFun a -> UTerm
convP (Program a
_ Version
_ Term NamedDeBruijn DefaultUni DefaultFun a
t) = Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv Term NamedDeBruijn DefaultUni DefaultFun a
t
conv :: Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv :: forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv (Var a
_ NamedDeBruijn
x) = Integer -> UTerm
UVar (Index -> Integer
unIndex (NamedDeBruijn -> Index
ndbnIndex NamedDeBruijn
x) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
conv (LamAbs a
_ NamedDeBruijn
_ Term NamedDeBruijn DefaultUni DefaultFun a
t) = UTerm -> UTerm
ULambda (Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv Term NamedDeBruijn DefaultUni DefaultFun a
t)
conv (Apply a
_ Term NamedDeBruijn DefaultUni DefaultFun a
t Term NamedDeBruijn DefaultUni DefaultFun a
u) = UTerm -> UTerm -> UTerm
UApp (Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv Term NamedDeBruijn DefaultUni DefaultFun a
t) (Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv Term NamedDeBruijn DefaultUni DefaultFun a
u)
conv (Builtin a
_ DefaultFun
b) = DefaultFun -> UTerm
UBuiltin DefaultFun
b
conv (Constant a
_ Some (ValueOf DefaultUni)
c) = Some (ValueOf DefaultUni) -> UTerm
UCon Some (ValueOf DefaultUni)
c
conv (Error a
_) = UTerm
UError
conv (Delay a
_ Term NamedDeBruijn DefaultUni DefaultFun a
t) = UTerm -> UTerm
UDelay (Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv Term NamedDeBruijn DefaultUni DefaultFun a
t)
conv (Force a
_ Term NamedDeBruijn DefaultUni DefaultFun a
t) = UTerm -> UTerm
UForce (Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv Term NamedDeBruijn DefaultUni DefaultFun a
t)
conv (Constr a
_ Word64
i [Term NamedDeBruijn DefaultUni DefaultFun a]
es) = Integer -> [UTerm] -> UTerm
UConstr (Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger Word64
i) ([UTerm] -> [Item [UTerm]]
forall l. IsList l => l -> [Item l]
toList ((Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm)
-> [Term NamedDeBruijn DefaultUni DefaultFun a] -> [UTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv [Term NamedDeBruijn DefaultUni DefaultFun a]
es))
conv (Case a
_ Term NamedDeBruijn DefaultUni DefaultFun a
arg Vector (Term NamedDeBruijn DefaultUni DefaultFun a)
cs) = UTerm -> [UTerm] -> UTerm
UCase (Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv Term NamedDeBruijn DefaultUni DefaultFun a
arg) (Vector UTerm -> [Item (Vector UTerm)]
forall l. IsList l => l -> [Item l]
toList ((Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm)
-> Vector (Term NamedDeBruijn DefaultUni DefaultFun a)
-> Vector UTerm
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
conv Vector (Term NamedDeBruijn DefaultUni DefaultFun a)
cs))
tmnames :: String
tmnames = [Char
'a' .. Char
'z']
uconv :: Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv :: Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv Int
i (UVar Integer
x) = () -> NamedDeBruijn -> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term 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
- Int
1 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 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)))
uconv Int
i (ULambda UTerm
t) = ()
-> NamedDeBruijn
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs
()
(Text -> Index -> NamedDeBruijn
NamedDeBruijn (String -> Text
T.pack [String
tmnames String -> Int -> Char
forall a. HasCallStack => [a] -> Int -> a
!! Int
i]) Index
deBruijnInitIndex)
(Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) UTerm
t)
uconv Int
i (UApp UTerm
t UTerm
u) = ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv Int
i UTerm
t) (Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv Int
i UTerm
u)
uconv Int
i (UCon Some (ValueOf DefaultUni)
c) = ()
-> Some (ValueOf DefaultUni)
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant () Some (ValueOf DefaultUni)
c
uconv Int
i UTerm
UError = () -> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ()
uconv Int
i (UBuiltin DefaultFun
b) = () -> DefaultFun -> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
b
uconv Int
i (UDelay UTerm
t) = ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv Int
i UTerm
t)
uconv Int
i (UForce UTerm
t) = ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv Int
i UTerm
t)
uconv Int
i (UConstr Integer
j [UTerm]
xs) = ()
-> Word64
-> [Term NamedDeBruijn DefaultUni DefaultFun ()]
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr () (Integer -> Word64
forall a. Num a => Integer -> a
fromInteger Integer
j) ((UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ())
-> [UTerm] -> [Term NamedDeBruijn DefaultUni DefaultFun ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv Int
i) [UTerm]
xs)
uconv Int
i (UCase UTerm
t [UTerm]
xs) = ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> Vector (Term NamedDeBruijn DefaultUni DefaultFun ())
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case () (Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv Int
i UTerm
t) ([Item (Vector (Term NamedDeBruijn DefaultUni DefaultFun ()))]
-> Vector (Term NamedDeBruijn DefaultUni DefaultFun ())
forall l. IsList l => [Item l] -> l
fromList ((UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ())
-> [UTerm] -> [Term NamedDeBruijn DefaultUni DefaultFun ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
uconv Int
i) [UTerm]
xs))