Add a new module for writing queries/analyses that aren't type checking but could be useful

Define in that a function for determining a default direction for vectors

4 files changed, 46 insertions, 0 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index bc7cba0d..39234b11 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1,6 +1,7 @@
 open Big_int
 open Ast
 open Type_internal
+open Spec_analysis
 type typ = Type_internal.t
 type 'a exp = 'a Ast.exp
 type 'a emap = 'a Envmap.t
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
new file mode 100644
index 00000000..1ed2711d
--- /dev/null
+++ b/src/spec_analysis.ml
@@ -0,0 +1,28 @@
+open Ast
+open Util
+open Big_int
+open Type_internal
+
+type typ = Type_internal.t
+
+(*Query a spec for its default order if one is provided. Assumes Inc if not *)
+let get_default_order_sp (DT_aux(spec,_)) =
+  match spec with
+  | DT_order (Ord_aux(o,_)) ->
+    (match o with
+     | Ord_inc -> Some {order = Oinc}
+     | Ord_dec -> Some { order = Odec}
+     | _ -> Some {order = Oinc})
+  | _ -> None
+
+let get_default_order_def = function
+  | DEF_default def_spec -> get_default_order_sp def_spec
+  | _ -> None
+
+let rec default_order (Defs defs) =
+  match defs with
+  | [] -> { order = Oinc } (*When no order is specified, we assume that it's inc*)
+  | def::defs ->
+    match get_default_order_def def with
+    | None -> default_order (Defs defs)
+    | Some o -> o
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
new file mode 100644
index 00000000..94698954
--- /dev/null
+++ b/src/spec_analysis.mli
@@ -0,0 +1,8 @@
+open Ast
+open Util
+open Big_int
+open Type_internal
+
+type typ = Type_internal.t
+
+val default_order : tannot defs -> order
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 2fb06ce0..0161bd96 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1382,6 +1382,15 @@ let uint16_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 16)
 let uint32_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 32) (big_int_of_string "4294967296"))])}
 let uint64_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 64) (big_int_of_string "18446744073709551616"))])}
 
+let int8_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 7) (big_int_of_int 128))) ;
+                                 TA_nexp (mk_c_int 127)])}
+let int16_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 15) (big_int_of_int 32768)));
+                                  TA_nexp (mk_c_int 32767)])}
+let int32_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 31) (big_int_of_int 2147483648))) ;
+                                  TA_nexp (mk_c_int 2147483647)])}
+let int64_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 63) (big_int_of_string "9223372036854775808")));
+                                  TA_nexp (mk_c (big_int_of_string "9223372036854775807"))])}
+
 let unit_t = { t = Tid "unit" }
 let bit_t = {t = Tid "bit" }
 let bool_t = {t = Tid "bool" }