Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Candle REPL fixes #904

Merged
merged 3 commits into from Aug 20, 2022
Merged

Candle REPL fixes #904

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
96dd4cc
Treat type variables more robustly in REPL
oskarabrahamsson Aug 16, 2022
13f7ac2
Various fixes to Candle REPL
oskarabrahamsson Aug 16, 2022
7bd9810
Use loads/needs instead of #load/#need in REPL
oskarabrahamsson Aug 16, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
190 changes: 139 additions & 51 deletions candle/prover/candle_boot.ml
View file
Open in desktop
Expand Up @@ -2,6 +2,11 @@
* Prelude
* ------------------------------------------------------------------------- *)

(* This is pointer equality, which is missing from CakeML.
|| x = y is just to get the type variables right:
*)
let (==) x y = false || x = y;;

let ref x = Ref x;;

let (/) = div;;
Expand All @@ -12,6 +17,11 @@ let (/.) = Double.(/);;

let failwith msg = raise (Failure msg);;

(* This is the pretty printer for exceptions, and you need to update it
each time you add an exception definition if you want it to print something
informative (see e.g. exception Unchanged in lib.ml).
*)

let pp_exn e =
match e with
| Chr -> Pretty_printer.token "Chr"
Expand All @@ -22,10 +32,28 @@ let pp_exn e =
| Failure s -> Pretty_printer.app_block "Failure" [Pretty_printer.pp_string s]
| _ -> Pretty_printer.token "<exn>";;

(*CML
(* OCaml parser doesn't like the tilde *)
val rat_minus = Rat.~;
*)

(* Some conversions in OCaml style: *)

let string_of_int = Int.toString;;
let string_of_int n =
if n < 0 then "-" ^ Int.toString (-n)
else Int.toString n
;;

let pp_int n = Pretty_printer.token (string_of_int n);;

let pp_rat r =
let n = Rat.numerator r in
let d = Rat.denominator r in
Pretty_printer.token (string_of_int n ^ "/" ^ string_of_int d)
;;

let string_of_float = Double.toString;;

let int_of_string = Option.valOf o Int.fromString;;

(* Left shifting integers. HOL Light expects these to not be bigints, so I
Expand All @@ -47,6 +75,7 @@ let string_escaped =
| '\b'::l -> '\\'::'b'::escape l
| '\t'::l -> '\\'::'t'::escape l
| '\n'::l -> '\\'::'n'::escape l
| '"'::l -> '\\'::'"'::escape l
| c::l -> c::escape l in
fun s -> String.implode (escape (String.explode s));;

Expand All @@ -71,6 +100,11 @@ let abs x = if x < 0 then -x else x;;

let ignore x = x; ();;

let rec rev_append xs acc =
match xs with
| [] -> acc
| x::xs -> rev_append xs (x::acc);;

(* ------------------------------------------------------------------------- *
* Helpful banner
* ------------------------------------------------------------------------- *)
Expand Down Expand Up @@ -219,9 +253,9 @@ let string_of_directive d =

type token =
| T_begin | T_end | T_struct | T_sig | T_semis | T_newline
| T_use | T_needs | T_loads (* converted into directives *)
| T_other of string
| T_symb of string
| T_directive of directive * string
| T_comment of string
| T_string of string
| T_quote of string
Expand All @@ -247,12 +281,21 @@ let string_of_token unquote tok =
| Some f -> "(" ^ f s ^ ")"
end
| T_char s -> "'" ^ s ^ "'"
| T_directive (d, f) ->
String.concat ["#"; string_of_directive d; " "; "\""; f; "\";;"]
| T_comment s | T_other s | T_symb s | T_number s | T_spaces s -> s
| T_use -> "#use"
| T_loads -> "loads"
| T_needs -> "needs"
| T_done -> "(* shouldn't happen *)"
;;

let directive_of_token t =
match t with
| T_needs -> Some D_need
| T_loads -> Some D_load
| T_use -> Some D_use
| _ -> None
;;

let scan nextChar peekChar =
let quoteSym c = c = '`' in
let tok_from_keyword =
Expand All @@ -261,6 +304,10 @@ let scan nextChar peekChar =
"end", T_end;
"struct", T_struct;
"sig", T_sig;
(* top-level directives *)
"#use", T_use;
"needs", T_needs;
"loads", T_loads;
] in
fun s -> match Alist.lookup keywords s with
| None -> T_other s
Expand Down Expand Up @@ -335,37 +382,6 @@ let scan nextChar peekChar =
let scan_spaces c =
Option.map (fun s -> T_spaces s)
(scan_while [c] (fun c -> c <> '\n' && Char.isSpace c)) in
let dir_from_string =
let dirs = [
"load", D_load;
"need", D_need;
"use", D_use ] in
Alist.lookup dirs in
let scan_directive () = (* TODO *)
match scan_while [] (fun x -> x <> ';') with
| None -> None
| Some s ->
nextChar ();
match peekChar () with
| None -> Some (T_other ("#" ^ s ^ ";"))
| Some c ->
if c <> ';' then
Some (T_other ("#" ^ s ^ ";" ^ String.str c))
else
begin
nextChar ();
match String.fields (fun x -> x = '"') s with
| [dir; fname; rest] ->
let dir = trimRight dir in
let rest = trimLeft rest in
if rest <> "" then Some (T_other ("#" ^ s ^ ";;")) else
begin
match dir_from_string dir with
| None -> Some (T_other ("#" ^ s ^ ";;"))
| Some d -> Some (T_directive (d, fname))
end
| _ -> Some (T_other ("#" ^ s ^ ";;"))
end in
let scan_escaped ch =
let rec nom acc =
Interrupt.check ();
Expand All @@ -383,9 +399,39 @@ let scan nextChar peekChar =
let scan_strlit () =
Option.map (fun s -> T_string s)
(scan_escaped '"') in
let scan_charlit () =
Option.map (fun s -> T_char s)
(scan_escaped '\'') in
(* This code will intentionally let through some bad tokens (it doesn't check
whether escape sequences are well formed), but those will get stuck in the
real lexer. *)
let scan_charlit_or_tyvar () =
match peekChar () with
(* Escaped character literal *)
| Some '\\' ->
begin
nextChar ();
Option.map (fun s -> T_char ("\\" ^ s))
(scan_escaped '\'')
end
(* A single tick, start of a type variable, but followed by space *)
| Some ' ' | Some '\n' | Some '\t' | Some '\r' -> Some (T_other "'")
(* Regular character literal, or a type variable *)
| Some c ->
begin
nextChar ();
match peekChar () with
(* Regular character literal *)
| Some '\'' ->
begin
nextChar ();
Some (T_char (String.str c))
end
(* Type variable *)
| Some _ -> Option.map (fun s -> T_other s)
(scan_while [c; '\''] is_name_char)
| None -> Some (T_other (String.implode ['\''; c]))
end
(* Two ticks following each other: '' *)
| Some '\'' -> Some (T_symb "''")
| None -> Some (T_symb "'") in
let rec nextToken () =
match nextChar () with
| None -> None
Expand All @@ -411,12 +457,12 @@ let scan nextChar peekChar =
end
| _ -> Some (T_symb "(")
end
(* Attempt to scan char literal *)
| Some '\'' -> scan_charlit ()
(* Attempt to scan char literal or type variable *)
| Some '\'' -> scan_charlit_or_tyvar ()
(* Attempt to scan string literal *)
| Some '"' -> scan_strlit ()
(* Attempt to scan load directive *)
| Some '#' -> scan_directive ()
(* A #use directive, maybe: *)
| Some '#' -> scan_name '#'
(* Newlines *)
| Some '\n' -> Some T_newline
(* Anything else *)
Expand Down Expand Up @@ -562,20 +608,61 @@ let () =
| Some tok -> Some tok
| None -> scan1 () in
let output_buffer = (Buffer.empty () : Lexer.token Buffer.buffer) in
let rec next_nonspace () =
match next () with
| Some (Lexer.T_spaces _) -> next_nonspace ()
| res -> res in
let rec scan level =
try match next () with
| None -> None
(* Attempt to use token as part of loading directive if it sits at the
top level (i.e. not inside parenthesis). The REPL fails and reports
and error unless the token is followed by a string literal and then
double semicolons. Ideally we should also check that the token sits
at the start of the line, but we don't, so odd things such as this:
foo needs "bar.ml";;
are OK and will cause the file bar.ml to be loaded and appear
directly after 'foo' in the token stream.
*)
| Some (Lexer.T_use | Lexer.T_needs | Lexer.T_loads as tok)
when level = 0 ->
begin
let dir = Option.valOf (Lexer.directive_of_token tok) in
match next_nonspace () with
(* Attempt to convert into directive: *)
| Some (Lexer.T_string fname as tok') ->
begin
match next_nonspace () with
(* OK directive, perform load: *)
| Some (Lexer.T_semis) ->
let lines = load dir fname in
if List.null lines then scan level else
begin
userInput := false;
scan_lines lines;
scan level
end
(* Malformed *)
| _ ->
failwith
(String.concat [
"\nREPL error: ";
Lexer.string_of_directive dir;
" \"string\" should be followed by a double";
" semicolon [;;].\n"])
end
(* Malformed *)
| _ ->
failwith
(String.concat [
"\nREPL error: ";
Lexer.string_of_directive dir;
" should be followed by a \"string literal\" and then a";
" double semicolon [;;].\n"])
end
| Some (Lexer.T_done) ->
userInput := true;
scan level
| Some (Lexer.T_directive (dir, fname)) ->
let lines = load dir fname in
if List.null lines then scan level else
begin
userInput := false;
scan_lines lines;
scan level
end
| Some tok ->
Buffer.push_back output_buffer tok;
match tok with
Expand Down Expand Up @@ -612,7 +699,8 @@ let () =
if not (!userInput) then print (!prompt1);
Buffer.flush input_buffer;
Buffer.flush output_buffer;
Repl.nextString := "" in
Repl.nextString := "";
userInput := true in
Repl.readNextString := (fun () ->
print (!prompt1);
next ();
Expand Down