From c2b8d93cf49554bb1ac0c6237c162e82c1406df6 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 21 Oct 2021 23:28:53 -0400 Subject: [PATCH] refactor proof storage --- src/base/Base_types.ml | 1 + src/base/Proof.ml | 99 +-- src/proof-trace-dump/proof_trace_dump.ml | 7 +- src/proof-trace/Storage.ml | 41 + src/proof-trace/Storage.mli | 8 + src/proof-trace/proof_ser.bare | 12 + src/proof-trace/proof_ser.ml | 86 ++- src/proof-trace/sidekick_base_proof_ser.ml | 762 ------------------- src/proof-trace/sidekick_base_proof_trace.ml | 3 + 9 files changed, 182 insertions(+), 837 deletions(-) create mode 100644 src/proof-trace/Storage.ml create mode 100644 src/proof-trace/Storage.mli delete mode 100644 src/proof-trace/sidekick_base_proof_ser.ml diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index 1f1c49c0..e77598c2 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -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 diff --git a/src/base/Proof.ml b/src/base/Proof.ml index bd7011a3..c1a19b18 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -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 diff --git a/src/proof-trace-dump/proof_trace_dump.ml b/src/proof-trace-dump/proof_trace_dump.ml index 68741091..352f02a6 100644 --- a/src/proof-trace-dump/proof_trace_dump.ml +++ b/src/proof-trace-dump/proof_trace_dump.ml @@ -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 diff --git a/src/proof-trace/Storage.ml b/src/proof-trace/Storage.ml new file mode 100644 index 00000000..74f869c6 --- /dev/null +++ b/src/proof-trace/Storage.ml @@ -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 diff --git a/src/proof-trace/Storage.mli b/src/proof-trace/Storage.mli new file mode 100644 index 00000000..4cc8b753 --- /dev/null +++ b/src/proof-trace/Storage.mli @@ -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 diff --git a/src/proof-trace/proof_ser.bare b/src/proof-trace/proof_ser.bare index 4dea2005..fcbb087a 100644 --- a/src/proof-trace/proof_ser.bare +++ b/src/proof-trace/proof_ser.bare @@ -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 diff --git a/src/proof-trace/proof_ser.ml b/src/proof-trace/proof_ser.ml index 6b187786..efaa29c0 100644 --- a/src/proof-trace/proof_ser.ml +++ b/src/proof-trace/proof_ser.ml @@ -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 -> diff --git a/src/proof-trace/sidekick_base_proof_ser.ml b/src/proof-trace/sidekick_base_proof_ser.ml deleted file mode 100644 index 6b187786..00000000 --- a/src/proof-trace/sidekick_base_proof_ser.ml +++ /dev/null @@ -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 - - diff --git a/src/proof-trace/sidekick_base_proof_trace.ml b/src/proof-trace/sidekick_base_proof_trace.ml index 3c2d90a4..67773fe8 100644 --- a/src/proof-trace/sidekick_base_proof_trace.ml +++ b/src/proof-trace/sidekick_base_proof_trace.ml @@ -6,3 +6,6 @@ proof later. *) module Proof_ser = Proof_ser +module Storage = Storage + +let iter_steps_backward = Storage.iter_steps_backward