diff options
| -rw-r--r-- | aarch64/prelude.sail | 10 | ||||
| -rw-r--r-- | lib/flow.sail | 4 | ||||
| -rw-r--r-- | riscv/prelude.sail | 5 | ||||
| -rw-r--r-- | src/lexer.mll | 9 | ||||
| -rw-r--r-- | src/process_file.ml | 16 | ||||
| -rw-r--r-- | test/typecheck/pass/arm_types.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_tlb.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/simple_record_access.sail | 2 |
8 files changed, 27 insertions, 23 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index ab916e27..8851b7aa 100644 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -5,10 +5,6 @@ $include <flow.sail> type bits ('n : Int) = vector('n, dec, bit) -infix 4 == - -val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool - val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool @@ -27,7 +23,7 @@ val list_length = {ocaml: "length", lem: "length_list"} : forall ('a : Type). li overload length = {bitvector_length, vector_length, list_length} -overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything} +overload operator == = {eq_vec, eq_string, eq_real, eq_anything} val vector_subrange_A = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) @@ -248,14 +244,10 @@ val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> r val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int -infixl 7 / - overload operator / = {quotient_nat, quotient, quotient_real} val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int -infixl 7 % - overload operator % = {modulus} val Real = {ocaml: "to_real", lem: "realFromInteger"} : int -> real diff --git a/lib/flow.sail b/lib/flow.sail index cb7b1b99..2ca0e1a8 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -25,6 +25,10 @@ val lteq_atom_range = "lteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> boo val gt_atom_range = "gt" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool + +overload operator == = {eq_atom, eq_int} + $ifdef TEST val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 19b8abd8..370f9370 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -2,7 +2,6 @@ default Order dec type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None, Some : 'a} -infix 4 == val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool @@ -251,14 +250,10 @@ val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> r val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int -infixl 7 / - overload operator / = {quotient_nat, quotient, quotient_real} val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int -infixl 7 % - overload operator % = {modulus} val Real = {ocaml: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real diff --git a/src/lexer.mll b/src/lexer.mll index 77fba70b..3538d5cb 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -93,7 +93,14 @@ let mk_operator prec n op = | InfixR, 9 -> Op9r op | _, _ -> assert false -let operators = ref M.empty +let operators = ref + (List.fold_left + (fun r (x, y) -> M.add x y r) + M.empty + [ ("==", mk_operator Infix 4 "=="); + ("/", mk_operator InfixL 7 "/"); + ("%", mk_operator InfixL 7 "%"); + ]) let kw_table = List.fold_left diff --git a/src/process_file.ml b/src/process_file.ml index 1ba8069f..8f75c7a3 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -93,7 +93,7 @@ let cond_pragma defs = else else_defs := (def :: !else_defs) in - + let rec scan = function | Parse_ast.DEF_pragma ("endif", _, _) :: defs when !depth = 0 -> (List.rev !then_defs, List.rev !else_defs, defs) @@ -108,13 +108,13 @@ let cond_pragma defs = | [] -> failwith "$ifdef or $ifndef never ended" in scan defs - + let rec preprocess = function | [] -> [] | Parse_ast.DEF_pragma ("define", symbol, _) :: defs -> symbols := StringSet.add symbol !symbols; preprocess defs - + | Parse_ast.DEF_pragma ("ifndef", symbol, _) :: defs -> let then_defs, else_defs, defs = cond_pragma defs in if not (StringSet.mem symbol !symbols) then @@ -128,7 +128,7 @@ let rec preprocess = function preprocess (then_defs @ defs) else preprocess (else_defs @ defs) - + | Parse_ast.DEF_pragma ("include", file, l) :: defs -> let len = String.length file in if len = 0 then @@ -151,18 +151,18 @@ let rec preprocess = function let file = Filename.concat sail_dir ("lib/" ^ file) in let (Parse_ast.Defs include_defs) = parse_file file in let include_defs = preprocess include_defs in - include_defs @ preprocess defs + include_defs @ preprocess defs else let help = "Make sure the filename is surrounded by quotes or angle brackets" in (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess defs) | Parse_ast.DEF_pragma (p, arg, _) :: defs -> - (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess defs) - + (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess defs) + | def :: defs -> def :: preprocess defs let preprocess_ast (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess defs) - + let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs let load_file_no_check order f = convert_ast order (preprocess_ast (parse_file f)) diff --git a/test/typecheck/pass/arm_types.sail b/test/typecheck/pass/arm_types.sail index 83cc8687..af0bcba9 100644 --- a/test/typecheck/pass/arm_types.sail +++ b/test/typecheck/pass/arm_types.sail @@ -1,3 +1,5 @@ +$include <flow.sail> + enum boolean = {FALSE, TRUE} enum signal = {LOW, HIGH} diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail index f1b79b3d..de15edf8 100644 --- a/test/typecheck/pass/exist_tlb.sail +++ b/test/typecheck/pass/exist_tlb.sail @@ -1,3 +1,5 @@ +$include <flow.sail> + val extz : forall ('n : Int) ('m : Int) ('ord : Order). vector('n, 'ord, bit) -> vector('m, 'ord, bit) diff --git a/test/typecheck/pass/simple_record_access.sail b/test/typecheck/pass/simple_record_access.sail index b1eab652..a6e34c8b 100644 --- a/test/typecheck/pass/simple_record_access.sail +++ b/test/typecheck/pass/simple_record_access.sail @@ -1,3 +1,5 @@ +$include <flow.sail> + enum signal = {LOW, HIGH} type Bit32 = vector(32, inc, bit) |