simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(const): remove opaque_to_cc

Browse source
This commit is contained in:
Simon Cruanes 2022-09-19 21:33:25 -04:00
parent d58c81e83f
commit 1c07b027ef
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
4 changed files with 0 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/core-logic/const.ml
View file

@ -6,7 +6,6 @@ module type DYN_OPS = sig
val pp : view Fmt.printer val pp : view Fmt.printer
val equal : view -> view -> bool val equal : view -> view -> bool
val hash : view -> int val hash : view -> int
val opaque_to_cc : view -> bool
end end
type ops = (module DYN_OPS) type ops = (module DYN_OPS)

1
src/core-logic/const.mli
View file

@ -10,7 +10,6 @@ module type DYN_OPS = sig
val pp : view Fmt.printer val pp : view Fmt.printer
val equal : view -> view -> bool val equal : view -> view -> bool
val hash : view -> int val hash : view -> int
val opaque_to_cc : view -> bool
end end
type ops = (module DYN_OPS) type ops = (module DYN_OPS)

5
src/core-logic/types_.ml
View file

@ -11,11 +11,6 @@ module type DYN_CONST_OPS = sig
val hash : const_view -> int val hash : const_view -> int
(** Hash constant *) (** Hash constant *)
val opaque_to_cc : const_view -> bool
(** If true, congruence closure will not apply for applications of this
constant. In other words, [c t1…tn] will appear to the congruence
closure as a single opaque term with no subterms. *)
end end
type const_ops = (module DYN_CONST_OPS) type const_ops = (module DYN_CONST_OPS)

4
src/core/default_cc_view.ml
View file

@ -9,10 +9,6 @@ let view_as_cc (t : Term.t) : _ CC_view.t =
| Term.E_const { Const.c_view = T_builtins.C_ite; _ }, [ _ty; a; b; c ] -> | Term.E_const { Const.c_view = T_builtins.C_ite; _ }, [ _ty; a; b; c ] ->
View.If (a, b, c) View.If (a, b, c)
| Term.E_const { Const.c_view = T_builtins.C_not; _ }, [ a ] -> View.Not a | Term.E_const { Const.c_view = T_builtins.C_not; _ }, [ a ] -> View.Not a
| Term.E_const { Const.c_ops = (module OP); c_view; _ }, _
when OP.opaque_to_cc c_view ->
(* this constant hides its arguments *)
View.Opaque t
| _ -> | _ ->
(match Term.view t with (match Term.view t with
| Term.E_app (f, a) -> View.App_ho (f, a) | Term.E_app (f, a) -> View.App_ho (f, a)