tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

equality.tri (1175B)

      1 !import prelude *
      2 !import io *
      3 !import consumers_source_worker as Source
      4 !import consumers_lexical_worker as L
      5 !export *
      6 -- Run from the repository root with --io --allow-read demos/consumers/lessons.
      7 
      8 -- Both are identity on all reduced trees. One returns its argument;
      9 -- the other inspects its shape and reconstructs the same tree. They are
     10 -- extensionally equal but not the same executable tree.
     11 idPlain = x : x
     12 idByShape = x : (triage t (child : t child)
     13   (left right : t left right) x)
     14 
     15 load = Source.loadSource "demos/consumers/lessons/equality/structural-equality.scp" t
     16 showComparison worker label left right = (putStrLn (append label
     17   (matchResult
     18     (problem _ : append "ERROR: " problem)
     19     (same _ : matchBool "same" "different" same)
     20     (L.lRunChecked worker (pair left right)))))
     21 run = onOk_ load (worker : thenIO
     22   (showComparison worker "same representation: " idPlain idPlain)
     23   (thenIO
     24     (showComparison worker "two identities: " idPlain idByShape)
     25     (thenIO
     26       (showComparison worker "result on Leaf: " (idPlain t) (idByShape t))
     27       (showComparison worker "result on Fork: "
     28         (idPlain (t t t)) (idByShape (t t t))))))
     29 main = io run