{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DerivingVia           #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE NumericUnderscores    #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Plutus.Contract.Test.Coverage.Analysis.DeBruijn where

import Control.Arrow hiding ((<+>))
import Data.List hiding (insert)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Maybe
import GHC.Stack
import PlutusCore.DeBruijn hiding (DeBruijn)
import PlutusCore.Name
import PlutusIR
import PlutusTx.Code
import PlutusTx.Code qualified as PlutusTx

import Plutus.Contract.Test.Coverage.Analysis.Common

-- *** Conversion to DeBruijn

type DBCtx nm = [nm]

class Eq n => IsName n where
  type DeBruijn n
  mkDeBruijn :: n -> Index -> DeBruijn n

instance IsName Name where
  type DeBruijn Name = NamedDeBruijn
  mkDeBruijn :: Name -> Index -> DeBruijn Name
mkDeBruijn (Name Text
t Unique
_) Index
i = Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
t Index
i

instance IsName TyName where
  type DeBruijn TyName = NamedTyDeBruijn
  mkDeBruijn :: TyName -> Index -> DeBruijn TyName
mkDeBruijn (TyName Name
n) Index
i = NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (Name -> Index -> DeBruijn Name
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn Name
n Index
i)

class IsDbName n where
  setDbIndex :: n -> Index -> n
  getDbIndex :: n -> Index

instance IsDbName NamedDeBruijn where
  setDbIndex :: NamedDeBruijn -> Index -> NamedDeBruijn
setDbIndex (NamedDeBruijn Text
x Index
_) Index
i = Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
x Index
i
  getDbIndex :: NamedDeBruijn -> Index
getDbIndex (NamedDeBruijn Text
_ Index
i) = Index
i

instance IsDbName NamedTyDeBruijn where
  setDbIndex :: NamedTyDeBruijn -> Index -> NamedTyDeBruijn
setDbIndex (NamedTyDeBruijn NamedDeBruijn
x) Index
i = NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (NamedDeBruijn -> Index -> NamedDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedDeBruijn
x Index
i)
  getDbIndex :: NamedTyDeBruijn -> Index
getDbIndex (NamedTyDeBruijn NamedDeBruijn
x) = NamedDeBruijn -> Index
forall n. IsDbName n => n -> Index
getDbIndex NamedDeBruijn
x

deBruijn :: HasCallStack => IsName n => DBCtx n -> n -> DeBruijn n
deBruijn :: DBCtx n -> n -> DeBruijn n
deBruijn DBCtx n
ctx n
n = case (n -> Bool) -> DBCtx n -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (n -> n -> Bool
forall a. Eq a => a -> a -> Bool
==n
n) DBCtx n
ctx of
  Maybe Int
Nothing -> [Char] -> DeBruijn n
forall a. HasCallStack => [Char] -> a
error [Char]
"no dumb here - this is a no dumb area"
  Just Int
i  -> n -> Index -> DeBruijn n
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn n
n (Index -> DeBruijn n) -> Index -> DeBruijn n
forall a b. (a -> b) -> a -> b
$ Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i

extendDBCtx :: HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx :: DBCtx n -> n -> DBCtx n
extendDBCtx = (n -> DBCtx n -> DBCtx n) -> DBCtx n -> n -> DBCtx n
forall a b c. (a -> b -> c) -> b -> a -> c
flip (:)

toDeBruijn_Trm :: HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm :: DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm DBCtx TyName
tyCtx DBCtx Name
trmCtx Trm'
trm = case Trm'
trm of
  Let ()
_ Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds Trm'
body
    | Recursivity
Rec <- Recursivity
rec ->
      let (DBCtx TyName
tyCtx', DBCtx Name
trmCtx') = ((DBCtx TyName, DBCtx Name)
 -> Binding TyName Name DefaultUni DefaultFun ()
 -> (DBCtx TyName, DBCtx Name))
-> (DBCtx TyName, DBCtx Name)
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> (DBCtx TyName, DBCtx Name)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl HasCallStack =>
(DBCtx TyName, DBCtx Name)
-> Binding TyName Name DefaultUni DefaultFun ()
-> (DBCtx TyName, DBCtx Name)
(DBCtx TyName, DBCtx Name)
-> Binding TyName Name DefaultUni DefaultFun ()
-> (DBCtx TyName, DBCtx Name)
bindCtx_Bind (DBCtx TyName
tyCtx, DBCtx Name
trmCtx) NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds in
      ()
-> Recursivity
-> NonEmpty
     (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> Trm
-> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec (HasCallStack =>
Bool
-> DBCtx TyName
-> DBCtx Name
-> Binding TyName Name DefaultUni DefaultFun ()
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
Bool
-> DBCtx TyName
-> DBCtx Name
-> Binding TyName Name DefaultUni DefaultFun ()
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
toDeBruijn_Bind Bool
True DBCtx TyName
tyCtx' DBCtx Name
trmCtx' (Binding TyName Name DefaultUni DefaultFun ()
 -> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> NonEmpty
     (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds) (HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm DBCtx TyName
tyCtx' DBCtx Name
trmCtx' Trm'
body)
    | Bool
otherwise  ->
      let (NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
binds', (DBCtx TyName
tyCtx', DBCtx Name
trmCtx')) = (DBCtx TyName, DBCtx Name)
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> (NonEmpty
      (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()),
    (DBCtx TyName, DBCtx Name))
go' (DBCtx TyName
tyCtx, DBCtx Name
trmCtx) NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds in
      ()
-> Recursivity
-> NonEmpty
     (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> Trm
-> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
binds' (HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm DBCtx TyName
tyCtx' DBCtx Name
trmCtx' Trm'
body)
      where
        go' :: (DBCtx TyName, DBCtx Name)
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> (NonEmpty
      (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()),
    (DBCtx TyName, DBCtx Name))
go' ctxs :: (DBCtx TyName, DBCtx Name)
ctxs@(DBCtx TyName
tyCtx, DBCtx Name
trmCtx) (Binding TyName Name DefaultUni DefaultFun ()
bind :| [Binding TyName Name DefaultUni DefaultFun ()]
binds) = ([Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
 -> NonEmpty
      (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()))
-> ([Binding
       NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()],
    (DBCtx TyName, DBCtx Name))
-> (NonEmpty
      (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()),
    (DBCtx TyName, DBCtx Name))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (HasCallStack =>
Bool
-> DBCtx TyName
-> DBCtx Name
-> Binding TyName Name DefaultUni DefaultFun ()
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
Bool
-> DBCtx TyName
-> DBCtx Name
-> Binding TyName Name DefaultUni DefaultFun ()
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
toDeBruijn_Bind Bool
False DBCtx TyName
tyCtx DBCtx Name
trmCtx Binding TyName Name DefaultUni DefaultFun ()
bind Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> NonEmpty
     (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
forall a. a -> [a] -> NonEmpty a
:|)
                                                         ((DBCtx TyName, DBCtx Name)
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> ([Binding
       NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()],
    (DBCtx TyName, DBCtx Name))
go (HasCallStack =>
(DBCtx TyName, DBCtx Name)
-> Binding TyName Name DefaultUni DefaultFun ()
-> (DBCtx TyName, DBCtx Name)
(DBCtx TyName, DBCtx Name)
-> Binding TyName Name DefaultUni DefaultFun ()
-> (DBCtx TyName, DBCtx Name)
bindCtx_Bind (DBCtx TyName, DBCtx Name)
ctxs Binding TyName Name DefaultUni DefaultFun ()
bind) [Binding TyName Name DefaultUni DefaultFun ()]
binds)
        go :: (DBCtx TyName, DBCtx Name)
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> ([Binding
       NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()],
    (DBCtx TyName, DBCtx Name))
go (DBCtx TyName, DBCtx Name)
ctxs []                           = ([], (DBCtx TyName, DBCtx Name)
ctxs)
        go ctxs :: (DBCtx TyName, DBCtx Name)
ctxs@(DBCtx TyName
tyCtx, DBCtx Name
trmCtx) (Binding TyName Name DefaultUni DefaultFun ()
bind:[Binding TyName Name DefaultUni DefaultFun ()]
binds) = ([Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
 -> [Binding
       NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()])
-> ([Binding
       NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()],
    (DBCtx TyName, DBCtx Name))
-> ([Binding
       NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()],
    (DBCtx TyName, DBCtx Name))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (HasCallStack =>
Bool
-> DBCtx TyName
-> DBCtx Name
-> Binding TyName Name DefaultUni DefaultFun ()
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
Bool
-> DBCtx TyName
-> DBCtx Name
-> Binding TyName Name DefaultUni DefaultFun ()
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
toDeBruijn_Bind Bool
False DBCtx TyName
tyCtx DBCtx Name
trmCtx Binding TyName Name DefaultUni DefaultFun ()
bind Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
forall a. a -> [a] -> [a]
:)
                                                     ((DBCtx TyName, DBCtx Name)
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> ([Binding
       NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()],
    (DBCtx TyName, DBCtx Name))
go (HasCallStack =>
(DBCtx TyName, DBCtx Name)
-> Binding TyName Name DefaultUni DefaultFun ()
-> (DBCtx TyName, DBCtx Name)
(DBCtx TyName, DBCtx Name)
-> Binding TyName Name DefaultUni DefaultFun ()
-> (DBCtx TyName, DBCtx Name)
bindCtx_Bind (DBCtx TyName, DBCtx Name)
ctxs Binding TyName Name DefaultUni DefaultFun ()
bind) [Binding TyName Name DefaultUni DefaultFun ()]
binds)

  Error ()
_ Type TyName DefaultUni ()
ty -> () -> Type NamedTyDeBruijn DefaultUni () -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error () (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
ty)

  Var ()
_ Name
x -> () -> NamedDeBruijn -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () (NamedDeBruijn -> Trm) -> NamedDeBruijn -> Trm
forall a b. (a -> b) -> a -> b
$ DBCtx Name -> Name -> DeBruijn Name
forall n. (HasCallStack, IsName n) => DBCtx n -> n -> DeBruijn n
deBruijn DBCtx Name
trmCtx Name
x

  TyAbs ()
_ TyName
x Kind ()
k Trm'
t -> () -> NamedTyDeBruijn -> Kind () -> Trm -> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs () (TyName -> Index -> DeBruijn TyName
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn TyName
x Index
0) Kind ()
k (Trm -> Trm) -> Trm -> Trm
forall a b. (a -> b) -> a -> b
$ HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm (DBCtx TyName -> TyName -> DBCtx TyName
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx TyName
tyCtx TyName
x) DBCtx Name
trmCtx Trm'
t

  LamAbs ()
_ Name
x Type TyName DefaultUni ()
a Trm'
t -> ()
-> NamedDeBruijn
-> Type NamedTyDeBruijn DefaultUni ()
-> Trm
-> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () (Name -> Index -> DeBruijn Name
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn Name
x Index
0) (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
a) (Trm -> Trm) -> Trm -> Trm
forall a b. (a -> b) -> a -> b
$
                                HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm DBCtx TyName
tyCtx (DBCtx Name -> Name -> DBCtx Name
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx Name
trmCtx Name
x) Trm'
t

  Apply ()
_ Trm'
t Trm'
t' -> () -> Trm -> Trm -> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () (HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm DBCtx TyName
tyCtx DBCtx Name
trmCtx Trm'
t) (HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm DBCtx TyName
tyCtx DBCtx Name
trmCtx Trm'
t')

  TyInst ()
_ Trm'
t Type TyName DefaultUni ()
a -> () -> Trm -> Type NamedTyDeBruijn DefaultUni () -> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () (HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm DBCtx TyName
tyCtx DBCtx Name
trmCtx Trm'
t) (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
a)

  Constant ()
_ Some (ValueOf DefaultUni)
c -> () -> Some (ValueOf DefaultUni) -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant () Some (ValueOf DefaultUni)
c

  Builtin ()
_ DefaultFun
b  -> () -> DefaultFun -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> fun -> Term tyname name uni fun a
Builtin () DefaultFun
b

  IWrap{}      -> [Char] -> Trm
forall a. HasCallStack => [Char] -> a
error [Char]
"toDeBruijn_Trm: IWrap"
  Unwrap{}     -> [Char] -> Trm
forall a. HasCallStack => [Char] -> a
error [Char]
"toDeBruijn_Trm: Unwrap"

toDeBruijn_Typ :: HasCallStack => DBCtx TyName -> Typ' -> Typ
toDeBruijn_Typ :: DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
a = case Type TyName DefaultUni ()
a of
  TyVar ()
_ TyName
x        -> () -> NamedTyDeBruijn -> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () (DBCtx TyName -> TyName -> DeBruijn TyName
forall n. (HasCallStack, IsName n) => DBCtx n -> n -> DeBruijn n
deBruijn DBCtx TyName
tyCtx TyName
x)
  TyBuiltin ()
_ SomeTypeIn DefaultUni
b    -> () -> SomeTypeIn DefaultUni -> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin () SomeTypeIn DefaultUni
b
  TyFun ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b      -> ()
-> 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 () (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
a) (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
b)
  TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
a -> ()
-> 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 () (TyName -> Index -> DeBruijn TyName
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn TyName
x Index
0) Kind ()
k (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ (DBCtx TyName -> TyName -> DBCtx TyName
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx TyName
tyCtx TyName
x) Type TyName DefaultUni ()
a)
  TyLam ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
a    -> ()
-> 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 () (TyName -> Index -> DeBruijn TyName
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn TyName
x Index
0) Kind ()
k (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ (DBCtx TyName -> TyName -> DBCtx TyName
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx TyName
tyCtx TyName
x) Type TyName DefaultUni ()
a)
  TyApp ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b      -> ()
-> 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 () (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
a) (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
b)
  TyIFix ()
_ Type TyName DefaultUni ()
_ Type TyName DefaultUni ()
_     -> [Char] -> Type NamedTyDeBruijn DefaultUni ()
forall a. HasCallStack => [Char] -> a
error [Char]
"normalizeType: TyIFix"

bindCtx_Dat :: HasCallStack => (DBCtx TyName, DBCtx Name) -> Dat' -> (DBCtx TyName, DBCtx Name)
bindCtx_Dat :: (DBCtx TyName, DBCtx Name) -> Dat' -> (DBCtx TyName, DBCtx Name)
bindCtx_Dat (DBCtx TyName
tyCtx, DBCtx Name
trmCtx) (Datatype ()
_ (TyVarDecl ()
_ TyName
n Kind ()
_) [TyVarDecl TyName ()]
_ Name
match [VarDecl TyName Name DefaultUni DefaultFun ()]
constrs) =
  (DBCtx TyName -> TyName -> DBCtx TyName
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx TyName
tyCtx TyName
n, (DBCtx Name -> Name -> DBCtx Name)
-> DBCtx Name -> DBCtx Name -> DBCtx Name
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DBCtx Name -> Name -> DBCtx Name
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx Name
trmCtx (DBCtx Name -> DBCtx Name) -> DBCtx Name -> DBCtx Name
forall a b. (a -> b) -> a -> b
$ Name
match Name -> DBCtx Name -> DBCtx Name
forall a. a -> [a] -> [a]
: [ Name
x | VarDecl ()
_ Name
x Type TyName DefaultUni ()
_ <- [VarDecl TyName Name DefaultUni DefaultFun ()]
constrs])

toDeBruijn_Dat :: HasCallStack => Bool -> DBCtx TyName -> Dat' -> Dat
toDeBruijn_Dat :: Bool -> DBCtx TyName -> Dat' -> Dat
toDeBruijn_Dat Bool
rec DBCtx TyName
tyCtx (Datatype ()
_ (TyVarDecl ()
_ TyName
n Kind ()
k) [TyVarDecl TyName ()]
args Name
match [VarDecl TyName Name DefaultUni DefaultFun ()]
constrs) =
  let tyCtx' :: DBCtx TyName
tyCtx' = (DBCtx TyName -> TyName -> DBCtx TyName)
-> DBCtx TyName -> DBCtx TyName -> DBCtx TyName
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DBCtx TyName -> TyName -> DBCtx TyName
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx TyName
tyCtx ([ TyName
n | Bool -> Bool
not Bool
rec ] DBCtx TyName -> DBCtx TyName -> DBCtx TyName
forall a. [a] -> [a] -> [a]
++ [ TyName
n | TyVarDecl ()
_ TyName
n Kind ()
_ <- [TyVarDecl TyName ()]
args ]) in
  ()
-> TyVarDecl NamedTyDeBruijn ()
-> [TyVarDecl NamedTyDeBruijn ()]
-> NamedDeBruijn
-> [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> Dat
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
Datatype () (() -> NamedTyDeBruijn -> Kind () -> TyVarDecl NamedTyDeBruijn ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () (TyName -> Index -> DeBruijn TyName
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn TyName
n Index
0) Kind ()
k)
              [() -> NamedTyDeBruijn -> Kind () -> TyVarDecl NamedTyDeBruijn ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () (TyName -> Index -> DeBruijn TyName
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn TyName
n Index
0) Kind ()
k | TyVarDecl ()
_ TyName
n Kind ()
k <- [TyVarDecl TyName ()]
args]
              (Name -> Index -> DeBruijn Name
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn Name
match Index
0)
              [()
-> NamedDeBruijn
-> Type NamedTyDeBruijn DefaultUni ()
-> VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl () (Name -> Index -> DeBruijn Name
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn Name
c Index
0) (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx' Type TyName DefaultUni ()
ty) | VarDecl ()
_ Name
c Type TyName DefaultUni ()
ty <- [VarDecl TyName Name DefaultUni DefaultFun ()]
constrs]

bindCtx_Bind :: HasCallStack => (DBCtx TyName, DBCtx Name) -> Bind' -> (DBCtx TyName, DBCtx Name)
bindCtx_Bind :: (DBCtx TyName, DBCtx Name)
-> Binding TyName Name DefaultUni DefaultFun ()
-> (DBCtx TyName, DBCtx Name)
bindCtx_Bind (DBCtx TyName
tyCtx, DBCtx Name
trmCtx) (TermBind ()
_ Strictness
_ (VarDecl ()
_ Name
x Type TyName DefaultUni ()
_) Trm'
_) = (DBCtx TyName
tyCtx, DBCtx Name -> Name -> DBCtx Name
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx Name
trmCtx Name
x)
bindCtx_Bind (DBCtx TyName
tyCtx, DBCtx Name
trmCtx) (TypeBind ()
_ (TyVarDecl ()
_ TyName
x Kind ()
_) Type TyName DefaultUni ()
_) = (DBCtx TyName -> TyName -> DBCtx TyName
forall n. HasCallStack => DBCtx n -> n -> DBCtx n
extendDBCtx DBCtx TyName
tyCtx TyName
x, DBCtx Name
trmCtx)
bindCtx_Bind (DBCtx TyName, DBCtx Name)
ctxs (DatatypeBind ()
_ Dat'
dat)                        = HasCallStack =>
(DBCtx TyName, DBCtx Name) -> Dat' -> (DBCtx TyName, DBCtx Name)
(DBCtx TyName, DBCtx Name) -> Dat' -> (DBCtx TyName, DBCtx Name)
bindCtx_Dat (DBCtx TyName, DBCtx Name)
ctxs Dat'
dat

toDeBruijn_Bind :: HasCallStack => Bool -> DBCtx TyName -> DBCtx Name -> Bind' -> Bind
toDeBruijn_Bind :: Bool
-> DBCtx TyName
-> DBCtx Name
-> Binding TyName Name DefaultUni DefaultFun ()
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
toDeBruijn_Bind Bool
_ DBCtx TyName
tyCtx DBCtx Name
trmCtx (TermBind ()
_ Strictness
s (VarDecl ()
_ Name
x Type TyName DefaultUni ()
ty) Trm'
body) =
  ()
-> Strictness
-> VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> Trm
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind () Strictness
s (()
-> NamedDeBruijn
-> Type NamedTyDeBruijn DefaultUni ()
-> VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl () (Name -> Index -> DeBruijn Name
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn Name
x Index
0) (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
ty)) (HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm DBCtx TyName
tyCtx DBCtx Name
trmCtx Trm'
body)
toDeBruijn_Bind Bool
_ DBCtx TyName
tyCtx DBCtx Name
_ (TypeBind ()
_ (TyVarDecl ()
_ TyName
x Kind ()
k) Type TyName DefaultUni ()
ty) =
  ()
-> TyVarDecl NamedTyDeBruijn ()
-> Type NamedTyDeBruijn DefaultUni ()
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind () (() -> NamedTyDeBruijn -> Kind () -> TyVarDecl NamedTyDeBruijn ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () (TyName -> Index -> DeBruijn TyName
forall n. IsName n => n -> Index -> DeBruijn n
mkDeBruijn TyName
x Index
0) Kind ()
k) (HasCallStack =>
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName
-> Type TyName DefaultUni () -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ DBCtx TyName
tyCtx Type TyName DefaultUni ()
ty)
toDeBruijn_Bind Bool
r DBCtx TyName
tyCtx DBCtx Name
_ (DatatypeBind ()
_ Dat'
dat) =
  ()
-> Dat
-> Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind () (HasCallStack => Bool -> DBCtx TyName -> Dat' -> Dat
Bool -> DBCtx TyName -> Dat' -> Dat
toDeBruijn_Dat Bool
r DBCtx TyName
tyCtx Dat'
dat)

getTrm :: HasCallStack => CompiledCode a -> Trm
getTrm :: CompiledCode a -> Trm
getTrm CompiledCode a
cc = let Program ()
_ Trm'
t = Maybe (Program TyName Name DefaultUni DefaultFun ())
-> Program TyName Name DefaultUni DefaultFun ()
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Program TyName Name DefaultUni DefaultFun ())
 -> Program TyName Name DefaultUni DefaultFun ())
-> Maybe (Program TyName Name DefaultUni DefaultFun ())
-> Program TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ CompiledCode a
-> Maybe (Program TyName Name DefaultUni DefaultFun ())
forall (uni :: * -> *) fun a.
(Closed uni, Everywhere uni Flat, Flat fun) =>
CompiledCodeIn uni fun a -> Maybe (Program TyName Name uni fun ())
PlutusTx.getPir CompiledCode a
cc in HasCallStack => DBCtx TyName -> DBCtx Name -> Trm' -> Trm
DBCtx TyName -> DBCtx Name -> Trm' -> Trm
toDeBruijn_Trm [] [] Trm'
t