Merge pull request #808 from ejgallego/hash_proof

[petanque] Hash proof states instead of system states

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_...
 ----------------------------------------------------

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

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
 

examples/ltac2_simple.v

@@ -3,4 +3,3 @@ From Ltac2 Require Import Ltac2.
 Goal True /\ True.
   split; exact I.
 Qed.
-

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. *)

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

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_

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

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

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

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