Project structure

Dockerfile

@@ -7,12 +7,9 @@ RUN git clone https://github.com/songyahui/AlgebraicEffect.git
 
 WORKDIR AlgebraicEffect
 
-RUN sudo apt-get update -y && sudo apt-get install -y libgmp-dev pkg-config python3
-
-RUN opam install dune menhir ppx_deriving ppx_expect unionFind visitors z3
-
-RUN sudo apt-get install -y libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev
-RUN opam install why3-ide
+RUN sudo apt-get update -y && \
+  sudo apt-get install -y libgmp-dev pkg-config python3 libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev && \
+  opam install dune menhir ppx_deriving ppx_expect unionFind visitors z3 why3-ide
 
 RUN eval $(opam env) && dune build @install
 ENV PATH $PWD:$PATH

README.md

@@ -13,14 +13,18 @@ ICFP24 (#95) submission:
 
 We have a docker image to try out our tool, which is detailed in the 
 
-```
-docker pull yahuuuuui/icfp24-heifer:ubuntu
-docker run -i -t yahuuuuui/fse24-heifer:ubuntu /bin/bash
+```sh
+docker pull yahuuuuui/heifer-icfp24:latest
+docker run -it --rm yahuuuuui/heifer-icfp24:latest bash
 ```
 
-The source code repository is placed in "/home/", called "AlgebraicEffect". 
+The source code repository is placed in `/home/opam/AlgebraicEffect`. 
 The benchmarks are also summarized in the docker env. 
-Alternatively, one could build \toolName from scratch using a Linux system (tested on Ubuntu 22.04.4 LTS), with the following dependencies:
+
+To build Heifer from scratch, the same Dockerfile used to build the above image is provided together with the source code, and may be used or consulted.
+
+<!--
+Alternatively, one could build Heifer from scratch using a Linux system (tested on Ubuntu 22.04.4 LTS), with the following dependencies:
 
 ```
 opam switch 5.0.0
@@ -30,23 +34,36 @@ which browserify
 dune build
 dune test
 ```
+-->
+
+Use `heifer $EXAMPLE` to run examples.
 
-Use `dune exec parsing/hip.exe $EXAMPLE` to run examples. Effect-related programs are in [src/evaluation](src/evaluation), higher-order programs are in [src/examples](src/examples).
+<!-- Effect-related programs are in [src/evaluation](src/evaluation), higher-order programs are in [src/examples](src/examples). -->
 
 ## Reproduce Table 1
 
+```sh
+heifer src/demo/1_State_Monad.ml
+heifer src/demo/2_Inductive_Sum.ml
+heifer src/demo/3_Deep_Right_Toss.ml
+heifer src/demo/4_Deep_Left_Toss.ml
+heifer src/demo/5_Shallow_Right_Toss.ml
+heifer src/demo/6_Shallow_Left_Toss.ml
+heifer src/demo/7_amb.ml
+heifer src/demo/8_schduler.ml
 ```
-dune exec parsing/hip.exe src/demo/1_State_Monad.ml
-dune exec parsing/hip.exe src/demo/2_Inductive_Sum.ml
-dune exec parsing/hip.exe src/demo/3_Deep_Right_Toss.ml
-dune exec parsing/hip.exe src/demo/4_Deep_Left_Toss.ml
-dune exec parsing/hip.exe src/demo/5_Shallow_Right_Toss.ml
-dune exec parsing/hip.exe src/demo/6_Shallow_Left_Toss.ml
-dune exec parsing/hip.exe src/demo/7_amb.ml
-dune exec parsing/hip.exe src/demo/8_schduler.ml
-```
 
 
+## Project structure
+
+The source code is in the `parsing` directory.
+The project builds with dune, and the `dune` file in that directory contains a listing of the project's components.
+A brief description of the relevant ones:
+
+- hip: entry point
+- ocamlfrontend: part of the OCaml 4.12 compiler frontend, modified to parse the `(*@ comments @*)` used for writing ESL specifications
+- hipcore: AST for staged/separation logic/pure formulae and operations such as pretty-printing, substitution, etc.
+- hipprover: the entailment prover for staged formulae, which consists of modules for applying the forward rules, applying lemmas, proof search, biabduction-based normalization, and entailment checking
 
 ## Docs