(* Partially known dynamic values for safe array indexing *) type bound (* A single bound, abstract *) val string_of_bound : bound -> string (* Partial order on bounds *) type fuzzy_bool = True | False | Undecided val leq_bound : bound -> bound -> fuzzy_bool val offset_bound : int -> bound -> bound type bounds = bound * bound (* Lower and higher bounds *) val string_of_bounds : bounds -> string val array_bounds : bounds (* Full bounds of an array *) (* A bounded dynamic value of the type int *) (* Hereafter, 'c stands for the environment classifier. *) type 'c bounded val string_of_bounded : 'c bounded -> string (* Extract the dynamic value from bounded *) val dyn_of_bounded : 'c bounded -> ('c,int) code (* Compare bounded: we compare bounds rather than code values *) val same_bounded : 'c bounded -> 'c bounded -> bool (* Check to see if one bounded immediately precedes the other. That is, the upper bound of one matches with the lower bound of the other. *) val successive_bounded : 'c bounded -> 'c bounded -> bool val offset_bounded : int -> 'c bounded -> 'c bounded (* The bounded value corresponding to the lower bound of an array *) val min_bounded : 'c bounded (* Check to see if a given bounded value is within the given bounds. Return: - None if it is definitely out of bounds - Some c where c is the code (dynamic value) if it is definitely within the bounds - raise an error if cannot decide *) val within_bounds : 'c bounded -> bounds -> ('c,int) code option (* Wrapper that produces the top-level function for the stencil computation with one input and one output array, given the generator for the computation *) val make_fun : ('c bounded -> (* for the upper bound of arrays *) ('c,float array) code -> (* input array *) ('c,float array) code -> (* output array *) ('c,'w) code) -> ('c, int -> float array -> float array -> 'w) code (* For-loop with bounded index bounds *) val forloop : 'c bounded -> 'c bounded -> ('c bounded -> ('c,unit) code) -> ('c,unit) code