[Git][monnier/typer][master] Integrate misc changes from the ift3065 assignments
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...
Afficher les réponses par date
participants (1)
-
Stefan