# Modules
Basic implementation of a module system including tests.
This commit is contained in:
@ -1,3 +1,7 @@
|
||||
!module Equality
|
||||
|
||||
!import "lib/base.tri" Lib
|
||||
|
||||
main = lambdaEqualsTC
|
||||
|
||||
-- We represent `false` with a Leaf and `true` with a Stem Leaf
|
||||
@ -24,7 +28,7 @@ not_Lambda? = demo_matchBool demo_false demo_true
|
||||
-- to different tree representations even if they share extensional behavior.
|
||||
|
||||
-- Let's see if these are the same:
|
||||
lambdaEqualsTC = equal? not_TC? not_Lambda?
|
||||
lambdaEqualsTC = Lib.equal? not_TC? not_Lambda?
|
||||
|
||||
-- Here are some checks to verify their extensional behavior is the same:
|
||||
true_TC? = not_TC? demo_false
|
||||
@ -33,5 +37,5 @@ 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?
|
||||
bothTrueEqual? = Lib.equal? true_TC? true_Lambda?
|
||||
bothFalseEqual? = Lib.equal? false_TC? false_Lambda?
|
||||
|
@ -1,3 +1,7 @@
|
||||
!module LOT
|
||||
|
||||
!import "lib/base.tri" Lib
|
||||
|
||||
main = exampleTwo
|
||||
-- Level Order Traversal of a labelled binary tree
|
||||
-- Objective: Print each "level" of the tree on a separate line
|
||||
@ -15,41 +19,41 @@ main = exampleTwo
|
||||
-- / / \
|
||||
-- 4 5 6
|
||||
|
||||
label = \node : head node
|
||||
label = \node : Lib.head node
|
||||
|
||||
left = (\node : if (emptyList? node)
|
||||
left = (\node : Lib.if (Lib.emptyList? node)
|
||||
[]
|
||||
(if (emptyList? (tail node))
|
||||
(Lib.if (Lib.emptyList? (Lib.tail node))
|
||||
[]
|
||||
(head (tail node))))
|
||||
(Lib.head (Lib.tail node))))
|
||||
|
||||
right = (\node : if (emptyList? node)
|
||||
right = (\node : Lib.if (Lib.emptyList? node)
|
||||
[]
|
||||
(if (emptyList? (tail node))
|
||||
(Lib.if (Lib.emptyList? (Lib.tail node))
|
||||
[]
|
||||
(if (emptyList? (tail (tail node)))
|
||||
(Lib.if (Lib.emptyList? (Lib.tail (Lib.tail node)))
|
||||
[]
|
||||
(head (tail (tail node))))))
|
||||
(Lib.head (Lib.tail (Lib.tail node))))))
|
||||
|
||||
processLevel = y (\self queue : if (emptyList? queue)
|
||||
processLevel = Lib.y (\self queue : Lib.if (Lib.emptyList? queue)
|
||||
[]
|
||||
(pair (map label queue) (self (filter
|
||||
(\node : not? (emptyList? node))
|
||||
(lconcat (map left queue) (map right queue))))))
|
||||
(Lib.pair (Lib.map label queue) (self (Lib.filter
|
||||
(\node : Lib.not? (Lib.emptyList? node))
|
||||
(Lib.lconcat (Lib.map left queue) (Lib.map right queue))))))
|
||||
|
||||
levelOrderTraversal_ = \a : processLevel (t a t)
|
||||
|
||||
toLineString = y (\self levels : if (emptyList? levels)
|
||||
toLineString = Lib.y (\self levels : Lib.if (Lib.emptyList? levels)
|
||||
""
|
||||
(lconcat
|
||||
(lconcat (map (\x : lconcat x " ") (head levels)) "")
|
||||
(if (emptyList? (tail levels)) "" (lconcat (t (t 10 t) t) (self (tail levels))))))
|
||||
(Lib.lconcat
|
||||
(Lib.lconcat (Lib.map (\x : Lib.lconcat x " ") (Lib.head levels)) "")
|
||||
(Lib.if (Lib.emptyList? (Lib.tail levels)) "" (Lib.lconcat (t (t 10 t) t) (self (Lib.tail levels))))))
|
||||
|
||||
levelOrderToString = \s : toLineString (levelOrderTraversal_ s)
|
||||
|
||||
flatten = foldl (\acc x : lconcat acc x) ""
|
||||
flatten = Lib.foldl (\acc x : Lib.lconcat acc x) ""
|
||||
|
||||
levelOrderTraversal = \s : lconcat (t 10 t) (flatten (levelOrderToString s))
|
||||
levelOrderTraversal = \s : Lib.lconcat (t 10 t) (flatten (levelOrderToString s))
|
||||
|
||||
exampleOne = levelOrderTraversal [("1")
|
||||
[("2") [("4") t t] t]
|
||||
|
@ -1,20 +1,24 @@
|
||||
!module Size
|
||||
|
||||
!import "lib/base.tri" Lib
|
||||
|
||||
main = size size
|
||||
|
||||
compose = \f g x : f (g x)
|
||||
|
||||
succ = y (\self :
|
||||
triage
|
||||
succ = Lib.y (\self :
|
||||
Lib.triage
|
||||
1
|
||||
t
|
||||
(triage
|
||||
(Lib.triage
|
||||
(t (t t))
|
||||
(\_ tail : t t (self tail))
|
||||
(\_ Lib.tail : t t (self Lib.tail))
|
||||
t))
|
||||
|
||||
size = (\x :
|
||||
(y (\self x :
|
||||
(Lib.y (\self x :
|
||||
compose succ
|
||||
(triage
|
||||
(Lib.triage
|
||||
(\x : x)
|
||||
self
|
||||
(\x y : compose (self x) (self y))
|
||||
|
@ -1,4 +1,8 @@
|
||||
main = toSource not?
|
||||
!module ToSource
|
||||
|
||||
!import "lib/base.tri" Lib
|
||||
|
||||
main = toSource Lib.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.
|
||||
@ -12,29 +16,29 @@ main = toSource not?
|
||||
-- triage = (\leaf stem fork : t (t leaf stem) fork)
|
||||
|
||||
-- Base case of a single Leaf
|
||||
sourceLeaf = t (head "t")
|
||||
sourceLeaf = t (Lib.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.
|
||||
t (Lib.head "(") -- Start with a left parenthesis "(".
|
||||
(t (Lib.head "t") -- Add a "t"
|
||||
(t (Lib.head " ") -- Add a space.
|
||||
(convert a -- Recursively convert the argument.
|
||||
(t (Lib.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.
|
||||
t (Lib.head "(") -- Start with a left parenthesis "(".
|
||||
(t (Lib.head "t") -- Add a "t"
|
||||
(t (Lib.head " ") -- Add a space.
|
||||
(convert a -- Recursively convert the first arg.
|
||||
(t (Lib.head " ") -- Add another space.
|
||||
(convert b -- Recursively convert the second arg.
|
||||
(t (Lib.head ")") rest)))))))) -- Close with ")" and append the rest.
|
||||
|
||||
-- Wrapper around triage
|
||||
toSource_ = y (\self arg :
|
||||
triage
|
||||
toSource_ = Lib.y (\self arg :
|
||||
Lib.triage
|
||||
sourceLeaf -- `triage` "a" case, Leaf
|
||||
(sourceStem self) -- `triage` "b" case, Stem
|
||||
(sourceFork self) -- `triage` "c" case, Fork
|
||||
@ -43,5 +47,5 @@ toSource_ = y (\self arg :
|
||||
-- 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)))"
|
||||
exampleOne = toSource Lib.true -- OUT: "(t t)"
|
||||
exampleTwo = toSource Lib.not? -- OUT: "(t (t (t t) (t t t)) (t t (t t t)))"
|
||||
|
Reference in New Issue
Block a user