From 70f0b3874c36fe67764fe0ab9a6c71fd80fc3d57 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 28 Feb 2023 23:28:12 -0500
Subject: [PATCH] wip: feat(leancheck): start binary to check lean proofs

---
 leancheck.sh                |  2 ++
 src/leancheck/dune          |  4 +++
 src/leancheck/leancheck.ml  | 35 ++++++++++++++++++++++++++
 src/leancheck/parse.ml      | 50 +++++++++++++++++++++++++++++++++++++
 src/leancheck/parse.mli     |  6 +++++
 src/leancheck/parse_intf.ml |  4 +++
 6 files changed, 101 insertions(+)
 create mode 100755 leancheck.sh
 create mode 100644 src/leancheck/dune
 create mode 100644 src/leancheck/leancheck.ml
 create mode 100644 src/leancheck/parse.ml
 create mode 100644 src/leancheck/parse.mli
 create mode 100644 src/leancheck/parse_intf.ml

diff --git a/leancheck.sh b/leancheck.sh
new file mode 100755
index 00000000..7077ef40
--- /dev/null
+++ b/leancheck.sh
@@ -0,0 +1,2 @@
+#!/bin/sh
+exec dune exec --profile=release --display=quiet -- src/leancheck/leancheck.exe $@
diff --git a/src/leancheck/dune b/src/leancheck/dune
new file mode 100644
index 00000000..afc5a15c
--- /dev/null
+++ b/src/leancheck/dune
@@ -0,0 +1,4 @@
+(executable
+ (name leancheck)
+ (flags :standard -w +32 -open Sidekick_sigs -open Sidekick_util)
+ (libraries containers sidekick.core-logic sidekick.util))
diff --git a/src/leancheck/leancheck.ml b/src/leancheck/leancheck.ml
new file mode 100644
index 00000000..75baceb7
--- /dev/null
+++ b/src/leancheck/leancheck.ml
@@ -0,0 +1,35 @@
+module T = Sidekick_core_logic.Term
+
+let ( let@ ) = ( @@ )
+
+let process_files (files : string list) : unit =
+  let st = T.Store.create ~size:1024 () in
+  Log.debugf 1 (fun k ->
+      k "(@[process-files %a@])" Fmt.Dump.(list string) files);
+
+  let proc_file (file : string) : unit =
+    let@ ic = CCIO.with_in file in
+    Parse.parse (`In ic)
+      (module struct
+        let ns _ _ = ()
+        let ni _ _ = ()
+      end)
+  in
+
+  List.iter proc_file files;
+  ()
+
+let () =
+  let files = ref [] in
+  let opts =
+    [
+      "--debug", Arg.Int Log.set_debug, " set debug level";
+      "-d", Arg.Int Log.set_debug, " like --debug";
+    ]
+    |> Arg.align
+  in
+
+  Arg.parse opts (CCList.Ref.push files) "leancheck file+";
+  if !files = [] then failwith "provide at least one file";
+
+  process_files (List.rev !files)
diff --git a/src/leancheck/parse.ml b/src/leancheck/parse.ml
new file mode 100644
index 00000000..27b94520
--- /dev/null
+++ b/src/leancheck/parse.ml
@@ -0,0 +1,50 @@
+module type CALLBACK = Parse_intf.CALLBACK
+
+type callback = (module CALLBACK)
+type input = [ `String of string | `In of in_channel ]
+
+module type IN = sig
+  val next_line : unit -> string option
+end
+
+let in_of_input (i : input) : (module IN) =
+  match i with
+  | `String s ->
+    (module struct
+      let i = ref 0
+
+      let next_line () =
+        if !i = String.length s then
+          None
+        else (
+          match String.index_from s !i '\n' with
+          | exception Not_found ->
+            let r = Some (String.sub s !i (String.length s - !i)) in
+            i := String.length s;
+            r
+          | j ->
+            let r = Some (String.sub s !i (j - !i)) in
+            i := j + 1;
+            r
+        )
+    end)
+  | `In ic ->
+    (module struct
+      let next_line () = try Some (input_line ic) with End_of_file -> None
+    end)
+
+let parse (input : input) (cb : callback) : unit =
+  let (module CB) = cb in
+  let (module IN) = in_of_input input in
+
+  let rec loop () =
+    match IN.next_line () with
+    | None -> ()
+    | Some line ->
+      Printf.eprintf "line %S\n" line;
+
+      (* TODO: cb *)
+      loop ()
+  in
+
+  loop ()
diff --git a/src/leancheck/parse.mli b/src/leancheck/parse.mli
new file mode 100644
index 00000000..81c66f1c
--- /dev/null
+++ b/src/leancheck/parse.mli
@@ -0,0 +1,6 @@
+module type CALLBACK = Parse_intf.CALLBACK
+
+type callback = (module CALLBACK)
+type input = [ `String of string | `In of in_channel ]
+
+val parse : input -> callback -> unit
diff --git a/src/leancheck/parse_intf.ml b/src/leancheck/parse_intf.ml
new file mode 100644
index 00000000..8cde17b2
--- /dev/null
+++ b/src/leancheck/parse_intf.ml
@@ -0,0 +1,4 @@
+module type CALLBACK = sig
+  val ns : int -> string -> unit
+  val ni : int -> int -> unit
+end