simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(cc): continue de-functorizing

Browse source
This commit is contained in:
Simon Cruanes 2022-07-29 00:15:05 -04:00
parent 464bc66474
commit c09650db51
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 22 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/cc/Sidekick_cc.ml
View file

@ -3,7 +3,20 @@ module View = View
module type ARG = Sigs.ARG module type ARG = Sigs.ARG
module type S = Sigs.S module type S = Sigs.S
module type DYN_MONOID_PLUGIN = Sigs.DYN_MONOID_PLUGIN
module type MONOID_PLUGIN_ARG = Sigs.MONOID_PLUGIN_ARG module type MONOID_PLUGIN_ARG = Sigs.MONOID_PLUGIN_ARG
module type MONOID_PLUGIN_BUILDER = Sigs.MONOID_PLUGIN_BUILDER module type MONOID_PLUGIN_BUILDER = Sigs.MONOID_PLUGIN_BUILDER
module Make (A : ARG) : S = Core_cc.Make (A) module Make (A : ARG) : S = Core_cc.Make (A)
module Base : S = Make (struct
let view_as_cc (t : Term.t) : _ View.t =
let f, args = Term.unfold_app t in
match Term.view f, args with
| _, [ _; t; u ] when Term.is_eq f -> View.Eq (t, u)
| _ ->
(match Term.view t with
| Term.E_app (f, a) -> View.App_ho (f, a)
| Term.E_const c -> View.App_fun (c, Iter.empty)
| _ -> View.Opaque t)
end)

28
src/cc/Sidekick_cc.mli
View file

@ -4,26 +4,12 @@ open Sidekick_core
module View = View module View = View
module type ARG = Sigs.ARG module type ARG = Sigs.ARG
module type S = Sigs.S
module type S = sig module type DYN_MONOID_PLUGIN = Sigs.DYN_MONOID_PLUGIN
include Sigs.S module type MONOID_PLUGIN_ARG = Sigs.MONOID_PLUGIN_ARG
module type MONOID_PLUGIN_BUILDER = Sigs.MONOID_PLUGIN_BUILDER
val create :
?stat:Stat.t -> ?size:[ `Small | `Big ] -> Term.store -> Proof_trace.t -> t
(** Create a new congruence closure.
@param term_store used to be able to create new terms. All terms
interacting with this congruence closure must belong in this term state
as well. *)
(**/**)
module Debug_ : sig
val pp : t Fmt.printer
(** Print the whole CC *)
end
(**/**)
end
module Make (_ : ARG) : S module Make (_ : ARG) : S
module Base : S
(** Basic implementation following terms' shape *)

5
src/cc/plugin/sidekick_cc_plugin.ml
View file

@ -1,3 +1,4 @@
open Sidekick_core
open Sidekick_cc open Sidekick_cc
module type EXTENDED_PLUGIN_BUILDER = sig module type EXTENDED_PLUGIN_BUILDER = sig
@ -23,8 +24,6 @@ module Make (M : MONOID_PLUGIN_ARG) :
module Cls_tbl = Backtrackable_tbl.Make (E_node) module Cls_tbl = Backtrackable_tbl.Make (E_node)
module Expl = CC.Expl module Expl = CC.Expl
type term = CC.term
module type DYN_PL_FOR_M = DYN_MONOID_PLUGIN with module M = M module type DYN_PL_FOR_M = DYN_MONOID_PLUGIN with module M = M
type t = (module DYN_PL_FOR_M) type t = (module DYN_PL_FOR_M)
@ -63,7 +62,7 @@ module Make (M : MONOID_PLUGIN_ARG) :
else else
None None
let on_new_term cc n (t : term) : CC.Handler_action.t list = let on_new_term cc n (t : Term.t) : CC.Handler_action.t list =
(*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*) (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*)
let acts = ref [] in let acts = ref [] in
let maybe_m, l = M.of_term cc n t in let maybe_m, l = M.of_term cc n t in