diff options
Diffstat (limited to 'src/spec_analysis.ml')
| -rw-r--r-- | src/spec_analysis.ml | 28 |
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 |
