# ROADMAP LEAFs - Learning Foundations of Computer Science using OCaml

Three technical tracks and one managment track

## Track OCamlFlat/OFLAT interaction with Learn-OCaml

### Description:

Adapt and integrate the OCamlFlat/OFLAT functionalities in the Learn OCaml environment.
Additionally, improve and extend the OCamlFlat FLAT library and the OFLAT graphical component.

### Team
Principal: Artur Miguel Dias (AMD)
Grant Holder: Rita Macedo (RM)
Master Student: Pedro Rocha (PR)

### Task 0 - Improve the user interface web-application OFLAT using a two-way communication between OCaml and JavaScript.

The initial version was limited to OCaml calling JavaScript.

- Main executor: RM
- Status: DONE

### Task 1 - Develop a method to enable the use the OCamlFlat library in Learn OCaml exercises.

Our first approach will involve: (1) a new Makefile rule to automatically merge all the code into a single file; (2) try to incorporate the source code of the entire Yojson library as a single module.

- Main executor: AMD
- Status: ongoing
- Start date: November 2020
- Due date: End of December 2020

#### % As of end of February - DONE
- Solution 1: The code of the library adjusted and extended to work in the constrained runtime environment of a standard Learn-OCaml installation (examples of restrictions: inability to load external libraries; unavailability of some language features, like mutually recursive modules).
- Solution 2: Lsylvestre taught us how to create a customized Learn-OCaml installation, with extra libraries.

### Task 2 - Graphical interface.

Regarding the graphical functionalities, make further efforts to improve code independency from the Ocsigen framework. We will start by developing a small static web page accessing most of the codebase of OFLAT and the OCaml code will be processed using the js_of_ocaml translator. Our graphical functionalities are currently available in OFLAT, a Ocsigen based web application.

We foresee a new software component that will be used: (1) in a Ocsigen application; (2) in a Learn OCaml plugin; (3) in an independent static web page.

- Main executor: RM
- Status: ongoing
- Start date: October 2020
- Due date: End of January 2021

#### % As of end of February - DONE
- Now there is a version of OFLAT that relies only on js_of_ocaml and this was a worthwhile effort.

### Task 3 - Review and reorganize the existing code of the OCamlFlat library.

The initial code (the supporting modules and the skeleton) has been written by a senior element. But the rest of the code (the logical elements) has been written by a junior element (under supervision).

- Main executor: AMD
- Status: to do
- Start date: December 2020
- Due date: End of January 2021

#### % As of end of February - DONE
- This has been an important reorganization of the code. Now the library is better prepared to continue to grow, as we envisage much more extensive functionalities in the future. Examples of what has been done: some cumbersome details has been simplified; got rid of mutually recursive modules to allow different modules in separate files; added a management system for predefined examples.

### Task 4 - Make the OCamlFlat library available in an opam-friendly way.

This should be easy, as soon as the protocols of OPAM are studied.

- Main executor: AMD
- Status: to do
- Start date: January 2021
- Due date: End of January 2021

#### % As of end of February - NOT DONE
- Makefiles has been developed for the OCamlFlat and OFLAT projects. However, no support for Dune as now. This will come later.

### Task 5 - Develop a number of FLAT exercises in the context of Learn OCaml.

Be creative and explore everything that Learn OCaml has to offer. Also enhance the concept of "exercise" already present in OCamlFlat.

- Main executor: PR
- Status: to do
- Start date: Mid December 2020
- Due date: End of January 2021

#### % As of end of February - ONGOING
- Unfortunately, PR stepped aside from his collaboration. But there is some work done by AMD and mainly by RM. We have some exercises successfully created, but we are still pursuing the optimal use of the testing mechanism of Learn-OCaml.

##### TODO:
- The work goes halfway and is going to continue. [RM - Due date: End of April]

##### NEW GOALS:
- Extend the OCamlFlat library to allow testing semantic properties of the models in the exercises (as now, only unit testing is supported). [AMD - Due date: End of April]
- Support a new more practical input format for models (as now, there are two formats supported - JSon and direct instantiation of a class - neither of which is practical to use in the context of Learn-OCaml). [AMD - Due date: End of April]

### Task 6 - Improve the internationalization mechanisms in OCamlFlat.

Currently, internationalization is working but is poorly implemented in OCamlFlat. It is worthwhile to improve this aspect and to consider the alternatives. ocplib-i18n (PPX + library) is a possible choice.

- Main executor: PR
- Status: to do
- Start date: February 2021
- Due date: End of February 2021

#### % As of end of February - NOT DONE YET
- Unfortunately, PR stepped aside from his collaboration. But this is a relatively easy task

#### TODO:
- Do it (and, by the way - add French). [RM - Due date: End of April]

#### Task 7 - Graphical interface and Learn-OCaml

Devise a way to use the OFLAT graphical functionalities inside Learn OCaml. Full plugin-like integration is the desired goal. However, a solution based on weak integration might also be pursued.

- Main executors: RM, PR
- Status: to do
- Start date: February 2021
- Due date: End of May 2021

#### % As of end of February - NOT DONE YET
- Unfortunately, PR stepped aside from his collaboration. He was supposedly to research the implementation of Learn-OCaml.

#### TODO:
- AMD thought about this general topic and we need to discuss some ideas. RM will be the main executor when we will have settled ideas.

### Task 8 - Refine the system

Improve the prototype to achieve superior quality and to make sure that a full range of features is supported.

- Main executors: RM, PR, AMD
- Status: to do
- Start date: June 2021
- Due date: End of September 2021

#### % As of end of February - ONGOING
- OFLAT: Better organization of the code, and this can (should) be improved further.
- OFLAT: Addition of tooltips.

#### Task 9 - Expand the functionalities of OCamlFlat/OFLAT

As now, OCamlFlat supports finite automata, regular expressions and context-free grammars; OFLAT supports finite automata, regular expressions, not yet context-free grammars. It would be nice to further develop OCamlFlat/OFLAT to support more topics from the usual introductory courses in Formal Language Theory, namely: LL(1) grammars, pushdown automata and Turing machines. The general challenge would be to devise effective pedagogical graphical interactions and the integration with exercise solving.

- This task might come to life in case there are students interested in writing a master's thesis on this topic.

## Track Code instrumentation and stepper

#### Description:

Propose and experiment automatic code instrumentation tools for step-by-step, forward and backward, execution with graphical visualisation of classical FLAT algorithms. The aim is a general mechanism, possibly using CPS transformations and log monads. The purpose here is to build a toolchain that accepts OCaml programs, automatically translates them into a step-by-step counterpart, and finally allows teachers/students to inspect how execution evolves.

##### Operational notes.
In a first call, we did not receive any application, since the previoulsy contacted student was no longer available when the call was launched. Since new master students are about to choose their mater thesis, we are about to open the call again.

###### new development:
The application process is now over. The grant holder to hire is Dário Vasco Santos.

#### Team
Principal: António Ravara
Simão Melo de Sousa
Grant Holder to hire

#### Task 0. Revisiting the log monad and CPS transformation

Departing from previous work [1][2], combining a log monad with

1. functions over primitive types or container types;
2. the automaton word accepter (as a basic example);
3. reimplementation of the CPS tranformation [2] using the new PPX Lib.

[[1] Rewinding functions through CPS - Marco Giunti](https://release.di.ubi.pt/factor/pdfs/rewind_exp_report.pdf)
[[2] Functional Programming with style and costless: CPS transformation "à la carte" (text in Portuguese) - Tiago Roxo, Mário Pereira, and Simão Melo de Sousa](https://release.di.ubi.pt/factor/pdfs/Programac%CC%A7a%CC%83o_funcional_com_estilo.pdf)

- Main executor: grant holder to hire
- Status: to do
- Start date: March 2021
- Due date: End of April 2021

#### Task 1. Combining a log monad with a CPS transformation on regular expressions.

Case study: empty word property, star height

- Main executor: grant holder to hire
- Status: to do
- Start date: May 2021
- Due date: mid of June 2021

#### Task 2. Combining a log monad with a CPS transformation on automata.

Case study: word acceptance problem

- Main executor: grant holder to hire
- Status: to do
- Start date: mid June 2021
- Due date: End of July 2021

#### Task 3. Generalisation to other data-structure.

In particular Push-Down automata and Grammars.
Case study: word acceptance problem

- Main executor: grant holder to hire
- Status: to do
- Start date: September 2021
- Due date: End of October 2021

#### Task 4. Generalisation to more advanced algorithms.

possible case studies: determinization, reg-exp to NDFA, LL(1) parser,...

- Main executor: grant holder to hire
- Status: to do
- Start date: November 2021
- Due date: End of December 2021

#### Task 5. Complete Integration into OFLAT.

- Main executor: grant holder to hire
- Status: to do
- Start date: January 2022
- Due date: End of January 2022

#### Task 6. Complete Integration with Learn-OCaml and reporting

- Main executor: grant holder to hire
- Status: to do
- Start date: February 2022
- Due date: End of March 2022

## Track PPX for program optimization

##### Description:

Development of rewriting tools, known as PPXs in the OCaml ecossystem, which manipulate the AST issued from the OCaml compiler in order to produce efficient and safe code from very declarative recursive implementations.
Our main goal within this track is to produce a toolbox of PPX rewriters that can be used to introduce students to the rewriters and meta-programming world. We also believe that having such methods and tools will improve the experience of newcomers with the OCaml language, since they will be able to easily translate mathematical notions (to which they are already familiar) into code, without incurring extra execution penalties.

#### Team
Principal: Mário Pereira
Artur Miguel Dias
Grant holder: Diogo Silvério

#### Task 0. Automatic memoization of recursive functions.
In this task, the grant holder started learning about the PPX machinery and its use as a meta-programming tool for OCaml code. As a warmup exercise, Diogo Silvério developed a PPX for the automatic memoization of recursive functions. This allowed us to turn mathematical textbook definitions (e.g., Fibonnaci, Ackerman) into linear-executing functions.

- Main executor: Diogo Silvério
- Status: done

#### Task 1. From higher-order to first-order implementations via defunctionalization.

We will develop a PPX that takes a higher-order OCaml program and turns it into a first-order one, via defunctionalization. Our starting point will be an existing PPX that turns a recursive definition into CPS, which we developed in previous work. By defunctionalizing CPS programs, we keep all the good guarantees about tail-recursive calls, but gain a constant execution factor. A challenging point about defunctionalization is that it requires typing information in order to build first-order representations of lambda-expressions. Typing is normally outside the scope of PPX rewriters, so we will use `compiler-libs` to interact with OCaml type-checker and obtain a typed version of our produced AST. A side interest about this task is concerned with our research interests on the formal verification of OCaml programs. We are the developers of Cameleer, a tool for the deductive verification of OCaml programs, on top of which we intend to explore the use of defunctionalization to verify (a subset of) higher-order implementations (https://github.com/mariojppereira/cameleer).
- Main executor: Diogo Silvério
- Status: ongoing
- Start date: November 2020
- Due date: End of January 2021

#### % As of mid March - Ongoing
- Unfortunalety, DS is struggling with a lot with this task, mainly due to his lack of experience in implementing compilers and programs manipulation software.
- The new due date is now end of March. MP will now work closely, on a daily basis, with DS in order to ensure the success of this task.

#### Task 2. Automatic hash-consing and memoization of data structures.

Our main goal here: to reproduce, automatically, the results by Conchon and Filliâtre in "Type-Safe Modular Hash-Consing", Workshop on ML 2006. More recently, Chet Murthy issued a thread on the ocaml discuss forum around the possibility of using PPX and ppx_lib to build automatic rewriters for hash-consed data structures (https://discuss.ocaml.org/t/bootstrapping-our-way-to-hashconsing-and-quotations-with-ppx-rewriters/6574).
- Main executor: Diogo Silvério
- Status: to do
- Start date: February 2021
- Due date: March 2021

#### % As of mid March - NOT DONE YET
- Due to delays in previous task, Task 2 has not started yet.
- The new due date is April 2021.

#### Task 3. Automatic conversion of recursive functions into loop structure.

Here, we intend to explore direct transformations of recursive definitions into equivalent loop constructions, without resorting to the CPS transformation. Our main goal is to investigate and implement the results by Liu and Stoller in "From recursion to iteration: what are the optimizations?", PEPM 2000.
- Main executor: Diogo Silvério
- Status: to do
- Start date: March 2021
- Due date: End of April 2021

#### % As of mid March - NOT DONE YET
- Due to delays in Task 1, Task 3 has not started yet.
- The new due date is end of May 2021.

#### Task 4. Study mechanisms for ensuring the correctness of developed PPX.

After developing a set of PPX rewriters, we want to ensure that these are indeed correct. A formal proof of correctness of our implementation would the most reliable approach, however we believe this is hardly feasible in the timeline of this project. Instead, we plan on using property-based testing tools, developed in OCaml, in order to provide increased guarantees about our rewriters. One can cite QCheck (https://github.com/c-cube/qcheck) and Monolith (https://gitlab.inria.fr/fpottier/monolith) as examples of such tools. We also plan on investigating approaches based on rich type and kind systems for sound meta-programming, developed in our institution (https://gitlab.inria.fr/fpottier/monolith).
- Main executor: Diogo Silvério
- Status: to do
- Start date: Beginning of May 2021
- Due date: End of May 2021

#### % As of mid March - NOT DONE YET
- Due to delays in Task 1, we will postpone the completion of Task 4.
- The new due date is end of June 2021.

#### Task 5. Reporting

The results of this track will be compiled as the core of Diogo's Master thesis. We will also write a pedagogical report on the obtained results, and use such document to guide students on their use and discovery of the PPX technology.
- Main executor: all
- Status: to do
- Start date: Beginning of June 2021
- Due date: End of June 2021

#### % As of mid March - NOT DONE YET
- We expect this task will not suffer any further delay.
- We will begin reporting in parallel with execution of Task 4.

## Track Managment

#### Description:

managment task for the LEAF project. This is a continuously changin task.

#### Team
Simão Melo de Sousa

#### Todo

#### Ongoing
- (always ongoing) web site for the project

#### Done

- Contract for the last grant holder
- Setup of a common Gitlab infrastruture for all LEAF tasks and gather all existing separate repositories below this one
- launch the call for grant for the last available master level grant
- Slack settings
- Hiring process for the two selected grant holders
- Public Call for 3 grants created and published (ecareers)
- Cooperation protocol defined and signed
- Registration of the projet in the UBI R&D project managment infrastruture