Stefan pushed to branch master at Stefan / Typer

Commits: 32ef5ef1 by Stefan Monnier at 2018-09-21T02:10:39Z Get rid of identifiers starting with underscore in *.ml

- - - - -

9 changed files:

- src/REPL.ml - src/debruijn.ml - src/debug_util.ml - src/elab.ml - src/eval.ml - src/fmt.ml - src/lexer.ml - src/lexp.ml - tests/sexp_test.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -56,9 +56,6 @@ open Debruijn module OL = Opslexp module EL = Elexp

-(* how to handle arrow keys ? *) -let _history = ref [] - let arg_batch = ref false

let print_input_line i = @@ -136,27 +133,27 @@ let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = lexprs; (ldecls, lexprs), lctx

-let ieval lexps rctx = +let ieval f str ectx rctx = + let ieval' lexps rctx = let (ldecls, lexprs) = lexps in let rctx = eval_decls_toplevel ldecls rctx in let vals = eval_all lexprs rctx false in - vals, rctx - -let _ieval f str ectx rctx = - let pres = (f str) in - let sxps = lex default_stt pres in - (* FIXME: This is too eager: it prevents one declaration from changing - * the grammar used in subsequent declarations. *) - let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in - - (* Different from usual typer *) - let pxps = ipexp_parse nods in - let lxps, ectx = ilexp_parse pxps ectx in - let elxps = ierase_type lxps in - let v, rctx = ieval elxps rctx in - v, ectx, rctx - -let _raw_eval f str ectx rctx = + vals, rctx in + + let pres = (f str) in + let sxps = lex default_stt pres in + (* FIXME: This is too eager: it prevents one declaration from changing + * the grammar used in subsequent declarations. *) + let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in + + (* Different from usual typer *) + let pxps = ipexp_parse nods in + let lxps, ectx = ilexp_parse pxps ectx in + let elxps = ierase_type lxps in + let v, rctx = ieval' elxps rctx in + v, ectx, rctx + +let raw_eval f str ectx rctx = let pres = (f str) in let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in @@ -172,21 +169,21 @@ let _raw_eval f str ectx rctx = (* This is for consistency with ieval *) [], ectx, rctx

-let ieval_string = _ieval prelex_string -let ieval_file = _ieval prelex_file +let ieval_string = ieval prelex_string +let ieval_file = ieval prelex_file

-let eval_string = _raw_eval prelex_string -let eval_file = _raw_eval prelex_file +let eval_string = raw_eval prelex_string +let eval_file = raw_eval prelex_file

-let _welcome_msg = +let welcome_msg = " Typer 0.0.0 - Interpreter - (c) 2016

%quit (%q) : leave REPL %help (%h) : print help "

-let _help_msg = +let help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment %info (%i) : print elaboration environment @@ -220,11 +217,10 @@ let readfiles files (i, lctx, rctx) prt = let rec repl i clxp rctx = let repl = repl (i + 1) in let ipt = try read_input i with End_of_file -> "%quit" in - _history := ipt::!_history; match ipt with (* Check special keywords *) | "%quit" | "%q" -> () - | "%help" | "%h" -> (print_string _help_msg; repl clxp rctx) + | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx)

@@ -287,7 +283,7 @@ let main () =

if not !arg_batch then (print_string (make_title " TYPER REPL "); - print_string _welcome_msg; + print_string welcome_msg; print_string (make_sep '-'); flush stdout);

===================================== src/debruijn.ml ===================================== @@ -135,47 +135,40 @@ let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int = get_size ectx - slen

-(* internal definitions - * ---------------------------------- *) - -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 - let search r = SMap.fold (fun name idx ps -> - if (Str.string_match r name 0) then - (n - idx - 1)::ps - else - ps - ) map [] in - if ((String.sub name 0 1) = "_" || - (String.sub name ((String.length name) - 1) 1) = "_") && - ((String.length name) > 1) then - search r - else [] - (* Public methods: DO USE * ---------------------------------- *)

+let empty_senv = (0, SMap.empty) +let empty_lctx = M.nil + let empty_elab_context : elab_context - = (Grammar.default_grammar, _make_senv_type, _make_myers, + = (Grammar.default_grammar, empty_senv, empty_lctx, (0, 0, ref SMap.empty))

(* senv_lookup caller were using Not_found exception *) -exception Senv_Lookup_Fail of (db_ridx list) +exception Senv_Lookup_Fail of (string 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 *) +(* Return its current DeBruijn index. *) let senv_lookup (name: string) (ctx: elab_context): int = let (_, (n, map), _, _) = ctx in try n - (SMap.find name map) - 1 - with Not_found -> senv_lookup_fail (_get_related_name n name map) + with Not_found + -> let get_related_names (n : db_ridx) name map = + let r = Str.regexp (".*"^name^".*") in + let search r = SMap.fold (fun name _ names + -> if (Str.string_match r name 0) then + name::names + else + names) + map [] in + if ((String.sub name 0 1) = "_" || + (String.sub name ((String.length name) - 1) 1) = "_") && + ((String.length name) > 1) then + search r + else [] in + + senv_lookup_fail (get_related_names n name map)

let lexp_ctx_cons (ctx : lexp_context) d v t = assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in @@ -237,16 +230,6 @@ 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/debug_util.ml ===================================== @@ -85,47 +85,30 @@ let get_p_option name = highlight (use console color to display hints) *)

-let _format_mode = ref false -let _ppctx = ref pretty_ppctx -let _format_dest = ref "" -let _write_file = ref false -let _typecheck = ref false +let format_mode = ref false +let ppctx = ref pretty_ppctx +let format_dest = ref "" +let write_file = ref false

+let mod_ctx name v = let f ctx = ctx := SMap.add name v !ctx in + f ppctx; f debug_ppctx

-let _set_print_pretty ctx v = - ctx := SMap.add "pretty" (Bool (v)) !ctx - -let _set_print_type ctx v = - ctx := SMap.add "print_type" (Bool (v)) !ctx - -let _set_print_index ctx v = - ctx := SMap.add "print_dbi" (Bool (v)) !ctx - -let _set_print_indent_size ctx v = - ctx := SMap.add "indent_size" (Int (v)) !ctx - -let _set_highlight ctx v = - ctx := SMap.add "color" (Bool (v))!ctx - -let mod_ctx f v = f _ppctx v; f debug_ppctx v - -let set_print_type v () = mod_ctx _set_print_type v -let set_print_index v () = mod_ctx _set_print_index v -let set_print_indent_size v = mod_ctx _set_print_indent_size v -let set_highlight v () = mod_ctx _set_highlight v -let set_print_pretty v () = mod_ctx _set_print_pretty v -let set_typecheck v () = _typecheck := v +let set_print_type v () = mod_ctx "print_type" (Bool v) +let set_print_index v () = mod_ctx "print_dbi" (Bool v) +let set_print_indent_size v = mod_ctx "indent_size" (Int v) +let set_highlight v () = mod_ctx "color" (Bool v) +let set_print_pretty v () = mod_ctx "pretty" (Bool v)

let output_to_file str = - _write_file := true; - _format_dest := str; + write_file := true; + format_dest := str; set_highlight false ()

let arg_defs = [ (* format *) ("--format", - Arg.Unit (fun () -> _format_mode := true), " format a typer source code"); + Arg.Unit (fun () -> format_mode := true), " format a typer source code"); ("-fmt-type=on", Arg.Unit (set_print_type true), " Print type info"); ("-fmt-pretty=on", @@ -200,11 +183,11 @@ let format_source () =

print_string (make_sep '-'); print_string "\n";

- let result = _lexp_str_decls (!_ppctx) (List.flatten lexps) in + let result = _lexp_str_decls (!ppctx) (List.flatten lexps) in

- if (!_write_file) then ( - print_string (" " ^ " Writing output file: " ^ (!_format_dest) ^ "\n"); - let file = open_out (!_format_dest) in + if (!write_file) then ( + print_string (" " ^ " Writing output file: " ^ (!format_dest) ^ "\n"); + let file = open_out (!format_dest) in

List.iter (fun str -> output_string file str) result;

@@ -226,7 +209,7 @@ let main () = if arg_n == 1 then (Arg.usage (Arg.align arg_defs) usage)

- else if (!_format_mode) then ( + else if (!format_mode) then ( format_source () ) else( @@ -320,7 +303,7 @@ let main () = let rctx = (try eval_decls_toplevel clean_lxp rctx; with e -> print_string reset; - print_rte_ctx (!_global_eval_ctx); + print_rte_ctx (!global_eval_ctx); print_eval_trace None; raise e) in print_string reset;

===================================== src/elab.ml ===================================== @@ -64,7 +64,7 @@ module EL = Elexp (* dummies *) let dloc = dummy_location

-let _parsing_internals = ref false +let parsing_internals = ref false let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl" @@ -107,9 +107,7 @@ let get_special_form name =

(* Used for sform_load because sform are * added before default context's function. *) -let _sform_default_ectx = ref empty_elab_context -let _set_default_ectx ectx = - _sform_default_ectx := ectx +let sform_default_ectx = ref empty_elab_context

(* The prefix `elab_check_` is used for functions which do internal checking * (i.e. errors signalled here correspond to internal errors rather than @@ -272,6 +270,12 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | _ -> sexp_error loc "define-operator expects 3 argument"; ctx

+let sform_dummy_ret ctx loc = + let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in + (newMetavar (ectx_to_lctx ctx) dummy_scope_level + (loc, Some "special-form-error") t, + Inferred t) + let elab_varref ctx (loc, name) = try let idx = senv_lookup name ctx in @@ -279,7 +283,14 @@ let elab_varref ctx (loc, name) 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 + with Senv_Lookup_Fail xs -> + (let relateds = + if ((List.length xs) > 0) then + ". Did you mean: " ^ (String.concat " or " xs) ^" ?" + else "" in + sexp_error loc ("The variable: `" ^ name ^ + "` was not declared" ^ relateds); + sform_dummy_ret ctx loc)

(* Turn metavar into plain vars after generalization. *) let rec meta_to_var ids o (e : lexp) = @@ -1177,12 +1188,6 @@ and get_attribute ctx loc largs = try Some (AttributeMap.find var map) with Not_found -> None

-and sform_dummy_ret ctx loc = - let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in - (newMetavar (ectx_to_lctx ctx) dummy_scope_level - (loc, Some "special-form-error") t, - Inferred t) - and sform_get_attribute ctx loc (sargs : sexp list) ot = match get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) with | Some e -> (e, Lazy) @@ -1222,7 +1227,7 @@ let sform_decltype ctx loc sargs ot = let builtin_value_types : ltype option SMap.t ref = ref SMap.empty

let sform_built_in ctx loc sargs ot = - match !_parsing_internals, sargs with + match !parsing_internals, sargs with | true, [String (_, name)] -> (match ot with | Some ltp @@ -1403,17 +1408,7 @@ let sform_identifier ctx loc sargs ot = match ot with Some _ -> Checked | None -> Lazy)

(* Normal identifier. *) - | [Symbol id] - -> (try elab_varref ctx id - with Senv_Lookup_Fail xs -> - (let (loc, name) = id in - 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)) + | [Symbol id] -> elab_varref ctx id

| [se] -> (sexp_error loc ("Non-symbol passed to ##typer-identifier"); @@ -1564,7 +1559,7 @@ let lexp_print_var_info ctx = print_string "\n") done

-let _in_pervasive = ref true +let in_pervasive = ref true

(* arguments : elab_context from where load is called, @@ -1584,16 +1579,16 @@ let sform_load usr_elctx loc sargs ot =

(* read file as elab_context *) let ld_elctx = match sargs with - | [String (_,file_name)] -> if !_in_pervasive then + | [String (_,file_name)] -> if !in_pervasive then read_file file_name usr_elctx else - read_file file_name !_sform_default_ectx - | _ -> (error loc "argument to load should be one file name (String)"; !_sform_default_ectx) in + read_file file_name !sform_default_ectx + | _ -> (error loc "argument to load should be one file name (String)"; !sform_default_ectx) in

(* get lexp_context *) let usr_lctx = ectx_to_lctx usr_elctx in let ld_lctx = ectx_to_lctx ld_elctx in - let dflt_lctx = ectx_to_lctx !_sform_default_ectx in + let dflt_lctx = ectx_to_lctx !sform_default_ectx in

(* length of some lexp_context *) let usr_len = M.length usr_lctx in @@ -1602,12 +1597,12 @@ let sform_load usr_elctx loc sargs ot = (* create a tuple from context and shift it to user context * * also check if we are in pervasive in which case * * we want to load in the current context rather than the default *) - let tuple = if !_in_pervasive then + let tuple = if !in_pervasive then OL.ctx2tup usr_lctx ld_lctx else OL.ctx2tup dflt_lctx ld_lctx in

- let tuple' = if !_in_pervasive then + let tuple' = if !in_pervasive then tuple else (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in @@ -1686,7 +1681,7 @@ let default_ectx (!BI.lmap) lctx in

(* read base file *) - let lctx = dynamic_bind _parsing_internals true + let lctx = dynamic_bind parsing_internals true (fun () -> read_file (btl_folder ^ "/builtins.typer") lctx) in @@ -1699,10 +1694,10 @@ let default_ectx

builtin_size := get_size lctx; - let lctx = dynamic_bind _in_pervasive true + let ectx = dynamic_bind in_pervasive true (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in - let _ = _set_default_ectx lctx in - lctx + let _ = sform_default_ectx := ectx in + ectx with (Stop_Compilation _) -> fatal dloc "compilation stopped in default context"

let default_rctx = EV.from_ectx default_ectx @@ -1710,28 +1705,23 @@ let default_rctx = EV.from_ectx default_ectx (* String Parsing * --------------------------------------------------------- *)

-(* Lexp helper *) -let _lexp_expr_str (str: string) (tenv: token_env) - (grm: grammar) (limit: string option) (ctx: elab_context) = - let pxps = _sexp_parse_str str tenv grm limit in - let lexps = lexp_parse_all pxps ctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) - lexps; - lexps - - -(* specialized version *) let lexp_expr_str str ctx = - try _lexp_expr_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx - with Stop_Compilation s -> (print_string s; []) - -let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) = - let sdecls = _sexp_parse_str str tenv grm limit in - lexp_p_decls sdecls ctx + try let tenv = default_stt in + let grm = ectx_get_grammar ctx in + let limit = Some ";" in + let pxps = sexp_parse_str str tenv grm limit in + let lexps = lexp_parse_all pxps ctx in + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) + lexps; + lexps + with Stop_Compilation s -> (print_string s; [])

-(* specialized version *) let lexp_decl_str str ctx = - try _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + try let tenv = default_stt in + let grm = ectx_get_grammar ctx in + let limit = Some ";" in + let sdecls = sexp_parse_str str tenv grm limit in + lexp_p_decls sdecls ctx with Stop_Compilation s -> (print_string s; ([],ctx))

@@ -1739,12 +1729,10 @@ let lexp_decl_str str ctx = * --------------------------------------------------------- *) (* Because we cant include Elab in eval.ml *)

-let _eval_expr_str str lctx rctx silent = - let lxps = lexp_expr_str str lctx in - let elxps = List.map OL.erase_type lxps in - (EV.eval_all elxps rctx silent) - -let eval_expr_str str lctx rctx = try _eval_expr_str str lctx rctx false +let eval_expr_str str lctx rctx = + try let lxps = lexp_expr_str str lctx in + let elxps = List.map OL.erase_type lxps in + EV.eval_all elxps rctx false with Stop_Compilation s -> (print_string s; [])

let eval_decl_str str lctx rctx =

===================================== src/eval.ml ===================================== @@ -52,9 +52,9 @@ module Prelexer = Prelexer (* prelex_string *) type eval_debug_info = elexp list * elexp list

let dloc = dummy_location -let _global_eval_trace = ref ([], []) -let _global_eval_ctx = ref make_runtime_ctx -let _eval_max_recursion_depth = ref 23000 +let global_eval_trace = ref ([], []) +let global_eval_ctx = ref make_runtime_ctx +(* let eval_max_recursion_depth = ref 23000 *)

let builtin_functions = ref (SMap.empty : ((location -> eval_debug_info @@ -68,14 +68,14 @@ let add_builtin_function name f arity = let append_eval_trace trace (expr : elexp) = let (a, b) = trace in let r = expr::a, b in - _global_eval_trace := r; r + global_eval_trace := r; r

let append_typer_trace trace (expr : elexp) = let (a, b) = trace in let r = (a, expr::b) in - _global_eval_trace := r; r + global_eval_trace := r; r

-let get_trace () = !_global_eval_trace +let get_trace () = !global_eval_trace

let rec_depth trace = let (a, b) = trace in @@ -105,7 +105,7 @@ let debug_messages error_type loc message messages = error_type loc (msg ^ "\n")

let root_string () = - let a, _ = !_global_eval_trace in + let a, _ = !global_eval_trace in match List.rev a with | [] -> "" | e::_ -> elexp_string e @@ -136,9 +136,9 @@ let tunit = Vcons ((dloc, "unit"), []) Another solution could be to define a function in elaboration step and then undefine it. The thing is elab_context may not exist at runtime so I must save it somewhere if the Elab.* function persist. *) -let _last_elab_context = ref empty_elab_context +let macro_monad_elab_context = ref empty_elab_context

-let set_getenv (ectx : elab_context) = _last_elab_context := ectx +let set_getenv (ectx : elab_context) = macro_monad_elab_context := ectx

(* * Builtins @@ -311,7 +311,7 @@ let parser_custom loc depth args_val = match args_val with

let parser_newest loc depth args_val = match args_val with | [Vsexp (Block (_,toks,_))] -> - let grm = ectx_get_grammar (!_last_elab_context) in + let grm = ectx_get_grammar (!macro_monad_elab_context) in o2v_list (sexp_parse_all_to_list grm (Lexer.lex default_stt toks) (Some ";")) | [s] -> (warning loc "Parser.newest do nothing without a Block"; s) | _ -> error loc "Parser.newest expects a Block as argument" @@ -372,13 +372,13 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type

(* This creates an O(N^2) cost for deep recursion because rec_depth * uses `length` on the stack trace. *) - (* (if (rec_depth trace) > (!_eval_max_recursion_depth) then + (* (if (rec_depth trace) > (!eval_max_recursion_depth) then * fatal (elexp_location lxp) "Recursion Depth exceeded"); *)

(* Save current trace in a global variable. If an error occur, we will be able to retrieve the most recent trace and context *) - _global_eval_ctx := ctx; - _global_eval_trace := trace; + global_eval_ctx := ctx; + global_eval_trace := trace;

match lxp with (* Leafs *) @@ -625,7 +625,7 @@ and print_typer_trace' trace =

let _ = List.iteri (fun i expr -> print_string " "; - Fmt._print_ct_tree i; print_string "+- "; + Fmt.print_ct_tree i; print_string "+- "; print_string ((elexp_string expr) ^ "\n")) trace in

print_string (Fmt.make_sep '=') @@ -633,7 +633,7 @@ and print_typer_trace' trace = and print_typer_trace trace = match trace with | Some t -> print_typer_trace' t - | None -> let (a, b) = !_global_eval_trace in + | None -> let (a, b) = !global_eval_trace in print_typer_trace' b

and print_trace title trace default = @@ -651,7 +651,7 @@ and print_trace title trace default = print_string (" [" ^ (loc_string (type_loc expr)) ^ "] ");

(* Print call trace visualization *) - Fmt._print_ct_tree i; print_string "+- "; + Fmt.print_ct_tree i; print_string "+- ";

(* Print element *) print_string ((type_name expr) ^ ": " ^ (type_string expr) ^ "\n") @@ -666,7 +666,7 @@ and print_trace title trace default = print_string (Fmt.make_sep '=')

and print_eval_trace trace = - let (a, b) = !_global_eval_trace in + let (a, b) = !global_eval_trace in print_trace " EVAL TRACE " trace a

let io_bind loc depth args_val = @@ -747,7 +747,7 @@ let gensym = let count = ref 0 in | _ -> error loc "gensym takes a Unit as argument")

let getenv loc depth args_val = match args_val with - | [v] -> Vcommand (fun () -> Velabctx !_last_elab_context) + | [v] -> Vcommand (fun () -> Velabctx !macro_monad_elab_context) | _ -> error loc "getenv takes a single Unit as argument"

let debug_doc loc depth args_val = match args_val with @@ -1053,7 +1053,7 @@ let eval lxp ctx = _eval lxp ctx ([], []) let debug_eval lxp ctx = try eval lxp ctx with e -> ( - print_rte_ctx (!_global_eval_ctx); + print_rte_ctx (!global_eval_ctx); print_eval_trace None; raise e)

===================================== src/fmt.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -117,7 +117,7 @@ let make_sep c = " " ^ (make_line c 76) ^ "\n"

(* used to help visualize the call trace *) -let _print_ct_tree i = +let print_ct_tree i = let rec loop j = if j = i then () else match j with

===================================== src/lexer.ml ===================================== @@ -1,6 +1,6 @@ (* lexer.ml --- Second half of lexical analysis of Typer.

-Copyright (C) 2011-2017 Free Software Foundation, Inc. +Copyright (C) 2011-2018 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -144,16 +144,11 @@ let lex tenv (pts : pretoken list) : sexp list = in gettokens pts bpos cpos (tok :: acc) in gettokens pts 0 0 []

-let _lex_str (str: string) tenv = +let lex_str (str: string) tenv = let pretoks = prelex_string str in lex tenv pretoks

-let lex_str str = _lex_str str default_stt - -let _sexp_parse_str (str: string) tenv grm limit = - let toks = _lex_str str tenv in +let sexp_parse_str (str: string) tenv grm limit = + let toks = lex_str str tenv in sexp_parse_all_to_list grm toks limit

-let sexp_parse_str str = - _sexp_parse_str str default_stt default_grammar (Some ";") -

===================================== src/lexp.ml ===================================== @@ -705,9 +705,11 @@ and _lexp_str ctx (exp : lexp) : string = let fun_call str = cyan ^ str ^ reset in

let index idx = - let _index idx = if pp_dbi ctx then ("[" ^ (string_of_int idx) ^ "]") else "" in - let str = _index idx in if idx < 0 then (error str) else - (green ^ str ^ reset) in + let str = if pp_dbi ctx + then ("[" ^ (string_of_int idx) ^ "]") + else "" in + if idx < 0 then error str + else green ^ str ^ reset in

let kind_str k = match k with | Aexplicit -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in

===================================== tests/sexp_test.ml ===================================== @@ -2,8 +2,12 @@ open Sexp open Lexer open Utest_lib

+let sexp_parse_str dcode + = sexp_parse_str dcode Grammar.default_stt Grammar.default_grammar (Some ";") + let test_sexp_add dcode testfun = - add_test "SEXP" dcode (fun () -> testfun (sexp_parse_str dcode)) + add_test "SEXP" dcode + (fun () -> testfun (sexp_parse_str dcode))

let _ = test_sexp_add "lambda x -> x + x" (fun ret -> match ret with

View it on GitLab: https://gitlab.com/monnier/typer/commit/32ef5ef1be1bb09c350aab9df82b49d3771a...