summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml1
-rw-r--r--src/initial_check.mli9
-rw-r--r--src/isail.ml17
-rw-r--r--src/lexer.mll2
-rw-r--r--src/parser.mly45
-rw-r--r--src/pretty_print_sail.ml5
-rw-r--r--src/type_check.ml8
7 files changed, 75 insertions, 12 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 ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 04:56:02 +0000