README.md

TAPL in Scala

Roadmap

1. tapl.arith - (chapters 3, 4).
2. tapl.untyped (chapters 5-7).
3. tapl.fulluntyped (chapters 5-7).
4. tapl.tyarith (chapter 8).
5. tapl.simplebool (chapter 10).
6. tapl.fullsimple (chapter 9 and 11).
7. tapl.fullref (chapter 13, 18)
8. tapl.fullerror (chapter 14)
9. tapl.rcdsubbot (chapter 15)
10. tapl.fullsub (chapters 15-17)
11. tapl.bot (chapter 16)
12. tapl.fullequirec (chapter 20).
13. tapl.fullisorec (chapter 20).
14. tapl.equirec (chapter 21).
15. tapl.recon (chapter 22).
16. tapl.fullrecon (chapter 22).
17. tapl.fullpoly (chapters 23, 24).
18. tapl.fullomega (chapters 23, 29, 30).
19. tapl.fullfsub (chapters 26, 28).
20. tapl.fullfomsub (chapters 26, 31).
21. tapl.fullfomsubref (chapter 27) combination of all systems from the book.

Code structure

The code structure for each implementation follows the original code structure and consists of 4 files:

• syntax.scala - AST, contexts, commands, pretty-printing.
• parser.scala - parsing.
• core.scala - evaluator and typer.
• demo.scala - the main application for processing input files.

Running

sbt
> run

Multiple main classes detected, select one to run:

 [1] tapl.fullisorec.FullIsorecDemo
 [2] tapl.rcdsubbot.RcdSubBotDemo
 [3] tapl.arith.ArithDemo
 [4] tapl.simplebool.SimpleBoolDemo
 [5] tapl.equirec.EquirecDemo
 [6] tapl.tyarith.TyArithDemo
 [7] tapl.untyped.UntypedDemo
 [8] tapl.fullfsub.FullFSubDemo
 [9] tapl.fullpoly.FullPolyDemo
 [10] tapl.recon.ReconDemo
 [11] tapl.fullfomsub.FullFomSubDemo
 [12] tapl.fullerror.FullErrorDemo
 [13] tapl.fulluntyped.UntypedDemo
 [14] tapl.fullsub.FullSubDemo
 [15] tapl.fullequirec.FullEquirecDemo
 [16] tapl.fullrecon.FullReconDemo
 [17] tapl.fullref.FullRefDemo
 [18] tapl.fullomega.FullOmegaDemo
 [19] tapl.fullsimple.FullSimpleDemo
 [20] tapl.fullfomsubref.FullFomSubRefDemo
 [21] tapl.bot.BotDemo

Enter number: 21

[info] Running tapl.bot.BotDemo
====================
(lambda x: Top. x): Top -> Top;
||
\/
(lambda x: Top. x): Top -> Top;
====================
((lambda x: Top. x) (lambda x: Top. x)): Top;
||
\/
(lambda x: Top. x): Top -> Top;
====================
((lambda x: Top -> Top. x) (lambda x: Top. x)): Top -> Top;
||
\/
(lambda x: Top. x): Top -> Top;
====================
(lambda x: Bot. x): Bot -> Bot;
||
\/
(lambda x: Bot. x): Bot -> Bot;
====================
(lambda x: Bot. x x): Bot -> Bot;
||
\/
(lambda x: Bot. x x): Bot -> Bot;

> run-main tapl.fulluntyped.UntypedDemo progs/fulluntyped.tapl
[info] Running tapl.fulluntyped.UntypedDemo progs/fulluntyped.tapl
====================
tru;
||
\/
(lambda t. lambda f. t);
====================
fls;
||
\/
(lambda t. lambda f. f);
====================
(tru tru);
||
\/
(lambda f. lambda t. lambda f'. t);
====================
(tru fls);
||
\/
(lambda f. lambda t. lambda f'. f');
====================
(test tru v w);
||
\/
((lambda m. lambda n. (lambda t. lambda f. t) m n) v w);
...