simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor proof storage

Browse source
This commit is contained in:
Simon Cruanes 2021-10-21 23:28:53 -04:00
parent a871192c5e
commit c2b8d93cf4
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
9 changed files with 182 additions and 837 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/base/Base_types.ml
View file

@ -6,6 +6,7 @@ module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
module Proof_ser = Sidekick_base_proof_trace.Proof_ser
module Storage = Sidekick_base_proof_trace.Storage
type lra_pred = Sidekick_arith_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
type lra_op = Sidekick_arith_lra.op = Plus | Minus

99
src/base/Proof.ml
View file

@ -3,6 +3,7 @@ open Base_types
(* we store steps as binary chunks *)
module CS = Chunk_stack
module PS = Proof_ser
module Config = struct
type storage =
@ -35,19 +36,6 @@ module Config = struct
let no_store self = {self with storage=No_store}
end
(* where we store steps *)
module Storage = struct
type t =
| No_store
| In_memory of CS.Buf.t
| On_disk of string * out_channel
let pp out = function
| No_store -> Fmt.string out "no-store"
| In_memory _ -> Fmt.string out "in-memory"
| On_disk (file,_) -> Fmt.fprintf out "(on-file %S)" file
end
(* a step is just a unique integer ID.
The actual step is stored in the chunk_stack. *)
type proof_step = Proof_ser.ID.t
@ -113,31 +101,8 @@ let create ?(config=Config.default) () : t =
let empty = create ~config:Config.empty ()
let iter_chunks_ (r:CS.Reader.t) k =
let rec loop () =
CS.Reader.next r
~finish:nop_
~yield:(fun b i _len ->
let step =
Proof_ser.Bare.of_bytes_exn Proof_ser.Step.decode b ~off:i in
k step;
loop ()
)
in
loop ()
let iter_steps_backward (self:t) : Proof_ser.Step.t Iter.t =
fun yield ->
begin match self.storage with
| Storage.No_store -> ()
| Storage.In_memory buf ->
let r = CS.Reader.from_buf buf in
iter_chunks_ r yield
| Storage.On_disk (file, _oc) ->
let ic = open_in file in
let iter = CS.Reader.from_channel_backward ~close_at_end:true ic in
iter_chunks_ iter yield
end
let iter_steps_backward (self:t) =
Storage.iter_steps_backward self.storage
let dummy_step : proof_step = Int32.min_int
@ -172,20 +137,20 @@ let rec emit_term_ (self:t) (t:Term.t) : term_id =
with Not_found ->
let view = match Term_cell.map (emit_term_ self) @@ Term.view t with
| Term_cell.Bool b ->
Proof_ser.Step_view.Expr_bool {Proof_ser.Expr_bool.b}
PS.Step_view.Expr_bool {PS.Expr_bool.b}
| Term_cell.Ite (a,b,c) ->
Proof_ser.Step_view.Expr_if {Proof_ser.Expr_if.cond=a; then_=b; else_=c}
PS.Step_view.Expr_if {PS.Expr_if.cond=a; then_=b; else_=c}
| Term_cell.Not a ->
Proof_ser.Step_view.Expr_not {Proof_ser.Expr_not.f=a}
PS.Step_view.Expr_not {PS.Expr_not.f=a}
| Term_cell.App_fun (f, arr) ->
let f = emit_fun_ self f in
Proof_ser.Step_view.Expr_app {Proof_ser.Expr_app.f; args=(arr:_ IArray.t:> _ array)}
PS.Step_view.Expr_app {PS.Expr_app.f; args=(arr:_ IArray.t:> _ array)}
| Term_cell.Eq (a, b) ->
Proof_ser.Step_view.Expr_eq {Proof_ser.Expr_eq.lhs=a; rhs=b}
PS.Step_view.Expr_eq {PS.Expr_eq.lhs=a; rhs=b}
| LRA _ -> assert false (* TODO *)
in
@ -200,32 +165,44 @@ let emit_lit_ (self:t) (lit:Lit.t) : term_id =
let t = emit_term_ self (Lit.term lit) in
if sign then t else Int32.neg t
let emit_redundant_clause lits ~hyps (self:t) =
let emit_ (self:t) f : proof_step =
if enabled self then (
let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
let clause = Proof_ser.{Clause.lits} in
let hyps = Iter.to_array hyps in
let view = f () in
let id = alloc_id self in
emit_step_ self (
Proof_ser.({Step.id; view=Step_view.Step_rup {res=clause; hyps}})
);
emit_step_ self {PS.Step.id; view};
id
) else dummy_step
let[@inline] emit_redundant_clause lits ~hyps (self:t) =
emit_ self @@ fun() ->
let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
let clause = Proof_ser.{Clause.lits} in
let hyps = Iter.to_array hyps in
PS.Step_view.Step_rup {res=clause; hyps}
let emit_input_clause (lits:Lit.t Iter.t) (self:t) =
if enabled self then (
let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
let id = alloc_id self in
emit_step_ self (
Proof_ser.({Step.id; view=Step_view.Step_input {Step_input.c={Clause.lits}}})
);
id
) else dummy_step
emit_ self @@ fun () ->
let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
PS.(Step_view.Step_input {Step_input.c={Clause.lits}})
let define_term t u (self:t) =
emit_ self @@ fun () ->
let t = emit_term_ self t and u = emit_term_ self u in
PS.(Step_view.Expr_def {Expr_def.c=t; rhs=u})
let define_term _ _ _ = dummy_step
let proof_p1 _ _ (_pr:t) = dummy_step
let lemma_preprocess _ _ ~using:_ (_pr:t) = dummy_step
let lemma_true _ _ = dummy_step
let lemma_preprocess t u ~using (self:t) =
emit_ self @@ fun () ->
let t = emit_term_ self t and u = emit_term_ self u in
let using = using |> Iter.to_array in
PS.(Step_view.Step_preprocess {Step_preprocess.t; u; using})
let lemma_true t (self:t) =
emit_ self @@ fun () ->
let t = emit_term_ self t in
PS.(Step_view.Step_true {Step_true.true_=t})
let lemma_cc _ _ = dummy_step
let lemma_rw_clause _ ~using:_ (_pr:t) = dummy_step
let with_defs _ _ (_pr:t) = dummy_step

7
src/proof-trace-dump/proof_trace_dump.ml
View file

@ -1,6 +1,7 @@
module CS = Chunk_stack
module Proof_ser = Sidekick_base_proof_trace.Proof_ser
module Pr_trace = Sidekick_base_proof_trace
module Proof_ser = Pr_trace.Proof_ser
let file = ref ""
let quiet = ref false
@ -10,6 +11,10 @@ let parse_file () : unit =
CS.Reader.with_file_backward !file @@ fun reader ->
(* TODO: use the storage module function
Pr_trace.iter_steps_backward (Pr_trace.Storage.
*)
let n = ref 0 in
let rec display_steps () =
CS.Reader.next reader

41
src/proof-trace/Storage.ml Normal file
View file

@ -0,0 +1,41 @@
module CS = Chunk_stack
type t =
| No_store
| In_memory of CS.Buf.t
| On_disk of string * out_channel
let pp out = function
| No_store -> Fmt.string out "no-store"
| In_memory _ -> Fmt.string out "in-memory"
| On_disk (file,_) -> Fmt.fprintf out "(on-file %S)" file
let nop_ _ = ()
let iter_chunks_ (r:CS.Reader.t) k =
let rec loop () =
CS.Reader.next r
~finish:nop_
~yield:(fun b i _len ->
let step =
Proof_ser.Bare.of_bytes_exn Proof_ser.Step.decode b ~off:i in
k step;
loop ()
)
in
loop ()
let iter_steps_backward (self:t) : Proof_ser.Step.t Iter.t =
let module CS = Chunk_stack in
fun yield ->
begin match self with
| No_store -> ()
| In_memory buf ->
let r = CS.Reader.from_buf buf in
iter_chunks_ r yield
| On_disk (file, _oc) ->
let ic = open_in file in
let iter = CS.Reader.from_channel_backward ~close_at_end:true ic in
iter_chunks_ iter yield
end

8
src/proof-trace/Storage.mli Normal file
View file

@ -0,0 +1,8 @@
type t =
| No_store
| In_memory of Chunk_stack.Buf.t
| On_disk of string * out_channel
val pp : Format.formatter -> t -> unit
val iter_steps_backward : t -> Proof_ser.Step.t Iter.t

12
src/proof-trace/proof_ser.bare
View file

@ -36,10 +36,20 @@ type Step_preprocess {
using: []ID
}
type Step_true {
true_: ID
}
type Fun_decl {
f: string
}
# define c := rhs
type Expr_def {
c: ID
rhs: ID
}
type Expr_bool {
b: bool
}
@ -70,7 +80,9 @@ type Step_view
| Step_bridge_lit_expr
| Step_cc
| Step_preprocess
| Step_true
| Fun_decl
| Expr_def
| Expr_bool
| Expr_if
| Expr_not

86
src/proof-trace/proof_ser.ml
View file

@ -480,6 +480,28 @@ module Step_preprocess = struct
end
module Step_true = struct
type t = {
true_: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let true_ = ID.decode dec in {true_; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin ID.encode enc self.true_; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "true_=%a;@ " ID.pp x.true_;
Format.fprintf out "@]}";
end) out self
end
module Fun_decl = struct
type t = {
f: string;
@ -502,6 +524,30 @@ module Fun_decl = struct
end
module Expr_def = struct
type t = {
c: ID.t;
rhs: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let c = ID.decode dec in let rhs = ID.decode dec in {c; rhs; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin ID.encode enc self.c; ID.encode enc self.rhs; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "c=%a;@ " ID.pp x.c;
Format.fprintf out "rhs=%a;@ " ID.pp x.rhs;
Format.fprintf out "@]}";
end) out self
end
module Expr_bool = struct
type t = {
b: bool;
@ -644,7 +690,9 @@ module Step_view = struct
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
| Step_cc of Step_cc.t
| Step_preprocess of Step_preprocess.t
| Step_true of Step_true.t
| Fun_decl of Fun_decl.t
| Expr_def of Expr_def.t
| Expr_bool of Expr_bool.t
| Expr_if of Expr_if.t
| Expr_not of Expr_not.t
@ -661,12 +709,14 @@ module Step_view = struct
| 2L -> Step_bridge_lit_expr (Step_bridge_lit_expr.decode dec)
| 3L -> Step_cc (Step_cc.decode dec)
| 4L -> Step_preprocess (Step_preprocess.decode dec)
| 5L -> Fun_decl (Fun_decl.decode dec)
| 6L -> Expr_bool (Expr_bool.decode dec)
| 7L -> Expr_if (Expr_if.decode dec)
| 8L -> Expr_not (Expr_not.decode dec)
| 9L -> Expr_eq (Expr_eq.decode dec)
| 10L -> Expr_app (Expr_app.decode dec)
| 5L -> Step_true (Step_true.decode dec)
| 6L -> Fun_decl (Fun_decl.decode dec)
| 7L -> Expr_def (Expr_def.decode dec)
| 8L -> Expr_bool (Expr_bool.decode dec)
| 9L -> Expr_if (Expr_if.decode dec)
| 10L -> Expr_not (Expr_not.decode dec)
| 11L -> Expr_eq (Expr_eq.decode dec)
| 12L -> Expr_app (Expr_app.decode dec)
| _ -> raise (Bare.Decode.Error(Printf.sprintf "unknown union tag Step_view.t: %Ld" tag))
@ -687,23 +737,29 @@ module Step_view = struct
| Step_preprocess x ->
Bare.Encode.uint enc 4L;
Step_preprocess.encode enc x
| Fun_decl x ->
| Step_true x ->
Bare.Encode.uint enc 5L;
Fun_decl.encode enc x
| Expr_bool x ->
Step_true.encode enc x
| Fun_decl x ->
Bare.Encode.uint enc 6L;
Fun_decl.encode enc x
| Expr_def x ->
Bare.Encode.uint enc 7L;
Expr_def.encode enc x
| Expr_bool x ->
Bare.Encode.uint enc 8L;
Expr_bool.encode enc x
| Expr_if x ->
Bare.Encode.uint enc 7L;
Bare.Encode.uint enc 9L;
Expr_if.encode enc x
| Expr_not x ->
Bare.Encode.uint enc 8L;
Bare.Encode.uint enc 10L;
Expr_not.encode enc x
| Expr_eq x ->
Bare.Encode.uint enc 9L;
Bare.Encode.uint enc 11L;
Expr_eq.encode enc x
| Expr_app x ->
Bare.Encode.uint enc 10L;
Bare.Encode.uint enc 12L;
Expr_app.encode enc x
@ -719,8 +775,12 @@ module Step_view = struct
Format.fprintf out "(@[Step_cc@ %a@])" Step_cc.pp x
| Step_preprocess x ->
Format.fprintf out "(@[Step_preprocess@ %a@])" Step_preprocess.pp x
| Step_true x ->
Format.fprintf out "(@[Step_true@ %a@])" Step_true.pp x
| Fun_decl x ->
Format.fprintf out "(@[Fun_decl@ %a@])" Fun_decl.pp x
| Expr_def x ->
Format.fprintf out "(@[Expr_def@ %a@])" Expr_def.pp x
| Expr_bool x ->
Format.fprintf out "(@[Expr_bool@ %a@])" Expr_bool.pp x
| Expr_if x ->

762
src/proof-trace/sidekick_base_proof_ser.ml
View file

@ -1,762 +0,0 @@
[@@@ocaml.warning "-26-27"]
(* embedded runtime library *)
module Bare = struct
module String_map = Map.Make(String)
let spf = Printf.sprintf
module Decode = struct
exception Error of string
type t = {
bs: bytes;
mutable off: int;
}
type 'a dec = t -> 'a
let fail_ e = raise (Error e)
let fail_eof_ what =
fail_ (spf "unexpected end of input, expected %s" what)
let uint (self:t) : int64 =
let rec loop () =
if self.off >= Bytes.length self.bs then fail_eof_ "uint";
let c = Char.code (Bytes.get self.bs self.off) in
self.off <- 1 + self.off; (* consume *)
if c land 0b1000_0000 <> 0 then (
let rest = loop() in
let c = Int64.of_int (c land 0b0111_1111) in
Int64.(logor (shift_left rest 7) c)
) else (
Int64.of_int c (* done *)
)
in
loop()
let int (self:t) : int64 =
let open Int64 in
let i = uint self in
let sign_bit = logand 0b1L i in (* true if negative *)
let sign = equal sign_bit 0L in
let res =
if sign then (
shift_right_logical i 1
) else (
(* put sign back *)
logor (shift_left 1L 63) (shift_right_logical (lognot i) 1)
)
in
res
let u8 self : char =
let x = Bytes.get self.bs self.off in
self.off <- self.off + 1;
x
let i8 = u8
let u16 self =
let x = Bytes.get_int16_le self.bs self.off in
self.off <- self.off + 2;
x
let i16 = u16
let u32 self =
let x = Bytes.get_int32_le self.bs self.off in
self.off <- self.off + 4;
x
let i32 = u32
let u64 self =
let i = Bytes.get_int64_le self.bs self.off in
self.off <- 8 + self.off;
i
let i64 = u64
let bool self : bool =
let c = Bytes.get self.bs self.off in
self.off <- 1 + self.off;
Char.code c <> 0
let f32 (self:t) : float =
let i = i32 self in
Int32.float_of_bits i
let f64 (self:t) : float =
let i = i64 self in
Int64.float_of_bits i
let data_of ~size self : bytes =
let s = Bytes.sub self.bs self.off size in
self.off <- self.off + size;
s
let data self : bytes =
let size = uint self in
if Int64.compare size (Int64.of_int Sys.max_string_length) > 0 then
fail_ "string too large";
let size = Int64.to_int size in (* fits, because of previous test *)
data_of ~size self
let string self : string =
Bytes.unsafe_to_string (data self)
let[@inline] optional dec self : _ option =
let c = u8 self in
if Char.code c = 0 then None else Some (dec self)
end
module Encode = struct
type t = Buffer.t
let of_buffer buf : t = buf
type 'a enc = t -> 'a -> unit
(* no need to check for overflow below *)
external unsafe_chr : int -> char = "%identity"
let uint (self:t) (i:int64) : unit =
let module I = Int64 in
let i = ref i in
let continue = ref true in
while !continue do
let j = I.logand 0b0111_1111L !i in
if !i = j then (
continue := false;
let j = I.to_int j in
Buffer.add_char self (unsafe_chr j)
) else (
(* set bit 8 to [1] *)
let lsb = I.to_int (I.logor 0b1000_0000L j) in
let lsb = (unsafe_chr lsb) in
Buffer.add_char self lsb;
i := I.shift_right_logical !i 7;
)
done
let[@inline] int (self:t) i =
let open Int64 in
let ui = logxor (shift_left i 1) (shift_right i 63) in
uint self ui
let u8 self x = Buffer.add_char self x
let i8 = u8
let u16 self x = Buffer.add_int16_le self x
let i16 = u16
let u32 self x = Buffer.add_int32_le self x
let i32 = u32
let u64 self x = Buffer.add_int64_le self x
let i64 = u64
let bool self x = Buffer.add_char self (if x then Char.chr 1 else Char.chr 0)
let f64 (self:t) x = Buffer.add_int64_le self (Int64.bits_of_float x)
let data_of ~size self x =
if size <> Bytes.length x then failwith "invalid length for Encode.data_of";
Buffer.add_bytes self x
let data self x =
uint self (Int64.of_int (Bytes.length x));
Buffer.add_bytes self x
let string self x = data self (Bytes.unsafe_of_string x)
let[@inline] optional enc self x : unit =
match x with
| None -> u8 self (Char.chr 0)
| Some x ->
u8 self (Char.chr 1);
enc self x
end
module Pp = struct
type 'a t = Format.formatter -> 'a -> unit
type 'a iter = ('a -> unit) -> unit
let unit out () = Format.pp_print_string out "()"
let int8 out c = Format.fprintf out "%d" (Char.code c)
let int out x = Format.fprintf out "%d" x
let int32 out x = Format.fprintf out "%ld" x
let int64 out x = Format.fprintf out "%Ld" x
let float out x = Format.fprintf out "%h" x
let bool = Format.pp_print_bool
let string out x = Format.fprintf out "%S" x
let data out x = string out (Bytes.unsafe_to_string x)
let option ppelt out x = match x with
| None -> Format.fprintf out "None"
| Some x -> Format.fprintf out "(Some %a)" ppelt x
let array ppelt out x =
Format.fprintf out "[@[";
Array.iteri (fun i x ->
if i>0 then Format.fprintf out ";@ ";
ppelt out x)
x;
Format.fprintf out "@]]"
let iter ppelt out xs =
Format.fprintf out "[@[";
let i = ref 0 in
xs (fun x ->
if !i>0 then Format.fprintf out ",@ ";
incr i;
ppelt out x);
Format.fprintf out "@]]"
let list ppelt out l = iter ppelt out (fun f->List.iter f l)
end
let to_string (e:'a Encode.enc) (x:'a) =
let buf = Buffer.create 32 in
e buf x;
Buffer.contents buf
let of_bytes_exn ?(off=0) dec bs =
let i = {Decode.bs; off} in
dec i
let of_bytes ?off dec bs =
try Ok (of_bytes_exn ?off dec bs)
with Decode.Error e -> Error e
let of_string_exn dec s = of_bytes_exn dec (Bytes.unsafe_of_string s)
let of_string dec s = of_bytes dec (Bytes.unsafe_of_string s)
(*$inject
let to_s f x =
let buf = Buffer.create 32 in
let out = Encode.of_buffer buf in
f out x;
Buffer.contents buf
let of_s f x =
let i = {Decode.off=0; bs=Bytes.unsafe_of_string x} in
f i
*)
(*$= & ~printer:Int64.to_string
37L (of_s Decode.uint (to_s Encode.uint 37L))
42L (of_s Decode.uint (to_s Encode.uint 42L))
0L (of_s Decode.uint (to_s Encode.uint 0L))
105542252L (of_s Decode.uint (to_s Encode.uint 105542252L))
Int64.max_int (of_s Decode.uint (to_s Encode.uint Int64.max_int))
*)
(*$= & ~printer:Int64.to_string
37L (of_s Decode.int (to_s Encode.int 37L))
42L (of_s Decode.int (to_s Encode.int 42L))
0L (of_s Decode.int (to_s Encode.int 0L))
105542252L (of_s Decode.int (to_s Encode.int 105542252L))
Int64.max_int (of_s Decode.int (to_s Encode.int Int64.max_int))
Int64.min_int (of_s Decode.int (to_s Encode.int Int64.min_int))
(-1209433446454112432L) (of_s Decode.int (to_s Encode.int (-1209433446454112432L)))
(-3112855215860398414L) (of_s Decode.int (to_s Encode.int (-3112855215860398414L)))
*)
(*$=
1 (let s = to_s Encode.int (-1209433446454112432L) in 0x1 land (Char.code s.[0]))
*)
(*$Q
Q.(int64) (fun s -> \
s = (of_s Decode.uint (to_s Encode.uint s)))
*)
(*$Q
Q.(int64) (fun s -> \
s = (of_s Decode.int (to_s Encode.int s)))
*)
(* TODO: some tests with qtest *)
end
module ID = struct
type t = int32
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
Bare.Decode.i32 dec
let encode (enc: Bare.Encode.t) (self: t) : unit =
Bare.Encode.i32 enc self
let pp out (self:t) : unit =
Bare.Pp.int32 out self
end
module Lit = struct
type t = ID.t
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
ID.decode dec
let encode (enc: Bare.Encode.t) (self: t) : unit =
ID.encode enc self
let pp out (self:t) : unit =
ID.pp out self
end
module Clause = struct
type t = {
lits: Lit.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let lits =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> Lit.decode dec)) in
{lits; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
(let arr = self.lits in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> Lit.encode enc xi) arr);
end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "lits=%a;@ " (Bare.Pp.array Lit.pp) x.lits;
Format.fprintf out "@]}";
end) out self
end
module Step_input = struct
type t = {
c: Clause.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let c = Clause.decode dec in {c; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin Clause.encode enc self.c; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "c=%a;@ " Clause.pp x.c;
Format.fprintf out "@]}";
end) out self
end
module Step_rup = struct
type t = {
res: Clause.t;
hyps: ID.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let res = Clause.decode dec in
let hyps =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
{res; hyps; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
Clause.encode enc self.res;
(let arr = self.hyps in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> ID.encode enc xi) arr);
end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "res=%a;@ " Clause.pp x.res;
Format.fprintf out "hyps=%a;@ " (Bare.Pp.array ID.pp) x.hyps;
Format.fprintf out "@]}";
end) out self
end
module Step_bridge_lit_expr = struct
type t = {
lit: Lit.t;
expr: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let lit = Lit.decode dec in let expr = ID.decode dec in {lit; expr; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin Lit.encode enc self.lit; ID.encode enc self.expr; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "lit=%a;@ " Lit.pp x.lit;
Format.fprintf out "expr=%a;@ " ID.pp x.expr;
Format.fprintf out "@]}";
end) out self
end
module Step_cc = struct
type t = {
eqns: ID.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let eqns =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
{eqns; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
(let arr = self.eqns in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> ID.encode enc xi) arr);
end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "eqns=%a;@ " (Bare.Pp.array ID.pp) x.eqns;
Format.fprintf out "@]}";
end) out self
end
module Step_preprocess = struct
type t = {
t: ID.t;
u: ID.t;
using: ID.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let t = ID.decode dec in
let u = ID.decode dec in
let using =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
{t; u; using; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
ID.encode enc self.t;
ID.encode enc self.u;
(let arr = self.using in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> ID.encode enc xi) arr);
end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "t=%a;@ " ID.pp x.t;
Format.fprintf out "u=%a;@ " ID.pp x.u;
Format.fprintf out "using=%a;@ " (Bare.Pp.array ID.pp) x.using;
Format.fprintf out "@]}";
end) out self
end
module Fun_decl = struct
type t = {
f: string;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let f = Bare.Decode.string dec in {f; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin Bare.Encode.string enc self.f; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "f=%a;@ " Bare.Pp.string x.f;
Format.fprintf out "@]}";
end) out self
end
module Expr_bool = struct
type t = {
b: bool;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let b = Bare.Decode.bool dec in {b; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin Bare.Encode.bool enc self.b; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "b=%a;@ " Bare.Pp.bool x.b;
Format.fprintf out "@]}";
end) out self
end
module Expr_if = struct
type t = {
cond: ID.t;
then_: ID.t;
else_: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let cond = ID.decode dec in
let then_ = ID.decode dec in
let else_ = ID.decode dec in
{cond; then_; else_; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
ID.encode enc self.cond;
ID.encode enc self.then_;
ID.encode enc self.else_;
end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "cond=%a;@ " ID.pp x.cond;
Format.fprintf out "then_=%a;@ " ID.pp x.then_;
Format.fprintf out "else_=%a;@ " ID.pp x.else_;
Format.fprintf out "@]}";
end) out self
end
module Expr_not = struct
type t = {
f: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let f = ID.decode dec in {f; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin ID.encode enc self.f; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "f=%a;@ " ID.pp x.f;
Format.fprintf out "@]}";
end) out self
end
module Expr_eq = struct
type t = {
lhs: ID.t;
rhs: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let lhs = ID.decode dec in let rhs = ID.decode dec in {lhs; rhs; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin ID.encode enc self.lhs; ID.encode enc self.rhs; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "lhs=%a;@ " ID.pp x.lhs;
Format.fprintf out "rhs=%a;@ " ID.pp x.rhs;
Format.fprintf out "@]}";
end) out self
end
module Expr_app = struct
type t = {
f: ID.t;
args: ID.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let f = ID.decode dec in
let args =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
{f; args; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
ID.encode enc self.f;
(let arr = self.args in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> ID.encode enc xi) arr);
end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "f=%a;@ " ID.pp x.f;
Format.fprintf out "args=%a;@ " (Bare.Pp.array ID.pp) x.args;
Format.fprintf out "@]}";
end) out self
end
module Step_view = struct
type t =
| Step_input of Step_input.t
| Step_rup of Step_rup.t
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
| Step_cc of Step_cc.t
| Step_preprocess of Step_preprocess.t
| Fun_decl of Fun_decl.t
| Expr_bool of Expr_bool.t
| Expr_if of Expr_if.t
| Expr_not of Expr_not.t
| Expr_eq of Expr_eq.t
| Expr_app of Expr_app.t
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let tag = Bare.Decode.uint dec in
match tag with
| 0L -> Step_input (Step_input.decode dec)
| 1L -> Step_rup (Step_rup.decode dec)
| 2L -> Step_bridge_lit_expr (Step_bridge_lit_expr.decode dec)
| 3L -> Step_cc (Step_cc.decode dec)
| 4L -> Step_preprocess (Step_preprocess.decode dec)
| 5L -> Fun_decl (Fun_decl.decode dec)
| 6L -> Expr_bool (Expr_bool.decode dec)
| 7L -> Expr_if (Expr_if.decode dec)
| 8L -> Expr_not (Expr_not.decode dec)
| 9L -> Expr_eq (Expr_eq.decode dec)
| 10L -> Expr_app (Expr_app.decode dec)
| _ -> raise (Bare.Decode.Error(Printf.sprintf "unknown union tag Step_view.t: %Ld" tag))
let encode (enc: Bare.Encode.t) (self: t) : unit =
match self with
| Step_input x ->
Bare.Encode.uint enc 0L;
Step_input.encode enc x
| Step_rup x ->
Bare.Encode.uint enc 1L;
Step_rup.encode enc x
| Step_bridge_lit_expr x ->
Bare.Encode.uint enc 2L;
Step_bridge_lit_expr.encode enc x
| Step_cc x ->
Bare.Encode.uint enc 3L;
Step_cc.encode enc x
| Step_preprocess x ->
Bare.Encode.uint enc 4L;
Step_preprocess.encode enc x
| Fun_decl x ->
Bare.Encode.uint enc 5L;
Fun_decl.encode enc x
| Expr_bool x ->
Bare.Encode.uint enc 6L;
Expr_bool.encode enc x
| Expr_if x ->
Bare.Encode.uint enc 7L;
Expr_if.encode enc x
| Expr_not x ->
Bare.Encode.uint enc 8L;
Expr_not.encode enc x
| Expr_eq x ->
Bare.Encode.uint enc 9L;
Expr_eq.encode enc x
| Expr_app x ->
Bare.Encode.uint enc 10L;
Expr_app.encode enc x
let pp out (self:t) : unit =
match self with
| Step_input x ->
Format.fprintf out "(@[Step_input@ %a@])" Step_input.pp x
| Step_rup x ->
Format.fprintf out "(@[Step_rup@ %a@])" Step_rup.pp x
| Step_bridge_lit_expr x ->
Format.fprintf out "(@[Step_bridge_lit_expr@ %a@])" Step_bridge_lit_expr.pp x
| Step_cc x ->
Format.fprintf out "(@[Step_cc@ %a@])" Step_cc.pp x
| Step_preprocess x ->
Format.fprintf out "(@[Step_preprocess@ %a@])" Step_preprocess.pp x
| Fun_decl x ->
Format.fprintf out "(@[Fun_decl@ %a@])" Fun_decl.pp x
| Expr_bool x ->
Format.fprintf out "(@[Expr_bool@ %a@])" Expr_bool.pp x
| Expr_if x ->
Format.fprintf out "(@[Expr_if@ %a@])" Expr_if.pp x
| Expr_not x ->
Format.fprintf out "(@[Expr_not@ %a@])" Expr_not.pp x
| Expr_eq x ->
Format.fprintf out "(@[Expr_eq@ %a@])" Expr_eq.pp x
| Expr_app x ->
Format.fprintf out "(@[Expr_app@ %a@])" Expr_app.pp x
end
module Step = struct
type t = {
id: ID.t;
view: Step_view.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let id = ID.decode dec in let view = Step_view.decode dec in {id; view; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin ID.encode enc self.id; Step_view.encode enc self.view; end
let pp out (self:t) : unit =
(fun out x ->
begin
Format.fprintf out "{@[ ";
Format.fprintf out "id=%a;@ " ID.pp x.id;
Format.fprintf out "view=%a;@ " Step_view.pp x.view;
Format.fprintf out "@]}";
end) out self
end

3
src/proof-trace/sidekick_base_proof_trace.ml
View file

@ -6,3 +6,6 @@
proof later. *)
module Proof_ser = Proof_ser
module Storage = Storage
let iter_steps_backward = Storage.iter_steps_backward