James Eversole
bf1000d174
Don't require/allow naming a module, instead require that the importer names it. Allow importing into the local scope with the name !Local. Simplify namespacing logic. Updates all tests to reflect these changes.
40 lines
1.3 KiB
Plaintext
40 lines
1.3 KiB
Plaintext
!import "lib/base.tri" !Local
|
|
|
|
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?
|