!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?