From 7349a494cdec0d47dd72042dc3fbb757504df2e3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 17 Jul 2024 16:54:09 +0200 Subject: [PATCH] [petanque] Hash proof states instead of system states --- CHANGES.md | 2 ++ coq/state.ml | 7 ++++++ coq/state.mli | 2 ++ examples/ltac2_simple.v | 1 - petanque/agent.ml | 30 +++++++++++++++++++++++++- petanque/agent.mli | 18 +++++++++++++--- petanque/json/interp.ml | 4 ++++ petanque/json/protocol.ml | 39 ++++++++++++++++++++++++++++++++++ petanque/json_shell/client.ml | 8 +++++++ petanque/json_shell/client.mli | 6 ++++++ petanque/test/json_api.ml | 3 +++ 11 files changed, 115 insertions(+), 5 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 801654be..22326677 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -66,6 +66,8 @@ configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, #779) + - [petanque] New methods to hash proof states; use proof state hash + by default in petanque agent (@ejgallego, @gbdrt, #808) # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_... ---------------------------------------------------- diff --git a/coq/state.ml b/coq/state.ml index 030a3d5e..e30c2dd3 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -78,6 +78,13 @@ module Proof = struct type t = Vernacstate.LemmaStack.t let to_coq x = x + let equal x y = x == y + + (* OCaml's defaults are 10, 100, we use this as to give best precision for + petanque-like users *) + let hash x = + let meaningful, total = (128, 256) in + Hashtbl.hash_param meaningful total x end let lemmas ~st = st.Vernacstate.interp.lemmas diff --git a/coq/state.mli b/coq/state.mli index dd9075b1..37dc3d4a 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -10,6 +10,8 @@ val parsing : st:t -> Pcoq.frozen_t module Proof : sig type t + val equal : t -> t -> bool + val hash : t -> int val to_coq : t -> Vernacstate.LemmaStack.t end diff --git a/examples/ltac2_simple.v b/examples/ltac2_simple.v index d8937f45..011f4ea6 100644 --- a/examples/ltac2_simple.v +++ b/examples/ltac2_simple.v @@ -3,4 +3,3 @@ From Ltac2 Require Import Ltac2. Goal True /\ True. split; exact I. Qed. - diff --git a/petanque/agent.ml b/petanque/agent.ml index c2801d35..7a74b241 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -30,6 +30,19 @@ module State = struct fun st1 st2 -> let st1, st2 = (Coq.State.lemmas ~st:st1, Coq.State.lemmas ~st:st2) in Option.equal Coq.Goals.Equality.equal_goals st1 st2 + + module Proof = struct + type t = Coq.State.Proof.t + + let equal ?(kind = Inspect.Physical) = + match kind with + | Physical -> Coq.State.Proof.equal + | Goals -> Coq.Goals.Equality.equal_goals + + let hash = Coq.State.Proof.hash + end + + let lemmas st = Coq.State.lemmas ~st end (** Petanque errors *) @@ -133,6 +146,21 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t = let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } = List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack +(* At some point we want to return both hashes *) +module Hash_kind = struct + type t = + | Full + | Proof + [@@warning "-37"] + + let hash ~kind st = + match kind with + | Full -> Some (State.hash st) + | Proof -> Option.map State.Proof.hash (State.lemmas st) +end + +let hash_mode = Hash_kind.Proof + let analyze_after_run ~hash st = let proof_finished = let goals = Fleche.Info.Goals.get_goals_unit ~st in @@ -141,7 +169,7 @@ let analyze_after_run ~hash st = | Some goals when proof_finished goals -> true | _ -> false in - let hash = if hash then Some (State.hash st) else None in + let hash = if hash then Hash_kind.hash ~kind:hash_mode st else None in Run_result.{ st; hash; proof_finished } (* Would be nice to keep this in sync with the type annotations. *) diff --git a/petanque/agent.mli b/petanque/agent.mli index 06395f46..37213703 100644 --- a/petanque/agent.mli +++ b/petanque/agent.mli @@ -6,14 +6,13 @@ (************************************************************************) (** Petanque.Agent *) - module State : sig + (** Full state of Coq *) type t val name : string - (** Fleche-based Coq state hash; it has been designed for interactive use, so - please report back *) + (** OCaml poly Coq state hash; tuned for interactive edition. *) val hash : t -> int module Inspect : sig @@ -28,6 +27,18 @@ module State : sig (** [equal ?kind st1 st2] [kind] defaults to [Inspect.Physical] *) val equal : ?kind:Inspect.t -> t -> t -> bool + + module Proof : sig + (** OCaml poly hash for Coq proof state. *) + type t + + (** [equal ?kind st1 st2] [kind] defaults to [Inspect.Physical] *) + val equal : ?kind:Inspect.t -> t -> t -> bool + + val hash : t -> int + end + + val lemmas : t -> Proof.t option end (** Petanque errors *) @@ -62,6 +73,7 @@ module Run_result : sig type 'a t = { st : 'a ; hash : int option [@default None] + (** [State.Proof.hash st] if enabled / proof is open. *) ; proof_finished : bool } end diff --git a/petanque/json/interp.ml b/petanque/json/interp.ml index 8570cd03..02e329ea 100644 --- a/petanque/json/interp.ml +++ b/petanque/json/interp.ml @@ -65,4 +65,8 @@ let handle_request ~(do_handle : 'a handle) ~unhandled ~token ~method_ ~params = do_handle ~token (do_request (module StateEqual) ~params) | s when String.equal StateHash.method_ s -> do_handle ~token (do_request (module StateHash) ~params) + | s when String.equal StateProofEqual.method_ s -> + do_handle ~token (do_request (module StateProofEqual) ~params) + | s when String.equal StateProofHash.method_ s -> + do_handle ~token (do_request (module StateProofHash) ~params) | _ -> unhandled ~token ~method_ diff --git a/petanque/json/protocol.ml b/petanque/json/protocol.ml index 0cd45c7c..8494146e 100644 --- a/petanque/json/protocol.ml +++ b/petanque/json/protocol.ml @@ -236,3 +236,42 @@ module StateHash = struct HType.Immediate (fun ~token:_ { Params.st } -> Ok (Agent.State.hash st)) end end + +module StateProofEqual = struct + let method_ = "petanque/state/proof/equal" + + module Params = StateEqual.Params + module Response = StateEqual.Response + + module Handler = struct + module Params = StateEqual.Handler.Params + module Response = Response + + let handler = + HType.Immediate + (fun ~token:_ { Params.kind; st1; st2 } -> + let pst1, pst2 = Agent.State.(lemmas st1, lemmas st2) in + Ok (Option.equal (Agent.State.Proof.equal ?kind) pst1 pst2)) + end +end + +module StateProofHash = struct + let method_ = "petanque/state/proof/hash" + + module Params = StateHash.Params + + module Response = struct + type t = int option [@@deriving yojson] + end + + module Handler = struct + module Params = StateHash.Handler.Params + module Response = Response + + let handler = + HType.Immediate + (fun ~token:_ { Params.st } -> + let pst = Agent.State.lemmas st in + Ok (Option.map Agent.State.Proof.hash pst)) + end +end diff --git a/petanque/json_shell/client.ml b/petanque/json_shell/client.ml index 7efd6394..8f3c553c 100644 --- a/petanque/json_shell/client.ml +++ b/petanque/json_shell/client.ml @@ -98,4 +98,12 @@ module S (C : Chans) = struct let state_hash = let module M = Wrap (StateHash) (C) in M.call + + let state_proof_equal = + let module M = Wrap (StateProofEqual) (C) in + M.call + + let state_proof_hash = + let module M = Wrap (StateProofHash) (C) in + M.call end diff --git a/petanque/json_shell/client.mli b/petanque/json_shell/client.mli index f3501a2d..daa3c543 100644 --- a/petanque/json_shell/client.mli +++ b/petanque/json_shell/client.mli @@ -23,4 +23,10 @@ module S (C : Chans) : sig StateEqual.Params.t -> (StateEqual.Response.t, string) result val state_hash : StateHash.Params.t -> (StateHash.Response.t, string) result + + val state_proof_equal : + StateProofEqual.Params.t -> (StateProofEqual.Response.t, string) result + + val state_proof_hash : + StateProofHash.Params.t -> (StateProofHash.Response.t, string) result end diff --git a/petanque/test/json_api.ml b/petanque/test/json_api.ml index 91052b71..5045144b 100644 --- a/petanque/test/json_api.ml +++ b/petanque/test/json_api.ml @@ -59,9 +59,12 @@ let run (ic, oc) = Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_premise) premises)); let* st = S.run { opts = None; st; tac = "induction l." } in let* h1 = S.state_hash { st = st.st } in + let* h1_p = S.state_proof_hash { st = st.st } in let* st = r ~st ~tac:"idtac." in let* h2 = S.state_hash { st = st.st } in + let* h2_p = S.state_proof_hash { st = st.st } in assert (Int.equal h1 h2); + assert (Option.equal Int.equal h1_p h2_p); let* st = r ~st ~tac:"-" in let* st = r ~st ~tac:"reflexivity." in let* h3 = S.state_hash { st = st.st } in