Skip to content
Snippets Groups Projects
Commit a2a2b924 authored by Michele Alberti's avatar Michele Alberti
Browse files

[language] Use common function for building float64 type symbol.

parent e4fd53c3
No related branches found
No related tags found
No related merge requests found
......@@ -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 =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment