Add proof3 in_channel reader

Author: wintersteiger

src/lib/proof3/entrypoint.ml

@@ -1,7 +1,7 @@
 (** Entrypoint of a proof file.
 
     This is the record containing the actual proof. *)
-type t = { tree: Tree_node.t  (** The proof tree *) }
+type t = { tree: Tree_node.t Types.offset_for  (** The proof tree *) }
 [@@deriving twine, make, typereg, show { with_path = false }]
 (** This is the entrypoint into a proof file, from which we explore proof steps,
     the proof tree, etc. *)

src/lib/proof3/gen/proof_spec.json

@@ -513,17 +513,20 @@
           "DeepProofStep"
         ]
       },
-      "doc": "Takes `A1…An,B ||- G` (main) and `C_i ||- A_i` (sides) and returns `B, C1…Cn ||- G`."
+      "doc": "Takes `A1…An, B ||- G` (main) and `C_i ||- A_i` (sides) and returns `B, C1…Cn ||- G`."
     },
     {
       "name": "deep_intro",
       "ret": "DeepProofStep",
       "args": {
         "concl": "DeepSequent",
-        "assumptions": ["List", "Sequent"],
+        "assumptions": [
+          "List",
+          "Sequent"
+        ],
         "last_step": "ProofStep"
       },
-      "doc": "Takes last step `A |- B`, a list of assumptions C1…Cn used to prove that last step, and returns `C1…Cn ||- (A |- B)`."
+      "doc": "Takes last step `A |- B`, a list of assumptions [C1…Cn] used to prove that last step, and returns `C1…Cn ||- (A |- B)`."
     },
     {
       "name": "deep_subst",
@@ -553,4 +556,4 @@
       "doc": "Takes some form of reference to another proof file, and an offset `p` within that file. Intended to be used for subtasks."
     }
   ]
-}
+}

src/lib/proof3/reader.ml

@@ -65,3 +65,23 @@ class twine ~(mt : Mir.Term.State.t) (str : string) : t =
       let off = Imandrakit_twine.Decode.get_entrypoint dec in
       Entrypoint.of_twine dec off
   end
+
+class twine_in_channel ~(mt : Mir.Term.State.t) (ic : in_channel) : t =
+  let dec = Imandrakit_twine.Decode.of_in_channel ic in
+  let () = Mir.Term.State.add_to_dec dec mt in
+  object
+    method descr = "<twine in_channel reader>"
+
+    method read_step (p : Types.proof_step offset_for) : Types.proof_step =
+      Imandrakit_twine.Decode.read_ref dec Types.proof_step_of_twine p
+
+    method read_deep_step (p : Types.deep_proof_step offset_for) =
+      Imandrakit_twine.Decode.read_ref dec Types.deep_proof_step_of_twine p
+
+    method read_tree (p : Tree_node.t offset_for) =
+      Imandrakit_twine.Decode.read_ref dec Tree_node.of_twine p
+
+    method read_entrypoint () : Entrypoint.t =
+      let off = Imandrakit_twine.Decode.get_entrypoint dec in
+      Entrypoint.of_twine dec off
+  end

src/lib/proof3/types.ml

@@ -248,13 +248,13 @@ and deep_proof_step =
       main: deep_proof_step offset_for;
       sides: deep_proof_step offset_for list
     }
-    (** Takes [A1…An,B ||- G] (main) and [C_i ||- A_i] (sides) and returns [B, C1…Cn ||- G]. *)
+    (** Takes [A1…An, B ||- G] (main) and [C_i ||- A_i] (sides) and returns [B, C1…Cn ||- G]. *)
   | Deep_intro of {
       concl: Deep_sequent.t;
       assumptions: Imandrax_api_mir.Sequent.t list;
       last_step: proof_step offset_for
     }
-    (** Takes last step [A |- B], a list of assumptions C1…Cn used to prove that last step, and returns [C1…Cn ||- (A |- B)]. *)
+    (** Takes last step [A |- B], a list of assumptions [C1…Cn] used to prove that last step, and returns [C1…Cn ||- (A |- B)]. *)
   | Deep_subst of {
       concl: Deep_sequent.t;
       p: deep_proof_step offset_for;