Merge branch 'main' into feature/ocaml-doc

.github/Dockerfile

@@ -6,5 +6,8 @@ ENV OPAMJOBS=$NCPUS
 
 RUN opam repo add coq-released https://coq.inria.fr/opam/released \
     && opam update \
-    && opam install coq-equations coq-menhirlib menhir ppx_inline_test \
+    && opam install coq-equations coq-menhirlib menhir ppx_expect \
     && eval $(opam env)
+
+RUN sudo apt-get update -y -q \
+    && DEBIAN_FRONTEND=noninteractive sudo apt-get install -y -q --no-install-recommends pandoc

.github/workflows/ci_build.yaml

@@ -3,9 +3,11 @@ on:
   push:
     branches:
       - main
+      - ext/**
   pull_request:
     branches:
       - main
+      - ext/**
   workflow_dispatch:
 
 permissions:
@@ -71,12 +73,14 @@ jobs:
             endGroup
           script: |
             startGroup "Build binary"
+              make pretty-timed
               if [[ "${{ env.DOC_DEPLOY }}" == 'true' ]]; then
                 make coqdoc
-              else
-                make
               fi
             endGroup
+            startGroup "Run inline tests"
+              dune runtest
+            endGroup
           after_script: |
             startGroup "after"
             endGroup

.gitignore

@@ -1,4 +1,5 @@
 _build
+*.opam
 
 # Ignore generated parser code
 **/parser.ml

.ocamlformat

@@ -1,2 +1,8 @@
 profile = default
-version = 0.24.1
+version = 0.26.2
+
+break-fun-decl = fit-or-vertical
+break-fun-sig = fit-or-vertical
+cases-exp-indent = 3
+exp-grouping = preserve
+if-then-else = keyword-first

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024 the CompLogic group, Mcgill University
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

Makefile

@@ -1,10 +1,14 @@
-.PHONY: all clean
+.PHONY: all pretty-timed test coqdoc clean
 
 all:
 	@$(MAKE) -C theories
 	@dune build
 
-coqdoc: all
+pretty-timed:
+	@$(MAKE) pretty-timed -C theories
+	@dune build
+
+coqdoc:
 	@${MAKE} coqdoc -C theories
 
 clean:

README.md

@@ -79,6 +79,10 @@ possible.
 
 Once `make` finishes, you can run the binary:
 ```
+dune exec mcltt examples/nary.mcl # or your own example
+```
+or more directly
+```
 _build/default/driver/mcltt.exe examples/nary.mcl # or your own example
 ```
 
@@ -88,3 +92,10 @@ cd theories
 make
 ```
 
+## Branches
+
+The Github repo includes the following special branches:
+
+1. `main`: the main branch that is used to generate this homepage and Coqdoc;
+2. `ext/*`: branches in this pattern are variations of `main` that implements various extensions. They are often used to implement extensions that require non-trivial workload and are aimed to be merged to `main` eventually;
+3. `gh-pages`: the branch to host the homepage.

assets/extra/header.html

@@ -18,7 +18,7 @@
     <span class="button" id="toggle-proofs"></span>
 
     <span class="right">
-      <a href="../">Project Page</a>
+      <a href="./">Project Page</a>
       <a href="./indexpage.html"> Index </a>
       <a href="./toc.html"> Table of Contents </a>
     </span>

driver/Lexer.mli

@@ -0,0 +1,7 @@
+val format_position : Format.formatter -> Lexing.position -> unit
+val format_range : Format.formatter -> Lexing.position * Lexing.position -> unit
+val format_token : Format.formatter -> MclttExtracted.Parser.token -> unit
+val read : Lexing.lexbuf -> MclttExtracted.Parser.token
+
+val lexbuf_to_token_buffer :
+  Lexing.lexbuf -> MclttExtracted.Parser.MenhirLibParser.Inter.buffer

driver/Lexer.mll

@@ -104,3 +104,14 @@ and comment =
   parse
   | "*)" { read lexbuf }
   | _ { comment lexbuf }
+
+{
+  let rec lexbuf_to_token_buffer lexbuf =
+    lazy
+      begin
+        try
+          MenhirLibParser.Inter.Buf_cons (read lexbuf, lexbuf_to_token_buffer lexbuf)
+        with
+        | Failure s -> prerr_string s; raise Exit
+      end
+}

driver/Main.ml

@@ -4,26 +4,23 @@ open Parser
 open MenhirLibParser.Inter
 open Entrypoint
 
-let main ?(default_fp = "") () =
-  let fp =
-    if default_fp <> ""
-    then default_fp
-    else
-      begin
-        print_string "File path to load: ";
-        read_line ()
-      end
-  in
-  let chan = open_in fp in
-  (* Before parsing, we must generate a token stream from a lexer buffer,
-     which we then feed into the parser. *)
-  let rec loop lexbuf =
-    lazy (
-        try
-          Buf_cons (Lexer.read lexbuf, loop lexbuf)
-        with
-        | Failure s -> prerr_string s; raise Exit) in
-  let token_stream = loop (Lexing.from_channel chan) in
-  let res = Entrypoint.main 500 token_stream in
-  Format.printf "%a@."
-    PrettyPrinter.format_main_result res
+let get_exit_code result : int =
+  match result with
+  | AllGood _ -> 0
+  | TypeCheckingFailure _ -> 1
+  | ElaborationFailure _ -> 2
+  | ParserFailure _ -> 3
+  | ParserTimeout _ -> 4
+
+let main_of_lexbuf lexbuf =
+  Lexer.lexbuf_to_token_buffer lexbuf
+  (* Here, the integer argument is a *log* version of fuel.
+     Thus, 500 means 2^500. *)
+  |> Entrypoint.main 500
+  |> fun r -> Format.printf "%a@." PrettyPrinter.format_main_result r; get_exit_code r
+
+let main_of_filename filename =
+  Lexing.from_channel (open_in filename) |> main_of_lexbuf
+
+let main_of_program_string program =
+  Lexing.from_string program |> main_of_lexbuf

driver/Main.mli

@@ -0,0 +1,2 @@
+val main_of_filename : string -> int
+val main_of_program_string : string -> int

driver/Mcltt.ml

@@ -1,10 +1,12 @@
 open Mcltt.Main
 
 let () =
-  if Array.length Sys.argv <> 2 then
-    begin
-      Printf.fprintf stderr "incorrect input: %s <input-file>\n" Sys.argv.(0);
-      exit 1
-    end;
+  if Array.length Sys.argv <> 2
+  then begin
+    Printf.fprintf stderr
+      "Missing <input-file> argument.\nUsage: %s <input-file>\n" Sys.argv.(0);
+    exit 5
+  end;
   let filename = Sys.argv.(1) in
-  main ~default_fp:filename ()
+  let code = main_of_filename filename in
+  exit code