diff options
198 files changed, 1164 insertions, 3680 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 5f3930b6..87adb290 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1022,7 +1022,6 @@ let generate_undefineds vs_ids (Defs defs) = gen_vs (mk_id "undefined_string") "unit -> string effect {undef}"; gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; - (* FIXME: How to handle inc/dec order correctly? *) gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}"; (* Only used with lem_mwords *) gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}"; diff --git a/src/initial_check.mli b/src/initial_check.mli index 9d1e0d30..5466dece 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -54,6 +54,15 @@ open Ast_util val opt_undefined_gen : bool ref val opt_magic_hash : bool ref +(* This is a bit of a hack right now - it ensures that the undefiend + builtins (undefined_vector etc), only get added to the ast + once. The original assumption in sail is that the whole AST gets + processed at once (therefore they could only get added once), and + this isn't true any more with the interpreter. This needs to be + public so the interpreter can set it back to false if it unloads + all the loaded files. *) +val have_undefined_builtins : bool ref + val ast_of_def_string : order -> string -> unit defs val process_ast : order -> Parse_ast.defs -> unit defs diff --git a/src/isail.ml b/src/isail.ml index a0e45e45..e6dcc809 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -112,6 +112,8 @@ let print_program () = let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep); print_endline out + | Evaluation (Done (_, v)) -> + print_endline (Value.string_of_value v |> Util.green |> Util.clear) | Evaluation _ -> () let rec run () = @@ -177,6 +179,8 @@ let help = function | ":l" | ":load" -> String.concat "\n" [ "(:l | :load) <files> - Load sail files and add their definitions to the interactive environment."; "Files containing scattered definitions must be loaded together." ] + | ":u" | ":unload" -> + "(:u | :unload) - Unload all loaded files." | cmd -> "Either invalid command passed to help, or no documentation for " ^ cmd ^ ". Try :help :help." @@ -236,8 +240,10 @@ let handle_input' input = | ":commands" -> let commands = [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :clear :commands :help"; - "Normal mode commands - :elf :(l)oad"; - "Evaluation mode commands - :(r)un :(s)tep :(n)ormal" ] + "Normal mode commands - :elf :(l)oad :(u)nload"; + "Evaluation mode commands - :(r)un :(s)tep :(n)ormal"; + ""; + ":(c)ommand can be called as either :c or :command." ] in List.iter print_endline commands | ":help" -> print_endline (help arg) @@ -263,6 +269,13 @@ let handle_input' input = interactive_state := initial_state !interactive_ast; interactive_env := env; vs_ids := Initial_check.val_spec_ids !interactive_ast + | ":u" | ":unload" -> + interactive_ast := Ast.Defs []; + interactive_env := Type_check.initial_env; + interactive_state := initial_state !interactive_ast; + vs_ids := Initial_check.val_spec_ids !interactive_ast; + (* See initial_check.mli for an explanation of why we need this. *) + Initial_check.have_undefined_builtins := false | _ -> unrecognised_command cmd end | Expression str -> diff --git a/src/lexer.mll b/src/lexer.mll index d13ba849..fb33552b 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -131,7 +131,6 @@ let kw_table = ("let", (fun x -> Let_)); ("var", (fun _ -> Var)); ("ref", (fun _ -> Ref)); - ("record", (fun _ -> Record)); ("Int", (fun x -> Int)); ("Order", (fun x -> Order)); ("pure", (fun x -> Pure)); @@ -201,6 +200,7 @@ rule token = parse | "@" { (At "@") } | "2" ws "^" { TwoCaret } | "^" { (Caret(r"^")) } + | "::" { ColonColon(r "::") } | ":" { Colon(r ":") } | "," { Comma } | ".." { DotDot } diff --git a/src/parser.mly b/src/parser.mly index 7af70687..b11b4b61 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -107,6 +107,7 @@ let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l) let mk_recn = (Rec_aux((Rec_nonrec), Unknown)) let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown)) let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown) +let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), loc n m) let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown) let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown) @@ -157,7 +158,7 @@ let rec desugar_rchain chain s e = %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token Repeat Until While Do Record Mutual Var Ref +%token Repeat Until While Do Mutual Var Ref %nonassoc Then %nonassoc Else @@ -173,7 +174,7 @@ let rec desugar_rchain chain s e = %token <string> String Bin Hex Real %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit -%token <string> Colon ExclEq +%token <string> Colon ColonColon ExclEq %token <string> GtEq %token <string> LtEq @@ -639,6 +640,8 @@ pat1: { $1 } | atomic_pat At pat_concat { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos } + | atomic_pat ColonColon pat1 + { mk_pat (P_cons ($1, $3)) $startpos $endpos } pat_concat: | atomic_pat @@ -679,6 +682,10 @@ atomic_pat: { mk_pat (P_tup ($2 :: $4)) $startpos $endpos } | Lsquare pat_list Rsquare { mk_pat (P_vector $2) $startpos $endpos } + | LsquareBar RsquareBar + { mk_pat (P_list []) $startpos $endpos } + | LsquareBar pat_list RsquareBar + { mk_pat (P_list $2) $startpos $endpos } lit: | True @@ -854,6 +861,7 @@ exp5: | exp5l op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos } + | exp6 ColonColon exp5r { mk_exp (E_cons ($1, $3)) $startpos $endpos } | exp6 { $1 } exp5l: | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } @@ -863,6 +871,7 @@ exp5r: | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos } + | exp6 ColonColon exp5r { mk_exp (E_cons ($1, $3)) $startpos $endpos } | exp6 { $1 } exp6: @@ -999,7 +1008,7 @@ atomic_exp: { mk_exp (E_vector_access ($1, $3)) $startpos $endpos } | atomic_exp Lsquare exp DotDot exp Rsquare { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos } - | Record Lcurly fexp_exp_list Rcurly + | Struct Lcurly fexp_exp_list Rcurly { mk_exp (E_record $3) $startpos $endpos } | Lcurly exp With fexp_exp_list Rcurly { mk_exp (E_record_update ($2, $4)) $startpos $endpos } @@ -1009,6 +1018,8 @@ atomic_exp: { mk_exp (E_vector_update ($2, $4, $6)) $startpos $endpos } | Lsquare exp With atomic_exp DotDot atomic_exp Eq exp Rsquare { mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos } + | LsquareBar RsquareBar + { mk_exp (E_list []) $startpos $endpos } | LsquareBar exp_list RsquareBar { mk_exp (E_list $2) $startpos $endpos } | Lparen exp Rparen @@ -1038,16 +1049,38 @@ funcl_patexp: | Lparen pat If_ exp Rparen Eq exp { mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos } +funcl_patexp_typ: + | pat Eq exp + { (mk_pexp (Pat_exp ($1, $3)) $startpos $endpos, mk_tannotn) } + | pat MinusGt funcl_typ Eq exp + { (mk_pexp (Pat_exp ($1, $5)) $startpos $endpos, $3) } + | Lparen pat If_ exp Rparen Eq exp + { (mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos, mk_tannotn) } + | Lparen pat If_ exp Rparen MinusGt funcl_typ Eq exp + { (mk_pexp (Pat_when ($2, $4, $9)) $startpos $endpos, $7) } + funcl: | id funcl_patexp { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos } -funcls: +funcls2: | id funcl_patexp { [mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos] } - | id funcl_patexp And funcls + | id funcl_patexp And funcls2 { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4 } +funcls: + | id funcl_patexp_typ + { let pexp, tannot = $2 in ([mk_funcl (FCL_Funcl ($1, pexp)) $startpos $endpos], tannot) } + | id funcl_patexp And funcls2 + { (mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4, mk_tannotn) } + +funcl_typ: + | Forall typquant Dot typ + { mk_tannot $2 $4 $startpos $endpos } + | typ + { mk_tannot mk_typqn $1 $startpos $endpos } + index_range: | Num { mk_ir (BF_single $1) $startpos $endpos } @@ -1130,7 +1163,7 @@ type_unions: fun_def: | Function_ funcls - { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } + { let funcls, tannot = $2 in mk_fun (FD_function (mk_recn, tannot, mk_eannotn, funcls)) $startpos $endpos } fun_def_list: | fun_def diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 930da39c..887b15a0 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -220,6 +220,7 @@ let rec doc_pat (P_aux (p_aux, _) as pat) = | P_wild -> string "_" | P_as (pat, id) -> separate space [doc_pat pat; string "as"; doc_id id] | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats) + | P_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_pat pats ^^ string "|]" | _ -> string (string_of_pat pat) (* if_block_x is true if x should be printed like a block, i.e. with @@ -285,8 +286,8 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp]) | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]" - | E_cons (exp1, exp2) -> string "E_cons" - | E_record fexps -> separate space [string "record"; string "{"; doc_fexps fexps; string "}"] + | E_cons (exp1, exp2) -> doc_atomic_exp exp1 ^^ space ^^ string "::" ^^ space ^^ doc_exp exp2 + | E_record fexps -> separate space [string "struct"; string "{"; doc_fexps fexps; string "}"] | E_loop (While, cond, exp) -> separate space [string "while"; doc_exp cond; string "do"; doc_exp exp] | E_loop (Until, cond, exp) -> diff --git a/src/type_check.ml b/src/type_check.ml index 01ff8649..3353daf4 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2722,6 +2722,14 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc) | _ -> assert false (* Unreachable *) end + (* Not sure if we need to do anything different with args here. *) + | Typ_aux (Typ_app (rectyp, args), _) as typ when Env.is_record rectyp env -> + begin + let inferred_acc, _ = infer_funapp' l (Env.no_casts env) field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] None in + match inferred_acc with + | E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc) + | _ -> assert false (* Unreachable *) + end | _ -> typ_error l ("Field expression " ^ string_of_exp exp ^ " :: " ^ string_of_typ (typ_of inferred_exp) ^ " is not valid") end | E_tuple exps -> diff --git a/test/typecheck/fail/assignment_simple1.sail b/test/typecheck/fail/assignment_simple1.sail deleted file mode 100644 index 1ad9f8bf..00000000 --- a/test/typecheck/fail/assignment_simple1.sail +++ /dev/null @@ -1,16 +0,0 @@ - -val ([:10:], unit) -> [:10:] effect pure f - -function [:10:] f (x, y) = x - -val unit -> [:10:] effect pure test - -function [:10:] test () = -{ - z := 9; - z -} - -val unit -> unit effect pure test2 - -function unit test2 () = x := 10 diff --git a/test/typecheck/fail/assignment_simple2.sail b/test/typecheck/fail/assignment_simple2.sail deleted file mode 100644 index db45bbcf..00000000 --- a/test/typecheck/fail/assignment_simple2.sail +++ /dev/null @@ -1,15 +0,0 @@ - -val ([:10:], unit) -> [:10:] effect pure f - -function [:10:] f (x, y) = x - -val unit -> [:10:] effect pure test - -function [:10:] test () = -{ - f(z, z := 10) -} - -val unit -> unit effect pure test2 - -function unit test2 () = x := 10 diff --git a/test/typecheck/fail/assignment_simple3.sail b/test/typecheck/fail/assignment_simple3.sail deleted file mode 100644 index 2a596c29..00000000 --- a/test/typecheck/fail/assignment_simple3.sail +++ /dev/null @@ -1,15 +0,0 @@ - -val (unit, [:10:]) -> [:10:] effect pure f - -function [:10:] f (x, y) = y - -val unit -> [:10:] effect pure test - -function [:10:] test () = -{ - f(z := 10, z) -} - -val unit -> unit effect pure test2 - -function unit test2 () = x := 10 diff --git a/test/typecheck/fail/bitwise_not_gen1.sail b/test/typecheck/fail/bitwise_not_gen1.sail deleted file mode 100644 index 272b1a65..00000000 --- a/test/typecheck/fail/bitwise_not_gen1.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not - -default Order dec - -val forall 'n. bit['n] -> bit['n - 1] effect pure test - -function forall 'n. bit['n - 1] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file diff --git a/test/typecheck/fail/bitwise_not_gen2.sail b/test/typecheck/fail/bitwise_not_gen2.sail deleted file mode 100644 index fdf17244..00000000 --- a/test/typecheck/fail/bitwise_not_gen2.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not - -default Order dec - -val forall 'n. bit['n] -> bit['n + 1] effect pure test - -function forall 'n. bit['n + 1] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file diff --git a/test/typecheck/fail/bv_simple_index_no_cast.sail b/test/typecheck/fail/bv_simple_index_no_cast.sail deleted file mode 100644 index 74f46ab7..00000000 --- a/test/typecheck/fail/bv_simple_index_no_cast.sail +++ /dev/null @@ -1,9 +0,0 @@ -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc - -overload vector_access [vector_access_inc; vector_access_dec] - -function bool bv ((bit[64]) x) = -{ - x[32] -} diff --git a/test/typecheck/fail/case_simple1.sail b/test/typecheck/fail/case_simple1.sail deleted file mode 100644 index 471c3565..00000000 --- a/test/typecheck/fail/case_simple1.sail +++ /dev/null @@ -1,9 +0,0 @@ - -val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test - -function forall Nat 'N. [|10:'N|] case_test (x, y) = -{ - switch (x, y) { - case _ -> x - } -} diff --git a/test/typecheck/fail/cast_lexp1.sail b/test/typecheck/fail/cast_lexp1.sail deleted file mode 100644 index dad4c84c..00000000 --- a/test/typecheck/fail/cast_lexp1.sail +++ /dev/null @@ -1,7 +0,0 @@ - -val unit -> nat effect pure test - -function nat test () = { - (int) y := 10; - y -} diff --git a/test/typecheck/fail/cast_simple.sail b/test/typecheck/fail/cast_simple.sail deleted file mode 100644 index 19768fbe..00000000 --- a/test/typecheck/fail/cast_simple.sail +++ /dev/null @@ -1,7 +0,0 @@ - -val unit -> nat effect pure test - -function nat test () = { - (int) y := ([|0:10|]) 10; - (nat) y -} diff --git a/test/typecheck/fail/default_order.sail b/test/typecheck/fail/default_order.sail deleted file mode 100644 index 8de5cc46..00000000 --- a/test/typecheck/fail/default_order.sail +++ /dev/null @@ -1,6 +0,0 @@ -(* Could make an argument for why this should be ok, but allowing -default order to change could have unintended consequences if we arn't -careful, so it seems safer to just forbid it *) - -default Order dec -default Order inc diff --git a/test/typecheck/fail/eff_escape.sail b/test/typecheck/fail/eff_escape.sail deleted file mode 100644 index 698cf0b1..00000000 --- a/test/typecheck/fail/eff_escape.sail +++ /dev/null @@ -1,7 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - exit () -} diff --git a/test/typecheck/fail/eff_undef.sail b/test/typecheck/fail/eff_undef.sail deleted file mode 100644 index d5d98a3f..00000000 --- a/test/typecheck/fail/eff_undef.sail +++ /dev/null @@ -1,7 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - undefined -} diff --git a/test/typecheck/fail/ex_cast.sail b/test/typecheck/fail/ex_cast.sail deleted file mode 100644 index 5ea22d14..00000000 --- a/test/typecheck/fail/ex_cast.sail +++ /dev/null @@ -1,12 +0,0 @@ - -default Order dec - -val cast int -> exist 'n. [:'n:] effect pure ex_int - -val [:'n:] -> bit['n] effect pure zeros - -val int -> unit effect pure test - -function test n = { - x := zeros(n) -} diff --git a/test/typecheck/fail/exist1.sail b/test/typecheck/fail/exist1.sail deleted file mode 100644 index 3fab1366..00000000 --- a/test/typecheck/fail/exist1.sail +++ /dev/null @@ -1,30 +0,0 @@ - -let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 - -val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test - -function test flag = -{ - if flag then 0 else 1 -} - -let ([|0:1|]) v2 = test(true) - -val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add - -let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 - -let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 - -let v5 = add(test(true), 4) - -let ([:4:]) v6 = 4 - -function unit unit_fn (([:4:]) x) = () - -val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add - -let (exist 'k, 'k = 4. [:'k:]) v7 = 4 - -let v8 = s_add(test(true), 4) - diff --git a/test/typecheck/fail/flow_gt1.sail b/test/typecheck/fail/flow_gt1.sail deleted file mode 100644 index 917793cd..00000000 --- a/test/typecheck/fail/flow_gt1.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order inc - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x > 31) - then x - 33 - else x + 32 -} diff --git a/test/typecheck/fail/flow_gt2.sail b/test/typecheck/fail/flow_gt2.sail deleted file mode 100644 index f5ea4978..00000000 --- a/test/typecheck/fail/flow_gt2.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order inc - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x > 31) - then x - 32 - else x + 33 -} diff --git a/test/typecheck/fail/flow_gteq1.sail b/test/typecheck/fail/flow_gteq1.sail deleted file mode 100644 index b55647d3..00000000 --- a/test/typecheck/fail/flow_gteq1.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order inc - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x >= 32) - then x - 33 - else x + 32 -} diff --git a/test/typecheck/fail/flow_gteq2.sail b/test/typecheck/fail/flow_gteq2.sail deleted file mode 100644 index 9d0a6201..00000000 --- a/test/typecheck/fail/flow_gteq2.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order inc - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x >= 32) - then x - 32 - else x + 33 -} diff --git a/test/typecheck/fail/flow_lt1.sail b/test/typecheck/fail/flow_lt1.sail deleted file mode 100644 index a127ccb0..00000000 --- a/test/typecheck/fail/flow_lt1.sail +++ /dev/null @@ -1,19 +0,0 @@ -default Order inc - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x < 32) - then x + 33 - else x - 32 -} diff --git a/test/typecheck/fail/flow_lt2.sail b/test/typecheck/fail/flow_lt2.sail deleted file mode 100644 index a537a084..00000000 --- a/test/typecheck/fail/flow_lt2.sail +++ /dev/null @@ -1,19 +0,0 @@ -default Order inc - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x < 32) - then x + 32 - else x - 33 -} diff --git a/test/typecheck/fail/flow_lteq1.sail b/test/typecheck/fail/flow_lteq1.sail deleted file mode 100644 index 3bebcc97..00000000 --- a/test/typecheck/fail/flow_lteq1.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order inc - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x <= 32) - then x + 32 - else x - 33 -} diff --git a/test/typecheck/fail/flow_lteq2.sail b/test/typecheck/fail/flow_lteq2.sail deleted file mode 100644 index c3ee9c0a..00000000 --- a/test/typecheck/fail/flow_lteq2.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order inc - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range - -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x <= 32) - then x + 31 - else x - 34 -} diff --git a/test/typecheck/fail/fun_simple_constraints1.sail b/test/typecheck/fail/fun_simple_constraints1.sail deleted file mode 100644 index 979e0cdf..00000000 --- a/test/typecheck/fail/fun_simple_constraints1.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus - -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) -and branch (([|51:64|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints2.sail b/test/typecheck/fail/fun_simple_constraints2.sail deleted file mode 100644 index 43a0b6d7..00000000 --- a/test/typecheck/fail/fun_simple_constraints2.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus - -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) -and branch (([|51:63|]) _) = ten_id(9) diff --git a/test/typecheck/fail/fun_simple_constraints3.sail b/test/typecheck/fail/fun_simple_constraints3.sail deleted file mode 100644 index 098054e4..00000000 --- a/test/typecheck/fail/fun_simple_constraints3.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus - -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) -and branch (([|51:63|]) _) = ten_id(plus(sizeof 'N, 1)) diff --git a/test/typecheck/fail/fun_simple_constraints4.sail b/test/typecheck/fail/fun_simple_constraints4.sail deleted file mode 100644 index 07b8c596..00000000 --- a/test/typecheck/fail/fun_simple_constraints4.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus - -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-54)) -and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints5.sail b/test/typecheck/fail/fun_simple_constraints5.sail deleted file mode 100644 index 7e28db85..00000000 --- a/test/typecheck/fail/fun_simple_constraints5.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus - -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-9)) -and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints6.sail b/test/typecheck/fail/fun_simple_constraints6.sail deleted file mode 100644 index 6dc5e0e6..00000000 --- a/test/typecheck/fail/fun_simple_constraints6.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'k, Nat 'm. ([:'n + 'k:], [:'m:]) -> [:'n + 'k + 'm:] effect pure plus - -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) -and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints7.sail b/test/typecheck/fail/fun_simple_constraints7.sail deleted file mode 100644 index 00d2a172..00000000 --- a/test/typecheck/fail/fun_simple_constraints7.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus - -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|11:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) -and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints8.sail b/test/typecheck/fail/fun_simple_constraints8.sail deleted file mode 100644 index e4c02da0..00000000 --- a/test/typecheck/fail/fun_simple_constraints8.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus - -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|11:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) -and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints9.sail b/test/typecheck/fail/fun_simple_constraints9.sail deleted file mode 100644 index 3563ae2d..00000000 --- a/test/typecheck/fail/fun_simple_constraints9.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus - -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id - -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = ten_id(plus(sizeof 'N, 1)) diff --git a/test/typecheck/fail/funret1.sail b/test/typecheck/fail/funret1.sail deleted file mode 100644 index 09a4fd54..00000000 --- a/test/typecheck/fail/funret1.sail +++ /dev/null @@ -1,16 +0,0 @@ - -default Order inc - -typedef option = const union forall Type 'a. { - None; - 'a Some - } - -typedef Test = const union { - A; - B; - C -} - -let (option<int>) x = C - diff --git a/test/typecheck/fail/funret2.sail b/test/typecheck/fail/funret2.sail deleted file mode 100644 index 19536599..00000000 --- a/test/typecheck/fail/funret2.sail +++ /dev/null @@ -1,16 +0,0 @@ - -default Order inc - -typedef option = const union forall Type 'a. { - None; - 'a Some - } - -typedef Test = const union { - A; - B; - C -} - - -function option<int> test2 () = C diff --git a/test/typecheck/fail/funret3.sail b/test/typecheck/fail/funret3.sail deleted file mode 100644 index d178f2ad..00000000 --- a/test/typecheck/fail/funret3.sail +++ /dev/null @@ -1,16 +0,0 @@ - -default Order inc - -typedef option = const union forall Type 'a. { - None; - 'a Some - } - -typedef Test = const union { - A; - B; - C -} - - -function option<(option<int>)> test () = Some(C) diff --git a/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail b/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail deleted file mode 100644 index 2f599aa9..00000000 --- a/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail +++ /dev/null @@ -1,27 +0,0 @@ -val forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv -val forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv - -default Order dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -register (CauseReg) CP0Cause - -val unit -> unit effect {wreg} test - -function unit test () = -{ - CP0Cause.BD := 2 -} diff --git a/test/typecheck/fail/mips_CauseReg1.sail b/test/typecheck/fail/mips_CauseReg1.sail deleted file mode 100644 index ae99e625..00000000 --- a/test/typecheck/fail/mips_CauseReg1.sail +++ /dev/null @@ -1,14 +0,0 @@ - -typedef CauseReg = register bits [ 30 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/fail/mips_CauseReg2.sail b/test/typecheck/fail/mips_CauseReg2.sail deleted file mode 100644 index 683f5a2a..00000000 --- a/test/typecheck/fail/mips_CauseReg2.sail +++ /dev/null @@ -1,14 +0,0 @@ - -typedef CauseReg = register bits [ 31 : 3 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/fail/mips_CauseReg3.sail b/test/typecheck/fail/mips_CauseReg3.sail deleted file mode 100644 index 09e27e27..00000000 --- a/test/typecheck/fail/mips_CauseReg3.sail +++ /dev/null @@ -1,14 +0,0 @@ - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 32 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/fail/mips_CauseReg4.sail b/test/typecheck/fail/mips_CauseReg4.sail deleted file mode 100644 index 1f14981f..00000000 --- a/test/typecheck/fail/mips_CauseReg4.sail +++ /dev/null @@ -1,14 +0,0 @@ - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 8 .. 15 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/fail/mips_CauseReg5.sail b/test/typecheck/fail/mips_CauseReg5.sail deleted file mode 100644 index 98fc614a..00000000 --- a/test/typecheck/fail/mips_CauseReg5.sail +++ /dev/null @@ -1,14 +0,0 @@ - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 22 : IV; (* special interrupt vector not supported *) - 23 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/fail/mips_CauseReg6.sail b/test/typecheck/fail/mips_CauseReg6.sail deleted file mode 100644 index ecb8322e..00000000 --- a/test/typecheck/fail/mips_CauseReg6.sail +++ /dev/null @@ -1,14 +0,0 @@ - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : BD; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/fail/mips_CauseReg7.sail b/test/typecheck/fail/mips_CauseReg7.sail deleted file mode 100644 index 48acd4f5..00000000 --- a/test/typecheck/fail/mips_CauseReg7.sail +++ /dev/null @@ -1,15 +0,0 @@ -default Order dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 23 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/fail/mismatch_return.sail b/test/typecheck/fail/mismatch_return.sail deleted file mode 100644 index 85b8b636..00000000 --- a/test/typecheck/fail/mismatch_return.sail +++ /dev/null @@ -1,7 +0,0 @@ - -val unit -> unit effect pure test - -function int test () = -{ - () -} diff --git a/test/typecheck/fail/modify_assignment1.sail b/test/typecheck/fail/modify_assignment1.sail deleted file mode 100644 index 99adc95c..00000000 --- a/test/typecheck/fail/modify_assignment1.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - z := 9; - z := 10 -}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_assignment2.sail b/test/typecheck/fail/modify_assignment2.sail deleted file mode 100644 index 6551afff..00000000 --- a/test/typecheck/fail/modify_assignment2.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - ([|0:9|]) z := 9; - z := ([|0:10|]) 10 -}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_let_bound.sail b/test/typecheck/fail/modify_let_bound.sail deleted file mode 100644 index a2ad1b98..00000000 --- a/test/typecheck/fail/modify_let_bound.sail +++ /dev/null @@ -1,16 +0,0 @@ - -default Order dec - -register bit[3] test - -val unit -> unit effect pure test - -function unit test () = -{ - let i = 10 in { - i := 20 - }; - z := 9; - z := 10; - test := 3 -}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain1.sail b/test/typecheck/fail/modify_type_chain1.sail deleted file mode 100644 index 3fff3b59..00000000 --- a/test/typecheck/fail/modify_type_chain1.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - ([|0:10|]) z := 9; - ([|0:9|]) z := ([|0:10|]) 8 -}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain2.sail b/test/typecheck/fail/modify_type_chain2.sail deleted file mode 100644 index 085e7db5..00000000 --- a/test/typecheck/fail/modify_type_chain2.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - ([|0:10|]) z := 9; - ([|0:7|]) z := ([|0:8|]) 8 -}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain3.sail b/test/typecheck/fail/modify_type_chain3.sail deleted file mode 100644 index cfe532aa..00000000 --- a/test/typecheck/fail/modify_type_chain3.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - ([|0:6|]) z := 9; - ([|0:7|]) z := ([|0:8|]) 8 -}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain4.sail b/test/typecheck/fail/modify_type_chain4.sail deleted file mode 100644 index c36a9086..00000000 --- a/test/typecheck/fail/modify_type_chain4.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - ([|0:10|]) z := 9; - ([|0:11|]) z := ([|0:13|]) 8 -}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain5.sail b/test/typecheck/fail/modify_type_chain5.sail deleted file mode 100644 index 3c3076a4..00000000 --- a/test/typecheck/fail/modify_type_chain5.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val unit -> unit effect pure test - -function unit test () = -{ - ([|0:10|]) z := 9; - ([|0:9|]) z := ([|0:13|]) 8 -}
\ No newline at end of file diff --git a/test/typecheck/fail/my_unsigned1.sail b/test/typecheck/fail/my_unsigned1.sail deleted file mode 100644 index 958340ff..00000000 --- a/test/typecheck/fail/my_unsigned1.sail +++ /dev/null @@ -1,8 +0,0 @@ - -default Order inc - -val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o >= 0, 'o + 1 <= 2**'m. vector<'n,'m,'ord,bit> -> [:'o:] effect pure my_unsigned - -let MAX = my_unsigned(0xff) - -let ([:0:]) MIN = MAX
\ No newline at end of file diff --git a/test/typecheck/fail/nat_set.sail b/test/typecheck/fail/nat_set.sail deleted file mode 100644 index 036183c5..00000000 --- a/test/typecheck/fail/nat_set.sail +++ /dev/null @@ -1,9 +0,0 @@ - -function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) = -{ - true -} - -let x = test(1) -let y = test(3) -let z = test(4)
\ No newline at end of file diff --git a/test/typecheck/fail/nondet.sail b/test/typecheck/fail/nondet.sail deleted file mode 100644 index bce110c6..00000000 --- a/test/typecheck/fail/nondet.sail +++ /dev/null @@ -1,10 +0,0 @@ - -register int z - -function int test () = { - nondet { - z := 0; - z := 1; - z - } -} diff --git a/test/typecheck/fail/option_either1.sail b/test/typecheck/fail/option_either1.sail deleted file mode 100644 index 569ba212..00000000 --- a/test/typecheck/fail/option_either1.sail +++ /dev/null @@ -1,35 +0,0 @@ -default Order inc - -typedef option = const union forall Type 'a. { - None; - 'a Some -} - -function forall Type 'a. option<'a> none () = None - -function forall Type 'a. option<'a> some (('a) x) = Some(x) - -function forall Type 'a. int test ((option<'a>) x) = -{ - switch x { - case None -> 0 - case (Some(y)) -> 1 - } -} - -typedef either = const union forall Type 'a, Type 'b. { - 'a Left; - 'b Right -} - -val forall Nat 'n, 'n >= 0. bit['n] -> int effect pure signed - -function forall Type 'a, Type 'b. either<'a,'b> right (('b) x) = Right(x) - -function int test2 ((either<int,bit[1]>) x) = -{ - switch x { - case (Left(l)) -> l - case (right(r)) -> signed(r) - } -} diff --git a/test/typecheck/fail/overlap_field_wreg.sail b/test/typecheck/fail/overlap_field_wreg.sail deleted file mode 100644 index 4c4d858d..00000000 --- a/test/typecheck/fail/overlap_field_wreg.sail +++ /dev/null @@ -1,13 +0,0 @@ - -typedef A = const struct {bool field_A; int shared} -typedef B = const struct {bool field_B; int shared} - -val (bool, int) -> A effect {undef, wreg} makeA - -function makeA (x, y) = -{ - (A) record := undefined; - record.field_A := x; - record.shared := y; - record -} diff --git a/test/typecheck/fail/procstate1.sail b/test/typecheck/fail/procstate1.sail deleted file mode 100644 index 00dc1ab1..00000000 --- a/test/typecheck/fail/procstate1.sail +++ /dev/null @@ -1,16 +0,0 @@ -default Order dec - -typedef ProcState = const struct forall Num 'n. -{ - bit['n] N; - bit[1] Z; - bit[1] C; - bit[1] V -} - -register ProcState<2> PSTATE - -function unit test () = -{ - PSTATE.N := 0b1 -} diff --git a/test/typecheck/fail/pure_record_arity.sail b/test/typecheck/fail/pure_record_arity.sail deleted file mode 100644 index 846df2c3..00000000 --- a/test/typecheck/fail/pure_record_arity.sail +++ /dev/null @@ -1,25 +0,0 @@ -default Order dec - -typedef State = const struct forall Type 'a, Nat 'n. { - vector<0, 'n, dec, 'a> N; - vector<0, 1, dec, bit> Z; -} - -register State procState - -let (State<bit,1>) myStateM = { - (State<bit,1>) r := undefined; - r.N := 0b1; - r.Z := 0b1; - r -} - -let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } - -val unit -> unit effect {undef} test - -function test () = { - (State<bit,1>) myState1 := undefined; - (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; - (State<bit,1>) myState3 := { myState2 with N = 0b0 } -} diff --git a/test/typecheck/fail/pure_record_arity2.sail b/test/typecheck/fail/pure_record_arity2.sail deleted file mode 100644 index a9566da8..00000000 --- a/test/typecheck/fail/pure_record_arity2.sail +++ /dev/null @@ -1,25 +0,0 @@ -default Order dec - -typedef State = const struct forall Type 'a, Nat 'n. { - vector<0, 'n, dec, 'a> N; - vector<0, 1, dec, bit> Z; -} - -register State<bit,inc> procState - -let (State<bit,1>) myStateM = { - (State<bit,1>) r := undefined; - r.N := 0b1; - r.Z := 0b1; - r -} - -let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } - -val unit -> unit effect {undef} test - -function test () = { - (State<bit,1>) myState1 := undefined; - (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; - (State<bit,1>) myState3 := { myState2 with N = 0b0 } -} diff --git a/test/typecheck/fail/reg_mod.sail b/test/typecheck/fail/reg_mod.sail deleted file mode 100644 index 24b318b4..00000000 --- a/test/typecheck/fail/reg_mod.sail +++ /dev/null @@ -1,11 +0,0 @@ - -register [|0:10|] reg - -val unit -> unit effect pure test - -function unit test () = -{ - reg := 9; - reg := 10; - reg := 8 -}
\ No newline at end of file diff --git a/test/typecheck/fail/return_simple2.sail b/test/typecheck/fail/return_simple2.sail deleted file mode 100644 index f212a945..00000000 --- a/test/typecheck/fail/return_simple2.sail +++ /dev/null @@ -1,9 +0,0 @@ - -val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test - -function forall Nat 'N. [|10:'N|] return_test x = -{ - x; - return x; - x -} diff --git a/test/typecheck/fail/return_simple3.sail b/test/typecheck/fail/return_simple3.sail deleted file mode 100644 index df75c5bd..00000000 --- a/test/typecheck/fail/return_simple3.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test - -function forall Nat 'N. [|10:'N|] return_test x = -{ - return 9; - x -} diff --git a/test/typecheck/fail/return_simple4.sail b/test/typecheck/fail/return_simple4.sail deleted file mode 100644 index aa7c3010..00000000 --- a/test/typecheck/fail/return_simple4.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test - -function forall Nat 'N. [|10:'N|] return_test x = -{ - return x; - 9 -} diff --git a/test/typecheck/fail/return_simple5.sail b/test/typecheck/fail/return_simple5.sail deleted file mode 100644 index d6947d91..00000000 --- a/test/typecheck/fail/return_simple5.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val forall Nat 'N. [|10:'N - 1|] -> [|10:'N - 1|] effect pure return_test - -function forall Nat 'N. [|10:'N - 1|] return_test x = -{ - return x; - sizeof 'N -} diff --git a/test/typecheck/fail/return_simple6.sail b/test/typecheck/fail/return_simple6.sail deleted file mode 100644 index 0e118632..00000000 --- a/test/typecheck/fail/return_simple6.sail +++ /dev/null @@ -1,8 +0,0 @@ - -val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test - -function forall Nat 'N. [|10:'N|] return_test x = -{ - return x; - sizeof 'N -} diff --git a/test/typecheck/fail/set_spsr1.sail b/test/typecheck/fail/set_spsr1.sail deleted file mode 100644 index 27c343b2..00000000 --- a/test/typecheck/fail/set_spsr1.sail +++ /dev/null @@ -1,17 +0,0 @@ -default Order dec - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec - -overload vector_subrange [vector_subrange_inc; vector_subrange_dec] - -register bit[32] SPSR_EL2 - -function unit set_SPSR_hyp (bit[32]) val_name = -{ - (bit[32]) r := val_name; - SPSR_EL2[30..0] := r -} diff --git a/test/typecheck/fail/set_spsr2.sail b/test/typecheck/fail/set_spsr2.sail deleted file mode 100644 index 00493444..00000000 --- a/test/typecheck/fail/set_spsr2.sail +++ /dev/null @@ -1,17 +0,0 @@ -default Order dec - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec - -overload vector_subrange [vector_subrange_inc; vector_subrange_dec] - -register bit[32] SPSR_EL2 - -function unit set_SPSR_hyp (bit[32]) val_name = -{ - (bit[32]) r := val_name; - SPSR_EL2[0..31] := r -} diff --git a/test/typecheck/fail/set_spsr3.sail b/test/typecheck/fail/set_spsr3.sail deleted file mode 100644 index c3a6208e..00000000 --- a/test/typecheck/fail/set_spsr3.sail +++ /dev/null @@ -1,17 +0,0 @@ -default Order dec - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec - -overload vector_subrange [vector_subrange_inc; vector_subrange_dec] - -register bit[32] SPSR_EL2 - -function unit set_SPSR_hyp (bit[32]) val_name = -{ - (bit[32]) r := val_name; - SPSR_EL2[32..1] := r -} diff --git a/test/typecheck/fail/set_spsr4.sail b/test/typecheck/fail/set_spsr4.sail deleted file mode 100644 index 65596b59..00000000 --- a/test/typecheck/fail/set_spsr4.sail +++ /dev/null @@ -1,17 +0,0 @@ -default Order dec - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec - -overload vector_subrange [vector_subrange_inc; vector_subrange_dec] - -register bit[31] SPSR_EL2 - -function unit set_SPSR_hyp (bit[32]) val_name = -{ - (bit[32]) r := val_name; - SPSR_EL2[31..0] := r -} diff --git a/test/typecheck/fail/set_spsr5.sail b/test/typecheck/fail/set_spsr5.sail deleted file mode 100644 index d8a6588c..00000000 --- a/test/typecheck/fail/set_spsr5.sail +++ /dev/null @@ -1,17 +0,0 @@ -default Order dec - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec - -overload vector_subrange [vector_subrange_inc; vector_subrange_dec] - -register bit[32] SPSR_EL2 - -function unit set_SPSR_hyp (bit[16]) val_name = -{ - (bit[32]) r := val_name; - SPSR_EL2[31..0] := r -} diff --git a/test/typecheck/fail/vec_pat1.sail b/test/typecheck/fail/vec_pat1.sail deleted file mode 100644 index e10838f6..00000000 --- a/test/typecheck/fail/vec_pat1.sail +++ /dev/null @@ -1,17 +0,0 @@ -default Order inc - -val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc" - -val forall Num 'n, Num 'm, Num 'o, Num 'p, Type 'a. - (vector<'n,'m,inc,'a>, vector<'o,'p,inc,'a>) -> vector<'n,'m + 'p,inc,'a> - effect pure vector_append_inc - -overload (deinfix +) [bv_add] -overload vector_append [vector_append_inc] - -val (bit[3], bit[3]) -> bit[3] effect pure test - -function bit[3] test (((bit[0]) x : 0b11 : 0b0), z) = -{ - (x : 0b11) + z -} diff --git a/test/typecheck/fail/vector_access1.sail b/test/typecheck/fail/vector_access1.sail deleted file mode 100644 index 1eef5250..00000000 --- a/test/typecheck/fail/vector_access1.sail +++ /dev/null @@ -1,12 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -default Order inc - -val bit[4] -> unit effect pure test - -function unit test v = -{ - z := vector_access(v,0); - z := v[4] -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_access2.sail b/test/typecheck/fail/vector_access2.sail deleted file mode 100644 index 0b4ba7c2..00000000 --- a/test/typecheck/fail/vector_access2.sail +++ /dev/null @@ -1,12 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -default Order inc - -val bit[4] -> unit effect pure test - -function unit test v = -{ - z := vector_access(v,-1); - z := v[3] -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_access3.sail b/test/typecheck/fail/vector_access3.sail deleted file mode 100644 index dd43cfea..00000000 --- a/test/typecheck/fail/vector_access3.sail +++ /dev/null @@ -1,12 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -default Order inc - -val bit[0] -> unit effect pure test - -function unit test v = -{ - z := vector_access(v,0); - z := v[0] -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_access4.sail b/test/typecheck/fail/vector_access4.sail deleted file mode 100644 index 31d34eae..00000000 --- a/test/typecheck/fail/vector_access4.sail +++ /dev/null @@ -1,12 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -default Order inc - -val bit[-5] -> unit effect pure test - -function unit test v = -{ - z := vector_access(v,([|0:-5|]) -1); - z := v[-1] -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append1.sail b/test/typecheck/fail/vector_append1.sail deleted file mode 100644 index e2429380..00000000 --- a/test/typecheck/fail/vector_append1.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append - -default Order inc - -val (bit[4], bit[4]) -> bit[7] effect pure test - -function bit[7] test (v1, v2) = -{ - z := vector_access(v1, 3); - z := v1[0]; - zv := vector_append(v1, v2); - zv := v1 : v2; - zv -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append2.sail b/test/typecheck/fail/vector_append2.sail deleted file mode 100644 index acaeb0b0..00000000 --- a/test/typecheck/fail/vector_append2.sail +++ /dev/null @@ -1,18 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append - -default Order inc - -val (bit[4], bit[4]) -> bit[9] effect pure test - -function bit[9] test (v1, v2) = -{ - z := vector_access(v1, 3); - z := v1[0]; - zv := vector_append(v1, v2); - zv := v1 : v2; - zv -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append3.sail b/test/typecheck/fail/vector_append3.sail deleted file mode 100644 index 82f0a861..00000000 --- a/test/typecheck/fail/vector_append3.sail +++ /dev/null @@ -1,18 +0,0 @@ -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc - -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append - -default Order inc - -val (bit[4], bit[4]) -> bit[7] effect pure test - -function bit[7] test (v1, v2) = -{ - z := vector_access(v1, 3); - z := v1[0]; - zv := vector_append(v1, v2); - zv := v1 : v2; - zv -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append_gen1.sail b/test/typecheck/fail/vector_append_gen1.sail deleted file mode 100644 index 727d5c14..00000000 --- a/test/typecheck/fail/vector_append_gen1.sail +++ /dev/null @@ -1,14 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append - -default Order inc - -val forall 'n, 'm. (bit['n], bit['m]) -> bit['n + 'm] effect pure test - -function forall 'n, 'm. bit['n + 'm] test (v1, v2) = -{ - v1 : v2; -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append_gen2.sail b/test/typecheck/fail/vector_append_gen2.sail deleted file mode 100644 index 8e534253..00000000 --- a/test/typecheck/fail/vector_append_gen2.sail +++ /dev/null @@ -1,14 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append - -default Order inc - -val forall 'n, 'm. (bit['n], bit['m]) -> bit['n + 'm] effect pure test - -function forall 'n, 'm. bit['n + 'm] test (v1, v2) = -{ - vector_append(v1, v2); -}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append_old.sail b/test/typecheck/fail/vector_append_old.sail deleted file mode 100644 index fb6018b9..00000000 --- a/test/typecheck/fail/vector_append_old.sail +++ /dev/null @@ -1,14 +0,0 @@ - -val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" - -default Order inc - -val (bit[4], bit[4]) -> bit[8] effect pure test - -function bit[8] test (v1, v2) = -{ - zv := vector_append(v1, v2); - zv := v1 : v2; - zv -} diff --git a/test/typecheck/fail/vector_arity.sail b/test/typecheck/fail/vector_arity.sail deleted file mode 100644 index 6ecc9565..00000000 --- a/test/typecheck/fail/vector_arity.sail +++ /dev/null @@ -1,4 +0,0 @@ - -val vector<0,5,inc,bit,bit> -> vector<0,5,inc,bit,bit> effect pure test - -function vector<0,5,inc,bit,bit> test x = x
\ No newline at end of file diff --git a/test/typecheck/fail/vector_subrange_gen1.sail b/test/typecheck/fail/vector_subrange_gen1.sail deleted file mode 100644 index 0ae6f9f9..00000000 --- a/test/typecheck/fail/vector_subrange_gen1.sail +++ /dev/null @@ -1,20 +0,0 @@ - -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'u, Order 'o, Type 'a, 'l >= 0, 'm <= 'u, 'u <= 'l. (vector<'n,'l,'o,'a>, [:'m:], [:'u:]) -> vector<'m,'u - 'm,'o,'a> effect pure vector_subrange - -val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure minus - -default Order inc - -val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 2] effect pure test - -function forall 'n, 'n >= 5. bit['n - 3] test v = -{ - z := vector_subrange(v, 0, minus(sizeof 'n, 3)); - z := v[0 .. minus(sizeof 'n, 2)]; - z -}
\ No newline at end of file diff --git a/test/typecheck/fail/word_width_bytes_mips.sail b/test/typecheck/fail/word_width_bytes_mips.sail deleted file mode 100644 index 91f3e787..00000000 --- a/test/typecheck/fail/word_width_bytes_mips.sail +++ /dev/null @@ -1,11 +0,0 @@ -typedef WordType = enumerate {B; H; W; D} - -(* This fails because it's not true for all combinations of 'r and WordType *) -(* Needs existential types, i.e. return type should be exists Nat 'r, 'r in {1,2,4,8}. [:'r:] *) -function forall Nat 'r, 'r IN {1,2,4,8}. wordWidthBytes((WordType) w) = - switch(w) { - case B -> 1 - case H -> 2 - case W -> 4 - case D -> 8 - } diff --git a/test/typecheck/pass/add_real.sail b/test/typecheck/pass/add_real.sail index 38a9cff3..54c64778 100644 --- a/test/typecheck/pass/add_real.sail +++ b/test/typecheck/pass/add_real.sail @@ -1,5 +1,5 @@ -val (real, real) -> real effect pure add_real +val add_real : (real, real) -> real -overload (deinfix +) [add_real] +overload operator + = {add_real} -let (real) r = 2.2 + 0.2 +let r : real = 2.2 + 0.2 diff --git a/test/typecheck/pass/add_vec_exts_no_annot.sail b/test/typecheck/pass/add_vec_exts_no_annot.sail index 54aa2d40..d1d3a7e8 100644 --- a/test/typecheck/pass/add_vec_exts_no_annot.sail +++ b/test/typecheck/pass/add_vec_exts_no_annot.sail @@ -1,19 +1,15 @@ default Order dec -val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. - vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts +val exts : forall ('n : Int) ('m : Int) ('ord : Order). + vector('n, 'ord, bit) -> vector('m, 'ord, bit) -overload EXTS [exts] +overload EXTS = {exts} -val forall Nat 'n, Nat 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec +val add_vec : forall ('n : Int) ('ord : Order). + (vector('n, 'ord, bit), vector('n, 'ord, bit)) -> vector('n, 'ord, bit) -overload (deinfix +) [add_vec] +overload operator + = {add_vec} -val (bit[32], bit[32]) -> unit effect pure test +val test : (vector(32, dec, bit), vector(32, dec, bit)) -> unit -function test (x, y) = -{ - let (bit[64]) z = add_vec(exts(x), exts(y)) in - () -} +function test (x, y) = let z : vector(64, dec, bit) = add_vec(exts(x), exts(y)) in () diff --git a/test/typecheck/pass/add_vec_exts_no_annot_overload.sail b/test/typecheck/pass/add_vec_exts_no_annot_overload.sail index 01e3bf7c..eb1ac00d 100644 --- a/test/typecheck/pass/add_vec_exts_no_annot_overload.sail +++ b/test/typecheck/pass/add_vec_exts_no_annot_overload.sail @@ -1,19 +1,15 @@ default Order dec -val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. - vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts +val exts : forall ('n : Int) ('m : Int) ('ord : Order). + vector('n, 'ord, bit) -> vector('m, 'ord, bit) -overload EXTS [exts] +overload EXTS = {exts} -val forall Nat 'n, Nat 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec +val add_vec : forall ('n : Int) ('ord : Order). + (vector('n, 'ord, bit), vector('n, 'ord, bit)) -> vector('n, 'ord, bit) -overload (deinfix +) [add_vec] +overload operator + = {add_vec} -val (bit[32], bit[32]) -> unit effect pure test +val test : (vector(32, dec, bit), vector(32, dec, bit)) -> unit -function test (x, y) = -{ - let (bit[64]) z = EXTS(x) + EXTS(y) in - () -} +function test (x, y) = let z : vector(64, dec, bit) = EXTS(x) + EXTS(y) in () diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail index 4d662a8d..7e5c873a 100644 --- a/test/typecheck/pass/add_vec_lit.sail +++ b/test/typecheck/pass/add_vec_lit.sail @@ -1,10 +1,14 @@ default Order inc -val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure add_vec = "add_vec" -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add_range" +val add_vec = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). + (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit) -val cast forall Num 'n. bit['n] -> [|0: 2** 'n - 1|] effect pure unsigned +val add_range = {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -overload (deinfix +) [add_vec; add_range] +val cast unsigned : forall ('n : Int). + vector('n, inc, bit) -> range(0, 2 ^ 'n - 1) -let (range<0,30>) x = 0xF + 0x2 +overload operator + = {add_vec, add_range} + +let x : range(0, 30) = 0xF + 0x2 diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail index f711a5ad..078beb4a 100644 --- a/test/typecheck/pass/arm_FPEXC1.sail +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -1,53 +1,51 @@ default Order dec -val extern forall Num 'n. (bit['n], int) -> bit effect pure vector_access = "bitvector_access_dec" - -val extern forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1. - (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "bitvector_subrange_dec" - -register vector<32 - 1, 32, dec, bit> _FPEXC32_EL2 - -val vector<32 - 1, 32, dec, bit> -> unit effect {wreg} set_FPEXC32_EL2 - -function set_FPEXC32_EL2 value_name = - { - _FPEXC32_EL2[0..0] := [value_name[0]]; - _FPEXC32_EL2[1..1] := [value_name[1]]; - _FPEXC32_EL2[2..2] := [value_name[2]]; - _FPEXC32_EL2[3..3] := [value_name[3]]; - _FPEXC32_EL2[4..4] := [value_name[4]]; - _FPEXC32_EL2[6..5] := value_name[6 .. 5]; - _FPEXC32_EL2[7..7] := [value_name[7]]; - _FPEXC32_EL2[20..11] := value_name[20 .. 11]; - _FPEXC32_EL2[29..29] := [value_name[29]]; - _FPEXC32_EL2[30..30] := [value_name[30]] - } - -val unit -> vector<32 - 1, 32, dec, bit> effect {rreg} get_FPEXC32_EL2 - -function get_FPEXC32_EL2 () = - { - (vector<32 - 1, 32, dec, bit> ) value_name := 0x04000700; - value_name[0..0] := [_FPEXC32_EL2[0]]; - value_name[1..1] := [_FPEXC32_EL2[1]]; - value_name[2..2] := [_FPEXC32_EL2[2]]; - value_name[3..3] := [_FPEXC32_EL2[3]]; - value_name[4..4] := [_FPEXC32_EL2[4]]; - value_name[6..5] := _FPEXC32_EL2[6 .. 5]; - value_name[7..7] := [_FPEXC32_EL2[7]]; - value_name[20..11] := _FPEXC32_EL2[20 .. 11]; - value_name[26..26] := [_FPEXC32_EL2[26]]; - value_name[29..29] := [_FPEXC32_EL2[29]]; - value_name[30..30] := [_FPEXC32_EL2[30]]; - value_name - } - -val vector<32 - 1, 32, dec, bit> -> unit effect {rreg, wreg} set_FPEXC - -function set_FPEXC val_name = - { - (vector<32 - 1, 32, dec, bit> ) r := val_name; - (vector<32 - 1, 32, dec, bit> ) __tmp_45 := get_FPEXC32_EL2(); - __tmp_45[31..0] := r; - set_FPEXC32_EL2(__tmp_45) - } +val vector_access = {ocaml: "bitvector_access_dec", lem: "bitvector_access_dec"}: forall ('n : Int). + (vector('n, dec, bit), int) -> bit + +val vector_subrange = {ocaml: "bitvector_subrange_dec", lem: "bitvector_subrange_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1. + (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit) + +register _FPEXC32_EL2 : vector(32, dec, bit) + +val set_FPEXC32_EL2 : vector(32, dec, bit) -> unit effect {wreg} + +function set_FPEXC32_EL2 value_name = { + _FPEXC32_EL2[0 .. 0] = [value_name[0]]; + _FPEXC32_EL2[1 .. 1] = [value_name[1]]; + _FPEXC32_EL2[2 .. 2] = [value_name[2]]; + _FPEXC32_EL2[3 .. 3] = [value_name[3]]; + _FPEXC32_EL2[4 .. 4] = [value_name[4]]; + _FPEXC32_EL2[6 .. 5] = value_name[6 .. 5]; + _FPEXC32_EL2[7 .. 7] = [value_name[7]]; + _FPEXC32_EL2[20 .. 11] = value_name[20 .. 11]; + _FPEXC32_EL2[29 .. 29] = [value_name[29]]; + _FPEXC32_EL2[30 .. 30] = [value_name[30]] +} + +val get_FPEXC32_EL2 : unit -> vector(32, dec, bit) effect {rreg} + +function get_FPEXC32_EL2 () = { + value_name : vector(32, dec, bit) = 0x04000700; + value_name[0 .. 0] = [_FPEXC32_EL2[0]]; + value_name[1 .. 1] = [_FPEXC32_EL2[1]]; + value_name[2 .. 2] = [_FPEXC32_EL2[2]]; + value_name[3 .. 3] = [_FPEXC32_EL2[3]]; + value_name[4 .. 4] = [_FPEXC32_EL2[4]]; + value_name[6 .. 5] = _FPEXC32_EL2[6 .. 5]; + value_name[7 .. 7] = [_FPEXC32_EL2[7]]; + value_name[20 .. 11] = _FPEXC32_EL2[20 .. 11]; + value_name[26 .. 26] = [_FPEXC32_EL2[26]]; + value_name[29 .. 29] = [_FPEXC32_EL2[29]]; + value_name[30 .. 30] = [_FPEXC32_EL2[30]]; + value_name +} + +val set_FPEXC : vector(32, dec, bit) -> unit effect {rreg, wreg} + +function set_FPEXC val_name = { + r : vector(32, dec, bit) = val_name; + __tmp_45 : vector(32, dec, bit) = get_FPEXC32_EL2(); + __tmp_45[31 .. 0] = r; + set_FPEXC32_EL2(__tmp_45) +} diff --git a/test/typecheck/pass/arm_types.sail b/test/typecheck/pass/arm_types.sail index d7244beb..83cc8687 100644 --- a/test/typecheck/pass/arm_types.sail +++ b/test/typecheck/pass/arm_types.sail @@ -1,140 +1,151 @@ +enum boolean = {FALSE, TRUE} -typedef boolean = enumerate {FALSE; TRUE} +enum signal = {LOW, HIGH} -typedef signal = enumerate {LOW; HIGH} +enum __RetCode = { + __RC_OK, + __RC_UNDEFINED, + __RC_UNPREDICTABLE, + __RC_SEE, + __RC_IMPLEMENTATION_DEFINED, + __RC_SUBARCHITECTURE_DEFINED, + __RC_EXCEPTION_TAKEN, + __RC_ASSERT_FAILED, + __RC_UNMATCHED_CASE +} -typedef __RetCode = - enumerate {__RC_OK; - __RC_UNDEFINED; - __RC_UNPREDICTABLE; - __RC_SEE; - __RC_IMPLEMENTATION_DEFINED; - __RC_SUBARCHITECTURE_DEFINED; - __RC_EXCEPTION_TAKEN; - __RC_ASSERT_FAILED; - __RC_UNMATCHED_CASE} +type TUBE_Type = vector(32, inc, bit) -typedef TUBE_Type = bit[32] +type ScheduleIRQ_Type = vector(32, inc, bit) -typedef ScheduleIRQ_Type = bit[32] +type ClearIRQ_Type = vector(32, inc, bit) -typedef ClearIRQ_Type = bit[32] +type ScheduleFIQ_Type = vector(32, inc, bit) -typedef ScheduleFIQ_Type = bit[32] +type ClearFIQ_Type = vector(32, inc, bit) -typedef ClearFIQ_Type = bit[32] +type TargetCPU_Type = vector(32, inc, bit) -typedef TargetCPU_Type = bit[32] +type AbortRgn64Lo1_Type = vector(32, inc, bit) -typedef AbortRgn64Lo1_Type = bit[32] +type AbortRgn64Lo1_Hi_Type = vector(32, inc, bit) -typedef AbortRgn64Lo1_Hi_Type = bit[32] +type AbortRgn64Hi1_Type = vector(32, inc, bit) -typedef AbortRgn64Hi1_Type = bit[32] +type AbortRgn64Hi1_Hi_Type = vector(32, inc, bit) -typedef AbortRgn64Hi1_Hi_Type = bit[32] +type AbortRgn64Lo2_Type = vector(32, inc, bit) -typedef AbortRgn64Lo2_Type = bit[32] +type AbortRgn64Lo2_Hi_Type = vector(32, inc, bit) -typedef AbortRgn64Lo2_Hi_Type = bit[32] +type AbortRgn64Hi2_Type = vector(32, inc, bit) -typedef AbortRgn64Hi2_Type = bit[32] +type AbortRgn64Hi2_Hi_Type = vector(32, inc, bit) -typedef AbortRgn64Hi2_Hi_Type = bit[32] +type AXIAbortCtl_Type = vector(32, inc, bit) -typedef AXIAbortCtl_Type = bit[32] +type GTE_API_Type = vector(32, inc, bit) -typedef GTE_API_Type = bit[32] +type GTE_API_PARAM_Type = vector(32, inc, bit) -typedef GTE_API_PARAM_Type = bit[32] +type GTE_API_STATUS_Type = vector(32, inc, bit) -typedef GTE_API_STATUS_Type = bit[32] +type PPURBAR_Type = vector(32, inc, bit) -typedef PPURBAR_Type = bit[32] +type PPURSER_Type = vector(32, inc, bit) -typedef PPURSER_Type = bit[32] +type PPURACR_Type = vector(32, inc, bit) -typedef PPURACR_Type = bit[32] +type GTE_API_STATUS_64_Type = vector(32, inc, bit) -typedef GTE_API_STATUS_64_Type = bit[32] +type GTE_API_STATUS_64_HI_Type = vector(32, inc, bit) -typedef GTE_API_STATUS_64_HI_Type = bit[32] +type GTE_API_PARAM_64_Type = vector(32, inc, bit) -typedef GTE_API_PARAM_64_Type = bit[32] +type GTE_API_PARAM_64_HI_Type = vector(32, inc, bit) -typedef GTE_API_PARAM_64_HI_Type = bit[32] +enum MemAtomicOp = { + MemAtomicOp_ADD, + MemAtomicOp_BIC, + MemAtomicOp_EOR, + MemAtomicOp_ORR, + MemAtomicOp_SMAX, + MemAtomicOp_SMIN, + MemAtomicOp_UMAX, + MemAtomicOp_UMIN, + MemAtomicOp_SWP +} -typedef MemAtomicOp = - enumerate {MemAtomicOp_ADD; - MemAtomicOp_BIC; - MemAtomicOp_EOR; - MemAtomicOp_ORR; - MemAtomicOp_SMAX; - MemAtomicOp_SMIN; - MemAtomicOp_UMAX; - MemAtomicOp_UMIN; - MemAtomicOp_SWP} +type SCRType = vector(32, inc, bit) -typedef SCRType = bit[32] +type SCTLRType = vector(32, inc, bit) -typedef SCTLRType = bit[32] +type MAIRType = vector(64, inc, bit) -typedef MAIRType = bit[64] +type ESRType = vector(32, inc, bit) -typedef ESRType = bit[32] +type FPCRType = vector(32, inc, bit) -typedef FPCRType = bit[32] +type FPSRType = vector(32, inc, bit) -typedef FPSRType = bit[32] +type FPSCRType = vector(32, inc, bit) -typedef FPSCRType = bit[32] +type CPSRType = vector(32, inc, bit) -typedef CPSRType = bit[32] +type APSRType = vector(32, inc, bit) -typedef APSRType = bit[32] +type ITSTATEType = vector(8, inc, bit) -typedef ITSTATEType = bit[8] +type CPACRType = vector(32, inc, bit) -typedef CPACRType = bit[32] +type CNTKCTLType = vector(32, inc, bit) -typedef CNTKCTLType = bit[32] +enum GTEParamType = {GTEParam_WORD, GTEParam_LIST, GTEParam_EOACCESS} -typedef GTEParamType = enumerate {GTEParam_WORD; GTEParam_LIST; GTEParam_EOACCESS} +type GTE_PPU_SizeEn_Type = vector(32, inc, bit) -typedef GTE_PPU_SizeEn_Type = bit[32] +type GTEExtObsAccess_Type = vector(16, inc, bit) -typedef GTEExtObsAccess_Type = bit[16] +type GTEASAccess_Type = vector(32, inc, bit) -typedef GTEASAccess_Type = bit[32] +type GTEASRecordedAccess_Type = vector(32, inc, bit) -typedef GTEASRecordedAccess_Type = bit[32] +enum AccType = { + AccType_NORMAL, + AccType_VEC, + AccType_STREAM, + AccType_VECSTREAM, + AccType_ATOMIC, + AccType_ORDERED, + AccType_UNPRIV, + AccType_IFETCH, + AccType_PTW, + AccType_DC, + AccType_IC, + AccType_DCZVA, + AccType_AT +} -typedef AccType = - enumerate {AccType_NORMAL; - AccType_VEC; - AccType_STREAM; - AccType_VECSTREAM; - AccType_ATOMIC; - AccType_ORDERED; - AccType_UNPRIV; - AccType_IFETCH; - AccType_PTW; - AccType_DC; - AccType_IC; - AccType_DCZVA; - AccType_AT} +enum MemType = {MemType_Normal, MemType_Device} -typedef MemType = enumerate {MemType_Normal; MemType_Device} +enum DeviceType = { + DeviceType_GRE, + DeviceType_nGRE, + DeviceType_nGnRE, + DeviceType_nGnRnE +} -typedef DeviceType = - enumerate {DeviceType_GRE; DeviceType_nGRE; DeviceType_nGnRE; DeviceType_nGnRnE} +struct MemAttrHints = { + attrs : vector(2, inc, bit), + hints : vector(2, inc, bit), + transient : bool +} -typedef MemAttrHints = const struct {bit[2] attrs; bit[2] hints; bool transient;} - -typedef MemoryAttributes = - const struct {MemType type; - DeviceType device; - MemAttrHints inner; - MemAttrHints outer; - bool shareable; - bool outershareable;} +struct MemoryAttributes = { + typ : MemType, + device : DeviceType, + inner : MemAttrHints, + outer : MemAttrHints, + shareable : bool, + outershareable : bool +} diff --git a/test/typecheck/pass/as_pattern.sail b/test/typecheck/pass/as_pattern.sail index a1cd9461..25e5fb2d 100644 --- a/test/typecheck/pass/as_pattern.sail +++ b/test/typecheck/pass/as_pattern.sail @@ -1,7 +1,3 @@ +val test : int -> int -val int -> int effect pure test - -function test ((int) _ as x) = -{ - x -} +function test _ : int as x = x diff --git a/test/typecheck/pass/assignment_simple.sail b/test/typecheck/pass/assignment_simple.sail index dc0c78d8..45125636 100644 --- a/test/typecheck/pass/assignment_simple.sail +++ b/test/typecheck/pass/assignment_simple.sail @@ -1,16 +1,14 @@ +val f : (atom(10), unit) -> atom(10) -val ([:10:], unit) -> [:10:] effect pure f +function f (x, y) = x -function [:10:] f (x, y) = x +val test : unit -> atom(10) -val unit -> [:10:] effect pure test - -function [:10:] test () = -{ - z := 10; +function test () = { + z = 10; z } -val unit -> unit effect pure test2 +val test2 : unit -> unit -function unit test2 () = x := 10
\ No newline at end of file +function test2 () = x = 10 diff --git a/test/typecheck/pass/atomcase.sail b/test/typecheck/pass/atomcase.sail index 18840867..2ed00a13 100644 --- a/test/typecheck/pass/atomcase.sail +++ b/test/typecheck/pass/atomcase.sail @@ -1,18 +1,20 @@ default Order dec -val extern forall Num 'n, Num 'm. (atom<'n>, atom<'m>) -> bool effect pure eq_atom -overload (deinfix ==) [eq_atom] +infix 4 == -val forall 'n, 'n in {8,16}. [:'n:] -> int effect pure test_fn -val forall 'n, 'n in {8,16}. [:'n:] -> int effect pure test_switch +val eq_atom = {ocaml: "eq_atom", lem: "eq_atom"}: forall ('n : Int) ('m : Int). + (atom('n), atom('m)) -> bool + +overload operator == = {eq_atom} + +val test_fn : forall 'n, 'n in {8, 16}. atom('n) -> int + +val test_switch : forall 'n, 'n in {8, 16}. atom('n) -> int function test_fn 8 = 8 and test_fn 16 = 16 - -function test_switch n = - switch(n) { - case 8 -> 8 - case 16 -> 16 - } - +function test_switch n = match n { + 8 => 8, + 16 => 16 +} diff --git a/test/typecheck/pass/bitwise_not.sail b/test/typecheck/pass/bitwise_not.sail index 1c4f8d3b..4bd29229 100644 --- a/test/typecheck/pass/bitwise_not.sail +++ b/test/typecheck/pass/bitwise_not.sail @@ -1,7 +1,8 @@ -val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not +val bitwise_not : forall ('m : Int) ('o : Order). + vector('m, 'o, bit) -> vector('m, 'o, bit) default Order dec - -val bit[5] -> bit[5] effect pure test - -function bit[5] test ((bit[5]) x) = bitwise_not(x)
\ No newline at end of file + +val test : vector(5, dec, bit) -> vector(5, dec, bit) + +function test x : vector(5, dec, bit) = bitwise_not(x) diff --git a/test/typecheck/pass/bitwise_not_gen.sail b/test/typecheck/pass/bitwise_not_gen.sail index 6d36c566..8b4c1de4 100644 --- a/test/typecheck/pass/bitwise_not_gen.sail +++ b/test/typecheck/pass/bitwise_not_gen.sail @@ -1,8 +1,9 @@ - -val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not +val bitwise_not : forall ('m : Int) ('o : Order). + vector('m, 'o, bit) -> vector('m, 'o, bit) default Order dec -val forall 'n. bit['n] -> bit['n] effect pure test +val test : forall 'n. + vector('n, dec, bit) -> vector('n, dec, bit) -function forall 'n. bit['n] test ((bit['n]) x) = bitwise_not(bitwise_not(x)) +function test x : vector('n, dec, bit) = bitwise_not(bitwise_not(x)) diff --git a/test/typecheck/pass/bitwise_not_x3.sail b/test/typecheck/pass/bitwise_not_x3.sail index 49d962a6..404e605f 100644 --- a/test/typecheck/pass/bitwise_not_x3.sail +++ b/test/typecheck/pass/bitwise_not_x3.sail @@ -1,7 +1,8 @@ -val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not +val bitwise_not : forall ('n : Int) ('o : Order). + vector('n, 'o, bit) -> vector('n, 'o, bit) default Order dec - -val bit[5] -> bit[5] effect pure test - -function bit[5] test ((bit[5]) x) = bitwise_not(bitwise_not(bitwise_not(x)))
\ No newline at end of file + +val test : vector(5, dec, bit) -> vector(5, dec, bit) + +function test x : vector(5, dec, bit) = bitwise_not(bitwise_not(bitwise_not(x))) diff --git a/test/typecheck/pass/bv_simple_index.sail b/test/typecheck/pass/bv_simple_index.sail deleted file mode 100644 index 811b3a5b..00000000 --- a/test/typecheck/pass/bv_simple_index.sail +++ /dev/null @@ -1,11 +0,0 @@ -val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec -val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc - -overload vector_access [bitvector_access_inc; bitvector_access_dec] - -val cast bit -> bool effect pure cast_bit_bool - -function bool bv ((bit[64]) x) = -{ - x[32] -} diff --git a/test/typecheck/pass/bv_simple_index_bit.sail b/test/typecheck/pass/bv_simple_index_bit.sail index 46bc19d6..ecaebbf5 100644 --- a/test/typecheck/pass/bv_simple_index_bit.sail +++ b/test/typecheck/pass/bv_simple_index_bit.sail @@ -1,9 +1,11 @@ -val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec -val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc +val bitvector_access_dec : forall ('n : Int), 'n >= 0. + (vector('n, dec, bit), range(0, 'n - 1)) -> bit -overload vector_access [bitvector_access_inc; bitvector_access_dec] +val bitvector_access_inc : forall ('n : Int), 'n >= 0. + (vector('n, inc, bit), range(0, 'n - 1)) -> bit -function bit bv ((bit[64]) x) = -{ - x[32] -} +overload vector_access = {bitvector_access_inc, bitvector_access_dec} + +val bv : vector(64, inc, bit) -> bit + +function bv x = x[32] diff --git a/test/typecheck/pass/case_simple1.sail b/test/typecheck/pass/case_simple1.sail index e4a81a36..dad3f99e 100644 --- a/test/typecheck/pass/case_simple1.sail +++ b/test/typecheck/pass/case_simple1.sail @@ -1,9 +1,3 @@ +val case_test : forall ('N : Int). (atom(10), range(10, 'N)) -> range(10, 'N) -val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test - -function forall Nat 'N. [|10:'N|] case_test (x, y) = -{ - switch (x, y) { - case _ -> y - } -} +function case_test (x, y) = match (x, y) {_ => y} diff --git a/test/typecheck/pass/case_simple2.sail b/test/typecheck/pass/case_simple2.sail index 0ffba780..9d41ebb4 100644 --- a/test/typecheck/pass/case_simple2.sail +++ b/test/typecheck/pass/case_simple2.sail @@ -1,9 +1,4 @@ +val case_test : forall ('N : Int), 'N >= 10. + (atom(10), range(10, 'N)) -> range(10, 'N) -val forall Nat 'N, 'N >= 10. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test - -function forall Nat 'N. [|10:'N|] case_test (x, y) = -{ - switch (x, y) { - case _ -> x - } -} +function case_test (x, y) = match (x, y) {_ => x} diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail index 335e10ee..4ac0fec4 100644 --- a/test/typecheck/pass/case_simple_constraints.sail +++ b/test/typecheck/pass/case_simple_constraints.sail @@ -1,18 +1,17 @@ +val plus = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int). + (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) -val extern forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus = "add" +val minus_ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n <= -10. + atom('n) -> atom('n) -val extern forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id = "id" +val ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n >= 10. + atom('n) -> atom('n) -val extern forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id = "id" +val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - switch x { - case ([|10:30|]) y -> y - case ([:31:]) _ -> sizeof 'N - case ([|31:40|]) _ -> plus(60,3) - } +function branch x = match x { + y : range(10, 30) => y, + _ : atom(31) => 'N, + _ : range(31, 40) => plus(60, 3) } -and branch (([|51:63|]) _) = ten_id(sizeof 'N) +and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/cast_lexp1.sail b/test/typecheck/pass/cast_lexp1.sail index b8b29b87..32ba267a 100644 --- a/test/typecheck/pass/cast_lexp1.sail +++ b/test/typecheck/pass/cast_lexp1.sail @@ -1,7 +1,6 @@ +val test : unit -> int -val unit -> int effect pure test - -function int test () = { - (int) y := 10; +function test () = { + y : int = 10; y } diff --git a/test/typecheck/pass/cast_lexp2.sail b/test/typecheck/pass/cast_lexp2.sail index a6f6d299..6eefcf41 100644 --- a/test/typecheck/pass/cast_lexp2.sail +++ b/test/typecheck/pass/cast_lexp2.sail @@ -1,7 +1,6 @@ +val test : unit -> int -val unit -> int effect pure test - -function int test () = { - (nat) y := 10; +function test () = { + y : nat = 10; y } diff --git a/test/typecheck/pass/cast_simple.sail b/test/typecheck/pass/cast_simple.sail index c1507f26..3ff4410d 100644 --- a/test/typecheck/pass/cast_simple.sail +++ b/test/typecheck/pass/cast_simple.sail @@ -1,7 +1,6 @@ +val test : unit -> int -val unit -> int effect pure test - -function int test () = { - (nat) y := ([|0:10|]) 10; - (int) y +function test () = { + y : nat = 10 : range(0, 10); + y : int } diff --git a/test/typecheck/pass/cons_pattern.sail b/test/typecheck/pass/cons_pattern.sail index 107bd6d5..2cc510c5 100644 --- a/test/typecheck/pass/cons_pattern.sail +++ b/test/typecheck/pass/cons_pattern.sail @@ -1,8 +1,6 @@ +val test : list(bit) -> unit -function unit test ((list<bit>) xs) = -{ - switch xs { - case x :: xs -> () - case [||||] -> () - } +function test xs = match xs { + x :: xs => (), + [||] => () } diff --git a/test/typecheck/pass/cons_pattern_synonym.sail b/test/typecheck/pass/cons_pattern_synonym.sail index f5b26294..dcc8e2c5 100644 --- a/test/typecheck/pass/cons_pattern_synonym.sail +++ b/test/typecheck/pass/cons_pattern_synonym.sail @@ -1,7 +1,8 @@ -typedef ty = list<(bit[8])> +type ty = list(vector(8, inc, bit)) -function bool foo ((ty) l) = - switch l { - case _ :: _ -> false - case _ -> true - }
\ No newline at end of file +val foo : ty -> bool + +function foo l = match l { + _ :: _ => false, + _ => true +} diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail index 8fc7c00e..991cd828 100644 --- a/test/typecheck/pass/deinfix_plus.sail +++ b/test/typecheck/pass/deinfix_plus.sail @@ -1,12 +1,10 @@ default Order inc -val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec" - -overload (deinfix +) [bv_add] +val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). + (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit) -val (bit[3], bit[3]) -> bit[3] effect pure test +overload operator + = {bv_add} -function bit[3] test (x, y) = -{ - x + y -} +val test : (vector(3, inc, bit), vector(3, inc, bit)) -> vector(3, inc, bit) + +function test (x, y) = x + y diff --git a/test/typecheck/pass/ex_cast.sail b/test/typecheck/pass/ex_cast.sail index 964bfa72..01716135 100644 --- a/test/typecheck/pass/ex_cast.sail +++ b/test/typecheck/pass/ex_cast.sail @@ -1,12 +1,9 @@ - default Order dec -val cast int -> exist 'n. [:'n:] effect pure ex_int +val cast ex_int : int -> {'n, true. atom('n)} -val forall 'n. [:'n:] -> bit['n] effect pure zeros +val zeros : forall 'n. atom('n) -> vector('n, dec, bit) -val int -> unit effect pure test +val test : int -> unit -function test n = { - x := zeros(n) -} +function test n = x = zeros(n) diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail index 1239fa44..ffa6d033 100644 --- a/test/typecheck/pass/exint.sail +++ b/test/typecheck/pass/exint.sail @@ -1,22 +1,21 @@ +type MyInt = {'n, true. atom('n)} -typedef Int = exist 'n. [:'n:] +val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n + 'm. atom('o)} -val forall 'n, 'm. ([:'n:], [:'m:]) -> exist 'o, 'o = 'n + 'm. [:'o:] effect pure add +val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n * 'm. atom('o)} -val forall 'n, 'm. ([:'n:], [:'m:]) -> exist 'o, 'o = 'n * 'm. [:'o:] effect pure mult +overload operator + = {add} -overload (deinfix +) [add] - -overload (deinfix * ) [mult] +overload operator * = {mult} let x = 3 + 4 let y = x + x * x -let ([:7 * 8:]) z = y +let z : atom(7 * 8) = y -typedef Range = forall Num 'n, Num 'm, 'n <= 'm. exist 'o, 'n <= 'o & 'o <= 'm. [:'o:] +type Range ('n : Int) ('m : Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)} -let (Range<3,4>) a = 3 +let a : Range(3, 4) = 3 -let (Range<2,5>) b = a + 1
\ No newline at end of file +let b : Range(2, 5) = a + 1 diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail index 31968f36..f6c0c073 100644 --- a/test/typecheck/pass/exist1.sail +++ b/test/typecheck/pass/exist1.sail @@ -1,30 +1,27 @@ +let v1 : {|0, 1|} = 0 -let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 +val test : bool -> {|0, 1|} -val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test +function test flag = if flag then 0 else 1 -function test flag = -{ - if flag then 0 else 1 -} +let v2 : range(0, 1) = test(true) -let ([|0:1|]) v2 = test(true) +val add : forall 'a 'b. (atom('a), atom('b)) -> atom('a + 'b) -val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add +let v3 : {|3, 4|} = 3 -let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 - -let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 +let v4 : {'q, 'q in {0, 1}. atom('q + 3)} = v3 let v5 = add(test(true), 4) -let ([:4:]) v6 = 4 +let v6 : atom(4) = 4 -function unit unit_fn (([:4:]) x) = () +val unit_fn : atom(4) -> unit -val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add +function unit_fn x : atom(4) = () -let (exist 'k, 'k = 4. [:'k:]) v7 = 4 +val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a) -let v8 = s_add(v7, 4) +let v7 : {'k, 'k = 4. atom('k)} = 4 +let v8 = s_add(v7, 4) diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail index 04ccb57b..42ec8cb1 100644 --- a/test/typecheck/pass/exist2.sail +++ b/test/typecheck/pass/exist2.sail @@ -1,46 +1,44 @@ +let v1 : {|0, 1|} = 0 -let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 +val test : bool -> {|0, 1|} -val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test +function test flag = if flag then 0 else 1 -function test flag = -{ - if flag then 0 else 1 -} +let v2 : range(0, 1) = test(true) -let ([|0:1|]) v2 = test(true) +val add : forall 'a 'b. (atom('a), atom('b)) -> atom('a + 'b) -val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add +let v3 : {|3, 4|} = 3 -let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 - -let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 +let v4 : {'q, 'q in {0, 1}. atom('q + 3)} = v3 let v5 = add(test(true), 4) -let ([:4:]) v6 = 4 +let v6 : atom(4) = 4 + +val unit_fn : atom(4) -> unit -function unit unit_fn (([:4:]) x) = () +function unit_fn x : atom(4) = () -val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add +val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a) -let (exist 'k, 'k = 4. [:'k:]) v7 = 4 +let v7 : {'k, 'k = 4. atom('k)} = 4 -(* let v8 = s_add(test(true), 4) *) +let v9 : {'n, 0 = 0. atom('n)} = 100 -let (exist 'n, 0 = 0. [:'n:]) v9 = 100 +let v10 : int = v9 -let (int) v10 = v9 +type MyInt = {'n, 0 = 0. atom('n)} -typedef Int = exist 'n, 0 = 0. [:'n:] +val existential_int : int -> MyInt -val int -> Int effect pure existential_int -val forall 'n, 'm. range<'n,'m> -> exist 'e, 'n <= 'e & 'e <= 'm. [:'e:] effect pure existential_range +val existential_range : forall 'n 'm. + range('n, 'm) -> {'e, 'n <= 'e & 'e <= 'm. atom('e)} -overload existential [existential_int; existential_range] +overload existential = {existential_int, existential_range} -let (exist 'n, 0 = 0. [:'n:]) v11 = existential(v10) +let v11 : {'n, 0 = 0. atom('n)} = existential(v10) -let (exist 'e, 0 <= 'e & 'e <= 3. [:'e:]) v12 = existential(([|0:3|]) 2) +let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = existential(2 : range(0, 3)) -let (Int) v13 = existential(v10) +let v13 : MyInt = existential(v10) diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index 4561074a..7d125d23 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -1,42 +1,52 @@ default Order inc -register nat n -register nat x -register nat y +infix 4 == -val (int, int) -> bool effect pure eq_int +register n : nat -overload (deinfix ==) [eq_int] +register x : nat -typedef wordsize = exist 'n, 'n IN {8,16,32}. [|'n|] -let (wordsize) word = ([|8|]) 8 +register y : nat -function nat main () = { +val eq_int : (int, int) -> bool - (* works - x and y are set to 42 *) - n := 1; - y := - (switch n { - case 0 -> { x := 21; x } - case 1 -> { x := 42; x } - case z -> { x := 99; x } - }); +overload operator == = {eq_int} - switch word { - case ([|8|]) 8 -> { x:= 32; } - case ([|16|]) 16 -> { x:= 64; } - case ([|32|]) 32 -> { x:= 128; } - }; +type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)} - switch 0b010101 { - case (0b01:(bit[1]) _:0b101) -> n:= 42 - case _ -> n:=0 - }; +let word : wordsize = 8 : range(0, 8) + +val main : unit -> int effect {wreg, rreg} - n := 3; - switch n { - case 0 -> { 21 } - case 1 -> { 42 } - case u -> { 99 } +function main () = { + n = 1; + y = match n { + 0 => { + x = 21; + x + }, + 1 => { + x = 42; + x + }, + z => { + x = 99; + x + } + }; + match word { + 8 : range(0, 8) => x = 32, + 16 : range(0, 16) => x = 64, + 32 : range(0, 32) => x = 128 + }; + match 0b010101 { + 0b01 @ _ : vector(1, inc, bit) @ 0b101 => n = 42, + _ => n = 0 }; + n = 3; + match n { + 0 => 21, + 1 => 42, + u => 99 + } } diff --git a/test/typecheck/pass/exist_simple.sail b/test/typecheck/pass/exist_simple.sail index 87e62b13..80d689f4 100644 --- a/test/typecheck/pass/exist_simple.sail +++ b/test/typecheck/pass/exist_simple.sail @@ -1,15 +1,9 @@ +register reg : bool -register bool reg +let A : {'n, 0 <= 'n & 'n <= 4. atom('n)} = 4 -let (exist 'n, 0 <= 'n & 'n <= 4. [:'n:]) A = 4 +let B : range(0, 4) = A -let ([|0:4|]) B = A +val test : unit -> {|0, 1|} effect {rreg} -val unit -> exist 'n, 'n in {0, 1}. [:'n:] effect {rreg} test - -function test () = -{ - if reg - then 0 - else 1 -} +function test () = if reg then 0 else 1 diff --git a/test/typecheck/pass/exist_subrange.sail b/test/typecheck/pass/exist_subrange.sail index de867b75..41f0e09b 100644 --- a/test/typecheck/pass/exist_subrange.sail +++ b/test/typecheck/pass/exist_subrange.sail @@ -1,12 +1,13 @@ default Order dec -val forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). - (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange +val vector_subrange : forall ('n : Int) ('m : Int) ('o : Int). + (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit) -function unit test ((bit[6]) xs) = -{ - (int) len := 4; - (exist 'n. [:'n:]) len := 5; - ys := xs[len .. 0]; +val test : vector(6, dec, bit) -> unit + +function test xs = { + len : int = 4; + len : {'n, true. atom('n)} = 5; + ys = xs[len .. 0]; () } diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail index 525d29c6..f1b79b3d 100644 --- a/test/typecheck/pass/exist_tlb.sail +++ b/test/typecheck/pass/exist_tlb.sail @@ -1,94 +1,103 @@ +val extz : forall ('n : Int) ('m : Int) ('ord : Order). + vector('n, 'ord, bit) -> vector('m, 'ord, bit) -(* Minimal prelude *) +val exts : forall ('n : Int) ('m : Int) ('ord : Order). + vector('n, 'ord, bit) -> vector('m, 'ord, bit) -val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. - vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz +overload EXTZ = {extz} -val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. - vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts +overload EXTS = {exts} -overload EXTZ [extz] -overload EXTS [exts] +val add_vec : forall ('n : Int) ('ord : Order). + (vector('n, 'ord, bit), vector('n, 'ord, bit)) -> vector('n, 'ord, bit) -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec +overload operator + = {add_vec} -overload (deinfix +) [add_vec] +val bool_not : bool -> bool -val bool -> bool effect pure bool_not -overload ~ [bool_not] - -(* MIPS spec subset *) +overload ~ = {bool_not} default Order dec -register (bit[1]) CP0LLBit -register (bit[64]) CP0LLAddr +register CP0LLBit : vector(1, dec, bit) + +register CP0LLAddr : vector(64, dec, bit) + +enum MemAccessType = {Instruction, LoadData, StoreData} + +type regno = vector(5, dec, bit) + +type imm16 = vector(16, dec, bit) + +enum Exception = { + EInt, + TLBMod, + TLBL, + TLBS, + AdEL, + AdES, + Sys, + Bp, + ResI, + CpU, + Ov, + Tr, + C2E, + C2Trap, + XTLBRefillL, + XTLBRefillS, + XTLBInvL, + XTLBInvS, + MCheck +} + +enum WordType = {B, H, W, D} + +val rGPR : vector(5, dec, bit) -> vector(64, dec, bit) effect {rreg} -typedef MemAccessType = enumerate {Instruction; LoadData; StoreData} +val isAddressAligned : (vector(64, dec, bit), WordType) -> bool -typedef regno = bit[5] (* a register number *) -typedef imm16 = bit[16] (* 16-bit immediate *) +val SignalExceptionBadAddr : forall ('o : Type). + (Exception, vector(64, dec, bit)) -> 'o -typedef Exception = enumerate -{ - Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap; - XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck +val wordWidthBytes : WordType -> {|1, 2, 4, 8|} + +function wordWidthBytes w = match w { + B => 1, + H => 2, + W => 4, + D => 8 } -typedef WordType = enumerate {B; H; W; D} +val MEMr_reserve_wrapper : forall ('n : Int). + (vector(64, dec, bit), atom('n)) -> vector(8 * 'n, dec, bit) effect {rmem} -val bit[5] -> bit[64] effect {rreg} rGPR -val (bit[64], WordType) -> bool effect pure isAddressAligned -val forall Type 'o. (Exception, bit[64]) -> 'o effect pure SignalExceptionBadAddr +val MEMr_wrapper : forall ('n : Int). + (vector(64, dec, bit), atom('n)) -> vector(8 * 'n, dec, bit) effect {rmem} -val WordType -> exist 'r, 'r in {1,2,4,8}. [:'r:] effect pure wordWidthBytes +val wGPR : (vector(5, dec, bit), vector(64, dec, bit)) -> unit effect {wreg} -function wordWidthBytes w = switch w { - case B -> 1 - case H -> 2 - case W -> 4 - case D -> 8 -} +val addrWrapper : (vector(64, dec, bit), MemAccessType, WordType) -> vector(64, dec, bit) -val forall Nat 'n. (bit[64], [:'n:]) -> bit[8 * 'n] effect {rmem} MEMr_reserve_wrapper -val forall Nat 'n. (bit[64], [:'n:]) -> bit[8 * 'n] effect {rmem} MEMr_wrapper -val (bit[5], bit[64]) -> unit effect {wreg} wGPR - -function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = addr - -function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = vAddr - -scattered typedef ast = const union - -val ast -> unit effect {rmem, rreg, wreg} execute - -scattered function unit execute - -union ast member (WordType, bool, bool, regno, regno, imm16) Load - -function clause execute (Load(width, signed, linked, base, rt, offset)) = - { - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, width); - if ~ (isAddressAligned(vAddr, width)) then - (SignalExceptionBadAddr(AdEL, vAddr)) (* unaligned access *) - else - let pAddr = (TLBTranslate(vAddr, LoadData)) in - { - (exist 't, 't in {1,2,4,8}. bit[8 * 't]) memResult := if linked then - { - CP0LLBit := 0b1; - CP0LLAddr := pAddr; - MEMr_reserve_wrapper(pAddr, wordWidthBytes(width)); - } - else - MEMr_wrapper(pAddr, wordWidthBytes(width)); - if (signed) then - wGPR(rt) := EXTS(memResult) - else - wGPR(rt) := EXTZ(memResult) - } - } +function addrWrapper (addr : vector(64, dec, bit), accessType : MemAccessType, width : WordType) = addr -end ast -end execute +val TLBTranslate : (vector(64, dec, bit), MemAccessType) -> vector(64, dec, bit) + +function TLBTranslate (vAddr : vector(64, dec, bit), accessType : MemAccessType) = vAddr + +union ast = {Load : (WordType, bool, bool, regno, regno, imm16)} + +val execute : ast -> unit effect {rmem, rreg, wreg} + +function execute Load(width, signed, linked, base, rt, offset) = { + vAddr : vector(64, dec, bit) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width); + if ~(isAddressAligned(vAddr, width)) then SignalExceptionBadAddr(AdEL, vAddr) else let pAddr = TLBTranslate(vAddr, LoadData) in { + memResult : {'t, 't in {1, 2, 4, 8}. vector(8 * 't, dec, bit)} = if linked then { + CP0LLBit = 0b1; + CP0LLAddr = pAddr; + MEMr_reserve_wrapper(pAddr, wordWidthBytes(width)) + } else MEMr_wrapper(pAddr, wordWidthBytes(width)); + if signed then wGPR(rt) = EXTS(memResult) + else wGPR(rt) = EXTZ(memResult) + } +} diff --git a/test/typecheck/pass/exist_true.sail b/test/typecheck/pass/exist_true.sail index a30fb87b..25d4a57f 100644 --- a/test/typecheck/pass/exist_true.sail +++ b/test/typecheck/pass/exist_true.sail @@ -1,7 +1,7 @@ +val test : unit -> unit -function unit test () = -{ - (exist 'n. [:'n:]) x := 4; - (exist 'n, true. [:'n:]) y := 5; +function test () = { + x : {'n, true. atom('n)} = 4; + y : {'n, true. atom('n)} = 5; () } diff --git a/test/typecheck/pass/exit1.sail b/test/typecheck/pass/exit1.sail index 92515c5a..ac7ea680 100644 --- a/test/typecheck/pass/exit1.sail +++ b/test/typecheck/pass/exit1.sail @@ -1,8 +1,6 @@ +val test : unit -> atom(6) effect {escape} -val unit -> [:6:] effect {escape} test - -function [:6:] test () = -{ - exit (); +function test () = { + exit(()); 6 } diff --git a/test/typecheck/pass/exit2.sail b/test/typecheck/pass/exit2.sail index 574302cc..a73c6d70 100644 --- a/test/typecheck/pass/exit2.sail +++ b/test/typecheck/pass/exit2.sail @@ -1,7 +1,3 @@ +val test : unit -> atom(6) effect {escape} -val unit -> [:6:] effect {escape} test - -function [:6:] test () = -{ - exit (); -} +function test () = exit(()) diff --git a/test/typecheck/pass/exit3.sail b/test/typecheck/pass/exit3.sail index e26ff95c..e3d0e328 100644 --- a/test/typecheck/pass/exit3.sail +++ b/test/typecheck/pass/exit3.sail @@ -1,7 +1,3 @@ +val test : forall ('a : Type). unit -> 'a effect {escape} -val forall Type 'a. unit -> 'a effect {escape} test - -function forall Type 'a. 'a test () = -{ - exit (); -} +function test () = exit(()) diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail index ddeefd53..95f9a854 100644 --- a/test/typecheck/pass/flow_gt1.sail +++ b/test/typecheck/pass/flow_gt1.sail @@ -1,28 +1,47 @@ default Order inc -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" - -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x > 31) - then x - 32 - else x + 32 -} +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +overload operator + = {add_range} + +overload operator - = {sub_range} + +overload operator < = {lt_atom_range, lt_range_atom} + +overload operator <= = {lteq_atom_range, lteq_range_atom} + +overload operator > = {gt_atom_range, gt_range_atom} + +overload operator >= = {gteq_atom_range, gteq_range_atom} + +val branch : range(0, 63) -> range(0, 63) + +function branch x = if x > 31 then x - 32 else x + 32 diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail index 47f7aa0f..d644ce40 100644 --- a/test/typecheck/pass/flow_gteq1.sail +++ b/test/typecheck/pass/flow_gteq1.sail @@ -1,28 +1,47 @@ default Order inc -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" - -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x >= 32) - then x - 32 - else x + 32 -} +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +overload operator + = {add_range} + +overload operator - = {sub_range} + +overload operator < = {lt_atom_range, lt_range_atom} + +overload operator <= = {lteq_atom_range, lteq_range_atom} + +overload operator > = {gt_atom_range, gt_range_atom} + +overload operator >= = {gteq_atom_range, gteq_range_atom} + +val branch : range(0, 63) -> range(0, 63) + +function branch x = if x >= 32 then x - 32 else x + 32 diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail index c210ed7a..569ec3aa 100644 --- a/test/typecheck/pass/flow_lt1.sail +++ b/test/typecheck/pass/flow_lt1.sail @@ -1,25 +1,41 @@ default Order inc -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" - -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x < 32) - then x + 32 - else x - 32 -} +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +overload operator + = {add_range} + +overload operator - = {sub_range} + +overload operator < = {lt_atom_range, lt_range_atom} + +val branch : range(0, 63) -> range(0, 63) + +function branch x = if x < 32 then x + 32 else x - 32 diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail index cccebaa3..d5b5cfd0 100644 --- a/test/typecheck/pass/flow_lt2.sail +++ b/test/typecheck/pass/flow_lt2.sail @@ -1,25 +1,41 @@ default Order inc -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" - -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x < 32) - then x + 2 - else x - 2 -} +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +overload operator + = {add_range} + +overload operator - = {sub_range} + +overload operator < = {lt_atom_range, lt_range_atom} + +val branch : range(0, 63) -> range(0, 63) + +function branch x = if x < 32 then x + 2 else x - 2 diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail index 9601f48f..40c09c8e 100644 --- a/test/typecheck/pass/flow_lt_assign.sail +++ b/test/typecheck/pass/flow_lt_assign.sail @@ -1,29 +1,47 @@ default Order inc -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" - -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - y := x; - if (y < 32) - then { - y := 31; +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +overload operator + = {add_range} + +overload operator - = {sub_range} + +overload operator < = {lt_atom_range, lt_range_atom} + +val branch : range(0, 63) -> range(0, 63) + +function branch x = { + y = x; + if y < 32 then { + y = 31; y + 32 - } - else y - 32 + } else y - 32 } diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail index ffa4dd8b..90c4fb17 100644 --- a/test/typecheck/pass/flow_lteq1.sail +++ b/test/typecheck/pass/flow_lteq1.sail @@ -1,28 +1,45 @@ default Order inc -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" - -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" - -overload (deinfix +) [add_range] -overload (deinfix -) [sub_range] -overload (deinfix <) [lt_atom_range; lt_range_atom] -overload (deinfix <=) [lteq_atom_range; lteq_range_atom] -overload (deinfix >) [gt_atom_range; gt_range_atom] -overload (deinfix >=) [gteq_atom_range; gteq_range_atom] - -function ([|63|]) branch (([|63|]) x) = -{ - if (x <= 32) - then x + 31 - else x - 33 -} +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). + (atom('n), range('m, 'o)) -> bool + +overload operator + = {add_range} + +overload operator - = {sub_range} + +overload operator < = {lt_atom_range, lt_range_atom} + +overload operator <= = {lteq_atom_range, lteq_range_atom} + +overload operator > = {gt_atom_range, gt_range_atom} + +overload operator >= = {gteq_atom_range, gteq_range_atom} + +function branch x : range(0, 63) -> range(0, 63) = if x <= 32 then x + 31 else x - 33 diff --git a/test/typecheck/pass/foreach_var_updates.sail b/test/typecheck/pass/foreach_var_updates.sail index e3e30ce6..19d491d0 100644 --- a/test/typecheck/pass/foreach_var_updates.sail +++ b/test/typecheck/pass/foreach_var_updates.sail @@ -1,15 +1,17 @@ -val extern (int, int) -> int effect pure add_int = "add" -overload (deinfix +) [ add_int ] - -val extern (int, int) -> int effect pure sub_int = "sub" -overload (deinfix -) [ sub_int ] - -function (int) foo ((int) w) = { - (int) x := w; - (int) y := w; - foreach (z from 0 to 10) { - x := x + z; - y := y - z; +val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int + +overload operator + = {add_int} + +val sub_int = {ocaml: "sub", lem: "sub"}: (int, int) -> int + +overload operator - = {sub_int} + +function foo w : int -> int = { + x : int = w; + y : int = w; + foreach (z from 0 to 10 by 1 in inc) { + x = x + z; + y = y - z }; - x + y; + x + y } diff --git a/test/typecheck/pass/fun_simple_constraints1.sail b/test/typecheck/pass/fun_simple_constraints1.sail index 7fd502b0..2731c2b9 100644 --- a/test/typecheck/pass/fun_simple_constraints1.sail +++ b/test/typecheck/pass/fun_simple_constraints1.sail @@ -1,18 +1,15 @@ +val plus : forall ('n : Int) ('m : Int). + (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus +val minus_ten_id : forall ('n : Int), 'n <= -10. atom('n) -> atom('n) -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id +val ten_id : forall ('n : Int), 'n >= 10. atom('n) -> atom('n) -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id +val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) -and branch (([|51:63|]) _) = ten_id(sizeof 'N)
\ No newline at end of file +function branch x = x +and branch y : range(10, 30) = y +and branch _ : atom(31) = 'N +and branch _ : range(31, 40) = plus(60, 3) +and branch _ : range(41, 50) = plus('N, minus_ten_id(-53)) +and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/fun_simple_constraints2.sail b/test/typecheck/pass/fun_simple_constraints2.sail index 338ef8e8..b6c4eef5 100644 --- a/test/typecheck/pass/fun_simple_constraints2.sail +++ b/test/typecheck/pass/fun_simple_constraints2.sail @@ -1,18 +1,15 @@ +val plus : forall ('n : Int) ('m : Int). + (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus +val minus_ten_id : forall ('n : Int), 'n <= -10. range('n, 'n) -> atom('n) -val forall Nat 'n, 'n <= -10. [|'n:'n|] -> [:'n:] effect pure minus_ten_id +val ten_id : forall ('n : Int), 'n >= 10. atom('n) -> atom('n) -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id +val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) -val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch - -function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = -{ - x -} -and branch (([|10:30|]) y) = y -and branch (([:31:]) _) = sizeof 'N -and branch (([|31:40|]) _) = plus(60,3) -and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) -and branch (([|51:63|]) _) = ten_id(sizeof 'N) +function branch x = x +and branch y : range(10, 30) = y +and branch _ : atom(31) = 'N +and branch _ : range(31, 40) = plus(60, 3) +and branch _ : range(41, 50) = plus('N, minus_ten_id(-53)) +and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail index 2811c428..9fc753e6 100644 --- a/test/typecheck/pass/guards.sail +++ b/test/typecheck/pass/guards.sail @@ -1,22 +1,26 @@ +infix 4 == +infixl 6 / -val (int, int) -> int effect pure add_int -overload (deinfix +) [add_int] +val add_int : (int, int) -> int -val forall Type 'a. ('a, 'a) -> bool effect pure eq -val forall Type 'a. ('a, 'a) -> bool effect pure neq +overload operator + = {add_int} -overload (deinfix ==) [eq] -overload (deinfix !=) [neq] +val eq : forall ('a : Type). ('a, 'a) -> bool -val (int, int) -> int effect pure quotient +val neq : forall ('a : Type). ('a, 'a) -> bool -overload (deinfix quot) [quotient] +overload operator == = {eq} -typedef T = const union { int C1; int C2 } +overload operator != = {neq} -function int test ((int) x, (T) y) = - switch y { - case (C1(z)) when z == 0 -> 0 - case (C1(z)) when z != 0 -> x quot z - case (C2(z)) -> z - } +val quotient : (int, int) -> int + +overload operator / = {quotient} + +union T = {C1 : int, C2 : int} + +function test (x : int, y : T) -> int = match y { + C1(z) if z == 0 => 0, + C1(z) if z != 0 => x / z, + C2(z) => z +} diff --git a/test/typecheck/pass/inline_typ.sail b/test/typecheck/pass/inline_typ.sail new file mode 100644 index 00000000..dd761b83 --- /dev/null +++ b/test/typecheck/pass/inline_typ.sail @@ -0,0 +1,2 @@ + +function test (x : atom('n), y : atom('m)) -> forall 'n 'm. atom('m + 'n) = undefined
\ No newline at end of file diff --git a/test/typecheck/pass/let_subtyp_bug.sail b/test/typecheck/pass/let_subtyp_bug.sail index e2abde2d..106ef710 100644 --- a/test/typecheck/pass/let_subtyp_bug.sail +++ b/test/typecheck/pass/let_subtyp_bug.sail @@ -1,9 +1,5 @@ -let ([|5|]) y = 2 +let y : range(0, 5) = 2 -val unit -> nat effect pure test +val test : unit -> nat -function test() = { - let ([|5|]) x = 2 in - x -} -
\ No newline at end of file +function test () = let x : range(0, 5) = 2 in x diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail deleted file mode 100644 index 321fb315..00000000 --- a/test/typecheck/pass/lexp_memory.sail +++ /dev/null @@ -1,68 +0,0 @@ -default Order dec - -register (bit[64]) GPR00 (* should never be read or written *) -register (bit[64]) GPR01 -register (bit[64]) GPR02 -register (bit[64]) GPR03 -register (bit[64]) GPR04 -register (bit[64]) GPR05 -register (bit[64]) GPR06 -register (bit[64]) GPR07 -register (bit[64]) GPR08 -register (bit[64]) GPR09 -register (bit[64]) GPR10 -register (bit[64]) GPR11 -register (bit[64]) GPR12 -register (bit[64]) GPR13 -register (bit[64]) GPR14 -register (bit[64]) GPR15 -register (bit[64]) GPR16 -register (bit[64]) GPR17 -register (bit[64]) GPR18 -register (bit[64]) GPR19 -register (bit[64]) GPR20 -register (bit[64]) GPR21 -register (bit[64]) GPR22 -register (bit[64]) GPR23 -register (bit[64]) GPR24 -register (bit[64]) GPR25 -register (bit[64]) GPR26 -register (bit[64]) GPR27 -register (bit[64]) GPR28 -register (bit[64]) GPR29 -register (bit[64]) GPR30 -register (bit[64]) GPR31 - -let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = - [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10, - GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20, - GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 - ] - -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc - -overload vector_access [vector_access_inc; vector_access_dec] - -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec - -overload (deinfix ==) [eq_vec] - -val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec - -val cast forall Nat 'n, Nat 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec -function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec i = to_vec_dec (sizeof 'n, sizeof 'l, i) -val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned -val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref - -val (bit[5], bit[64]) -> unit effect {wreg} wGPR - -function unit wGPR (idx, v) = -{ - if idx == 0 then () else GPR[idx] := v -} - -function unit test () = -{ - wGPR(0b00001) := 0 -} diff --git a/test/typecheck/pass/list_cons.sail b/test/typecheck/pass/list_cons.sail index 6f103bf6..c129cbab 100644 --- a/test/typecheck/pass/list_cons.sail +++ b/test/typecheck/pass/list_cons.sail @@ -1 +1 @@ -function list<int> foo ((int) i, (list<int>) l) = i :: l +function foo (i : int, l : list(int)) -> list(int) = i :: l diff --git a/test/typecheck/pass/list_cons2.sail b/test/typecheck/pass/list_cons2.sail index 8c34282b..1eaa9191 100644 --- a/test/typecheck/pass/list_cons2.sail +++ b/test/typecheck/pass/list_cons2.sail @@ -1,7 +1,9 @@ -function list<int> foo ((int) i, (list<int>) l) = i :: l +function foo (i : int, l : list(int)) -> list(int) = i :: l -function list<int> bar () = [||||] +val bar : forall ('a : Type). unit -> list('a) -function list<int> baz ((list<int>) l) = l +function bar () = [||] -function list<int> quux () = baz ([||||]) +function baz l : list(int) -> list(int) = l + +function quux () -> list(int) = baz(bar ()) diff --git a/test/typecheck/pass/list_lit.sail b/test/typecheck/pass/list_lit.sail index d4febadf..a24b4a6f 100644 --- a/test/typecheck/pass/list_lit.sail +++ b/test/typecheck/pass/list_lit.sail @@ -1,2 +1 @@ - -let (list<int>) xs = [||1,2,3,4,5,6||] +let xs : list(int) = [|1, 2, 3, 4, 5, 6|] diff --git a/test/typecheck/pass/mips400.sail b/test/typecheck/pass/mips400.sail deleted file mode 100644 index 951f5126..00000000 --- a/test/typecheck/pass/mips400.sail +++ /dev/null @@ -1,785 +0,0 @@ -(* New typechecker prelude *) - -val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned - -val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed - -val extern forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec = "to_vec_dec" - -val extern forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec = "to_vec_dec" - -(* Vector access can't actually be properly polymorphic on vector - direction because of the ranges being different for each type, so - we overload it instead *) -val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc -val forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec -val forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc - -overload vector_access [bitvector_access_inc; bitvector_access_dec; vector_access_inc; vector_access_dec] - -(* Type safe vector subrange *) -(* vector_subrange(v, m, o) returns the subvector of v with elements with - indices from m up to and *including* o. *) -val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,'a> effect pure vector_subrange_inc - -val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,('m - 'o) + 1,dec,'a> effect pure vector_subrange_dec - -val forall Num 'n, Num 'l, Order 'ord. - (vector<'n,'l,'ord,bit>, int, int) -> list<bit> effect pure vector_subrange_bl - -val forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,bit> effect pure bitvector_subrange_inc - -val forall Num 'n, Num 'l, Num 'm, Num 'o, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,bit>, [:'m:], [:'o:]) -> vector<'m,('m - 'o) + 1,dec,bit> effect pure bitvector_subrange_dec - -overload vector_subrange [bitvector_subrange_inc; bitvector_subrange_dec; vector_subrange_inc; vector_subrange_dec; vector_subrange_bl] - -(* Type safe vector append *) -val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append = "vector_concat" - -val (list<bit>, list<bit>) -> list<bit> effect pure list_append - -val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvec_append = "bitvector_concat" - -overload vector_append [bitvec_append; vec_append; list_append] - -(* Implicit register dereferencing *) -val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref - -(* Bitvector duplication *) -val forall Num 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate - -val (bit, int) -> list<bit> effect pure duplicate_to_list - -val forall Num 'n, Num 'm, Num 'o, Order 'ord. - (vector<'o,'n,'ord,bit>, [:'m:]) -> vector<'o,'m*'n,'ord,bit> effect pure duplicate_bits - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o,'n,'ord,bit>, int) -> list<bit> effect pure duplicate_bits_to_list - -overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_bits_to_list] - -(* Bitvector extension *) -val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. - vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz - -val forall Num 'm, Num 'p, Order 'ord. - list<bit> -> vector<'p, 'm, 'ord, bit> effect pure extz_bl - -val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. - vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts - -val forall Num 'm, Num 'p, Order 'ord. - list<bit> -> vector<'p, 'm, 'ord, bit> effect pure exts_bl - -(* If we want an automatic bitvector extension, then this is the function to - use, but I've disabled the cast because it hides signedness bugs. *) -val (*cast*) forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n. - vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extzi - -overload EXTZ [extz; extz_bl] -overload EXTS [exts; exts_bl] - -val forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o. - vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask - -(* Adjust the start index of a decreasing bitvector *) -val cast forall Num 'n, Num 'm, 'n >= 'm - 1. - vector<'n,'m,dec,bit> -> vector<'m - 1,'m,dec,bit> - effect pure norm_dec - -val cast forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1. - vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> - effect pure adjust_dec - -(* Various casts from 0 and 1 to bitvectors *) -val cast forall Num 'n, Num 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec -val cast forall Num 'n, Num 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec -val cast forall Num 'n, Num 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec - -val cast forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool -val cast bit -> bool effect pure cast_bit_bool - -val cast forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. bit -> vector<'n,'m,dec,bit> effect pure cast_bit_vec - -(* MSB *) -val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant - -(* Arithmetic *) - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. - ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add - -val extern (nat, nat) -> nat effect pure add_nat = "add" - -val extern (int, int) -> int effect pure add_int = "add" - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. - ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub - -val extern (int, int) -> int effect pure sub_int = "sub" - -val forall Num 'n, Num 'm, Order 'ord. - (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_vec_int - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure sub_vec - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure sub_underflow_vec - -overload (deinfix +) [ - add_vec; - add_overflow_vec; - add_vec_int; - add; - add_nat; - add_int -] - -overload (deinfix -) [ - sub_vec_int; - sub_vec; - sub_underflow_vec; - sub; - sub_int -] - -val extern bool -> bit effect pure bool_to_bit = "bool_to_bitU" - -val (int, int) -> int effect pure mul_int -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_vec - -overload (deinfix * ) [ - mul_vec; - mul_int -] - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_svec - -overload (deinfix *_s) [ - mul_svec -] - -val extern (bool, bool) -> bool effect pure bool_xor - -val extern forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure xor_vec = "bitwise_xor" - -overload (deinfix ^) [ - bool_xor; - xor_vec -] - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftl - -overload (deinfix <<) [ - shiftl -] - -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftr - -overload (deinfix >>) [ - shiftr -] - -(* Boolean operators *) -val extern bool -> bool effect pure bool_not = "not" -val (bool, bool) -> bool effect pure bool_or -val (bool, bool) -> bool effect pure bool_and - -val forall Num 'n, Num 'm, Order 'ord. - vector<'n,'m,'ord,bit> -> vector<'n,'m,'ord,bit> effect pure bitwise_not - -val forall Num 'n, Num 'm, Order 'ord. - (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> vector<'n,'m,'ord,bit> effect pure bitwise_and - -val forall Num 'n, Num 'm, Order 'ord. - (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> vector<'n,'m,'ord,bit> effect pure bitwise_or - -overload ~ [bool_not; bitwise_not] -overload (deinfix &) [bool_and; bitwise_and] -overload (deinfix |) [bool_or; bitwise_or] - -(* Equality *) - -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec - -val forall Type 'a. ('a, 'a) -> bool effect pure eq - -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure neq_vec - -val forall Type 'a. ('a, 'a) -> bool effect pure neq - -function forall Num 'n, Num 'm, Order 'ord. bool neq_vec (v1, v2) = bool_not(eq_vec(v1, v2)) - -overload (deinfix ==) [eq_vec; eq] -overload (deinfix !=) [neq_vec; neq] - -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_vec -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gt_vec -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lteq_vec -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lt_vec - -val extern (int, int) -> bool effect pure gteq_int = "gteq" -val extern (int, int) -> bool effect pure gt_int = "gt" -val extern (int, int) -> bool effect pure lteq_int = "lteq" -val extern (int, int) -> bool effect pure lt_int = "lt" - -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" -val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" - -val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom = "lteq" -val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gteq_atom_atom = "gteq" -val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_atom = "lt" -val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom = "gt" - -overload (deinfix >=) [gteq_atom_atom; gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int] -overload (deinfix >) [gt_atom_atom; gt_vec; gt_int] -overload (deinfix <=) [lteq_atom_atom; lteq_range_atom; lteq_atom_range; lteq_vec; lteq_int] -overload (deinfix <) [lt_atom_atom; lt_vec; lt_int] - -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_svec -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gt_svec -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lteq_svec -val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lt_svec - -overload (deinfix <_s) [lt_svec] -overload (deinfix <=_s) [lteq_svec] -overload (deinfix >_s) [gt_svec] -overload (deinfix >=_s) [gteq_svec] - -val (int, int) -> int effect pure quotient - -overload (deinfix quot) [quotient] - -val (int, int) -> int effect pure modulo - -overload (deinfix mod) [modulo] - -val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vec_length = "length" -val forall Type 'a. list<'a> -> nat effect pure list_length - -val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bvlength" - -overload length [bitvector_length; vector_length; list_length] - -val cast forall Num 'n. [:'n:] -> [|'n|] effect pure upper - -typedef option = const union forall Type 'a. { - None; - 'a Some -} - -(* Mips spec starts here *) - -(*========================================================================*) -(* *) -(* Copyright (c) 2015-2017 Robert M. Norton *) -(* Copyright (c) 2015-2017 Kathyrn Gray *) -(* 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. *) -(*========================================================================*) - -(* mips_prelude.sail: declarations of mips registers, and functions common - to mips instructions (e.g. address translation) *) - -(* bit vectors have indices decreasing from left i.e. msb is highest index *) -default Order dec - -register (bit[64]) PC -register (bit[64]) nextPC - -(* CP0 Registers *) - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -typedef TLBEntryLoReg = register bits [63 : 0] { - 63 : CapS; - 62 : CapL; - 29 .. 6 : PFN; - 5 .. 3 : C; - 2 : D; - 1 : V; - 0 : G; -} - -typedef TLBEntryHiReg = register bits [63 : 0] { - 63 .. 62 : R; - 39 .. 13 : VPN2; - 7 .. 0 : ASID; -} - -typedef ContextReg = register bits [63 : 0] { - 63 .. 23 : PTEBase; - 22 .. 4 : BadVPN2; - (*3 .. 0 : ZR;*) -} - -typedef XContextReg = register bits [63 : 0] { - 63 .. 33: PTEBase; - 32 .. 31: R; - 30 .. 4: BadVPN2; -} - -let ([:64:]) TLBNumEntries = 64 -typedef TLBIndexT = (bit[6]) -let (TLBIndexT) TLBIndexMax = 0b111111 - -let MAX_U64 = unsigned(0xffffffffffffffff) -let MAX_VA = unsigned(0xffffffffff) -let MAX_PA = unsigned(0xfffffffff) - -typedef TLBEntry = register bits [116 : 0] { - 116 .. 101: pagemask; - 100 .. 99 : r ; - 98 .. 72 : vpn2 ; - 71 .. 64 : asid ; - 63 : g ; - 62 : valid ; - 61 : caps1 ; - 60 : capl1 ; - 59 .. 36 : pfn1 ; - 35 .. 33 : c1 ; - 32 : d1 ; - 31 : v1 ; - 30 : caps0 ; - 29 : capl0 ; - 28 .. 5 : pfn0 ; - 4 .. 2 : c0 ; - 1 : d0 ; - 0 : v0 ; -} - -register (bit[1]) TLBProbe -register (TLBIndexT) TLBIndex -register (TLBIndexT) TLBRandom -register (TLBEntryLoReg) TLBEntryLo0 -register (TLBEntryLoReg) TLBEntryLo1 -register (ContextReg) TLBContext -register (bit[16]) TLBPageMask -register (TLBIndexT) TLBWired -register (TLBEntryHiReg) TLBEntryHi -register (XContextReg) TLBXContext - -register (TLBEntry) TLBEntry00 -register (TLBEntry) TLBEntry01 -register (TLBEntry) TLBEntry02 -register (TLBEntry) TLBEntry03 -register (TLBEntry) TLBEntry04 -register (TLBEntry) TLBEntry05 -register (TLBEntry) TLBEntry06 -register (TLBEntry) TLBEntry07 -register (TLBEntry) TLBEntry08 -register (TLBEntry) TLBEntry09 -register (TLBEntry) TLBEntry10 -register (TLBEntry) TLBEntry11 -register (TLBEntry) TLBEntry12 -register (TLBEntry) TLBEntry13 -register (TLBEntry) TLBEntry14 -register (TLBEntry) TLBEntry15 -register (TLBEntry) TLBEntry16 -register (TLBEntry) TLBEntry17 -register (TLBEntry) TLBEntry18 -register (TLBEntry) TLBEntry19 -register (TLBEntry) TLBEntry20 -register (TLBEntry) TLBEntry21 -register (TLBEntry) TLBEntry22 -register (TLBEntry) TLBEntry23 -register (TLBEntry) TLBEntry24 -register (TLBEntry) TLBEntry25 -register (TLBEntry) TLBEntry26 -register (TLBEntry) TLBEntry27 -register (TLBEntry) TLBEntry28 -register (TLBEntry) TLBEntry29 -register (TLBEntry) TLBEntry30 -register (TLBEntry) TLBEntry31 -register (TLBEntry) TLBEntry32 -register (TLBEntry) TLBEntry33 -register (TLBEntry) TLBEntry34 -register (TLBEntry) TLBEntry35 -register (TLBEntry) TLBEntry36 -register (TLBEntry) TLBEntry37 -register (TLBEntry) TLBEntry38 -register (TLBEntry) TLBEntry39 -register (TLBEntry) TLBEntry40 -register (TLBEntry) TLBEntry41 -register (TLBEntry) TLBEntry42 -register (TLBEntry) TLBEntry43 -register (TLBEntry) TLBEntry44 -register (TLBEntry) TLBEntry45 -register (TLBEntry) TLBEntry46 -register (TLBEntry) TLBEntry47 -register (TLBEntry) TLBEntry48 -register (TLBEntry) TLBEntry49 -register (TLBEntry) TLBEntry50 -register (TLBEntry) TLBEntry51 -register (TLBEntry) TLBEntry52 -register (TLBEntry) TLBEntry53 -register (TLBEntry) TLBEntry54 -register (TLBEntry) TLBEntry55 -register (TLBEntry) TLBEntry56 -register (TLBEntry) TLBEntry57 -register (TLBEntry) TLBEntry58 -register (TLBEntry) TLBEntry59 -register (TLBEntry) TLBEntry60 -register (TLBEntry) TLBEntry61 -register (TLBEntry) TLBEntry62 -register (TLBEntry) TLBEntry63 - -let (vector <0, 64, inc, (register<TLBEntry>)>) TLBEntries = [ -TLBEntry00, -TLBEntry01, -TLBEntry02, -TLBEntry03, -TLBEntry04, -TLBEntry05, -TLBEntry06, -TLBEntry07, -TLBEntry08, -TLBEntry09, -TLBEntry10, -TLBEntry11, -TLBEntry12, -TLBEntry13, -TLBEntry14, -TLBEntry15, -TLBEntry16, -TLBEntry17, -TLBEntry18, -TLBEntry19, -TLBEntry20, -TLBEntry21, -TLBEntry22, -TLBEntry23, -TLBEntry24, -TLBEntry25, -TLBEntry26, -TLBEntry27, -TLBEntry28, -TLBEntry29, -TLBEntry30, -TLBEntry31, -TLBEntry32, -TLBEntry33, -TLBEntry34, -TLBEntry35, -TLBEntry36, -TLBEntry37, -TLBEntry38, -TLBEntry39, -TLBEntry40, -TLBEntry41, -TLBEntry42, -TLBEntry43, -TLBEntry44, -TLBEntry45, -TLBEntry46, -TLBEntry47, -TLBEntry48, -TLBEntry49, -TLBEntry50, -TLBEntry51, -TLBEntry52, -TLBEntry53, -TLBEntry54, -TLBEntry55, -TLBEntry56, -TLBEntry57, -TLBEntry58, -TLBEntry59, -TLBEntry60, -TLBEntry61, -TLBEntry62, -TLBEntry63 -] - -register (bit[32]) CP0Compare -register (CauseReg) CP0Cause -register (bit[64]) CP0EPC -register (bit[64]) CP0ErrorEPC -register (bit[1]) CP0LLBit -register (bit[64]) CP0LLAddr -register (bit[64]) CP0BadVAddr -register (bit[32]) CP0Count -register (bit[32]) CP0HWREna -register (bit[64]) CP0UserLocal - -typedef StatusReg = register bits [31:0] { - 31 .. 28 : CU; (* co-processor enable bits *) - (* RP/FR/RE/MX/PX not implemented *) - 22 : BEV; (* use boot exception vectors (initialised to one) *) - (* TS/SR/NMI not implemented *) - 15 .. 8 : IM; (* Interrupt mask *) - 7 : KX; (* kernel 64-bit enable *) - 6 : SX; (* supervisor 64-bit enable *) - 5 : UX; (* user 64-bit enable *) - 4 .. 3 : KSU; (* Processor mode *) - 2 : ERL; (* error level (should be initialised to one, but BERI is different) *) - 1 : EXL; (* exception level *) - 0 : IE; (* interrupt enable *) -} -register (StatusReg) CP0Status - -(* Implementation registers -- not ISA defined *) -register (bit[1]) branchPending (* Set by branch instructions to implement branch delay *) -register (bit[1]) inBranchDelay (* Needs to be set by outside world when in branch delay slot *) -register (bit[64]) delayedPC (* Set by branch instructions to implement branch delay *) - -(* General purpose registers *) - -register (bit[64]) GPR00 (* should never be read or written *) -register (bit[64]) GPR01 -register (bit[64]) GPR02 -register (bit[64]) GPR03 -register (bit[64]) GPR04 -register (bit[64]) GPR05 -register (bit[64]) GPR06 -register (bit[64]) GPR07 -register (bit[64]) GPR08 -register (bit[64]) GPR09 -register (bit[64]) GPR10 -register (bit[64]) GPR11 -register (bit[64]) GPR12 -register (bit[64]) GPR13 -register (bit[64]) GPR14 -register (bit[64]) GPR15 -register (bit[64]) GPR16 -register (bit[64]) GPR17 -register (bit[64]) GPR18 -register (bit[64]) GPR19 -register (bit[64]) GPR20 -register (bit[64]) GPR21 -register (bit[64]) GPR22 -register (bit[64]) GPR23 -register (bit[64]) GPR24 -register (bit[64]) GPR25 -register (bit[64]) GPR26 -register (bit[64]) GPR27 -register (bit[64]) GPR28 -register (bit[64]) GPR29 -register (bit[64]) GPR30 -register (bit[64]) GPR31 - -(* Special registers For MUL/DIV *) -register (bit[64]) HI -register (bit[64]) LO - -let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = - [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10, - GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20, - GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 - ] - -(* JTAG Uart registers *) - -register (bit[8]) UART_WDATA -register (bit[1]) UART_WRITTEN -register (bit[8]) UART_RDATA -register (bit[1]) UART_RVALID - -(* Check whether a given 64-bit vector is a properly sign extended 32-bit word *) -val bit[64] -> bool effect pure NotWordVal -function bool NotWordVal (word) = - (word[31] ^^ 32) != word[63..32] - -(* Read numbered GP reg. (r0 is always zero) *) -val bit[5] -> bit[64] effect {rreg} rGPR -function bit[64] rGPR idx = { - if idx == 0 then 0 else GPR[idx] -} - -(* Write numbered GP reg. (writes to r0 ignored) *) -val (bit[5], bit[64]) -> unit effect {wreg} wGPR -function unit wGPR (idx, v) = { - if idx == 0 then () else GPR[idx] := v -} - -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve -val extern unit -> unit effect { barr } MEM_sync - -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmv } MEMval_conditional - -typedef Exception = enumerate -{ - Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap; - XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck -} - -(* Return the ISA defined code for an exception condition *) -function (bit[5]) ExceptionCode ((Exception) ex) = - switch (ex) - { - case Int -> mask(0x00) (* Interrupt *) - case TLBMod -> mask(0x01) (* TLB modification exception *) - case TLBL -> mask(0x02) (* TLB exception (load or fetch) *) - case TLBS -> mask(0x03) (* TLB exception (store) *) - case AdEL -> mask(0x04) (* Address error (load or fetch) *) - case AdES -> mask(0x05) (* Address error (store) *) - case Sys -> mask(0x08) (* Syscall *) - case Bp -> mask(0x09) (* Breakpoint *) - case ResI -> mask(0x0a) (* Reserved instruction *) - case CpU -> mask(0x0b) (* Coprocessor Unusable *) - case Ov -> mask(0x0c) (* Arithmetic overflow *) - case Tr -> mask(0x0d) (* Trap *) - case C2E -> mask(0x12) (* C2E coprocessor 2 exception *) - case C2Trap -> mask(0x12) (* C2Trap maps to same exception code, different vector *) - case XTLBRefillL -> mask(0x02) - case XTLBRefillS -> mask(0x03) - case XTLBInvL -> mask(0x02) - case XTLBInvS -> mask(0x03) - case MCheck -> mask(0x18) - } - - - -function forall Type 'o. 'o SignalExceptionMIPS ((Exception) ex, (bit[64]) kccBase) = - { - (* Only update EPC and BD if not already in EXL mode *) - if (~ (CP0Status.EXL)) then - { - if (inBranchDelay[0]) then - { - CP0EPC := PC - 4; - CP0Cause.BD := 1; - } - else - { - CP0EPC := PC; - CP0Cause.BD := 0; - } - }; - - (* choose an exception vector to branch to. Some are not supported - e.g. Reset *) - vectorOffset := - if (CP0Status.EXL) then - 0x180 (* Always use common vector if in exception mode already *) - else if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) then - 0x080 - else if (ex == C2Trap) then - 0x280 (* Special vector for CHERI traps *) - else - 0x180; (* Common vector *) - (bit[64]) vectorBase := if CP0Status.BEV then - 0xFFFFFFFFBFC00200 - else - 0xFFFFFFFF80000000; - (* On CHERI we have to subtract KCC.base so that we end up at the - right absolute vector address after indirecting via new PCC *) - nextPC := ((bit[64])(vectorBase + (bit[64])(EXTS(vectorOffset)))) - kccBase; - CP0Cause.ExcCode := ExceptionCode(ex); - CP0Status.EXL := 1; - exit (); - } - -val forall Type 'o . Exception -> 'o effect {escape, rreg, wreg} SignalException - -function forall Type 'o. 'o SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) = - { - CP0BadVAddr := badAddr; - SignalException(ex); - } - -function forall Type 'o. 'o SignalExceptionTLB((Exception) ex, (bit[64]) badAddr) = { - CP0BadVAddr := badAddr; - (TLBContext.BadVPN2) := (badAddr[31..13]); - (TLBXContext.BadVPN2):= (badAddr[39..13]); - (TLBXContext.R) := (badAddr[63..62]); - (TLBEntryHi.R) := (badAddr[63..62]); - (TLBEntryHi.VPN2) := (badAddr[39..13]); - SignalException(ex); -} - -typedef MemAccessType = enumerate {Instruction; LoadData; StoreData} -typedef AccessLevel = enumerate {User; Supervisor; Kernel} - -function AccessLevel getAccessLevel() = - if ((CP0Status.EXL) | (CP0Status.ERL)) then - Kernel - else switch (bit[2]) (CP0Status.KSU) - { - case 0b00 -> Kernel - case 0b01 -> Supervisor - case 0b10 -> User - case _ -> User (* behaviour undefined, assume user *) - } - -function unit checkCP0Access () = - { - let accessLevel = getAccessLevel() in - if ((accessLevel != Kernel) & (~(CP0Status[28] (*CU0*)))) then - { - (CP0Cause.CE) := 0b00; - SignalException(CpU); - } - } - -function forall Type 'o. 'o SignalException ((Exception) ex) = SignalExceptionMIPS(ex, 0x0000000000000000) diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail deleted file mode 100644 index 54ae354f..00000000 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ /dev/null @@ -1,32 +0,0 @@ -val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec -val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec - -val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec - -function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) -function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) - -default Order dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -register (CauseReg) CP0Cause - -val unit -> unit effect {wreg} test - -function unit test () = -{ - CP0Cause.BD := 1 -} diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail deleted file mode 100644 index 2e80f538..00000000 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail +++ /dev/null @@ -1,32 +0,0 @@ -val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec -val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec - -val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec - -function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) -function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) - -default Order dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -register (CauseReg) CP0Cause - -val unit -> unit effect {wreg} test - -function unit test () = -{ - CP0Cause.BD := 0 -} diff --git a/test/typecheck/pass/mips_CP0Cause_access.sail b/test/typecheck/pass/mips_CP0Cause_access.sail deleted file mode 100644 index eb3b9389..00000000 --- a/test/typecheck/pass/mips_CP0Cause_access.sail +++ /dev/null @@ -1,34 +0,0 @@ -(* val forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. - vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> - effect pure ADJUST -*) - -val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec -val extern forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc - -overload vector_access [bitvector_access_inc; bitvector_access_dec] - -default Order dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -register (CauseReg) CP0Cause - -val unit -> bit effect {rreg} test - -function bit test () = -{ - CP0Cause[30] -} diff --git a/test/typecheck/pass/mips_CauseReg1.sail b/test/typecheck/pass/mips_CauseReg1.sail deleted file mode 100644 index b9503efa..00000000 --- a/test/typecheck/pass/mips_CauseReg1.sail +++ /dev/null @@ -1,15 +0,0 @@ -default Order dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/pass/mips_CauseReg2.sail b/test/typecheck/pass/mips_CauseReg2.sail deleted file mode 100644 index 7600c9f1..00000000 --- a/test/typecheck/pass/mips_CauseReg2.sail +++ /dev/null @@ -1,15 +0,0 @@ -default Order dec - -typedef CauseReg = register bits [ 31 : 1 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} diff --git a/test/typecheck/pass/mips_reg_field_bit.sail b/test/typecheck/pass/mips_reg_field_bit.sail deleted file mode 100644 index 4c37a6e9..00000000 --- a/test/typecheck/pass/mips_reg_field_bit.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order dec - -val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. - vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> - effect pure adjust_dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -register (CauseReg) CP0Cause - -val unit -> unit effect {wreg} test - -function unit test () = -{ - (CP0Cause.CE)[28] := bitone -} diff --git a/test/typecheck/pass/mips_reg_field_bv.sail b/test/typecheck/pass/mips_reg_field_bv.sail deleted file mode 100644 index 0ce19b4f..00000000 --- a/test/typecheck/pass/mips_reg_field_bv.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order dec - -val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. - vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> - effect pure adjust_dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -register (CauseReg) CP0Cause - -val unit -> unit effect {wreg} test - -function unit test () = -{ - CP0Cause.CE := 0b11 -} diff --git a/test/typecheck/pass/mips_regtyps.sail b/test/typecheck/pass/mips_regtyps.sail deleted file mode 100644 index f7a3ce91..00000000 --- a/test/typecheck/pass/mips_regtyps.sail +++ /dev/null @@ -1,53 +0,0 @@ - -(* mips_prelude.sail: declarations of mips registers, and functions common - to mips instructions (e.g. address translation) *) - -(* bit vectors have indices decreasing from left i.e. msb is highest index *) -default Order dec - -register (bit[64]) PC -register (bit[64]) nextPC - -(* CP0 Registers *) - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -typedef TLBEntryLoReg = register bits [63 : 0] { - 63 : CapS; - 62 : CapL; - 29 .. 6 : PFN; - 5 .. 3 : C; - 2 : D; - 1 : V; - 0 : G; -} - -typedef TLBEntryHiReg = register bits [63 : 0] { - 63 .. 62 : R; - 39 .. 13 : VPN2; - 7 .. 0 : ASID; -} - -typedef ContextReg = register bits [63 : 0] { - 63 .. 23 : PTEBase; - 22 .. 4 : BadVPN2; - (*3 .. 0 : ZR;*) -} - -typedef XContextReg = register bits [63 : 0] { - 63 .. 33: PTEBase; - 32 .. 31: R; - 30 .. 4: BadVPN2; -} diff --git a/test/typecheck/pass/mips_tlbindext_dec.sail b/test/typecheck/pass/mips_tlbindext_dec.sail deleted file mode 100644 index af98cd85..00000000 --- a/test/typecheck/pass/mips_tlbindext_dec.sail +++ /dev/null @@ -1,5 +0,0 @@ - -default Order dec - -typedef TLBIndexT = (bit[6]) -let (TLBIndexT) TLBIndexMax = 0b111111 diff --git a/test/typecheck/pass/mips_tlbindext_inc.sail b/test/typecheck/pass/mips_tlbindext_inc.sail deleted file mode 100644 index d64ffd68..00000000 --- a/test/typecheck/pass/mips_tlbindext_inc.sail +++ /dev/null @@ -1,5 +0,0 @@ - -default Order inc - -typedef TLBIndexT = (bit[6]) -let (TLBIndexT) TLBIndexMax = 0b111111 diff --git a/test/typecheck/pass/modify_assignment1.sail b/test/typecheck/pass/modify_assignment1.sail index 1c7ab614..f7c54092 100644 --- a/test/typecheck/pass/modify_assignment1.sail +++ b/test/typecheck/pass/modify_assignment1.sail @@ -1,8 +1,6 @@ +val test : unit -> unit -val unit -> unit effect pure test - -function unit test () = -{ - ([|0:10|]) z := 9; - z := ([|0:9|]) 8 -}
\ No newline at end of file +function test () = { + z : range(0, 10) = 9; + z = 8 : range(0, 9) +} diff --git a/test/typecheck/pass/modify_type_chain.sail b/test/typecheck/pass/modify_type_chain.sail index 14651787..1156587a 100644 --- a/test/typecheck/pass/modify_type_chain.sail +++ b/test/typecheck/pass/modify_type_chain.sail @@ -1,8 +1,6 @@ +val test : unit -> unit -val unit -> unit effect pure test - -function unit test () = -{ - ([|0:10|]) z := 9; - ([|0:9|]) z := ([|0:8|]) 8 -}
\ No newline at end of file +function test () = { + z : range(0, 10) = 9; + z : range(0, 9) = 8 : range(0, 8) +} diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail index 46338353..a12e81da 100644 --- a/test/typecheck/pass/nat_set.sail +++ b/test/typecheck/pass/nat_set.sail @@ -1,8 +1,5 @@ - -function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) = -{ - true -} +function test x : atom('n) -> forall 'n. bool = true let x = test(1) -let y = test(3)
\ No newline at end of file + +let y = test(3) diff --git a/test/typecheck/pass/nondet.sail b/test/typecheck/pass/nondet.sail deleted file mode 100644 index 8a353c66..00000000 --- a/test/typecheck/pass/nondet.sail +++ /dev/null @@ -1,12 +0,0 @@ - -register int z - -val unit -> unit effect {wreg} test - -function unit test () = { - nondet { - z := 0; - z := 1; - z := 2; - } -} diff --git a/test/typecheck/pass/nondet_assert.sail b/test/typecheck/pass/nondet_assert.sail deleted file mode 100644 index 501432d3..00000000 --- a/test/typecheck/pass/nondet_assert.sail +++ /dev/null @@ -1,14 +0,0 @@ - -register int z - -val unit -> int effect {wreg, rreg, escape} test - -function int test () = { - nondet { - z := 0; - assert(false, "Nondeterministic assert"); - return z; - z := 1; - }; - z -} diff --git a/test/typecheck/pass/nondet_return.sail b/test/typecheck/pass/nondet_return.sail deleted file mode 100644 index 56fcfd5a..00000000 --- a/test/typecheck/pass/nondet_return.sail +++ /dev/null @@ -1,13 +0,0 @@ - -register int z - -val unit -> int effect {wreg, rreg} test - -function int test () = { - nondet { - z := 0; - return z; - z := 1; - }; - z -} diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail index 3e23e529..e498cded 100644 --- a/test/typecheck/pass/nzcv.sail +++ b/test/typecheck/pass/nzcv.sail @@ -1,13 +1,12 @@ default Order dec -val bit[4] -> unit effect pure test +val test : vector(4, dec, bit) -> unit -function test nzcv = -{ - N := 0b0; - Z := 0b0; - C := 0b0; - V := 0b0; - (N,Z,C,V) := nzcv; +function test nzcv = { + N = 0b0; + Z = 0b0; + C = 0b0; + V = 0b0; + (N, Z, C, V) = nzcv; () } diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail index c466daf4..632b882d 100644 --- a/test/typecheck/pass/option_either.sail +++ b/test/typecheck/pass/option_either.sail @@ -1,33 +1,21 @@ default Order inc -typedef option = const union forall Type 'a. { - None; - 'a Some -} +union option ('a : Type) = {None, Some : 'a} -function forall Type 'a. option<'a> none () = None +function none () -> forall ('a : Type). option('a) = None -function forall Type 'a. option<'a> some (('a) x) = Some(x) +function some x : 'a -> forall ('a : Type). option('a) = Some(x) -function forall Type 'a. int test ((option<'a>) x) = -{ - switch x { - case None -> 0 - case (Some(y)) -> 1 - } +function test x : option('a) -> forall ('a : Type). range(0, 1) = match x { + None => 0, + Some(y) => 1 } -typedef either = const union forall Type 'a, Type 'b. { - 'a Left; - 'b Right -} +union either ('a : Type) ('b : Type) = {Left : 'a, Right : 'b} -val forall Nat 'n, 'n >= 0. bit['n] -> int effect pure signed +val signed : forall ('n : Int), 'n >= 0. vector('n, inc, bit) -> int -function int test2 ((either<int,bit[1]>) x) = -{ - switch x { - case (Left(l)) -> l - case (Right(r)) -> signed(r) - } +function test2 x : either(int, vector(1, inc, bit)) -> int = match x { + Left(l) => l, + Right(r) => signed(r) } diff --git a/test/typecheck/pass/overlap_field.sail b/test/typecheck/pass/overlap_field.sail index 82e685ee..c30cd6d8 100644 --- a/test/typecheck/pass/overlap_field.sail +++ b/test/typecheck/pass/overlap_field.sail @@ -1,13 +1,12 @@ +struct A = {field_A : bool, shared : int} -typedef A = const struct {bool field_A; int shared} -typedef B = const struct {bool field_B; int shared} +struct B = {field_B : bool, shared : int} -val (bool, int) -> A effect {undef} makeA +val makeA : (bool, int) -> A effect {undef} -function makeA (x, y) = -{ - (A) record := undefined; - record.field_A := x; - record.shared := y; +function makeA (x, y) = { + record : A = undefined; + record.field_A = x; + record.shared = y; record } diff --git a/test/typecheck/pass/overload_plus.sail b/test/typecheck/pass/overload_plus.sail index 2aa8ecc5..991cd828 100644 --- a/test/typecheck/pass/overload_plus.sail +++ b/test/typecheck/pass/overload_plus.sail @@ -1,12 +1,10 @@ default Order inc -val extern forall Nat 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec" - -overload (deinfix +) [bv_add] +val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). + (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit) -val (bit[3], bit[3]) -> bit[3] effect pure test +overload operator + = {bv_add} -function bit[3] test (x, y) = -{ - x + y -} +val test : (vector(3, inc, bit), vector(3, inc, bit)) -> vector(3, inc, bit) + +function test (x, y) = x + y diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail index 5a89372a..e1587ebc 100644 --- a/test/typecheck/pass/patternrefinement.sail +++ b/test/typecheck/pass/patternrefinement.sail @@ -1,19 +1,27 @@ default Order dec -val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. - vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz -val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure length -val extern forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec -val extern forall Num 'n, Num 'm. ([:'n:],[:'m:]) -> bool effect pure eq_atom -val extern forall Type 'a. ('a, 'a) -> bool effect pure eq -overload (deinfix ==) [eq_vec; eq_atom; eq] - - -val forall 'n, 'n in {32,64}. bit['n] -> bit[64] effect pure test - -function test(v) = { - switch (length(v)) { - case 32 -> extz(v) - case 64 -> v - } +infix 4 == + +val extz = {ocaml: "extz", lem: "extz"}: forall ('n : Int) ('m : Int) ('ord : Order). + vector('n, 'ord, bit) -> vector('m, 'ord, bit) + +val length = {ocaml: "length", lem: "length"}: forall ('m : Int) ('ord : Order) ('a : Type). + vector('m, 'ord, 'a) -> atom('m) + +val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order). + (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool + +val eq_atom = {ocaml: "eq_atom", lem: "eq_atom"}: forall ('n : Int) ('m : Int). + (atom('n), atom('m)) -> bool + +val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool + +overload operator == = {eq_vec, eq_atom, eq} + +val test : forall 'n, 'n in {32, 64}. + vector('n, dec, bit) -> vector(64, dec, bit) + +function test v = match length(v) { + 32 => extz(v), + 64 => v } diff --git a/test/typecheck/pass/phantom_num.sail b/test/typecheck/pass/phantom_num.sail index c676807d..96663073 100644 --- a/test/typecheck/pass/phantom_num.sail +++ b/test/typecheck/pass/phantom_num.sail @@ -1,17 +1,9 @@ +val gt_int = {ocaml: "gt", lem: "gt"}: (int, int) -> bool -val extern (int, int) -> bool effect pure gt_int = "gt" +overload operator > = {gt_int} -(* val cast forall Num 'n, Num 'm. [|'n:'m|] -> int effect pure cast_range_int *) +register z : int -overload (deinfix >) [gt_int] +val test : forall ('n : Int). unit -> unit effect {wreg} -register int z - -val forall Nat 'n. unit -> unit effect {wreg} test - -function forall Nat 'n. unit test () = -{ - if sizeof 'n > 3 - then z := 0 - else z := 1 -} +function test () = if 'n > 3 then z = 0 else z = 1 diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail index 95ba97db..726f9575 100644 --- a/test/typecheck/pass/procstate1.sail +++ b/test/typecheck/pass/procstate1.sail @@ -1,16 +1,16 @@ default Order dec -typedef ProcState = const struct forall Num 'n. -{ - bit['n] N; - bit[1] Z; - bit[1] C; - bit[1] V -} +infix 4 == -register ProcState<1> PSTATE +val operator == : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool -function unit test () = -{ - PSTATE.N := 0b1 +struct ProcState ('n : Int) = { + N : vector('n, dec, bit), + Z : vector(1, dec, bit), + C : vector(1, dec, bit), + V : vector(1, dec, bit) } + +register PSTATE : ProcState(1) + +function test () -> bool = PSTATE.N == 0b1 diff --git a/test/typecheck/pass/pure_record.sail b/test/typecheck/pass/pure_record.sail index c7bc373a..b56a1a98 100644 --- a/test/typecheck/pass/pure_record.sail +++ b/test/typecheck/pass/pure_record.sail @@ -1,22 +1,22 @@ default Order dec -typedef State = const struct forall Type 'a. { - vector<0, 1, dec, 'a> N; - vector<0, 1, dec, bit> Z; +struct State ('a : Type) = { + N : vector(1, dec, 'a), + Z : vector(1, dec, bit) } -let (State<bit>) myStateM = { - (State<bit>) r := undefined; - r.N := 0b1; - r.Z := 0b1; +let myStateM : State(bit) = { + r : State(bit) = undefined; + r.N = 0b1; + r.Z = 0b1; r } -let (State<bit>) myState = { N = 0b1; Z = 0b1 } +let myState : State(bit) = struct { N = 0b1, Z = 0b1 } -val unit -> unit effect {undef} test +val test : unit -> unit effect {undef} function test () = { - (State<bit>) myState2 := { N = undefined; Z = 0b1 }; - (State<bit>) myState3 := { myState2 with N = 0b0 } + myState2 : State(bit) = struct { N = undefined, Z = 0b1 }; + myState3 : State(bit) = { myState2 with N = 0b0 } } diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail index a0a85313..2ca42541 100644 --- a/test/typecheck/pass/pure_record2.sail +++ b/test/typecheck/pass/pure_record2.sail @@ -1,22 +1,22 @@ default Order dec -typedef State = const struct forall Type 'a, Nat 'n. { - vector<0, 'n, dec, 'a> N; - vector<0, 1, dec, bit> Z; +struct State ('a : Type) ('n : Int) = { + N : vector('n, dec, 'a), + Z : vector(1, dec, bit) } -let (State<bit,1>) myStateM = { - (State<bit,1>) r := undefined; - r.N := 0b1; - r.Z := 0b1; +let myStateM : State(bit, 1) = { + r : State(bit, 1) = undefined; + r.N = 0b1; + r.Z = 0b1; r } -let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } +let myState : State(bit, 1) = struct { N = 0b1, Z = 0b1 } -val unit -> unit effect {undef} test +val test : unit -> unit effect {undef} function test () = { - (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; - (State<bit,1>) myState3 := { myState2 with N = 0b0 } + myState2 : State(bit, 1) = struct { N = undefined, Z = 0b1 }; + myState3 : State(bit, 1) = { myState2 with N = 0b0 } } diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail index 61d74ebf..6db6dc5e 100644 --- a/test/typecheck/pass/pure_record3.sail +++ b/test/typecheck/pass/pure_record3.sail @@ -1,25 +1,25 @@ default Order dec -typedef State = const struct forall Type 'a, Nat 'n. { - vector<0, 'n, dec, 'a> N; - vector<0, 1, dec, bit> Z; +struct State ('a : Type) ('n : Int) = { + N : vector('n, dec, 'a), + Z : vector(1, dec, bit) } -register State<bit,1> procState +register procState : State(bit, 1) -let (State<bit,1>) myStateM = { - (State<bit,1>) r := undefined; - r.N := 0b1; - r.Z := 0b1; +let myStateM : State(bit, 1) = { + r : State(bit, 1) = undefined; + r.N = 0b1; + r.Z = 0b1; r } -let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } +let myState : State(bit, 1) = struct { N = 0b1, Z = 0b1 } -val unit -> unit effect {undef} test +val test : unit -> unit effect {undef} function test () = { - (State<bit,1>) myState1 := undefined; - (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; - (State<bit,1>) myState3 := { myState2 with N = 0b0 } + myState1 : State(bit, 1) = undefined; + myState2 : State(bit, 1) = struct { N = undefined, Z = 0b1 }; + myState3 : State(bit, 1) = { myState2 with N = 0b0 } } diff --git a/test/typecheck/pass/real.sail b/test/typecheck/pass/real.sail index 5ae1456b..509d48b0 100644 --- a/test/typecheck/pass/real.sail +++ b/test/typecheck/pass/real.sail @@ -1,2 +1 @@ - -let (real) r = 2.2 +let r : real = 2.2 diff --git a/test/typecheck/pass/reg_mod.sail b/test/typecheck/pass/reg_mod.sail index 37c8d890..8c0d4d66 100644 --- a/test/typecheck/pass/reg_mod.sail +++ b/test/typecheck/pass/reg_mod.sail @@ -1,11 +1,9 @@ +register reg : range(0, 10) -register [|0:10|] reg +val test : unit -> unit effect {wreg} -val unit -> unit effect {wreg} test - -function unit test () = -{ - reg := 9; - reg := 10; - reg := 8 -}
\ No newline at end of file +function test () = { + reg = 9; + reg = 10; + reg = 8 +} diff --git a/test/typecheck/pass/regtyp_vec.sail b/test/typecheck/pass/regtyp_vec.sail deleted file mode 100644 index 28978882..00000000 --- a/test/typecheck/pass/regtyp_vec.sail +++ /dev/null @@ -1,36 +0,0 @@ -(* val forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. - vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> - effect pure ADJUST -*) - -val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec -(* -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc -*) - -overload vector_access [bitvector_access_dec] - -default Order dec - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -register (CauseReg) CP0Cause - -val unit -> bit effect {rreg} test - -function bit test () = -{ - CP0Cause[30] -} diff --git a/test/typecheck/pass/return_simple1.sail b/test/typecheck/pass/return_simple1.sail index 26e6fc1d..29af9888 100644 --- a/test/typecheck/pass/return_simple1.sail +++ b/test/typecheck/pass/return_simple1.sail @@ -1,8 +1,6 @@ +val return_test : forall ('N : Int). range(10, 'N) -> range(10, 'N) -val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test - -function forall Nat 'N. [|10:'N|] return_test x = -{ - return x; +function return_test x = { + return(x); x } diff --git a/test/typecheck/pass/return_simple2.sail b/test/typecheck/pass/return_simple2.sail index 06ce9757..8753e3f2 100644 --- a/test/typecheck/pass/return_simple2.sail +++ b/test/typecheck/pass/return_simple2.sail @@ -1,11 +1,9 @@ +val return_test : forall ('N : Int). range(10, 'N) -> range(10, 'N) -val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test - -function forall Nat 'N. [|10:'N|] return_test x = -{ - return x; - return x; - return x; - return x; +function return_test x = { + return(x); + return(x); + return(x); + return(x); x } diff --git a/test/typecheck/pass/return_simple3.sail b/test/typecheck/pass/return_simple3.sail index 7e81b5b2..fdda96dc 100644 --- a/test/typecheck/pass/return_simple3.sail +++ b/test/typecheck/pass/return_simple3.sail @@ -1,8 +1,6 @@ +val return_test : forall ('N : Int), 'N >= 10. range(10, 'N) -> range(10, 'N) -val forall Nat 'N, 'N >= 10. [|10:'N|] -> [|10:'N|] effect pure return_test - -function forall Nat 'N, 'N >= 10. [|10:'N|] return_test x = -{ - return x; - sizeof 'N +function return_test x = { + return(x); + 'N } diff --git a/test/typecheck/pass/return_simple4.sail b/test/typecheck/pass/return_simple4.sail index 1bbc0e73..b4909746 100644 --- a/test/typecheck/pass/return_simple4.sail +++ b/test/typecheck/pass/return_simple4.sail @@ -1,7 +1,3 @@ +val return_test : forall ('N : Int). range(10, 'N) -> range(10, 'N) -val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test - -function forall Nat 'N. [|10:'N|] return_test x = -{ - return x -} +function return_test x = return(x) diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail deleted file mode 100644 index af0b5ba2..00000000 --- a/test/typecheck/pass/set_mark.sail +++ /dev/null @@ -1,11 +0,0 @@ - -val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec - -val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec -function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) - -default Order dec - -function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x - -let x = Foo32( (bit[32]) 0) diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail deleted file mode 100644 index 591c17ad..00000000 --- a/test/typecheck/pass/set_mark2.sail +++ /dev/null @@ -1,11 +0,0 @@ - -val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec - -val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec -function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) - -default Order dec - -function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x - -let x = Foo32( (bit[64]) 0) diff --git a/test/typecheck/pass/set_spsr.sail b/test/typecheck/pass/set_spsr.sail deleted file mode 100644 index 7fac206c..00000000 --- a/test/typecheck/pass/set_spsr.sail +++ /dev/null @@ -1,17 +0,0 @@ -default Order dec - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc - -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec - -overload vector_subrange [vector_subrange_inc; vector_subrange_dec] - -register bit[32] SPSR_EL2 - -function unit set_SPSR_hyp (bit[32]) val_name = -{ - (bit[32]) r := val_name; - SPSR_EL2[31..0] := r -} diff --git a/test/typecheck/pass/simple_record_access.sail b/test/typecheck/pass/simple_record_access.sail index d4f4d61f..b1eab652 100644 --- a/test/typecheck/pass/simple_record_access.sail +++ b/test/typecheck/pass/simple_record_access.sail @@ -1,16 +1,11 @@ -typedef signal = enumerate {LOW; HIGH} +enum signal = {LOW, HIGH} -typedef Bit32 = bit[32] +type Bit32 = vector(32, inc, bit) -typedef Record = - const struct {signal rsig; - Bit32 bitfield;} +struct Record = {rsig : signal, bitf : Bit32} -register bit[32] R0 +register R0 : vector(32, inc, bit) -val Record -> unit effect {wreg} test +val test : Record -> unit effect {wreg} -function unit test ((Record) r) = -{ - R0 := r.bitfield; -} +function test r : Record = R0 = r.bitf diff --git a/test/typecheck/pass/simple_scattered.sail b/test/typecheck/pass/simple_scattered.sail index a500cd1f..bb4a1a14 100644 --- a/test/typecheck/pass/simple_scattered.sail +++ b/test/typecheck/pass/simple_scattered.sail @@ -1,22 +1,19 @@ - default Order dec -scattered typedef ast = const union forall Num 'datasize, Num 'destsize, Num 'regsize. +scattered union ast ('datasize : Int) ('destsize : Int) ('regsize : Int) -val forall Num 'datasize, Num 'destsize, Num 'regsize. - ast<'datasize,'destsize,'regsize> -> unit effect pure execute +val execute : forall ('datasize : Int) ('destsize : Int) ('regsize : Int). + ast('datasize, 'destsize, 'regsize) -> unit -scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execute +scattered function execute -union ast member (bit[8], bit['regsize]) test +union clause ast = test : (vector(8, dec, bit), vector('regsize, dec, bit)) -union ast member int test2 +function clause execute test(x, y) = return(()) -function clause execute (test (x, y)) = -{ - return () -} +union clause ast = test2 : int -end ast +function clause execute test2(_) = return(()) end execute +end ast
\ No newline at end of file diff --git a/test/typecheck/pass/simple_scattered2.sail b/test/typecheck/pass/simple_scattered2.sail deleted file mode 100644 index 8cd26e95..00000000 --- a/test/typecheck/pass/simple_scattered2.sail +++ /dev/null @@ -1,27 +0,0 @@ - -default Order dec - -scattered typedef ast = const union forall Num 'datasize, Num 'destsize, Num 'regsize. - -val forall Num 'datasize, Num 'destsize, Num 'regsize. - ast<'datasize,'destsize,'regsize> -> unit effect pure execute - -scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execute - -union ast member (bit[8], bit['regsize]) test - -function clause execute (test (x, y)) = -{ - return () -} - -union ast member int test2 - -function clause execute (test2(x)) = -{ - return () -} - -end ast - -end execute diff --git a/test/typecheck/pass/sizeof_vector_start_index.sail b/test/typecheck/pass/sizeof_vector_start_index.sail deleted file mode 100644 index 6ad8ef06..00000000 --- a/test/typecheck/pass/sizeof_vector_start_index.sail +++ /dev/null @@ -1,12 +0,0 @@ -val forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'n:] effect pure vector_start_index - -function forall Num 'n, Num 'm, Order 'ord, Type 'a. [:'n:] vector_start_index ((vector<'n,'m,'ord,'a>) vec) = -{ - sizeof 'n -} - -function int test ((vector<47,11,dec,bit>) vec) = -{ - vector_start_index(vec) -} - diff --git a/test/typecheck/pass/trycatch.sail b/test/typecheck/pass/trycatch.sail deleted file mode 100644 index b7f97dd0..00000000 --- a/test/typecheck/pass/trycatch.sail +++ /dev/null @@ -1,20 +0,0 @@ - -scattered typedef exception = const union - -union exception member int IntEx - -val unit -> unit effect {escape} test2 - -function test2 () = throw (IntEx(3)) - -val unit -> unit effect {escape} test - -function test () = - try { - test2(); - () - } catch { - case (IntEx(_)) -> () - } - -end exception diff --git a/test/typecheck/pass/union_infer.sail b/test/typecheck/pass/union_infer.sail index 397525e0..15eb5c60 100644 --- a/test/typecheck/pass/union_infer.sail +++ b/test/typecheck/pass/union_infer.sail @@ -1,16 +1,7 @@ - default Order inc -typedef option = const union forall Type 'a. { - None; - 'a Some - } - -typedef Test = const union { - A; - B; - C -} +union option ('a : Type) = {None, Some : 'a} +union Test = {A, B, C} -function option<Test> test () = Some(C) +function test () -> option(Test) = Some(C) diff --git a/test/typecheck/pass/varity.sail b/test/typecheck/pass/varity.sail index 750d70eb..5157c8da 100644 --- a/test/typecheck/pass/varity.sail +++ b/test/typecheck/pass/varity.sail @@ -1,19 +1,21 @@ +val f1 : int -> unit -val int -> unit effect pure f1 -val (int, int) -> unit effect pure f2 -val (int, int, int) -> unit effect pure f3 +val f2 : (int, int) -> unit + +val f3 : (int, int, int) -> unit + +function f1 i1 = () -function f1 (i1) = () function f2 (i1, i2) = () + function f3 (i1, i2, i3) = () -overload f [f1; f2; f3] +overload f = {f1, f2, f3} -val unit -> unit effect pure test +val test : unit -> unit -function test () = -{ +function test () = { f(1); f(2, 3); - f(4, 5, 6); + f(4, 5, 6) } diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail index b22f0029..9376b2a8 100644 --- a/test/typecheck/pass/vec_pat1.sail +++ b/test/typecheck/pass/vec_pat1.sail @@ -1,20 +1,18 @@ default Order inc -val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec" +val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). + (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit) -val extern forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,'o + 1 - 'm,inc,bit> effect pure vector_subrange = "bitvector_subrange_inc" +val vector_subrange = {ocaml: "bitvector_subrange_inc", lem: "bitvector_subrange_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. + (vector('l, inc, bit), atom('m), atom('o)) -> vector('o + 1 - 'm, inc, bit) -val forall Num 'n, Num 'm, Num 'o, Num 'p. - (vector<'n,'m,inc,bit>, vector<'o,'p,inc,bit>) -> vector<'n,'m + 'p,inc,bit> - effect pure bitvector_concat +val bitvector_concat : forall ('m : Int) ('p : Int). + (vector('m, inc, bit), vector('p, inc, bit)) -> vector('m + 'p, inc, bit) -overload (deinfix +) [bv_add] -overload append [bitvector_concat] +overload operator + = {bv_add} -val (bit[3], bit[3]) -> bit[3] effect pure test +overload append = {bitvector_concat} -function bit[3] test (((bit[1]) x : 0b1 : 0b0), z) = -{ - (x : 0b11) + z -} +val test : (vector(3, inc, bit), vector(3, inc, bit)) -> vector(3, inc, bit) + +function test (x : vector(1, inc, bit) @ 0b1 @ 0b0, z) = (x @ 0b11) + z diff --git a/test/typecheck/pass/vector_access.sail b/test/typecheck/pass/vector_access.sail index 4228a62e..2e6ae0d2 100644 --- a/test/typecheck/pass/vector_access.sail +++ b/test/typecheck/pass/vector_access.sail @@ -1,15 +1,16 @@ +val vector_access_dec : forall 'l ('a : Type), 'l >= 0. + (vector('l, dec, 'a), range(0, 'l - 1)) -> 'a -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc +val vector_access_inc : forall ('l : Int) ('a : Type), 'l >= 0. + (vector('l, inc, 'a), range(0, 'l - 1)) -> 'a default Order inc -overload vector_access [vector_access_inc; vector_access_dec] +overload vector_access = {vector_access_inc, vector_access_dec} -val bit[4] -> unit effect pure test - -function unit test v = -{ - z := vector_access(v,3); - z := v[3] -}
\ No newline at end of file +val test : vector(4, inc, bit) -> unit + +function test v = { + z = vector_access(v, 3); + z = v[3] +} diff --git a/test/typecheck/pass/vector_access_dec.sail b/test/typecheck/pass/vector_access_dec.sail index c59100f0..e21d79e5 100644 --- a/test/typecheck/pass/vector_access_dec.sail +++ b/test/typecheck/pass/vector_access_dec.sail @@ -1,15 +1,16 @@ +val vector_access_dec : forall ('l : Int) ('a : Type), 'l >= 0. + (vector('l, dec, 'a), range(0, 'l - 1)) -> 'a -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc +val vector_access_inc : forall ('l : Int) ('a : Type), 'l >= 0. + (vector('l, inc, 'a), range(0, 'l - 1)) -> 'a -overload vector_access [vector_access_inc; vector_access_dec] +overload vector_access = {vector_access_inc, vector_access_dec} default Order dec -val bit[4] -> unit effect pure test - -function unit test v = -{ - z := vector_access(v,3); - z := v[3] -}
\ No newline at end of file +val test : vector(4, dec, bit) -> unit + +function test v = { + z = vector_access(v, 3); + z = v[3] +} diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail index df610fb1..8a1bfae4 100644 --- a/test/typecheck/pass/vector_append.sail +++ b/test/typecheck/pass/vector_append.sail @@ -1,14 +1,12 @@ - -val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure append = "bitvector_concat" +val append = "bitvector_concat" : forall ('l1 : Int) ('l2 : Int) ('o : Order), 'l1 >= 0 & 'l2 >= 0. + (vector('l1, 'o, bit), vector('l2, 'o, bit)) -> vector('l1 + 'l2, 'o, bit) default Order inc -val (bit[4], bit[4]) -> bit[8] effect pure test +val test : (vector(4, inc, bit), vector(4, inc, bit)) -> vector(8, inc, bit) -function bit[8] test (v1, v2) = -{ - zv := append(v1, v2); - zv := v1 : v2; +function test (v1, v2) = { + zv = append(v1, v2); + zv = v1 @ v2; zv } diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail index ce63ed87..6ce5bf90 100644 --- a/test/typecheck/pass/vector_append_gen.sail +++ b/test/typecheck/pass/vector_append_gen.sail @@ -1,12 +1,9 @@ - -val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" +val vector_append = "bitvector_concat": forall 'l1 'l2 ('o : Order), 'l1 >= 0 & 'l2 >= 0. + (vector('l1, 'o, bit), vector('l2, 'o, bit)) -> vector('l1 + 'l2, 'o, bit) default Order inc -val forall 'n, 'm, 'n >= 0, 'm >= 0. (bit['n], bit['m]) -> bit['n + 'm] effect pure test - -function forall 'n, 'm. bit['n + 'm] test (v1, v2) = -{ - vector_append(v1, v2); -} +val test : forall 'n 'm, 'n >= 0 & 'm >= 0. + (vector('n, inc, bit), vector('m, inc, bit)) -> vector('n + 'm, inc, bit) + +function test (v1, v2) = vector_append(v1, v2) diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail index 4ec067de..aff87df4 100644 --- a/test/typecheck/pass/vector_subrange_gen.sail +++ b/test/typecheck/pass/vector_subrange_gen.sail @@ -1,21 +1,21 @@ +val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0. + (vector('l, 'o, 'a), range(0, 'l - 1)) -> 'a -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access +val vector_append : forall ('l1 : Int) ('l2 : Int) ('o : Order) ('a : Type), 'l1 >= 0 & 'l2 >= 0. + (vector('l1, 'o, 'a), vector('l2, 'o, 'a)) -> vector('l1 + 'l2, 'o, 'a) -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append +val vector_subrange = "bitvector_subrange_inc" : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. + (vector('l, inc, bit), atom('m), atom('o)) -> vector('o - 'm + 1, inc, bit) -val extern forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. - (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,bit> effect pure vector_subrange = "bitvector_subrange_inc" - -val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure sub +val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm) default Order inc -val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 1] effect pure test +val test : forall 'n 'm, 'n >= 5. + vector('n, inc, bit) -> vector('n - 1, inc, bit) -function forall 'n, 'n >= 5. bit['n - 1] test v = -{ - z := vector_subrange(v, 0, sub(sizeof 'n, 2)); - z := v[0 .. sub(sizeof 'n, 2)]; +function test v = { + z = vector_subrange(v, 0, sub('n, 2)); + z = v[0 .. sub('n, 2)]; z } diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail deleted file mode 100644 index bd0acaa6..00000000 --- a/test/typecheck/pass/vector_synonym_cast.sail +++ /dev/null @@ -1,8 +0,0 @@ - -typedef vecsyn = vector<0,1,dec,bit> - -val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure norm_dec - -val vector<1,1,dec,bit> -> vecsyn effect pure test - -function test x = x diff --git a/test/typecheck/pass/while_MM.sail b/test/typecheck/pass/while_MM.sail index e6916edd..b416c24a 100644 --- a/test/typecheck/pass/while_MM.sail +++ b/test/typecheck/pass/while_MM.sail @@ -1,23 +1,25 @@ default Order dec -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. - ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add" -val extern (int, int) -> int effect pure add_int = "add" -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int -overload (deinfix +) [add_vec_int; add_range; add_int] +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val extern bool -> bool effect pure bool_not = "not" +val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int -val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,dec,bit> effect pure cast_0_vec_dec +val add_vec_int : forall ('n : Int) ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) -register (bit[64]) COUNT -register (bool) INT +overload operator + = {add_vec_int, add_range, add_int} -function (unit) test () = { - COUNT := 0; - while (bool_not(INT)) do { - COUNT := COUNT + 1; - } -} +val bool_not = {ocaml: "not", lem: "not"}: bool -> bool + +val cast cast_0_vec_dec : forall ('l : Int). + atom(0) -> vector('l, dec, bit) + +register COUNT : vector(64, dec, bit) +register INT : bool + +function test () -> unit = { + COUNT = 0; + while bool_not(INT) do COUNT = COUNT + 1 +} diff --git a/test/typecheck/pass/while_MP.sail b/test/typecheck/pass/while_MP.sail index 05d396e2..60b5fb90 100644 --- a/test/typecheck/pass/while_MP.sail +++ b/test/typecheck/pass/while_MP.sail @@ -1,17 +1,15 @@ default Order dec -val extern (int, int) -> int effect pure add_int = "add" -overload (deinfix +) [add_vec_int; add_range; add_int] +val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int -val extern bool -> bool effect pure bool_not = "not" +overload operator + = {add_vec_int, add_range, add_int} -register (bool) INT +val bool_not = {ocaml: "not", lem: "not"}: bool -> bool -function (int) test () = { - (int) count := 0; - while (bool_not(INT)) do { - count := count + 1; - }; - return count; -} +register INT : bool +function test () -> int = { + count : int = 0; + while bool_not(INT) do count = count + 1; + return(count) +} diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail index b03a87dc..39ecdb2b 100644 --- a/test/typecheck/pass/while_PM.sail +++ b/test/typecheck/pass/while_PM.sail @@ -1,23 +1,28 @@ default Order dec -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern (int, int) -> bool effect pure lt_int = "lt" -overload (deinfix <) [lt_range_atom; lt_int] +val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. - ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add" -val extern (int, int) -> int effect pure add_int = "add" -overload (deinfix +) [add_range; add_int] +val lt_int = {ocaml: "lt", lem: "lt"}: (int, int) -> bool -val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, int) -> bit effect pure vector_access = "bitvector_access_dec" +overload operator < = {lt_range_atom, lt_int} -register (bit[64]) GPR00 +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -function (unit) test ((bit) b) = { - (int) i := 0; - while (i < 64) do { - GPR00[i] := b; - i := i + 1; +val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int + +overload operator + = {add_range, add_int} + +val vector_access = "bitvector_access_dec" : forall ('l : Int), 'l >= 0. + (vector('l, dec, bit), int) -> bit + +register GPR00 : vector(64, dec, bit) + +function test b : bit -> unit = { + i : int = 0; + while i < 64 do { + GPR00[i] = b; + i = i + 1 } } - diff --git a/test/typecheck/pass/while_PP.sail b/test/typecheck/pass/while_PP.sail index 454cc9ac..557bf963 100644 --- a/test/typecheck/pass/while_PP.sail +++ b/test/typecheck/pass/while_PP.sail @@ -1,24 +1,29 @@ default Order dec -val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" -val extern (int, int) -> bool effect pure lt_int = "lt" -overload (deinfix <) [lt_range_atom; lt_int] - -val (int, int) -> int effect pure mult_int -overload (deinfix * ) [mult_int] - -val extern forall Num 'n, Num 'm, Num 'o, Num 'p. - ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add" -val extern (int, int) -> int effect pure add_int = "add" -overload (deinfix +) [add_range; add_int] - -function (int) test ((int) n) = { - (int) i := 1; - (int) j := 1; - while (i < n) do { - j := i * j; - i := i + 1; +val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). + (range('n, 'm), atom('o)) -> bool + +val lt_int = {ocaml: "lt", lem: "lt"}: (int, int) -> bool + +overload operator < = {lt_range_atom, lt_int} + +val mult_int : (int, int) -> int + +overload operator * = {mult_int} + +val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int + +overload operator + = {add_range, add_int} + +function test n : int -> int = { + i : int = 1; + j : int = 1; + while i < n do { + j = i * j; + i = i + 1 }; j } - diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index a2567d21..8da7347f 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -11,19 +11,9 @@ NC='\033[0m' mkdir -p $DIR/rtpass mkdir -p $DIR/rtpass2 -mkdir -p $DIR/lem -mkdir -p $DIR/rtfail rm -f $DIR/tests.xml -MIPS="$SAILDIR/mips_new_tc" - -cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.sail -cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail -cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail -cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_ast_decl.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail -cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb_stub.sail $MIPS/mips_wrappers.sail $MIPS/mips_ast_decl.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_notlb.sail - pass=0 fail=0 @@ -58,7 +48,7 @@ function finish_suite { printf "<testsuites>\n" >> $DIR/tests.xml -for i in `ls $DIR/pass/`; +for i in `ls $DIR/pass/ | grep sail`; do if $SAILDIR/sail -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i; then @@ -80,81 +70,4 @@ done finish_suite "Expecting pass" -for i in `ls $DIR/fail/`; -do - if $SAILDIR/sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i; - then - red "tested $i expecting fail" "pass" - else - if $SAILDIR/sail -dno_cast -dmagic_hash -just_check $DIR/rtfail/$i 2> /dev/null; - then - yellow "tested $i expecting fail" "passed re-check" - else - green "tested $i expecting fail" "fail" - fi - fi -done - -finish_suite "Expecting fail" - -function test_lem { - for i in `ls $DIR/pass/`; - do - # MIPS requires an additional library, Mips_extras_embed. - # It might be useful to allow adding options for specific test cases. - # For now, include the library for all test cases, which doesn't seem to hurt. - if $SAILDIR/sail -lem -lem_lib Mips_extras_embed -lem_sequential -lem_mwords $DIR/$1/$i 2> /dev/null - then - green "generated lem for $1/$i" "pass" - - cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/ - # mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/ - # mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ - # Test sequential embedding for now - # TODO: Add tests for the free monad - if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types_sequential.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null - then - green "typechecking lem for $1/$i" "pass" - else - red "typechecking lem for $1/$i" "fail" - fi - else - red "generated lem for $1/$i" "fail" - red "typechecking lem for $1/$i" "fail" - fi - done -} - -test_lem pass - -finish_suite "Lem generation 1" - -test_lem rtpass - -finish_suite "Lem generation 2" - -# function test_ocaml { -# for i in `ls $DIR/pass/`; -# do -# if $SAILDIR/sail -ocaml $DIR/$1/$i 2> /dev/null -# then -# green "generated ocaml for $1/$i" "pass" - -# rm $SAILDIR/${i%%.*}.ml -# else -# red "generated ocaml for $1/$i" "fail" -# fi -# done -# } - -# test_ocaml pass - -# finish_suite "Ocaml generation 1" - -# test_ocaml rtpass - -# finish_suite "Ocaml generation 2" - printf "</testsuites>\n" >> $DIR/tests.xml |