!import "../lib/Base.tri" !Local
!import "../lib/List.tri" !Local

main = toSource not?
-- Thanks to intensionality, we can inspect the structure of a given value
-- even if it's a function. This includes lambdas which are eliminated to
-- Tree Calculus (TC) terms during evaluation.

-- `triage` takes four arguments: the first three represent behaviors for each 
-- structural case in Tree Calculus (Leaf, Stem, and Fork).
-- The fourth argument is the value whose structure is inspected. By evaluating 
-- the Tree Calculus term, `triage` enables branching logic based on the term's 
-- shape, making it possible to perform structure-specific operations such as
-- reconstructing the terms' source code representation.
-- triage = (\leaf stem fork : t (t leaf stem) fork)

-- Base case of a single Leaf
sourceLeaf = t (head "t")

-- Stem case
sourceStem = convert : (a rest :
  t (head "(")                       -- Start with a left parenthesis "(".
    (t (head "t")                    -- Add a "t"
      (t (head " ")                  -- Add a space.
        (convert a                   -- Recursively convert the argument.
          (t (head ")") rest)))))   -- Close with ")" and append the rest.

-- Fork case
sourceFork = convert : (a b rest :
  t (head "(")                           -- Start with a left parenthesis "(".
    (t (head "t")                        -- Add a "t"
      (t (head " ")                      -- Add a space.
        (convert a                       -- Recursively convert the first arg.
          (t (head " ")                  -- Add another space.
            (convert b                   -- Recursively convert the second arg.
              (t (head ")") rest))))))) -- Close with ")" and append the rest.

-- Wrapper around triage 
toSource_ = y (self arg :
  triage
    sourceLeaf        -- `triage` "a" case, Leaf
    (sourceStem self) -- `triage` "b" case, Stem
    (sourceFork self) -- `triage` "c" case, Fork
    arg)              -- The term to be inspected

-- toSource takes a single TC term and returns a String
toSource = v : toSource_ v ""

exampleOne = toSource true -- OUT: "(t t)"
exampleTwo = toSource not? -- OUT: "(t (t (t t) (t t t)) (t t (t t t)))"