{-# LANGUAGE GADTs      #-}
{-# LANGUAGE LambdaCase #-}

-- Still some stuff that isn't used yet
{-# OPTIONS_GHC -Wno-unused-top-binds #-}

-- | Interface to automatically extracted code from plutus-cert (Coq):
-- - Conversion functions for PIR's AST to the representation in Coq.
-- - Boolean decision procedures for translation relations
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
  -- P.GreaterThanInteger   -> E.GreaterThanInteger
  -- P.GreaterThanEqInteger -> E.GreaterThanEqInteger
  DefaultFun
P.EqualsInteger          -> DefaultFun
E.EqInteger
  -- P.Concatenate          -> E.Concatenate
  -- P.TakeByteString       -> E.TakeByteString
  -- P.DropByteString       -> E.DropByteString
  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
  -- P.GtByteString         -> E.GtByteString
  DefaultFun
P.IfThenElse             -> DefaultFun
E.IfThenElse
  -- P.CharToString         -> E.CharToString
  DefaultFun
P.AppendString           -> DefaultFun
E.Append
  DefaultFun
P.Trace                  -> DefaultFun
E.Trace

  -- TODO: support current set of builtin functions
  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 ()
        -- P.DefaultUniInteger    -> E.unsafeCoerce (glueInteger x)
        -- P.DefaultUniChar       -> E.unsafeCoerce (glueChar x)
        -- P.DefaultUniUnit       -> E.unsafeCoerce x -- same rep ()
        -- P.DefaultUniBool       -> E.unsafeCoerce (glueBool x)
        -- P.DefaultUniString     -> E.unsafeCoerce (glueString x)
        -- P.DefaultUniByteString -> E.unsafeCoerce (glueString (show x))
  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))



-- Coq's representation of Positive: https://coq.inria.fr/library/Coq.Numbers.BinNums.html
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)

-- This is hacky: we use (unique) strings for variable names in Coq,
-- so we just `show` the Unique
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
  -- TODO: implement current constructors of DefaultUni
  -- _                      -> E.DefaultUniInteger
  DefaultUni a
P.DefaultUniInteger    -> DefaultUni
E.DefaultUniInteger
  DefaultUni a
P.DefaultUniByteString -> DefaultUni
E.DefaultUniByteString
  DefaultUni a
P.DefaultUniString     -> DefaultUni
E.DefaultUniString
  -- P.DefaultUniChar       -> E.DefaultUniChar
  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')
-- TODO: Support TySOP
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)


-- * Decision procedures for translation relations

toBool :: E.Bool -> Bool
toBool :: Bool -> Bool
toBool Bool
E.True  = Bool
True
toBool Bool
E.False = Bool
False

-- | Check if only pure let bindings were eliminated
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)

-- | Check if a term has unique binders
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