Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: e98cf539 by Jonathan Graveline at 2018-07-05T19:03:15Z Using rlwrap to add auto-completion and history

- - - - - a0f050f7 by Jonathan Graveline at 2018-07-05T19:40:51Z Stop compiler on first error

- - - - - ece77ad2 by Jonathan Graveline at 2018-07-05T19:43:43Z Don't try to print value if there's none

- - - - - 72bfc552 by Jonathan Graveline at 2018-07-05T19:49:54Z Added .directory to .gitignore

- - - - - f3667866 by Jonathan Graveline at 2018-07-06T03:03:52Z Print similar name with error message when a variable isn't found

- - - - -

8 changed files:

- .gitignore - GNUmakefile - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/util.ml - tests/eval_test.ml - + typer.sh

Changes:

===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -25,3 +25,4 @@ gmon.out ocamlprof.dump emacs/*-autoloads.el emacs/*-pkg.el +.directory

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -8,7 +8,7 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml)

-OBFLAGS = -tag debug -tag profile -build-dir $(BUILDDIR) -pkg num +OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg num # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str # OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -232,7 +232,12 @@ let rec repl i clxp rctx = | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( match (str_split ipt ' ') with | "%readfile"::args -> - let (i, clxp, rctx) = readfiles args (i, clxp, rctx) false in + let (i, clxp, rctx) = + try + readfiles args (i, clxp, rctx) false + with Util.Stop_Compilation s -> + (print_string s; (i,clxp,rctx)) + in repl clxp rctx; | "%who"::args | "%w"::args -> ( let _ = match args with @@ -255,8 +260,9 @@ let rec repl i clxp rctx = try let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in List.iter (print_eval_result i) ret; repl clxp rctx - with e -> - repl clxp rctx) + with e -> match e with + | Util.Stop_Compilation msg -> (print_string msg; repl clxp rctx) + | _ -> repl clxp rctx)

let arg_files = ref []

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -32,6 +32,8 @@ * * ---------------------------------------------------------------------------*)

+module Str = Str + open Util open Lexp module L = Lexp @@ -140,6 +142,15 @@ let _make_scope = SMap.empty let _make_senv_type = (0, _make_scope) let _make_myers = M.nil

+let _get_related_name (n : db_ridx) name map = + let r = Str.regexp (name^".*") in + SMap.fold (fun name idx ps -> + if (Str.string_match r name 0) then + (n - idx - 1)::ps + else + ps + ) map [] + (* Public methods: DO USE * ---------------------------------- *)

@@ -147,10 +158,19 @@ let empty_elab_context : elab_context = (Grammar.default_grammar, _make_senv_type, _make_myers, (0, 0, ref SMap.empty))

+(* senv_lookup caller were using Not_found exception *) +exception Senv_Lookup_Fail of (db_ridx list) +let senv_lookup_fail relateds = raise (Senv_Lookup_Fail relateds) + +let get_related_name (name: string) (ctx: elab_context) = + let (_, (n, map), _, _) = ctx in + _get_related_name n name map + (* return its current DeBruijn index *) -let rec senv_lookup (name: string) (ctx: elab_context): int = +let senv_lookup (name: string) (ctx: elab_context): int = let (_, (n, map), _, _) = ctx in - n - (SMap.find name map) - 1 + try n - (SMap.find name map) - 1 + with Not_found -> senv_lookup_fail (_get_related_name n name map)

let lexp_ctx_cons (ctx : lexp_context) d v t = assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in @@ -212,6 +232,16 @@ let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx

+(* Print related name raised by senv_lookup_fail *) +let print_related (xs : db_ridx list) (ctx: lexp_context) = + let tab = List.fold_left (fun str idx -> + let ((_, name), _, _) = env_lookup_by_index idx ctx in + match name with + | Some name -> (str ^ "\n\t" ^ name ^ "[" ^ (string_of_int idx) ^ "]") + | _ -> (str ^ "\n\t" ^ "[" ^ (string_of_int idx) ^ "]") + ) "" xs in + tab ^ "\n" + (* Print context *) let print_lexp_ctx_n (ctx : lexp_context) start = let n = (M.length ctx) - 1 in

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -273,13 +273,6 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | _ -> sexp_error loc "define-operator expects 3 argument"; ctx

-let elab_varref ctx (loc, name) - = let idx = senv_lookup name ctx in - let id = (loc, Some name) in - let lxp = mkVar (id, idx) in - let ltp = env_lookup_type ctx (id, idx) in - (lxp, Inferred ltp) - (* Turn metavar into plain vars after generalization. *) let rec meta_to_var ids o (e : lexp) = let rec loop e = match e with @@ -435,6 +428,15 @@ let rec elaborate ctx se ot = * through `typr-identifier`)? *) elab_call ctx ft args

+and elab_varref ctx (loc, name) + = try + let idx = senv_lookup name ctx in + let id = (loc, Some name) in + let lxp = mkVar (id, idx) in + let ltp = env_lookup_type ctx (id, idx) in + (lxp, Inferred ltp) + with Senv_Lookup_Fail xs -> senv_lookup_fail xs + and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with | (_, Checked) -> fatal (sexp_location p) "`infer` got Checked!" @@ -462,7 +464,7 @@ and get_implicit_arg ctx loc oname t = let pidx, pname = (senv_lookup "default" ctx), "default" in let default = Var ((dloc, Some pname), pidx) in get_attribute ctx loc [default; t] - with Not_found -> None with + with e -> None with | Some attr -> (* FIXME: The `default` attribute table shouldn't contain elements of * type `Macro` but elements of type `something -> Sexp`. @@ -725,7 +727,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Cons _ (* It's indeed a constructor! *) -> add_branch (Symbol (l, name)) [] | _ -> add_default var (* A named default branch. *) - with Not_found -> add_default var) + with e -> add_default var)

| Ppatcons (pctor, pargs) -> add_branch pctor pargs in

@@ -925,7 +927,7 @@ and sexp_decls_macro_print sxp_decls = | e -> sexp_print e; print_string "\n"

and lexp_decls_macro (loc, mname) sargs ctx: sexp = - try let lxp, ltp = infer (Symbol (loc, mname)) ctx in + try let lxp, ltp = infer (Symbol (loc, mname)) ctx in

(* FIXME: Check that (conv_p ltp Macro)! *) let ret = lexp_expand_macro loc lxp sargs ctx None in @@ -935,8 +937,12 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp")) | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp")

- with e -> - fatal loc ("Macro `" ^ mname ^ "`not found") + with e -> + let relateds = get_related_name mname ctx in + let msg = if ((List.length relateds) > 0) then + ". Did you mean:" ^ (print_related relateds (ectx_to_lctx ctx)) + else "" in + fatal loc ("Macro `" ^ mname ^ "`not found" ^ msg)

and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) @@ -1394,9 +1400,14 @@ let sform_identifier ctx loc sargs ot = (* Normal identifier. *) | [Symbol id] -> (try elab_varref ctx id - with Not_found -> + with Senv_Lookup_Fail xs -> (let (loc, name) = id in - sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); + let relateds = + if ((List.length xs) > 0) then + ". Did you mean: " ^ (print_related xs (ectx_to_lctx ctx)) + else "" in + sexp_error loc ("The variable: `" ^ name ^ + "` was not declared" ^ relateds); sform_dummy_ret ctx loc))

| [se] @@ -1700,10 +1711,14 @@ let _eval_expr_str str lctx rctx silent = let elxps = List.map OL.erase_type lxps in (EV.eval_all elxps rctx silent)

-let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false +let eval_expr_str str lctx rctx = try _eval_expr_str str lctx rctx false + with Util.Stop_Compilation s -> (print_string s; [])

let eval_decl_str str lctx rctx = - let lxps, lctx = lexp_decl_str str lctx in - let elxps = (List.map OL.clean_decls lxps) in - (EV.eval_decls_toplevel elxps rctx), lctx + let prev_lctx, prev_rctx = lctx, rctx in + try + let lxps, lctx = lexp_decl_str str lctx in + let elxps = (List.map OL.clean_decls lxps) in + (EV.eval_decls_toplevel elxps rctx), lctx + with Util.Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx)

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -63,26 +63,38 @@ let internal_error s = raise (Internal_error s) exception Unreachable_error of string let typer_unreachable s = raise (Unreachable_error s)

+exception Stop_Compilation of string +let stop_compilation s = raise (Stop_Compilation s) + (* Section is the name of the compilation step [for debugging] *) (* 'prerr' output is ugly *) -let msg_message lvl kind section (loc: location) msg = - if lvl <= !_typer_verbose then - print_string (loc.file +let msg_message stop lvl kind section (loc: location) msg = + let preppend_loc msg = (loc.file ^ ":" ^ string_of_int loc.line ^ ":" ^ string_of_int loc.column ^ ":" ^ kind ^ (if section = "" then " " else "(" ^ section ^ ") ") - ^ msg ^ "\n") + ^ msg ^ "\n") in + if lvl <= !_typer_verbose then + (print_string (preppend_loc msg); + if stop then + stop_compilation (preppend_loc "Compiler stopped on first error") + else ()) + else if stop then + stop_compilation (preppend_loc "Compiler stopped on first error") else ()

+(* I would like to add optional stop on warning but I think *) +(* warning may be thrown at runtime *) + let msg_fatal s l m = - msg_message 0 "[X] Fatal " s l m; + msg_message false 0 "[X] Fatal " s l m; flush stdout; internal_error "Compiler Fatal Error"

-let msg_error = msg_message 1 "Error:" -let msg_warning = msg_message 2 "Warning:" -let msg_info = msg_message 3 "Info:" +let msg_error = msg_message true 1 "Error:" +let msg_warning = msg_message false 2 "Warning:" +let msg_info = msg_message false 3 "Info:"

(* Compiler Internal Debug print *) let debug_msg expr =

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -55,8 +55,17 @@ let test_eval_eqv_named name decl run res = if value_eq_list erun eres then success () else ( - value_print (List.hd erun); - value_print (List.hd eres); + (* List.hd was throwing when run or res failed to compile *) + (if (List.length erun >= 1) + then + value_print (List.hd erun) + else + print_string ("no run expression\n")); + (if (List.length eres >= 1) + then + value_print (List.hd eres) + else + print_string ("no result expression\n")); failure ()))

let test_eval_eqv decl run res = test_eval_eqv_named run decl run res

===================================== typer.sh ===================================== --- /dev/null +++ b/typer.sh @@ -0,0 +1,14 @@ +#!/bin/sh + +# I saw _history in REPL.ml and I'm not sure if there's a +# simple way to do it portably. Anyway this solution (for linux) seemed so simple +# that I had to try it. + +# Alternative for history, user input, etc. are ledit which isn't on my base +# repository or ncurses which is a dependency and not a wrapper. + +# complete-filenames is useful for "%readfile ..." command +# history-no-dupes just make it faster to search history with up and down key +rlwrap --complete-filenames --history-no-dupes 1 ./_build/typer $* + +# if not specified history must be kept in "~/.typer_history"

View it on GitLab: https://gitlab.com/monnier/typer/compare/124601a5ba7e451dbe8c5f33e01e7ba3e01...