{-# 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

-- Untyped (Raw) syntax

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)])
                -- PLC's debruijn starts counting from 1, while in the metatheory it starts from 0.
                 (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))