# 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
	 James Eversole
						James Eversole