new proof terms

.github/workflows/format.yml

@@ -16,4 +16,4 @@ jobs:
     - id: 'dune-fmt'
       name: 'dune build @fmt'
       run: |-
-        nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs/archive/bffc22eb12172e6db3c5dde9e3e5628f8e3e7912.tar.gz  dep/format.nix --command "make check-format DUNE=dune"
+        nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs/archive/bffc22eb12172e6db3c5dde9e3e5628f8e3e7912.tar.gz  dep/format.nix --command "make check-format DUNE=dune DUNE_OPTS='--ignore-promoted-rules'"

dune-project

@@ -38,6 +38,7 @@
   imandrakit
   imandrakit-log
   imandrakit-io
+  (yojson-five :with-build)
   (pbrt
    (>= 3.0))
   (pbrt_yojson

imandrax-api.opam

@@ -18,6 +18,7 @@ depends: [
   "imandrakit"
   "imandrakit-log"
   "imandrakit-io"
+  "yojson-five" {with-build}
   "pbrt" {>= "3.0"}
   "pbrt_yojson" {>= "3.0"}
   "ocaml-protoc" {>= "3.1.1" & with-dev-setup}

src/lib/cir/typed_symbol.ml

@@ -1,6 +1,7 @@
 include Imandrax_api_common.Typed_symbol
 
-type t = Type.t t_poly [@@deriving twine, typereg, eq, ord, show]
+type t = Type.t Imandrax_api_common.Typed_symbol.t_poly
+[@@deriving twine, typereg, eq, ord, show]
 (** A value with its type schema *)
 
 let pp_ = ref pp

src/lib/cir/var.ml

@@ -2,7 +2,7 @@
 
 include Imandrax_api_common.Var
 
-type t = Type.t t_poly [@@deriving twine, typereg, show]
+type t = Type.t Imandrax_api_common.Var.t_poly [@@deriving twine, typereg, show]
 
 open Imandrax_api
 

src/lib/genbindings/gen_python.ml

@@ -23,6 +23,9 @@ from . import twine
 
 __all__ = ['twine']
 
+# offset in file
+type OffsetFor[T] = int
+
 type Error = Error_Error_core
 def twine_result[T,E](d: twine.Decoder, off: int, d0: Callable[...,T], d1: Callable[...,E]) -> T | E:
     match d.get_cstor(off=off):
@@ -122,6 +125,8 @@ let rec gen_type_expr (ty : tyexpr) : string =
       spf "%s | %s" (gen_type_expr x) (gen_type_expr y)
     | "Imandrakit_error__Error_core.Data.t", [] -> spf "unit"
     | "option", [ x ] -> spf "None | %s" (gen_type_expr x)
+    | "Imandrakit_twine.offset_for", [ x ] ->
+      spf "OffsetFor[%s]" (gen_type_expr x)
     | "Util_twine_.With_tag7.t", [ x ] -> spf "WithTag7[%s]" (gen_type_expr x)
     | "Util_twine_.Q.t", [] -> "tuple[int, int]"
     | s, [] -> mangle_ty_name s

src/lib/genbindings/resolve_ty_defs.ml

@@ -47,6 +47,7 @@ let names_to_exclude : Str_set.t =
       "Util_twine_.With_tag7.t";
       "Imandrakit_error__Error_core.Data.t";
       "Imandrax_api_eval__Value.Custom_value.t";
+      "Imandrakit_twine.offset_for";
       "option";
       "Util_twine_.Z.t";
       "Util_twine_.Q.t";

src/lib/gentypereg/dune

@@ -12,6 +12,7 @@
   imandrax-api.eval
   imandrax-api.report
   imandrax-api.proof
+  imandrax-api.proof3
   imandrax-api.tasks
   imandrax-api.artifact)
  (flags :standard -linkall))

src/lib/proof3/.ocamlformat-ignore

@@ -0,0 +1 @@
+types.ml

src/lib/proof3/common_pr_.ml

@@ -0,0 +1,5 @@
+module Mir = Imandrax_api_mir
+module MT = Mir.Term
+module MTy = Mir.Type
+
+type 'a offset_for = 'a Imandrakit_twine.offset_for [@@deriving eq, show, twine]

src/lib/proof3/deep_proof_step.ml

@@ -0,0 +1,5 @@
+include Types
+
+type t = deep_proof_step
+
+let iter = iter_deep_proof_step

src/lib/proof3/deep_sequent.ml

@@ -0,0 +1,11 @@
+(** A deep sequent, ie a constructive sequent of sequents. *)
+
+open Common_
+
+(** A deep sequent, ie a constructive sequent of sequents. *)
+type t = {
+  hyps: Imandrax_api_mir.Sequent.t list;  (** List of hypothese *)
+  concl: Imandrax_api_mir.Sequent.t;  (** Conclusion *)
+}
+[@@deriving eq, twine, typereg, show { with_path = false }]
+(** A deep sequent: constructive sequent of sequents *)

src/lib/proof3/dune

@@ -0,0 +1,36 @@
+(library
+ (name imandrax_api_proof3)
+ (public_name imandrax-api.proof3)
+ (synopsis "Proof terms for ImandraX.")
+ (flags
+  :standard
+  -open
+  Imandrakit
+  -open
+  Imandrax_api
+  -open
+  Imandrax_api_common)
+ (preprocess
+  (pps ppx_deriving.std imandrakit.twine.ppx imandrakit.typereg.ppx))
+ (libraries imandrakit imandrax-api imandrax-api.common imandrax-api.mir))
+
+(rule
+ (targets types.ml)
+ (mode promote)
+ (action
+  (with-stdout-to
+   %{targets}
+   (run ./gen/mk_rules.exe))))
+
+;(rule
+; (targets doc.md)
+; (mode promote)
+; (action
+;  (with-stdout-to
+;   %{targets}
+;   (run gen/mk_rules.exe --doc))))
+;
+;(install
+; (section doc)
+; (package imandrax-api)
+; (files doc.md))

src/lib/proof3/entrypoint.ml

@@ -0,0 +1,7 @@
+(** Entrypoint of a proof file.
+
+    This is the record containing the actual proof. *)
+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/codegen_md.ml

@@ -0,0 +1,92 @@
+module P = Spec_
+
+(*
+let bpf = Printf.bprintf
+let spf = Printf.sprintf
+
+let indent n s =
+  match String.split_on_char '\n' s with
+  | [] -> ""
+  | [ _ ] -> s
+  | s :: tl ->
+    String.concat "\n"
+    @@ (s :: List.map (fun line -> String.make n ' ' ^ line) tl)
+
+let terms_by_ret_type_ : (P.meta_type, P.dag_term list) Hashtbl.t =
+  let res = Hashtbl.create 32 in
+  List.iter
+    (fun (t : P.dag_term) ->
+      let l = Hashtbl.find_opt res t.ret |> Option.value ~default:[] in
+      Hashtbl.replace res t.ret (t :: l))
+    spec.dag_terms;
+  res
+
+let is_dag_type s : bool = Hashtbl.mem terms_by_ret_type_ (P.M_ty s)
+
+let rec pp_meta_type (m : P.meta_type) : string =
+  match m with
+  | M_ty s -> s
+  | M_list s -> spf "[%s]" (pp_meta_type s)
+  | M_option s -> spf "optional(%s)" (pp_meta_type s)
+  | M_tuple l -> spf "(%s)" @@ String.concat ", " @@ List.map pp_meta_type l
+
+let gendoc (out : Buffer.t) : unit =
+  let emit_dag_term (t : P.dag_term) : unit =
+    bpf out "- `%s : %s -> %s`\n" t.name
+      (String.concat ", " @@ List.map pp_meta_type t.args)
+      (pp_meta_type t.ret);
+    Option.iter
+      (fun n2 -> bpf out "  (full name used for codegen: `%s`)\n" n2)
+      t.full_name;
+    bpf out "  %s\n\n" (indent 2 t.doc)
+  in
+
+  let emit_dag_type (ty : P.dag_type) : unit =
+    bpf out "- `%s`: %s\n\n" ty.name ty.doc
+  in
+
+  bpf out "\n## DAG types \n\n";
+  List.iter emit_dag_type spec.dag_types;
+
+  bpf out "\n## DAG terms\n\n";
+
+  Hashtbl.iter
+    (fun (ty : P.meta_type) ts ->
+      bpf out "### Terms returning `%s`\n\n" (pp_meta_type ty);
+      List.iter emit_dag_term ts;
+      bpf out "\n")
+    terms_by_ret_type_;
+
+  let emit_builtin_sym (t : P.builtin_symbol) =
+    (* TODO: a comment with the type signature *)
+    if t.ret = P.M_ty "Type" then (
+      assert (t.args = []);
+      bpf out "- type builtin `%s`\n\n" t.name
+    ) else
+      bpf out "- builtin symbol `%s : %s%s -> %s`\n\n" t.name
+        (match t.params with
+        | [] -> ""
+        | l -> spf "forall %s. " (String.concat "," l))
+        (String.concat ", " @@ List.map pp_meta_type t.args)
+        (pp_meta_type t.ret)
+    (* TODO: doc? *)
+  in
+
+  (* shortcuts for builtins *)
+  bpf out "\n## Builtin symbols\n\n";
+  List.iter emit_builtin_sym spec.builtin_symbols;
+
+  ()
+
+let codegen (oc : out_channel) : unit =
+  let module M = Make (struct
+    let spec = P.spec
+  end) in
+  let buf = Buffer.create 32 in
+  bpf buf "# Imandra Proof System\n\n";
+  M.gendoc buf;
+  Buffer.output_buffer oc buf
+  *)
+
+(* TODO *)
+let gen = ignore

src/lib/proof3/gen/dune

@@ -0,0 +1,24 @@
+(executable
+ (name mk_rules)
+ (modules mk_rules parse_spec spec_ codegen_md)
+ (flags :standard)
+ (preprocess
+  (pps ppx_deriving_yojson ppx_deriving.std))
+ (libraries containers yojson-five))
+
+(rule
+ (targets spec_.ml)
+ (deps
+  (:file proof_spec.json5))
+ (action
+  (with-stdout-to
+   %{targets}
+   (progn
+    (echo "let spec = {json|")
+    (cat %{file})
+    (echo "|json}")))))
+
+(install
+ (package imandrax-api)
+ (section share)
+ (files proof_spec.json))