From 6dbda66b58afc66bcf50dc97db0838302020846c Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Mon, 4 Oct 2021 17:29:18 +0200
Subject: [PATCH] Able to parse inputs and outputs shape for ONNX

---
 lib/onnx/onnx.mli      |    2 +
 onnx_piqi.ml           | 1320 ----------------------------------------
 onnx_piqi.mli          |  718 ----------------------
 src/dune               |    2 +-
 src/language.ml        |   82 ++-
 src/language.mli       |    9 +-
 src/transformations.ml |    4 +-
 src/verification.ml    |    1 +
 8 files changed, 89 insertions(+), 2049 deletions(-)
 delete mode 100644 onnx_piqi.ml
 delete mode 100644 onnx_piqi.mli

diff --git a/lib/onnx/onnx.mli b/lib/onnx/onnx.mli
index 3c708435..775d08b1 100644
--- a/lib/onnx/onnx.mli
+++ b/lib/onnx/onnx.mli
@@ -4,6 +4,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module Opiqi = Onnx_piqi
+
 type t = Onnx_piqi.Model_proto.t
 
 val parse : string -> (t, string) Result.t
diff --git a/onnx_piqi.ml b/onnx_piqi.ml
deleted file mode 100644
index 2a0636f1..00000000
--- a/onnx_piqi.ml
+++ /dev/null
@@ -1,1320 +0,0 @@
-module rec Onnx_piqi:
-  sig
-    type float32 = float
-    type float64 = float
-    type uint64 = int64
-    type protobuf_int64 = int64
-    type binary = string
-    type protobuf_int32 = int32
-    type attribute_proto_attribute_type =
-      [
-        | `undefined
-        | `float
-        | `int
-        | `string
-        | `tensor
-        | `graph
-        | `sparse_tensor
-        | `type_proto
-        | `floats
-        | `ints
-        | `strings
-        | `tensors
-        | `graphs
-        | `sparse_tensors
-        | `type_protos
-      ]
-    type tensor_proto_data_type =
-      [
-        | `undefined
-        | `float
-        | `uint8
-        | `int8
-        | `uint16
-        | `int16
-        | `int32
-        | `int64
-        | `string
-        | `bool
-        | `float16
-        | `double
-        | `uint32
-        | `uint64
-        | `complex64
-        | `complex128
-        | `bfloat16
-      ]
-    type tensor_proto_data_location =
-      [
-        | `default
-        | `externall
-      ]
-    type version =
-      [
-        | `start_version
-        | `ir_version_2017_10_10
-        | `ir_version_2017_10_30
-        | `ir_version_2017_11_3
-        | `ir_version_2019_1_22
-        | `ir_version_2019_3_18
-        | `ir_version_2019_9_19
-        | `ir_version_2020_5_8
-        | `ir_version
-      ]
-    type operator_status =
-      [
-        | `experimental
-        | `stable
-      ]
-    type attribute_proto = Attribute_proto.t
-    type value_info_proto = Value_info_proto.t
-    type node_proto = Node_proto.t
-    type training_info_proto = Training_info_proto.t
-    type model_proto = Model_proto.t
-    type string_string_entry_proto = String_string_entry_proto.t
-    type tensor_annotation = Tensor_annotation.t
-    type graph_proto = Graph_proto.t
-    type tensor_proto = Tensor_proto.t
-    type tensor_proto_segment = Tensor_proto_segment.t
-    type sparse_tensor_proto = Sparse_tensor_proto.t
-    type tensor_shape_proto = Tensor_shape_proto.t
-    type tensor_shape_proto_dimension = Tensor_shape_proto_dimension.t
-    type type_proto = Type_proto.t
-    type type_proto_tensor = Type_proto_tensor.t
-    type type_proto_sequence = Type_proto_sequence.t
-    type type_proto_map = Type_proto_map.t
-    type type_proto_optional = Type_proto_optional.t
-    type type_proto_sparse_tensor = Type_proto_sparse_tensor.t
-    type operator_set_id_proto = Operator_set_id_proto.t
-    type function_proto = Function_proto.t
-  end = Onnx_piqi
-and Attribute_proto:
-  sig
-    type t = {
-      mutable name: string option;
-      mutable ref_attr_name: string option;
-      mutable doc_string: string option;
-      mutable type_: Onnx_piqi.attribute_proto_attribute_type option;
-      mutable f: Onnx_piqi.float32 option;
-      mutable i: Onnx_piqi.protobuf_int64 option;
-      mutable s: Onnx_piqi.binary option;
-      mutable t: Onnx_piqi.tensor_proto option;
-      mutable g: Onnx_piqi.graph_proto option;
-      mutable sparse_tensor: Onnx_piqi.sparse_tensor_proto option;
-      mutable tp: Onnx_piqi.type_proto option;
-      mutable floats: Onnx_piqi.float32 list;
-      mutable ints: Onnx_piqi.protobuf_int64 list;
-      mutable strings: Onnx_piqi.binary list;
-      mutable tensors: Onnx_piqi.tensor_proto list;
-      mutable graphs: Onnx_piqi.graph_proto list;
-      mutable sparse_tensors: Onnx_piqi.sparse_tensor_proto list;
-      mutable type_protos: Onnx_piqi.type_proto list;
-    }
-  end = Attribute_proto
-and Value_info_proto:
-  sig
-    type t = {
-      mutable name: string option;
-      mutable type_: Onnx_piqi.type_proto option;
-      mutable doc_string: string option;
-    }
-  end = Value_info_proto
-and Node_proto:
-  sig
-    type t = {
-      mutable input: string list;
-      mutable output: string list;
-      mutable name: string option;
-      mutable op_type: string option;
-      mutable domain: string option;
-      mutable attribute: Onnx_piqi.attribute_proto list;
-      mutable doc_string: string option;
-    }
-  end = Node_proto
-and Training_info_proto:
-  sig
-    type t = {
-      mutable initialization: Onnx_piqi.graph_proto option;
-      mutable algorithm: Onnx_piqi.graph_proto option;
-      mutable initialization_binding: Onnx_piqi.string_string_entry_proto list;
-      mutable update_binding: Onnx_piqi.string_string_entry_proto list;
-    }
-  end = Training_info_proto
-and Model_proto:
-  sig
-    type t = {
-      mutable ir_version: Onnx_piqi.protobuf_int64 option;
-      mutable opset_import: Onnx_piqi.operator_set_id_proto list;
-      mutable producer_name: string option;
-      mutable producer_version: string option;
-      mutable domain: string option;
-      mutable model_version: Onnx_piqi.protobuf_int64 option;
-      mutable doc_string: string option;
-      mutable graph: Onnx_piqi.graph_proto option;
-      mutable metadata_props: Onnx_piqi.string_string_entry_proto list;
-      mutable training_info: Onnx_piqi.training_info_proto list;
-      mutable functions: Onnx_piqi.function_proto list;
-    }
-  end = Model_proto
-and String_string_entry_proto:
-  sig
-    type t = {
-      mutable key: string option;
-      mutable value: string option;
-    }
-  end = String_string_entry_proto
-and Tensor_annotation:
-  sig
-    type t = {
-      mutable tensor_name: string option;
-      mutable quant_parameter_tensor_names: Onnx_piqi.string_string_entry_proto list;
-    }
-  end = Tensor_annotation
-and Graph_proto:
-  sig
-    type t = {
-      mutable node: Onnx_piqi.node_proto list;
-      mutable name: string option;
-      mutable initializer_: Onnx_piqi.tensor_proto list;
-      mutable sparse_initializer: Onnx_piqi.sparse_tensor_proto list;
-      mutable doc_string: string option;
-      mutable input: Onnx_piqi.value_info_proto list;
-      mutable output: Onnx_piqi.value_info_proto list;
-      mutable value_info: Onnx_piqi.value_info_proto list;
-      mutable quantization_annotation: Onnx_piqi.tensor_annotation list;
-    }
-  end = Graph_proto
-and Tensor_proto:
-  sig
-    type t = {
-      mutable dims: Onnx_piqi.protobuf_int64 list;
-      mutable data_type: Onnx_piqi.protobuf_int32 option;
-      mutable segment: Onnx_piqi.tensor_proto_segment option;
-      mutable float_data: Onnx_piqi.float32 list;
-      mutable int32_data: Onnx_piqi.protobuf_int32 list;
-      mutable string_data: Onnx_piqi.binary list;
-      mutable int64_data: Onnx_piqi.protobuf_int64 list;
-      mutable name: string option;
-      mutable doc_string: string option;
-      mutable raw_data: Onnx_piqi.binary option;
-      mutable externall_data: Onnx_piqi.string_string_entry_proto list;
-      mutable data_location: Onnx_piqi.tensor_proto_data_location option;
-      mutable double_data: Onnx_piqi.float64 list;
-      mutable uint64_data: Onnx_piqi.uint64 list;
-    }
-  end = Tensor_proto
-and Tensor_proto_segment:
-  sig
-    type t = {
-      mutable begin_: Onnx_piqi.protobuf_int64 option;
-      mutable end_: Onnx_piqi.protobuf_int64 option;
-    }
-  end = Tensor_proto_segment
-and Sparse_tensor_proto:
-  sig
-    type t = {
-      mutable values: Onnx_piqi.tensor_proto option;
-      mutable indices: Onnx_piqi.tensor_proto option;
-      mutable dims: Onnx_piqi.protobuf_int64 list;
-    }
-  end = Sparse_tensor_proto
-and Tensor_shape_proto:
-  sig
-    type t = {
-      mutable dim: Onnx_piqi.tensor_shape_proto_dimension list;
-    }
-  end = Tensor_shape_proto
-and Tensor_shape_proto_dimension:
-  sig
-    type t = {
-      mutable dim_value: Onnx_piqi.protobuf_int64 option;
-      mutable dim_param: string option;
-      mutable denotation: string option;
-    }
-  end = Tensor_shape_proto_dimension
-and Type_proto:
-  sig
-    type t = {
-      mutable tensor_type: Onnx_piqi.type_proto_tensor option;
-      mutable sequence_type: Onnx_piqi.type_proto_sequence option;
-      mutable map_type: Onnx_piqi.type_proto_map option;
-      mutable optional_type: Onnx_piqi.type_proto_optional option;
-      mutable sparse_tensor_type: Onnx_piqi.type_proto_sparse_tensor option;
-      mutable denotation: string option;
-    }
-  end = Type_proto
-and Type_proto_tensor:
-  sig
-    type t = {
-      mutable elem_type: Onnx_piqi.protobuf_int32 option;
-      mutable shape: Onnx_piqi.tensor_shape_proto option;
-    }
-  end = Type_proto_tensor
-and Type_proto_sequence:
-  sig
-    type t = {
-      mutable elem_type: Onnx_piqi.type_proto option;
-    }
-  end = Type_proto_sequence
-and Type_proto_map:
-  sig
-    type t = {
-      mutable key_type: Onnx_piqi.protobuf_int32 option;
-      mutable value_type: Onnx_piqi.type_proto option;
-    }
-  end = Type_proto_map
-and Type_proto_optional:
-  sig
-    type t = {
-      mutable elem_type: Onnx_piqi.type_proto option;
-    }
-  end = Type_proto_optional
-and Type_proto_sparse_tensor:
-  sig
-    type t = {
-      mutable elem_type: Onnx_piqi.protobuf_int32 option;
-      mutable shape: Onnx_piqi.tensor_shape_proto option;
-    }
-  end = Type_proto_sparse_tensor
-and Operator_set_id_proto:
-  sig
-    type t = {
-      mutable domain: string option;
-      mutable version: Onnx_piqi.protobuf_int64 option;
-    }
-  end = Operator_set_id_proto
-and Function_proto:
-  sig
-    type t = {
-      mutable name: string option;
-      mutable input: string list;
-      mutable output: string list;
-      mutable attribute: string list;
-      mutable node: Onnx_piqi.node_proto list;
-      mutable doc_string: string option;
-      mutable opset_import: Onnx_piqi.operator_set_id_proto list;
-      mutable domain: string option;
-    }
-  end = Function_proto
-
-
-let rec parse_int64 x = Piqirun.int64_of_zigzag_varint x
-and packed_parse_int64 x = Piqirun.int64_of_packed_zigzag_varint x
-
-and parse_int32 x = Piqirun.int32_of_zigzag_varint x
-and packed_parse_int32 x = Piqirun.int32_of_packed_zigzag_varint x
-
-and parse_string x = Piqirun.string_of_block x
-
-and parse_float32 x = Piqirun.float_of_fixed32 x
-and packed_parse_float32 x = Piqirun.float_of_packed_fixed32 x
-
-and parse_protobuf_int64 x = Piqirun.int64_of_signed_varint x
-and packed_parse_protobuf_int64 x = Piqirun.int64_of_packed_signed_varint x
-
-and parse_binary x = Piqirun.string_of_block x
-
-and parse_protobuf_int32 x = Piqirun.int32_of_signed_varint x
-and packed_parse_protobuf_int32 x = Piqirun.int32_of_packed_signed_varint x
-
-and parse_float64 x = Piqirun.float_of_fixed64 x
-and packed_parse_float64 x = Piqirun.float_of_packed_fixed64 x
-
-and parse_uint64 x = Piqirun.int64_of_varint x
-and packed_parse_uint64 x = Piqirun.int64_of_packed_varint x
-
-and parse_attribute_proto x =
-  let x = Piqirun.parse_record x in
-  let _name, x = Piqirun.parse_optional_field 1 parse_string x in
-  let _f, x = Piqirun.parse_optional_field 2 parse_float32 x in
-  let _i, x = Piqirun.parse_optional_field 3 parse_protobuf_int64 x in
-  let _s, x = Piqirun.parse_optional_field 4 parse_binary x in
-  let _t, x = Piqirun.parse_optional_field 5 parse_tensor_proto x in
-  let _g, x = Piqirun.parse_optional_field 6 parse_graph_proto x in
-  let _floats, x = Piqirun.parse_repeated_field 7 parse_float32 x in
-  let _ints, x = Piqirun.parse_repeated_field 8 parse_protobuf_int64 x in
-  let _strings, x = Piqirun.parse_repeated_field 9 parse_binary x in
-  let _tensors, x = Piqirun.parse_repeated_field 10 parse_tensor_proto x in
-  let _graphs, x = Piqirun.parse_repeated_field 11 parse_graph_proto x in
-  let _doc_string, x = Piqirun.parse_optional_field 13 parse_string x in
-  let _tp, x = Piqirun.parse_optional_field 14 parse_type_proto x in
-  let _type_protos, x = Piqirun.parse_repeated_field 15 parse_type_proto x in
-  let _type_, x = Piqirun.parse_optional_field 20 parse_attribute_proto_attribute_type x in
-  let _ref_attr_name, x = Piqirun.parse_optional_field 21 parse_string x in
-  let _sparse_tensor, x = Piqirun.parse_optional_field 22 parse_sparse_tensor_proto x in
-  let _sparse_tensors, x = Piqirun.parse_repeated_field 23 parse_sparse_tensor_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Attribute_proto.name = _name;
-    Attribute_proto.f = _f;
-    Attribute_proto.i = _i;
-    Attribute_proto.s = _s;
-    Attribute_proto.t = _t;
-    Attribute_proto.g = _g;
-    Attribute_proto.floats = _floats;
-    Attribute_proto.ints = _ints;
-    Attribute_proto.strings = _strings;
-    Attribute_proto.tensors = _tensors;
-    Attribute_proto.graphs = _graphs;
-    Attribute_proto.doc_string = _doc_string;
-    Attribute_proto.tp = _tp;
-    Attribute_proto.type_protos = _type_protos;
-    Attribute_proto.type_ = _type_;
-    Attribute_proto.ref_attr_name = _ref_attr_name;
-    Attribute_proto.sparse_tensor = _sparse_tensor;
-    Attribute_proto.sparse_tensors = _sparse_tensors;
-  }
-
-and parse_attribute_proto_attribute_type x =
-  match Piqirun.int32_of_signed_varint x with
-    | 0l -> `undefined
-    | 1l -> `float
-    | 2l -> `int
-    | 3l -> `string
-    | 4l -> `tensor
-    | 5l -> `graph
-    | 11l -> `sparse_tensor
-    | 13l -> `type_proto
-    | 6l -> `floats
-    | 7l -> `ints
-    | 8l -> `strings
-    | 9l -> `tensors
-    | 10l -> `graphs
-    | 12l -> `sparse_tensors
-    | 14l -> `type_protos
-    | x -> Piqirun.error_enum_const x
-and packed_parse_attribute_proto_attribute_type x =
-  match Piqirun.int32_of_packed_signed_varint x with
-    | 0l -> `undefined
-    | 1l -> `float
-    | 2l -> `int
-    | 3l -> `string
-    | 4l -> `tensor
-    | 5l -> `graph
-    | 11l -> `sparse_tensor
-    | 13l -> `type_proto
-    | 6l -> `floats
-    | 7l -> `ints
-    | 8l -> `strings
-    | 9l -> `tensors
-    | 10l -> `graphs
-    | 12l -> `sparse_tensors
-    | 14l -> `type_protos
-    | x -> Piqirun.error_enum_const x
-
-and parse_value_info_proto x =
-  let x = Piqirun.parse_record x in
-  let _name, x = Piqirun.parse_optional_field 1 parse_string x in
-  let _type_, x = Piqirun.parse_optional_field 2 parse_type_proto x in
-  let _doc_string, x = Piqirun.parse_optional_field 3 parse_string x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Value_info_proto.name = _name;
-    Value_info_proto.type_ = _type_;
-    Value_info_proto.doc_string = _doc_string;
-  }
-
-and parse_node_proto x =
-  let x = Piqirun.parse_record x in
-  let _input, x = Piqirun.parse_repeated_field 1 parse_string x in
-  let _output, x = Piqirun.parse_repeated_field 2 parse_string x in
-  let _name, x = Piqirun.parse_optional_field 3 parse_string x in
-  let _op_type, x = Piqirun.parse_optional_field 4 parse_string x in
-  let _attribute, x = Piqirun.parse_repeated_field 5 parse_attribute_proto x in
-  let _doc_string, x = Piqirun.parse_optional_field 6 parse_string x in
-  let _domain, x = Piqirun.parse_optional_field 7 parse_string x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Node_proto.input = _input;
-    Node_proto.output = _output;
-    Node_proto.name = _name;
-    Node_proto.op_type = _op_type;
-    Node_proto.attribute = _attribute;
-    Node_proto.doc_string = _doc_string;
-    Node_proto.domain = _domain;
-  }
-
-and parse_training_info_proto x =
-  let x = Piqirun.parse_record x in
-  let _initialization, x = Piqirun.parse_optional_field 1 parse_graph_proto x in
-  let _algorithm, x = Piqirun.parse_optional_field 2 parse_graph_proto x in
-  let _initialization_binding, x = Piqirun.parse_repeated_field 3 parse_string_string_entry_proto x in
-  let _update_binding, x = Piqirun.parse_repeated_field 4 parse_string_string_entry_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Training_info_proto.initialization = _initialization;
-    Training_info_proto.algorithm = _algorithm;
-    Training_info_proto.initialization_binding = _initialization_binding;
-    Training_info_proto.update_binding = _update_binding;
-  }
-
-and parse_model_proto x =
-  let x = Piqirun.parse_record x in
-  let _ir_version, x = Piqirun.parse_optional_field 1 parse_protobuf_int64 x in
-  let _producer_name, x = Piqirun.parse_optional_field 2 parse_string x in
-  let _producer_version, x = Piqirun.parse_optional_field 3 parse_string x in
-  let _domain, x = Piqirun.parse_optional_field 4 parse_string x in
-  let _model_version, x = Piqirun.parse_optional_field 5 parse_protobuf_int64 x in
-  let _doc_string, x = Piqirun.parse_optional_field 6 parse_string x in
-  let _graph, x = Piqirun.parse_optional_field 7 parse_graph_proto x in
-  let _opset_import, x = Piqirun.parse_repeated_field 8 parse_operator_set_id_proto x in
-  let _metadata_props, x = Piqirun.parse_repeated_field 14 parse_string_string_entry_proto x in
-  let _training_info, x = Piqirun.parse_repeated_field 20 parse_training_info_proto x in
-  let _functions, x = Piqirun.parse_repeated_field 25 parse_function_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Model_proto.ir_version = _ir_version;
-    Model_proto.producer_name = _producer_name;
-    Model_proto.producer_version = _producer_version;
-    Model_proto.domain = _domain;
-    Model_proto.model_version = _model_version;
-    Model_proto.doc_string = _doc_string;
-    Model_proto.graph = _graph;
-    Model_proto.opset_import = _opset_import;
-    Model_proto.metadata_props = _metadata_props;
-    Model_proto.training_info = _training_info;
-    Model_proto.functions = _functions;
-  }
-
-and parse_string_string_entry_proto x =
-  let x = Piqirun.parse_record x in
-  let _key, x = Piqirun.parse_optional_field 1 parse_string x in
-  let _value, x = Piqirun.parse_optional_field 2 parse_string x in
-  Piqirun.check_unparsed_fields x;
-  {
-    String_string_entry_proto.key = _key;
-    String_string_entry_proto.value = _value;
-  }
-
-and parse_tensor_annotation x =
-  let x = Piqirun.parse_record x in
-  let _tensor_name, x = Piqirun.parse_optional_field 1 parse_string x in
-  let _quant_parameter_tensor_names, x = Piqirun.parse_repeated_field 2 parse_string_string_entry_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Tensor_annotation.tensor_name = _tensor_name;
-    Tensor_annotation.quant_parameter_tensor_names = _quant_parameter_tensor_names;
-  }
-
-and parse_graph_proto x =
-  let x = Piqirun.parse_record x in
-  let _node, x = Piqirun.parse_repeated_field 1 parse_node_proto x in
-  let _name, x = Piqirun.parse_optional_field 2 parse_string x in
-  let _initializer_, x = Piqirun.parse_repeated_field 5 parse_tensor_proto x in
-  let _doc_string, x = Piqirun.parse_optional_field 10 parse_string x in
-  let _input, x = Piqirun.parse_repeated_field 11 parse_value_info_proto x in
-  let _output, x = Piqirun.parse_repeated_field 12 parse_value_info_proto x in
-  let _value_info, x = Piqirun.parse_repeated_field 13 parse_value_info_proto x in
-  let _quantization_annotation, x = Piqirun.parse_repeated_field 14 parse_tensor_annotation x in
-  let _sparse_initializer, x = Piqirun.parse_repeated_field 15 parse_sparse_tensor_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Graph_proto.node = _node;
-    Graph_proto.name = _name;
-    Graph_proto.initializer_ = _initializer_;
-    Graph_proto.doc_string = _doc_string;
-    Graph_proto.input = _input;
-    Graph_proto.output = _output;
-    Graph_proto.value_info = _value_info;
-    Graph_proto.quantization_annotation = _quantization_annotation;
-    Graph_proto.sparse_initializer = _sparse_initializer;
-  }
-
-and parse_tensor_proto x =
-  let x = Piqirun.parse_record x in
-  let _dims, x = Piqirun.parse_repeated_field 1 parse_protobuf_int64 x in
-  let _data_type, x = Piqirun.parse_optional_field 2 parse_protobuf_int32 x in
-  let _segment, x = Piqirun.parse_optional_field 3 parse_tensor_proto_segment x in
-  let _float_data, x = Piqirun.parse_packed_repeated_field 4 packed_parse_float32 parse_float32 x in
-  let _int32_data, x = Piqirun.parse_packed_repeated_field 5 packed_parse_protobuf_int32 parse_protobuf_int32 x in
-  let _string_data, x = Piqirun.parse_repeated_field 6 parse_binary x in
-  let _int64_data, x = Piqirun.parse_packed_repeated_field 7 packed_parse_protobuf_int64 parse_protobuf_int64 x in
-  let _name, x = Piqirun.parse_optional_field 8 parse_string x in
-  let _raw_data, x = Piqirun.parse_optional_field 9 parse_binary x in
-  let _double_data, x = Piqirun.parse_packed_repeated_field 10 packed_parse_float64 parse_float64 x in
-  let _uint64_data, x = Piqirun.parse_packed_repeated_field 11 packed_parse_uint64 parse_uint64 x in
-  let _doc_string, x = Piqirun.parse_optional_field 12 parse_string x in
-  let _externall_data, x = Piqirun.parse_repeated_field 13 parse_string_string_entry_proto x in
-  let _data_location, x = Piqirun.parse_optional_field 14 parse_tensor_proto_data_location x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Tensor_proto.dims = _dims;
-    Tensor_proto.data_type = _data_type;
-    Tensor_proto.segment = _segment;
-    Tensor_proto.float_data = _float_data;
-    Tensor_proto.int32_data = _int32_data;
-    Tensor_proto.string_data = _string_data;
-    Tensor_proto.int64_data = _int64_data;
-    Tensor_proto.name = _name;
-    Tensor_proto.raw_data = _raw_data;
-    Tensor_proto.double_data = _double_data;
-    Tensor_proto.uint64_data = _uint64_data;
-    Tensor_proto.doc_string = _doc_string;
-    Tensor_proto.externall_data = _externall_data;
-    Tensor_proto.data_location = _data_location;
-  }
-
-and parse_tensor_proto_segment x =
-  let x = Piqirun.parse_record x in
-  let _begin_, x = Piqirun.parse_optional_field 1 parse_protobuf_int64 x in
-  let _end_, x = Piqirun.parse_optional_field 2 parse_protobuf_int64 x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Tensor_proto_segment.begin_ = _begin_;
-    Tensor_proto_segment.end_ = _end_;
-  }
-
-and parse_tensor_proto_data_type x =
-  match Piqirun.int32_of_signed_varint x with
-    | 0l -> `undefined
-    | 1l -> `float
-    | 2l -> `uint8
-    | 3l -> `int8
-    | 4l -> `uint16
-    | 5l -> `int16
-    | 6l -> `int32
-    | 7l -> `int64
-    | 8l -> `string
-    | 9l -> `bool
-    | 10l -> `float16
-    | 11l -> `double
-    | 12l -> `uint32
-    | 13l -> `uint64
-    | 14l -> `complex64
-    | 15l -> `complex128
-    | 16l -> `bfloat16
-    | x -> Piqirun.error_enum_const x
-and packed_parse_tensor_proto_data_type x =
-  match Piqirun.int32_of_packed_signed_varint x with
-    | 0l -> `undefined
-    | 1l -> `float
-    | 2l -> `uint8
-    | 3l -> `int8
-    | 4l -> `uint16
-    | 5l -> `int16
-    | 6l -> `int32
-    | 7l -> `int64
-    | 8l -> `string
-    | 9l -> `bool
-    | 10l -> `float16
-    | 11l -> `double
-    | 12l -> `uint32
-    | 13l -> `uint64
-    | 14l -> `complex64
-    | 15l -> `complex128
-    | 16l -> `bfloat16
-    | x -> Piqirun.error_enum_const x
-
-and parse_tensor_proto_data_location x =
-  match Piqirun.int32_of_signed_varint x with
-    | 0l -> `default
-    | 1l -> `externall
-    | x -> Piqirun.error_enum_const x
-and packed_parse_tensor_proto_data_location x =
-  match Piqirun.int32_of_packed_signed_varint x with
-    | 0l -> `default
-    | 1l -> `externall
-    | x -> Piqirun.error_enum_const x
-
-and parse_sparse_tensor_proto x =
-  let x = Piqirun.parse_record x in
-  let _values, x = Piqirun.parse_optional_field 1 parse_tensor_proto x in
-  let _indices, x = Piqirun.parse_optional_field 2 parse_tensor_proto x in
-  let _dims, x = Piqirun.parse_repeated_field 3 parse_protobuf_int64 x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Sparse_tensor_proto.values = _values;
-    Sparse_tensor_proto.indices = _indices;
-    Sparse_tensor_proto.dims = _dims;
-  }
-
-and parse_tensor_shape_proto x =
-  let x = Piqirun.parse_record x in
-  let _dim, x = Piqirun.parse_repeated_field 1 parse_tensor_shape_proto_dimension x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Tensor_shape_proto.dim = _dim;
-  }
-
-and parse_tensor_shape_proto_dimension x =
-  let x = Piqirun.parse_record x in
-  let _dim_value, x = Piqirun.parse_optional_field 1 parse_protobuf_int64 x in
-  let _dim_param, x = Piqirun.parse_optional_field 2 parse_string x in
-  let _denotation, x = Piqirun.parse_optional_field 3 parse_string x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Tensor_shape_proto_dimension.dim_value = _dim_value;
-    Tensor_shape_proto_dimension.dim_param = _dim_param;
-    Tensor_shape_proto_dimension.denotation = _denotation;
-  }
-
-and parse_type_proto x =
-  let x = Piqirun.parse_record x in
-  let _tensor_type, x = Piqirun.parse_optional_field 1 parse_type_proto_tensor x in
-  let _sequence_type, x = Piqirun.parse_optional_field 4 parse_type_proto_sequence x in
-  let _map_type, x = Piqirun.parse_optional_field 5 parse_type_proto_map x in
-  let _denotation, x = Piqirun.parse_optional_field 6 parse_string x in
-  let _sparse_tensor_type, x = Piqirun.parse_optional_field 8 parse_type_proto_sparse_tensor x in
-  let _optional_type, x = Piqirun.parse_optional_field 9 parse_type_proto_optional x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Type_proto.tensor_type = _tensor_type;
-    Type_proto.sequence_type = _sequence_type;
-    Type_proto.map_type = _map_type;
-    Type_proto.denotation = _denotation;
-    Type_proto.sparse_tensor_type = _sparse_tensor_type;
-    Type_proto.optional_type = _optional_type;
-  }
-
-and parse_type_proto_tensor x =
-  let x = Piqirun.parse_record x in
-  let _elem_type, x = Piqirun.parse_optional_field 1 parse_protobuf_int32 x in
-  let _shape, x = Piqirun.parse_optional_field 2 parse_tensor_shape_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Type_proto_tensor.elem_type = _elem_type;
-    Type_proto_tensor.shape = _shape;
-  }
-
-and parse_type_proto_sequence x =
-  let x = Piqirun.parse_record x in
-  let _elem_type, x = Piqirun.parse_optional_field 1 parse_type_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Type_proto_sequence.elem_type = _elem_type;
-  }
-
-and parse_type_proto_map x =
-  let x = Piqirun.parse_record x in
-  let _key_type, x = Piqirun.parse_optional_field 1 parse_protobuf_int32 x in
-  let _value_type, x = Piqirun.parse_optional_field 2 parse_type_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Type_proto_map.key_type = _key_type;
-    Type_proto_map.value_type = _value_type;
-  }
-
-and parse_type_proto_optional x =
-  let x = Piqirun.parse_record x in
-  let _elem_type, x = Piqirun.parse_optional_field 1 parse_type_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Type_proto_optional.elem_type = _elem_type;
-  }
-
-and parse_type_proto_sparse_tensor x =
-  let x = Piqirun.parse_record x in
-  let _elem_type, x = Piqirun.parse_optional_field 1 parse_protobuf_int32 x in
-  let _shape, x = Piqirun.parse_optional_field 2 parse_tensor_shape_proto x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Type_proto_sparse_tensor.elem_type = _elem_type;
-    Type_proto_sparse_tensor.shape = _shape;
-  }
-
-and parse_operator_set_id_proto x =
-  let x = Piqirun.parse_record x in
-  let _domain, x = Piqirun.parse_optional_field 1 parse_string x in
-  let _version, x = Piqirun.parse_optional_field 2 parse_protobuf_int64 x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Operator_set_id_proto.domain = _domain;
-    Operator_set_id_proto.version = _version;
-  }
-
-and parse_function_proto x =
-  let x = Piqirun.parse_record x in
-  let _name, x = Piqirun.parse_optional_field 1 parse_string x in
-  let _input, x = Piqirun.parse_repeated_field 4 parse_string x in
-  let _output, x = Piqirun.parse_repeated_field 5 parse_string x in
-  let _attribute, x = Piqirun.parse_repeated_field 6 parse_string x in
-  let _node, x = Piqirun.parse_repeated_field 7 parse_node_proto x in
-  let _doc_string, x = Piqirun.parse_optional_field 8 parse_string x in
-  let _opset_import, x = Piqirun.parse_repeated_field 9 parse_operator_set_id_proto x in
-  let _domain, x = Piqirun.parse_optional_field 10 parse_string x in
-  Piqirun.check_unparsed_fields x;
-  {
-    Function_proto.name = _name;
-    Function_proto.input = _input;
-    Function_proto.output = _output;
-    Function_proto.attribute = _attribute;
-    Function_proto.node = _node;
-    Function_proto.doc_string = _doc_string;
-    Function_proto.opset_import = _opset_import;
-    Function_proto.domain = _domain;
-  }
-
-and parse_version x =
-  match Piqirun.int32_of_signed_varint x with
-    | 0l -> `start_version
-    | 1l -> `ir_version_2017_10_10
-    | 2l -> `ir_version_2017_10_30
-    | 3l -> `ir_version_2017_11_3
-    | 4l -> `ir_version_2019_1_22
-    | 5l -> `ir_version_2019_3_18
-    | 6l -> `ir_version_2019_9_19
-    | 7l -> `ir_version_2020_5_8
-    | 8l -> `ir_version
-    | x -> Piqirun.error_enum_const x
-and packed_parse_version x =
-  match Piqirun.int32_of_packed_signed_varint x with
-    | 0l -> `start_version
-    | 1l -> `ir_version_2017_10_10
-    | 2l -> `ir_version_2017_10_30
-    | 3l -> `ir_version_2017_11_3
-    | 4l -> `ir_version_2019_1_22
-    | 5l -> `ir_version_2019_3_18
-    | 6l -> `ir_version_2019_9_19
-    | 7l -> `ir_version_2020_5_8
-    | 8l -> `ir_version
-    | x -> Piqirun.error_enum_const x
-
-and parse_operator_status x =
-  match Piqirun.int32_of_signed_varint x with
-    | 0l -> `experimental
-    | 1l -> `stable
-    | x -> Piqirun.error_enum_const x
-and packed_parse_operator_status x =
-  match Piqirun.int32_of_packed_signed_varint x with
-    | 0l -> `experimental
-    | 1l -> `stable
-    | x -> Piqirun.error_enum_const x
-
-
-let rec gen__int64 code x = Piqirun.int64_to_zigzag_varint code x
-and packed_gen__int64 x = Piqirun.int64_to_packed_zigzag_varint x
-
-and gen__int32 code x = Piqirun.int32_to_zigzag_varint code x
-and packed_gen__int32 x = Piqirun.int32_to_packed_zigzag_varint x
-
-and gen__string code x = Piqirun.string_to_block code x
-
-and gen__float32 code x = Piqirun.float_to_fixed32 code x
-and packed_gen__float32 x = Piqirun.float_to_packed_fixed32 x
-
-and gen__protobuf_int64 code x = Piqirun.int64_to_signed_varint code x
-and packed_gen__protobuf_int64 x = Piqirun.int64_to_packed_signed_varint x
-
-and gen__binary code x = Piqirun.string_to_block code x
-
-and gen__protobuf_int32 code x = Piqirun.int32_to_signed_varint code x
-and packed_gen__protobuf_int32 x = Piqirun.int32_to_packed_signed_varint x
-
-and gen__float64 code x = Piqirun.float_to_fixed64 code x
-and packed_gen__float64 x = Piqirun.float_to_packed_fixed64 x
-
-and gen__uint64 code x = Piqirun.int64_to_varint code x
-and packed_gen__uint64 x = Piqirun.int64_to_packed_varint x
-
-and gen__attribute_proto code x =
-  let _name = Piqirun.gen_optional_field 1 gen__string x.Attribute_proto.name in
-  let _f = Piqirun.gen_optional_field 2 gen__float32 x.Attribute_proto.f in
-  let _i = Piqirun.gen_optional_field 3 gen__protobuf_int64 x.Attribute_proto.i in
-  let _s = Piqirun.gen_optional_field 4 gen__binary x.Attribute_proto.s in
-  let _t = Piqirun.gen_optional_field 5 gen__tensor_proto x.Attribute_proto.t in
-  let _g = Piqirun.gen_optional_field 6 gen__graph_proto x.Attribute_proto.g in
-  let _floats = Piqirun.gen_repeated_field 7 gen__float32 x.Attribute_proto.floats in
-  let _ints = Piqirun.gen_repeated_field 8 gen__protobuf_int64 x.Attribute_proto.ints in
-  let _strings = Piqirun.gen_repeated_field 9 gen__binary x.Attribute_proto.strings in
-  let _tensors = Piqirun.gen_repeated_field 10 gen__tensor_proto x.Attribute_proto.tensors in
-  let _graphs = Piqirun.gen_repeated_field 11 gen__graph_proto x.Attribute_proto.graphs in
-  let _doc_string = Piqirun.gen_optional_field 13 gen__string x.Attribute_proto.doc_string in
-  let _tp = Piqirun.gen_optional_field 14 gen__type_proto x.Attribute_proto.tp in
-  let _type_protos = Piqirun.gen_repeated_field 15 gen__type_proto x.Attribute_proto.type_protos in
-  let _type_ = Piqirun.gen_optional_field 20 gen__attribute_proto_attribute_type x.Attribute_proto.type_ in
-  let _ref_attr_name = Piqirun.gen_optional_field 21 gen__string x.Attribute_proto.ref_attr_name in
-  let _sparse_tensor = Piqirun.gen_optional_field 22 gen__sparse_tensor_proto x.Attribute_proto.sparse_tensor in
-  let _sparse_tensors = Piqirun.gen_repeated_field 23 gen__sparse_tensor_proto x.Attribute_proto.sparse_tensors in
-  Piqirun.gen_record code (_name :: _f :: _i :: _s :: _t :: _g :: _floats :: _ints :: _strings :: _tensors :: _graphs :: _doc_string :: _tp :: _type_protos :: _type_ :: _ref_attr_name :: _sparse_tensor :: _sparse_tensors :: [])
-
-and gen__attribute_proto_attribute_type code x =
-  Piqirun.int32_to_signed_varint code (match x with
-    | `undefined -> 0l
-    | `float -> 1l
-    | `int -> 2l
-    | `string -> 3l
-    | `tensor -> 4l
-    | `graph -> 5l
-    | `sparse_tensor -> 11l
-    | `type_proto -> 13l
-    | `floats -> 6l
-    | `ints -> 7l
-    | `strings -> 8l
-    | `tensors -> 9l
-    | `graphs -> 10l
-    | `sparse_tensors -> 12l
-    | `type_protos -> 14l
-  )
-and packed_gen__attribute_proto_attribute_type x =
-  Piqirun.int32_to_packed_signed_varint (match x with
-    | `undefined -> 0l
-    | `float -> 1l
-    | `int -> 2l
-    | `string -> 3l
-    | `tensor -> 4l
-    | `graph -> 5l
-    | `sparse_tensor -> 11l
-    | `type_proto -> 13l
-    | `floats -> 6l
-    | `ints -> 7l
-    | `strings -> 8l
-    | `tensors -> 9l
-    | `graphs -> 10l
-    | `sparse_tensors -> 12l
-    | `type_protos -> 14l
-  )
-
-and gen__value_info_proto code x =
-  let _name = Piqirun.gen_optional_field 1 gen__string x.Value_info_proto.name in
-  let _type_ = Piqirun.gen_optional_field 2 gen__type_proto x.Value_info_proto.type_ in
-  let _doc_string = Piqirun.gen_optional_field 3 gen__string x.Value_info_proto.doc_string in
-  Piqirun.gen_record code (_name :: _type_ :: _doc_string :: [])
-
-and gen__node_proto code x =
-  let _input = Piqirun.gen_repeated_field 1 gen__string x.Node_proto.input in
-  let _output = Piqirun.gen_repeated_field 2 gen__string x.Node_proto.output in
-  let _name = Piqirun.gen_optional_field 3 gen__string x.Node_proto.name in
-  let _op_type = Piqirun.gen_optional_field 4 gen__string x.Node_proto.op_type in
-  let _attribute = Piqirun.gen_repeated_field 5 gen__attribute_proto x.Node_proto.attribute in
-  let _doc_string = Piqirun.gen_optional_field 6 gen__string x.Node_proto.doc_string in
-  let _domain = Piqirun.gen_optional_field 7 gen__string x.Node_proto.domain in
-  Piqirun.gen_record code (_input :: _output :: _name :: _op_type :: _attribute :: _doc_string :: _domain :: [])
-
-and gen__training_info_proto code x =
-  let _initialization = Piqirun.gen_optional_field 1 gen__graph_proto x.Training_info_proto.initialization in
-  let _algorithm = Piqirun.gen_optional_field 2 gen__graph_proto x.Training_info_proto.algorithm in
-  let _initialization_binding = Piqirun.gen_repeated_field 3 gen__string_string_entry_proto x.Training_info_proto.initialization_binding in
-  let _update_binding = Piqirun.gen_repeated_field 4 gen__string_string_entry_proto x.Training_info_proto.update_binding in
-  Piqirun.gen_record code (_initialization :: _algorithm :: _initialization_binding :: _update_binding :: [])
-
-and gen__model_proto code x =
-  let _ir_version = Piqirun.gen_optional_field 1 gen__protobuf_int64 x.Model_proto.ir_version in
-  let _producer_name = Piqirun.gen_optional_field 2 gen__string x.Model_proto.producer_name in
-  let _producer_version = Piqirun.gen_optional_field 3 gen__string x.Model_proto.producer_version in
-  let _domain = Piqirun.gen_optional_field 4 gen__string x.Model_proto.domain in
-  let _model_version = Piqirun.gen_optional_field 5 gen__protobuf_int64 x.Model_proto.model_version in
-  let _doc_string = Piqirun.gen_optional_field 6 gen__string x.Model_proto.doc_string in
-  let _graph = Piqirun.gen_optional_field 7 gen__graph_proto x.Model_proto.graph in
-  let _opset_import = Piqirun.gen_repeated_field 8 gen__operator_set_id_proto x.Model_proto.opset_import in
-  let _metadata_props = Piqirun.gen_repeated_field 14 gen__string_string_entry_proto x.Model_proto.metadata_props in
-  let _training_info = Piqirun.gen_repeated_field 20 gen__training_info_proto x.Model_proto.training_info in
-  let _functions = Piqirun.gen_repeated_field 25 gen__function_proto x.Model_proto.functions in
-  Piqirun.gen_record code (_ir_version :: _producer_name :: _producer_version :: _domain :: _model_version :: _doc_string :: _graph :: _opset_import :: _metadata_props :: _training_info :: _functions :: [])
-
-and gen__string_string_entry_proto code x =
-  let _key = Piqirun.gen_optional_field 1 gen__string x.String_string_entry_proto.key in
-  let _value = Piqirun.gen_optional_field 2 gen__string x.String_string_entry_proto.value in
-  Piqirun.gen_record code (_key :: _value :: [])
-
-and gen__tensor_annotation code x =
-  let _tensor_name = Piqirun.gen_optional_field 1 gen__string x.Tensor_annotation.tensor_name in
-  let _quant_parameter_tensor_names = Piqirun.gen_repeated_field 2 gen__string_string_entry_proto x.Tensor_annotation.quant_parameter_tensor_names in
-  Piqirun.gen_record code (_tensor_name :: _quant_parameter_tensor_names :: [])
-
-and gen__graph_proto code x =
-  let _node = Piqirun.gen_repeated_field 1 gen__node_proto x.Graph_proto.node in
-  let _name = Piqirun.gen_optional_field 2 gen__string x.Graph_proto.name in
-  let _initializer_ = Piqirun.gen_repeated_field 5 gen__tensor_proto x.Graph_proto.initializer_ in
-  let _doc_string = Piqirun.gen_optional_field 10 gen__string x.Graph_proto.doc_string in
-  let _input = Piqirun.gen_repeated_field 11 gen__value_info_proto x.Graph_proto.input in
-  let _output = Piqirun.gen_repeated_field 12 gen__value_info_proto x.Graph_proto.output in
-  let _value_info = Piqirun.gen_repeated_field 13 gen__value_info_proto x.Graph_proto.value_info in
-  let _quantization_annotation = Piqirun.gen_repeated_field 14 gen__tensor_annotation x.Graph_proto.quantization_annotation in
-  let _sparse_initializer = Piqirun.gen_repeated_field 15 gen__sparse_tensor_proto x.Graph_proto.sparse_initializer in
-  Piqirun.gen_record code (_node :: _name :: _initializer_ :: _doc_string :: _input :: _output :: _value_info :: _quantization_annotation :: _sparse_initializer :: [])
-
-and gen__tensor_proto code x =
-  let _dims = Piqirun.gen_repeated_field 1 gen__protobuf_int64 x.Tensor_proto.dims in
-  let _data_type = Piqirun.gen_optional_field 2 gen__protobuf_int32 x.Tensor_proto.data_type in
-  let _segment = Piqirun.gen_optional_field 3 gen__tensor_proto_segment x.Tensor_proto.segment in
-  let _float_data = Piqirun.gen_packed_repeated_field 4 packed_gen__float32 x.Tensor_proto.float_data in
-  let _int32_data = Piqirun.gen_packed_repeated_field 5 packed_gen__protobuf_int32 x.Tensor_proto.int32_data in
-  let _string_data = Piqirun.gen_repeated_field 6 gen__binary x.Tensor_proto.string_data in
-  let _int64_data = Piqirun.gen_packed_repeated_field 7 packed_gen__protobuf_int64 x.Tensor_proto.int64_data in
-  let _name = Piqirun.gen_optional_field 8 gen__string x.Tensor_proto.name in
-  let _raw_data = Piqirun.gen_optional_field 9 gen__binary x.Tensor_proto.raw_data in
-  let _double_data = Piqirun.gen_packed_repeated_field 10 packed_gen__float64 x.Tensor_proto.double_data in
-  let _uint64_data = Piqirun.gen_packed_repeated_field 11 packed_gen__uint64 x.Tensor_proto.uint64_data in
-  let _doc_string = Piqirun.gen_optional_field 12 gen__string x.Tensor_proto.doc_string in
-  let _externall_data = Piqirun.gen_repeated_field 13 gen__string_string_entry_proto x.Tensor_proto.externall_data in
-  let _data_location = Piqirun.gen_optional_field 14 gen__tensor_proto_data_location x.Tensor_proto.data_location in
-  Piqirun.gen_record code (_dims :: _data_type :: _segment :: _float_data :: _int32_data :: _string_data :: _int64_data :: _name :: _raw_data :: _double_data :: _uint64_data :: _doc_string :: _externall_data :: _data_location :: [])
-
-and gen__tensor_proto_segment code x =
-  let _begin_ = Piqirun.gen_optional_field 1 gen__protobuf_int64 x.Tensor_proto_segment.begin_ in
-  let _end_ = Piqirun.gen_optional_field 2 gen__protobuf_int64 x.Tensor_proto_segment.end_ in
-  Piqirun.gen_record code (_begin_ :: _end_ :: [])
-
-and gen__tensor_proto_data_type code x =
-  Piqirun.int32_to_signed_varint code (match x with
-    | `undefined -> 0l
-    | `float -> 1l
-    | `uint8 -> 2l
-    | `int8 -> 3l
-    | `uint16 -> 4l
-    | `int16 -> 5l
-    | `int32 -> 6l
-    | `int64 -> 7l
-    | `string -> 8l
-    | `bool -> 9l
-    | `float16 -> 10l
-    | `double -> 11l
-    | `uint32 -> 12l
-    | `uint64 -> 13l
-    | `complex64 -> 14l
-    | `complex128 -> 15l
-    | `bfloat16 -> 16l
-  )
-and packed_gen__tensor_proto_data_type x =
-  Piqirun.int32_to_packed_signed_varint (match x with
-    | `undefined -> 0l
-    | `float -> 1l
-    | `uint8 -> 2l
-    | `int8 -> 3l
-    | `uint16 -> 4l
-    | `int16 -> 5l
-    | `int32 -> 6l
-    | `int64 -> 7l
-    | `string -> 8l
-    | `bool -> 9l
-    | `float16 -> 10l
-    | `double -> 11l
-    | `uint32 -> 12l
-    | `uint64 -> 13l
-    | `complex64 -> 14l
-    | `complex128 -> 15l
-    | `bfloat16 -> 16l
-  )
-
-and gen__tensor_proto_data_location code x =
-  Piqirun.int32_to_signed_varint code (match x with
-    | `default -> 0l
-    | `externall -> 1l
-  )
-and packed_gen__tensor_proto_data_location x =
-  Piqirun.int32_to_packed_signed_varint (match x with
-    | `default -> 0l
-    | `externall -> 1l
-  )
-
-and gen__sparse_tensor_proto code x =
-  let _values = Piqirun.gen_optional_field 1 gen__tensor_proto x.Sparse_tensor_proto.values in
-  let _indices = Piqirun.gen_optional_field 2 gen__tensor_proto x.Sparse_tensor_proto.indices in
-  let _dims = Piqirun.gen_repeated_field 3 gen__protobuf_int64 x.Sparse_tensor_proto.dims in
-  Piqirun.gen_record code (_values :: _indices :: _dims :: [])
-
-and gen__tensor_shape_proto code x =
-  let _dim = Piqirun.gen_repeated_field 1 gen__tensor_shape_proto_dimension x.Tensor_shape_proto.dim in
-  Piqirun.gen_record code (_dim :: [])
-
-and gen__tensor_shape_proto_dimension code x =
-  let _dim_value = Piqirun.gen_optional_field 1 gen__protobuf_int64 x.Tensor_shape_proto_dimension.dim_value in
-  let _dim_param = Piqirun.gen_optional_field 2 gen__string x.Tensor_shape_proto_dimension.dim_param in
-  let _denotation = Piqirun.gen_optional_field 3 gen__string x.Tensor_shape_proto_dimension.denotation in
-  Piqirun.gen_record code (_dim_value :: _dim_param :: _denotation :: [])
-
-and gen__type_proto code x =
-  let _tensor_type = Piqirun.gen_optional_field 1 gen__type_proto_tensor x.Type_proto.tensor_type in
-  let _sequence_type = Piqirun.gen_optional_field 4 gen__type_proto_sequence x.Type_proto.sequence_type in
-  let _map_type = Piqirun.gen_optional_field 5 gen__type_proto_map x.Type_proto.map_type in
-  let _denotation = Piqirun.gen_optional_field 6 gen__string x.Type_proto.denotation in
-  let _sparse_tensor_type = Piqirun.gen_optional_field 8 gen__type_proto_sparse_tensor x.Type_proto.sparse_tensor_type in
-  let _optional_type = Piqirun.gen_optional_field 9 gen__type_proto_optional x.Type_proto.optional_type in
-  Piqirun.gen_record code (_tensor_type :: _sequence_type :: _map_type :: _denotation :: _sparse_tensor_type :: _optional_type :: [])
-
-and gen__type_proto_tensor code x =
-  let _elem_type = Piqirun.gen_optional_field 1 gen__protobuf_int32 x.Type_proto_tensor.elem_type in
-  let _shape = Piqirun.gen_optional_field 2 gen__tensor_shape_proto x.Type_proto_tensor.shape in
-  Piqirun.gen_record code (_elem_type :: _shape :: [])
-
-and gen__type_proto_sequence code x =
-  let _elem_type = Piqirun.gen_optional_field 1 gen__type_proto x.Type_proto_sequence.elem_type in
-  Piqirun.gen_record code (_elem_type :: [])
-
-and gen__type_proto_map code x =
-  let _key_type = Piqirun.gen_optional_field 1 gen__protobuf_int32 x.Type_proto_map.key_type in
-  let _value_type = Piqirun.gen_optional_field 2 gen__type_proto x.Type_proto_map.value_type in
-  Piqirun.gen_record code (_key_type :: _value_type :: [])
-
-and gen__type_proto_optional code x =
-  let _elem_type = Piqirun.gen_optional_field 1 gen__type_proto x.Type_proto_optional.elem_type in
-  Piqirun.gen_record code (_elem_type :: [])
-
-and gen__type_proto_sparse_tensor code x =
-  let _elem_type = Piqirun.gen_optional_field 1 gen__protobuf_int32 x.Type_proto_sparse_tensor.elem_type in
-  let _shape = Piqirun.gen_optional_field 2 gen__tensor_shape_proto x.Type_proto_sparse_tensor.shape in
-  Piqirun.gen_record code (_elem_type :: _shape :: [])
-
-and gen__operator_set_id_proto code x =
-  let _domain = Piqirun.gen_optional_field 1 gen__string x.Operator_set_id_proto.domain in
-  let _version = Piqirun.gen_optional_field 2 gen__protobuf_int64 x.Operator_set_id_proto.version in
-  Piqirun.gen_record code (_domain :: _version :: [])
-
-and gen__function_proto code x =
-  let _name = Piqirun.gen_optional_field 1 gen__string x.Function_proto.name in
-  let _input = Piqirun.gen_repeated_field 4 gen__string x.Function_proto.input in
-  let _output = Piqirun.gen_repeated_field 5 gen__string x.Function_proto.output in
-  let _attribute = Piqirun.gen_repeated_field 6 gen__string x.Function_proto.attribute in
-  let _node = Piqirun.gen_repeated_field 7 gen__node_proto x.Function_proto.node in
-  let _doc_string = Piqirun.gen_optional_field 8 gen__string x.Function_proto.doc_string in
-  let _opset_import = Piqirun.gen_repeated_field 9 gen__operator_set_id_proto x.Function_proto.opset_import in
-  let _domain = Piqirun.gen_optional_field 10 gen__string x.Function_proto.domain in
-  Piqirun.gen_record code (_name :: _input :: _output :: _attribute :: _node :: _doc_string :: _opset_import :: _domain :: [])
-
-and gen__version code x =
-  Piqirun.int32_to_signed_varint code (match x with
-    | `start_version -> 0l
-    | `ir_version_2017_10_10 -> 1l
-    | `ir_version_2017_10_30 -> 2l
-    | `ir_version_2017_11_3 -> 3l
-    | `ir_version_2019_1_22 -> 4l
-    | `ir_version_2019_3_18 -> 5l
-    | `ir_version_2019_9_19 -> 6l
-    | `ir_version_2020_5_8 -> 7l
-    | `ir_version -> 8l
-  )
-and packed_gen__version x =
-  Piqirun.int32_to_packed_signed_varint (match x with
-    | `start_version -> 0l
-    | `ir_version_2017_10_10 -> 1l
-    | `ir_version_2017_10_30 -> 2l
-    | `ir_version_2017_11_3 -> 3l
-    | `ir_version_2019_1_22 -> 4l
-    | `ir_version_2019_3_18 -> 5l
-    | `ir_version_2019_9_19 -> 6l
-    | `ir_version_2020_5_8 -> 7l
-    | `ir_version -> 8l
-  )
-
-and gen__operator_status code x =
-  Piqirun.int32_to_signed_varint code (match x with
-    | `experimental -> 0l
-    | `stable -> 1l
-  )
-and packed_gen__operator_status x =
-  Piqirun.int32_to_packed_signed_varint (match x with
-    | `experimental -> 0l
-    | `stable -> 1l
-  )
-
-
-let gen_int64 x = gen__int64 (-1) x
-let gen_int32 x = gen__int32 (-1) x
-let gen_string x = gen__string (-1) x
-let gen_float32 x = gen__float32 (-1) x
-let gen_protobuf_int64 x = gen__protobuf_int64 (-1) x
-let gen_binary x = gen__binary (-1) x
-let gen_protobuf_int32 x = gen__protobuf_int32 (-1) x
-let gen_float64 x = gen__float64 (-1) x
-let gen_uint64 x = gen__uint64 (-1) x
-let gen_attribute_proto x = gen__attribute_proto (-1) x
-let gen_attribute_proto_attribute_type x = gen__attribute_proto_attribute_type (-1) x
-let gen_value_info_proto x = gen__value_info_proto (-1) x
-let gen_node_proto x = gen__node_proto (-1) x
-let gen_training_info_proto x = gen__training_info_proto (-1) x
-let gen_model_proto x = gen__model_proto (-1) x
-let gen_string_string_entry_proto x = gen__string_string_entry_proto (-1) x
-let gen_tensor_annotation x = gen__tensor_annotation (-1) x
-let gen_graph_proto x = gen__graph_proto (-1) x
-let gen_tensor_proto x = gen__tensor_proto (-1) x
-let gen_tensor_proto_segment x = gen__tensor_proto_segment (-1) x
-let gen_tensor_proto_data_type x = gen__tensor_proto_data_type (-1) x
-let gen_tensor_proto_data_location x = gen__tensor_proto_data_location (-1) x
-let gen_sparse_tensor_proto x = gen__sparse_tensor_proto (-1) x
-let gen_tensor_shape_proto x = gen__tensor_shape_proto (-1) x
-let gen_tensor_shape_proto_dimension x = gen__tensor_shape_proto_dimension (-1) x
-let gen_type_proto x = gen__type_proto (-1) x
-let gen_type_proto_tensor x = gen__type_proto_tensor (-1) x
-let gen_type_proto_sequence x = gen__type_proto_sequence (-1) x
-let gen_type_proto_map x = gen__type_proto_map (-1) x
-let gen_type_proto_optional x = gen__type_proto_optional (-1) x
-let gen_type_proto_sparse_tensor x = gen__type_proto_sparse_tensor (-1) x
-let gen_operator_set_id_proto x = gen__operator_set_id_proto (-1) x
-let gen_function_proto x = gen__function_proto (-1) x
-let gen_version x = gen__version (-1) x
-let gen_operator_status x = gen__operator_status (-1) x
-
-
-let rec default_int64 () = 0L
-and default_int32 () = 0l
-and default_string () = ""
-and default_float32 () = 0.0
-and default_protobuf_int64 () = default_int64 ()
-and default_binary () = ""
-and default_protobuf_int32 () = default_int32 ()
-and default_float64 () = 0.0
-and default_uint64 () = 0L
-and default_attribute_proto () =
-  {
-    Attribute_proto.name = None;
-    Attribute_proto.f = None;
-    Attribute_proto.i = None;
-    Attribute_proto.s = None;
-    Attribute_proto.t = None;
-    Attribute_proto.g = None;
-    Attribute_proto.floats = [];
-    Attribute_proto.ints = [];
-    Attribute_proto.strings = [];
-    Attribute_proto.tensors = [];
-    Attribute_proto.graphs = [];
-    Attribute_proto.doc_string = None;
-    Attribute_proto.tp = None;
-    Attribute_proto.type_protos = [];
-    Attribute_proto.type_ = None;
-    Attribute_proto.ref_attr_name = None;
-    Attribute_proto.sparse_tensor = None;
-    Attribute_proto.sparse_tensors = [];
-  }
-and default_attribute_proto_attribute_type () = `undefined
-and default_value_info_proto () =
-  {
-    Value_info_proto.name = None;
-    Value_info_proto.type_ = None;
-    Value_info_proto.doc_string = None;
-  }
-and default_node_proto () =
-  {
-    Node_proto.input = [];
-    Node_proto.output = [];
-    Node_proto.name = None;
-    Node_proto.op_type = None;
-    Node_proto.attribute = [];
-    Node_proto.doc_string = None;
-    Node_proto.domain = None;
-  }
-and default_training_info_proto () =
-  {
-    Training_info_proto.initialization = None;
-    Training_info_proto.algorithm = None;
-    Training_info_proto.initialization_binding = [];
-    Training_info_proto.update_binding = [];
-  }
-and default_model_proto () =
-  {
-    Model_proto.ir_version = None;
-    Model_proto.producer_name = None;
-    Model_proto.producer_version = None;
-    Model_proto.domain = None;
-    Model_proto.model_version = None;
-    Model_proto.doc_string = None;
-    Model_proto.graph = None;
-    Model_proto.opset_import = [];
-    Model_proto.metadata_props = [];
-    Model_proto.training_info = [];
-    Model_proto.functions = [];
-  }
-and default_string_string_entry_proto () =
-  {
-    String_string_entry_proto.key = None;
-    String_string_entry_proto.value = None;
-  }
-and default_tensor_annotation () =
-  {
-    Tensor_annotation.tensor_name = None;
-    Tensor_annotation.quant_parameter_tensor_names = [];
-  }
-and default_graph_proto () =
-  {
-    Graph_proto.node = [];
-    Graph_proto.name = None;
-    Graph_proto.initializer_ = [];
-    Graph_proto.doc_string = None;
-    Graph_proto.input = [];
-    Graph_proto.output = [];
-    Graph_proto.value_info = [];
-    Graph_proto.quantization_annotation = [];
-    Graph_proto.sparse_initializer = [];
-  }
-and default_tensor_proto () =
-  {
-    Tensor_proto.dims = [];
-    Tensor_proto.data_type = None;
-    Tensor_proto.segment = None;
-    Tensor_proto.float_data = [];
-    Tensor_proto.int32_data = [];
-    Tensor_proto.string_data = [];
-    Tensor_proto.int64_data = [];
-    Tensor_proto.name = None;
-    Tensor_proto.raw_data = None;
-    Tensor_proto.double_data = [];
-    Tensor_proto.uint64_data = [];
-    Tensor_proto.doc_string = None;
-    Tensor_proto.externall_data = [];
-    Tensor_proto.data_location = None;
-  }
-and default_tensor_proto_segment () =
-  {
-    Tensor_proto_segment.begin_ = None;
-    Tensor_proto_segment.end_ = None;
-  }
-and default_tensor_proto_data_type () = `undefined
-and default_tensor_proto_data_location () = `default
-and default_sparse_tensor_proto () =
-  {
-    Sparse_tensor_proto.values = None;
-    Sparse_tensor_proto.indices = None;
-    Sparse_tensor_proto.dims = [];
-  }
-and default_tensor_shape_proto () =
-  {
-    Tensor_shape_proto.dim = [];
-  }
-and default_tensor_shape_proto_dimension () =
-  {
-    Tensor_shape_proto_dimension.dim_value = None;
-    Tensor_shape_proto_dimension.dim_param = None;
-    Tensor_shape_proto_dimension.denotation = None;
-  }
-and default_type_proto () =
-  {
-    Type_proto.tensor_type = None;
-    Type_proto.sequence_type = None;
-    Type_proto.map_type = None;
-    Type_proto.denotation = None;
-    Type_proto.sparse_tensor_type = None;
-    Type_proto.optional_type = None;
-  }
-and default_type_proto_tensor () =
-  {
-    Type_proto_tensor.elem_type = None;
-    Type_proto_tensor.shape = None;
-  }
-and default_type_proto_sequence () =
-  {
-    Type_proto_sequence.elem_type = None;
-  }
-and default_type_proto_map () =
-  {
-    Type_proto_map.key_type = None;
-    Type_proto_map.value_type = None;
-  }
-and default_type_proto_optional () =
-  {
-    Type_proto_optional.elem_type = None;
-  }
-and default_type_proto_sparse_tensor () =
-  {
-    Type_proto_sparse_tensor.elem_type = None;
-    Type_proto_sparse_tensor.shape = None;
-  }
-and default_operator_set_id_proto () =
-  {
-    Operator_set_id_proto.domain = None;
-    Operator_set_id_proto.version = None;
-  }
-and default_function_proto () =
-  {
-    Function_proto.name = None;
-    Function_proto.input = [];
-    Function_proto.output = [];
-    Function_proto.attribute = [];
-    Function_proto.node = [];
-    Function_proto.doc_string = None;
-    Function_proto.opset_import = [];
-    Function_proto.domain = None;
-  }
-and default_version () = `start_version
-and default_operator_status () = `experimental
-
-
-include Onnx_piqi
diff --git a/onnx_piqi.mli b/onnx_piqi.mli
deleted file mode 100644
index 97ea99f4..00000000
--- a/onnx_piqi.mli
+++ /dev/null
@@ -1,718 +0,0 @@
-module rec Onnx_piqi :
-  sig
-    type float32 = float
-    type float64 = float
-    type uint64 = int64
-    type protobuf_int64 = int64
-    type binary = string
-    type protobuf_int32 = int32
-    type attribute_proto_attribute_type =
-        [ `float
-        | `floats
-        | `graph
-        | `graphs
-        | `int
-        | `ints
-        | `sparse_tensor
-        | `sparse_tensors
-        | `string
-        | `strings
-        | `tensor
-        | `tensors
-        | `type_proto
-        | `type_protos
-        | `undefined ]
-    type tensor_proto_data_type =
-        [ `bfloat16
-        | `bool
-        | `complex128
-        | `complex64
-        | `double
-        | `float
-        | `float16
-        | `int16
-        | `int32
-        | `int64
-        | `int8
-        | `string
-        | `uint16
-        | `uint32
-        | `uint64
-        | `uint8
-        | `undefined ]
-    type tensor_proto_data_location = [ `default | `externall ]
-    type version =
-        [ `ir_version
-        | `ir_version_2017_10_10
-        | `ir_version_2017_10_30
-        | `ir_version_2017_11_3
-        | `ir_version_2019_1_22
-        | `ir_version_2019_3_18
-        | `ir_version_2019_9_19
-        | `ir_version_2020_5_8
-        | `start_version ]
-    type operator_status = [ `experimental | `stable ]
-    type attribute_proto = Attribute_proto.t
-    type value_info_proto = Value_info_proto.t
-    type node_proto = Node_proto.t
-    type training_info_proto = Training_info_proto.t
-    type model_proto = Model_proto.t
-    type string_string_entry_proto = String_string_entry_proto.t
-    type tensor_annotation = Tensor_annotation.t
-    type graph_proto = Graph_proto.t
-    type tensor_proto = Tensor_proto.t
-    type tensor_proto_segment = Tensor_proto_segment.t
-    type sparse_tensor_proto = Sparse_tensor_proto.t
-    type tensor_shape_proto = Tensor_shape_proto.t
-    type tensor_shape_proto_dimension = Tensor_shape_proto_dimension.t
-    type type_proto = Type_proto.t
-    type type_proto_tensor = Type_proto_tensor.t
-    type type_proto_sequence = Type_proto_sequence.t
-    type type_proto_map = Type_proto_map.t
-    type type_proto_optional = Type_proto_optional.t
-    type type_proto_sparse_tensor = Type_proto_sparse_tensor.t
-    type operator_set_id_proto = Operator_set_id_proto.t
-    type function_proto = Function_proto.t
-  end
-and Attribute_proto :
-  sig
-    type t = {
-      mutable name : string option;
-      mutable ref_attr_name : string option;
-      mutable doc_string : string option;
-      mutable type_ : Onnx_piqi.attribute_proto_attribute_type option;
-      mutable f : Onnx_piqi.float32 option;
-      mutable i : Onnx_piqi.protobuf_int64 option;
-      mutable s : Onnx_piqi.binary option;
-      mutable t : Onnx_piqi.tensor_proto option;
-      mutable g : Onnx_piqi.graph_proto option;
-      mutable sparse_tensor : Onnx_piqi.sparse_tensor_proto option;
-      mutable tp : Onnx_piqi.type_proto option;
-      mutable floats : Onnx_piqi.float32 list;
-      mutable ints : Onnx_piqi.protobuf_int64 list;
-      mutable strings : Onnx_piqi.binary list;
-      mutable tensors : Onnx_piqi.tensor_proto list;
-      mutable graphs : Onnx_piqi.graph_proto list;
-      mutable sparse_tensors : Onnx_piqi.sparse_tensor_proto list;
-      mutable type_protos : Onnx_piqi.type_proto list;
-    }
-  end
-and Value_info_proto :
-  sig
-    type t = {
-      mutable name : string option;
-      mutable type_ : Onnx_piqi.type_proto option;
-      mutable doc_string : string option;
-    }
-  end
-and Node_proto :
-  sig
-    type t = {
-      mutable input : string list;
-      mutable output : string list;
-      mutable name : string option;
-      mutable op_type : string option;
-      mutable domain : string option;
-      mutable attribute : Onnx_piqi.attribute_proto list;
-      mutable doc_string : string option;
-    }
-  end
-and Training_info_proto :
-  sig
-    type t = {
-      mutable initialization : Onnx_piqi.graph_proto option;
-      mutable algorithm : Onnx_piqi.graph_proto option;
-      mutable initialization_binding :
-        Onnx_piqi.string_string_entry_proto list;
-      mutable update_binding : Onnx_piqi.string_string_entry_proto list;
-    }
-  end
-and Model_proto :
-  sig
-    type t = {
-      mutable ir_version : Onnx_piqi.protobuf_int64 option;
-      mutable opset_import : Onnx_piqi.operator_set_id_proto list;
-      mutable producer_name : string option;
-      mutable producer_version : string option;
-      mutable domain : string option;
-      mutable model_version : Onnx_piqi.protobuf_int64 option;
-      mutable doc_string : string option;
-      mutable graph : Onnx_piqi.graph_proto option;
-      mutable metadata_props : Onnx_piqi.string_string_entry_proto list;
-      mutable training_info : Onnx_piqi.training_info_proto list;
-      mutable functions : Onnx_piqi.function_proto list;
-    }
-  end
-and String_string_entry_proto :
-  sig
-    type t = { mutable key : string option; mutable value : string option; }
-  end
-and Tensor_annotation :
-  sig
-    type t = {
-      mutable tensor_name : string option;
-      mutable quant_parameter_tensor_names :
-        Onnx_piqi.string_string_entry_proto list;
-    }
-  end
-and Graph_proto :
-  sig
-    type t = {
-      mutable node : Onnx_piqi.node_proto list;
-      mutable name : string option;
-      mutable initializer_ : Onnx_piqi.tensor_proto list;
-      mutable sparse_initializer : Onnx_piqi.sparse_tensor_proto list;
-      mutable doc_string : string option;
-      mutable input : Onnx_piqi.value_info_proto list;
-      mutable output : Onnx_piqi.value_info_proto list;
-      mutable value_info : Onnx_piqi.value_info_proto list;
-      mutable quantization_annotation : Onnx_piqi.tensor_annotation list;
-    }
-  end
-and Tensor_proto :
-  sig
-    type t = {
-      mutable dims : Onnx_piqi.protobuf_int64 list;
-      mutable data_type : Onnx_piqi.protobuf_int32 option;
-      mutable segment : Onnx_piqi.tensor_proto_segment option;
-      mutable float_data : Onnx_piqi.float32 list;
-      mutable int32_data : Onnx_piqi.protobuf_int32 list;
-      mutable string_data : Onnx_piqi.binary list;
-      mutable int64_data : Onnx_piqi.protobuf_int64 list;
-      mutable name : string option;
-      mutable doc_string : string option;
-      mutable raw_data : Onnx_piqi.binary option;
-      mutable externall_data : Onnx_piqi.string_string_entry_proto list;
-      mutable data_location : Onnx_piqi.tensor_proto_data_location option;
-      mutable double_data : Onnx_piqi.float64 list;
-      mutable uint64_data : Onnx_piqi.uint64 list;
-    }
-  end
-and Tensor_proto_segment :
-  sig
-    type t = {
-      mutable begin_ : Onnx_piqi.protobuf_int64 option;
-      mutable end_ : Onnx_piqi.protobuf_int64 option;
-    }
-  end
-and Sparse_tensor_proto :
-  sig
-    type t = {
-      mutable values : Onnx_piqi.tensor_proto option;
-      mutable indices : Onnx_piqi.tensor_proto option;
-      mutable dims : Onnx_piqi.protobuf_int64 list;
-    }
-  end
-and Tensor_shape_proto :
-  sig
-    type t = { mutable dim : Onnx_piqi.tensor_shape_proto_dimension list; }
-  end
-and Tensor_shape_proto_dimension :
-  sig
-    type t = {
-      mutable dim_value : Onnx_piqi.protobuf_int64 option;
-      mutable dim_param : string option;
-      mutable denotation : string option;
-    }
-  end
-and Type_proto :
-  sig
-    type t = {
-      mutable tensor_type : Onnx_piqi.type_proto_tensor option;
-      mutable sequence_type : Onnx_piqi.type_proto_sequence option;
-      mutable map_type : Onnx_piqi.type_proto_map option;
-      mutable optional_type : Onnx_piqi.type_proto_optional option;
-      mutable sparse_tensor_type : Onnx_piqi.type_proto_sparse_tensor option;
-      mutable denotation : string option;
-    }
-  end
-and Type_proto_tensor :
-  sig
-    type t = {
-      mutable elem_type : Onnx_piqi.protobuf_int32 option;
-      mutable shape : Onnx_piqi.tensor_shape_proto option;
-    }
-  end
-and Type_proto_sequence :
-  sig type t = { mutable elem_type : Onnx_piqi.type_proto option; } end
-and Type_proto_map :
-  sig
-    type t = {
-      mutable key_type : Onnx_piqi.protobuf_int32 option;
-      mutable value_type : Onnx_piqi.type_proto option;
-    }
-  end
-and Type_proto_optional :
-  sig type t = { mutable elem_type : Onnx_piqi.type_proto option; } end
-and Type_proto_sparse_tensor :
-  sig
-    type t = {
-      mutable elem_type : Onnx_piqi.protobuf_int32 option;
-      mutable shape : Onnx_piqi.tensor_shape_proto option;
-    }
-  end
-and Operator_set_id_proto :
-  sig
-    type t = {
-      mutable domain : string option;
-      mutable version : Onnx_piqi.protobuf_int64 option;
-    }
-  end
-and Function_proto :
-  sig
-    type t = {
-      mutable name : string option;
-      mutable input : string list;
-      mutable output : string list;
-      mutable attribute : string list;
-      mutable node : Onnx_piqi.node_proto list;
-      mutable doc_string : string option;
-      mutable opset_import : Onnx_piqi.operator_set_id_proto list;
-      mutable domain : string option;
-    }
-  end
-val parse_int64 : Piqirun.t -> int64
-val packed_parse_int64 : Piqirun.IBuf.t -> int64
-val parse_int32 : Piqirun.t -> int32
-val packed_parse_int32 : Piqirun.IBuf.t -> int32
-val parse_string : Piqirun.t -> string
-val parse_float32 : Piqirun.t -> Onnx_piqi.float32
-val packed_parse_float32 : Piqirun.IBuf.t -> Onnx_piqi.float32
-val parse_protobuf_int64 : Piqirun.t -> Onnx_piqi.protobuf_int64
-val packed_parse_protobuf_int64 : Piqirun.IBuf.t -> Onnx_piqi.protobuf_int64
-val parse_binary : Piqirun.t -> Onnx_piqi.binary
-val parse_protobuf_int32 : Piqirun.t -> Onnx_piqi.protobuf_int32
-val packed_parse_protobuf_int32 : Piqirun.IBuf.t -> Onnx_piqi.protobuf_int32
-val parse_float64 : Piqirun.t -> Onnx_piqi.float64
-val packed_parse_float64 : Piqirun.IBuf.t -> Onnx_piqi.float64
-val parse_uint64 : Piqirun.t -> Onnx_piqi.uint64
-val packed_parse_uint64 : Piqirun.IBuf.t -> Onnx_piqi.uint64
-val parse_attribute_proto : Piqirun.t -> Onnx_piqi.attribute_proto
-val parse_attribute_proto_attribute_type :
-  Piqirun.t -> Onnx_piqi.attribute_proto_attribute_type
-val packed_parse_attribute_proto_attribute_type :
-  Piqirun.IBuf.t ->
-  [> `float
-   | `floats
-   | `graph
-   | `graphs
-   | `int
-   | `ints
-   | `sparse_tensor
-   | `sparse_tensors
-   | `string
-   | `strings
-   | `tensor
-   | `tensors
-   | `type_proto
-   | `type_protos
-   | `undefined ]
-val parse_value_info_proto : Piqirun.t -> Onnx_piqi.value_info_proto
-val parse_node_proto : Piqirun.t -> Onnx_piqi.node_proto
-val parse_training_info_proto : Piqirun.t -> Onnx_piqi.training_info_proto
-val parse_model_proto : Piqirun.t -> Model_proto.t
-val parse_string_string_entry_proto :
-  Piqirun.t -> Onnx_piqi.string_string_entry_proto
-val parse_tensor_annotation : Piqirun.t -> Onnx_piqi.tensor_annotation
-val parse_graph_proto : Piqirun.t -> Onnx_piqi.graph_proto
-val parse_tensor_proto : Piqirun.t -> Onnx_piqi.tensor_proto
-val parse_tensor_proto_segment : Piqirun.t -> Onnx_piqi.tensor_proto_segment
-val parse_tensor_proto_data_type :
-  Piqirun.t ->
-  [> `bfloat16
-   | `bool
-   | `complex128
-   | `complex64
-   | `double
-   | `float
-   | `float16
-   | `int16
-   | `int32
-   | `int64
-   | `int8
-   | `string
-   | `uint16
-   | `uint32
-   | `uint64
-   | `uint8
-   | `undefined ]
-val packed_parse_tensor_proto_data_type :
-  Piqirun.IBuf.t ->
-  [> `bfloat16
-   | `bool
-   | `complex128
-   | `complex64
-   | `double
-   | `float
-   | `float16
-   | `int16
-   | `int32
-   | `int64
-   | `int8
-   | `string
-   | `uint16
-   | `uint32
-   | `uint64
-   | `uint8
-   | `undefined ]
-val parse_tensor_proto_data_location :
-  Piqirun.t -> Onnx_piqi.tensor_proto_data_location
-val packed_parse_tensor_proto_data_location :
-  Piqirun.IBuf.t -> [> `default | `externall ]
-val parse_sparse_tensor_proto : Piqirun.t -> Onnx_piqi.sparse_tensor_proto
-val parse_tensor_shape_proto : Piqirun.t -> Onnx_piqi.tensor_shape_proto
-val parse_tensor_shape_proto_dimension :
-  Piqirun.t -> Onnx_piqi.tensor_shape_proto_dimension
-val parse_type_proto : Piqirun.t -> Onnx_piqi.type_proto
-val parse_type_proto_tensor : Piqirun.t -> Onnx_piqi.type_proto_tensor
-val parse_type_proto_sequence : Piqirun.t -> Onnx_piqi.type_proto_sequence
-val parse_type_proto_map : Piqirun.t -> Onnx_piqi.type_proto_map
-val parse_type_proto_optional : Piqirun.t -> Onnx_piqi.type_proto_optional
-val parse_type_proto_sparse_tensor :
-  Piqirun.t -> Onnx_piqi.type_proto_sparse_tensor
-val parse_operator_set_id_proto :
-  Piqirun.t -> Onnx_piqi.operator_set_id_proto
-val parse_function_proto : Piqirun.t -> Onnx_piqi.function_proto
-val parse_version :
-  Piqirun.t ->
-  [> `ir_version
-   | `ir_version_2017_10_10
-   | `ir_version_2017_10_30
-   | `ir_version_2017_11_3
-   | `ir_version_2019_1_22
-   | `ir_version_2019_3_18
-   | `ir_version_2019_9_19
-   | `ir_version_2020_5_8
-   | `start_version ]
-val packed_parse_version :
-  Piqirun.IBuf.t ->
-  [> `ir_version
-   | `ir_version_2017_10_10
-   | `ir_version_2017_10_30
-   | `ir_version_2017_11_3
-   | `ir_version_2019_1_22
-   | `ir_version_2019_3_18
-   | `ir_version_2019_9_19
-   | `ir_version_2020_5_8
-   | `start_version ]
-val parse_operator_status : Piqirun.t -> [> `experimental | `stable ]
-val packed_parse_operator_status :
-  Piqirun.IBuf.t -> [> `experimental | `stable ]
-val gen__int64 : int -> int64 -> Piqirun.OBuf.t
-val packed_gen__int64 : int64 -> Piqirun.OBuf.t
-val gen__int32 : int -> int32 -> Piqirun.OBuf.t
-val packed_gen__int32 : int32 -> Piqirun.OBuf.t
-val gen__string : int -> string -> Piqirun.OBuf.t
-val gen__float32 : int -> Onnx_piqi.float32 -> Piqirun.OBuf.t
-val packed_gen__float32 : Onnx_piqi.float32 -> Piqirun.OBuf.t
-val gen__protobuf_int64 : int -> Onnx_piqi.protobuf_int64 -> Piqirun.OBuf.t
-val packed_gen__protobuf_int64 : Onnx_piqi.protobuf_int64 -> Piqirun.OBuf.t
-val gen__binary : int -> Onnx_piqi.binary -> Piqirun.OBuf.t
-val gen__protobuf_int32 : int -> Int32.t -> Piqirun.OBuf.t
-val packed_gen__protobuf_int32 : Int32.t -> Piqirun.OBuf.t
-val gen__float64 : int -> float -> Piqirun.OBuf.t
-val packed_gen__float64 : Onnx_piqi.float64 -> Piqirun.OBuf.t
-val gen__uint64 : int -> int64 -> Piqirun.OBuf.t
-val packed_gen__uint64 : Onnx_piqi.uint64 -> Piqirun.OBuf.t
-val gen__attribute_proto : int -> Onnx_piqi.attribute_proto -> Piqirun.OBuf.t
-val gen__attribute_proto_attribute_type :
-  int -> Onnx_piqi.attribute_proto_attribute_type -> Piqirun.OBuf.t
-val packed_gen__attribute_proto_attribute_type :
-  [< `float
-   | `floats
-   | `graph
-   | `graphs
-   | `int
-   | `ints
-   | `sparse_tensor
-   | `sparse_tensors
-   | `string
-   | `strings
-   | `tensor
-   | `tensors
-   | `type_proto
-   | `type_protos
-   | `undefined ] ->
-  Piqirun.OBuf.t
-val gen__value_info_proto :
-  int -> Onnx_piqi.value_info_proto -> Piqirun.OBuf.t
-val gen__node_proto : int -> Onnx_piqi.node_proto -> Piqirun.OBuf.t
-val gen__training_info_proto :
-  int -> Onnx_piqi.training_info_proto -> Piqirun.OBuf.t
-val gen__model_proto : int -> Model_proto.t -> Piqirun.OBuf.t
-val gen__string_string_entry_proto :
-  int -> Onnx_piqi.string_string_entry_proto -> Piqirun.OBuf.t
-val gen__tensor_annotation :
-  int -> Onnx_piqi.tensor_annotation -> Piqirun.OBuf.t
-val gen__graph_proto : int -> Onnx_piqi.graph_proto -> Piqirun.OBuf.t
-val gen__tensor_proto : int -> Onnx_piqi.tensor_proto -> Piqirun.OBuf.t
-val gen__tensor_proto_segment :
-  int -> Onnx_piqi.tensor_proto_segment -> Piqirun.OBuf.t
-val gen__tensor_proto_data_type :
-  int ->
-  [< `bfloat16
-   | `bool
-   | `complex128
-   | `complex64
-   | `double
-   | `float
-   | `float16
-   | `int16
-   | `int32
-   | `int64
-   | `int8
-   | `string
-   | `uint16
-   | `uint32
-   | `uint64
-   | `uint8
-   | `undefined ] ->
-  Piqirun.OBuf.t
-val packed_gen__tensor_proto_data_type :
-  [< `bfloat16
-   | `bool
-   | `complex128
-   | `complex64
-   | `double
-   | `float
-   | `float16
-   | `int16
-   | `int32
-   | `int64
-   | `int8
-   | `string
-   | `uint16
-   | `uint32
-   | `uint64
-   | `uint8
-   | `undefined ] ->
-  Piqirun.OBuf.t
-val gen__tensor_proto_data_location :
-  int -> Onnx_piqi.tensor_proto_data_location -> Piqirun.OBuf.t
-val packed_gen__tensor_proto_data_location :
-  [< `default | `externall ] -> Piqirun.OBuf.t
-val gen__sparse_tensor_proto :
-  int -> Onnx_piqi.sparse_tensor_proto -> Piqirun.OBuf.t
-val gen__tensor_shape_proto :
-  int -> Onnx_piqi.tensor_shape_proto -> Piqirun.OBuf.t
-val gen__tensor_shape_proto_dimension :
-  int -> Onnx_piqi.tensor_shape_proto_dimension -> Piqirun.OBuf.t
-val gen__type_proto : int -> Onnx_piqi.type_proto -> Piqirun.OBuf.t
-val gen__type_proto_tensor :
-  int -> Onnx_piqi.type_proto_tensor -> Piqirun.OBuf.t
-val gen__type_proto_sequence :
-  int -> Onnx_piqi.type_proto_sequence -> Piqirun.OBuf.t
-val gen__type_proto_map : int -> Onnx_piqi.type_proto_map -> Piqirun.OBuf.t
-val gen__type_proto_optional :
-  int -> Onnx_piqi.type_proto_optional -> Piqirun.OBuf.t
-val gen__type_proto_sparse_tensor :
-  int -> Onnx_piqi.type_proto_sparse_tensor -> Piqirun.OBuf.t
-val gen__operator_set_id_proto :
-  int -> Onnx_piqi.operator_set_id_proto -> Piqirun.OBuf.t
-val gen__function_proto : int -> Onnx_piqi.function_proto -> Piqirun.OBuf.t
-val gen__version :
-  int ->
-  [< `ir_version
-   | `ir_version_2017_10_10
-   | `ir_version_2017_10_30
-   | `ir_version_2017_11_3
-   | `ir_version_2019_1_22
-   | `ir_version_2019_3_18
-   | `ir_version_2019_9_19
-   | `ir_version_2020_5_8
-   | `start_version ] ->
-  Piqirun.OBuf.t
-val packed_gen__version :
-  [< `ir_version
-   | `ir_version_2017_10_10
-   | `ir_version_2017_10_30
-   | `ir_version_2017_11_3
-   | `ir_version_2019_1_22
-   | `ir_version_2019_3_18
-   | `ir_version_2019_9_19
-   | `ir_version_2020_5_8
-   | `start_version ] ->
-  Piqirun.OBuf.t
-val gen__operator_status :
-  int -> [< `experimental | `stable ] -> Piqirun.OBuf.t
-val packed_gen__operator_status :
-  [< `experimental | `stable ] -> Piqirun.OBuf.t
-val gen_int64 : int64 -> Piqirun.OBuf.t
-val gen_int32 : int32 -> Piqirun.OBuf.t
-val gen_string : string -> Piqirun.OBuf.t
-val gen_float32 : Onnx_piqi.float32 -> Piqirun.OBuf.t
-val gen_protobuf_int64 : Onnx_piqi.protobuf_int64 -> Piqirun.OBuf.t
-val gen_binary : Onnx_piqi.binary -> Piqirun.OBuf.t
-val gen_protobuf_int32 : Int32.t -> Piqirun.OBuf.t
-val gen_float64 : float -> Piqirun.OBuf.t
-val gen_uint64 : int64 -> Piqirun.OBuf.t
-val gen_attribute_proto : Onnx_piqi.attribute_proto -> Piqirun.OBuf.t
-val gen_attribute_proto_attribute_type :
-  Onnx_piqi.attribute_proto_attribute_type -> Piqirun.OBuf.t
-val gen_value_info_proto : Onnx_piqi.value_info_proto -> Piqirun.OBuf.t
-val gen_node_proto : Onnx_piqi.node_proto -> Piqirun.OBuf.t
-val gen_training_info_proto : Onnx_piqi.training_info_proto -> Piqirun.OBuf.t
-val gen_model_proto : Model_proto.t -> Piqirun.OBuf.t
-val gen_string_string_entry_proto :
-  Onnx_piqi.string_string_entry_proto -> Piqirun.OBuf.t
-val gen_tensor_annotation : Onnx_piqi.tensor_annotation -> Piqirun.OBuf.t
-val gen_graph_proto : Onnx_piqi.graph_proto -> Piqirun.OBuf.t
-val gen_tensor_proto : Onnx_piqi.tensor_proto -> Piqirun.OBuf.t
-val gen_tensor_proto_segment :
-  Onnx_piqi.tensor_proto_segment -> Piqirun.OBuf.t
-val gen_tensor_proto_data_type :
-  [< `bfloat16
-   | `bool
-   | `complex128
-   | `complex64
-   | `double
-   | `float
-   | `float16
-   | `int16
-   | `int32
-   | `int64
-   | `int8
-   | `string
-   | `uint16
-   | `uint32
-   | `uint64
-   | `uint8
-   | `undefined ] ->
-  Piqirun.OBuf.t
-val gen_tensor_proto_data_location :
-  Onnx_piqi.tensor_proto_data_location -> Piqirun.OBuf.t
-val gen_sparse_tensor_proto : Onnx_piqi.sparse_tensor_proto -> Piqirun.OBuf.t
-val gen_tensor_shape_proto : Onnx_piqi.tensor_shape_proto -> Piqirun.OBuf.t
-val gen_tensor_shape_proto_dimension :
-  Onnx_piqi.tensor_shape_proto_dimension -> Piqirun.OBuf.t
-val gen_type_proto : Onnx_piqi.type_proto -> Piqirun.OBuf.t
-val gen_type_proto_tensor : Onnx_piqi.type_proto_tensor -> Piqirun.OBuf.t
-val gen_type_proto_sequence : Onnx_piqi.type_proto_sequence -> Piqirun.OBuf.t
-val gen_type_proto_map : Onnx_piqi.type_proto_map -> Piqirun.OBuf.t
-val gen_type_proto_optional : Onnx_piqi.type_proto_optional -> Piqirun.OBuf.t
-val gen_type_proto_sparse_tensor :
-  Onnx_piqi.type_proto_sparse_tensor -> Piqirun.OBuf.t
-val gen_operator_set_id_proto :
-  Onnx_piqi.operator_set_id_proto -> Piqirun.OBuf.t
-val gen_function_proto : Onnx_piqi.function_proto -> Piqirun.OBuf.t
-val gen_version :
-  [< `ir_version
-   | `ir_version_2017_10_10
-   | `ir_version_2017_10_30
-   | `ir_version_2017_11_3
-   | `ir_version_2019_1_22
-   | `ir_version_2019_3_18
-   | `ir_version_2019_9_19
-   | `ir_version_2020_5_8
-   | `start_version ] ->
-  Piqirun.OBuf.t
-val gen_operator_status : [< `experimental | `stable ] -> Piqirun.OBuf.t
-val default_int64 : unit -> int64
-val default_int32 : unit -> int32
-val default_string : unit -> string
-val default_float32 : unit -> float
-val default_protobuf_int64 : unit -> int64
-val default_binary : unit -> string
-val default_protobuf_int32 : unit -> int32
-val default_float64 : unit -> float
-val default_uint64 : unit -> int64
-val default_attribute_proto : unit -> Attribute_proto.t
-val default_attribute_proto_attribute_type : unit -> [> `undefined ]
-val default_value_info_proto : unit -> Value_info_proto.t
-val default_node_proto : unit -> Node_proto.t
-val default_training_info_proto : unit -> Training_info_proto.t
-val default_model_proto : unit -> Model_proto.t
-val default_string_string_entry_proto : unit -> String_string_entry_proto.t
-val default_tensor_annotation : unit -> Tensor_annotation.t
-val default_graph_proto : unit -> Graph_proto.t
-val default_tensor_proto : unit -> Tensor_proto.t
-val default_tensor_proto_segment : unit -> Tensor_proto_segment.t
-val default_tensor_proto_data_type : unit -> [> `undefined ]
-val default_tensor_proto_data_location : unit -> [> `default ]
-val default_sparse_tensor_proto : unit -> Sparse_tensor_proto.t
-val default_tensor_shape_proto : unit -> Tensor_shape_proto.t
-val default_tensor_shape_proto_dimension :
-  unit -> Tensor_shape_proto_dimension.t
-val default_type_proto : unit -> Type_proto.t
-val default_type_proto_tensor : unit -> Type_proto_tensor.t
-val default_type_proto_sequence : unit -> Type_proto_sequence.t
-val default_type_proto_map : unit -> Type_proto_map.t
-val default_type_proto_optional : unit -> Type_proto_optional.t
-val default_type_proto_sparse_tensor : unit -> Type_proto_sparse_tensor.t
-val default_operator_set_id_proto : unit -> Operator_set_id_proto.t
-val default_function_proto : unit -> Function_proto.t
-val default_version : unit -> [> `start_version ]
-val default_operator_status : unit -> [> `experimental ]
-type float32 = float
-type float64 = float
-type uint64 = int64
-type protobuf_int64 = int64
-type binary = string
-type protobuf_int32 = int32
-type attribute_proto_attribute_type =
-    [ `float
-    | `floats
-    | `graph
-    | `graphs
-    | `int
-    | `ints
-    | `sparse_tensor
-    | `sparse_tensors
-    | `string
-    | `strings
-    | `tensor
-    | `tensors
-    | `type_proto
-    | `type_protos
-    | `undefined ]
-type tensor_proto_data_type =
-    [ `bfloat16
-    | `bool
-    | `complex128
-    | `complex64
-    | `double
-    | `float
-    | `float16
-    | `int16
-    | `int32
-    | `int64
-    | `int8
-    | `string
-    | `uint16
-    | `uint32
-    | `uint64
-    | `uint8
-    | `undefined ]
-type tensor_proto_data_location = [ `default | `externall ]
-type version =
-    [ `ir_version
-    | `ir_version_2017_10_10
-    | `ir_version_2017_10_30
-    | `ir_version_2017_11_3
-    | `ir_version_2019_1_22
-    | `ir_version_2019_3_18
-    | `ir_version_2019_9_19
-    | `ir_version_2020_5_8
-    | `start_version ]
-type operator_status = [ `experimental | `stable ]
-type attribute_proto = Attribute_proto.t
-type value_info_proto = Value_info_proto.t
-type node_proto = Node_proto.t
-type training_info_proto = Training_info_proto.t
-type model_proto = Model_proto.t
-type string_string_entry_proto = String_string_entry_proto.t
-type tensor_annotation = Tensor_annotation.t
-type graph_proto = Graph_proto.t
-type tensor_proto = Tensor_proto.t
-type tensor_proto_segment = Tensor_proto_segment.t
-type sparse_tensor_proto = Sparse_tensor_proto.t
-type tensor_shape_proto = Tensor_shape_proto.t
-type tensor_shape_proto_dimension = Tensor_shape_proto_dimension.t
-type type_proto = Type_proto.t
-type type_proto_tensor = Type_proto_tensor.t
-type type_proto_sequence = Type_proto_sequence.t
-type type_proto_map = Type_proto_map.t
-type type_proto_optional = Type_proto_optional.t
-type type_proto_sparse_tensor = Type_proto_sparse_tensor.t
-type operator_set_id_proto = Operator_set_id_proto.t
-type function_proto = Function_proto.t
diff --git a/src/dune b/src/dune
index a8874d6f..f091c2c3 100644
--- a/src/dune
+++ b/src/dune
@@ -1,7 +1,7 @@
 (executable
   (name main)
   (public_name caisar)
-  (libraries menhirLib yojson cmdliner logs logs.cli logs.fmt fmt.tty base unix str ppx_deriving_yojson.runtime nnet why3 dune-site)
+  (libraries menhirLib yojson cmdliner logs logs.cli logs.fmt fmt.tty base unix str ppx_deriving_yojson.runtime nnet onnx why3 dune-site)
   (preprocess (pps ppx_deriving_yojson ppx_deriving.show ppx_deriving.ord ppx_deriving.eq))
   (package caisar)
 )
diff --git a/src/language.ml b/src/language.ml
index 34b21be0..de019445 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -6,18 +6,18 @@
 
 open Base
 
-(* -- Support for the NNet neural network format. *)
+(* -- Support for the NNet and ONNX neural network format. *)
 
-type nnet = {
+type net = {
   nb_inputs : int;
   nb_outputs : int;
   ty_data : Why3.Ty.ty;
   filename : string;
 }
 
-let loaded_nnets = Why3.Term.Hls.create 10
+let loaded_nets = Why3.Term.Hls.create 10
 
-let lookup_loaded_nnets = Why3.Term.Hls.find_opt loaded_nnets
+let lookup_loaded_nets = Why3.Term.Hls.find_opt loaded_nets
 
 let nnet_parser env _ filename _ =
   let open Why3 in
@@ -41,7 +41,7 @@ let nnet_parser env _ filename _ =
         (List.init header.n_inputs ~f)
         (Ty.ty_tuple (List.init header.n_outputs ~f))
     in
-    Why3.Term.Hls.add loaded_nnets ls_nnet_apply
+    Why3.Term.Hls.add loaded_nets ls_nnet_apply
       {
         filename;
         nb_inputs = header.n_inputs;
@@ -54,7 +54,79 @@ let nnet_parser env _ filename _ =
     in
     Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
 
+let onnx_parser env _ filename _ =
+  let open Why3 in
+  let header = Onnx.parse filename in
+  match header with
+  | Error s -> Loc.errorm "%s" s
+  | Ok model ->
+    let onnx = Pmodule.read_module env [ "caisar" ] "NNet" in
+    let onnx_input_type =
+      Ty.ty_app
+        Theory.(ns_find_ts onnx.mod_theory.th_export [ "input_type" ])
+        []
+    in
+    let id_as_tuple = Ident.id_fresh "AsTuple" in
+    let th_uc = Pmodule.create_module env id_as_tuple in
+    let th_uc = Pmodule.use_export th_uc onnx in
+    let ins, outs = match model.graph with
+      | Some g -> Some g.input, Some g.output
+      | None -> None, None
+    in
+    let get_nested_dims (s:Onnx.Opiqi.value_info_proto list) = match List.nth_exn s 0 with
+      | {type_ = Some {tensor_type =
+                         Some {shape =
+                                 Some v; _};_}; _} ->
+        v.dim
+      | _ -> []
+    in
+    let input_shape, output_shape = match ins, outs with
+      | Some i, Some o ->
+        get_nested_dims i,
+        get_nested_dims o
+
+      | _-> [], []
+    in
+    (*TODO: here we only get the flattened dimension
+     * of inputs and outputs, but more interesting parsing
+     * could be done later on *)
+    let flattened_dim (dim:Onnx.Opiqi.tensor_shape_proto_dimension list) =
+      List.fold ~init:1 dim
+        ~f:(fun acc x -> match x.dim_value with
+            | Some v -> acc * (Int64.to_int_exn v)
+            | None -> acc)
+    in
+    let input_flat_dim, output_flat_dim =
+      (flattened_dim input_shape),
+      (flattened_dim output_shape)
+    in
+    let ls_onnx_apply =
+      (*TODO: find out input and output size for ONNX*)
+      let f _ = onnx_input_type in
+      Term.create_fsymbol
+        (Ident.id_fresh "onnx_apply")
+        (List.init input_flat_dim ~f)
+        (Ty.ty_tuple (List.init output_flat_dim ~f))
+    in
+    Why3.Term.Hls.add loaded_nets ls_onnx_apply
+      {
+        filename;
+        nb_inputs = input_flat_dim;
+        nb_outputs = output_flat_dim;
+        ty_data = onnx_input_type;
+      };
+    let th_uc =
+      Pmodule.add_pdecl ~vc:false th_uc
+        (Pdecl.create_pure_decl (Decl.create_param_decl ls_onnx_apply))
+    in
+    Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
+
 let register_nnet_support () =
   Why3.(
     Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
       "NNet" [ "nnet" ] nnet_parser)
+
+let register_onnx_support () =
+  Why3.(
+    Env.register_format ~desc:"ONNX format" Pmodule.mlw_language
+      "ONNX" [ "ONNX" ] onnx_parser)
diff --git a/src/language.mli b/src/language.mli
index 71482631..33606475 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -4,15 +4,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type nnet = {
+type net = {
   nb_inputs : int;
   nb_outputs : int;
   ty_data : Why3.Ty.ty;
   filename : string;
 }
 
-val lookup_loaded_nnets : Why3.Term.lsymbol -> nnet option
+val lookup_loaded_nets : Why3.Term.lsymbol -> net option
 (** @return the filename of a nnet Why3 representation. *)
 
 val register_nnet_support : unit -> unit
-(** Register nnet parser. *)
+(** Register NNet parser. *)
+
+val register_onnx_support : unit -> unit
+(** Register ONNX parser. *)
diff --git a/src/transformations.ml b/src/transformations.ml
index 5c7fff1d..0b87f968 100644
--- a/src/transformations.ml
+++ b/src/transformations.ml
@@ -24,7 +24,7 @@ let get_input_variables =
   let rec aux acc (term : Why3.Term.term) =
     match term.t_node with
     | Why3.Term.Tapp (ls, args) -> (
-      match Language.lookup_loaded_nnets ls with
+      match Language.lookup_loaded_nets ls with
       | None -> acc
       | Some _ ->
         let add i acc = function
@@ -48,7 +48,7 @@ let simplify_goal env input_variables =
   let rec aux hls (term : Why3.Term.term) =
     match term.t_node with
     | Why3.Term.Tapp (ls, _) -> (
-      match Language.lookup_loaded_nnets ls with
+      match Language.lookup_loaded_nets ls with
       | None -> Why3.Term.t_map (aux hls) term
       | Some nnet ->
         let outputs =
diff --git a/src/verification.ml b/src/verification.ml
index 02f14d60..7e87ea9c 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -8,6 +8,7 @@ open Base
 module Filename = Caml.Filename
 
 let () = Language.register_nnet_support ()
+let () = Language.register_onnx_support ()
 
 let create_env loadpath =
   let config = Autodetection.autodetect ~debug:true () in
-- 
GitLab