wip: feat(leancheck): start binary to check lean proofs

leancheck.sh

@@ -0,0 +1,2 @@
+#!/bin/sh
+exec dune exec --profile=release --display=quiet -- src/leancheck/leancheck.exe $@

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))

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)

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 ()

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

src/leancheck/parse_intf.ml

@@ -0,0 +1,4 @@
+module type CALLBACK = sig
+  val ns : int -> string -> unit
+  val ni : int -> int -> unit
+end