diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 29 | ||||
| -rw-r--r-- | src/ast_util.mli | 6 | ||||
| -rw-r--r-- | src/initial_check.ml | 9 | ||||
| -rw-r--r-- | src/lexer.mll | 5 | ||||
| -rw-r--r-- | src/lexer2.mll | 11 | ||||
| -rw-r--r-- | src/monomorphise.ml | 46 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 2 | ||||
| -rw-r--r-- | src/parse_ast.ml | 15 | ||||
| -rw-r--r-- | src/parser.mly | 17 | ||||
| -rw-r--r-- | src/parser2.mly | 13 | ||||
| -rw-r--r-- | src/pretty_print.ml | 1 | ||||
| -rw-r--r-- | src/pretty_print.mli | 2 | ||||
| -rw-r--r-- | src/pretty_print_common.ml | 7 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 32 | ||||
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 20 | ||||
| -rw-r--r-- | src/pretty_print_ocaml.ml | 705 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 3 | ||||
| -rw-r--r-- | src/pretty_print_sail2.ml | 13 | ||||
| -rw-r--r-- | src/process_file.ml | 10 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/rewriter.ml | 70 | ||||
| -rw-r--r-- | src/rewriter.mli | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 100 | ||||
| -rw-r--r-- | src/type_check.mli | 3 |
24 files changed, 204 insertions, 918 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 7d472891..d26e12ed 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -133,7 +133,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 -> Pervasives.compare c1 c2 + | Nexp_constant c1, Nexp_constant c2 -> compare_big_int 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) -> @@ -178,7 +178,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 (c1 + c2) + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (add_big_int c1 c2) | _, Nexp_neg n2 -> Nexp_minus (n1, n2) | _, _ -> Nexp_sum (n1, n2) end @@ -187,9 +187,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 1, _ -> n2_simp - | _, Nexp_constant 1 -> n1_simp - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2) + | 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_times (n1, n2) end | Nexp_minus (n1, n2) -> @@ -197,10 +197,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 (c1 - c2) + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (sub_big_int 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 c1 = -c2 -> n + when eq_big_int c1 (minus_big_int c2) -> n | _, _ -> Nexp_minus (n1, n2) end | nexp -> nexp @@ -241,6 +241,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 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) @@ -253,8 +254,8 @@ 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) let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown) -let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1)) -let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1)) +let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nint 1)) +let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nint 1)) let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2)) let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2)) let nc_true = mk_nc NC_true @@ -485,7 +486,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_int c + | Nexp_constant c -> string_of_big_int 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 ^ ")" @@ -520,7 +521,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_int ns ^ "}" + string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_big_int ns ^ "}" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" @@ -553,7 +554,7 @@ let string_of_lit (L_aux (lit, _)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num n -> string_of_int n + | L_num n -> string_of_big_int n | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_undef -> "undefined" @@ -652,8 +653,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_int n - | BF_range (n, m) -> string_of_int n ^ " .. " ^ string_of_int m + | BF_single n -> string_of_big_int n + | BF_range (n, m) -> string_of_big_int n ^ " .. " ^ string_of_big_int 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, _))) = diff --git a/src/ast_util.mli b/src/ast_util.mli index 8f8a2889..2059bb7f 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -43,6 +43,7 @@ (**************************************************************************) open Ast +open Big_int val no_annot : unit annot @@ -110,7 +111,8 @@ val mk_effect : base_effect_aux list -> effect val nexp_simp : nexp -> nexp (* Utilities for building n-expressions *) -val nconstant : int -> nexp +val nconstant : big_int -> nexp +val nint : int -> nexp val nminus : nexp -> nexp -> nexp val nsum : nexp -> nexp -> nexp val ntimes : nexp -> nexp -> nexp @@ -129,7 +131,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 -> int list -> n_constraint +val nc_set : kid -> big_int list -> n_constraint (* Negate a n_constraint. Note that there's no NC_not constructor, so this flips all the inequalites a the n_constraint leaves and uses diff --git a/src/initial_check.ml b/src/initial_check.ml index e80ff9a4..de5b625b 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -43,6 +43,7 @@ open Ast open Util open Ast_util +open Big_int let opt_undefined_gen = ref false @@ -164,12 +165,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 ((t-b)+1),l) + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (add_big_int (sub_big_int t b) unit_big_int),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 1,Parse_ast.Unknown)), + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant unit_big_int,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 @@ -185,9 +186,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 (t-1),l) + | 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) | t -> (Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (-1),Parse_ast.Unknown)), + (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (minus_big_int unit_big_int),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) diff --git a/src/lexer.mll b/src/lexer.mll index fb091f67..3b1a1583 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -42,6 +42,7 @@ { open Parser +open Big_int module M = Map.Make(String) exception LexError of string * Lexing.position @@ -321,8 +322,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(int_of_string i)) } - | "-" digit+ as i { (Num(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 1763b3a6..40e7eec6 100644 --- a/src/lexer2.mll +++ b/src/lexer2.mll @@ -42,6 +42,7 @@ { open Parser2 +open Big_int open Parse_ast module M = Map.Make(String) exception LexError of string * Lexing.position @@ -216,13 +217,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, 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, 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, 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)) } @@ -239,8 +240,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(int_of_string i)) } - | "-" digit+ as i { (Num(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 5c7cf483..79e276e1 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1,6 +1,7 @@ open Parse_ast open Ast open Ast_util +open Big_int open Type_check let size_set_limit = 8 @@ -87,21 +88,18 @@ let subst_src_typ substs t = in s_styp substs t let make_vector_lit sz i = - let f j = if (i lsr (sz-j-1)) mod 2 = 0 then '0' else '1' in + 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 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 n = 0 then acc' else aux acc' (n-1) - in if n = 0 then [] else aux [] (n-1) + 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) let make_vectors sz = - tabulate (make_vector_lit sz) (1 lsl sz) - - - + tabulate (make_vector_lit sz) (shift_left_big_int unit_big_int sz) let pat_id_is_variable env id = match Env.lookup_id id env with @@ -364,7 +362,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_int i + | (k,Some i) -> string_of_kid k ^ string_of_big_int 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) @@ -373,11 +371,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) -> (eval n1) + (eval n2) - | Nexp_minus (n1,n2) -> (eval n1) - (eval n2) - | Nexp_times (n1,n2) -> (eval n1) * (eval n2) - | Nexp_exp n -> 1 lsl (eval n) - | Nexp_neg n -> - (eval n) + | 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) | _ -> raise (Reporting_basic.err_general Unknown ("Couldn't turn nexp " ^ string_of_nexp nexp ^ " into concrete value")) @@ -575,10 +573,10 @@ let lit_match = function (* There's no undefined nexp, so replace undefined sizes with a plausible size. 32 is used as a sensible default. *) let fabricate_nexp l = function - | None -> Nexp_aux (Nexp_constant 32,Unknown) + | None -> nint 32 | Some (env,typ,_) -> match Type_check.destruct_exist env typ with - | None -> Nexp_aux (Nexp_constant 32,Unknown) + | None -> nint 32 | Some (kids,nc,typ') -> match kids,nc,Env.expand_synonyms env typ' with | ([kid],NC_aux (NC_set (kid',i::_),_), @@ -594,7 +592,7 @@ let fabricate_nexp l = function Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) when Kid.compare kid kid'' = 0 && Kid.compare kid kid''' = 0 -> - Nexp_aux (Nexp_constant 32,Unknown) + nint 32 | _ -> raise (Reporting_basic.err_general l ("Undefined value at unsupported type " ^ string_of_typ typ)) @@ -613,8 +611,8 @@ let rec drop_casts = function (* TODO: ought to be a big int of some form, but would need L_num to be one *) let int_of_lit = function - | L_hex hex -> int_of_string ("0x" ^ hex) - | L_bin bin -> 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,_)) = @@ -656,7 +654,7 @@ 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 (i lsl j),new_l)),(l,ann))) + Some (E_aux (E_lit (L_aux (L_num (shift_left_big_int i (int_of_big_int j)),new_l)),(l,ann))) | _ -> None else if is_id "ex_int" then match args with @@ -667,8 +665,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_lit lit in - let b = (v lsr i) land 1 in - let lit' = if b = 1 then L_one else L_zero 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 Some (E_aux (E_lit (L_aux (lit',new_l)),(l,ann))) | _ -> None else None @@ -1173,14 +1171,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 sz <= vector_split_limit then - let lits = make_vectors sz in + if int_of_big_int sz <= vector_split_limit then + let lits = make_vectors (int_of_big_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_int sz ^ + ("Refusing to split vector type of length " ^ string_of_big_int 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 5fb0d177..9b8ac56a 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -127,7 +127,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_int" ^^ space ^^ string (string_of_int n)) + | L_num n -> parens (string "big_int_of_string" ^^ space ^^ string ("\"" ^ Big_int.string_of_big_int 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))) diff --git a/src/parse_ast.ml b/src/parse_ast.ml index fb6c75e1..bdf56cc8 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -42,6 +42,7 @@ (* generated by Ott 0.25 from: l2_parse.ott *) +open Big_int type text = string @@ -130,7 +131,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 int (* constant *) + | ATyp_constant of big_int (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) | ATyp_minus of atyp * atyp (* subtraction *) @@ -161,7 +162,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 * (int) list + | NC_set of kid * (big_int) list | NC_or of n_constraint * n_constraint | NC_and of n_constraint * n_constraint | NC_true @@ -204,7 +205,7 @@ lit_aux = (* Literal constant *) | L_one (* $_ : _$ *) | L_true (* $_ : _$ *) | L_false (* $_ : _$ *) - | L_num of int (* natural number constant *) + | L_num of big_int (* 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 *) @@ -387,8 +388,8 @@ type_union = type index_range_aux = (* index specification, for bitfields in register types *) - BF_single of int (* single index *) - | BF_range of int * int (* index range *) + BF_single of big_int (* single index *) + | BF_range of big_int * big_int (* index range *) | BF_concat of index_range * index_range (* concatenation of index ranges *) and index_range = @@ -483,7 +484,7 @@ scattered_def = type prec = Infix | InfixL | InfixR -type fixity_token = (prec * int * string) +type fixity_token = (prec * big_int * string) type def = (* Top-level definition *) @@ -492,7 +493,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 * int * id (* fixity declaration *) + | DEF_fixity of prec * big_int * 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 edfc0783..2cfa8e80 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -44,6 +44,7 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *) +open Big_int open Parse_ast let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos()) @@ -99,16 +100,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(0), Unknown)) typ1 + make_range_sugar_bounded (ATyp_aux(ATyp_constant(zero_big_int), 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 ((t-b)+1),l) + ATyp_aux(ATyp_constant (add_big_int (sub_big_int t b) unit_big_int),l) | bot,(ATyp_aux(_,l) as top) -> - ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), + ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant unit_big_int,Unknown)), Unknown)), (ATyp_aux ((ATyp_neg bot),Unknown)))), l) let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 = @@ -122,11 +123,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 0,Unknown)) in + let zero = (ATyp_aux(ATyp_constant zero_big_int,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 (t-1),l) + | (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(_, l)) -> zero,ATyp_aux (ATyp_sum (typ1, - ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), l) + ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant unit_big_int,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 @@ -157,7 +158,7 @@ let make_vector_sugar order_set is_inc typ typ1 = /*Terminals with content*/ %token <string> Id TyVar TyId -%token <int> Num +%token <Big_int.big_int> Num %token <string> String Bin Hex Real %token <string> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde @@ -685,7 +686,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 1))) in + let step = eloc (E_lit(lloc (L_num unit_big_int))) 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 ee8cdfb8..a752e5c1 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -44,6 +44,7 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *) +open Big_int open Parse_ast let loc n m = Range (n, m) @@ -104,12 +105,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 1) s e)) s e, n2)) s e + mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant unit_big_int) 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 1) s e)) s e, n2)) s e in + 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 mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e | _ -> assert false @@ -123,12 +124,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 1) s e)) s e)) s e + mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant unit_big_int) 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 1) s e)) s e)) s e in + 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 mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e | _ -> assert false @@ -153,7 +154,7 @@ let rec desugar_rchain chain s e = /*Terminals with content*/ %token <string> Id TyVar -%token <int> Num +%token <Big_int.big_int> Num %token <string> String Bin Hex Real %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit @@ -724,7 +725,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 1) $startpos $endpos in + let step = mk_lit_exp (L_num unit_big_int) $startpos $endpos in let ord = if $6 = "to" then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6)) diff --git a/src/pretty_print.ml b/src/pretty_print.ml index e827320b..f778fe08 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -42,5 +42,4 @@ include Pretty_print_lem_ast include Pretty_print_sail -include Pretty_print_ocaml include Pretty_print_lem diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 835d4648..b878d29e 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -50,6 +50,4 @@ val pat_to_string : 'a pat -> string (* Prints on formatter the defs as Lem Ast nodes *) val pp_lem_defs : Format.formatter -> tannot defs -> unit - -val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit val pp_defs_lem : bool -> bool -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index 5cf85002..315772a4 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -41,6 +41,7 @@ (**************************************************************************) open Ast +open Big_int open PPrint let pipe = string "|" @@ -67,7 +68,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_int i) +let doc_int i = string (string_of_big_int i) let doc_op symb a b = infix 2 1 symb a b let doc_unop symb a = prefix 2 1 symb a @@ -167,7 +168,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 n = 0 then nexp m else doc_op colon (doc_int n) (nexp m))) + (squarebars (if eq_big_int n zero_big_int 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) -> @@ -211,7 +212,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 i < 0 then parens(doc_int i) else doc_int i + | Nexp_constant i -> if lt_big_int i zero_big_int 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 22f210e8..2855adbc 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -155,14 +155,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_int i) + | Nexp_constant i -> string ("ty" ^ string_of_big_int 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_int i + | Nexp_constant i -> Pretty_print_lem_ast.lemnum string_of_big_int 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 @@ -356,10 +356,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_int i in + let ipp = string_of_big_int i in utf8string ( if in_pat then "("^ipp^":nn)" - else if i < 0 then "((0"^ipp^"):ii)" + else if lt_big_int i zero_big_int 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*)*) @@ -759,7 +759,7 @@ let doc_exp_lem, doc_let_lem = let start_idx = match nexp_simp (start) with | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i) | _ -> - let nc = nc_eq start (nminus len (nconstant 1)) in + let nc = nc_eq start (nminus len (nint 1)) in if prove (env_of full_exp) nc then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v else raise (Reporting_basic.err_unreachable l @@ -787,7 +787,7 @@ let doc_exp_lem, doc_let_lem = let start_idx = match nexp_simp (start) with | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i) | _ -> - let nc = nc_eq start (nminus len (nconstant 1)) in + let nc = nc_eq start (nminus len (nint 1)) in if prove (env_of full_exp) nc then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v else raise (Reporting_basic.err_unreachable l @@ -951,7 +951,7 @@ let doc_exp_lem, doc_let_lem = | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) ->*) 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_int i + | Nexp_aux (Nexp_constant i, _) -> string_of_big_int i | _ -> if dir then "0" else string_of_int (List.length exps) in let expspp = match exps with @@ -983,7 +983,7 @@ let doc_exp_lem, doc_let_lem = let start_idx = match nexp_simp (start) with | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i) | _ -> - let nc = nc_eq start (nminus len (nconstant 1)) in + let nc = nc_eq start (nminus len (nint 1)) in if prove (env_of full_exp) nc then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v else raise (Reporting_basic.err_unreachable l @@ -1000,7 +1000,7 @@ let doc_exp_lem, doc_let_lem = let start_idx = match nexp_simp (start) with | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i) | _ -> - let nc = nc_eq start (nminus len (nconstant 1)) in + let nc = nc_eq start (nminus len (nint 1)) in if prove (env_of full_exp) nc then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v else raise (Reporting_basic.err_unreachable l @@ -1261,12 +1261,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 - | _ -> (0, true) in + | _ -> (zero_big_int, 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_int start)); semi_sp; + doc_op equals (string "field_start") (string (string_of_big_int 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 @@ -1463,7 +1463,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 i2-i1 +1 else i1-i2 + 1 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 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); @@ -1474,7 +1474,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with | BF_aux (BF_single i, _) -> (i, i) | BF_aux (BF_range (i, j), _) -> (i, j) | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in - let fsize = if dir_b then j-i+1 else i-j+1 in + let fsize = if dir_b then add_big_int (sub_big_int j i) unit_big_int else add_big_int (sub_big_int i j) unit_big_int in let ftyp = vector_typ (nconstant i) (nconstant fsize) ord bit_typ in let reftyp = mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), @@ -1491,7 +1491,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with (concat [string "let "; parens (concat [doc_id_lem id; 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_int i ^ ";"); hardline; + space; space; space; string (" field_start = " ^ string_of_big_int i ^ ";"); hardline; space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline; space; space; space; string " get_field = (fun reg -> " ^^ doc_exp_lem sequential mwords false false get ^^ string ");"; hardline; space; space; space; string " set_field = (fun reg v -> " ^^ doc_exp_lem sequential mwords false false set ^^ string ") "; ranglebar]) @@ -1794,10 +1794,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 - | _ -> (0, true) in + | _ -> (zero_big_int, true) in concat [string "let "; idd; string " = <|"; hardline; string " reg_name = \""; idd; string "\";"; hardline; - string " reg_start = "; string (string_of_int start); string ";"; hardline; + string " reg_start = "; string (string_of_big_int 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 379b3a15..a91a6f08 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -70,11 +70,11 @@ let base ppf s = fprintf ppf "%s" s let quot_string ppf s = fprintf ppf "\"%s\"" s let lemnum default n = - if 0 <= n && n <= 128 then - "int" ^ string_of_int n - else if n >= 0 then + 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 default n - else ("(zero - " ^ (default (abs n)) ^ ")") + else ("(zero - " ^ (default (abs_big_int n)) ^ ")") let pp_format_id (Id_aux(i,_)) = match i with @@ -143,7 +143,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_int i) ^ ")" + | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_big_int 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) ^ ")" @@ -207,7 +207,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_int bounds ^ + list_format "; " string_of_big_int bounds ^ "])") ^ " " ^ (pp_format_l_lem l) ^ ")" @@ -270,7 +270,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_int i) ^ ")" + | L_num(i) -> "(L_num " ^ (lemnum string_of_big_int i) ^ ")" | L_hex(n) -> "(L_hex \"" ^ n ^ "\")" | L_bin(n) -> "(L_bin \"" ^ n ^ "\")" | L_undef -> "L_undef" @@ -519,8 +519,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)" i pp_lem_l l - | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" i1 i2 pp_lem_l l + | 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_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))) = @@ -627,7 +627,7 @@ let 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_int n) pp_lem_id id + | 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 | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") let pp_lem_defs ppf (Defs(defs)) = diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml deleted file mode 100644 index 74461aab..00000000 --- a/src/pretty_print_ocaml.ml +++ /dev/null @@ -1,705 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* Kathyrn Gray *) -(* Shaked Flur *) -(* Stephen Kell *) -(* Gabriel Kerneis *) -(* Robert Norton-Wright *) -(* Christopher Pulte *) -(* Peter Sewell *) -(* *) -(* All rights reserved. *) -(* *) -(* This software was developed by the University of Cambridge Computer *) -(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) -(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in *) -(* the documentation and/or other materials provided with the *) -(* distribution. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) -(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) -(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) -(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) -(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) -(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) -(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) -(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) -(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) -(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) -(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) -(* SUCH DAMAGE. *) -(**************************************************************************) - -open Big_int -open Ast -open Ast_util -open Type_check -open PPrint -open Pretty_print_common - -(**************************************************************************** - * PPrint-based sail-to-ocaml pretty printer -****************************************************************************) - -let star_sp = star ^^ space - -let sanitize_name s = - "_" ^ s - -let doc_id_ocaml (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string (sanitize_name i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string x; empty]) - -let doc_id_ocaml_type (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string (sanitize_name i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string (String.uncapitalize x); empty]) - -let doc_id_ocaml_ctor (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string ((* TODO if n > 246 then "`" else "") ^ *) (String.capitalize i)) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string (String.capitalize x); empty]) - -let doc_typ_ocaml, doc_atomic_typ_ocaml = - (* following the structure of parser for precedence *) - let rec typ ty = fn_typ ty - and fn_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_fn(arg,ret,efct) -> - separate space [tup_typ arg; arrow; fn_typ ret] - | _ -> tup_typ ty - and tup_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_tup typs -> parens (separate_map star app_typ typs) - | _ -> app_typ ty - and app_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_app(Id_aux (Id "vector", _), [ - Typ_arg_aux(Typ_arg_nexp n, _); - Typ_arg_aux(Typ_arg_nexp m, _); - Typ_arg_aux (Typ_arg_order ord, _); - Typ_arg_aux (Typ_arg_typ typ, _)]) -> - string "value" - | Typ_app(Id_aux (Id "range", _), [ - Typ_arg_aux(Typ_arg_nexp n, _); - Typ_arg_aux(Typ_arg_nexp m, _);]) -> - (string "number") - | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> - (string "number") - | Typ_app(id,args) -> - (separate_map space doc_typ_arg_ocaml args) ^^ space ^^ (doc_id_ocaml_type id) - | _ -> atomic_typ ty - and atomic_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_id id -> doc_id_ocaml_type id - | Typ_var v -> doc_var v - | Typ_app _ | Typ_tup _ | Typ_fn _ -> - (* exhaustiveness matters here to avoid infinite loops - * if we add a new Typ constructor *) - group (parens (typ ty)) - and doc_typ_arg_ocaml (Typ_arg_aux(t,_)) = match t with - | Typ_arg_typ t -> app_typ t - | Typ_arg_nexp n -> empty - | Typ_arg_order o -> empty - in typ, atomic_typ - -let doc_lit_ocaml in_pat (L_aux(l,_)) = - utf8string (match l with - | L_unit -> "()" - | L_zero -> "Vzero" - | L_one -> "Vone" - | L_true -> "Vone" - | L_false -> "Vzero" - | L_num i -> - let s = string_of_int i in - if (i >= 0) && (i <= 257) then - "bi" ^ s - else - "(big_int_of_int (" ^ s ^ "))" - | L_hex n -> "(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*) - | L_bin n -> "(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*) - | L_undef -> "(failwith \"undef literal not supported\")" (* XXX Undef vectors get handled with to_vec_undef. We could support undef bit but would need to check type. For the moment treat as runtime error. *) - | L_string s -> "\"" ^ s ^ "\"" - | L_real s -> s) - -(* typ_doc is the doc for the type being quantified *) -let doc_typquant_ocaml (TypQ_aux(tq,_)) typ_doc = typ_doc - -let doc_typscm_ocaml (TypSchm_aux(TypSchm_ts(tq,t),_)) = - (doc_typquant_ocaml tq (doc_typ_ocaml t)) - -(*Note: vector concatenation, literal vectors, indexed vectors, and record should - be removed prior to pp. The latter two have never yet been seen -*) -let doc_pat_ocaml = - let rec pat pa = app_pat pa - and app_pat ((P_aux(p,(l,annot))) as pa) = match p with - | P_app(id, ((_ :: _) as pats)) -> - (* TODO This check fails for some reason in the MIPS execute function; - lookup_id returns Unbound, maybe because the environment is not - propagated correctly during rewriting. - I comment out the check for now. *) - (* (match annot with - | Some (env, typ, eff) -> - (match Env.lookup_id id env with - | Union _ -> *) - doc_unop (doc_id_ocaml_ctor id) (parens (separate_map comma_sp pat pats)) - (* | _ -> empty) - | _ -> empty) *) - | P_lit lit -> doc_lit_ocaml true lit - | P_wild -> underscore - | P_id id -> doc_id_ocaml id - | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_ocaml id]) - | P_typ(typ,p) -> parens (doc_op colon (pat p) (doc_typ_ocaml typ)) - | P_app(id,[]) -> - (match annot with - | Some (env, typ, eff) -> - (match Env.lookup_id id env with - | Union _ | Enum _ -> doc_id_ocaml_ctor id - | _ -> failwith "encountered unexpected P_app pattern") - | _ -> failwith "encountered unexpected P_app pattern") - | P_vector pats -> - let non_bit_print () = - parens - (separate space [string "VvectorR"; - parens (separate comma_sp [squarebars (separate_map semi pat pats); - underscore; - underscore])]) in - (match annot with - | Some (env, typ, _) -> - if is_bitvector_typ (Env.base_typ_of env typ) - then parens (separate space [string "Vvector"; - parens (separate comma_sp [squarebars (separate_map semi pat pats); - underscore; - underscore])]) - else non_bit_print() - | None -> non_bit_print()) - | P_tup pats -> parens (separate_map comma_sp pat pats) - | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in ocaml*) - | P_cons (p,p') -> doc_op (string "::") (pat p) (pat p') - | P_record _ -> raise (Reporting_basic.err_unreachable l "unhandled record pattern") - | P_vector_concat _ -> raise (Reporting_basic.err_unreachable l "unhandled vector_concat pattern") - in pat - -let id_is_local_var id env = match Env.lookup_id id env with - | Local _ | Unbound -> true - | _ -> false - -let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with - | LEXP_memory _ -> false - | LEXP_id id - | LEXP_cast (_, id) -> id_is_local_var id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps - | LEXP_vector (lexp,_) - | LEXP_vector_range (lexp,_,_) - | LEXP_field (lexp,_) -> lexp_is_local lexp env - -let is_regtyp (Typ_aux (typ,_)) env = match typ with - | Typ_app (register, _) -> string_of_id register = "register" - | Typ_id id -> Env.is_regtyp id env - | _ -> false - -let doc_exp_ocaml, doc_let_ocaml = - let rec top_exp read_registers (E_aux (e, (l,annot)) as full_exp) = - let exp = top_exp read_registers in - let (env, typ, eff) = match annot with - | Some (env, typ, eff) -> (env, typ, eff) - | None -> raise (Reporting_basic.err_unreachable l "no type annotation") in - match e with - | E_assign((LEXP_aux(le_act,tannot) as le),e) -> - if lexp_is_local le env - then - (match le_act with - | LEXP_id _ | LEXP_cast _ -> - (*Setting local variable fully *) - doc_op coloneq (doc_lexp_ocaml true le) (exp e) - | LEXP_vector _ -> - doc_op (string "<-") (doc_lexp_array_ocaml le) (exp e) - | LEXP_vector_range _ | LEXP_field _ -> - doc_lexp_rwrite le e) - else - (match le_act with - | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ | LEXP_id _ -> - (doc_lexp_rwrite le e) - | LEXP_memory _ -> (doc_lexp_fcall le e)) - | E_vector_append(l,r) -> - parens ((string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r)) - | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) - | E_if(c,t,E_aux(E_block [], _)) -> - parens (string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ - string "then" ^^ space ^^ (exp t)) - | E_if(c,t,e) -> - parens ( - string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ - string "then" ^^ space ^^ group (exp t) ^/^ - string "else" ^^ space ^^ group (exp e)) - | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> - let var= doc_id_ocaml id in - let (compare,next) = if order = Ord_inc then string "le_big_int",string "add_big_int" else string "ge_big_int",string "sub_big_int" in - let by = exp exp3 in - let stop = exp exp2 in - (*takes over two names but doesn't require building a closure*) - parens - (separate space [(string "let (__stop,__by) = ") ^^ (parens (doc_op comma stop by)); - string "in" ^/^ empty; - string "let rec foreach"; - var; - equals; - string "if"; - parens (compare ^^ space ^^ var ^^ space ^^ (string "__stop") ); - string "then"; - parens (exp exp4 ^^ space ^^ semi ^^ (string "foreach") ^^ - parens (next ^^ space ^^ var ^^ space ^^ (string "__by"))); - string "in"; - string "foreach"; - exp exp1]) - (*Requires fewer introduced names but introduces a closure*) - (*let forL = if order = Ord_inc then string "foreach_inc" else string "foreach_dec" in - forL ^^ space ^^ (group (exp exp1)) ^^ (group (exp exp2)) ^^ (group (exp full_exp3)) ^/^ - group ((string "fun") ^^ space ^^ (doc_id id) ^^ space ^^ arrow ^/^ (exp exp4)) - - (* this way requires the following OCaml declarations first - - let rec foreach_inc i stop by body = - if i <= stop then (body i; foreach_inc (i + by) stop by body) else () - - let rec foreach_dec i stop by body = - if i >= stop then (body i; foreach_dec (i - by) stop by body) else () - - *)*) - | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) - | E_app(f,args) -> - let call,ctor = match Env.lookup_id f env with - | Union _ -> doc_id_ocaml_ctor f,true - | _ -> doc_id_ocaml f,false in - let base_print () = parens (doc_unop call (parens (separate_map comma exp args))) in - if not(ctor) - then base_print () - else (match args with - | [] -> call - | [arg] -> (match arg with - | E_aux(E_lit (L_aux(L_unit,_)),_) -> call - | _ -> base_print()) - | args -> base_print()) - | E_vector_access(v,e) -> - let call = - if is_bit_typ (Env.base_typ_of env typ) - then (string "bit_vector_access") - else (string "vector_access") in - parens (call ^^ space ^^ exp v ^^ space ^^ exp e) - | E_vector_subrange(v,e1,e2) -> - parens ((string "vector_subrange") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | E_field((E_aux(_,(fl,fannot)) as fexp),id) -> - let ftyp = typ_of_annot (fl,fannot) in - if (is_regtyp ftyp env) then - let field_f = - if (is_bit_typ (Env.base_typ_of env ftyp)) - then string "get_register_field_bit" - else string "get_register_field_vec" in - parens (field_f ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id id)) - else exp fexp ^^ dot ^^ doc_id_ocaml id - | E_block [] -> string "()" - | E_block exps | E_nondet exps -> - let exps_doc = separate_map (semi ^^ hardline) exp exps in - surround 2 1 (string "begin") exps_doc (string "end") - | E_id id -> - (match Env.lookup_id id env with - | Local (Mutable, _) -> - string "!" ^^ doc_id_ocaml id - | Union _ | Enum _ -> doc_id_ocaml_ctor id - | _ -> - if (is_regtyp typ env) then - if read_registers - then string "(read_register " ^^ doc_id_ocaml id ^^ string ")" - else doc_id_ocaml id - else doc_id_ocaml id) - (*match annot with - | Base((_,t),Alias alias_info,_,_,_,_) -> - (match alias_info with - | Alias_field(reg,field) -> - let field_f = match t.t with - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "get_register_field_bit" - | _ -> string "get_register_field_vec" in - parens (separate space [field_f; string (sanitize_name reg); string_lit (string field)]) - | Alias_extract(reg,start,stop) -> - if start = stop - then parens (separate space [string "bit_vector_access";string (sanitize_name reg);doc_int start]) - else parens - (separate space [string "vector_subrange"; string (sanitize_name reg); doc_int start; doc_int stop]) - | Alias_pair(reg1,reg2) -> - parens (separate space [string "vector_concat"; - string (sanitize_name reg1); - string (sanitize_name reg2)])) *) - | E_lit lit -> doc_lit_ocaml false lit - | E_cast(typ,e) -> - (* (match annot with - | Base(_,External _,_,_,_,_) -> - if read_registers - then parens (string "read_register" ^^ space ^^ exp e) - else exp e - | _ -> *) - let (Typ_aux (t,_)) = typ in - (match t with - | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) -> - parens ((concat [string "set_start";space;string (string_of_int i)]) ^//^ - exp e) - | Typ_var (Kid_aux (Var "length",_)) -> - parens ((string "set_start_to_length") ^//^ exp e) - | _ -> - parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))) - | E_tuple exps -> - parens (separate_map comma exp exps) - | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> - braces (separate_map semi_sp doc_fexp fexps) - | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps)) - | E_vector exps -> - let (start, _, order, _) = vector_typ_args_of (Env.base_typ_of env typ) in - (*match annot with - | Base((_,t),_,_,_,_,_) -> - match t.t with - | Tapp("vector", [TA_nexp start; _; TA_ord order; _]) - | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; _; TA_ord order; _])}) ->*) - let call = if is_bitvector_typ typ then (string "Vvector") else (string "VvectorR") in - let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in - let start = match start with - | Nexp_aux (Nexp_constant i, _) -> string_of_int i - | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) -> - string_of_int (Util.power 2 i) - | _ -> if dir then "0" else string_of_int (List.length exps) in - parens (separate space [call; parens (separate comma_sp [squarebars (separate_map semi exp exps); - string start; - string dir_out])]) - | E_vector_update(v,e1,e2) -> - (*Has never happened to date*) - brackets (doc_op (string "with") (exp v) (doc_op equals (exp e1) (exp e2))) - | E_vector_update_subrange(v,e1,e2,e3) -> - (*Has never happened to date*) - brackets ( - doc_op (string "with") (exp v) - (doc_op equals (exp e1 ^^ colon ^^ exp e2) (exp e3))) - | E_list exps -> - brackets (separate_map semi exp exps) - | E_case(e,pexps) -> - let opening = separate space [string "("; string "match"; top_exp false e; string "with"] in - let cases = separate_map (break 1) doc_case pexps in - surround 2 1 opening cases rparen - | E_exit e -> - separate space [string "exit"; exp e;] - | E_return e -> - separate space [string "begin ret := Some" ; exp e ; string "; raise Sail_return; end"] - | E_app_infix (e1,id,e2) -> - let call = - (* match annot with - | Base((_,t),External(Some name),_,_,_,_) -> string name - | _ -> *) doc_id_ocaml id in - parens (separate space [call; parens (separate_map comma exp [e1;e2])]) - | E_internal_let(lexp, eq_exp, in_exp) -> - separate space [string "let"; - doc_lexp_ocaml true lexp; (*Rewriter/typecheck should ensure this is only cast or id*) - equals; - string "ref"; - exp eq_exp; - string "in"; - exp in_exp] - - | E_internal_plet (pat,e1,e2) -> - (separate space [(exp e1); string ">>= fun"; doc_pat_ocaml pat;arrow]) ^/^ - exp e2 - - | E_internal_return (e1) -> - separate space [string "return"; exp e1;] - | E_assert (e1, e2) -> - (string "assert") ^^ parens ((string "to_bool") ^^ space ^^ exp e1) (* XXX drops e2 *) - | E_sizeof _ -> raise (Reporting_basic.err_unreachable l - "E_sizeof should have been rewritten before pretty-printing") - | E_constraint _ -> empty - | E_sizeof_internal _ | E_internal_exp_user (_, _) | E_internal_cast (_, _) - | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l - "internal expression should have been rewritten before pretty-printing") - | E_comment _ | E_comment_struc _ -> empty (* TODO Should we output comments? *) - and let_exp (LB_aux(lb,_)) = match lb with - | LB_val(pat,e) -> - prefix 2 1 - (separate space [string "let"; doc_pat_ocaml pat; equals]) - (top_exp false e) - - and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_ocaml id) (top_exp false e) - - and doc_case = function - | (Pat_aux(Pat_exp(pat,e),_)) -> - doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (group (top_exp false e)) - | (Pat_aux(Pat_when(pat,guard,e),_)) -> - doc_op arrow - (separate space [pipe; - doc_op (string "when") (doc_pat_ocaml pat) (top_exp false guard)]) - (group (top_exp false e)) - - and doc_lexp_ocaml top_call ((LEXP_aux(lexp,(l,annot))) as le) = - let exp = top_exp false in - match lexp with - | LEXP_vector(v,e) -> doc_lexp_array_ocaml le - | LEXP_vector_range(v,e1,e2) -> - parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_ocaml false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | LEXP_field(v,id) -> (doc_lexp_ocaml false v) ^^ dot ^^ doc_id_ocaml id - | LEXP_id id | LEXP_cast(_,id) -> - let name = doc_id_ocaml id in - match annot,top_call with - | Some (env, _, _), false -> - (match Env.lookup_id id env with - | Local (Mutable, _) -> string "!" ^^ name - | _ -> name) - | _ -> name - - and doc_lexp_array_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with - | LEXP_vector(v,e) -> - (match annot with - | Some (env, t, _) -> - if (is_bit_typ (Env.base_typ_of env t)) - then parens ((string "get_barray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e)) - else parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e)) - | _ -> - parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e))) - | _ -> empty - - and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = - let exp = top_exp false in - let (is_bit,is_bitv) = match annot with - | Some (env, typ, _) -> - let typ = Env.base_typ_of env typ in - (is_bit_typ typ, is_bitvector_typ typ) - | _ -> (false, false) in - match lexp with - | LEXP_vector(v,e) -> - if is_bit then (* XXX check whether register or not?? *) - parens ((string "set_register_bit" ^^ space ^^ doc_lexp_ocaml false v ^^ space ^^ exp e ^^ space ^^ exp e_new_v)) - else (* XXX Check whether vector of reg? XXX Does not work for decreasing vector. *) - parens ((string "set_register") ^^ space ^^ - ((group (parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) ^^ space ^^ (exp e_new_v))) - | LEXP_vector_range(v,e1,e2) -> - parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ - doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) - | LEXP_field(v,id) -> - parens ((string (if is_bit then "set_register_field_bit" else "set_register_field_v")) ^^ space ^^ - doc_lexp_ocaml false v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v) - | LEXP_id id | LEXP_cast (_,id) -> - (* (match annot with - | Base(_,Alias alias_info,_,_,_,_) -> - (match alias_info with - | Alias_field(reg,field) -> - parens ((if is_bit then string "set_register_field_bit" else string "set_register_field_v") ^^ space ^^ - string (sanitize_name reg) ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v) - | Alias_extract(reg,start,stop) -> - if start = stop - then - doc_op (string "<-") - (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ string reg)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (doc_int start))) - (exp e_new_v) - else - parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ - string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v) - | Alias_pair(reg1,reg2) -> - parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v)) - | _ -> *) - parens (separate space [string "set_register"; doc_id_ocaml id; exp e_new_v]) - - and doc_lexp_fcall ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = match lexp with - | LEXP_memory(id,args) -> doc_id_ocaml id ^^ parens (separate_map comma (top_exp false) (args@[e_new_v])) - - (* expose doc_exp and doc_let *) - in top_exp false, let_exp - -(*TODO Upcase and downcase type and constructors as needed*) -let doc_type_union_ocaml n (Tu_aux(typ_u,_)) = match typ_u with - | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_ocaml_ctor id; string "of"; doc_typ_ocaml typ;] - | Tu_id id -> separate space [pipe; doc_id_ocaml_ctor id] - -let rec doc_range_ocaml (BF_aux(r,_)) = match r with - | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i)) - | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2)) - | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) - -let doc_typdef_ocaml (TD_aux(td,_)) = match td with - | TD_abbrev(id,nm,typschm) -> - doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typscm_ocaml typschm) - | TD_record(id,nm,typq,fs,_) -> - let f_pp (typ,id) = concat [doc_id_ocaml_type id; space; colon; doc_typ_ocaml typ; semi] in - let fs_doc = group (separate_map (break 1) f_pp fs) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typquant_ocaml typq (braces fs_doc)) - | TD_variant(id,nm,typq,ar,_) -> - let n = List.length ar in - let ar_doc = group (separate_map (break 1) (doc_type_union_ocaml n) ar) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) - (if n > 246 - then brackets (space ^^(doc_typquant_ocaml typq ar_doc)) - else (doc_typquant_ocaml typq ar_doc)) - | TD_enum(id,nm,enums,_) -> - let n = List.length enums in - let enums_doc = group (separate_map (break 1 ^^ pipe) (doc_id_ocaml_ctor) enums) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) - (enums_doc) - | TD_register(id,n1,n2,rs) -> - let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;]) in - let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in - match n1,n2 with - | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> - let dir = i1 < i2 in - let size = if dir then i2-i1 +1 else i1-i2+1 in - doc_op equals - ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val")) - (separate space [string "Vregister"; - (parens (separate comma_sp - [parens (separate space - [string "match init_val with"; - pipe; - string "None"; - arrow; - string "ref"; - string "(Array.make"; - doc_int size; - string "Vzero)"; - pipe; - string "Some init_val"; - arrow; - string "ref init_val";]); - doc_nexp n1; - string (if dir then "true" else "false"); - string_lit (doc_id id); - brackets doc_rids]))]) - -let doc_kdef_ocaml (KD_aux(kd,_)) = match kd with - | KD_nabbrev (k, id, name_scm, nexp) -> - separate space [string "let" ; - doc_id_ocaml id; - equals; - doc_nexp nexp] - -let doc_rec_ocaml (Rec_aux(r,_)) = match r with - | Rec_nonrec -> empty - | Rec_rec -> string "rec" ^^ space - -let doc_tannot_opt_ocaml (Typ_annot_opt_aux(t,_)) = match t with - | Typ_annot_opt_some(tq,typ) -> doc_typquant_ocaml tq (doc_typ_ocaml typ) - -let doc_funcl_exp_ocaml (E_aux (e, (l, annot)) as ea) = match annot with - | Some (_, t, efctsum) -> - (* | Base((_,t),tag,nes,efct,efctsum,_) -> *) - if has_effect efctsum BE_lret then - separate hardline [string "let ret = ref None in"; - string "try"; - (doc_exp_ocaml ea); - string "with Sail_return -> match(!ret) with"; - string "| Some(x) -> x"; - string "| None -> failwith \"ret unset\"" - ] - else - doc_exp_ocaml ea - | _ -> doc_exp_ocaml ea - -let doc_funcl_ocaml (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - group (doc_op arrow (doc_pat_ocaml pat) (doc_funcl_exp_ocaml exp)) - -let get_id = function - | [] -> failwith "FD_function with empty list" - | (FCL_aux (FCL_Funcl (id,_,_),_))::_ -> id - -let doc_fundef_ocaml (FD_aux(FD_function(r, typa, efa, fcls),_)) = - match fcls with - | [] -> failwith "FD_function with empty function list" - | [FCL_aux (FCL_Funcl(id,pat,exp),_)] -> - (separate space [(string "let"); (doc_rec_ocaml r); (doc_id_ocaml id); (doc_pat_ocaml pat); equals]) ^^ hardline ^^ (doc_funcl_exp_ocaml exp) - | _ -> - let id = get_id fcls in - let sep = hardline ^^ pipe ^^ space in - let clauses = separate_map sep doc_funcl_ocaml fcls in - separate space [string "let"; - doc_rec_ocaml r; - doc_id_ocaml id; - equals; - (string "function"); - (hardline^^pipe); - clauses] - -let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = - match reg with - | DEC_reg(typ,id) -> - if is_vector_typ typ then - let (start, size, order, itemt) = vector_typ_args_of typ in - if is_bit_typ itemt && is_nexp_constant start && is_nexp_constant size then - let o = if is_order_inc order then string "true" else string "false" in - separate space [string "let"; - doc_id_ocaml id; - equals; - string "Vregister"; - parens (separate comma [separate space [string "ref"; - parens (separate space - [string "Array.make"; - doc_nexp size; - string "Vzero";])]; - doc_nexp start; - o; - string_lit (doc_id id); - brackets empty])] - else raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ)) - else - (match typ with - | Typ_aux (Typ_id idt, _) -> - (* | Tapp("register", [TA_typ {t=Tid idt}]) | - Tabbrev( {t= Tid idt}, _) -> *) - separate space [string "let"; - doc_id_ocaml id; - equals; - doc_id_ocaml idt; - string "None"] - |_-> raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ))) - (* | _ -> failwith "annot was not Base") *) - | DEC_alias(id,alspec) -> empty (* - doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) *) - | DEC_typ_alias(typ,id,alspec) -> empty (* - doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec) *) - -let doc_def_ocaml def = group (match def with - | DEF_default df -> empty - | DEF_spec v_spec -> empty (*unless we want to have a separate pass to create mli files*) - | DEF_type t_def -> doc_typdef_ocaml t_def - | DEF_fundef f_def -> doc_fundef_ocaml f_def - | DEF_val lbind -> doc_let_ocaml lbind - | DEF_reg_dec dec -> doc_dec_ocaml dec - | DEF_scattered sdef -> empty (*shoulnd't still be here*) - | DEF_kind k_def -> doc_kdef_ocaml k_def - | DEF_overload _ -> empty - | DEF_comm _ -> failwith "unhandled DEF_comm" - ) ^^ hardline - -let doc_defs_ocaml (Defs(defs)) = - separate_map hardline doc_def_ocaml defs -let pp_defs_ocaml f d top_line opens = - print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ - (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ - (doc_defs_ocaml d)) diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index c53d30b4..e585a8f1 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -42,6 +42,7 @@ open Ast open Ast_util +open Big_int open PPrint open Pretty_print_common @@ -88,7 +89,7 @@ let doc_lit (L_aux(l,_)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num i -> string_of_int i + | L_num i -> string_of_big_int i | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_real r -> r diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 56560de2..e354fe58 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -1,6 +1,7 @@ open Ast open Ast_util +open Big_int open PPrint let doc_op symb a b = infix 2 1 symb a b @@ -12,7 +13,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_int n) +let doc_int n = string (string_of_big_int n) let doc_ord (Ord_aux(o,_)) = match o with | Ord_var v -> doc_kid v @@ -22,7 +23,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_int c) + | Nexp_constant c -> string (string_of_big_int c) | Nexp_id id -> doc_id id | Nexp_var kid -> doc_kid kid | _ -> parens (nexp0 nexp) @@ -30,8 +31,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 c < 0 -> - separate space [nexp0 n1; string "-"; doc_int (abs c)] + | 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, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2] | _ -> nexp1 nexp and nexp1 (Nexp_aux (n_aux, _) as nexp) = @@ -143,7 +144,7 @@ let doc_lit (L_aux(l,_)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num i -> string_of_int i + | L_num i -> string_of_big_int i | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_real r -> r @@ -216,7 +217,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_try (exp, pexps) -> assert false | E_return exp -> string "return" ^^ parens (doc_exp exp) | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> - separate space [doc_int 2; string "^"; doc_atomic_exp exp] + separate space [string "2"; string "^"; doc_atomic_exp exp] | _ -> doc_atomic_exp exp and doc_atomic_exp (E_aux (e_aux, _) as exp) = match e_aux with diff --git a/src/process_file.ml b/src/process_file.ml index 4c70400c..344e5951 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -47,7 +47,6 @@ let opt_lem_mwords = ref false type out_type = | Lem_ast_out | Lem_out of string option - | Ocaml_out of string option let get_lexbuf f = let in_chan = open_in f in @@ -198,15 +197,6 @@ let output1 libpath out_arg filename defs = output_lem f' [] defs | Lem_out (Some lib) -> output_lem f' [lib] defs - | Ocaml_out None -> - let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in - begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"]; - close_output_with_check ext_o - end - | Ocaml_out (Some lib) -> - let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in - Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z"; "Sail_values"; lib]; - close_output_with_check ext_o let output libpath out_arg files = List.iter diff --git a/src/process_file.mli b/src/process_file.mli index afde469e..b575bd14 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -67,7 +67,6 @@ val opt_auto_mono : bool ref type out_type = | Lem_ast_out | Lem_out of string option (* If present, the string is a file to open in the lem backend*) - | Ocaml_out of string option (* If present, the string is a file to open in the ocaml backend*) val output : string -> (* The path to the library *) diff --git a/src/rewriter.ml b/src/rewriter.ml index 025bade2..62e4f7ef 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -539,21 +539,13 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) = | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced") | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced") | _ -> rewrap exp - + let rewrite_let rewriters (LB_aux(letbind,(l,annot))) = - (*let local_map = get_map_tannot annot in - let map = - match map,local_map with - | None,None -> None - | None,Some m -> Some(m, Envmap.empty) - | Some(m,s), None -> Some(m,s) - | Some(m,s), Some m' -> match merge_option_maps (Some m) local_map with - | None -> Some(m,s) (*Shouldn't happen*) - | Some new_m -> Some(new_m,s) in*) match letbind with | LB_val ( pat, exp) -> LB_aux(LB_val (rewriters.rewrite_pat rewriters pat, - rewriters.rewrite_exp rewriters exp),(l,annot)) + rewriters.rewrite_exp rewriters exp), + (l, annot)) let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = let rewrap le = LEXP_aux(le,(l,annot)) in @@ -658,7 +650,6 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat | P_list ps -> alg.p_list (List.map (fold_pat alg) ps) | P_cons (ph,pt) -> alg.p_cons (fold_pat alg ph, fold_pat alg pt) - and fold_pat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat -> 'pat = function | P_aux (pat,annot) -> alg.p_aux (fold_pat_aux alg pat,annot) @@ -670,7 +661,7 @@ and fold_fpat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat -> 'f | FP_aux (fpat,annot) -> alg.fP_aux (fold_fpat_aux alg fpat,annot) (* identity fold from term alg to term alg *) -let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = +let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = { p_lit = (fun lit -> P_lit lit) ; p_wild = P_wild ; p_as = (fun (pat,id) -> P_as (pat,id)) @@ -688,7 +679,7 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot)) ; fP_Fpat = (fun (id,pat) -> FP_Fpat (id,pat)) } - + type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = @@ -749,11 +740,11 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; pat_exp : 'pat * 'exp -> 'pexp_aux ; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux ; pat_aux : 'pexp_aux * 'a annot -> 'pexp - ; lB_val : 'pat * 'exp -> 'letbind_aux + ; lB_val : 'pat * 'exp -> 'letbind_aux ; lB_aux : 'letbind_aux * 'a annot -> 'letbind ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } - + let rec fold_exp_aux alg = function | E_block es -> alg.e_block (List.map (fold_exp alg) es) | E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es) @@ -1484,7 +1475,9 @@ let remove_vector_concat_pat pat = let rtyp = Env.base_typ_of (env_of_annot rannot') (typ_of_annot rannot') in 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 start + length - 1 else start - length + 1) + (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) | _ -> raise (Reporting_basic.err_unreachable (fst rannot') ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in @@ -1493,14 +1486,15 @@ let remove_vector_concat_pat pat = let (_,length,ord,_) = vector_typ_args_of ctyp in let (pos',index_j) = match length with | Nexp_aux (Nexp_constant i,_) -> - if is_order_inc ord then (pos+i, pos+i-1) - else (pos-i, pos-i+1) + 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) | Nexp_aux (_,l) -> - if is_last then (pos,last_idx) - else - raise - (Reporting_basic.err_unreachable - l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in + if is_last then (pos,last_idx) + else + raise + (Reporting_basic.err_unreachable + l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in (match p with (* if we see a named vector pattern, remove the name and remember to declare it later *) @@ -1594,8 +1588,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 a > b then [] else a :: aux (a+1) b in - if a > b then List.rev (aux b a) else aux a b in + 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 remove_vector_concats = let p_vector_concat ps = @@ -1609,9 +1603,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 0 (length - 1))) + acc @ (List.map wild (range zero_big_int (sub_big_int length unit_big_int))) | _, _ -> - (*if is_last then*) acc @ [wild 0] + (*if is_last then*) acc @ [wild zero_big_int] else raise (Reporting_basic.err_unreachable l ("remove_vector_concats: Non-vector in vector-concat pattern " ^ @@ -1936,15 +1930,15 @@ let remove_bitvector_pat pat = let test_subvec_exp rootid l typ i j lits = let (start, length, ord, _) = vector_typ_args_of typ in - let length' = nconstant (List.length lits) in + let length' = nint (List.length lits) in let start' = - if is_order_inc ord then nconstant 0 - else nminus length' (nconstant 1) in + if is_order_inc ord then nint 0 + else nminus length' (nint 1) in let typ' = vector_typ start' length' ord bit_typ in let subvec_exp = match start, length with | Nexp_aux (Nexp_constant s, _), Nexp_aux (Nexp_constant l, _) - when s = i && l = List.length lits -> + when eq_big_int s i && eq_big_int l (big_int_of_int (List.length lits)) -> E_id rootid | _ -> (*if vec_start t = i && vec_length t = List.length lits @@ -1988,7 +1982,7 @@ let remove_bitvector_pat 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 idx + 1 else idx - 1 in + let idx' = if is_order_inc ord then add_big_int idx unit_big_int else add_big_int idx unit_big_int in (match ps with | pat :: ps' -> (match pat with @@ -2717,15 +2711,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 - | _ -> 1 - else 1 in + | _ -> unit_big_int + else unit_big_int in let next i step = if is_order_inc ord - then (i + step - 1, i + step) - else (i - step + 1, i - step) in + 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 let i = match nexp_simp start with | (Nexp_aux (Nexp_constant i, _)) -> i - | _ -> if is_order_inc ord then 0 else List.length lexps - 1 in + | _ -> if is_order_inc ord then zero_big_int 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/rewriter.mli b/src/rewriter.mli index 412852d4..c107be25 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -53,7 +53,7 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; rewrite_def : 'a rewriters -> 'a def -> 'a def; rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; } - + val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp val rewrite_defs : tannot defs -> tannot defs val rewrite_undefined : bool -> tannot defs -> tannot defs diff --git a/src/type_check.ml b/src/type_check.ml index aff5567f..3a8f2e59 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -304,9 +304,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 -> int -> int -> (index_range * id) list -> t -> t + val add_regtyp : id -> big_int -> big_int -> (index_range * id) list -> t -> t val is_regtyp : id -> t -> bool - val get_regtyp : id -> t -> int * int * (index_range * id) list + val get_regtyp : id -> t -> big_int * big_int * (index_range * id) list val is_mutable : id -> t -> bool val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t @@ -361,7 +361,7 @@ end = struct locals : (mut * typ) Bindings.t; union_ids : (typquant * typ) Bindings.t; registers : typ Bindings.t; - regtyps : (int * int * (index_range * id) list) Bindings.t; + regtyps : (big_int * big_int * (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; @@ -764,11 +764,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_int [f; n; t]) + else typ_error l ("Badly ordered index range: " ^ string_of_list ", " string_of_big_int [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_int [f; n1; n2; t]) + else typ_error l ("Badly ordered index range: " ^ string_of_list ", " string_of_big_int [f; n1; n2; t]) | BF_concat _ -> typ_error l "Index range concatenation currently unsupported" let rec check_index_ranges ids cmp base top = function @@ -798,9 +798,9 @@ end = struct else begin typ_print ("Adding register type " ^ string_of_id id); - if base > top - then check_index_ranges IdSet.empty (fun x y -> x > y) (base + 1) (top - 1) ranges - else check_index_ranges IdSet.empty (fun x y -> x < y) (base - 1) (top + 1) ranges; + 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; { env with regtyps = Bindings.add id (base, top, ranges) env.regtyps } end @@ -921,7 +921,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 = abs(top - base) + 1 in + let len = sub_big_int (abs_big_int (sub_big_int top base)) unit_big_int 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 @@ -960,9 +960,9 @@ let dvector_typ env n m typ = vector_typ n m (Env.get_default_order env) typ let lvector_typ env l typ = match Env.get_default_order env with | Ord_aux (Ord_inc, _) as ord -> - vector_typ (nconstant 0) l ord typ + vector_typ (nint 0) l ord typ | Ord_aux (Ord_dec, _) as ord -> - vector_typ (nminus l (nconstant 1)) l ord typ + vector_typ (nminus l (nint 1)) l ord typ let ex_counter = ref 0 @@ -1066,7 +1066,7 @@ let rec normalize_typ env (Typ_aux (typ, l)) = match typ with | Typ_id (Id_aux (Id "int", _)) -> Tnf_index_sort IS_int | Typ_id (Id_aux (Id "nat", _)) -> - let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(nconstant 0, nvar kid)])) + let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(nint 0, nvar kid)])) | Typ_id v -> begin try normalize_typ env (Env.get_typ_synonym v env env []) with @@ -1121,7 +1121,7 @@ let rec nexp_constraint env var_of (Nexp_aux (nexp, l)) = match nexp with | Nexp_id v -> nexp_constraint env var_of (Env.get_num_def v env) | Nexp_var kid -> Constraint.variable (var_of kid) - | Nexp_constant c -> Constraint.constant (big_int_of_int c) + | Nexp_constant c -> Constraint.constant c | Nexp_times (nexp1, nexp2) -> Constraint.mult (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2) | 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) @@ -1138,8 +1138,8 @@ let rec nc_constraint env var_of (NC_aux (nc, l)) = | NC_set (_, []) -> Constraint.literal false | NC_set (kid, (int :: ints)) -> List.fold_left Constraint.disj - (Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant (big_int_of_int int))) - (List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant (big_int_of_int i))) ints) + (Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant int)) + (List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant i)) ints) | NC_or (nc1, nc2) -> Constraint.disj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2) | NC_and (nc1, nc2) -> Constraint.conj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2) | NC_false -> Constraint.literal false @@ -1181,12 +1181,12 @@ let prove env (NC_aux (nc_aux, _) as nc) = | _, _ -> false in match nc_aux with - | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 = c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true - | NC_bounded_le (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <= c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true - | NC_bounded_ge (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 >= c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true - | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <> c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false - | NC_bounded_le (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 > c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false - | NC_bounded_ge (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 < c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false + | 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 (fun c1 c2 -> not (eq_big_int c1 c2)) (nexp_simp nexp1) (nexp_simp nexp2) -> false + | NC_bounded_le (nexp1, nexp2) when compare_const gt_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> false + | NC_bounded_ge (nexp1, nexp2) when compare_const lt_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> false | NC_true -> true | NC_false -> false | _ -> prove_z3 env nc @@ -1288,7 +1288,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 -> c1 = c2 + | Nexp_constant c1, Nexp_constant c2 -> eq_big_int 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 @@ -1400,8 +1400,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 c2 mod c1 = 0 -> - unify_nexps l env goals n1b (mk_nexp (Nexp_constant (c2 / c1))) + | 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))) | _ -> 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) @@ -1683,22 +1683,22 @@ let infer_lit env (L_aux (lit_aux, l) as lit) = begin match Env.get_default_order env with | Ord_aux (Ord_inc, _) -> - dvector_typ env (nconstant 0) (nconstant (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nint 0) (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) | Ord_aux (Ord_dec, _) -> dvector_typ env - (nconstant (String.length str - 1)) - (nconstant (String.length str)) + (nint (String.length str - 1)) + (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) end | L_hex str -> begin match Env.get_default_order env with | Ord_aux (Ord_inc, _) -> - dvector_typ env (nconstant 0) (nconstant (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nint 0) (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) | Ord_aux (Ord_dec, _) -> dvector_typ env - (nconstant (String.length str * 4 - 1)) - (nconstant (String.length str * 4)) + (nint (String.length str * 4 - 1)) + (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) end | L_undef -> typ_error l "Cannot infer the type of undefined" @@ -1781,7 +1781,7 @@ let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) (* Flow typing *) let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with - | Nexp_constant c -> Some (big_int_of_int c) + | 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) | Nexp_sum (n1, n2) -> @@ -1870,10 +1870,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 (nconstant 1)))) + restrict_range_lower (succ_big_int 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 (nconstant 1)))) + restrict_range_upper (pred_big_int c) (nexp_simp (nminus nexp (nint 1)))) let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) = match exp_aux with @@ -1882,7 +1882,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 (nconstant 1))))], [] + [(v, Flow_lteq (pred_big_int 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" -> @@ -1897,7 +1897,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 (nconstant 1))))], [] + [(v, Flow_gteq (succ_big_int 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" -> @@ -2164,7 +2164,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | E_vector vec, _ -> let (start, len, ord, vtyp) = destruct_vec_typ l env typ in let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in - if prove env (nc_eq (nconstant (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ + if prove env (nc_eq (nint (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ else typ_error l "List length didn't match" (* FIXME: improve error message *) | E_lit (L_aux (L_undef, _) as lit), _ -> if is_typ_monomorphic typ || Env.polymorphic_undefineds env @@ -2292,7 +2292,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) annot_pat (P_var (typed_pat, kid)) typ, env | None, Typ_aux (Typ_id id, _) when Id.compare id (mk_id "nat") == 0 -> let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_gt (nvar kid) (nconstant 0)) env in + let env = Env.add_constraint (nc_gt (nvar kid) (nint 0)) env in let typed_pat, env = bind_pat env pat (atom_typ (nvar kid)) in annot_pat (P_var (typed_pat, kid)) typ, env | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) @@ -2412,7 +2412,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = in let ((typed_pat :: typed_pats) as pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in - let len = nexp_simp (nconstant (List.length pats)) in + let len = nexp_simp (nint (List.length pats)) in let etyp = pat_typ_of typed_pat in List.map (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats; annot_pat (P_vector pats) (lvector_typ env len etyp), env @@ -2482,9 +2482,9 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as in let vec_typ = match range, Env.get_default_order env with | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> - dvector_typ env (nconstant n) (nconstant 1) (mk_typ (Typ_id (mk_id "bit"))) + 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 (n - m + 1)) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int n m) unit_big_int)) (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 @@ -2605,7 +2605,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = tlexp :: tlexps, env, nsum llen llen' | _ -> typ_error l "bit vector assignment must only contain identifiers" in - let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nconstant 0) in + let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nint 0) in if prove env (nc_eq vec_len lexp_len) then annot_lexp (LEXP_tup tlexps) typ, env else typ_error l "Vector and tuple length must be the same in assignment" @@ -2709,16 +2709,16 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = begin match range, Env.get_default_order env with | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in + 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 (n - m + 1)) bit_typ in + let vec_typ = dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int n m) unit_big_int)) 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) (nconstant 1) bit_typ in + 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 (m - n + 1)) bit_typ in + let vec_typ = dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int m n) unit_big_int)) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | _, _ -> typ_error l "Invalid register field type" end @@ -2824,14 +2824,14 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let vec_typ = match Env.get_default_order env with | Ord_aux (Ord_inc, _) -> mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp (nconstant 0)); - mk_typ_arg (Typ_arg_nexp (nconstant (List.length vec))); + [mk_typ_arg (Typ_arg_nexp (nint 0)); + mk_typ_arg (Typ_arg_nexp (nint (List.length vec))); mk_typ_arg (Typ_arg_order (Env.get_default_order env)); mk_typ_arg (Typ_arg_typ (typ_of inferred_item))])) | Ord_aux (Ord_dec, _) -> mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp (nconstant (List.length vec - 1))); - mk_typ_arg (Typ_arg_nexp (nconstant (List.length vec))); + [mk_typ_arg (Typ_arg_nexp (nint (List.length vec - 1))); + mk_typ_arg (Typ_arg_nexp (nint (List.length vec))); mk_typ_arg (Typ_arg_order (Env.get_default_order env)); mk_typ_arg (Typ_arg_typ (typ_of inferred_item))])) in @@ -3416,7 +3416,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 ((basec - topc) + 1)) bit_typ in + let vec_typ = dvector_typ env base (nconstant (add_big_int (sub_big_int basec topc) unit_big_int)) 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 1254ec36..99385b31 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -43,6 +43,7 @@ open Ast open Ast_util +open Big_int val opt_tc_debug : int ref val opt_no_effects : bool ref @@ -76,7 +77,7 @@ module Env : sig val get_register : id -> t -> typ - val get_regtyp : id -> t -> int * int * (index_range * id) list + val get_regtyp : id -> t -> big_int * big_int * (index_range * id) list (* Return all the identifiers in an enumeration. Throws a type error if the enumeration doesn't exist. *) |