diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewriter.ml | 2 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 41 | ||||
| -rw-r--r-- | src/spec_analysis.mli | 11 | ||||
| -rw-r--r-- | src/type_internal.ml | 2 | ||||
| -rw-r--r-- | src/type_internal.mli | 4 |
5 files changed, 58 insertions, 2 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 2a9782ba..f90c5b90 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -999,8 +999,8 @@ let remove_blocks_exp_alg = E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in let rec f = function + | [] -> E_aux (E_lit (L_aux (L_unit,Unknown)), (Unknown,simple_annot ({t = Tid "unit"}))) | [e] -> e (* check with Kathy if that annotation is fine *) - | e -> E_aux (E_lit (L_aux (L_unit,Unknown)), (Unknown,simple_annot ({t = Tid "unit"}))) | e :: es -> letbind_wild e (f es) in let e_aux = function diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 1ed2711d..8ea1407f 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -26,3 +26,44 @@ let rec default_order (Defs defs) = match get_default_order_def def with | None -> default_order (Defs defs) | Some o -> o + +(*Is within range*) + +let check_in_range (candidate : big_int) (range : typ) : bool = + match range.t with + | Tapp("range", [TA_nexp min; TA_nexp max]) | Tabbrev(_,{t=Tapp("range", [TA_nexp min; TA_nexp max])}) -> + let min,max = + match min.nexp,max.nexp with + | (Nconst min, Nconst max) + | (Nconst min, N2n(_, Some max)) + | (N2n(_, Some min), Nconst max) + | (N2n(_, Some min), N2n(_, Some max)) + -> min, max + | (Nneg n, Nconst max) | (Nneg n, N2n(_, Some max))-> + (match n.nexp with + | Nconst abs_min | N2n(_,Some abs_min) -> + (minus_big_int abs_min), max + | _ -> assert false (*Put a better error message here*)) + | (Nconst min,Nneg n) | (N2n(_, Some min), Nneg n) -> + (match n.nexp with + | Nconst abs_max | N2n(_,Some abs_max) -> + min, (minus_big_int abs_max) + | _ -> assert false (*Put a better error message here*)) + | (Nneg nmin, Nneg nmax) -> + ((match nmin.nexp with + | Nconst abs_min | N2n(_,Some abs_min) -> (minus_big_int abs_min) + | _ -> assert false (*Put a better error message here*)), + (match nmax.nexp with + | Nconst abs_max | N2n(_,Some abs_max) -> (minus_big_int abs_max) + | _ -> assert false (*Put a better error message here*))) + | _ -> assert false + in le_big_int min candidate && le_big_int candidate max + | _ -> assert false + + +let is_within_range candidate range constraints = + match candidate.t with + | Tapp("atom", [TA_nexp n]) -> + (match n.nexp with + | Nconst i -> if check_in_range i range then Yes else No + | _ -> Maybe) diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index 94698954..1b1197dd 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -5,4 +5,15 @@ open Type_internal type typ = Type_internal.t +(*Returns the declared default order of a set of definitions, defaulting to Inc if no default is provided *) val default_order : tannot defs -> order + +(*Determines if the first typ is within the range of the the second typ, + using the constraints provided when the first typ contains variables. + It is an error for second typ to be anything other than a range type + If the first typ is a vector, then determines if the max representable + number is in the range of the second; it is an error for the first typ + to be anything other than a vector, a range, an atom, or a bit (after + suitable unwrapping of abbreviations, reg, and registers). +*) +val is_within_range: typ -> typ -> nexp_range list -> triple diff --git a/src/type_internal.ml b/src/type_internal.ml index 0161bd96..5366d5dd 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1154,7 +1154,7 @@ let equate_o (o_box : order) (o : order) : unit = (match o_box.order with | Ouvar(u) -> u.osubst <- Some(o) - | _ -> assert false) + | _ -> o.order <- o_box.order) | _ -> o_box.order <- o.order) let equate_e (e_box : effect) (e : effect) : unit = diff --git a/src/type_internal.mli b/src/type_internal.mli index ac1ae525..63eac320 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -10,6 +10,10 @@ val zero : big_int val one : big_int val two : big_int +(*Trinary replacement for boolean, as sometimes we do want to distinguish we just don't know from a certain yes or no*) +type triple = Yes | No | Maybe +val triple_negate : triple -> triple + type kind = { mutable k : k_aux } and k_aux = | K_Typ |