michaelpj

-- A stateful funciton with a counter and a boolean saying if it has terminated
-- We use bracket to always set the termination boolean, even if there is an exception
-- in the initial action.
ghci> let f st act = 
  bracket 
    (pure ()) 
    (\_ -> modify st (\(c,fin) -> (c, True))) 
    (\_ -> do { act; modify st (\(c, fin) -> ((c + 1), fin)) })
ghci> :t f
f :: (st :> es, Num a1) =>

michaelpj

{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
module Traversable1 where

import Data.Functor.Apply
import Data.Semigroup.Foldable
import Data.Semigroup.Traversable

-- | Apply a non-empty container of functions to a possibly-empty-with-unit container of values.
(<.*>) :: (Apply f) => f (a -> b) -> MaybeApply f a -> f b

michaelpj

{ pkgs ? import ./nixpkgs.nix
, haskellCompiler ? "ghc865"
}:

let
  haskellNix = import (builtins.fetchTarball
    ( "https://github.com/input-output-hk/haskell.nix/archive/"
    + "59cf05606e7efbbc4741ae28fd8cc610cec94eb8.tar.gz"
    )) {};
  nixpkgsSrc = haskellNix.sources.nixpkgs-default;

michaelpj

cradle:
  multi:
    - path: ./.
      config:
        cradle:
          cabal:
    - path: ./.
      config:
        cradle:
          cabal:

michaelpj

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

michaelpj

-- | Vesting scheme as a PLC contract
module Vesting where

import           Control.Monad                (void)

import qualified Language.PlutusTx            as PlutusTx
import qualified Ledger.Interval              as Interval
import qualified Language.PlutusTx.Prelude    as P
import           Ledger
import           Ledger.Ada                   (Ada)

michaelpj

{-# OPTIONS --type-in-type #-}

fstFun : ∀ {A B} -> A -> B -> A
fstFun x _ = x

sndFun : ∀ {A B} -> A -> B -> B
sndFun _ y = y

uncurryFun : ∀ {A B C} -> (A -> B -> C) -> (∀ {R} -> (A -> B -> R) -> R) -> C
uncurryFun f k = f (k fstFun) (k sndFun)

michaelpj

-- In "readable" notation. "Definitions" are for clarity and will in fact all appear inline.

Pair :: * -> * -> *
Pair = 
  -- type params
  \a :: * . \b :: * .
  -- match output type
  forall t :: * . 
  -- matcher type
  a -> b -> t

michaelpj

delay :: MonadQuote m => (PC.Term PC.TyName PC.Name ()) -> m (PC.Term PC.TyName PC.Name ())
delay body = PC.LamAbs () <$> safeFreshName "thunk" <*> liftQuote Unit.getBuiltinUnit <*> pure body

delayType :: MonadQuote m => (PC.Type PC.Tyname ()) -> m (PC.Type PC.Tyname ())
delayType orig = PC.TyFun () <$> liftQuote Unit.getBuiltinUnit <*> pure orig

force :: MonadQuote m => (PC.Term PC.TyName PC.Name ()) -> m (PC.Term PC.TyName PC.Name ())
force thunk = PC.Apply () thunk <$> liftQuote Unit.getBuiltinUnitval

delayFunction :: MonadQuote m => (PC.Type PC.Tyname ()) -> (PC.Term PC.TyName PC.Name ()) -> m (PC.Term PC.TyName PC.Name ())

michaelpj

(program 1.0.0
  [
    (lam
      fib_37
      (fun [(con integer) (con 64)] [(con integer) (con 64)])
      [ fib_37 (con 64 ! 4) ]
    )
    [
      {
        {