{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
module PlutusIR.Certifier (is_dead_code, is_unique) where
import PlutusCore qualified as P (DefaultFun (..), DefaultUni (..), Some (..), SomeTypeIn (..),
ValueOf (..))
import PlutusIR qualified as P
import PlutusIR.Certifier.Extracted qualified as E
import Data.Char
import Data.List.NonEmpty
type EString = E.String
type Term a = P.Term P.TyName P.Name P.DefaultUni P.DefaultFun a
type ETerm = E.Term EString EString EString EString
type Binding a = P.Binding P.TyName P.Name P.DefaultUni P.DefaultFun a
type EBinding = E.Binding EString EString EString EString
type PDatatype a = P.Datatype P.TyName P.Name P.DefaultUni a
type EDatatype = E.Dtdecl EString EString EString
type Type a = P.Type P.TyName P.DefaultUni a
type EType = E.Ty EString EString
type Kind a = P.Kind a
type EKind = E.Kind
type PVarDecl a = P.VarDecl P.TyName P.Name P.DefaultUni a
type EVarDecl = E.Vdecl EString EString EString
type PTyVarDecl a = P.TyVarDecl P.TyName a
type ETyVarDecl = E.Tvdecl EString
type EConstr = E.Constr EString EString EString
glueString :: String -> EString
glueString :: String -> EString
glueString = (Char -> EString -> EString) -> EString -> String -> EString
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Prelude.foldr (Ascii0 -> EString -> EString
E.String0 (Ascii0 -> EString -> EString)
-> (Char -> Ascii0) -> Char -> EString -> EString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Ascii0
glueChar) EString
E.EmptyString
intToNat :: Int -> E.Nat
intToNat :: Int -> Nat
intToNat Int
0 = Nat
E.O
intToNat Int
n
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = String -> Nat
forall a. HasCallStack => String -> a
error String
"intToNat: negative Int"
| Bool
otherwise = Nat -> Nat
E.S (Int -> Nat
intToNat (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
glueChar :: Char -> E.Ascii0
glueChar :: Char -> Ascii0
glueChar = Nat -> Ascii0
E.ascii_of_nat (Nat -> Ascii0) -> (Char -> Nat) -> Char -> Ascii0
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat
intToNat (Int -> Nat) -> (Char -> Int) -> Char -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord
glueNonEmpty :: NonEmpty a -> E.List a
glueNonEmpty :: forall a. NonEmpty a -> List a
glueNonEmpty (a
x :| [a]
xs) = a -> List a -> List a
forall a. a -> List a -> List a
E.Cons a
x ([a] -> List a
forall a. [a] -> List a
glueList [a]
xs)
glueList :: [a] -> E.List a
glueList :: forall a. [a] -> List a
glueList [] = List a
forall a. List a
E.Nil
glueList (a
x : [a]
xs) = a -> List a -> List a
forall a. a -> List a -> List a
E.Cons a
x ([a] -> List a
forall a. [a] -> List a
glueList [a]
xs)
glueTerm :: Term a -> ETerm
glueTerm :: forall a. Term a -> ETerm
glueTerm = \case
P.Let a
_ Recursivity
r NonEmpty (Binding TyName Name DefaultUni DefaultFun a)
bs Term a
t -> Recursivity
-> List (Binding EString EString EString EString) -> ETerm -> ETerm
forall name tyname binderName binderTyname.
Recursivity
-> List (Binding name tyname binderName binderTyname)
-> Term name tyname binderName binderTyname
-> Term name tyname binderName binderTyname
E.Let
(Recursivity -> Recursivity
glueRecursivity Recursivity
r)
(NonEmpty (Binding EString EString EString EString)
-> List (Binding EString EString EString EString)
forall a. NonEmpty a -> List a
glueNonEmpty ((Binding TyName Name DefaultUni DefaultFun a
-> Binding EString EString EString EString)
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun a)
-> NonEmpty (Binding EString EString EString EString)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Binding TyName Name DefaultUni DefaultFun a
-> Binding EString EString EString EString
forall a. Binding a -> Binding EString EString EString EString
glueBinding NonEmpty (Binding TyName Name DefaultUni DefaultFun a)
bs))
(Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t)
P.Var a
_ Name
name -> EString -> ETerm
forall name tyname binderName binderTyname.
name -> Term name tyname binderName binderTyname
E.Var (Name -> EString
glueName Name
name)
P.TyAbs a
_ TyName
tyname Kind a
k Term a
t -> EString -> Kind -> ETerm -> ETerm
forall name tyname binderName binderTyname.
binderTyname
-> Kind
-> Term name tyname binderName binderTyname
-> Term name tyname binderName binderTyname
E.TyAbs (TyName -> EString
glueTyName TyName
tyname) (Kind a -> Kind
forall a. Kind a -> Kind
glueKind Kind a
k) (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t)
P.LamAbs a
_ Name
name Type TyName DefaultUni a
ty Term a
t -> EString -> Ty EString EString -> ETerm -> ETerm
forall name tyname binderName binderTyname.
binderName
-> Ty tyname binderTyname
-> Term name tyname binderName binderTyname
-> Term name tyname binderName binderTyname
E.LamAbs (Name -> EString
glueName Name
name) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
ty) (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t)
P.Apply a
_ Term a
t Term a
t' -> ETerm -> ETerm -> ETerm
forall name tyname binderName binderTyname.
Term name tyname binderName binderTyname
-> Term name tyname binderName binderTyname
-> Term name tyname binderName binderTyname
E.Apply (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t) (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t')
P.Constant a
_ Some (ValueOf DefaultUni)
c -> Some0 ValueOf -> ETerm
forall name tyname binderName binderTyname.
Some0 ValueOf -> Term name tyname binderName binderTyname
E.Constant (Some (ValueOf DefaultUni) -> Some0 ValueOf
glueConstant Some (ValueOf DefaultUni)
c)
P.Builtin a
_ DefaultFun
fun -> DefaultFun -> ETerm
forall name tyname binderName binderTyname.
DefaultFun -> Term name tyname binderName binderTyname
E.Builtin (DefaultFun -> DefaultFun
glueDefaultFun DefaultFun
fun)
P.TyInst a
_ Term a
t Type TyName DefaultUni a
ty -> ETerm -> Ty EString EString -> ETerm
forall name tyname binderName binderTyname.
Term name tyname binderName binderTyname
-> Ty tyname binderTyname
-> Term name tyname binderName binderTyname
E.TyInst (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
ty)
P.Unwrap a
_ Term a
t -> ETerm -> ETerm
forall name tyname binderName binderTyname.
Term name tyname binderName binderTyname
-> Term name tyname binderName binderTyname
E.Unwrap (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t)
P.IWrap a
_ Type TyName DefaultUni a
ty1 Type TyName DefaultUni a
ty2 Term a
t -> Ty EString EString -> Ty EString EString -> ETerm -> ETerm
forall name tyname binderName binderTyname.
Ty tyname binderTyname
-> Ty tyname binderTyname
-> Term name tyname binderName binderTyname
-> Term name tyname binderName binderTyname
E.IWrap (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
ty1) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
ty2) (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t)
P.Error a
_ Type TyName DefaultUni a
ty -> Ty EString EString -> ETerm
forall name tyname binderName binderTyname.
Ty tyname binderTyname -> Term name tyname binderName binderTyname
E.Error (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
ty)
P.Case a
_ Type TyName DefaultUni a
_ Term a
_ [Term a]
_ -> String -> ETerm
forall a. HasCallStack => String -> a
error String
"glueTerm: Case not supported"
P.Constr a
_ Type TyName DefaultUni a
_ Word64
_ [Term a]
_ -> String -> ETerm
forall a. HasCallStack => String -> a
error String
"glueTerm: Constr not supported"
glueRecursivity :: P.Recursivity -> E.Recursivity
glueRecursivity :: Recursivity -> Recursivity
glueRecursivity Recursivity
P.Rec = Recursivity
E.Rec
glueRecursivity Recursivity
P.NonRec = Recursivity
E.NonRec
glueDefaultFun :: P.DefaultFun -> E.DefaultFun
glueDefaultFun :: DefaultFun -> DefaultFun
glueDefaultFun = \case
DefaultFun
P.AddInteger -> DefaultFun
E.AddInteger
DefaultFun
P.SubtractInteger -> DefaultFun
E.SubtractInteger
DefaultFun
P.MultiplyInteger -> DefaultFun
E.MultiplyInteger
DefaultFun
P.DivideInteger -> DefaultFun
E.DivideInteger
DefaultFun
P.QuotientInteger -> DefaultFun
E.QuotientInteger
DefaultFun
P.RemainderInteger -> DefaultFun
E.RemainderInteger
DefaultFun
P.ModInteger -> DefaultFun
E.ModInteger
DefaultFun
P.LessThanInteger -> DefaultFun
E.LessThanInteger
DefaultFun
P.LessThanEqualsInteger -> DefaultFun
E.LessThanEqInteger
DefaultFun
P.EqualsInteger -> DefaultFun
E.EqInteger
DefaultFun
P.Sha2_256 -> DefaultFun
E.SHA2
DefaultFun
P.Sha3_256 -> DefaultFun
E.SHA3
DefaultFun
P.VerifyEd25519Signature -> DefaultFun
E.VerifySignature
DefaultFun
P.EqualsByteString -> DefaultFun
E.EqByteString
DefaultFun
P.LessThanByteString -> DefaultFun
E.LtByteString
DefaultFun
P.IfThenElse -> DefaultFun
E.IfThenElse
DefaultFun
P.AppendString -> DefaultFun
E.Append
DefaultFun
P.Trace -> DefaultFun
E.Trace
DefaultFun
_ -> DefaultFun
E.Trace
glueConstant :: P.Some (P.ValueOf P.DefaultUni) -> E.Some0 E.ValueOf
glueConstant :: Some (ValueOf DefaultUni) -> Some0 ValueOf
glueConstant (P.Some (P.ValueOf DefaultUni (Esc a)
u a
_x)) =
let anyU :: ValueOf
anyU = case DefaultUni (Esc a)
u of
DefaultUni (Esc a)
_ -> () -> ValueOf
forall a b. a -> b
E.unsafeCoerce ()
in DefaultUni -> ValueOf -> Some0 ValueOf
forall f. DefaultUni -> f -> Some0 f
E.Some' (DefaultUni (Esc a) -> DefaultUni
forall a. DefaultUni a -> DefaultUni
glueDefaultUni DefaultUni (Esc a)
u) (ValueOf -> ValueOf
forall a b. a -> b
E.unsafeCoerce ValueOf
anyU)
glueInteger :: Integer -> E.Z
glueInteger :: Integer -> Z
glueInteger Integer
x
| Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Z
E.Z0
| Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Positive -> Z
E.Zpos (Integer -> Positive
gluePositive Integer
x)
| Bool
otherwise = Positive -> Z
E.Zneg (Integer -> Positive
gluePositive (-Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
x))
gluePositive :: Integer -> E.Positive
gluePositive :: Integer -> Positive
gluePositive Integer
n
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = String -> Positive
forall a. HasCallStack => String -> a
error String
"gluePositive: non-positive number provided"
| Bool
otherwise = [Bool] -> Positive
bitsToPos (Integer -> [Bool]
forall {a}. Integral a => a -> [Bool]
go Integer
n)
where
go :: a -> [Bool]
go a
0 = []
go a
m = case a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
divMod a
m a
2 of
(a
r, a
0) -> Bool
False Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: a -> [Bool]
go a
r
(a
r, a
1) -> Bool
True Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: a -> [Bool]
go a
r
(a, a)
_ -> String -> [Bool]
forall a. HasCallStack => String -> a
error String
"gluePositive: impossible"
bitsToPos :: [Bool] -> E.Positive
bitsToPos :: [Bool] -> Positive
bitsToPos [Bool
True] = Positive
E.XH
bitsToPos (Bool
True : [Bool]
xs) = Positive -> Positive
E.XI ([Bool] -> Positive
bitsToPos [Bool]
xs)
bitsToPos (Bool
False : [Bool]
xs) = Positive -> Positive
E.XO ([Bool] -> Positive
bitsToPos [Bool]
xs)
bitsToPos [] =
String -> Positive
forall a. HasCallStack => String -> a
error String
"bitsToPos: positive number should have a most significant (leading) 1 bit"
glueBool :: Bool -> E.Bool
glueBool :: Bool -> Bool
glueBool Bool
True = Bool
E.True
glueBool Bool
False = Bool
E.False
glueStrictness :: P.Strictness -> E.Strictness
glueStrictness :: Strictness -> Strictness
glueStrictness Strictness
P.Strict = Strictness
E.Strict
glueStrictness Strictness
P.NonStrict = Strictness
E.NonStrict
glueVarDecl :: PVarDecl a -> EVarDecl
glueVarDecl :: forall a. PVarDecl a -> EVarDecl
glueVarDecl (P.VarDecl a
_ Name
name Type TyName DefaultUni a
ty) = EString -> Ty EString EString -> EVarDecl
forall tyname binderName binderTyname.
binderName
-> Ty tyname binderTyname -> Vdecl tyname binderName binderTyname
E.VarDecl (Name -> EString
glueName Name
name) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
ty)
glueTyVarDecl :: PTyVarDecl a -> ETyVarDecl
glueTyVarDecl :: forall a. PTyVarDecl a -> ETyVarDecl
glueTyVarDecl (P.TyVarDecl a
_ TyName
tyname Kind a
k) = EString -> Kind -> ETyVarDecl
forall binderTyname. binderTyname -> Kind -> Tvdecl binderTyname
E.TyVarDecl (TyName -> EString
glueTyName TyName
tyname) (Kind a -> Kind
forall a. Kind a -> Kind
glueKind Kind a
k)
glueConstructor :: PVarDecl a -> EConstr
glueConstructor :: forall a. PVarDecl a -> EConstr
glueConstructor (P.VarDecl a
_ Name
name Type TyName DefaultUni a
ty) =
EVarDecl -> Nat -> EConstr
forall tyname binderName binderTyname.
Vdecl tyname binderName binderTyname
-> Nat -> Constr tyname binderName binderTyname
E.Constructor
(EString -> Ty EString EString -> EVarDecl
forall tyname binderName binderTyname.
binderName
-> Ty tyname binderTyname -> Vdecl tyname binderName binderTyname
E.VarDecl (Name -> EString
glueName Name
name)
(Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
ty))
(Type TyName DefaultUni a -> Nat
forall tyname (uni :: * -> *) a. Type tyname uni a -> Nat
arity Type TyName DefaultUni a
ty)
where
arity :: P.Type tyname uni a -> E.Nat
arity :: forall tyname (uni :: * -> *) a. Type tyname uni a -> Nat
arity (P.TyFun a
_ Type tyname uni a
_a Type tyname uni a
b) = Nat -> Nat
E.S (Type tyname uni a -> Nat
forall tyname (uni :: * -> *) a. Type tyname uni a -> Nat
arity Type tyname uni a
b)
arity Type tyname uni a
_ = Nat
E.O
glueDatatype :: PDatatype a -> EDatatype
glueDatatype :: forall a. PDatatype a -> EDatatype
glueDatatype (P.Datatype a
_ TyVarDecl TyName a
tvd [TyVarDecl TyName a]
tvs Name
elim [VarDecl TyName Name DefaultUni a]
cs) =
ETyVarDecl
-> List ETyVarDecl -> EString -> List EConstr -> EDatatype
forall tyname binderName binderTyname.
Tvdecl binderTyname
-> List (Tvdecl binderTyname)
-> binderName
-> List (Constr tyname binderName binderTyname)
-> Dtdecl tyname binderName binderTyname
E.Datatype
(TyVarDecl TyName a -> ETyVarDecl
forall a. PTyVarDecl a -> ETyVarDecl
glueTyVarDecl TyVarDecl TyName a
tvd)
([ETyVarDecl] -> List ETyVarDecl
forall a. [a] -> List a
glueList ((TyVarDecl TyName a -> ETyVarDecl)
-> [TyVarDecl TyName a] -> [ETyVarDecl]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyVarDecl TyName a -> ETyVarDecl
forall a. PTyVarDecl a -> ETyVarDecl
glueTyVarDecl [TyVarDecl TyName a]
tvs))
(Name -> EString
glueName Name
elim)
([EConstr] -> List EConstr
forall a. [a] -> List a
glueList ((VarDecl TyName Name DefaultUni a -> EConstr)
-> [VarDecl TyName Name DefaultUni a] -> [EConstr]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VarDecl TyName Name DefaultUni a -> EConstr
forall a. PVarDecl a -> EConstr
glueConstructor [VarDecl TyName Name DefaultUni a]
cs))
glueBinding :: Binding a -> EBinding
glueBinding :: forall a. Binding a -> Binding EString EString EString EString
glueBinding = \case
P.TermBind a
_ Strictness
s VarDecl TyName Name DefaultUni a
vd Term TyName Name DefaultUni DefaultFun a
t -> Strictness
-> EVarDecl -> ETerm -> Binding EString EString EString EString
forall name tyname binderName binderTyname.
Strictness
-> Vdecl tyname binderName binderTyname
-> Term name tyname binderName binderTyname
-> Binding name tyname binderName binderTyname
E.TermBind (Strictness -> Strictness
glueStrictness Strictness
s) (VarDecl TyName Name DefaultUni a -> EVarDecl
forall a. PVarDecl a -> EVarDecl
glueVarDecl VarDecl TyName Name DefaultUni a
vd) (Term TyName Name DefaultUni DefaultFun a -> ETerm
forall a. Term a -> ETerm
glueTerm Term TyName Name DefaultUni DefaultFun a
t)
P.TypeBind a
_ TyVarDecl TyName a
tvd Type TyName DefaultUni a
ty -> ETyVarDecl
-> Ty EString EString -> Binding EString EString EString EString
forall name tyname binderName binderTyname.
Tvdecl binderTyname
-> Ty tyname binderTyname
-> Binding name tyname binderName binderTyname
E.TypeBind (TyVarDecl TyName a -> ETyVarDecl
forall a. PTyVarDecl a -> ETyVarDecl
glueTyVarDecl TyVarDecl TyName a
tvd) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
ty)
P.DatatypeBind a
_ Datatype TyName Name DefaultUni a
dtd -> EDatatype -> Binding EString EString EString EString
forall name tyname binderName binderTyname.
Dtdecl tyname binderName binderTyname
-> Binding name tyname binderName binderTyname
E.DatatypeBind (Datatype TyName Name DefaultUni a -> EDatatype
forall a. PDatatype a -> EDatatype
glueDatatype Datatype TyName Name DefaultUni a
dtd)
glueName :: P.Name -> EString
glueName :: Name -> EString
glueName (P.Name Text
_str Unique
uniq) = String -> EString
glueString (Unique -> String
forall a. Show a => a -> String
show Unique
uniq)
glueTyName :: P.TyName -> EString
glueTyName :: TyName -> EString
glueTyName (P.TyName Name
n) = Name -> EString
glueName Name
n
glueDefaultUni :: P.DefaultUni a -> E.DefaultUni
glueDefaultUni :: forall a. DefaultUni a -> DefaultUni
glueDefaultUni DefaultUni a
u = case DefaultUni a
u of
DefaultUni a
P.DefaultUniInteger -> DefaultUni
E.DefaultUniInteger
DefaultUni a
P.DefaultUniByteString -> DefaultUni
E.DefaultUniByteString
DefaultUni a
P.DefaultUniString -> DefaultUni
E.DefaultUniString
DefaultUni a
P.DefaultUniUnit -> DefaultUni
E.DefaultUniUnit
DefaultUni a
P.DefaultUniBool -> DefaultUni
E.DefaultUniBool
DefaultUni a
_ -> DefaultUni
E.DefaultUniInteger
glueBuiltinType :: P.SomeTypeIn P.DefaultUni -> E.Some0 ()
glueBuiltinType :: SomeTypeIn DefaultUni -> Some0 ()
glueBuiltinType (P.SomeTypeIn DefaultUni (Esc a)
u) = DefaultUni -> () -> Some0 ()
forall f. DefaultUni -> f -> Some0 f
E.Some' (DefaultUni (Esc a) -> DefaultUni
forall a. DefaultUni a -> DefaultUni
glueDefaultUni DefaultUni (Esc a)
u) ()
glueType :: Type a -> EType
glueType :: forall a. Type a -> Ty EString EString
glueType (P.TyVar a
_ TyName
tyname) = EString -> Ty EString EString
forall tyname binderTyname. tyname -> Ty tyname binderTyname
E.Ty_Var (TyName -> EString
glueTyName TyName
tyname)
glueType (P.TyFun a
_ Type TyName DefaultUni a
t Type TyName DefaultUni a
t') = Ty EString EString -> Ty EString EString -> Ty EString EString
forall tyname binderTyname.
Ty tyname binderTyname
-> Ty tyname binderTyname -> Ty tyname binderTyname
E.Ty_Fun (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
t) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
t')
glueType (P.TyIFix a
_ Type TyName DefaultUni a
t Type TyName DefaultUni a
t') = Ty EString EString -> Ty EString EString -> Ty EString EString
forall tyname binderTyname.
Ty tyname binderTyname
-> Ty tyname binderTyname -> Ty tyname binderTyname
E.Ty_IFix (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
t) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
t')
glueType (P.TyForall a
_ TyName
tyname Kind a
k Type TyName DefaultUni a
t) = EString -> Kind -> Ty EString EString -> Ty EString EString
forall tyname binderTyname.
binderTyname
-> Kind -> Ty tyname binderTyname -> Ty tyname binderTyname
E.Ty_Forall (TyName -> EString
glueTyName TyName
tyname) (Kind a -> Kind
forall a. Kind a -> Kind
glueKind Kind a
k) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
t)
glueType (P.TyBuiltin a
_ SomeTypeIn DefaultUni
b) = Some0 () -> Ty EString EString
forall tyname binderTyname. Some0 () -> Ty tyname binderTyname
E.Ty_Builtin (SomeTypeIn DefaultUni -> Some0 ()
glueBuiltinType SomeTypeIn DefaultUni
b)
glueType (P.TyLam a
_ TyName
tyname Kind a
k Type TyName DefaultUni a
t) = EString -> Kind -> Ty EString EString -> Ty EString EString
forall tyname binderTyname.
binderTyname
-> Kind -> Ty tyname binderTyname -> Ty tyname binderTyname
E.Ty_Lam (TyName -> EString
glueTyName TyName
tyname) (Kind a -> Kind
forall a. Kind a -> Kind
glueKind Kind a
k) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
t)
glueType (P.TyApp a
_ Type TyName DefaultUni a
t Type TyName DefaultUni a
t') = Ty EString EString -> Ty EString EString -> Ty EString EString
forall tyname binderTyname.
Ty tyname binderTyname
-> Ty tyname binderTyname -> Ty tyname binderTyname
E.Ty_App (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
t) (Type TyName DefaultUni a -> Ty EString EString
forall a. Type a -> Ty EString EString
glueType Type TyName DefaultUni a
t')
glueType (P.TySOP a
_ [[Type TyName DefaultUni a]]
_) = String -> Ty EString EString
forall a. HasCallStack => String -> a
error String
"glueType: TySOP not supported"
glueKind :: Kind a -> EKind
glueKind :: forall a. Kind a -> Kind
glueKind (P.Type a
_) = Kind
E.Kind_Base
glueKind (P.KindArrow a
_ Kind a
k1 Kind a
k2) = Kind -> Kind -> Kind
E.Kind_Arrow (Kind a -> Kind
forall a. Kind a -> Kind
glueKind Kind a
k1) (Kind a -> Kind
forall a. Kind a -> Kind
glueKind Kind a
k2)
toBool :: E.Bool -> Bool
toBool :: Bool -> Bool
toBool Bool
E.True = Bool
True
toBool Bool
E.False = Bool
False
is_dead_code :: Term a -> Term a -> Bool
is_dead_code :: forall a. Term a -> Term a -> Bool
is_dead_code Term a
t1 Term a
t2 = Bool -> Bool
toBool (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ETerm -> ETerm -> Bool
E.dec_Term (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t1) (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t2)
is_unique :: Term a -> Bool
is_unique :: forall a. Term a -> Bool
is_unique Term a
t = case ETerm -> Nat -> Option Bool
E.dec_unique (Term a -> ETerm
forall a. Term a -> ETerm
glueTerm Term a
t) Nat
infinity of
E.Some Bool
b -> Bool -> Bool
toBool Bool
b
Option Bool
_ -> Bool
False
where
infinity :: E.Nat
infinity :: Nat
infinity = Nat -> Nat
E.S Nat
infinity