Stefan pushed to branch master at Stefan / Typer

Commits: 117d4d4c by Stefan Monnier at 2017-02-27T16:19:00-05:00 Integrate misc changes from the ift3065 assignments

* btl/pervasive.typer (List_foldl): New function. * btl/list.typer: Remove.

* emacs/typer-mode.el (typer-font-lock-keywords): Highlight "keywords".

* src/REPL.ml (arg_batch): New var. (arg_defs): Add --batch arg. (main): Obey it.

* src/elexp.ml (elexp_string): Print data constructors more explicitly.

* src/env.ml (env_cell): Remove.

* src/eval.ml (_eval, io_run): Silence compiler warnings.

- - - - -

7 changed files:

- − btl/list.typer - btl/pervasive.typer - emacs/typer-mode.el - src/REPL.ml - src/elexp.ml - src/env.ml - src/eval.ml

Changes:

===================================== btl/list.typer deleted ===================================== --- a/btl/list.typer +++ /dev/null @@ -1,9 +0,0 @@ -accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; -accumulate = lambda (t : Type) ≡> - lambda (acc-op : (t -> t -> t)) -> - lambda (init : t) -> - lambda (list : List t) -> - case list - | cons hd tl => accumulate acc-op (acc-op init hd) tl - | nil => init; -

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -86,6 +86,11 @@ List_map = lambda a b ≡> lambda f xs -> case xs | nil => nil | cons x xs => cons (f x) (List_map f xs);

+List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; +List_foldl = lambda a b ≡> lambda f i xs -> case xs + | nil => i + | cons x xs => List_foldl f (f i x) xs; + %%%% Quasi-Quote macro

%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"])

===================================== emacs/typer-mode.el ===================================== --- a/emacs/typer-mode.el +++ b/emacs/typer-mode.el @@ -56,7 +56,10 @@ "Syntax table for `typer-mode'.")

(defvar typer-font-lock-keywords - '(("deftoken[ \t]+\([^ \t\n]+\)" (1 font-lock-function-name-face)) + `(("deftoken[ \t]+\([^ \t\n]+\)" (1 font-lock-function-name-face)) + (,(concat "\_<" (regexp-opt '("type" "case" "lambda" "let" "in")) "\_>") + (0 font-lock-keyword-face)) + ("\_<type[ \t]+\([^ \t\n]+\)" (1 font-lock-function-name-face)) ("^\([^() \t]+\)[ \t]" (1 font-lock-function-name-face)) ("^%%\(%+\)\(?:.* ---\)?\(.*\)" (2 (typer--section-face (- (match-end 1) (match-beginning 1))) prepend))

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -60,6 +60,8 @@ module EL = Elexp (* how to handle arrow keys ? *) let _history = ref []

+let arg_batch = ref false + let print_input_line i = print_string " In["; ralign_print_int i 2; @@ -163,6 +165,12 @@ let _raw_eval f str lctx rctx = let pxps = pexp_decls_all nods in let lxps, lctx = lexp_p_decls pxps lctx in let elxps = List.map OL.clean_decls lxps in + (* At this point, `elxps` is a `(vname * elexp) list list`, where: + * - each `(vname * elexp)` is a definition + * - each `(vname * elexp) list` is a list of definitions which can + * refer to each other (i.e. they can be mutually recursive). + * - hence the overall "list of lists" is a sequence of such + * blocs of mutually-recursive definitions. *) let rctx = eval_decls_toplevel elxps rctx in (* This is for consistency with ieval *) [], lctx, rctx @@ -258,6 +266,8 @@ let arg_files = ref []

(* ./typer [options] files *) let arg_defs = [ + ("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) (*"-I", Arg.String (fun f -> searchpath := f::!searchpath), "Append a directory to the search path"*) @@ -272,17 +282,20 @@ let main () = let ectx = default_ectx in let rctx = default_rctx in

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

- let (i, ectx, rctx) = readfiles (List.rev !arg_files) (1, ectx, rctx) true in + let (i, ectx, rctx) = readfiles (List.rev !arg_files) (1, ectx, rctx) + (not !arg_batch) in

flush stdout;

- (* Initiate REPL. This will allow us to inspect interpreted code *) - repl i ectx rctx + if not !arg_batch then + (* Initiate REPL. This will allow us to inspect interpreted code *) + repl i ectx rctx

let _ = main ()

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -136,7 +136,7 @@ and elexp_string lxp = | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), i) -> s ^ "[" ^ string_of_int i ^ "]" - | Cons((_, s)) -> s + | Cons((_, s)) -> "datacons(" ^ s ^")"

| Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_string b)

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -62,8 +62,7 @@ type value_type = | Vcommand of (unit -> value_type)

(* Runtime Environ *) - and env_cell = (string option * (value_type ref)) - and runtime_env = env_cell M.myers + and runtime_env = (string option * (value_type ref)) M.myers

let rec value_equal a b = match a, b with

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -243,13 +243,12 @@ let file_write loc depth args_val = match args_val with let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) =

let trace = append_eval_trace trace lxp in - let tloc = elexp_location lxp in let eval lxp ctx = _eval lxp ctx trace in

(* 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 - * fatal tloc "Recursion Depth exceeded"); *) + * 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 *) @@ -551,7 +550,7 @@ let io_bind loc depth args_val = | _ -> error loc "Wrong number of args or wrong first arg value in `IO.bind`"

let io_run loc depth args_val = match args_val with - | [Vcommand cmd; v] -> cmd (); v + | [Vcommand cmd; v] -> let _ = cmd () in v | _ -> error loc "IO.run expects a monad and a function as arguments"

let io_return loc depth args_val = match args_val with @@ -641,8 +640,8 @@ let eval_decls decls ctx = _eval_decls decls ctx ([], [])

let eval_decls_toplevel (decls: (vname * elexp) list list) ctx = (* Add toplevel decls function *) - List.fold_left (fun ctx decls -> - eval_decls decls ctx) ctx decls + List.fold_left (fun ctx decls -> eval_decls decls ctx) + ctx decls

(* Eval a list of lexp *) let eval_all lxps rctx silent =

View it on GitLab: https://gitlab.com/monnier/typer/commit/117d4d4c273732fda47cc502c50f834e25ce...