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

refactor(simplify): use new proof trace from sidekick.proof

Browse source
This commit is contained in:
Simon Cruanes 2022-10-12 12:20:50 -04:00
parent 4b359a40f2
commit 8a3e7528c3
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 14 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/simplify/dune
View file

@ -2,5 +2,5 @@
(name Sidekick_simplify)
(public_name sidekick.simplify)
(synopsis "Simplifier")
(libraries containers iter sidekick.core sidekick.util)
(libraries containers iter sidekick.core sidekick.util sidekick.proof)
(flags :standard -w +32 -open Sidekick_util))

14
src/simplify/sidekick_simplify.ml
View file

@ -2,17 +2,18 @@ open Sidekick_core
type t = {
tst: Term.store;
proof: Proof_trace.t;
proof: Sidekick_proof.Tracer.t;
mutable hooks: hook list;
(* store [t --> u by step_ids] in the cache.
We use a bag for the proof steps because it gives us structural
sharing of subproofs. *)
cache: (Term.t * Proof_step.id Bag.t) Term.Tbl.t;
cache: (Term.t * Sidekick_proof.Step.id Bag.t) Term.Tbl.t;
}
and hook = t -> Term.t -> (Term.t * Proof_step.id Iter.t) option
and hook = t -> Term.t -> (Term.t * Sidekick_proof.Step.id Iter.t) option
let create tst ~proof : t =
let proof = (proof : #Sidekick_proof.Tracer.t :> Sidekick_proof.Tracer.t) in
{ tst; proof; hooks = []; cache = Term.Tbl.create 32 }
let[@inline] tst self = self.tst
@ -20,7 +21,8 @@ let[@inline] proof self = self.proof
let add_hook self f = self.hooks <- f :: self.hooks
let clear self = Term.Tbl.clear self.cache
let normalize (self : t) (t : Term.t) : (Term.t * Proof_step.id) option =
let normalize (self : t) (t : Term.t) : (Term.t * Sidekick_proof.Step.id) option
=
(* compute and cache normal form of [t] *)
let rec loop t : Term.t * _ Bag.t =
match Term.Tbl.find self.cache t with
@ -67,8 +69,8 @@ let normalize (self : t) (t : Term.t) : (Term.t * Proof_step.id) option =
else (
(* proof: [sub_proofs |- t=u] by CC + subproof *)
let step =
Proof_trace.add_step self.proof @@ fun () ->
Proof_core.lemma_preprocess t u ~using:(Bag.to_list pr_u)
Sidekick_proof.Tracer.add_step self.proof @@ fun () ->
Sidekick_proof.Core_rules.lemma_preprocess t u ~using:(Bag.to_list pr_u)
in
Some (u, step)
)

10
src/simplify/sidekick_simplify.mli
View file

@ -6,16 +6,16 @@ type t
val tst : t -> Term.store
val create : Term.store -> proof:Proof_trace.t -> t
val create : Term.store -> proof:#Sidekick_proof.Tracer.t -> t
(** Create a simplifier *)
val clear : t -> unit
(** Reset internal cache, etc. *)
val proof : t -> Proof_trace.t
val proof : t -> Sidekick_proof.Tracer.t
(** Access proof *)
type hook = t -> Term.t -> (Term.t * Proof_step.id Iter.t) option
type hook = t -> Term.t -> (Term.t * Sidekick_proof.Step.id Iter.t) option
(** Given a Term.t, try to simplify it. Return [None] if it didn't change.
A simple example could be a hook that takes a Term.t [t],
@ -28,12 +28,12 @@ type hook = t -> Term.t -> (Term.t * Proof_step.id Iter.t) option
val add_hook : t -> hook -> unit
val normalize : t -> Term.t -> (Term.t * Proof_step.id) option
val normalize : t -> Term.t -> (Term.t * Sidekick_proof.Step.id) option
(** Normalize a Term.t using all the hooks. This performs
a fixpoint, i.e. it only stops when no hook applies anywhere inside
the Term.t. *)
val normalize_t : t -> Term.t -> Term.t * Proof_step.id option
val normalize_t : t -> Term.t -> Term.t * Sidekick_proof.Step.id option
(** Normalize a Term.t using all the hooks, along with a proof that the
simplification is correct.
returns [t, ø] if no simplification occurred. *)