diff options
Diffstat (limited to 'src/spec_analysis.mli')
| -rw-r--r-- | src/spec_analysis.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index 731bd822..6aeb711b 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -18,3 +18,15 @@ val default_order : tannot defs -> order *) val is_within_range: typ -> typ -> nexp_range list -> triple val is_within_machine64 : typ -> nexp_range list -> triple + +(* free variables and dependencies *) + +(*fv_of_def consider_ty_vars consider_scatter_as_one all_defs all_defs def -> (bound_by_def, free_in_def) *) +val fv_of_def: bool -> bool -> (tannot def) list -> tannot def -> Nameset.t * Nameset.t + +(*group_defs consider_scatter_as_one all_defs -> ((bound_by_def, free_in_def), def) list *) +val group_defs : bool -> tannot defs -> ((Nameset.t * Nameset.t) * (tannot def)) list + +(*reodering definitions, initial functions *) +(* produce a new ordering for defs, limiting to those listed in the list, which respects dependencies *) +val restrict_defs : tannot defs -> string list -> tannot defs |