summaryrefslogtreecommitdiff
path: root/src/spec_analysis.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/spec_analysis.ml')
-rw-r--r--src/spec_analysis.ml28
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