James Eversole
c9d0d04630
To encourage organizing code in a way that helps in understanding, I have implemented the common idiom of requiring a `main` function. In tricu and other functional languages, it is usually placed near the top of the module. The evaluator gracefully handles the situation of passing multiple files where the intermediary "library" files do not have main functions.
38 lines
1.3 KiB
Plaintext
38 lines
1.3 KiB
Plaintext
main = lambdaEqualsTC
|
|
|
|
-- 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?
|