diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 8 | ||||
| -rw-r--r-- | src/_tags | 7 | ||||
| -rw-r--r-- | src/ast_util.ml | 35 | ||||
| -rw-r--r-- | src/ast_util.mli | 6 | ||||
| -rw-r--r-- | src/constraint.ml | 18 | ||||
| -rw-r--r-- | src/constraint.mli | 4 | ||||
| -rw-r--r-- | src/gen_lib/prompt.lem | 1 | ||||
| -rw-r--r-- | src/initial_check.ml | 15 | ||||
| -rw-r--r-- | src/lexer.mll | 6 | ||||
| -rw-r--r-- | src/lexer2.mll | 12 | ||||
| -rw-r--r-- | src/monomorphise.ml | 48 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 14 | ||||
| -rw-r--r-- | src/parse_ast.ml | 16 | ||||
| -rw-r--r-- | src/parser.mly | 18 | ||||
| -rw-r--r-- | src/parser2.mly | 14 | ||||
| -rw-r--r-- | src/pretty_print_common.ml | 9 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 40 | ||||
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 26 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 7 | ||||
| -rw-r--r-- | src/pretty_print_sail2.ml | 15 | ||||
| -rw-r--r-- | src/rewriter.ml | 2 | ||||
| -rw-r--r-- | src/rewriter.mli | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 36 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 68 | ||||
| -rw-r--r-- | src/type_check.ml | 68 | ||||
| -rw-r--r-- | src/type_check.mli | 4 | ||||
| -rw-r--r-- | src/value.ml | 4 |
27 files changed, 248 insertions, 255 deletions
diff --git a/src/Makefile b/src/Makefile index 403dcca1..34560a5a 100644 --- a/src/Makefile +++ b/src/Makefile @@ -57,8 +57,12 @@ all: sail lib doc full: sail lib power doc test -ast.ml: ../language/l2.ott - ott -sort false -generate_aux_rules true -o ast.ml -picky_multiple_parses true ../language/l2.ott +ast.lem: ../language/l2.ott + ott -sort false -generate_aux_rules true -o ast.lem -picky_multiple_parses true ../language/l2.ott + +ast.ml: ast.lem + lem -ocaml ast.lem + sed -i -f ast.sed ast.ml lem_interp/interp_ast.lem: ../language/l2.ott ott -sort false -generate_aux_rules true -o lem_interp/interp_ast.lem -picky_multiple_parses true ../language/l2.ott @@ -1,10 +1,11 @@ true: -traverse, debug, use_menhir <**/*.ml>: bin_annot, annot -<lem_interp> or <test>: include -<sail.{byte,native}>: use_pprint, use_nums, use_unix, use_str -<isail.{byte,native}>: package(linenoise), use_pprint, use_nums, use_unix, use_str +# <lem_interp> or <test>: include +<sail.{byte,native}>: package(zarith), use_pprint, use_nums, use_unix, use_str, use_lem +<isail.{byte,native}>: package(linenoise), use_pprint, use_nums, use_unix, use_str, use_lem <isail.ml>: package(linenoise) <pprint> or <pprint/src>: include +<*.m{l,li}>: use_lem # see http://caml.inria.fr/mantis/view.php?id=4943 <lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, use_lem diff --git a/src/ast_util.ml b/src/ast_util.ml index 2fd43db5..61b67c31 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -50,7 +50,7 @@ open Ast open Util -open Big_int +module Big_int = Nat_big_num let no_annot = (Parse_ast.Unknown, ()) @@ -141,7 +141,7 @@ module Nexp = struct match nexp1, nexp2 with | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2 - | Nexp_constant c1, Nexp_constant c2 -> compare_big_int c1 c2 + | Nexp_constant c1, Nexp_constant c2 -> Big_int.compare c1 c2 | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b) | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b) | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) -> @@ -186,7 +186,7 @@ and nexp_simp_aux = function let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (add_big_int c1 c2) + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (Big_int.add c1 c2) | _, Nexp_neg n2 -> Nexp_minus (n1, n2) | _, _ -> Nexp_sum (n1, n2) end @@ -195,9 +195,9 @@ and nexp_simp_aux = function let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in match n1_simp, n2_simp with - | Nexp_constant c, _ when eq_big_int c unit_big_int -> n2_simp - | _, Nexp_constant c when eq_big_int c unit_big_int -> n1_simp - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (mult_big_int c1 c2) + | Nexp_constant c, _ when Big_int.equal c (Big_int.of_int 1) -> n2_simp + | _, Nexp_constant c when Big_int.equal c (Big_int.of_int 1) -> n1_simp + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (Big_int.mul c1 c2) | _, _ -> Nexp_times (n1, n2) end | Nexp_minus (n1, n2) -> @@ -205,10 +205,10 @@ and nexp_simp_aux = function let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (sub_big_int c1 c2) + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (Big_int.sub c1 c2) (* A vector range x['n-1 .. 0] can result in the size "('n-1) - -1" *) | Nexp_minus (Nexp_aux (n,_), Nexp_aux (Nexp_constant c1,_)), Nexp_constant c2 - when eq_big_int c1 (minus_big_int c2) -> n + when Big_int.equal c1 (Big_int.negate c2) -> n | _, _ -> Nexp_minus (n1, n2) end | nexp -> nexp @@ -249,7 +249,7 @@ let vector_typ n m ord typ = let exc_typ = mk_id_typ (mk_id "exception") let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown) -let nint i = nconstant (big_int_of_int i) +let nint i = nconstant (Big_int.of_int i) let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown) let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown) let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown) @@ -258,7 +258,7 @@ let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown) let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown) let nc_set kid nums = mk_nc (NC_set (kid, nums)) -let nc_int_set kid ints = mk_nc (NC_set (kid, List.map big_int_of_int ints)) +let nc_int_set kid ints = mk_nc (NC_set (kid, List.map Big_int.of_int ints)) let nc_eq n1 n2 = mk_nc (NC_equal (n1, n2)) let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2)) let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown) @@ -479,8 +479,6 @@ let string_of_base_effect = function | BE_aux (beff, _) -> string_of_base_effect_aux beff let string_of_effect = function - | Effect_aux (Effect_var kid, _) -> - string_of_kid kid | Effect_aux (Effect_set [], _) -> "pure" | Effect_aux (Effect_set beffs, _) -> "{" ^ string_of_list ", " string_of_base_effect beffs ^ "}" @@ -495,7 +493,7 @@ let rec string_of_nexp = function and string_of_nexp_aux = function | Nexp_id id -> string_of_id id | Nexp_var kid -> string_of_kid kid - | Nexp_constant c -> string_of_big_int c + | Nexp_constant c -> Big_int.to_string c | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")" | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")" | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")" @@ -530,7 +528,7 @@ and string_of_n_constraint = function | NC_aux (NC_and (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> - string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_big_int ns ^ "}" + string_of_kid kid ^ " IN {" ^ string_of_list ", " Big_int.to_string ns ^ "}" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" @@ -563,7 +561,7 @@ let string_of_lit (L_aux (lit, _)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num n -> string_of_big_int n + | L_num n -> Big_int.to_string n | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_undef -> "undefined" @@ -662,8 +660,8 @@ and string_of_letbind (LB_aux (lb, l)) = let rec string_of_index_range (BF_aux (ir, _)) = match ir with - | BF_single n -> string_of_big_int n - | BF_range (n, m) -> string_of_big_int n ^ " .. " ^ string_of_big_int m + | BF_single n -> Big_int.to_string n + | BF_range (n, m) -> Big_int.to_string n ^ " .. " ^ Big_int.to_string m | BF_concat (ir1, ir2) -> "(" ^ string_of_index_range ir1 ^ ") : (" ^ string_of_index_range ir2 ^ ")" let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) = @@ -774,9 +772,6 @@ let is_bitvector_typ typ = let has_effect (Effect_aux (eff,_)) searched_for = match eff with | Effect_set effs -> List.exists (fun (BE_aux (be,_)) -> be = searched_for) effs - | Effect_var _ -> - raise (Reporting_basic.err_unreachable Parse_ast.Unknown - "has_effect called on effect variable") let effect_set (Effect_aux (eff,_)) = match eff with | Effect_set effs -> BESet.of_list effs diff --git a/src/ast_util.mli b/src/ast_util.mli index a45ca4e9..a3ccc00c 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -49,7 +49,7 @@ (**************************************************************************) open Ast -open Big_int +module Big_int = Nat_big_num val no_annot : unit annot val gen_loc : Parse_ast.l -> Parse_ast.l @@ -118,7 +118,7 @@ val mk_effect : base_effect_aux list -> effect val nexp_simp : nexp -> nexp (* Utilities for building n-expressions *) -val nconstant : big_int -> nexp +val nconstant : Big_int.num -> nexp val nint : int -> nexp val nminus : nexp -> nexp -> nexp val nsum : nexp -> nexp -> nexp @@ -138,7 +138,7 @@ val nc_and : n_constraint -> n_constraint -> n_constraint val nc_or : n_constraint -> n_constraint -> n_constraint val nc_true : n_constraint val nc_false : n_constraint -val nc_set : kid -> big_int list -> n_constraint +val nc_set : kid -> Big_int.num list -> n_constraint val nc_int_set : kid -> int list -> n_constraint (* Negate a n_constraint. Note that there's no NC_not constructor, so diff --git a/src/constraint.ml b/src/constraint.ml index 3d5a3689..ae72d956 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -48,7 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Big_int +module Big_int = Nat_big_num open Util (* ===== Integer Constraints ===== *) @@ -58,13 +58,13 @@ type nexp_op = string type nexp = | NFun of (nexp_op * nexp list) | N2n of nexp - | NConstant of big_int + | NConstant of Big_int.num | NVar of int -let big_int_op : nexp_op -> (big_int -> big_int -> big_int) option = function - | "+" -> Some add_big_int - | "-" -> Some sub_big_int - | "*" -> Some mult_big_int +let big_int_op : nexp_op -> (Big_int.num -> Big_int.num -> Big_int.num) option = function + | "+" -> Some Big_int.add + | "-" -> Some Big_int.sub + | "*" -> Some Big_int.mul | _ -> None let rec arith constr = @@ -80,7 +80,7 @@ let rec arith constr = | Some op -> NConstant (op x y) | None -> c end - | N2n (NConstant x) -> NConstant (power_int_positive_big_int 2 x) + | N2n (NConstant x) -> NConstant (Big_int.pow_int_positive 2 (Big_int.to_int x)) | c -> c (* ===== Boolean Constraints ===== *) @@ -157,7 +157,7 @@ let cop_sexpr op x y = let rec sexpr_of_nexp = function | NFun (op, xs) -> sfun op (List.map sexpr_of_nexp xs) | N2n x -> sfun "^" [Atom "2"; sexpr_of_nexp x] - | NConstant c -> Atom (string_of_big_int c) (* CHECK: do we do negative constants right? *) + | NConstant c -> Atom (Big_int.to_string c) (* CHECK: do we do negative constants right? *) | NVar var -> Atom ("v" ^ string_of_int var) let rec sexpr_of_constraint = function @@ -303,6 +303,6 @@ let mult x y : nexp = NFun ("*", [x; y]) let app f xs : nexp = NFun (f, xs) -let constant (x : big_int) : nexp = NConstant x +let constant (x : Big_int.num) : nexp = NConstant x let variable (v : int) : nexp = NVar v diff --git a/src/constraint.mli b/src/constraint.mli index 89f2c625..2111a4e3 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -48,6 +48,8 @@ (* SUCH DAMAGE. *) (**************************************************************************) +module Big_int = Nat_big_num + type nexp type t @@ -80,5 +82,5 @@ val sub : nexp -> nexp -> nexp val mult : nexp -> nexp -> nexp val app : string -> nexp list -> nexp -val constant : Big_int.big_int -> nexp +val constant : Big_int.num -> nexp val variable : int -> nexp diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 4646ef6f..e9684414 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -26,7 +26,6 @@ let rec bind m f = match m with | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt)) end - let inline (>>=) = bind val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r let inline (>>) m n = m >>= fun _ -> n diff --git a/src/initial_check.ml b/src/initial_check.ml index ee88e16c..d5502d63 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -51,7 +51,7 @@ open Ast open Util open Ast_util -open Big_int +module Big_int = Nat_big_num let opt_undefined_gen = ref false let opt_magic_hash = ref false @@ -185,12 +185,12 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) let make_r bot top = match bot,top with | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) -> - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (add_big_int (sub_big_int t b) unit_big_int),l) + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) | bot,(Parse_ast.ATyp_aux(_,l) as top) -> Parse_ast.ATyp_aux((Parse_ast.ATyp_sum ((Parse_ast.ATyp_aux (Parse_ast.ATyp_sum (top, - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant unit_big_int,Parse_ast.Unknown)), + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.of_int 1),Parse_ast.Unknown)), Parse_ast.Unknown)), (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in let base = to_ast_nexp k_env b in @@ -206,9 +206,9 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) -> let make_sub_one t = match t with - | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (sub_big_int t unit_big_int),l) + | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.sub t (Big_int.of_int 1)),l) | t -> (Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (minus_big_int unit_big_int),Parse_ast.Unknown)), + (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.negate (Big_int.of_int 1)),Parse_ast.Unknown)), Parse_ast.Unknown)) in let (base,rise) = match def_ord with | Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r) @@ -291,10 +291,7 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect = let v = to_ast_var v in let mk = Envmap.apply k_env (var_to_string v) in (match mk with - | Some(k) -> (match k.k with - | K_Efct -> Effect_var v - | K_infer -> k.k <- K_Efct; Effect_var v - | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k)) + | Some k -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k) | None -> typ_error l "Encountered an unbound variable" None (Some v) None) | Parse_ast.ATyp_set(effects) -> Effect_set( List.map diff --git a/src/lexer.mll b/src/lexer.mll index 35ab6627..814e645e 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -50,7 +50,7 @@ { open Parser -open Big_int +module Big_int = Nat_big_num module M = Map.Make(String) exception LexError of string * Lexing.position @@ -330,8 +330,8 @@ rule token = parse | (digit+ as i1) "." (digit+ as i2) { (Real (i1 ^ "." ^ i2)) } | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) } - | digit+ as i { (Num(big_int_of_string i)) } - | "-" digit+ as i { (Num(big_int_of_string i)) } + | digit+ as i { (Num(Big_int.of_string i)) } + | "-" digit+ as i { (Num(Big_int.of_string i)) } | "0b" (binarydigit+ as i) { (Bin(i)) } | "0x" (hexdigit+ as i) { (Hex(i)) } | '"' { (String( diff --git a/src/lexer2.mll b/src/lexer2.mll index e43bd3e1..04ecdca3 100644 --- a/src/lexer2.mll +++ b/src/lexer2.mll @@ -50,7 +50,7 @@ { open Parser2 -open Big_int +module Big_int = Nat_big_num open Parse_ast module M = Map.Make(String) exception LexError of string * Lexing.position @@ -229,13 +229,13 @@ rule token = parse | "<=" { (LtEq(r"<=")) } | "infix" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators; - Fixity (Infix, big_int_of_string (Char.escaped p), op) } + Fixity (Infix, Big_int.of_string (Char.escaped p), op) } | "infixl" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators; - Fixity (InfixL, big_int_of_string (Char.escaped p), op) } + Fixity (InfixL, Big_int.of_string (Char.escaped p), op) } | "infixr" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators; - Fixity (InfixR, big_int_of_string (Char.escaped p), op) } + Fixity (InfixR, Big_int.of_string (Char.escaped p), op) } | operator as op { try M.find op !operators with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) } @@ -252,8 +252,8 @@ rule token = parse else Id(r i) } | (digit+ as i1) "." (digit+ as i2) { (Real (i1 ^ "." ^ i2)) } | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) } - | digit+ as i { (Num(big_int_of_string i)) } - | "-" digit+ as i { (Num(big_int_of_string i)) } + | digit+ as i { (Num(Big_int.of_string i)) } + | "-" digit+ as i { (Num(Big_int.of_string i)) } | "0b" (binarydigit+ as i) { (Bin(i)) } | "0x" (hexdigit+ as i) { (Hex(i)) } | '"' { (String( diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 05b9efcb..7d72b974 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -51,7 +51,7 @@ open Parse_ast open Ast open Ast_util -open Big_int +module Big_int = Nat_big_num open Type_check let size_set_limit = 8 @@ -138,18 +138,18 @@ let subst_src_typ substs t = in s_styp substs t let make_vector_lit sz i = - let f j = if eq_big_int (mod_big_int (shift_right_big_int i (sz-j-1)) (big_int_of_int 2)) zero_big_int then '0' else '1' in + let f j = if Big_int.equal (Big_int.modulus (Big_int.shift_right i (sz-j-1)) (Big_int.of_int 2)) Big_int.zero then '0' else '1' in let s = String.init sz f in L_aux (L_bin s,Generated Unknown) let tabulate f n = let rec aux acc n = let acc' = f n::acc in - if eq_big_int n zero_big_int then acc' else aux acc' (sub_big_int n unit_big_int) - in if eq_big_int n zero_big_int then [] else aux [] (sub_big_int n unit_big_int) + if Big_int.equal n Big_int.zero then acc' else aux acc' (Big_int.sub n (Big_int.of_int 1)) + in if Big_int.equal n Big_int.zero then [] else aux [] (Big_int.sub n (Big_int.of_int 1)) let make_vectors sz = - tabulate (make_vector_lit sz) (shift_left_big_int unit_big_int sz) + tabulate (make_vector_lit sz) (Big_int.shift_left (Big_int.of_int 1) sz) let pat_id_is_variable env id = match Env.lookup_id id env with @@ -412,7 +412,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) = in let name_seg = function | (_,None) -> "" - | (k,Some i) -> string_of_kid k ^ string_of_big_int i + | (k,Some i) -> string_of_kid k ^ Big_int.to_string i in let name l i = String.concat "_" (i::(List.map name_seg l)) in Some (List.map (fun (l,ty) -> (l, wrap (name l),ty)) variants) @@ -421,11 +421,11 @@ let reduce_nexp subst ne = let rec eval (Nexp_aux (ne,_) as nexp) = match ne with | Nexp_constant i -> i - | Nexp_sum (n1,n2) -> add_big_int (eval n1) (eval n2) - | Nexp_minus (n1,n2) -> sub_big_int (eval n1) (eval n2) - | Nexp_times (n1,n2) -> mult_big_int (eval n1) (eval n2) - | Nexp_exp n -> shift_left_big_int (eval n) 1 - | Nexp_neg n -> minus_big_int (eval n) + | Nexp_sum (n1,n2) -> Big_int.add (eval n1) (eval n2) + | Nexp_minus (n1,n2) -> Big_int.sub (eval n1) (eval n2) + | Nexp_times (n1,n2) -> Big_int.mul (eval n1) (eval n2) + | Nexp_exp n -> Big_int.shift_left (eval n) 1 + | Nexp_neg n -> Big_int.negate (eval n) | _ -> raise (Reporting_basic.err_general Unknown ("Couldn't turn nexp " ^ string_of_nexp nexp ^ " into concrete value")) @@ -465,7 +465,7 @@ let refine_constructor refinements l env id args = (fun v (_,w) -> match v,w with | _,None -> true - | Some (U_nexp (Nexp_aux (Nexp_constant n, _))),Some m -> eq_big_int n m + | Some (U_nexp (Nexp_aux (Nexp_constant n, _))),Some m -> Big_int.equal n m | _,_ -> false) bindings mapping in match List.find matches_refinement irefinements with @@ -617,7 +617,7 @@ let remove_bound env pat = let lit_match = function | (L_zero | L_false), (L_zero | L_false) -> true | (L_one | L_true ), (L_one | L_true ) -> true - | L_num i1, L_num i2 -> eq_big_int i1 i2 + | L_num i1, L_num i2 -> Big_int.equal i1 i2 | l1,l2 -> l1 = l2 (* There's no undefined nexp, so replace undefined sizes with a plausible size. @@ -660,8 +660,8 @@ let rec drop_casts = function | exp -> exp let int_of_str_lit = function - | L_hex hex -> big_int_of_string ("0x" ^ hex) - | L_bin bin -> big_int_of_string ("0b" ^ bin) + | L_hex hex -> Big_int.of_string ("0x" ^ hex) + | L_bin bin -> Big_int.of_string ("0b" ^ bin) | _ -> assert false let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) = @@ -670,9 +670,9 @@ let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) = | (L_one |L_true ), (L_one |L_true) -> Some true | (L_hex _| L_bin _), (L_hex _|L_bin _) - -> Some (eq_big_int (int_of_str_lit l1) (int_of_str_lit l2)) + -> Some (Big_int.equal (int_of_str_lit l1) (int_of_str_lit l2)) | L_undef, _ | _, L_undef -> None - | L_num i1, L_num i2 -> Some (eq_big_int i1 i2) + | L_num i1, L_num i2 -> Some (Big_int.equal i1 i2) | _ -> Some (l1 = l2) let try_app (l,ann) (id,args) = @@ -704,12 +704,12 @@ let try_app (l,ann) (id,args) = else if is_id "shl_int" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> - Some (E_aux (E_lit (L_aux (L_num (shift_left_big_int i (int_of_big_int j)),new_l)),(l,ann))) + Some (E_aux (E_lit (L_aux (L_num (Big_int.shift_left i (Big_int.to_int j)),new_l)),(l,ann))) | _ -> None else if is_id "mult_int" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> - Some (E_aux (E_lit (L_aux (L_num (mult_big_int i j),new_l)),(l,ann))) + Some (E_aux (E_lit (L_aux (L_num (Big_int.mul i j),new_l)),(l,ann))) | _ -> None else if is_id "ex_int" then match args with @@ -720,8 +720,8 @@ let try_app (l,ann) (id,args) = | [E_aux (E_lit L_aux ((L_hex _ | L_bin _) as lit,_),_); E_aux (E_lit L_aux (L_num i,_),_)] -> let v = int_of_str_lit lit in - let b = and_big_int (shift_right_big_int v (int_of_big_int i)) unit_big_int in - let lit' = if eq_big_int b unit_big_int then L_one else L_zero in + let b = Big_int.bitwise_and (Big_int.shift_right v (Big_int.to_int i)) (Big_int.of_int 1) in + let lit' = if Big_int.equal b (Big_int.of_int 1) then L_one else L_zero in Some (E_aux (E_lit (L_aux (lit',new_l)),(l,ann))) | _ -> None else None @@ -1231,14 +1231,14 @@ let split_defs splits defs = | Typ_app (Id_aux (Id "vector",_), [_;Typ_arg_aux (Typ_arg_nexp len,_);_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> (match len with | Nexp_aux (Nexp_constant sz,_) -> - if int_of_big_int sz <= vector_split_limit then - let lits = make_vectors (int_of_big_int sz) in + if Big_int.to_int sz <= vector_split_limit then + let lits = make_vectors (Big_int.to_int sz) in List.map (fun lit -> P_aux (P_lit lit,(l,annot)), [var,E_aux (E_lit lit,(new_l,annot))]) lits else raise (Reporting_basic.err_general l - ("Refusing to split vector type of length " ^ string_of_big_int sz ^ + ("Refusing to split vector type of length " ^ Big_int.to_string sz ^ " above limit " ^ string_of_int vector_split_limit ^ " for variable " ^ v)) | _ -> diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index ac6f6ef3..aed736a7 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -53,6 +53,8 @@ open Ast_util open PPrint open Type_check +module Big_int = Nat_big_num + (* Option to turn tracing features on or off *) let opt_trace_ocaml = ref false @@ -179,7 +181,7 @@ let ocaml_lit (L_aux (lit_aux, _)) = | L_one -> string "B1" | L_true -> string "true" | L_false -> string "false" - | L_num n -> parens (string "big_int_of_string" ^^ space ^^ string ("\"" ^ Big_int.string_of_big_int n ^ "\"")) + | L_num n -> parens (string "Big_int.of_string" ^^ space ^^ string ("\"" ^ Big_int.to_string n ^ "\"")) | L_undef -> failwith "undefined should have been re-written prior to ocaml backend" | L_string str -> string_lit str | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str))) @@ -281,13 +283,13 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in let loop_mod = match ord with - | Ord_aux (Ord_inc, _) -> string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step - | Ord_aux (Ord_dec, _) -> string "sub_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step + | Ord_aux (Ord_inc, _) -> string "Big_int.add" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step + | Ord_aux (Ord_dec, _) -> string "Big_int.sub" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step in let loop_compare = match ord with - | Ord_aux (Ord_inc, _) -> string "le_big_int" - | Ord_aux (Ord_dec, _) -> string "gt_big_int" + | Ord_aux (Ord_inc, _) -> string "Big_int.less_equal" + | Ord_aux (Ord_dec, _) -> string "Big_int.greater" in let loop_body = separate space [string "if"; loop_compare; zencode ctx id; ocaml_atomic_exp ctx exp_to] @@ -614,7 +616,7 @@ let ocaml_defs (Defs defs) = else empty in (string "open Sail_lib;;" ^^ hardline) - ^^ (string "open Big_int" ^^ ocaml_def_end) + ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end) ^^ concat (List.map (ocaml_def ctx) defs) ^^ empty_reg_init diff --git a/src/parse_ast.ml b/src/parse_ast.ml index b684725f..bfbb0090 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -50,7 +50,7 @@ (* generated by Ott 0.25 from: l2_parse.ott *) -open Big_int +module Big_int = Nat_big_num type text = string @@ -139,7 +139,7 @@ type atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) ATyp_id of id (* identifier *) | ATyp_var of kid (* ticked variable *) - | ATyp_constant of big_int (* constant *) + | ATyp_constant of Big_int.num (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) | ATyp_minus of atyp * atyp (* subtraction *) @@ -170,7 +170,7 @@ n_constraint_aux = (* constraint over kind $_$ *) | NC_bounded_ge of atyp * atyp | NC_bounded_le of atyp * atyp | NC_not_equal of atyp * atyp - | NC_set of kid * (big_int) list + | NC_set of kid * (Big_int.num) list | NC_or of n_constraint * n_constraint | NC_and of n_constraint * n_constraint | NC_true @@ -213,7 +213,7 @@ lit_aux = (* Literal constant *) | L_one (* $_ : _$ *) | L_true (* $_ : _$ *) | L_false (* $_ : _$ *) - | L_num of big_int (* natural number constant *) + | L_num of Big_int.num (* natural number constant *) | L_hex of string (* bit vector constant, C-style *) | L_bin of string (* bit vector constant, C-style *) | L_undef (* undefined value *) @@ -396,8 +396,8 @@ type_union = type index_range_aux = (* index specification, for bitfields in register types *) - BF_single of big_int (* single index *) - | BF_range of big_int * big_int (* index range *) + BF_single of Big_int.num (* single index *) + | BF_range of Big_int.num * Big_int.num (* index range *) | BF_concat of index_range * index_range (* concatenation of index ranges *) and index_range = @@ -492,7 +492,7 @@ scattered_def = type prec = Infix | InfixL | InfixR -type fixity_token = (prec * big_int * string) +type fixity_token = (prec * Big_int.num * string) type def = (* Top-level definition *) @@ -501,7 +501,7 @@ def = (* Top-level definition *) | DEF_fundef of fundef (* function definition *) | DEF_val of letbind (* value definition *) | DEF_overload of id * id list (* operator overload specifications *) - | DEF_fixity of prec * big_int * id (* fixity declaration *) + | DEF_fixity of prec * Big_int.num * id (* fixity declaration *) | DEF_spec of val_spec (* top-level type constraint *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) diff --git a/src/parser.mly b/src/parser.mly index 5e4a2cad..43dc0a74 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -52,7 +52,7 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *) -open Big_int +module Big_int = Nat_big_num open Parse_ast let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos()) @@ -108,16 +108,16 @@ let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown) let make_range_sugar_bounded typ1 typ2 = ATyp_app(Id_aux(Id("range"),Unknown),[typ1; typ2;]) let make_range_sugar typ1 = - make_range_sugar_bounded (ATyp_aux(ATyp_constant(zero_big_int), Unknown)) typ1 + make_range_sugar_bounded (ATyp_aux(ATyp_constant(Big_int.zero), Unknown)) typ1 let make_atom_sugar typ1 = ATyp_app(Id_aux(Id("atom"),Unknown),[typ1]) let make_r bot top = match bot,top with | ATyp_aux(ATyp_constant b,_),ATyp_aux(ATyp_constant t,l) -> - ATyp_aux(ATyp_constant (add_big_int (sub_big_int t b) unit_big_int),l) + ATyp_aux(ATyp_constant (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) | bot,(ATyp_aux(_,l) as top) -> - ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant unit_big_int,Unknown)), Unknown)), + ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant (Big_int.of_int 1),Unknown)), Unknown)), (ATyp_aux ((ATyp_neg bot),Unknown)))), l) let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 = @@ -131,11 +131,11 @@ let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 = else (typ2, ATyp_default_ord,"vector_sugar_r") (* rise and base not calculated, rise only from specification *) in ATyp_app(Id_aux(Id(name),Unknown),[typ1;rise;ATyp_aux(ord,Unknown);typ]) let make_vector_sugar order_set is_inc typ typ1 = - let zero = (ATyp_aux(ATyp_constant zero_big_int,Unknown)) in + let zero = (ATyp_aux(ATyp_constant Big_int.zero,Unknown)) in let (typ1,typ2) = match (order_set,is_inc,typ1) with - | (true,true,ATyp_aux(ATyp_constant t,l)) -> zero,ATyp_aux(ATyp_constant (sub_big_int t unit_big_int),l) + | (true,true,ATyp_aux(ATyp_constant t,l)) -> zero,ATyp_aux(ATyp_constant (Big_int.sub t (Big_int.of_int 1)),l) | (true,true,ATyp_aux(_, l)) -> zero,ATyp_aux (ATyp_sum (typ1, - ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant unit_big_int,Unknown)), Unknown)), l) + ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant (Big_int.of_int 1),Unknown)), Unknown)), l) | (true,false,_) -> typ1,zero | (false,_,_) -> zero,typ1 in make_vector_sugar_bounded order_set is_inc "vector_sugar_r" typ typ1 typ2 @@ -166,7 +166,7 @@ let make_vector_sugar order_set is_inc typ typ1 = /*Terminals with content*/ %token <string> Id TyVar TyId -%token <Big_int.big_int> Num +%token <Nat_big_num.num> Num %token <string> String Bin Hex Real %token <string> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde @@ -694,7 +694,7 @@ right_atomic_exp: raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop")); if $6 <> "to" && $6 <> "downto" then raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop")); - let step = eloc (E_lit(lloc (L_num unit_big_int))) in + let step = eloc (E_lit(lloc (L_num (Big_int.of_int 1)))) in let ord = if $6 = "to" then ATyp_aux(ATyp_inc,(locn 6 6)) diff --git a/src/parser2.mly b/src/parser2.mly index c222bb39..6021596f 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -52,7 +52,7 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *) -open Big_int +module Big_int = Nat_big_num open Parse_ast let loc n m = Range (n, m) @@ -113,12 +113,12 @@ let rec desugar_lchain chain s e = | [LC_nexp n1; LC_lteq; LC_nexp n2] -> mk_nc (NC_bounded_le (n1, n2)) s e | [LC_nexp n1; LC_lt; LC_nexp n2] -> - mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant unit_big_int) s e)) s e, n2)) s e + mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e, n2)) s e | (LC_nexp n1 :: LC_lteq :: LC_nexp n2 :: chain) -> let nc1 = mk_nc (NC_bounded_le (n1, n2)) s e in mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e | (LC_nexp n1 :: LC_lt :: LC_nexp n2 :: chain) -> - let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant unit_big_int) s e)) s e, n2)) s e in + let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e, n2)) s e in mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e | _ -> assert false @@ -132,12 +132,12 @@ let rec desugar_rchain chain s e = | [RC_nexp n1; RC_gteq; RC_nexp n2] -> mk_nc (NC_bounded_ge (n1, n2)) s e | [RC_nexp n1; RC_gt; RC_nexp n2] -> - mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant unit_big_int) s e)) s e)) s e + mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e)) s e | (RC_nexp n1 :: RC_gteq :: RC_nexp n2 :: chain) -> let nc1 = mk_nc (NC_bounded_ge (n1, n2)) s e in mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e | (RC_nexp n1 :: RC_gt :: RC_nexp n2 :: chain) -> - let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant unit_big_int) s e)) s e)) s e in + let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e)) s e in mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e | _ -> assert false @@ -162,7 +162,7 @@ let rec desugar_rchain chain s e = /*Terminals with content*/ %token <string> Id TyVar -%token <Big_int.big_int> Num +%token <Nat_big_num.num> Num %token <string> String Bin Hex Real %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit @@ -739,7 +739,7 @@ exp: raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop")); if $6 <> "to" && $6 <> "downto" then raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop")); - let step = mk_lit_exp (L_num unit_big_int) $startpos $endpos in + let step = mk_lit_exp (L_num (Big_int.of_int 1)) $startpos $endpos in let ord = if $6 = "to" then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6)) diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index bad03034..98efa4ce 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -49,7 +49,7 @@ (**************************************************************************) open Ast -open Big_int +module Big_int = Nat_big_num open PPrint let pipe = string "|" @@ -76,7 +76,7 @@ let comma_sp = comma ^^ space let colon_sp = spaces colon let doc_var (Kid_aux(Var v,_)) = string v -let doc_int i = string (string_of_big_int i) +let doc_int i = string (Big_int.to_string i) let doc_op symb a b = infix 2 1 symb a b let doc_unop symb a = prefix 2 1 symb a @@ -112,7 +112,6 @@ let doc_effect (BE_aux (e,_)) = | BE_nondet -> "nondet") let doc_effects (Effect_aux(e,_)) = match e with - | Effect_var v -> doc_var v | Effect_set [] -> string "pure" | Effect_set s -> braces (separate_map comma_sp doc_effect s) @@ -176,7 +175,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = | Typ_app(Id_aux (Id "range", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); Typ_arg_aux(Typ_arg_nexp m, _);]) -> - (squarebars (if eq_big_int n zero_big_int then nexp m else doc_op colon (doc_int n) (nexp m))) + (squarebars (if Big_int.equal n Big_int.zero then nexp m else doc_op colon (doc_int n) (nexp m))) | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> (squarecolons (nexp n)) | Typ_app(id,args) -> @@ -220,7 +219,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_var v -> doc_var v | Nexp_id i -> braces (doc_id i) - | Nexp_constant i -> if lt_big_int i zero_big_int then parens(doc_int i) else doc_int i + | Nexp_constant i -> if Big_int.less i Big_int.zero then parens(doc_int i) else doc_int i | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _-> group (parens (nexp ne)) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c76be843..11b34a3d 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -52,7 +52,6 @@ open Type_check open Ast open Ast_util open Rewriter -open Big_int open PPrint open Pretty_print_common @@ -149,10 +148,7 @@ let effectful_set = | BE_escape -> true | _ -> false) -let effectful (Effect_aux (eff,_)) = - match eff with - | Effect_var _ -> failwith "effectful: Effect_var not supported" - | Effect_set effs -> effectful_set effs +let effectful (Effect_aux (Effect_set effs, _)) = effectful_set effs let is_regtyp (Typ_aux (typ, _)) env = match typ with | Typ_app(id, _) when string_of_id id = "register" -> true @@ -162,14 +158,14 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with let doc_nexp_lem nexp = let (Nexp_aux (nexp, l) as full_nexp) = nexp_simp nexp in match nexp with - | Nexp_constant i -> string ("ty" ^ string_of_big_int i) + | Nexp_constant i -> string ("ty" ^ Big_int.to_string i) | Nexp_var v -> string (string_of_kid (orig_kid v)) | _ -> let rec mangle_nexp (Nexp_aux (nexp, _)) = begin match nexp with | Nexp_id id -> string_of_id id | Nexp_var kid -> string_of_id (id_of_kid (orig_kid kid)) - | Nexp_constant i -> Pretty_print_lem_ast.lemnum string_of_big_int i + | Nexp_constant i -> Pretty_print_lem_ast.lemnum Big_int.to_string i | Nexp_times (n1, n2) -> mangle_nexp n1 ^ "_times_" ^ mangle_nexp n2 | Nexp_sum (n1, n2) -> mangle_nexp n1 ^ "_plus_" ^ mangle_nexp n2 | Nexp_minus (n1, n2) -> mangle_nexp n1 ^ "_minus_" ^ mangle_nexp n2 @@ -362,10 +358,10 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a = | L_false -> utf8string "false" | L_true -> utf8string "true" | L_num i -> - let ipp = string_of_big_int i in + let ipp = Big_int.to_string i in utf8string ( if in_pat then "("^ipp^":nn)" - else if lt_big_int i zero_big_int then "((0"^ipp^"):ii)" + else if Big_int.less i Big_int.zero then "((0"^ipp^"):ii)" else "("^ipp^":ii)") | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) @@ -391,14 +387,14 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a = using this would require adding a dependency on ZArith to Sail. *) let parts = Util.split_on_char '.' s in let (num, denom) = match parts with - | [i] -> (big_int_of_string i, unit_big_int) + | [i] -> (Big_int.of_string i, (Big_int.of_int 1)) | [i;f] -> - let denom = power_int_positive_int 10 (String.length f) in - (add_big_int (mult_big_int (big_int_of_string i) denom) (big_int_of_string f), denom) + let denom = Big_int.pow_int_positive 10 (String.length f) in + (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom) | _ -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in - separate space (List.map string ["realFromFrac"; string_of_big_int num; string_of_big_int denom]) + separate space (List.map string ["realFromFrac"; Big_int.to_string num; Big_int.to_string denom]) (* typ_doc is the doc for the type being quantified *) let doc_quant_item vars_included (QI_aux (qi, _)) = match qi with @@ -791,7 +787,7 @@ let doc_exp_lem, doc_let_lem = "E_vector of non-vector type") in let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in let start = match nexp_simp start with - | Nexp_aux (Nexp_constant i, _) -> string_of_big_int i + | Nexp_aux (Nexp_constant i, _) -> Big_int.to_string i | _ -> if dir then "0" else string_of_int (List.length exps) in let expspp = match exps with @@ -973,12 +969,12 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with raise (Reporting_basic.err_unreachable Parse_ast.Unknown ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start)) with - | _ -> (zero_big_int, true) in + | _ -> (Big_int.zero, true) in doc_op equals (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) (anglebars (concat [space; doc_op equals (string "field_name") (string_lit (doc_id_lem fid)); semi_sp; - doc_op equals (string "field_start") (string (string_of_big_int start)); semi_sp; + doc_op equals (string "field_start") (string (Big_int.to_string start)); semi_sp; doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp; doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in @@ -1174,7 +1170,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with let dir = (if dir_b then "true" else "false") in let dir_suffix = (if dir_b then "_inc" else "_dec") in let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in - let size = if dir_b then add_big_int (sub_big_int i2 i1) unit_big_int else add_big_int (sub_big_int i1 i2) unit_big_int in + let size = if dir_b then Big_int.add (Big_int.sub i2 i1) (Big_int.of_int 1) else Big_int.add (Big_int.sub i1 i2) (Big_int.of_int 1) in let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in let tannot = doc_tannot_lem sequential mwords false vtyp in let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id); @@ -1405,11 +1401,11 @@ let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) = | BF_aux (BF_range (i, j), _) -> (i, j) | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown ("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in - let fsize = succ_big_int (abs_big_int (sub_big_int i j)) in + let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in (* TODO Assumes normalised, decreasing bitvector slices; however, since start indices or indexing order do not appear in Lem type annotations, this does not matter. *) - let ftyp = vector_typ (nconstant (pred_big_int fsize)) (nconstant fsize) dec_ord bit_typ in + let ftyp = vector_typ (nconstant (Big_int.pred fsize)) (nconstant fsize) dec_ord bit_typ in let reftyp = mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), [mk_typ_arg (Typ_arg_typ (mk_id_typ (mk_id tname))); @@ -1419,7 +1415,7 @@ let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) = (concat [string "let "; parens (concat [string tname; underscore; doc_id_lem fid; rfannot])]) (concat [ space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline; - space; space; space; string (" field_start = " ^ string_of_big_int i ^ ";"); hardline; + space; space; space; string (" field_start = " ^ Big_int.to_string i ^ ";"); hardline; space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline; space; space; space; string (" get_field = (fun reg -> get_" ^ tname ^ "_" ^ string_of_id fid ^ "(reg));"); hardline; space; space; space; string (" set_field = (fun reg v -> set_" ^ tname ^ "_" ^ string_of_id fid ^ "(reg, v)) "); ranglebar]) @@ -1525,10 +1521,10 @@ let doc_register_refs_lem registers = raise (Reporting_basic.err_unreachable Parse_ast.Unknown ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start)) with - | _ -> (zero_big_int, true) in + | _ -> (Big_int.zero, true) in concat [string "let "; idd; string " = <|"; hardline; string " reg_name = \""; idd; string "\";"; hardline; - string " reg_start = "; string (string_of_big_int start); string ";"; hardline; + string " reg_start = "; string (Big_int.to_string start); string ";"; hardline; string " reg_is_inc = "; string (if is_inc then "true" else "false"); string ";"; hardline; string " read_from = (fun s -> s."; field; string ");"; hardline; string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 3b7a7345..110c0b31 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -51,7 +51,6 @@ open Type_check open Ast open Format -open Big_int open Pretty_print_common (**************************************************************************** @@ -78,11 +77,11 @@ let base ppf s = fprintf ppf "%s" s let quot_string ppf s = fprintf ppf "\"%s\"" s let lemnum default n = - if le_big_int zero_big_int n && le_big_int n (big_int_of_int 128) then - "int" ^ string_of_big_int n - else if ge_big_int n zero_big_int then + if Big_int.less_equal Big_int.zero n && Big_int.less_equal n (Big_int.of_int 128) then + "int" ^ Big_int.to_string n + else if Big_int.greater_equal n Big_int.zero then default n - else ("(int0 - " ^ (default (abs_big_int n)) ^ ")") + else ("(int0 - " ^ (default (Big_int.abs n)) ^ ")") let pp_format_id (Id_aux(i,_)) = match i with @@ -151,7 +150,7 @@ and pp_format_nexp_lem (Nexp_aux(n,l)) = (match n with | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")" | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")" - | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_big_int i) ^ ")" + | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum Big_int.to_string i) ^ ")" | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" @@ -189,7 +188,6 @@ and pp_format_base_effect_lem (BE_aux(e,l)) = and pp_format_effects_lem (Effect_aux(e,l)) = "(Effect_aux " ^ (match e with - | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")" | Effect_set(efcts) -> "(Effect_set [" ^ (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^ @@ -215,7 +213,7 @@ and pp_format_nexp_constraint_lem (NC_aux(nc,l)) = | NC_set(id,bounds) -> "(NC_set " ^ pp_format_var_lem id ^ " [" ^ - list_format "; " string_of_big_int bounds ^ + list_format "; " Big_int.to_string bounds ^ "])") ^ " " ^ (pp_format_l_lem l) ^ ")" @@ -278,7 +276,7 @@ let pp_format_lit_lem (L_aux(lit,l)) = | L_one -> "L_one" | L_true -> "L_true" | L_false -> "L_false" - | L_num(i) -> "(L_num " ^ (lemnum string_of_big_int i) ^ ")" + | L_num(i) -> "(L_num " ^ (lemnum Big_int.to_string i) ^ ")" | L_hex(n) -> "(L_hex \"" ^ n ^ "\")" | L_bin(n) -> "(L_bin \"" ^ n ^ "\")" | L_undef -> "L_undef" @@ -430,14 +428,14 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) = | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> (match r.nexp with | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" - kwd (lemnum string_of_int (int_of_big_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) + kwd (lemnum string_of_int (Big_int.to_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]" kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length")) | Tapp("implicit",[TA_nexp r]) -> (match r.nexp with | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" - kwd (lemnum string_of_int (int_of_big_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) + kwd (lemnum string_of_int (Big_int.to_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]" kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const")) @@ -518,8 +516,8 @@ let pp_lem_namescm ppf (Name_sect_aux(ns,l)) = let rec pp_lem_range ppf (BF_aux(r,l)) = match r with - | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" (int_of_big_int i) pp_lem_l l - | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" (int_of_big_int i1) (int_of_big_int i2) pp_lem_l l + | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" (Big_int.to_int i) pp_lem_l l + | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" (Big_int.to_int i1) (Big_int.to_int i2) pp_lem_l l | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l let pp_lem_typdef ppf (TD_aux(td,(l,annot))) = @@ -626,7 +624,7 @@ let rec pp_lem_def ppf d = | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec | DEF_comm d -> fprintf ppf "" - | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum string_of_big_int n) pp_lem_id id + | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum Big_int.to_string n) pp_lem_id id | DEF_internal_mutrec f_defs -> List.iter (fun f_def -> pp_lem_def ppf (DEF_fundef f_def)) f_defs | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 3868502b..8302c32d 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -50,7 +50,6 @@ open Ast open Ast_util -open Big_int open PPrint open Pretty_print_common @@ -97,7 +96,7 @@ let doc_lit (L_aux(l,_)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num i -> string_of_big_int i + | L_num i -> Big_int.to_string i | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_real r -> r @@ -357,12 +356,12 @@ let doc_exp, doc_let = | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> (match r.nexp with | Nvar v -> utf8string v - | Nconst bi -> utf8string (Big_int.string_of_big_int bi) + | Nconst bi -> utf8string (Big_int.Big_int.to_string bi) | _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given vector without known length, instead given " ^ n_to_string r))) | Tapp("implicit",[TA_nexp r]) -> (match r.nexp with - | Nconst bi -> utf8string (Big_int.string_of_big_int bi) + | Nconst bi -> utf8string (Big_int.Big_int.to_string bi) | Nvar v -> utf8string v | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const")) | _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t))) diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 17185cc9..33743188 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -50,9 +50,10 @@ open Ast open Ast_util -open Big_int open PPrint +module Big_int = Nat_big_num + let doc_op symb a b = infix 2 1 symb a b let doc_id (Id_aux (id_aux, _)) = @@ -62,7 +63,7 @@ let doc_id (Id_aux (id_aux, _)) = let doc_kid kid = string (Ast_util.string_of_kid kid) -let doc_int n = string (string_of_big_int n) +let doc_int n = string (Big_int.to_string n) let doc_ord (Ord_aux(o,_)) = match o with | Ord_var v -> doc_kid v @@ -72,7 +73,7 @@ let doc_ord (Ord_aux(o,_)) = match o with let rec doc_nexp = let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) = match n_aux with - | Nexp_constant c -> string (string_of_big_int c) + | Nexp_constant c -> string (Big_int.to_string c) | Nexp_id id -> doc_id id | Nexp_var kid -> doc_kid kid | _ -> parens (nexp0 nexp) @@ -80,8 +81,8 @@ let rec doc_nexp = match n_aux with | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) -> separate space [nexp0 n1; string "-"; nexp1 n2] - | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when lt_big_int c zero_big_int -> - separate space [nexp0 n1; string "-"; doc_int (abs_big_int c)] + | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when Big_int.less c Big_int.zero -> + separate space [nexp0 n1; string "-"; doc_int (Big_int.abs c)] | Nexp_sum (n1, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2] | _ -> nexp1 nexp and nexp1 (Nexp_aux (n_aux, _) as nexp) = @@ -197,7 +198,7 @@ let doc_lit (L_aux(l,_)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num i -> string_of_big_int i + | L_num i -> Big_int.to_string i | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_real r -> r @@ -517,7 +518,7 @@ let rec doc_def def = group (match def with | DEF_reg_dec dec -> doc_dec dec | DEF_scattered sdef -> doc_scattered sdef | DEF_fixity (prec, n, id) -> - fixities := Bindings.add id (prec, int_of_big_int n) !fixities; + fixities := Bindings.add id (prec, Big_int.to_int n) !fixities; separate space [doc_prec prec; doc_int n; doc_id id] | DEF_overload (id, ids) -> separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] diff --git a/src/rewriter.ml b/src/rewriter.ml index 88fb17a5..468b3a84 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -48,7 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Big_int +module Big_int = Nat_big_num open Ast open Ast_util open Type_check diff --git a/src/rewriter.mli b/src/rewriter.mli index dc592a4d..09dddb95 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -48,7 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Big_int +module Big_int = Nat_big_num open Ast open Type_check diff --git a/src/rewrites.ml b/src/rewrites.ml index 424931c3..2b5df2a2 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -48,7 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Big_int +module Big_int = Nat_big_num open Ast open Ast_util open Type_check @@ -169,7 +169,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = constants? This will resolve a 'n - 1 sizeof when 'n is in scope. *) | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) -> - let one_exp = infer_exp env (mk_lit_exp (L_num unit_big_int)) in + let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in Some (E_aux (E_app (mk_id "add_range", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect)))) | _ -> begin @@ -643,8 +643,8 @@ let remove_vector_concat_pat pat = let (start,last_idx) = (match vector_typ_args_of rtyp with | (Nexp_aux (Nexp_constant start,_), Nexp_aux (Nexp_constant length,_), ord, _) -> (start, if is_order_inc ord - then sub_big_int (add_big_int start length) unit_big_int - else add_big_int (sub_big_int start length) unit_big_int) + then Big_int.sub (Big_int.add start length) (Big_int.of_int 1) + else Big_int.add (Big_int.sub start length) (Big_int.of_int 1)) | _ -> raise (Reporting_basic.err_unreachable (fst rannot') ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in @@ -654,8 +654,8 @@ let remove_vector_concat_pat pat = let (pos',index_j) = match length with | Nexp_aux (Nexp_constant i,_) -> if is_order_inc ord - then (add_big_int pos i, sub_big_int (add_big_int pos i) unit_big_int) - else (sub_big_int pos i, add_big_int (sub_big_int pos i) unit_big_int) + then (Big_int.add pos i, Big_int.sub (Big_int.add pos i) (Big_int.of_int 1)) + else (Big_int.sub pos i, Big_int.add (Big_int.sub pos i) (Big_int.of_int 1)) | Nexp_aux (_,l) -> if is_last then (pos,last_idx) else @@ -755,8 +755,8 @@ let remove_vector_concat_pat pat = with vector_concats patterns as direct child-nodes anymore *) let range a b = - let rec aux a b = if gt_big_int a b then [] else a :: aux (add_big_int a unit_big_int) b in - if gt_big_int a b then List.rev (aux b a) else aux a b in + let rec aux a b = if Big_int.greater a b then [] else a :: aux (Big_int.add a (Big_int.of_int 1)) b in + if Big_int.greater a b then List.rev (aux b a) else aux a b in let remove_vector_concats = let p_vector_concat ps = @@ -770,9 +770,9 @@ let remove_vector_concat_pat pat = match p, vector_typ_args_of typ with | P_vector ps,_ -> acc @ ps | _, (_,Nexp_aux (Nexp_constant length,_),_,_) -> - acc @ (List.map wild (range zero_big_int (sub_big_int length unit_big_int))) + acc @ (List.map wild (range Big_int.zero (Big_int.sub length (Big_int.of_int 1)))) | _, _ -> - (*if is_last then*) acc @ [wild zero_big_int] + (*if is_last then*) acc @ [wild Big_int.zero] else raise (Reporting_basic.err_unreachable l ("remove_vector_concats: Non-vector in vector-concat pattern " ^ @@ -1106,7 +1106,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = let subvec_exp = match start, length with | Nexp_aux (Nexp_constant s, _), Nexp_aux (Nexp_constant l, _) - when eq_big_int s i && eq_big_int l (big_int_of_int (List.length lits)) -> + when Big_int.equal s i && Big_int.equal l (Big_int.of_int (List.length lits)) -> mk_exp (E_id rootid) | _ -> mk_exp (E_vector_subrange (mk_exp (E_id rootid), mk_num_exp i, mk_num_exp j)) in @@ -1139,7 +1139,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = let collect_guards_decls ps rootid t = let (start,_,ord,_) = vector_typ_args_of t in let rec collect current (guards,dls) idx ps = - let idx' = if is_order_inc ord then add_big_int idx unit_big_int else sub_big_int idx unit_big_int in + let idx' = if is_order_inc ord then Big_int.add idx (Big_int.of_int 1) else Big_int.sub idx (Big_int.of_int 1) in (match ps with | pat :: ps' -> (match pat with @@ -1547,7 +1547,7 @@ let rewrite_register_ref_writes (Defs defs) = let dir_b = i1 < i2 in let dir = (if dir_b then "true" else "false") in let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in - let size = if dir_b then succ_big_int (sub_big_int i2 i1) else succ_big_int (sub_big_int i1 i2) in + let size = if dir_b then Big_int.succ (Big_int.sub i2 i1) else Big_int.succ (Big_int.sub i1 i2) in let rtyp = mk_id_typ id in let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in let accessors (fr, fid) = @@ -2016,15 +2016,15 @@ let rewrite_tuple_vector_assignments defs = let (_, len, _, _) = vector_typ_args_of ltyp in match nexp_simp len with | Nexp_aux (Nexp_constant len, _) -> len - | _ -> unit_big_int - else unit_big_int in + | _ -> (Big_int.of_int 1) + else (Big_int.of_int 1) in let next i step = if is_order_inc ord - then (sub_big_int (add_big_int i step) unit_big_int, add_big_int i step) - else (add_big_int (sub_big_int i step) unit_big_int, sub_big_int i step) in + then (Big_int.sub (Big_int.add i step) (Big_int.of_int 1), Big_int.add i step) + else (Big_int.add (Big_int.sub i step) (Big_int.of_int 1), Big_int.sub i step) in let i = match nexp_simp start with | (Nexp_aux (Nexp_constant i, _)) -> i - | _ -> if is_order_inc ord then zero_big_int else big_int_of_int (List.length lexps - 1) in + | _ -> if is_order_inc ord then Big_int.zero else Big_int.of_int (List.length lexps - 1) in let l = gen_loc (fst annot) in let exp' = if small exp then strip_exp exp 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) diff --git a/src/type_check.ml b/src/type_check.ml index 5bd633ee..ac5f19f8 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -51,7 +51,7 @@ open Ast open Util open Ast_util -open Big_int +module Big_int = Nat_big_num (* opt_tc_debug controls the verbosity of the type checker. 0 is silent, 1 prints a tree of the type derivation and 2 is like 1 but @@ -303,9 +303,9 @@ module Env : sig val is_register : id -> t -> bool val get_register : id -> t -> typ val add_register : id -> typ -> t -> t - val add_regtyp : id -> big_int -> big_int -> (index_range * id) list -> t -> t + val add_regtyp : id -> Big_int.num -> Big_int.num -> (index_range * id) list -> t -> t val is_regtyp : id -> t -> bool - val get_regtyp : id -> t -> big_int * big_int * (index_range * id) list + val get_regtyp : id -> t -> Big_int.num * Big_int.num * (index_range * id) list val is_mutable : id -> t -> bool val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t @@ -360,7 +360,7 @@ end = struct locals : (mut * typ) Bindings.t; union_ids : (typquant * typ) Bindings.t; registers : typ Bindings.t; - regtyps : (big_int * big_int * (index_range * id) list) Bindings.t; + regtyps : (Big_int.num * Big_int.num * (index_range * id) list) Bindings.t; variants : (typquant * type_union list) Bindings.t; typ_vars : base_kind_aux KBindings.t; typ_synonyms : (t -> typ_arg list -> typ) Bindings.t; @@ -763,11 +763,11 @@ end = struct | BF_single n -> if cmp f n && cmp n t then n - else typ_error l ("Badly ordered index range: " ^ string_of_list ", " string_of_big_int [f; n; t]) + else typ_error l ("Badly ordered index range: " ^ string_of_list ", " Big_int.to_string [f; n; t]) | BF_range (n1, n2) -> if cmp f n1 && cmp n1 n2 && cmp n2 t then n2 - else typ_error l ("Badly ordered index range: " ^ string_of_list ", " string_of_big_int [f; n1; n2; t]) + else typ_error l ("Badly ordered index range: " ^ string_of_list ", " Big_int.to_string [f; n1; n2; t]) | BF_concat _ -> typ_error l "Index range concatenation currently unsupported" let rec check_index_ranges ids cmp base top = function @@ -797,9 +797,9 @@ end = struct else begin typ_print ("Adding register type " ^ string_of_id id); - if gt_big_int base top - then check_index_ranges IdSet.empty gt_big_int (add_big_int base unit_big_int) (sub_big_int top unit_big_int) ranges - else check_index_ranges IdSet.empty lt_big_int (sub_big_int base unit_big_int) (add_big_int top unit_big_int) ranges; + if Big_int.greater base top + then check_index_ranges IdSet.empty Big_int.greater (Big_int.add base (Big_int.of_int 1)) (Big_int.sub top (Big_int.of_int 1)) ranges + else check_index_ranges IdSet.empty Big_int.less (Big_int.sub base (Big_int.of_int 1)) (Big_int.add top (Big_int.of_int 1)) ranges; { env with regtyps = Bindings.add id (base, top, ranges) env.regtyps } end @@ -920,7 +920,7 @@ end = struct rewrap (Typ_app (id, List.map aux_arg targs)) | Typ_id id when is_regtyp id env -> let base, top, ranges = get_regtyp id env in - let len = succ_big_int (abs_big_int (sub_big_int top base)) in + let len = Big_int.succ (Big_int.abs (Big_int.sub top base)) in vector_typ (nconstant base) (nconstant len) (get_default_order env) bit_typ (* TODO registers with non-default order? non-bitvector registers? *) | t -> rewrap t @@ -1124,7 +1124,7 @@ let rec nexp_constraint env var_of (Nexp_aux (nexp, l)) = | Nexp_sum (nexp1, nexp2) -> Constraint.add (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2) | Nexp_minus (nexp1, nexp2) -> Constraint.sub (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2) | Nexp_exp nexp -> Constraint.pow2 (nexp_constraint env var_of nexp) - | Nexp_neg nexp -> Constraint.sub (Constraint.constant (big_int_of_int 0)) (nexp_constraint env var_of nexp) + | Nexp_neg nexp -> Constraint.sub (Constraint.constant (Big_int.of_int 0)) (nexp_constraint env var_of nexp) | Nexp_app (id, nexps) -> Constraint.app (Env.get_smt_op id env) (List.map (nexp_constraint env var_of) nexps) let rec nc_constraint env var_of (NC_aux (nc, l)) = @@ -1179,9 +1179,9 @@ let prove env (NC_aux (nc_aux, _) as nc) = | _, _ -> false in match nc_aux with - | NC_equal (nexp1, nexp2) when compare_const eq_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true - | NC_bounded_le (nexp1, nexp2) when compare_const le_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true - | NC_bounded_ge (nexp1, nexp2) when compare_const ge_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true + | NC_equal (nexp1, nexp2) when compare_const Big_int.equal (nexp_simp nexp1) (nexp_simp nexp2) -> true + | NC_bounded_le (nexp1, nexp2) when compare_const Big_int.less_equal (nexp_simp nexp1) (nexp_simp nexp2) -> true + | NC_bounded_ge (nexp1, nexp2) when compare_const Big_int.greater_equal (nexp_simp nexp1) (nexp_simp nexp2) -> true | NC_true -> true | _ -> prove_z3 env nc @@ -1282,7 +1282,7 @@ let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) = match nexp1, nexp2 with | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 = 0 | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2 = 0 - | Nexp_constant c1, Nexp_constant c2 -> eq_big_int c1 c2 + | Nexp_constant c1, Nexp_constant c2 -> Big_int.equal c1 c2 | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b @@ -1394,8 +1394,8 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne | Nexp_constant c2 -> begin match n1a with - | Nexp_aux (Nexp_constant c1,_) when eq_big_int (mod_big_int c2 c1) zero_big_int -> - unify_nexps l env goals n1b (mk_nexp (Nexp_constant (div_big_int c2 c1))) + | Nexp_aux (Nexp_constant c1,_) when Big_int.equal (Big_int.modulus c2 c1) Big_int.zero -> + unify_nexps l env goals n1b (mk_nexp (Nexp_constant (Big_int.div c2 c1))) | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) end | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) @@ -1777,13 +1777,13 @@ let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with | Nexp_constant c -> Some c | Nexp_times (n1, n2) -> - Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2) + Util.option_binop Big_int.add (big_int_of_nexp n1) (big_int_of_nexp n2) | Nexp_sum (n1, n2) -> - Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2) + Util.option_binop Big_int.add (big_int_of_nexp n1) (big_int_of_nexp n2) | Nexp_minus (n1, n2) -> - Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2) + Util.option_binop Big_int.add (big_int_of_nexp n1) (big_int_of_nexp n2) | Nexp_exp n -> - Util.option_map (power_int_positive_big_int 2) (big_int_of_nexp n) + Util.option_map (fun n -> Big_int.pow_int_positive 2 (Big_int.to_int n)) (big_int_of_nexp n) | _ -> None let destruct_atom (Typ_aux (typ_aux, _)) = @@ -1795,7 +1795,7 @@ let destruct_atom (Typ_aux (typ_aux, _)) = when string_of_id f = "range" -> begin match big_int_of_nexp nexp1, big_int_of_nexp nexp2 with - | Some c1, Some c2 -> if eq_big_int c1 c2 then Some (c1, nexp1) else None + | Some c1, Some c2 -> if Big_int.equal c1 c2 then Some (c1, nexp1) else None | _ -> None end | _ -> None @@ -1830,8 +1830,8 @@ let rec assert_constraint env (E_aux (exp_aux, _) as exp) = None type flow_constraint = - | Flow_lteq of big_int * nexp - | Flow_gteq of big_int * nexp + | Flow_lteq of Big_int.num * nexp + | Flow_gteq of Big_int.num * nexp let restrict_range_upper c1 nexp1 (Typ_aux (typ_aux, l) as typ) = match typ_aux with @@ -1840,7 +1840,7 @@ let restrict_range_upper c1 nexp1 (Typ_aux (typ_aux, l) as typ) = begin match big_int_of_nexp nexp2 with | Some c2 -> - let upper = if (lt_big_int c1 c2) then nexp1 else nexp2 in + let upper = if (Big_int.less c1 c2) then nexp1 else nexp2 in range_typ nexp upper | _ -> typ end @@ -1853,7 +1853,7 @@ let restrict_range_lower c1 nexp1 (Typ_aux (typ_aux, l) as typ) = begin match big_int_of_nexp nexp2 with | Some c2 -> - let lower = if (gt_big_int c1 c2) then nexp1 else nexp2 in + let lower = if (Big_int.greater c1 c2) then nexp1 else nexp2 in range_typ lower nexp | _ -> typ end @@ -1862,10 +1862,10 @@ let restrict_range_lower c1 nexp1 (Typ_aux (typ_aux, l) as typ) = let apply_flow_constraint = function | Flow_lteq (c, nexp) -> (restrict_range_upper c nexp, - restrict_range_lower (succ_big_int c) (nexp_simp (nsum nexp (nint 1)))) + restrict_range_lower (Big_int.succ c) (nexp_simp (nsum nexp (nint 1)))) | Flow_gteq (c, nexp) -> (restrict_range_lower c nexp, - restrict_range_upper (pred_big_int c) (nexp_simp (nminus nexp (nint 1)))) + restrict_range_upper (Big_int.pred c) (nexp_simp (nminus nexp (nint 1)))) let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) = match exp_aux with @@ -1874,7 +1874,7 @@ let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) = begin match destruct_atom (typ_of y) with | Some (c, nexp) -> - [(v, Flow_lteq (pred_big_int c, nexp_simp (nminus nexp (nint 1))))], [] + [(v, Flow_lteq (Big_int.pred c, nexp_simp (nminus nexp (nint 1))))], [] | _ -> [], [] end | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lteq_range_atom" -> @@ -1889,7 +1889,7 @@ let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) = begin match destruct_atom (typ_of y) with | Some (c, nexp) -> - [(v, Flow_gteq (succ_big_int c, nexp_simp (nsum nexp (nint 1))))], [] + [(v, Flow_gteq (Big_int.succ c, nexp_simp (nsum nexp (nint 1))))], [] | _ -> [], [] end | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gteq_range_atom" -> @@ -2502,7 +2502,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> dvector_typ env (nconstant n) (nint 1) (mk_typ (Typ_id (mk_id "bit"))) | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> - dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int n m) unit_big_int)) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nconstant n) (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) (mk_typ (Typ_id (mk_id "bit"))) | _, _ -> typ_error l "Not implemented this register field type yet..." in let checked_exp = crule check_exp env exp vec_typ in @@ -2730,13 +2730,13 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let vec_typ = dvector_typ env (nconstant n) (nint 1) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int n m) unit_big_int)) bit_typ in + let vec_typ = dvector_typ env (nconstant n) (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_single n, _), Ord_aux (Ord_inc, _) -> let vec_typ = dvector_typ env (nconstant n) (nint 1) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_range (n, m), _), Ord_aux (Ord_inc, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int m n) unit_big_int)) bit_typ in + let vec_typ = dvector_typ env (nconstant n) (nconstant (Big_int.add (Big_int.sub m n) (Big_int.of_int 1))) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | _, _ -> typ_error l "Invalid register field type" end @@ -3467,7 +3467,7 @@ let check_register env id base top ranges = | Nexp_aux (Nexp_constant basec, _), Nexp_aux (Nexp_constant topc, _) -> let no_typq = TypQ_aux (TypQ_tq [], Parse_ast.Unknown) (* Maybe could be TypQ_no_forall? *) in (* FIXME: wrong for default Order inc? *) - let vec_typ = dvector_typ env base (nconstant (add_big_int (sub_big_int basec topc) unit_big_int)) bit_typ in + let vec_typ = dvector_typ env base (nconstant (Big_int.add (Big_int.sub basec topc) (Big_int.of_int 1))) bit_typ in let cast_typ = mk_typ (Typ_fn (mk_id_typ id, vec_typ, no_effect)) in let cast_to_typ = mk_typ (Typ_fn (vec_typ, mk_id_typ id, no_effect)) in env diff --git a/src/type_check.mli b/src/type_check.mli index 92949c85..1931ce03 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -50,7 +50,7 @@ open Ast open Ast_util -open Big_int +module Big_int = Nat_big_num val opt_tc_debug : int ref val opt_no_effects : bool ref @@ -84,7 +84,7 @@ module Env : sig val get_register : id -> t -> typ - val get_regtyp : id -> t -> big_int * big_int * (index_range * id) list + val get_regtyp : id -> t -> Big_int.num * Big_int.num * (index_range * id) list (* Return all the identifiers in an enumeration. Throws a type error if the enumeration doesn't exist. *) diff --git a/src/value.ml b/src/value.ml index 0c67f487..4974ca83 100644 --- a/src/value.ml +++ b/src/value.ml @@ -48,14 +48,14 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Big_int +module Big_int = Nat_big_num type bit = B0 | B1 type value = | V_vector of value list | V_list of value list - | V_int of big_int + | V_int of Big_int.num | V_bool of bool | V_bit of bit | V_tuple of value list |