diff options
Diffstat (limited to 'src/spec_analysis.ml')
| -rw-r--r-- | src/spec_analysis.ml | 68 |
1 files changed, 34 insertions, 34 deletions
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index b35bc48f..7386e9fa 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -101,64 +101,64 @@ let rec default_order (Defs defs) = | (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 + (Big_int.negate 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) + min, (Big_int.negate 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) + | Nconst abs_min | N2n(_,Some abs_min) -> (Big_int.negate 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) + | Nconst abs_max | N2n(_,Some abs_max) -> (Big_int.negate abs_max) | _ -> assert false (*Put a better error message here*))) | _ -> assert false - in le_big_int min candidate && le_big_int candidate max + in Big_int.less_equal min candidate && Big_int.less_equal candidate max | _ -> assert false (*Rmove me when switch to zarith*) let rec power_big_int b n = - if eq_big_int n zero_big_int - then unit_big_int - else mult_big_int b (power_big_int b (sub_big_int n unit_big_int)) + if Big_int.equal n Big_int.zero + then (Big_int.of_int 1) + else Big_int.mul b (power_big_int b (Big_int.sub n (Big_int.of_int 1))) let unpower_of_2 b = - let two = big_int_of_int 2 in - let four = big_int_of_int 4 in - let eight = big_int_of_int 8 in - let sixteen = big_int_of_int 16 in - let thirty_two = big_int_of_int 32 in - let sixty_four = big_int_of_int 64 in - let onetwentyeight = big_int_of_int 128 in - let twofiftysix = big_int_of_int 256 in - let fivetwelve = big_int_of_int 512 in - let oneotwentyfour = big_int_of_int 1024 in - let to_the_sixteen = big_int_of_int 65536 in - let to_the_thirtytwo = big_int_of_string "4294967296" in - let to_the_sixtyfour = big_int_of_string "18446744073709551616" in - let ck i = eq_big_int b i in - if ck unit_big_int then zero_big_int - else if ck two then unit_big_int + let two = Big_int.of_int 2 in + let four = Big_int.of_int 4 in + let eight = Big_int.of_int 8 in + let sixteen = Big_int.of_int 16 in + let thirty_two = Big_int.of_int 32 in + let sixty_four = Big_int.of_int 64 in + let onetwentyeight = Big_int.of_int 128 in + let twofiftysix = Big_int.of_int 256 in + let fivetwelve = Big_int.of_int 512 in + let oneotwentyfour = Big_int.of_int 1024 in + let to_the_sixteen = Big_int.of_int 65536 in + let to_the_thirtytwo = Big_int.of_string "4294967296" in + let to_the_sixtyfour = Big_int.of_string "18446744073709551616" in + let ck i = Big_int.equal b i in + if ck (Big_int.of_int 1) then Big_int.zero + else if ck two then (Big_int.of_int 1) else if ck four then two - else if ck eight then big_int_of_int 3 + else if ck eight then Big_int.of_int 3 else if ck sixteen then four - else if ck thirty_two then big_int_of_int 5 - else if ck sixty_four then big_int_of_int 6 - else if ck onetwentyeight then big_int_of_int 7 + else if ck thirty_two then Big_int.of_int 5 + else if ck sixty_four then Big_int.of_int 6 + else if ck onetwentyeight then Big_int.of_int 7 else if ck twofiftysix then eight - else if ck fivetwelve then big_int_of_int 9 - else if ck oneotwentyfour then big_int_of_int 10 + else if ck fivetwelve then Big_int.of_int 9 + else if ck oneotwentyfour then Big_int.of_int 10 else if ck to_the_sixteen then sixteen else if ck to_the_thirtytwo then thirty_two else if ck to_the_sixtyfour then sixty_four else let rec unpower b power = - if eq_big_int b unit_big_int + if Big_int.equal b (Big_int.of_int 1) then power - else (unpower (div_big_int b two) (succ_big_int power)) in - unpower b zero_big_int + else (unpower (Big_int.div b two) (Big_int.succ power)) in + unpower b Big_int.zero let is_within_range candidate range constraints = let candidate_actual = match candidate.t with @@ -183,7 +183,7 @@ let is_within_range candidate range constraints = | Tapp("vector", [_; TA_nexp size ; _; _]) -> (match size.nexp with | Nconst i | N2n(_, Some i) -> - if check_in_range (power_big_int (big_int_of_int 2) i) range + if check_in_range (power_big_int (Big_int.of_int 2) i) range then Yes else No | _ -> Maybe) |