From 6fee09848bd4b4b2fbc087af0dcd1b8e6ad0ca4b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 6 Mar 2023 21:51:13 -0500
Subject: [PATCH] leancheck: parse ind

---
 src/leancheck/leancheck.ml  | 19 +++++++++++++++++++
 src/leancheck/parse.ml      | 17 +++++++++++++++++
 src/leancheck/parse_intf.ml |  8 ++++++++
 3 files changed, 44 insertions(+)

diff --git a/src/leancheck/leancheck.ml b/src/leancheck/leancheck.ml
index 761a22e1..b9111b98 100644
--- a/src/leancheck/leancheck.ml
+++ b/src/leancheck/leancheck.ml
@@ -138,6 +138,25 @@ let process_files ~max_err (files : string list) : unit =
             (T.pi (binder_of_string b) (Idx.get_name idx n)
                ~var_ty:(Idx.get_term idx i) (Idx.get_term idx j))
 
+        let ind ~n_params ~nidx ~tyidx ~intros ~univ_params : unit =
+          let name = Idx.get_name idx nidx in
+          let ty = Idx.get_term idx tyidx in
+          let intros =
+            List.map
+              (fun (i, j) -> Idx.get_name idx i, Idx.get_term idx j)
+              intros
+          in
+          let univ_params =
+            List.map (fun i -> Idx.get_name idx i) univ_params
+          in
+          Fmt.eprintf "@[<2>>> @{<Green>Ind@} %s %a:%a [%d params] :=@ %a@]@."
+            name
+            Fmt.Dump.(list string)
+            univ_params T.pp_debug ty n_params
+            Fmt.(hvbox @@ Dump.(list @@ pair string T.pp_debug))
+            intros;
+          ()
+
         let after_line () = Fmt.eprintf "%a@." Idx.dump idx
       end)
   in
diff --git a/src/leancheck/parse.ml b/src/leancheck/parse.ml
index 46385ba2..30f07858 100644
--- a/src/leancheck/parse.ml
+++ b/src/leancheck/parse.ml
@@ -83,6 +83,23 @@ let parse ?(max_errors = max_int) (input : input) (cb : callback) : unit =
          | [ I at; S "#ES"; I i ] -> CB.es ~at i
          | [ I at; S "#EL"; S b; I n; I i; I j ] -> CB.el ~at b n i j
          | [ I at; S "#EP"; S b; I n; I i; I j ] -> CB.ep ~at b n i j
+         | S "#IND" :: I n_params :: I nidx :: I tyidx :: I n_intros :: tl ->
+           let rec get_intros n acc = function
+             | l when n = 0 -> List.rev acc, l
+             | [] | [ _ ] -> failwith "missing intro"
+             | I nidx :: I tyidx :: tl ->
+               get_intros (n - 1) ((nidx, tyidx) :: acc) tl
+             | _ -> failwith "invalid intro"
+           in
+           let intros, l = get_intros n_intros [] tl in
+           let univ_params =
+             List.map
+               (function
+                 | I i -> i
+                 | _ -> failwith "invalid param")
+               l
+           in
+           CB.ind ~n_params ~nidx ~tyidx ~intros ~univ_params
          | _ ->
            incr n_errors;
            Fmt.eprintf "@{<Yellow>warn@}: unhandled line %d: %s@." !n_line line
diff --git a/src/leancheck/parse_intf.ml b/src/leancheck/parse_intf.ml
index 8834e4bd..051e034e 100644
--- a/src/leancheck/parse_intf.ml
+++ b/src/leancheck/parse_intf.ml
@@ -13,4 +13,12 @@ module type CALLBACK = sig
   val es : at:int -> int -> unit
   val el : at:int -> string -> int -> int -> int -> unit
   val ep : at:int -> string -> int -> int -> int -> unit
+
+  val ind :
+    n_params:int ->
+    nidx:int ->
+    tyidx:int ->
+    intros:(int * int) list ->
+    univ_params:int list ->
+    unit
 end