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

1 files changed, 28 insertions, 0 deletions

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