diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | language/l2.ott | 160 | ||||
| -rw-r--r-- | src/Makefile | 5 | ||||
| -rw-r--r-- | src/_tags | 2 | ||||
| -rw-r--r-- | src/initial_check.ml | 4 | ||||
| -rw-r--r-- | src/initial_check.mli | 2 | ||||
| -rw-r--r-- | src/interpreter.ml | 310 | ||||
| -rw-r--r-- | src/isail.ml | 92 | ||||
| -rw-r--r-- | src/myocamlbuild.ml | 2 | ||||
| -rw-r--r-- | src/parser2.mly | 6 | ||||
| -rw-r--r-- | src/pretty_print_sail2.ml | 12 | ||||
| -rw-r--r-- | src/sail.ml | 10 | ||||
| -rw-r--r-- | src/util.ml | 15 | ||||
| -rw-r--r-- | src/util.mli | 11 | ||||
| -rw-r--r-- | src/value.ml | 123 |
15 files changed, 677 insertions, 81 deletions
@@ -6,6 +6,10 @@ sail: $(MAKE) -C src ln -f -s src/sail.native sail +isail: + $(MAKE) -C src isail + ln -f -s src/isail.native sail + language: $(MAKE) -C language diff --git a/language/l2.ott b/language/l2.ott index 02823237..c9b4f140 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -55,10 +55,16 @@ metavar real ::= {{ hol string }} {{ com Real number literal }} +metavar value ::= + {{ phantom }} + {{ ocaml value }} + {{ lem value }} + embed {{ ocaml open Big_int +open Value type text = string @@ -627,83 +633,83 @@ end grammar -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Interpreter specific things % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} - | x :: :: optx_x - {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} - | :: :: optx_none - {{ lem Nothing }} {{ ocaml None }} - -tag :: 'Tag_' ::= -{{ com Data indicating where the identifier arises and thus information necessary in compilation }} - | None :: :: empty - | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} - | Set :: :: set {{ com Denotes an expression that mutates a local variable }} - | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} - | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} - | Ctor :: :: ctor {{ com Data constructor from a type union }} - | Extern optx :: :: extern {{ com External function, specied only with a val statement }} - | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} - | Spec :: :: spec - | Enum num :: :: enum - | Alias :: :: alias - | Unknown_path optx :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}} - -embed -{{ lem - -type tannot = maybe (typ * tag * list unit * effect * effect) - -}} - -embed -{{ ocaml - -(* Interpreter specific things are just set to unit here *) -type tannot = unit - -type reg_form_set = unit - -}} - -grammar -tannot :: '' ::= - {{ phantom }} - {{ ocaml unit }} - {{ lem tannot }} - -i_direction :: 'I' ::= - | IInc :: :: Inc - | IDec :: :: Dec - -ctor_kind :: 'C_' ::= - | C_Enum nat :: :: Enum - | C_Union :: :: Union - -reg_form :: 'Form_' ::= - | Reg id tannot i_direction :: :: Reg - | SubReg id reg_form index_range :: :: SubReg - -reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} - -alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} - -value :: 'V_' ::= {{ com interpreter evaluated value }} - | Boxref nat typ :: :: boxref - | Lit lit :: :: lit - | Tuple ( value1 , ... , valuen ) :: :: tuple - | List ( value1 , ... , valuen ) :: :: list - | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector - | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse - | Record typ ( id1 value1 , ... , idn valuen ) :: :: record - | V_ctor id typ ctor_kind value1 :: :: ctor - | Unknown :: :: unknown - | Register reg_form :: :: register - | Register_alias alias_spec_tannot tannot :: :: register_alias - | Track value reg_form_set :: :: track +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % Interpreter specific things % +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} +% | x :: :: optx_x +% {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} +% | :: :: optx_none +% {{ lem Nothing }} {{ ocaml None }} + +% tag :: 'Tag_' ::= +% {{ com Data indicating where the identifier arises and thus information necessary in compilation }} +% | None :: :: empty +% | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} +% | Set :: :: set {{ com Denotes an expression that mutates a local variable }} +% | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} +% | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} +% | Ctor :: :: ctor {{ com Data constructor from a type union }} +% | Extern optx :: :: extern {{ com External function, specied only with a val statement }} +% | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} +% | Spec :: :: spec +% | Enum num :: :: enum +% | Alias :: :: alias +% | Unknown_path optx :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}} + +% embed +% {{ lem + +% type tannot = maybe (typ * tag * list unit * effect * effect) + +% }} + +% embed +% {{ ocaml + +% (* Interpreter specific things are just set to unit here *) +% type tannot = unit + +% type reg_form_set = unit + +% }} + +% grammar +% tannot :: '' ::= +% {{ phantom }} +% {{ ocaml unit }} +% {{ lem tannot }} + +% i_direction :: 'I' ::= +% | IInc :: :: Inc +% | IDec :: :: Dec + +% ctor_kind :: 'C_' ::= +% | C_Enum nat :: :: Enum +% | C_Union :: :: Union + +% reg_form :: 'Form_' ::= +% | Reg id tannot i_direction :: :: Reg +% | SubReg id reg_form index_range :: :: SubReg + +% reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} + +% alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} + +% value :: 'V_' ::= {{ com interpreter evaluated value }} +% | Boxref nat typ :: :: boxref +% | Lit lit :: :: lit +% | Tuple ( value1 , ... , valuen ) :: :: tuple +% | List ( value1 , ... , valuen ) :: :: list +% | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector +% | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse +% | Record typ ( id1 value1 , ... , idn valuen ) :: :: record +% | V_ctor id typ ctor_kind value1 :: :: ctor +% | Unknown :: :: unknown +% | Register reg_form :: :: register +% | Register_alias alias_spec_tannot tannot :: :: register_alias +% | Track value reg_form_set :: :: track %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Expressions % diff --git a/src/Makefile b/src/Makefile index abf03c4f..403dcca1 100644 --- a/src/Makefile +++ b/src/Makefile @@ -64,7 +64,10 @@ lem_interp/interp_ast.lem: ../language/l2.ott ott -sort false -generate_aux_rules true -o lem_interp/interp_ast.lem -picky_multiple_parses true ../language/l2.ott sail: ast.ml - ocamlbuild sail.native + ocamlbuild -use-ocamlfind sail.native + +isail: ast.ml + ocamlbuild -use-ocamlfind isail.native sail.native: sail @@ -2,6 +2,8 @@ true: -traverse, debug, use_menhir <**/*.ml>: bin_annot, annot <lem_interp> or <test>: include <sail.{byte,native}>: use_pprint, use_nums, use_unix, use_str +<isail.{byte,native}>: package(linenoise), use_pprint, use_nums, use_unix, use_str +<isail.ml>: package(linenoise) <pprint> or <pprint/src>: include # see http://caml.inria.fr/mantis/view.php?id=4943 diff --git a/src/initial_check.ml b/src/initial_check.ml index 689df577..ee88e16c 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -951,6 +951,10 @@ let initial_kind_env = ("itself", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); ] +let exp_of_string order str = + let exp = Parser2.exp_eof Lexer2.token (Lexing.from_string str) in + to_ast_exp initial_kind_env order exp + let typschm_of_string order str = let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in diff --git a/src/initial_check.mli b/src/initial_check.mli index 01cf3bec..6059b0ac 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -59,3 +59,5 @@ val process_ast : order -> Parse_ast.defs -> unit defs val val_spec_ids : 'a defs -> IdSet.t val val_spec_of_string : order -> id -> string -> unit def + +val exp_of_string : order -> string -> unit exp diff --git a/src/interpreter.ml b/src/interpreter.ml new file mode 100644 index 00000000..55fb7b32 --- /dev/null +++ b/src/interpreter.ml @@ -0,0 +1,310 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Value +(* open Type_check *) + +type state = St + +let value_of_lit (L_aux (l_aux, _)) = + match l_aux with + | L_unit -> V_unit + | L_zero -> V_bit B0 + | L_one -> V_bit B1 + | L_true -> V_bool true + | L_false -> V_bool false + | L_string str -> V_string str + +let is_value = function + | (E_aux (E_internal_value _, _)) -> true + | _ -> false + +let is_true = function + | (E_aux (E_internal_value (V_bool b), _)) -> b == true + | _ -> false + +let is_false = function + | (E_aux (E_internal_value (V_bool b), _)) -> b == false + | _ -> false + +let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, None))) +let value_of_exp (E_aux (E_internal_value v, _)) = v + +(**************************************************************************) +(* 1. Interpreter Monad *) +(**************************************************************************) + +type 'a response = + | Final of value + | Exception of value + | Assertion_failed of string + | Call of id * value list * (value -> 'a) + | Gets of (state -> 'a) + | Puts of state * 'a + +and 'a monad = + | Pure of 'a + | Yield of ('a monad response) + +let map_response f = function + | Final v -> Final v + | Exception v -> Exception v + | Assertion_failed str -> Assertion_failed str + | Gets g -> Gets (fun s -> f (g s)) + | Puts (s, x) -> Puts (s, f x) + | Call (id, vals, cont) -> Call (id, vals, fun v -> f (cont v)) + +let rec liftM f = function + | Pure x -> Pure (f x) + | Yield g -> Yield (map_response (liftM f) g) + +let return x = Pure x + +let rec bind m f = + match m with + | Pure x -> f x + | Yield m -> Yield (map_response (fun m -> bind m f) m) + +let ( >>= ) m f = bind m f + +let ( >> ) m1 m2 = bind m1 (function () -> m2) + +type ('a, 'b) either = + | Left of 'a + | Right of 'b + +(* Support for interpreting exceptions *) + +let catch m = + match m with + | Pure x -> Pure (Right x) + | Yield (Exception v) -> Pure (Left v) + | Yield resp -> Yield (map_response (fun m -> liftM (fun r -> Right r) m) resp) + +let call (f : id) (args : value list) : value monad = + Yield (Call (f, args, fun v -> Pure v)) + +let throw v = Yield (Exception v) + +let gets : state monad = + Yield (Gets (fun s -> Pure s)) + +let puts (s : state) : unit monad = + Yield (Puts (s, Pure ())) + +let final v = Yield (Final v) + +let assertion_failed msg = Yield (Assertion_failed msg) + +let liftM2 f m1 m2 = m1 >>= fun x -> m2 >>= fun y -> return (f x y) + +let rec subst id value (E_aux (e_aux, annot) as exp) = + let wrap e_aux = E_aux (e_aux, annot) in + let e_aux = match e_aux with + | E_block exps -> E_block (List.map (subst id value) exps) + | E_nondet exps -> E_nondet (List.map (subst id value) exps) + | E_id id' -> if Id.compare id id' = 0 then unaux_exp (exp_of_value value) else E_id id' + | E_cast (typ, exp) -> E_cast (typ, subst id value exp) + | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps) + in + wrap e_aux + + +(**************************************************************************) +(* 2. Expression Evaluation *) +(**************************************************************************) + +let rec step (E_aux (e_aux, annot)) = + let wrap e_aux' = return (E_aux (e_aux', annot)) in + match e_aux with + | E_block [] -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) + | E_block [exp] when is_value exp -> return exp + | E_block (exp :: exps) when is_value exp -> wrap (E_block exps) + | E_block (exp :: exps) -> + step exp >>= fun exp' -> wrap (E_block (exp' :: exps)) + + | E_lit lit -> return (exp_of_value (value_of_lit lit)) + + | E_if (exp, then_exp, else_exp) when is_true exp -> return then_exp + | E_if (exp, then_exp, else_exp) when is_false exp -> return else_exp + | E_if (exp, then_exp, else_exp) -> + step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp)) + + | E_assert (exp, msg) when is_true exp -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) + | E_assert (exp, msg) when is_false exp -> assertion_failed "FIXME" + | E_assert (exp, msg) -> + step exp >>= fun exp' -> wrap (E_assert (exp', msg)) + + | E_app (id, exps) -> + let evaluated, unevaluated = Util.take_drop is_value exps in + begin + let open Type_check in + match unevaluated with + | exp :: exps -> + step exp >>= fun exp' -> wrap (E_app (id, evaluated @ exp' :: exps)) + | [] when Env.is_union_constructor id (env_of_annot annot) -> + return (exp_of_value (V_ctor (string_of_id id, List.map value_of_exp evaluated))) + | [] when Env.is_extern id (env_of_annot annot) "interpreter" -> + begin + let primop = StringMap.find (Env.get_extern id (env_of_annot annot) "interpreter") primops in + return (exp_of_value (primop (List.map value_of_exp evaluated))) + end + | [] -> liftM exp_of_value (call id (List.map value_of_exp evaluated)) + end + | E_app_infix (x, id, y) when is_value x && is_value y -> + liftM exp_of_value (call id [value_of_exp x; value_of_exp y]) + | E_app_infix (x, id, y) when is_value x -> + step y >>= fun y' -> wrap (E_app_infix (x, id, y')) + | E_app_infix (x, id, y) -> + step x >>= fun x' -> wrap (E_app_infix (x', id, y)) + + | E_return exp when is_value exp -> final (value_of_exp exp) + | E_return exp -> step exp >>= fun exp' -> wrap (E_return exp') + + | E_tuple exps -> + let evaluated, unevaluated = Util.take_drop is_value exps in + begin + match unevaluated with + | exp :: exps -> + step exp >>= fun exp' -> wrap (E_tuple (evaluated @ exp' :: exps)) + | [] -> return (exp_of_value (tuple_value (List.map value_of_exp exps))) + end + + | E_case (exp, pexps) when not (is_value exp) -> + step exp >>= fun exp' -> wrap (E_case (exp', pexps)) + | E_case (_, []) -> failwith "Pattern matching failed" + | E_case (exp, Pat_aux (Pat_exp (pat, body), _) :: pexps) -> + let matched, bindings = pattern_match pat (value_of_exp exp) in + if matched then + return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings)) + else + wrap (E_case (exp, pexps)) + + | E_cast (typ, exp) -> return exp + + | E_throw exp when is_value exp -> throw (value_of_exp exp) + | E_throw exp -> step exp >>= fun exp' -> wrap (E_throw exp') + + | E_try (exp, pexps) when is_value exp -> return exp + | E_try (exp, pexps) -> + begin + catch (step exp) >>= fun exp' -> + match exp' with + | Left exn -> wrap (E_case (exp_of_value exn, pexps)) + | Right exp' -> wrap (E_try (exp', pexps)) + end + + | E_sizeof _ | E_constraint _ -> assert false (* Must be re-written before interpreting *) + +and combine _ v1 v2 = + match (v1, v2) with + | None, None -> None + | Some v1, None -> Some v1 + | None, Some v2 -> Some v2 + | Some v1, Some v2 -> failwith "Pattern binds same identifier twice!" + +and pattern_match (P_aux (p_aux, _) as pat) value = + print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear); + match p_aux with + | P_lit lit -> eq_value (value_of_lit lit) value, Bindings.empty + | P_wild -> true, Bindings.empty + | P_as (pat, id) -> + let matched, bindings = pattern_match pat value in + matched, Bindings.add id value bindings + | P_typ (_, pat) -> pattern_match pat value + | P_id id -> true, Bindings.singleton id value + | P_app (id, pats) -> + let (ctor, vals) = coerce_ctor value in + if Id.compare id (mk_id ctor) = 0 then + let matches = List.map2 pattern_match pats vals in + List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches) + else + false, Bindings.empty + | P_record _ -> assert false (* TODO *) + | P_vector _ -> assert false (* TODO *) + | P_vector_concat _ -> assert false (* TODO *) + | P_tup pats | P_list pats -> + let matches = List.map2 pattern_match pats (coerce_listlike value) in + List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches) + | P_cons _ -> assert false (* TODO *) + +let exp_of_fundef (FD_aux (FD_function (_, _, _, funcls), _)) value = + let pexp_of_funcl (FCL_aux (FCL_Funcl (_, pexp), _)) = pexp in + E_aux (E_case (exp_of_value value, List.map pexp_of_funcl funcls), (Parse_ast.Unknown, None)) + +let rec get_fundef id (Defs defs) = + match defs with + | [] -> failwith (string_of_id id ^ " definition not found") + | (DEF_fundef fdef) :: _ when Id.compare id (id_of_fundef fdef) = 0 -> fdef + | _ :: defs -> get_fundef id (Defs defs) + +let rec eval_exp ast m = + match m with + | Pure v when is_value v -> value_of_exp v + | Pure exp' -> + Pretty_print_sail2.pretty_sail stdout (Pretty_print_sail2.doc_exp exp'); + print_newline (); + eval_exp ast (step exp') + | Yield (Call (id, vals, cont)) -> + print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); + let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in + let body = exp_of_fundef (get_fundef id ast) arg in + let v = eval_exp ast (return body) in + eval_exp ast (cont v) + | _ -> assert false + +let rec run_interpreter ast env = + let str = read_line () in + let exp = Type_check.infer_exp env (Initial_check.exp_of_string Ast_util.dec_ord str) in + let v = eval_exp ast (step exp) in + print_endline ("Result = " ^ string_of_value v); + run_interpreter ast env; diff --git a/src/isail.ml b/src/isail.ml new file mode 100644 index 00000000..5a225174 --- /dev/null +++ b/src/isail.ml @@ -0,0 +1,92 @@ +open Sail + +open Ast +open Ast_util +open Pretty_print_sail2 + +let rec user_input prompt callback = + match LNoise.linenoise prompt with + | None -> () + | Some v -> + callback v; + user_input prompt 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 + [ " ___ ___ ___ ___ "; + " /\\ \\ /\\ \\ /\\ \\ /\\__\\"; + " /::\\ \\ /::\\ \\ _\\:\\ \\ /:/ /"; + " /\\:\\:\\__\\ /::\\:\\__\\ /\\/::\\__\\ /:/__/ "; + " \\:\\:\\/__/ \\/\\::/ / \\::/\\/__/ \\:\\ \\ "; + " \\::/ / /:/ / \\:\\__\\ \\:\\__\\"; + " \\/__/ \\/__/ \\/__/ \\/__/"; + "" + ] + |> List.map banner + +let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast) + +let handle_input input = + LNoise.history_add input |> ignore; + + 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 + | ":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 (); + | ":q" | ":quit" -> + exit 0 + | ":i" | ":infer" -> + let exp = Initial_check.exp_of_string dec_ord arg in + let exp = Type_check.infer_exp !interactive_env exp in + pretty_sail stdout (doc_typ (Type_check.typ_of exp)); + print_newline () + | ":v" | ":verbose" -> + Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 2 + + | _ -> print_endline ("Unrecognised command " ^ input) + else + let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in + let v = Interpreter.eval_exp !interactive_ast (Interpreter.step exp) in + print_endline ("Result = " ^ Value.string_of_value v) + + +let () = + List.iter print_endline sail_logo; + + (* Auto complete function names based on val specs *) + LNoise.set_completion_callback + begin + fun line_so_far ln_completions -> + let line_so_far, last_id = + try + let p = Str.search_backward (Str.regexp "[^a-zA-Z0-9_]") line_so_far (String.length line_so_far - 1) in + Str.string_before line_so_far (p + 1), Str.string_after line_so_far (p + 1) + with + | Not_found -> "", line_so_far + | Invalid_argument _ -> line_so_far, "" + in + if last_id <> "" then + IdSet.elements !vs_ids + |> List.map string_of_id + |> List.filter (fun id -> Str.string_match (Str.regexp_string last_id) id 0) + |> List.map (fun completion -> line_so_far ^ completion) + |> List.iter (LNoise.add_completion ln_completions) + else () + end; + + LNoise.history_load ~filename:"sail_history" |> ignore; + LNoise.history_set ~max_length:100 |> ignore; + + if !opt_interactive then + user_input "sail> " handle_input + else () diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml index a437e7e6..03257458 100644 --- a/src/myocamlbuild.ml +++ b/src/myocamlbuild.ml @@ -80,7 +80,7 @@ let lem_opts = [A "-lib"; P "../lem_interp"; A "-wl_pat_fail"; P "ign"; A "-wl_unused_vars"; P "ign"; (* A "-suppress_renaming";*) -] ;; + ] ;; dispatch begin function | After_rules -> diff --git a/src/parser2.mly b/src/parser2.mly index 59c7f1c4..c222bb39 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -178,7 +178,9 @@ let rec desugar_rchain chain s e = %start file %start typschm_eof +%start exp_eof %type <Parse_ast.typschm> typschm_eof +%type <Parse_ast.exp> exp_eof %type <Parse_ast.defs> file %% @@ -690,6 +692,10 @@ lit: | Real { mk_lit (L_real $1) $startpos $endpos } +exp_eof: + | exp Eof + { $1 } + exp: | exp0 { $1 } diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 0c531301..17185cc9 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -171,13 +171,17 @@ let doc_quants quants = | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) -let doc_typschm (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = + + +let doc_binding (TypQ_aux (tq_aux, _), typ) = match tq_aux with | TypQ_no_forall -> doc_typ typ | TypQ_tq [] -> doc_typ typ | TypQ_tq qs -> string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ +let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ) + let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = @@ -322,7 +326,8 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = end (* Resugar an assert with an empty message *) | E_throw exp -> string "throw" ^^ parens (doc_exp exp) - | E_try (exp, pexps) -> assert false + | E_try (exp, pexps) -> + separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps] | E_return exp -> string "return" ^^ parens (doc_exp exp) | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp) | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> @@ -368,6 +373,7 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) = brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3]) | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4]) + | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear) | _ -> parens (doc_exp exp) and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) = separate_map (comma ^^ space) doc_fexp fexps @@ -523,3 +529,5 @@ let doc_defs (Defs(defs)) = separate_map hardline doc_def defs let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d) + +let pretty_sail f doc = ToChannel.pretty 1. 120 f doc diff --git a/src/sail.ml b/src/sail.ml index aecbcbec..519ec916 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -52,6 +52,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_print_version = ref false let opt_print_initial_env = ref false let opt_print_verbose = ref false @@ -71,6 +72,9 @@ let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), "<prefix> select output filename prefix"); + ( "-i", + Arg.Set opt_interactive, + " start interactive interpreter"); ( "-ocaml", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], " output an OCaml translated version of the input"); @@ -169,6 +173,8 @@ let _ = opt_file_arguments := (!opt_file_arguments) @ [s]) usage_msg +let interactive_ast = ref (Ast.Defs []) +let interactive_env = ref Type_check.initial_env let main() = if !opt_print_version @@ -208,6 +214,10 @@ let main() = (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) begin + (if !(opt_interactive) + then + (interactive_ast := ast; interactive_env := type_envs) + else ()); (if !(opt_sanity) then let _ = rewrite_ast_check ast in diff --git a/src/util.ml b/src/util.ml index 6f7d6a95..bd083a8b 100644 --- a/src/util.ml +++ b/src/util.ml @@ -372,9 +372,24 @@ let is_some = function | Some _ -> true | None -> false +let rec take_drop f = function + | [] -> ([], []) + | (x :: xs) when not (f x) -> ([], x :: xs) + | (x :: xs) -> + let (ys, zs) = take_drop f xs in + (x :: ys, zs) + let is_none opt = not (is_some opt) let rec take n xs = match n, xs with | 0, _ -> [] | n, [] -> [] | n, (x :: xs) -> x :: take (n - 1) xs + +let termcode n = "\x1B[" ^ string_of_int n ^ "m" +let bold str = termcode 1 ^ str +let green str = termcode 92 ^ str +let yellow str = termcode 93 ^ str +let red str = termcode 91 ^ str +let cyan str = termcode 96 ^ str +let clear str = str ^ termcode 0 diff --git a/src/util.mli b/src/util.mli index 73dbd30b..bdf6e594 100644 --- a/src/util.mli +++ b/src/util.mli @@ -228,3 +228,14 @@ val is_some : 'a option -> bool val is_none : 'a option -> bool val take : int -> 'a list -> 'a list + +val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list) + +(* Terminal color codes *) +val termcode : int -> string +val bold : string -> string +val green : string -> string +val red : string -> string +val yellow : string -> string +val cyan : string -> string +val clear : string -> string diff --git a/src/value.ml b/src/value.ml new file mode 100644 index 00000000..0c67f487 --- /dev/null +++ b/src/value.ml @@ -0,0 +1,123 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Big_int + +type bit = B0 | B1 + +type value = + | V_vector of value list + | V_list of value list + | V_int of big_int + | V_bool of bool + | V_bit of bit + | V_tuple of value list + | V_unit + | V_string of string + | V_ctor of string * value list + +let rec string_of_value = function + | V_vector _ -> "VEC" + | V_bool true -> "true" + | V_bool false -> "false" + | V_bit B0 -> "bitzero" + | V_bit B1 -> "bitone" + | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" + | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]" + | V_unit -> "()" + | V_string str -> "\"" ^ str ^ "\"" + | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" + +let eq_value v1 v2 = string_of_value v1 = string_of_value v2 + +let coerce_bit = function + | V_bit b -> b + | _ -> assert false + +let coerce_ctor = function + | V_ctor (str, vals) -> (str, vals) + | _ -> assert false + +let coerce_bool = function + | V_bool b -> b + | _ -> assert false + +let and_bool [v1; v2] = V_bool (coerce_bool v1 && coerce_bool v2) +let or_bool [v1; v2] = V_bool (coerce_bool v1 || coerce_bool v2) +let print [v] = print_endline (string_of_value v |> Util.red |> Util.clear); V_unit + +let tuple_value (vs : value list) : value = V_tuple vs + +let coerce_tuple = function + | V_tuple vs -> vs + | _ -> assert false + +let coerce_listlike = function + | V_tuple vs -> vs + | V_list vs -> vs + | _ -> assert false + +let coerce_cons = function + | V_list (v :: vs) -> Some (v, vs) + | V_list [] -> None + | _ -> assert false + +let unit_value = V_unit + +module StringMap = Map.Make(String) + +let primops = + List.fold_left + (fun r (x, y) -> StringMap.add x y r) + StringMap.empty + [ ("and_bool", and_bool); + ("or_bool", or_bool); + ("print_endline", print); + ] |