Skip to content

Instantly share code, notes, and snippets.

@j-mueller

j-mueller/Multisig.hs

Last active May 14, 2019 11:16
Show Gist options
  • Save j-mueller/e931d0f7e2220f5499488458bcab4107 to your computer and use it in GitHub Desktop.
Save j-mueller/e931d0f7e2220f5499488458bcab4107 to your computer and use it in GitHub Desktop.
Download ZIP
Multisig PLC
Raw
Multisig.hs
validate :: MultiSig -> () -> () -> PendingTx -> ()
validate =
let
validate (MultiSig keys num) () () p =
let
present = $$(P.length) ($$(P.filter) ($$(V.txSignedBy) p) keys)
in
if $$(P.geq) present num
then ()
else $$(P.error) ($$(P.traceH) "WRONG!" ())
in
validate
Raw
Multisig.pir
(program
(let
(nonrec)
(termbind (vardecl emptyString (con string)) (con ))
(let
(nonrec)
(termbind
(vardecl appendString (fun (con string) (fun (con string) (con string)))
)
(builtin append)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl PendingTxOutType (type))
PendingTxOutType_match
(vardecl DataTxOut PendingTxOutType)
(vardecl PubKeyTxOut (fun (con bytestring) PendingTxOutType))
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl Tuple2 (fun (type) (fun (type) (type))))
(tyvardecl a (type)) (tyvardecl b (type))
Tuple2_match
(vardecl Tuple2 (fun a (fun b [[Tuple2 a] b])))
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl Unit (fun (type) (type)))
(tyvardecl a (type))
Unit_match
(vardecl Unit (fun a [Unit a]))
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl Unit (type)) Unit_match (vardecl Unit Unit)
)
)
(let
(nonrec)
(termbind
(vardecl trace (fun (con string) Unit))
(lam
arg
(con string)
[
(lam b (all a (type) (fun a a)) Unit)
[ (builtin trace) arg ]
]
)
)
(let
(nonrec)
(termbind
(vardecl error (all a (type) (fun Unit a)))
(abs e (type) (lam thunk Unit (error e)))
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl Maybe (fun (type) (type)))
(tyvardecl a (type))
Maybe_match
(vardecl Just (fun a [Maybe a]))
(vardecl Nothing [Maybe a])
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl Interval (fun (type) (type)))
(tyvardecl a (type))
Interval_match
(vardecl
Interval
(fun [Maybe a] (fun [Maybe a] [Interval a]))
)
)
)
(let
(rec)
(datatypebind
(datatype
(tyvardecl List (fun (type) (type)))
(tyvardecl a (type))
Nil_match
(vardecl Nil [List a])
(vardecl Cons (fun a (fun [List a] [List a])))
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl Map (fun (type) (fun (type) (type))))
(tyvardecl k (type)) (tyvardecl v (type))
Map_match
(vardecl
Map (fun [List [[Tuple2 k] v]] [[Map k] v])
)
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl PendingTxOutRef (type))
PendingTxOutRef_match
(vardecl
PendingTxOutRef
(fun (con bytestring) (fun (con integer) PendingTxOutRef))
)
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl PendingTxIn (type))
PendingTxIn_match
(vardecl
PendingTxIn
(fun PendingTxOutRef (fun [Maybe [[Tuple2 (con bytestring)] (con bytestring)]] (fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] PendingTxIn)))
)
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl PendingTxOut (type))
PendingTxOut_match
(vardecl
PendingTxOut
(fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] (fun [Maybe [[Tuple2 (con bytestring)] (con bytestring)]] (fun PendingTxOutType PendingTxOut)))
)
)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl PendingTx (type))
PendingTx_match
(vardecl
PendingTx
(fun [List PendingTxIn] (fun [List PendingTxOut] (fun (con integer) (fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] (fun PendingTxIn (fun [Interval (con integer)] (fun [List [[Tuple2 (con bytestring)] (con bytestring)]] (fun (con bytestring) PendingTx))))))))
)
)
)
(let
(nonrec)
(termbind
(vardecl
addInteger
(fun (con integer) (fun (con integer) (con integer)))
)
(builtin addInteger)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl MultiSig (type))
MultiSig_match
(vardecl
MultiSig
(fun [List (con bytestring)] (fun (con integer) MultiSig))
)
)
)
(let
(nonrec)
(termbind
(vardecl
charToString
(fun (con integer) (con string))
)
(builtin charToString)
)
(let
(nonrec)
(datatypebind
(datatype
(tyvardecl Bool (type))
Bool_match
(vardecl True Bool)
(vardecl False Bool)
)
)
(let
(nonrec)
(termbind
(vardecl
equalsByteString
(fun (con bytestring) (fun (con bytestring) Bool))
)
(lam
arg
(con bytestring)
(lam
arg
(con bytestring)
[
(lam
b
(all a (type) (fun a (fun a a)))
[
[ { b Bool } True ]
False
]
)
[
[
(builtin
equalsByteString
)
arg
]
arg
]
]
)
)
)
(let
(nonrec)
(termbind
(vardecl
greaterThanEqInteger
(fun (con integer) (fun (con integer) Bool))
)
(lam
arg
(con integer)
(lam
arg
(con integer)
[
(lam
b
(all a (type) (fun a (fun a a)))
[
[ { b Bool } True ]
False
]
)
[
[
(builtin
greaterThanEqualsInteger
)
arg
]
arg
]
]
)
)
)
(let
(nonrec)
(termbind
(vardecl
verifySignature
(fun (con bytestring) (fun (con bytestring) (fun (con bytestring) Bool)))
)
(lam
arg
(con bytestring)
(lam
arg
(con bytestring)
(lam
arg
(con bytestring)
[
(lam
b
(all a (type) (fun a (fun a a)))
[
[
{ b Bool } True
]
False
]
)
[
[
[
(builtin
verifySignature
)
arg
]
arg
]
arg
]
]
)
)
)
)
(let
(nonrec)
(termbind
(vardecl
validate
(fun MultiSig (fun Unit (fun Unit (fun PendingTx Unit))))
)
(lam
ds
MultiSig
(lam
ds
Unit
(lam
ds
Unit
(lam
p
PendingTx
[
{
[
MultiSig_match
ds
]
Unit
}
(lam
keys
[List (con bytestring)]
(lam
num
(con integer)
[
[
{
[
Unit_match
ds
]
(fun Unit Unit)
}
(lam
thunk
Unit
[
[
{
[
Unit_match
ds
]
(fun Unit Unit)
}
(lam
thunk
Unit
(let
(nonrec
)
(termbind
(vardecl
present
(con integer)
)
[
[
[
{
{
(let
(rec
)
(termbind
(vardecl
foldr
(all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))
)
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun a (fun b b))
(lam
acc
b
(lam
l
[List a]
[
[
{
[
{
Nil_match
a
}
l
]
b
}
acc
]
(lam
x
a
(lam
xs
[List a]
[
[
f
x
]
[
[
[
{
{
foldr
a
}
b
}
f
]
acc
]
xs
]
]
)
)
]
)
)
)
)
)
)
foldr
)
(con bytestring)
}
(con integer)
}
(lam
ds
(con bytestring)
(lam
acc
(con integer)
[
[
addInteger
acc
]
(con
1
)
]
)
)
]
(con
0
)
]
[
(let
(nonrec
)
(termbind
(vardecl
pred
(fun (con bytestring) Bool)
)
(lam
k
(con bytestring)
(let
(nonrec
)
(termbind
(vardecl
ds
PendingTx
)
p
)
(let
(nonrec
)
(termbind
(vardecl
sigs
[List [[Tuple2 (con bytestring)] (con bytestring)]]
)
[
{
[
PendingTx_match
ds
]
[List [[Tuple2 (con bytestring)] (con bytestring)]]
}
(lam
ds
[List PendingTxIn]
(lam
ds
[List PendingTxOut]
(lam
ds
(con integer)
(lam
ds
[[Map (con bytestring)] [[Map (con bytestring)] (con integer)]]
(lam
ds
PendingTxIn
(lam
ds
[Interval (con integer)]
(lam
sigs
[List [[Tuple2 (con bytestring)] (con bytestring)]]
(lam
hsh
(con bytestring)
sigs
)
)
)
)
)
)
)
)
]
)
(let
(nonrec
)
(termbind
(vardecl
hsh
(con bytestring)
)
[
{
[
PendingTx_match
ds
]
(con bytestring)
}
(lam
ds
[List PendingTxIn]
(lam
ds
[List PendingTxOut]
(lam
ds
(con integer)
(lam
ds
[[Map (con bytestring)] [[Map (con bytestring)] (con integer)]]
(lam
ds
PendingTxIn
(lam
ds
[Interval (con integer)]
(lam
sigs
[List [[Tuple2 (con bytestring)] (con bytestring)]]
(lam
hsh
(con bytestring)
hsh
)
)
)
)
)
)
)
)
]
)
(let
(nonrec
)
(termbind
(vardecl
signedBy
(fun (con bytestring) Bool)
)
(lam
ds
(con bytestring)
(let
(nonrec
)
(termbind
(vardecl
msg
(con bytestring)
)
(let
(nonrec
)
(termbind
(vardecl
ds
(con bytestring)
)
hsh
)
ds
)
)
(let
(nonrec
)
(termbind
(vardecl
pk
(con bytestring)
)
[
{
[
{
Unit_match
(con bytestring)
}
(let
(nonrec
)
(termbind
(vardecl
ds
(con bytestring)
)
k
)
[
{
Unit
(con bytestring)
}
ds
]
)
]
(con bytestring)
}
(lam
pk
(con bytestring)
pk
)
]
)
[
[
[
verifySignature
pk
]
msg
]
ds
]
)
)
)
)
(let
(rec
)
(termbind
(vardecl
go
(fun [List [[Tuple2 (con bytestring)] (con bytestring)]] Bool)
)
(lam
l
[List [[Tuple2 (con bytestring)] (con bytestring)]]
[
[
{
[
{
Nil_match
[[Tuple2 (con bytestring)] (con bytestring)]
}
l
]
Bool
}
False
]
(lam
ds
[[Tuple2 (con bytestring)] (con bytestring)]
(lam
r
[List [[Tuple2 (con bytestring)] (con bytestring)]]
[
{
[
{
{
Tuple2_match
(con bytestring)
}
(con bytestring)
}
ds
]
Bool
}
(lam
pk
(con bytestring)
(lam
sig
(con bytestring)
[
[
[
{
[
Bool_match
[
(lam
ds
(con bytestring)
[
[
equalsByteString
k
]
ds
]
)
pk
]
]
(fun Unit Bool)
}
(lam
thunk
Unit
[
[
[
{
[
Bool_match
[
signedBy
sig
]
]
(fun Unit Bool)
}
(lam
thunk
Unit
True
)
]
(lam
thunk
Unit
[
(let
(nonrec
)
(termbind
(vardecl
str
[List (con integer)]
)
[
[
{
Cons
(con integer)
}
(con
109
)
]
[
[
{
Cons
(con integer)
}
(con
97
)
]
[
[
{
Cons
(con integer)
}
(con
116
)
]
[
[
{
Cons
(con integer)
}
(con
99
)
]
[
[
{
Cons
(con integer)
}
(con
104
)
]
[
[
{
Cons
(con integer)
}
(con
105
)
]
[
[
{
Cons
(con integer)
}
(con
110
)
]
[
[
{
Cons
(con integer)
}
(con
103
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
112
)
]
[
[
{
Cons
(con integer)
}
(con
117
)
]
[
[
{
Cons
(con integer)
}
(con
98
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
107
)
]
[
[
{
Cons
(con integer)
}
(con
101
)
]
[
[
{
Cons
(con integer)
}
(con
121
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
119
)
]
[
[
{
Cons
(con integer)
}
(con
105
)
]
[
[
{
Cons
(con integer)
}
(con
116
)
]
[
[
{
Cons
(con integer)
}
(con
104
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
105
)
]
[
[
{
Cons
(con integer)
}
(con
110
)
]
[
[
{
Cons
(con integer)
}
(con
118
)
]
[
[
{
Cons
(con integer)
}
(con
97
)
]
[
[
{
Cons
(con integer)
}
(con
108
)
]
[
[
{
Cons
(con integer)
}
(con
105
)
]
[
[
{
Cons
(con integer)
}
(con
100
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
115
)
]
[
[
{
Cons
(con integer)
}
(con
105
)
]
[
[
{
Cons
(con integer)
}
(con
103
)
]
[
[
{
Cons
(con integer)
}
(con
110
)
]
[
[
{
Cons
(con integer)
}
(con
97
)
]
[
[
{
Cons
(con integer)
}
(con
116
)
]
[
[
{
Cons
(con integer)
}
(con
117
)
]
[
[
{
Cons
(con integer)
}
(con
114
)
]
[
[
{
Cons
(con integer)
}
(con
101
)
]
{
Nil
(con integer)
}
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
]
)
(lam
a
Bool
[
(let
(nonrec
)
(termbind
(vardecl
str
(con string)
)
[
(let
(nonrec
)
(termbind
(vardecl
f
(fun [List (con integer)] (con string))
)
(let
(rec
)
(termbind
(vardecl
f
(fun [List (con integer)] (con string))
)
(lam
str
[List (con integer)]
[
[
{
[
{
Nil_match
(con integer)
}
str
]
(con string)
}
emptyString
]
(lam
c
(con integer)
(lam
rest
[List (con integer)]
[
[
appendString
[
charToString
c
]
]
[
f
rest
]
]
)
)
]
)
)
f
)
)
f
)
str
]
)
(lam
a
Bool
[
{
[
Unit_match
[
trace
str
]
]
Bool
}
a
]
)
)
a
]
)
)
[
go
r
]
]
)
]
Unit
]
)
]
(lam
thunk
Unit
[
go
r
]
)
]
Unit
]
)
)
]
)
)
]
)
)
[
go
sigs
]
)
)
)
)
)
)
)
[
[
{
{
(let
(rec
)
(termbind
(vardecl
foldr
(all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))
)
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun a (fun b b))
(lam
acc
b
(lam
l
[List a]
[
[
{
[
{
Nil_match
a
}
l
]
b
}
acc
]
(lam
x
a
(lam
xs
[List a]
[
[
f
x
]
[
[
[
{
{
foldr
a
}
b
}
f
]
acc
]
xs
]
]
)
)
]
)
)
)
)
)
)
foldr
)
(con bytestring)
}
[List (con bytestring)]
}
(lam
e
(con bytestring)
(lam
xs
[List (con bytestring)]
[
[
[
{
[
Bool_match
[
pred
e
]
]
(fun Unit [List (con bytestring)])
}
(lam
thunk
Unit
[
[
{
Cons
(con bytestring)
}
e
]
xs
]
)
]
(lam
thunk
Unit
xs
)
]
Unit
]
)
)
]
{
Nil
(con bytestring)
}
]
)
keys
]
]
)
[
[
[
{
[
Bool_match
[
[
greaterThanEqInteger
present
]
num
]
]
(fun Unit Unit)
}
(lam
thunk
Unit
Unit
)
]
(lam
thunk
Unit
[
{
error
Unit
}
[
(let
(nonrec
)
(termbind
(vardecl
str
[List (con integer)]
)
[
[
{
Cons
(con integer)
}
(con
87
)
]
[
[
{
Cons
(con integer)
}
(con
82
)
]
[
[
{
Cons
(con integer)
}
(con
79
)
]
[
[
{
Cons
(con integer)
}
(con
78
)
]
[
[
{
Cons
(con integer)
}
(con
71
)
]
[
[
{
Cons
(con integer)
}
(con
33
)
]
{
Nil
(con integer)
}
]
]
]
]
]
]
)
(lam
a
Unit
[
(let
(nonrec
)
(termbind
(vardecl
str
(con string)
)
[
(let
(nonrec
)
(termbind
(vardecl
f
(fun [List (con integer)] (con string))
)
(let
(rec
)
(termbind
(vardecl
f
(fun [List (con integer)] (con string))
)
(lam
str
[List (con integer)]
[
[
{
[
{
Nil_match
(con integer)
}
str
]
(con string)
}
emptyString
]
(lam
c
(con integer)
(lam
rest
[List (con integer)]
[
[
appendString
[
charToString
c
]
]
[
f
rest
]
]
)
)
]
)
)
f
)
)
f
)
str
]
)
(lam
a
Unit
[
{
[
Unit_match
[
trace
str
]
]
Unit
}
a
]
)
)
a
]
)
)
Unit
]
]
)
]
Unit
]
)
)
]
Unit
]
)
]
Unit
]
)
)
]
)
)
)
)
)
validate
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Raw
Multisig.plc
This file has been truncated, but you can view the full file.
(program 1.0.0
[
[
(lam
emptyString
(con string)
[
(lam
appendString
(fun (con string) (fun (con string) (con string)))
[
[
[
{
(abs
PendingTxOutType
(type)
(lam
DataTxOut
PendingTxOutType
(lam
PubKeyTxOut
(fun (con bytestring) PendingTxOutType)
(lam
PendingTxOutType_match
(fun PendingTxOutType (all out_PendingTxOutType (type) (fun out_PendingTxOutType (fun (fun (con bytestring) out_PendingTxOutType) out_PendingTxOutType))))
[
[
{
(abs
Tuple2
(fun (type) (fun (type) (type)))
(lam
Tuple2
(all a (type) (all b (type) (fun a (fun b [[Tuple2 a] b]))))
(lam
Tuple2_match
(all a (type) (all b (type) (fun [[Tuple2 a] b] (all out_Tuple2 (type) (fun (fun a (fun b out_Tuple2)) out_Tuple2)))))
[
[
{
(abs
Unit
(fun (type) (type))
(lam
Unit
(all a (type) (fun a [Unit a]))
(lam
Unit_match
(all a (type) (fun [Unit a] (all out_Unit (type) (fun (fun a out_Unit) out_Unit))))
[
[
{
(abs
Unit
(type)
(lam
Unit
Unit
(lam
Unit_match
(fun Unit (all out_Unit (type) (fun out_Unit out_Unit)))
[
(lam
trace
(fun (con string) Unit)
[
(lam
error
(all a (type) (fun Unit a))
[
[
[
{
(abs
Maybe
(fun (type) (type))
(lam
Just
(all a (type) (fun a [Maybe a]))
(lam
Nothing
(all a (type) [Maybe a])
(lam
Maybe_match
(all a (type) (fun [Maybe a] (all out_Maybe (type) (fun (fun a out_Maybe) (fun out_Maybe out_Maybe)))))
[
[
{
(abs
Interval
(fun (type) (type))
(lam
Interval
(all a (type) (fun [Maybe a] (fun [Maybe a] [Interval a])))
(lam
Interval_match
(all a (type) (fun [Interval a] (all out_Interval (type) (fun (fun [Maybe a] (fun [Maybe a] out_Interval)) out_Interval))))
[
[
[
{
(abs
List
(fun (type) (type))
(lam
Nil
(all a (type) [List a])
(lam
Cons
(all a (type) (fun a (fun [List a] [List a])))
(lam
Nil_match
(all a (type) (fun [List a] (all out_List (type) (fun out_List (fun (fun a (fun [List a] out_List)) out_List)))))
[
[
{
(abs
Map
(fun (type) (fun (type) (type)))
(lam
Map
(all k (type) (all v (type) (fun [List [[Tuple2 k] v]] [[Map k] v])))
(lam
Map_match
(all k (type) (all v (type) (fun [[Map k] v] (all out_Map (type) (fun (fun [List [[Tuple2 k] v]] out_Map) out_Map)))))
[
[
{
(abs
PendingTxOutRef
(type)
(lam
PendingTxOutRef
(fun (con bytestring) (fun (con integer) PendingTxOutRef))
(lam
PendingTxOutRef_match
(fun PendingTxOutRef (all out_PendingTxOutRef (type) (fun (fun (con bytestring) (fun (con integer) out_PendingTxOutRef)) out_PendingTxOutRef)))
[
[
{
(abs
PendingTxIn
(type)
(lam
PendingTxIn
(fun PendingTxOutRef (fun [Maybe [[Tuple2 (con bytestring)] (con bytestring)]] (fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] PendingTxIn)))
(lam
PendingTxIn_match
(fun PendingTxIn (all out_PendingTxIn (type) (fun (fun PendingTxOutRef (fun [Maybe [[Tuple2 (con bytestring)] (con bytestring)]] (fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] out_PendingTxIn))) out_PendingTxIn)))
[
[
{
(abs
PendingTxOut
(type)
(lam
PendingTxOut
(fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] (fun [Maybe [[Tuple2 (con bytestring)] (con bytestring)]] (fun PendingTxOutType PendingTxOut)))
(lam
PendingTxOut_match
(fun PendingTxOut (all out_PendingTxOut (type) (fun (fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] (fun [Maybe [[Tuple2 (con bytestring)] (con bytestring)]] (fun PendingTxOutType out_PendingTxOut))) out_PendingTxOut)))
[
[
{
(abs
PendingTx
(type)
(lam
PendingTx
(fun [List PendingTxIn] (fun [List PendingTxOut] (fun (con integer) (fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] (fun PendingTxIn (fun [Interval (con integer)] (fun [List [[Tuple2 (con bytestring)] (con bytestring)]] (fun (con bytestring) PendingTx))))))))
(lam
PendingTx_match
(fun PendingTx (all out_PendingTx (type) (fun (fun [List PendingTxIn] (fun [List PendingTxOut] (fun (con integer) (fun [[Map (con bytestring)] [[Map (con bytestring)] (con integer)]] (fun PendingTxIn (fun [Interval (con integer)] (fun [List [[Tuple2 (con bytestring)] (con bytestring)]] (fun (con bytestring) out_PendingTx)))))))) out_PendingTx)))
[
(lam
addInteger
(fun (con integer) (fun (con integer) (con integer)))
[
[
{
(abs
MultiSig
(type)
(lam
MultiSig
(fun [List (con bytestring)] (fun (con integer) MultiSig))
(lam
MultiSig_match
(fun MultiSig (all out_MultiSig (type) (fun (fun [List (con bytestring)] (fun (con integer) out_MultiSig)) out_MultiSig)))
[
(lam
charToString
(fun (con integer) (con string))
[
[
[
{
(abs
Bool
(type)
(lam
True
Bool
(lam
False
Bool
(lam
Bool_match
(fun Bool (all out_Bool (type) (fun out_Bool (fun out_Bool out_Bool))))
[
(lam
equalsByteString
(fun (con bytestring) (fun (con bytestring) Bool))
[
(lam
greaterThanEqInteger
(fun (con integer) (fun (con integer) Bool))
[
(lam
verifySignature
(fun (con bytestring) (fun (con bytestring) (fun (con bytestring) Bool)))
[
(lam
validate
(fun MultiSig (fun Unit (fun Unit (fun PendingTx Unit))))
validate
)
(lam
ds
MultiSig
(lam
ds
Unit
(lam
ds
Unit
(lam
p
PendingTx
[
{
[
MultiSig_match
ds
]
Unit
}
(lam
keys
[List (con bytestring)]
(lam
num
(con integer)
[
[
{
[
Unit_match
ds
]
(fun Unit Unit)
}
(lam
thunk
Unit
[
[
{
[
Unit_match
ds
]
(fun Unit Unit)
}
(lam
thunk
Unit
[
(lam
present
(con integer)
[
[
[
{
[
Bool_match
[
[
greaterThanEqInteger
present
]
num
]
]
(fun Unit Unit)
}
(lam
thunk
Unit
Unit
)
]
(lam
thunk
Unit
[
{
error
Unit
}
[
[
(lam
str
[List (con integer)]
(lam
a
Unit
[
[
(lam
str
(con string)
(lam
a
Unit
[
{
[
Unit_match
[
trace
str
]
]
Unit
}
a
]
)
)
[
[
(lam
f
(fun [List (con integer)] (con string))
f
)
[
(lam
tup
(all r (type) (fun (fun (fun [List (con integer)] (con string)) r) r))
[
(lam
f
(fun [List (con integer)] (con string))
f
)
[
{
tup
(fun [List (con integer)] (con string))
}
(lam
arg_0
(fun [List (con integer)] (con string))
arg_0
)
]
]
)
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(all Q (type) (fun (fun (fun a b) Q) (fun (fun a b) Q)))
[
[
{
(abs
F
(fun (type) (type))
(lam
by
(fun (all Q (type) (fun [F Q] Q)) (all Q (type) (fun [F Q] Q)))
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun (fun a b) (fun a b))
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
(iwrap
(lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]]))
(lam dat (fun (type) (type)) [dat (fun a b)])
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) (fun a b)]
(lam
x
a
[
[
f
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
s
]
]
x
]
)
)
)
]
)
)
)
(all Q (type) (fun [F Q] [F Q]))
}
(all Q (type) (fun [F Q] Q))
}
(lam
rec
(fun (all Q (type) (fun [F Q] [F Q])) (all Q (type) (fun [F Q] Q)))
(lam
h
(all Q (type) (fun [F Q] [F Q]))
(abs
R
(type)
(lam
fr
[F R]
[
{
[
by
(abs
Q
(type)
(lam
fq
[F Q]
[
{
[
rec
h
]
Q
}
[
{
h
Q
}
fq
]
]
)
)
]
R
}
fr
]
)
)
)
)
]
)
)
(lam X (type) (fun (fun a b) X))
}
(lam
k
(all Q (type) (fun (fun (fun a b) Q) Q))
(abs
S
(type)
(lam
h
(fun (fun a b) S)
[
h
(lam
x
a
[
{
k
b
}
(lam
f_0
(fun a b)
[
f_0
x
]
)
]
)
]
)
)
)
]
f
]
)
)
)
[List (con integer)]
}
(con string)
}
(abs
Q
(type)
(lam
choose
(fun (fun [List (con integer)] (con string)) Q)
(lam
f
(fun [List (con integer)] (con string))
[
choose
(lam
str
[List (con integer)]
[
[
{
[
{
Nil_match
(con integer)
}
str
]
(con string)
}
emptyString
]
(lam
c
(con integer)
(lam
rest
[List (con integer)]
[
[
appendString
[
charToString
c
]
]
[
f
rest
]
]
)
)
]
)
]
)
)
)
]
]
]
str
]
]
a
]
)
)
[
[
{
Cons
(con integer)
}
(con
87
)
]
[
[
{
Cons
(con integer)
}
(con
82
)
]
[
[
{
Cons
(con integer)
}
(con
79
)
]
[
[
{
Cons
(con integer)
}
(con
78
)
]
[
[
{
Cons
(con integer)
}
(con
71
)
]
[
[
{
Cons
(con integer)
}
(con
33
)
]
{
Nil
(con integer)
}
]
]
]
]
]
]
]
Unit
]
]
)
]
Unit
]
)
[
[
[
{
{
[
(lam
tup
(all r (type) (fun (fun (fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))) r) r))
[
(lam
foldr_thunked
(fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b))))))
[
(lam
foldr
(all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))
foldr
)
[
foldr_thunked
(abs
a
(type)
(lam
x
a
x
)
)
]
]
)
[
{
tup
(fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b))))))
}
(lam
arg_0
(fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b))))))
arg_0
)
]
]
)
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(all Q (type) (fun (fun (fun a b) Q) (fun (fun a b) Q)))
[
[
{
(abs
F
(fun (type) (type))
(lam
by
(fun (all Q (type) (fun [F Q] Q)) (all Q (type) (fun [F Q] Q)))
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun (fun a b) (fun a b))
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
(iwrap
(lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]]))
(lam dat (fun (type) (type)) [dat (fun a b)])
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) (fun a b)]
(lam
x
a
[
[
f
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
s
]
]
x
]
)
)
)
]
)
)
)
(all Q (type) (fun [F Q] [F Q]))
}
(all Q (type) (fun [F Q] Q))
}
(lam
rec
(fun (all Q (type) (fun [F Q] [F Q])) (all Q (type) (fun [F Q] Q)))
(lam
h
(all Q (type) (fun [F Q] [F Q]))
(abs
R
(type)
(lam
fr
[F R]
[
{
[
by
(abs
Q
(type)
(lam
fq
[F Q]
[
{
[
rec
h
]
Q
}
[
{
h
Q
}
fq
]
]
)
)
]
R
}
fr
]
)
)
)
)
]
)
)
(lam X (type) (fun (fun a b) X))
}
(lam
k
(all Q (type) (fun (fun (fun a b) Q) Q))
(abs
S
(type)
(lam
h
(fun (fun a b) S)
[
h
(lam
x
a
[
{
k
b
}
(lam
f_0
(fun a b)
[
f_0
x
]
)
]
)
]
)
)
)
]
f
]
)
)
)
(all a (type) (fun a a))
}
(all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))
}
(abs
Q
(type)
(lam
choose
(fun (fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))) Q)
(lam
foldr_thunked
(fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b))))))
[
choose
(lam
arg
(all a (type) (fun a a))
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun a (fun b b))
(lam
acc
b
(lam
l
[List a]
[
[
{
[
{
Nil_match
a
}
l
]
b
}
acc
]
(lam
x
a
(lam
xs
[List a]
[
[
f
x
]
[
[
[
{
{
[
foldr_thunked
(abs
a
(type)
(lam
x
a
x
)
)
]
a
}
b
}
f
]
acc
]
xs
]
]
)
)
]
)
)
)
)
)
)
]
)
)
)
]
]
(con bytestring)
}
(con integer)
}
(lam
ds
(con bytestring)
(lam
acc
(con integer)
[
[
addInteger
acc
]
(con
1
)
]
)
)
]
(con
0
)
]
[
[
(lam
pred
(fun (con bytestring) Bool)
[
[
{
{
[
(lam
tup
(all r (type) (fun (fun (fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))) r) r))
[
(lam
foldr_thunked
(fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b))))))
[
(lam
foldr
(all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))
foldr
)
[
foldr_thunked
(abs
a
(type)
(lam
x
a
x
)
)
]
]
)
[
{
tup
(fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b))))))
}
(lam
arg_0
(fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b))))))
arg_0
)
]
]
)
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(all Q (type) (fun (fun (fun a b) Q) (fun (fun a b) Q)))
[
[
{
(abs
F
(fun (type) (type))
(lam
by
(fun (all Q (type) (fun [F Q] Q)) (all Q (type) (fun [F Q] Q)))
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun (fun a b) (fun a b))
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
(iwrap
(lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]]))
(lam dat (fun (type) (type)) [dat (fun a b)])
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) (fun a b)]
(lam
x
a
[
[
f
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
s
]
]
x
]
)
)
)
]
)
)
)
(all Q (type) (fun [F Q] [F Q]))
}
(all Q (type) (fun [F Q] Q))
}
(lam
rec
(fun (all Q (type) (fun [F Q] [F Q])) (all Q (type) (fun [F Q] Q)))
(lam
h
(all Q (type) (fun [F Q] [F Q]))
(abs
R
(type)
(lam
fr
[F R]
[
{
[
by
(abs
Q
(type)
(lam
fq
[F Q]
[
{
[
rec
h
]
Q
}
[
{
h
Q
}
fq
]
]
)
)
]
R
}
fr
]
)
)
)
)
]
)
)
(lam X (type) (fun (fun a b) X))
}
(lam
k
(all Q (type) (fun (fun (fun a b) Q) Q))
(abs
S
(type)
(lam
h
(fun (fun a b) S)
[
h
(lam
x
a
[
{
k
b
}
(lam
f_0
(fun a b)
[
f_0
x
]
)
]
)
]
)
)
)
]
f
]
)
)
)
(all a (type) (fun a a))
}
(all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))
}
(abs
Q
(type)
(lam
choose
(fun (fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b)))))) Q)
(lam
foldr_thunked
(fun (all a (type) (fun a a)) (all a (type) (all b (type) (fun (fun a (fun b b)) (fun b (fun [List a] b))))))
[
choose
(lam
arg
(all a (type) (fun a a))
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun a (fun b b))
(lam
acc
b
(lam
l
[List a]
[
[
{
[
{
Nil_match
a
}
l
]
b
}
acc
]
(lam
x
a
(lam
xs
[List a]
[
[
f
x
]
[
[
[
{
{
[
foldr_thunked
(abs
a
(type)
(lam
x
a
x
)
)
]
a
}
b
}
f
]
acc
]
xs
]
]
)
)
]
)
)
)
)
)
)
]
)
)
)
]
]
(con bytestring)
}
[List (con bytestring)]
}
(lam
e
(con bytestring)
(lam
xs
[List (con bytestring)]
[
[
[
{
[
Bool_match
[
pred
e
]
]
(fun Unit [List (con bytestring)])
}
(lam
thunk
Unit
[
[
{
Cons
(con bytestring)
}
e
]
xs
]
)
]
(lam
thunk
Unit
xs
)
]
Unit
]
)
)
]
{
Nil
(con bytestring)
}
]
)
(lam
k
(con bytestring)
[
(lam
ds
PendingTx
[
(lam
sigs
[List [[Tuple2 (con bytestring)] (con bytestring)]]
[
(lam
hsh
(con bytestring)
[
(lam
signedBy
(fun (con bytestring) Bool)
[
(lam
tup
(all r (type) (fun (fun (fun [List [[Tuple2 (con bytestring)] (con bytestring)]] Bool) r) r))
[
(lam
go
(fun [List [[Tuple2 (con bytestring)] (con bytestring)]] Bool)
[
go
sigs
]
)
[
{
tup
(fun [List [[Tuple2 (con bytestring)] (con bytestring)]] Bool)
}
(lam
arg_0
(fun [List [[Tuple2 (con bytestring)] (con bytestring)]] Bool)
arg_0
)
]
]
)
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(all Q (type) (fun (fun (fun a b) Q) (fun (fun a b) Q)))
[
[
{
(abs
F
(fun (type) (type))
(lam
by
(fun (all Q (type) (fun [F Q] Q)) (all Q (type) (fun [F Q] Q)))
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun (fun a b) (fun a b))
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
(iwrap
(lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]]))
(lam dat (fun (type) (type)) [dat (fun a b)])
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) (fun a b)]
(lam
x
a
[
[
f
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
s
]
]
x
]
)
)
)
]
)
)
)
(all Q (type) (fun [F Q] [F Q]))
}
(all Q (type) (fun [F Q] Q))
}
(lam
rec
(fun (all Q (type) (fun [F Q] [F Q])) (all Q (type) (fun [F Q] Q)))
(lam
h
(all Q (type) (fun [F Q] [F Q]))
(abs
R
(type)
(lam
fr
[F R]
[
{
[
by
(abs
Q
(type)
(lam
fq
[F Q]
[
{
[
rec
h
]
Q
}
[
{
h
Q
}
fq
]
]
)
)
]
R
}
fr
]
)
)
)
)
]
)
)
(lam X (type) (fun (fun a b) X))
}
(lam
k
(all Q (type) (fun (fun (fun a b) Q) Q))
(abs
S
(type)
(lam
h
(fun (fun a b) S)
[
h
(lam
x
a
[
{
k
b
}
(lam
f_0
(fun a b)
[
f_0
x
]
)
]
)
]
)
)
)
]
f
]
)
)
)
[List [[Tuple2 (con bytestring)] (con bytestring)]]
}
Bool
}
(abs
Q
(type)
(lam
choose
(fun (fun [List [[Tuple2 (con bytestring)] (con bytestring)]] Bool) Q)
(lam
go
(fun [List [[Tuple2 (con bytestring)] (con bytestring)]] Bool)
[
choose
(lam
l
[List [[Tuple2 (con bytestring)] (con bytestring)]]
[
[
{
[
{
Nil_match
[[Tuple2 (con bytestring)] (con bytestring)]
}
l
]
Bool
}
False
]
(lam
ds
[[Tuple2 (con bytestring)] (con bytestring)]
(lam
r
[List [[Tuple2 (con bytestring)] (con bytestring)]]
[
{
[
{
{
Tuple2_match
(con bytestring)
}
(con bytestring)
}
ds
]
Bool
}
(lam
pk
(con bytestring)
(lam
sig
(con bytestring)
[
[
[
{
[
Bool_match
[
(lam
ds
(con bytestring)
[
[
equalsByteString
k
]
ds
]
)
pk
]
]
(fun Unit Bool)
}
(lam
thunk
Unit
[
[
[
{
[
Bool_match
[
signedBy
sig
]
]
(fun Unit Bool)
}
(lam
thunk
Unit
True
)
]
(lam
thunk
Unit
[
[
(lam
str
[List (con integer)]
(lam
a
Bool
[
[
(lam
str
(con string)
(lam
a
Bool
[
{
[
Unit_match
[
trace
str
]
]
Bool
}
a
]
)
)
[
[
(lam
f
(fun [List (con integer)] (con string))
f
)
[
(lam
tup
(all r (type) (fun (fun (fun [List (con integer)] (con string)) r) r))
[
(lam
f
(fun [List (con integer)] (con string))
f
)
[
{
tup
(fun [List (con integer)] (con string))
}
(lam
arg_0
(fun [List (con integer)] (con string))
arg_0
)
]
]
)
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(all Q (type) (fun (fun (fun a b) Q) (fun (fun a b) Q)))
[
[
{
(abs
F
(fun (type) (type))
(lam
by
(fun (all Q (type) (fun [F Q] Q)) (all Q (type) (fun [F Q] Q)))
[
{
{
(abs
a
(type)
(abs
b
(type)
(lam
f
(fun (fun a b) (fun a b))
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
(iwrap
(lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]]))
(lam dat (fun (type) (type)) [dat (fun a b)])
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) (fun a b)]
(lam
x
a
[
[
f
[
{
(abs
a
(type)
(lam
s
[(lam a (type) (ifix (lam rec (fun (fun (fun (type) (type)) (type)) (type)) (lam spine (fun (fun (type) (type)) (type)) [spine [(lam self (fun (type) (type)) (lam a (type) (fun [self a] a))) (lam a (type) [rec (lam dat (fun (type) (type)) [dat a])])]])) (lam dat (fun (type) (type)) [dat a]))) a]
[
(unwrap
s
)
s
]
)
)
(fun a b)
}
s
]
]
x
]
)
)
)
]
)
)
)
(all Q (type) (fun [F Q] [F Q]))
}
(all Q (type) (fun [F Q] Q))
}
(lam
rec
(fun (all Q (type) (fun [F Q] [F Q])) (all Q (type) (fun [F Q] Q)))
(lam
h
(all Q (type) (fun [F Q] [F Q]))
(abs
R
(type)
(lam
fr
[F R]
[
{
[
by
(abs
Q
(type)
(lam
fq
[F Q]
[
{
[
rec
h
]
Q
}
[
{
h
Q
}
fq
]
]
)
)
]
R
}
fr
]
)
)
)
)
]
)
)
(lam X (type) (fun (fun a b) X))
}
(lam
k
(all Q (type) (fun (fun (fun a b) Q) Q))
(abs
S
(type)
(lam
h
(fun (fun a b) S)
[
h
(lam
x
a
[
{
k
b
}
(lam
f_0
(fun a b)
[
f_0
x
]
)
]
)
]
)
)
)
]
f
]
)
)
)
[List (con integer)]
}
(con string)
}
(abs
Q
(type)
(lam
choose
(fun (fun [List (con integer)] (con string)) Q)
(lam
f
(fun [List (con integer)] (con string))
[
choose
(lam
str
[List (con integer)]
[
[
{
[
{
Nil_match
(con integer)
}
str
]
(con string)
}
emptyString
]
(lam
c
(con integer)
(lam
rest
[List (con integer)]
[
[
appendString
[
charToString
c
]
]
[
f
rest
]
]
)
)
]
)
]
)
)
)
]
]
]
str
]
]
a
]
)
)
[
[
{
Cons
(con integer)
}
(con
109
)
]
[
[
{
Cons
(con integer)
}
(con
97
)
]
[
[
{
Cons
(con integer)
}
(con
116
)
]
[
[
{
Cons
(con integer)
}
(con
99
)
]
[
[
{
Cons
(con integer)
}
(con
104
)
]
[
[
{
Cons
(con integer)
}
(con
105
)
]
[
[
{
Cons
(con integer)
}
(con
110
)
]
[
[
{
Cons
(con integer)
}
(con
103
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
112
)
]
[
[
{
Cons
(con integer)
}
(con
117
)
]
[
[
{
Cons
(con integer)
}
(con
98
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
107
)
]
[
[
{
Cons
(con integer)
}
(con
101
)
]
[
[
{
Cons
(con integer)
}
(con
121
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
119
)
]
[
[
{
Cons
(con integer)
}
(con
105
)
]
[
[
{
Cons
(con integer)
}
(con
116
)
]
[
[
{
Cons
(con integer)
}
(con
104
)
]
[
[
{
Cons
(con integer)
}
(con
32
)
]
[
[
{
Cons
(con integer)
}
(con
105
)
]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment