36 lines
1.2 KiB
Plaintext
36 lines
1.2 KiB
Plaintext
-- We represent `false` with a Leaf and `true` with a Stem Leaf
|
|
demo_false = t
|
|
demo_true = t t
|
|
|
|
-- Tree Calculus representation of the Boolean `not` function
|
|
not_TC? = t (t (t t) (t t t)) (t t (t t t))
|
|
|
|
-- /demos/toSource.tri contains an explanation of `triage`
|
|
demo_triage = \a b c : t (t a b) c
|
|
demo_matchBool = (\ot of : demo_triage
|
|
of
|
|
(\_ : ot)
|
|
(\_ _ : ot)
|
|
)
|
|
-- Lambda representation of the Boolean `not` function
|
|
not_Lambda? = demo_matchBool demo_false demo_true
|
|
|
|
-- Since tricu eliminates Lambda terms to SKI combinators, the tree form of many
|
|
-- functions defined via Lambda terms are larger than the most efficient TC
|
|
-- representation. Between different languages that evaluate to tree calculus
|
|
-- terms, the exact implementation of Lambda elimination may differ and lead
|
|
-- to different tree representations even if they share extensional behavior.
|
|
|
|
-- Let's see if these are the same:
|
|
lambdaEqualsTC = equal? not_TC? not_Lambda?
|
|
|
|
-- Here are some checks to verify their extensional behavior is the same:
|
|
true_TC? = not_TC? demo_false
|
|
false_TC? = not_TC? demo_true
|
|
|
|
true_Lambda? = not_Lambda? demo_false
|
|
false_Lambda? = not_Lambda? demo_true
|
|
|
|
bothTrueEqual? = equal? true_TC? true_Lambda?
|
|
bothFalseEqual? = equal? false_TC? false_Lambda?
|