From a2a2b924bce2bcecd737159644c319580e835565 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 25 May 2023 16:27:33 +0200
Subject: [PATCH] [language] Use common function for building float64 type
symbol.
---
src/language.ml | 11 ++++-------
1 file changed, 4 insertions(+), 7 deletions(-)
diff --git a/src/language.ml b/src/language.ml
index 39afa6c..05ad16d 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -160,14 +160,14 @@ let register_ovo_support () =
let vectors = Term.Hls.create 10
-let vector_elt_ty env =
+let float64_t_ty env =
let th = Env.read_theory env [ "ieee_float" ] "Float64" in
Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
let create_vector =
Env.Wenv.memoize 13 (fun env ->
let h = Hashtbl.create (module Int) in
- let ty_elt = vector_elt_ty env in
+ let ty_elt = float64_t_ty env in
let ty =
let th = Env.read_theory env [ "interpretation" ] "Vector" in
Ty.ty_app (Theory.ns_find_ts th.th_export [ "vector" ]) [ ty_elt ]
@@ -207,10 +207,7 @@ let fresh_nn_ls env name =
let create_nn_nnet =
Env.Wenv.memoize 13 (fun env ->
let h = Hashtbl.create (module String) in
- let ty_elt =
- let th = Env.read_theory env [ "ieee_float" ] "Float64" in
- Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
- in
+ let ty_elt = float64_t_ty env in
Hashtbl.findi_or_add h ~default:(fun filename ->
let ls = fresh_nn_ls env "nnet_nn" in
let nn =
@@ -232,7 +229,7 @@ let create_nn_nnet =
let create_nn_onnx =
Env.Wenv.memoize 13 (fun env ->
let h = Hashtbl.create (module String) in
- let ty_elt = vector_elt_ty env in
+ let ty_elt = float64_t_ty env in
Hashtbl.findi_or_add h ~default:(fun filename ->
let ls = fresh_nn_ls env "onnx_nn" in
let onnx =
--
GitLab