Merge pull request #115 from AestheticIntegration/ewen/fullImandraAnn…

…otations Ewen/full imandra annotations
imandra-ai · Oct 9, 2019 · f85831e · f85831e
2 parents 3e860a1 + 21af87b
commit f85831e
Show file tree

Hide file tree

Showing 166 changed files with 1,630 additions and 724 deletions.
diff --git a/Makefile b/Makefile
@@ -1,18 +1,19 @@
 # Makefile
 #
 build:
-	@echo "(ignored_subdirs (src-protocol-exts-vg src-protocol-exts-pp-vg))" > dune
+	@echo "(ignored_subdirs (src-protocol-exts-vg src-protocol-exts-pp-vg src-core-utils-vg))" > dune
 	dune build @install
 	rm dune
 
 build_vgs:
-	@echo "(ignored_subdirs (src-protocol-exts src-protocol-exts-pp src-model src-simulation))" > dune
+	@echo "(ignored_subdirs (src-protocol-exts src-protocol-exts-pp src-model src-simulation src-simulation-utils src-core-utils src-tests-utils))" > dune
 	dune build @install
 	rm dune
 
 build_tests:
-	@echo "(ignored_subdirs (src-protocol-exts-vg src-protocol-exts-pp-vg))" > dune
+	@echo "(ignored_subdirs (src-protocol-exts-vg src-protocol-exts-pp-vg src-core-utils-vg))" > dune
 	dune build src-tests/test_runner.bc 
+	dune build src-tests/test_cache.bc
 	rm dune
 
 doc:
@@ -28,12 +29,12 @@ module_graph.svg: _build/doc/all_modules.docdir/all_modules.dot
 	sed -e 's/rotate=90;//g' "$<" | dot -Tsvg -o $@
 
 server:
-	@echo "(ignored_subdirs (src-protocol-exts-vg src-protocol-exts-pp-vg))" > dune
+	@echo "(ignored_subdirs (src-protocol-exts-vg src-protocol-exts-pp-vg src-core-utils-vg))" > dune
 	dune build src-simulation/server.bc
 	rm dune
 
 client:
-	@echo "(ignored_subdirs (src-protocol-exts-vg src-protocol-exts-pp-vg))" > dune
+	@echo "(ignored_subdirs (src-protocol-exts-vg src-protocol-exts-pp-vg src-core-utils-vg))" > dune
 	dune build  src-simulation/client.bc
 	rm dune
 

diff --git a/dash/base_dashes.iml b/dash/base_dashes.iml
@@ -1,6 +1,6 @@
 (**
 
-    Aesthetic Integration Limited
+    Imandra Inc.
     Copyright (c) 2014 - 2017
 
     Dash version:

diff --git a/dash/heartbeat_dashes.iml b/dash/heartbeat_dashes.iml
@@ -1,6 +1,6 @@
 (** 
 
-    Aesthetic Integration Limited
+    Imandra Inc.
     Copyright (c) 2014 - 2017
 
     Dash versions of VGs covering behaviour of Heartbeat message ( Vol 2, page 16 ).

diff --git a/fix-engine.opam b/fix-engine.opam
@@ -16,4 +16,6 @@ depends: [
   "lwt-zmq"
   "yojson"
   "zmq"
+  "decoders"
+  "decoders-yojson"
 ]
diff --git a/src-core-pp/base_types_json.iml b/src-core-pp/base_types_json.iml
@@ -1,12 +1,14 @@
 (** JSON printers/parsers for base FIX types. *)
 (***
 
-    Aesthetic Integration Limited
-    Copyright (c) 2014 - 2018
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
 
-    base_types_json.ml 
+    base_types_json.iml 
 *)
-
+[@@@require "decoders-yojson"]
+[@@@import "../src-core/numeric.iml"]
+[@@@program]
 open Yojson;;
 open Numeric;;
 module JU = Yojson.Basic.Util;;
@@ -255,3 +257,4 @@ let bool_opt_to_json : bool option -> json = function
   | None   -> `Null
   | Some x -> bool_to_json x 
 ;;
+[@@@logic]
diff --git a/src-core-pp/datetime_json.iml b/src-core-pp/datetime_json.iml
@@ -1,12 +1,14 @@
 (** JSON printers/parsers for datetime types. *)
 (***
 
-    Aesthetic Integration Limited
-    Copyright (c) 2014 - 2018
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
 
-    datetime_json.ml 
+    datetime_json.iml 
 *)
-
+[@@@import "../src-core/datetime.iml"]
+[@@@import "base_types_json.iml"]
+[@@@program]
 open Yojson;;
 open Datetime;;
 open Base_types_json;;
@@ -277,3 +279,4 @@ let monthyear_opt_to_json = function
   | None    -> `Null
   | Some x  -> monthyear_to_json x
 ;;
+[@@@logic]
diff --git a/src-core-pp/encode_base_types.iml b/src-core-pp/encode_base_types.iml
@@ -1,12 +1,13 @@
 (** JSON printers/parsers for base FIX types. *)
 (***
 
-    Aesthetic Integration Limited
-    Copyright (c) 2014 - 2018
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
 
-    base_types_json.ml 
+    base_types_json.iml 
 *)
-
+[@@@import "../src-core/numeric.iml"]
+[@@@program]
 open Numeric;;
 
 
@@ -30,4 +31,5 @@ let encode_symbol x = x;;
 let encode_bool : bool -> string = function
     | true  -> "Y" 
     | false -> "N" 
-;;
+;;
+[@@@logic]
diff --git a/src-core-pp/encode_datetime.iml b/src-core-pp/encode_datetime.iml
@@ -1,13 +1,15 @@
 (** Parsers for datetime types. *)
 (***
 
-    Aesthetic Integration Limited
-    Copyright (c) 2014 - 2018
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
 
-    parse_datetime.ml
+    parse_datetime.iml
 
 *)
-
+[@@@import "../src-core/datetime.iml"]
+[@@@import "encode_base_types.iml"]
+[@@@program]
 open Datetime;;
 open Encode_base_types;;
 
@@ -101,4 +103,5 @@ let encode_Duration (x : fix_duration) : string =
   let days = 
     (duration_to_seconds x) / (60*60*24) in
   "D"^(Z.to_string days)
-;;
+;;
+[@@@logic]
diff --git a/src-core-pp/parse_base_types.iml b/src-core-pp/parse_base_types.iml
@@ -1,12 +1,13 @@
 (** Parsers for base types. *)
 (***
 
-    Aesthetic Integration Limited
-    Copyright (c) 2014 - 2018
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
 
-    datetime_json.ml 
+    datetime_json.iml 
 *)
-
+[@@@import "../src-core/numeric.iml"]
+[@@@program]
 open Numeric;;
 
 let parse_string (str : string) : string option = 
@@ -49,3 +50,4 @@ let parse_float (str: string) : Numeric.fix_float_6 option =
     Some (Float_6 (Z.of_int whole * 1000000 + Z.of_int fraction * pow10 (6 - frlen)))
     else None
 ;;
+[@@@logic]
diff --git a/src-core-pp/parse_datetime.iml b/src-core-pp/parse_datetime.iml
@@ -1,13 +1,14 @@
 (** Parsers for datetime types. *)
 (***
 
-    Aesthetic Integration Limited
-    Copyright (c) 2014 - 2018
+    Imandra Inc.
+    Copyright (c) 2014 - 201
 
     parse_datetime.ml
 
 *)
-
+[@@@import "../src-core/datetime.iml"]
+[@@@program]
 open Datetime;;
 
 
@@ -175,4 +176,5 @@ let parse_Duration (str:string) : fix_duration option =
            }))
      | _,_ -> None)
   else None 
-;;
+;;
+[@@@logic]
diff --git a/src-core-pp/parser_utils.iml b/src-core-pp/parser_utils.iml
@@ -1,7 +1,7 @@
 (** Various parser utilities. *)
 (***
 
-    Aesthetic Integration Limited
+    Imandra Inc.
     Copyright (c) 2014 - 2017
 
     parser_utils.ml
@@ -11,7 +11,8 @@
 (** OCaml Stream processing helper functions that break a raw byte stream into 
     a stream of key=value pairs and then into a stream of messages.  
 *)
-
+[@@@program]
+[@@@import "parse_base_types.iml"]
 (**  Splits a stream of characters into a stream of [(key * value)] pairs. *)
 let split_into_key_value (spliton : char) ( stream : char Stream.t ) : (string * string) Stream.t =
   let current = ref [] in
@@ -311,3 +312,4 @@ module Parser = struct
 
 end
 
+[@@@logic]
diff --git a/src-core-printer/core_printer.iml b/src-core-printer/core_printer.iml
@@ -1,16 +1,19 @@
 (** Printers for core types appearing in messages *)
 (***
 
-    Aesthetic Integration Limited
-    Copyright (c) 2014 - 2018
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
 
     core_printer.ml
 
 *)
-
+[@@@import "../src-core-pp/encode_base_types.iml"]
+[@@@import "../src-core-pp/encode_datetime.iml"]
+[@@@import "../src-core-time-defaults-pp/time_defaults_pp.iml"]
+[@@@program]
 open Encode_base_types;;
 open Encode_datetime;;
-open TimeDefaults_pp;;
+open Time_defaults_pp;;
 
 let fix_float_0_to_string x =
   encode_float_0 x
@@ -79,3 +82,4 @@ let fix_monthyear_to_string x =
 let fix_duration_to_string x =
   encode_Duration x
 ;;
+[@@@logic]
diff --git a/src-core-time-defaults-pp/dune b/src-core-time-defaults-pp/dune
@@ -1,30 +1,30 @@
 (rule
-  (targets timeDefaults_parser.ml)
-  (deps timeDefaults_parser.iml)
+  (targets time_defaults_parser.ml)
+  (deps time_defaults_parser.iml)
    (action
-    (with-stdout-to timeDefaults_parser.ml
-       (run imandra-extract  timeDefaults_parser.iml))))
+    (with-stdout-to time_defaults_parser.ml
+       (run imandra-extract  time_defaults_parser.iml))))
 
 (rule
-  (targets timeDefaults_pp.ml)
-  (deps timeDefaults_pp.iml)
+  (targets time_defaults_pp.ml)
+  (deps time_defaults_pp.iml)
    (action
-    (with-stdout-to timeDefaults_pp.ml
-       (run imandra-extract  timeDefaults_pp.iml))))
+    (with-stdout-to time_defaults_pp.ml
+       (run imandra-extract  time_defaults_pp.iml))))
 
 (rule
-  (targets timeDefaults_current_time.ml)
-  (deps timeDefaults_current_time.iml)
+  (targets time_defaults_current_time.ml)
+  (deps time_defaults_current_time.iml)
    (action
-    (with-stdout-to timeDefaults_current_time.ml
-       (run imandra-extract  timeDefaults_current_time.iml))))
+    (with-stdout-to time_defaults_current_time.ml
+       (run imandra-extract  time_defaults_current_time.iml))))
 
 (rule
-  (targets timeDefaults_json.ml)
-  (deps timeDefaults_json.iml)
+  (targets time_defaults_json.ml)
+  (deps time_defaults_json.iml)
    (action
-    (with-stdout-to timeDefaults_json.ml
-       (run imandra-extract  timeDefaults_json.iml))))
+    (with-stdout-to time_defaults_json.ml
+       (run imandra-extract  time_defaults_json.iml))))
 
 (library
   (name core_time_defaults_pp)

diff --git a/src-core-time-defaults-pp/timeDefaults_current_time.iml b/src-core-time-defaults-pp/timeDefaults_current_time.iml
diff --git a/src-core-time-defaults-pp/timeDefaults_parser.iml b/src-core-time-defaults-pp/timeDefaults_parser.iml
diff --git a/src-core-time-defaults-pp/timeDefaults_pp.iml b/src-core-time-defaults-pp/timeDefaults_pp.iml
diff --git a/src-core-time-defaults-pp/time_defaults_current_time.iml b/src-core-time-defaults-pp/time_defaults_current_time.iml
@@ -0,0 +1,18 @@
+(** Time defaults for a particular FIX implementation *)
+(***
+
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
+
+    time_defaults_current_time.iml
+
+*)
+[@@@import "../src-core-utils-pp/current_time.iml"]
+[@@@program]
+open Current_time;;
+
+let get_current_utctimestamp = get_current_utctimestamp_milli;;
+
+let get_current_utctimeonly = get_current_utctimeonly_milli;;
+
+[@@@logic]
diff --git a/...re-time-defaults-pp/timeDefaults_json.iml → ...e-time-defaults-pp/time_defaults_json.iml b/...re-time-defaults-pp/timeDefaults_json.iml → ...e-time-defaults-pp/time_defaults_json.iml
@@ -1,4 +1,14 @@
-(* Aesthetic Integration copyright 2018 *)
+(** Time defaults for a particular FIX implementation *)
+(***
+
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
+
+    time_defaults_json.iml
+
+*)
+[@@@import "../src-core-pp/datetime_json.iml"]
+[@@@program]
 open Datetime_json;;
 
 let utctimestamp_to_json = utctimestamp_milli_to_json;;
@@ -8,3 +18,4 @@ let utctimestamp_opt_to_json = utctimestamp_milli_opt_to_json;;
 let utctimeonly_to_json = utctimeonly_milli_to_json;;
 
 let utctimeonly_opt_to_json = utctimeonly_milli_opt_to_json;;
+[@@@logic]
diff --git a/src-core-time-defaults-pp/time_defaults_parser.iml b/src-core-time-defaults-pp/time_defaults_parser.iml
@@ -0,0 +1,17 @@
+(** Time defaults for a particular FIX implementation *)
+(***
+
+    Imandra Inc.
+    Copyright (c) 2014 - 2019
+
+    time_defaults_parser.iml
+
+*)
+[@@@import "../src-core-pp/parse_datetime.iml"]
+[@@@program]
+open Parse_datetime;;
+
+let parse_UTCTimestamp = parse_UTCTimestamp_milli;;
+
+let parse_UTCTimeOnly = parse_UTCTimeOnly_milli;;
+[@@@logic]