diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/interpreter.ml | 2 | ||||
| -rw-r--r-- | src/isail.ml | 157 | ||||
| -rw-r--r-- | src/lexer.mll | 8 | ||||
| -rw-r--r-- | src/sail.ml | 5 | ||||
| -rw-r--r-- | src/type_check.ml | 5 |
5 files changed, 120 insertions, 57 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index 3196ee34..e88c5e93 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -488,7 +488,6 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = else failwith ("Could not find variable or register " ^ string_of_id id) - return (exp_of_value (V_ref (string_of_id id))) | E_id id -> begin let open Type_check in @@ -598,7 +597,6 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let values = coerce_tuple (value_of_exp exp) in wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values)) *) - | E_assign _ -> failwith (string_of_exp orig_exp); | E_try (exp, pexps) when is_value exp -> return exp | E_try (exp, pexps) -> diff --git a/src/isail.ml b/src/isail.ml index d8aa55c1..3009aeb3 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -82,13 +82,8 @@ let rec user_input callback = end; user_input callback -let termcode n = "\x1B[" ^ string_of_int n ^ "m" -let bold str = termcode 1 ^ str -let red str = termcode 91 ^ str -let clear str = str ^ termcode 0 - let sail_logo = - let banner str = str |> bold |> red |> clear in + let banner str = str |> Util.bold |> Util.red |> Util.clear in [ {| ___ ___ ___ ___ |}; {| /\ \ /\ \ /\ \ /\__\|}; {| /::\ \ /::\ \ _\:\ \ /:/ /|}; @@ -102,6 +97,8 @@ let sail_logo = let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast) +let interactive_state = ref (initial_state !interactive_ast) + let print_program () = match !current_mode with | Normal -> () @@ -111,8 +108,6 @@ let print_program () = print_endline out | Evaluation _ -> () -let interactive_state = ref (initial_state !interactive_ast) - let rec run () = match !current_mode with | Normal -> () @@ -150,22 +145,42 @@ let rec run_steps n = current_mode := Evaluation frame end -let handle_input input = +type input = Command of string * string | Expression of string | Empty + +(* This function is called on every line of input passed to the interpreter *) +let handle_input' input = LNoise.history_add input |> ignore; - match !current_mode with - | Normal -> - begin - if input <> "" && input.[0] = ':' then - let n = try String.index input ' ' with Not_found -> String.length input in - let cmd = Str.string_before input n in - let arg = String.trim (Str.string_after input n) in + + (* Process the input and check if it's a command, a raw expression, + or empty. *) + let input = + if input <> "" && input.[0] = ':' then + let n = try String.index input ' ' with Not_found -> String.length input in + let cmd = Str.string_before input n in + let arg = String.trim (Str.string_after input n) in + Command (cmd, arg) + else if input <> "" then + Expression input + else + Empty + in + + let recognised = ref true in + + let unrecognised_command cmd = + if !recognised = false then print_endline ("Command " ^ cmd ^ " is not a valid command") else () + in + + (* First handle commands that are mode-independent *) + begin + match input with + | Command (cmd, arg) -> + begin match cmd with | ":t" | ":type" -> let typq, typ = Type_check.Env.get_val_spec (mk_id arg) !interactive_env in pretty_sail stdout (doc_binding (typq, typ)); print_newline (); - | ":elf" -> - Elf_loader.load_elf arg | ":q" | ":quit" -> exit 0 | ":i" | ":infer" -> let exp = Initial_check.exp_of_string dec_ord arg in @@ -175,42 +190,73 @@ let handle_input input = | ":v" | ":verbose" -> Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 3; print_endline ("Verbosity: " ^ string_of_int !Type_check.opt_tc_debug) + | _ -> recognised := false + end + | _ -> () + end; - | _ -> print_endline ("Unrecognised command " ^ input) - else if input <> "" then - let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in - current_mode := Evaluation (eval_frame !interactive_ast (Step ("", !interactive_state, return exp, []))); - print_program () - else () + match !current_mode with + | Normal -> + begin + match input with + | Command (cmd, arg) -> + (* Normal mode commands *) + begin + match cmd with + | ":elf" -> Elf_loader.load_elf arg + | _ -> unrecognised_command cmd + end + | Expression str -> + (* An expression in normal mode is type checked, then puts + us in evaluation mode. *) + let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord str) in + current_mode := Evaluation (eval_frame !interactive_ast (Step ("", !interactive_state, return exp, []))); + print_program () + | Empty -> () end | Evaluation frame -> begin - if input <> "" && input.[0] = ':' then - let n = try String.index input ' ' with Not_found -> String.length input in - let cmd = Str.string_before input n in - let arg = String.trim (Str.string_after input n) in - match cmd with - | ":r" | ":run" -> - run () - | ":s" | ":step" -> - run_steps (int_of_string arg) - | ":q" | ":quit" -> exit 0 - | _ -> print_endline ("Unrecognised command " ^ input) - else - match frame with - | Done (state, v) -> - interactive_state := state; - print_endline ("Result = " ^ Value.string_of_value v); - current_mode := Normal - | Step (out, state, _, stack) -> - interactive_state := state; - current_mode := Evaluation (eval_frame !interactive_ast frame); - print_program () - | Break frame -> - print_endline "Breakpoint"; - current_mode := Evaluation frame + match input with + | Command (cmd, arg) -> + (* Evaluation mode commands *) + begin + match cmd with + | ":r" | ":run" -> + run () + | ":s" | ":step" -> + run_steps (int_of_string arg) + | ":n" | ":normal" -> + current_mode := Normal + | _ -> unrecognised_command cmd + end + | Expression str -> + print_endline "Already evaluating expression" + | Empty -> + (* Empty input will evaluate one step, or switch back to + normal mode when evaluation is completed. *) + begin + match frame with + | Done (state, v) -> + interactive_state := state; + print_endline ("Result = " ^ Value.string_of_value v); + current_mode := Normal + | Step (out, state, _, stack) -> + interactive_state := state; + current_mode := Evaluation (eval_frame !interactive_ast frame); + print_program () + | Break frame -> + print_endline "Breakpoint"; + current_mode := Evaluation frame + end end +let handle_input input = + try handle_input' input with + | Type_check.Type_error (l, err) -> + print_endline (Type_check.string_of_type_error err) + | exn -> + print_endline (Printexc.to_string exn) + let () = (* Auto complete function names based on val specs *) LNoise.set_completion_callback @@ -231,6 +277,21 @@ let () = |> List.map (fun completion -> line_so_far ^ completion) |> List.iter (LNoise.add_completion ln_completions) else () + end; + + (* Read the script file if it is set with the -is option, and excute them *) + begin + match !opt_interactive_script with + | None -> () + | Some file -> + let chan = open_in file in + try + while true do + let line = input_line chan in + handle_input line; + done; + with + | End_of_file -> () end; LNoise.history_load ~filename:"sail_history" |> ignore; diff --git a/src/lexer.mll b/src/lexer.mll index ccbe12a5..d13ba849 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -181,8 +181,8 @@ let kw_table = let ws = [' ''\t']+ let letter = ['a'-'z''A'-'Z''?'] let digit = ['0'-'9'] -let binarydigit = ['0'-'1'] -let hexdigit = ['0'-'9''A'-'F''a'-'f'] +let binarydigit = ['0'-'1''_'] +let hexdigit = ['0'-'9''A'-'F''a'-'f''_'] let alphanum = letter|digit let startident = letter|'_' let ident = alphanum|['_''\'''#'] @@ -260,8 +260,8 @@ rule token = parse | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) } | digit+ as i { (Num(Big_int.of_string i)) } | "-" digit+ as i { (Num(Big_int.of_string i)) } - | "0b" (binarydigit+ as i) { (Bin(i)) } - | "0x" (hexdigit+ as i) { (Hex(i)) } + | "0b" (binarydigit+ as i) { (Bin(Util.string_of_list "" (fun s -> s) (Util.split_on_char '_' i))) } + | "0x" (hexdigit+ as i) { (Hex(Util.string_of_list "" (fun s -> s) (Util.split_on_char '_' i))) } | '"' { (String( string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) } | eof { Eof } diff --git a/src/sail.ml b/src/sail.ml index a5d1de67..c8f30e09 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -53,6 +53,7 @@ open Process_file let lib = ref ([] : string list) let opt_file_out : string option ref = ref None let opt_interactive = ref false +let opt_interactive_script : string option ref = ref None let opt_print_version = ref false let opt_print_initial_env = ref false let opt_print_verbose = ref false @@ -74,6 +75,10 @@ let options = Arg.align ([ ( "-i", Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen], " start interactive interpreter"); + ( "-is", + Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen; + Arg.String (fun s -> opt_interactive_script := Some s)], + "<filename> start interactive interpreter and execute commands in script"); ( "-ocaml", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], " output an OCaml translated version of the input"); diff --git a/src/type_check.ml b/src/type_check.ml index d705c190..01ff8649 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -88,14 +88,13 @@ let pp_type_error err = let rec pp_err = function | Err_no_casts (exp, trigger, []) -> (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp) - ^/^ (string "Failed because" ^//^ pp_err trigger) - ^/^ string "There were no possible casts" + ^^ hardline ^^ (string "Failed because" ^//^ pp_err trigger) | Err_no_casts (exp, trigger, errs) -> (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp) ^/^ string "Failed because" ^//^ pp_err trigger | Err_no_overloading (id, errs) -> string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^ - group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^^ space ^^ pp_err err) errs) + group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^//^ pp_err err) errs) | Err_subtype (typ1, typ2, []) -> separate space [ string (string_of_typ typ1); string "is not a subtype of"; |