Handwritten PIR code

Handwritten.hs

{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE NoImplicitPrelude   #-}
{-# LANGUAGE OverloadedStrings   #-}

module Spec.Plutus.CodeSize.Handwritten where

import PlutusTx.Prelude

import Data.List.NonEmpty (NonEmpty(..))

import PlutusCore qualified as PLC
import PlutusIR.Core.Type qualified as PIR

{-------------------------------------------------------------------------------
  Hand-written terms

  For some examples, it's convenient if we can write PIR by hand, to avoid
  the compilation pipeline "optimizing" the example before we can discuss it.
-------------------------------------------------------------------------------}

type HandwrittenPIR = PIR.Term PLC.TyName PLC.Name PLC.DefaultUni PLC.DefaultFun ()

-- | Illustrate the need for delay/force to replace type arguments
--
-- > boom :: forall a. a -> a
-- > boom = undefined
-- >
-- > id :: forall a. a -> a
-- > id = undefined
-- >
-- > example :: Bool -> (forall a. a -> a)
-- > example b = if b then boom else id
--
-- This example is hand-crafted to get exactly the code we want.
handwrittenBoom :: HandwrittenPIR
handwrittenBoom =
      PIR.Let () PIR.NonRec (bindingBoom :| [bindingId])
    $ PIR.LamAbs () nameB typeBool
    $ (       PIR.TyInst () (PIR.Builtin () PLC.IfThenElse) typeId
        `app` PIR.Var () nameB
        `app` PIR.Var () nameBoom
        `app` PIR.Var () nameId
      )
  where
    --
    -- BINDINGS
    --

    bindingBoom :: PIR.Binding PIR.TyName PIR.Name PLC.DefaultUni PLC.DefaultFun ()
    bindingBoom =
        PIR.TermBind ()
          PIR.Strict
          (PIR.VarDecl () nameBoom typeId)
          termBoom

    bindingId :: PIR.Binding PIR.TyName PIR.Name PLC.DefaultUni PLC.DefaultFun ()
    bindingId =
        PIR.TermBind ()
          PIR.Strict
          (PIR.VarDecl () nameId typeId)
          termId

    --
    -- TYPES
    --

    typeBool :: PIR.Type PIR.TyName PLC.DefaultUni ()
    typeBool =  PLC.TyBuiltin () (PLC.SomeTypeIn PLC.DefaultUniBool)

    -- forall a. a -> a
    typeId :: PIR.Type PIR.TyName PLC.DefaultUni ()
    typeId =
          PLC.TyForall () tynameA (PLC.Type ())
        $ PLC.TyVar () tynameA `tyFun` PLC.TyVar () tynameA

    --
    -- TERMS
    --

    -- \{a}. ERROR {a -> a}
    termBoom :: PIR.Term PIR.TyName PIR.Name PLC.DefaultUni PLC.DefaultFun ()
    termBoom =
          PIR.TyAbs () tynameA (PIR.Type ())
        $ PIR.Error () (PIR.TyVar () tynameA `tyFun` PIR.TyVar () tynameA)

    -- \{a} (x :: a). x
    termId :: PIR.Term PIR.TyName PIR.Name PLC.DefaultUni PLC.DefaultFun ()
    termId =
          PIR.TyAbs () tynameA (PIR.Type ())
        $ PIR.LamAbs () nameX (PIR.TyVar () tynameA)
        $ PIR.Var () nameX

    --
    -- NAMES
    --

    nameBoom, nameId, nameB, nameX :: PLC.Name
    nameBoom = PLC.Name "boom" (PLC.Unique 0)
    nameId   = PLC.Name "id"   (PLC.Unique 1)
    nameB    = PLC.Name "b"    (PLC.Unique 2)
    nameX    = PLC.Name "x"    (PLC.Unique 3)

    tynameA :: PLC.TyName
    tynameA = PLC.TyName $ PLC.Name "a" (PLC.Unique 100)

    --
    -- INFIX OPERATORS
    --

    infixr `tyFun`
    tyFun ::
          PIR.Type tyname uni ()
       -> PIR.Type tyname uni ()
       -> PIR.Type tyname uni ()
    tyFun = PLC.TyFun ()

    infixl `app`
    app ::
         PIR.Term tyname name uni fun ()
      -> PIR.Term tyname name uni fun ()
      -> PIR.Term tyname name uni fun ()
    app = PIR.Apply ()