Skip to content

Instantly share code, notes, and snippets.

@edsko
Created December 12, 2022 10:19
Show Gist options
  • Save edsko/9007b47e57297ff8217e50ff4e4c8058 to your computer and use it in GitHub Desktop.
Save edsko/9007b47e57297ff8217e50ff4e4c8058 to your computer and use it in GitHub Desktop.
Handwritten PIR code
{-# 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 ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment