From edb3e413b71a1e0ef274b4fb2d9b00aec0b298d3 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Wed, 9 Jun 2021 16:57:18 +0200
Subject: [PATCH] Extend Nodes.ml with conversion utilities
---
src_colibri2/core/structures/nodes.ml | 163 +++++++++++++------------
src_colibri2/core/structures/nodes.mli | 23 ++--
src_colibri2/theories/FP/float32.ml | 6 +-
3 files changed, 102 insertions(+), 90 deletions(-)
diff --git a/src_colibri2/core/structures/nodes.ml b/src_colibri2/core/structures/nodes.ml
index 5e6239f6a..f6208b8e0 100644
--- a/src_colibri2/core/structures/nodes.ml
+++ b/src_colibri2/core/structures/nodes.ml
@@ -29,8 +29,8 @@ exception AlreadyRedirected
let debug_create = Debug.register_info_flag
- ~desc:"for the core solver class creation information"
- "index"
+ ~desc:"for the core solver class creation information"
+ "index"
module ThTermKind = Keys.Make_key(struct end)
module ValueKind = Keys.Make_key(struct end)
@@ -226,7 +226,7 @@ module RegisterThTerm (D:ThTerm) : RegisteredThTerm with type s = D.t = struct
let sem : t -> D.t =
fun (Node.ThTerm(_,sem,v)) ->
- let Poly.Eq = ThTermKind.Eq.coerce_type sem D.key in v
+ let Poly.Eq = ThTermKind.Eq.coerce_type sem D.key in v
let thterm: t -> ThTerm.t = fun x -> x
@@ -257,9 +257,9 @@ module Value = struct
let value : type a. a ValueKind.t -> t -> a option =
fun value (Node.Value(_,value',v)) ->
- match ValueKind.Eq.eq_type value value' with
- | Poly.Neq -> None
- | Poly.Eq -> Some v
+ match ValueKind.Eq.eq_type value value' with
+ | Poly.Neq -> None
+ | Poly.Eq -> Some v
type kind =
| Value: 'a ValueKind.t * 'a -> kind
@@ -286,10 +286,14 @@ module type RegisteredValue = sig
(** Return the value from a nodevalue *)
val nodevalue: t -> Value.t
+
val of_nodevalue: Value.t -> t option
+ val of_value: s -> t
+
val coerce_nodevalue: Value.t -> t
+ val coerce_value: Value.t -> s
end
@@ -310,78 +314,81 @@ module RegisterValue (D:Value) : RegisteredValue with type s = D.t = struct
module All = struct
- module V = D
- module HC = Hashcons.MakeTag(struct
- open Node
- type t = nodevalue
-
- let next_tag = Node.next_tag
- let incr_tag = Node.incr_tag
-
- let equal: t -> t -> bool = fun a b ->
- match a, b with
- | Value(_,valuea,va), Value(_,valueb,vb) ->
- match ValueKind.Eq.coerce_type valuea D.key,
- ValueKind.Eq.coerce_type valueb D.key with
- | Poly.Eq, Poly.Eq -> D.equal va vb
-
- let hash: t -> int = fun a ->
- match a with
- | Value(_,valuea,va) ->
- let Poly.Eq = ValueKind.Eq.coerce_type valuea D.key in
- (D.hash va)
-
- let set_tag: int -> t -> t = fun tag x ->
- match x with
- | Value(_,value,v) -> Value(tag,value,v)
-
- let tag: t -> int = function
- | Value(tag,_,_) -> tag
-
- let pp fmt x =
- Format.pp_print_char fmt '@';
- Format.pp_print_string fmt (Simple_vector.get names (tag x))
- end)
-
- include HC
-
- type s = D.t
- let key = D.key
-
- let tag: t -> int = function
- | Node.Value(tag,_,_) -> tag
-
- let index ?(basename="") v =
- let node =
- HC.hashcons2
- (fun tag value v -> Node.Value(tag,value,v))
- D.key v in
- let i = tag node in
- Simple_vector.inc_size (i+1) Node.names;
- begin
- if Simple_vector.is_uninitialized Node.names i then
- let s = Strings.find_new_name Node.used_names basename in
- Debug.dprintf3 debug_create "[Egraph] @[@@%s is %a@]"
- s D.pp v;
- Simple_vector.set Node.names i s
- end;
- node
-
- let node = Node.of_nodevalue
-
- let value : t -> D.t = function
- | Node.Value(_,value,v) ->
- let Poly.Eq = ValueKind.Eq.coerce_type value D.key in v
-
- let nodevalue: t -> Value.t = fun x -> x
-
- let of_nodevalue: Value.t -> t option = function
- | Node.Value(_,value',_) as v when ValueKind.equal value' D.key -> Some v
- | _ -> None
-
- let coerce_nodevalue: Value.t -> t = function
- | Node.Value(_,value',_) as v -> assert (ValueKind.equal value' D.key); v
-
+ module V = D
+ module HC = Hashcons.MakeTag(struct
+ open Node
+ type t = nodevalue
+
+ let next_tag = Node.next_tag
+ let incr_tag = Node.incr_tag
+
+ let equal: t -> t -> bool = fun a b ->
+ match a, b with
+ | Value(_,valuea,va), Value(_,valueb,vb) ->
+ match ValueKind.Eq.coerce_type valuea D.key,
+ ValueKind.Eq.coerce_type valueb D.key with
+ | Poly.Eq, Poly.Eq -> D.equal va vb
+
+ let hash: t -> int = fun a ->
+ match a with
+ | Value(_,valuea,va) ->
+ let Poly.Eq = ValueKind.Eq.coerce_type valuea D.key in
+ (D.hash va)
+
+ let set_tag: int -> t -> t = fun tag x ->
+ match x with
+ | Value(_,value,v) -> Value(tag,value,v)
+
+ let tag: t -> int = function
+ | Value(tag,_,_) -> tag
+
+ let pp fmt x =
+ Format.pp_print_char fmt '@';
+ Format.pp_print_string fmt (Simple_vector.get names (tag x))
+ end)
+
+ include HC
+
+ type s = D.t
+ let key = D.key
+
+ let tag: t -> int = function
+ | Node.Value(tag,_,_) -> tag
+
+ let index ?(basename="") v =
+ let node =
+ HC.hashcons2
+ (fun tag value v -> Node.Value(tag,value,v))
+ D.key v in
+ let i = tag node in
+ Simple_vector.inc_size (i+1) Node.names;
+ begin
+ if Simple_vector.is_uninitialized Node.names i then
+ let s = Strings.find_new_name Node.used_names basename in
+ Debug.dprintf3 debug_create "[Egraph] @[@@%s is %a@]"
+ s D.pp v;
+ Simple_vector.set Node.names i s
+ end;
+ node
+
+ let node = Node.of_nodevalue
+
+ let value : t -> D.t = function
+ | Node.Value(_,value,v) ->
+ let Poly.Eq = ValueKind.Eq.coerce_type value D.key in v
+
+ let nodevalue: t -> Value.t = fun x -> x
+
+ let of_nodevalue: Value.t -> t option = function
+ | Node.Value(_,value',_) as v when ValueKind.equal value' D.key -> Some v
+ | _ -> None
+
+ let of_value v = nodevalue (index v)
+
+ let coerce_nodevalue: Value.t -> t = function
+ | Node.Value(_,value',_) as v -> assert (ValueKind.equal value' D.key); v
+
+ let coerce_value x = value (coerce_nodevalue x)
end
include All
diff --git a/src_colibri2/core/structures/nodes.mli b/src_colibri2/core/structures/nodes.mli
index 200d5181a..1b4c9638a 100644
--- a/src_colibri2/core/structures/nodes.mli
+++ b/src_colibri2/core/structures/nodes.mli
@@ -141,11 +141,11 @@ module Value: sig
val value: 'a ValueKind.t -> t -> 'a option
type kind =
- | Value: 'a ValueKind.t * 'a -> kind
+ | Value: 'a ValueKind.t * 'a -> kind
val kind: t -> kind
- (** give the value associated with a node, make sense only for not merged
- class. So only the module solver can use it *)
+ (** give the value associated with a node, make sense only for not merged
+ class. So only the module solver can use it *)
end
@@ -171,10 +171,15 @@ module type RegisteredValue = sig
(** Return the value from a nodevalue *)
val nodevalue: t -> Value.t
+
val of_nodevalue: Value.t -> t option
+ val of_value: s -> t
+
val coerce_nodevalue: Value.t -> t
+ val coerce_value: Value.t -> s
+
end
module RegisterValue (D:Value) : RegisteredValue with type s = D.t
@@ -192,18 +197,18 @@ module Only_for_solver: sig
val thterm:
Node.t -> ThTerm.t option
- (** give the sem associated with a node, make sense only for not merged
- class. So only the module solver can use it *)
+ (** give the sem associated with a node, make sense only for not merged
+ class. So only the module solver can use it *)
val sem_of_node:
ThTerm.t -> sem_of_node
- (** give the sem associated with a node, make sense only for not merged
- class. So only the module solver can use it *)
+ (** give the sem associated with a node, make sense only for not merged
+ class. So only the module solver can use it *)
val nodevalue:
Node.t -> Value.t option
- (** give the value associated with a node, make sense only for not merged
- class. So only the module solver can use it *)
+ (** give the value associated with a node, make sense only for not merged
+ class. So only the module solver can use it *)
val node_of_thterm: ThTerm.t -> Node.t
val node_of_nodevalue: Value.t -> Node.t
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
index dc04934ea..a5a508a2c 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -50,9 +50,9 @@ let init_ty d =
let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
let compute_ground d t =
- let (!>>>) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) in
- let (!>>) t = Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t)) in
- let (!>) t = Float32.value (Float32.coerce_nodevalue (interp d t)) in
+ let (!>>>) t = RealValue.coerce_value (interp d t) in
+ let (!>>) t = Rounding_mode.coerce_value (interp d t) in
+ let (!>) t = Float32.coerce_value (interp d t) in
let (!<) v = `Some (Float32.nodevalue (Float32.index v)) in
let (!<<) v = `Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v)) in
match Ground.sem t with
--
GitLab