Simon Génier pushed to branch simon--pp-print-value at Stefan / Typer

Commits: d1c43a74 by Simon Génier at 2023-03-16T14:48:16-04:00 Use format to print values.

- - - - - b61ab4c1 by Simon Génier at 2023-03-16T14:48:20-04:00 Oops: missing closing parenthesis when printing an inductive type.

- - - - - 5275c788 by Simon Génier at 2023-03-16T14:49:49-04:00 Cosmetic changes to Env.

* Give associated functions names more in line with those of containers in Stdlib. * Merge a try and a match.

- - - - - fe6e8b28 by Simon Génier at 2023-03-16T14:49:54-04:00 Rename Elexp.elexp to Elexp.t.

Its shorter and nicer?

- - - - -

13 changed files:

- debug_util.ml - src/builtin.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/gambit.ml - src/heap.ml - src/lexp.ml - src/opslexp.ml - tests/env_test.ml - tests/eval_test.ml - tests/utest_lib.ml

Changes:

===================================== debug_util.ml ===================================== @@ -48,7 +48,6 @@ open Grammar

(* environments *) open Debruijn -open Env

(* Argument parsing *) let arg_print_options = ref SMap.empty @@ -158,13 +157,13 @@ let main () = let rctx = (try eval_decls_toplevel clean_lxp rctx; with e -> print_string reset; - print_rte_ctx (!global_eval_ctx); + Env.print_rctx ~start:0 (!global_eval_ctx); print_eval_trace None; raise e) in print_string reset;

(if (get_p_option "rctx") then( - print_rte_ctx rctx; print_string "\n")); + Env.print_rctx ~start:0 rctx));

(* Eval Each Expression *) print_string (make_title " Eval Print "); @@ -174,7 +173,7 @@ let main () = let main = (senv_lookup "main" nctx) in

(* get main body *) - let body = (get_rte_variable (dsinfo, Some "main") main rctx) in + let body = Env.find main rctx in

(* eval main *) print_eval_result 1 body

===================================== src/builtin.ml ===================================== @@ -126,8 +126,8 @@ let v2o_list v = | _ -> log_raise_error ~loc:(E.value_location v) - "Failed to convert the %s with value:\n%s\n to a list." - (E.value_name v) (E.value_string v) + "Failed to convert to a list:\n%s\n" + (Env.string_of_value v) in v2o_list [] v

===================================== src/elab.ml ===================================== @@ -85,12 +85,10 @@ let indent_line str = " > " ^ str let print_indent_line str = print_endline (indent_line str) -let print_details to_name to_str elem = - print_indent_line ((to_name elem) ^ ": " ^ (to_str elem)) let lexp_print_details lexp () = print_indent_line (Lexp.to_string lexp) let value_print_details value () = - print_details value_name value_string value + print_indent_line (Env.string_of_value value)

let lexp_error loc lexp fmt = error ~loc ~print_action:(lexp_print_details lexp) fmt

===================================== src/elexp.ml ===================================== @@ -34,7 +34,7 @@ open Sexp

module SMap = Util.SMap

-type elexp = +type t = (* A constant, either string, integer, or float. *) | Imm of sexp

@@ -44,18 +44,18 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref

- | Proj of Source.Location.t * elexp * int + | Proj of Source.Location.t * t * int

(* Recursive `let` binding. *) - | Let of Source.Location.t * eldecls * elexp + | Let of Source.Location.t * decls * t

(* An anonymous function. *) - | Lambda of vname * elexp + | Lambda of vname * t

(* A (curried) function call. * In other words, Call(f, [e1, e2]) * is just a shorthand for Call (Call (f, [e1]), [e2]). *) - | Call of elexp * elexp list + | Call of t * t list

(* A data constructor, such as `cons` or `nil`. The int is its arity and the * symbol, its name. *) @@ -66,18 +66,18 @@ type elexp = * tests the value of `e`, and either selects the corresponding branch * in `branches` or branches to the `default`. *) | Case of Source.Location.t - * elexp - * (Source.Location.t * vname list * elexp) SMap.t - * (vname * elexp) option + * t + * (Source.Location.t * vname list * t) SMap.t + * (vname * t) option

(* A Type expression. There's no useful operation we can apply to it, * but they can appear in the code. *) | Type of Lexp.lexp

-and eldecl = vname * elexp -and eldecls = eldecl list +and decl = vname * t +and decls = decl list

-let rec location : elexp -> Source.Location.t = function +let rec location : t -> Source.Location.t = function | Imm s -> Sexp.location s | Var ((l, _), _) -> Sexp.location l | Proj (l, _, _) -> l @@ -89,7 +89,7 @@ let rec location : elexp -> Source.Location.t = function | Case (l, _, _, _) -> l | Type (e) -> Lexp.location e

-let rec pp_print (f : Format.formatter) (e : elexp) : unit = +let rec pp_print (f : Format.formatter) (e : t) : unit = let open Format in match e with | Imm (value) @@ -130,9 +130,9 @@ let rec pp_print (f : Format.formatter) (e : elexp) : unit = | Type (e) -> fprintf f "Type(%a)" Lexp.pp_print e

-and pp_print_decl_block (f : Format.formatter) (decls : eldecls) : unit = +and pp_print_decl_block (f : Format.formatter) (decls : decls) : unit = let open Format in - let pp_print_decl (f : Format.formatter) (name, body : eldecl) : unit = + let pp_print_decl (f : Format.formatter) (name, body : decl) : unit = fprintf f "@[<hov 2>%s =@ %a;@]" (string_of_vname name) pp_print body in fprintf @@ -141,7 +141,7 @@ and pp_print_decl_block (f : Format.formatter) (decls : eldecls) : unit = (pp_print_list ~pp_sep:pp_print_space pp_print_decl) decls

-let pp_print_decls (f : Format.formatter) (eldecls : eldecls list) : unit = +let pp_print_decls (f : Format.formatter) (eldecls : decls list) : unit = let open Format in fprintf f @@ -149,5 +149,5 @@ let pp_print_decls (f : Format.formatter) (eldecls : eldecls list) : unit = (pp_print_list ~pp_sep:pp_print_cut pp_print_decl_block) eldecls

-let to_string : elexp -> string = +let to_string : t -> string = Format.asprintf "%a" pp_print

===================================== src/env.ml ===================================== @@ -30,9 +30,6 @@ * * --------------------------------------------------------------------------- *)

-open Elexp -open Fmt (* make_title, table util *) -open Printf open Sexp

module M = Myers @@ -43,8 +40,6 @@ let fatal ?print_action ?loc fmt = let warning ?print_action ?loc fmt = Log.log_warning ~section:"ENV" ?print_action ?loc fmt

-let str_idx idx = "[" ^ (string_of_int idx) ^ "]" - type value = | Vint of int | Vinteger of Z.t @@ -52,7 +47,7 @@ type value = | Vcons of symbol * value list | Vbuiltin of string | Vfloat of float - | Closure of vname * elexp * runtime_env + | Closure of vname * Elexp.t * runtime_env | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vundefined @@ -67,6 +62,8 @@ type value = (* Runtime Environ *) and runtime_env = (vname * value ref) M.myers

+let empty = M.nil + let rec value_equal a b = match a, b with | Vint (i1), Vint (i2) -> i1 = i2 @@ -103,144 +100,105 @@ let rec value_equal a b =

| _ -> false

-let rec value_eq_list a b = - match a, b with - | [], [] -> true - | v1::vv1, v2::vv2 -> value_equal v1 v2 && value_eq_list vv1 vv2 - | _ -> false - let value_location : value -> Source.Location.t = function | Vcons ((loc, _), _) -> loc | Closure (_, lxp, _) -> Elexp.location lxp (* location info was lost or never existed *) | _ -> Source.Location.dummy

-let rec value_name v = - match v with - | Vin _ -> "Vin" - | Vout _ -> "Vout" - | Vint _ -> "Vint" - | Vinteger _ -> "Vinteger" - | Vsexp _ -> "Vsexp" - | Vtype _ -> "Vtype" - | Vcons _ -> "Vcons" - | Vfloat _ -> "Vfloat" - | Vundefined -> "Vundefined" - | Vstring _ -> "Vstring" - | Closure _ -> "Closure" - | Vbuiltin _ -> "Vbuiltin" - | Vcommand _ -> "Vcommand" - | Vref v -> ("Vref of "^(value_name (!v))) - | Velabctx _ -> ("Velabctx") - | Varray _ -> ("Varray") - -let rec value_string v = - match v with - | Vin _ -> "in_channel" - | Vout _ -> "out_channel" - | Vundefined -> "<undefined!>" - | Vcommand _ -> "command" - | Vstring s -> """ ^ s ^ """ - | Vbuiltin s -> s - | Vint i -> string_of_int i - | Vinteger i -> Z.to_string i - | Vfloat f -> string_of_float f - | Vsexp s -> Sexp.to_string s - | Vtype e -> Lexp.to_string e - | Closure ((_, s), elexp, _) - -> "(lambda " ^ Lexp.maybename s ^ " -> " ^ Elexp.to_string elexp ^ ")" - | Vcons ((_, s), lst) - -> let args = List.fold_left - (fun str v -> str ^ " " ^ value_string v) - "" lst in - "(" ^ s ^ args ^ ")" - | Vref (v) -> ("Ref of "^(value_string (!v))) - | Velabctx _ -> ("Velabctx") - | Varray a -> if ( (Array.length a) = 0 ) - then "[]" - else ( let - str = (Array.fold_left - (fun str v -> (str^(value_string v)^";")) "" a) - in ("["^(String.sub str 0 ((String.length str) - 1))^"]") ) - -let value_print (vtp: value) = print_string (value_string vtp) - -let make_runtime_ctx = M.nil - -let get_rte_size (ctx: runtime_env): int = M.length ctx - -let print_myers_list l print_fun start = - let n = (M.length l) - 1 in - print_string (make_title " ENVIRONMENT "); - make_rheader [(None, "INDEX"); - (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; - print_string (make_sep '-'); - - for i = start to n do - printf " | %5d | " (n -i); - print_fun (M.nth (n - i) l); - done; - print_string (make_sep '=') - -let print_rte_ctx_n (ctx: runtime_env) start = - print_myers_list - ctx - (fun (n, vref) -> - let g = !vref in - let _ = - match n with - | (_, Some m) -> Printf.printf "%-12s | " m - | _ -> print_string (make_line ' ' 12); print_string " | " in - - value_print g; print_string "\n") start - -(* Only print user defined variables *) -let print_rte_ctx ctx = - print_rte_ctx_n ctx (!Lexp.builtin_size) - -(* Dump the whole context *) -let dump_rte_ctx ctx = - print_rte_ctx_n ctx 0 - -let get_rte_variable (name: vname) (idx: int) - (ctx: runtime_env): value = - try - let (defname, ref_cell) = (M.nth idx ctx) in - let x = !ref_cell in - match (defname, name) with - | ((_, Some n1), (_, Some n2)) - -> if n1 = n2 - then x - else - fatal - ~print_action:(fun () -> dump_rte_ctx ctx) - {|Variable lookup failure. Expected "%s[%d]" got "%s"|} n2 idx n1 - | _ -> x - with - | Not_found - -> let n = match name with (_, Some n) -> n | _ -> "" in - fatal {|Variable lookup failure. Var: "%s" idx: %d|} n idx - -let add_rte_variable (name:vname) (x: value) (ctx: runtime_env) - : runtime_env = - let valcell = ref x in - M.cons (name, valcell) ctx - -let set_rte_variable idx name (v: value) (ctx : runtime_env) = - let (n, ref_cell) = (M.nth idx ctx) in - - (match (n, name) with - | ((_, Some n1), (_, Some n2)) when n1 != n2 - -> fatal {|Variable names must match: "%s" vs "%s"|} n1 n2 - | _ -> ()); - - ref_cell := v - -(* Select the n first variable present in the env *) -let nfirst_rte_var n ctx = - let rec loop i acc = - if i < n then - loop (i + 1) ((get_rte_variable Lexp.vdummy i ctx)::acc) - else - List.rev acc in - loop 0 [] +let rec pp_print_value (f : Format.formatter) : value -> unit = + let open Format in + function + | Vin _ -> pp_print_string f "#<in_channel>" + | Vout _ -> pp_print_string f "#<out_channel>" + | Vundefined -> pp_print_string f "#<undefined!>" + | Vcommand _ -> pp_print_string f "#<command>" + | Velabctx _ -> pp_print_string f "#<elabctx>" + | Vstring (value) -> fprintf f "%S" value + | Vbuiltin (name) -> fprintf f "##%s" name + | Vint (value) -> pp_print_int f value + | Vinteger (value) -> Z.pp_print f value + | Vfloat (value) -> pp_print_float f value + | Vsexp (value) -> Sexp.pp_print f value + | Vtype (value) -> Lexp.pp_print f value + | Vref (value) -> fprintf f "Ref of %a" pp_print_value !value + + | Closure (param, body, _) + -> fprintf + f "@[<hov 1>(lambda %a ->@ %a)@]" + (Sexp.pp_print_vname ~default:"_") param + Elexp.pp_print body + + | Vcons (name, fields) + -> fprintf f "@[<hov 1>(%a" Sym.pp_print name; + List.iter (fun field -> fprintf f "@ %a" pp_print_value field) fields; + fprintf f ")@]" + + | Varray (elements) + -> fprintf + f "@[<hov 1>[%a]@]" + (pp_print_list ~pp_sep:(fun f () -> fprintf f ";@ ") pp_print_value) + (Array.to_list elements) + +let print_value : value -> unit = + Format.printf "%a" pp_print_value + +let string_of_value : value -> string = + Format.asprintf "%a" pp_print_value + +let pp_print_rctx + (f : Format.formatter) ~(start : int) (rctx : runtime_env) + : unit = + + let open Format in + pp_print_string f (Fmt.make_title "Environment"); + for i = start to Myers.length rctx - 1 do + let name, value = Myers.nth i rctx in + fprintf + f "@[<hov 2>%a =@ %a;@]@." + (Sexp.pp_print_vname ~default:"_") name + pp_print_value !value + done; + pp_print_string f (Fmt.make_sep '=') + +let print_rctx ~(start : int) : runtime_env -> unit = + Format.printf "%a" (pp_print_rctx ~start) + +(** Finds the [n]th entry. If provided, the name is checked against the one + recorded to mitigate Debruijn index errors. Mutating the resulting ref + {e will} mutate the environment. *) +let find_entry ?(name : vname option) (idx : int) (rctx : runtime_env) : value ref = + let name = Option.bind name (fun (_, y) -> y) in + match Myers.nth idx rctx, name with + | exception Not_found + -> fatal + {|Variable lookup failure. Var: "%s" idx: %d|} + (Lexp.maybename name) + idx + + | ((_, Some actual), _), Some expected when actual <> expected + -> fatal + ~print_action:(fun () -> Format.printf "%a@." (pp_print_rctx ~start:0) rctx) + {|Variable lookup failure. Expected "%s[%d]" got "%s"|} + expected + idx + actual + + | (_, entry), _ -> entry + +(** Like [find_entry], but returns the value directly. *) +let find ?(name : vname option) (idx : int) (rctx : runtime_env) : value = + !(find_entry ?name idx rctx) + +(** Creates a new environment with one additional binding. *) +let cons (name : vname) (x : value) (rctx : runtime_env) : runtime_env = + Myers.cons (name, ref x) rctx + +(** Selects the n first variable present in the env. *) +let take n ctx = + let rec loop i acc = + if i < n + then loop (i + 1) (find i ctx :: acc) + else List.rev acc + in + loop 0 []

===================================== src/eval.ml ===================================== @@ -44,11 +44,11 @@ open Env open Printf (* IO Monad *) module OL = Opslexp

-type eval_debug_info = elexp list * elexp list +type eval_debug_info = Elexp.t list * Elexp.t list

let dloc = dummy_location let global_eval_trace = ref ([], []) -let global_eval_ctx = ref make_runtime_ctx +let global_eval_ctx = ref Env.empty (* let eval_max_recursion_depth = ref 23000 *)

type builtin_function = @@ -60,12 +60,12 @@ let builtin_functions : (builtin_function * int) SMap.t ref = ref SMap.empty let add_builtin_function name (f : builtin_function) arity = builtin_functions := SMap.add name (f, arity) (!builtin_functions)

-let append_eval_trace trace (expr : elexp) = +let append_eval_trace trace (expr : Elexp.t) = let (a, b) = trace in let r = expr::a, b in global_eval_trace := r; r

-let append_typer_trace trace (expr : elexp) = +let append_typer_trace trace (expr : Elexp.t) = let (a, b) = trace in let r = (a, expr::b) in global_eval_trace := r; r @@ -110,12 +110,11 @@ let root_string () =

let trace_value (value : value) : string = sprintf - "\t> %s : %s\n\t> Root: %s\n" - (value_name value) - (value_string value) + "\t> %s\n\t> Root: %s\n" + (Env.string_of_value value) (root_string ())

-let trace_elexp (elexp : elexp) : string = +let trace_elexp (elexp : Elexp.t) : string = Format.asprintf "\t>%a\n\t> Root: %s\n" Elexp.pp_print @@ -404,7 +403,7 @@ let file_read loc _depth args_val = match args_val with * or actually pay attention to the second arg. *) | [Vin channel; Vint _n] -> Vstring (input_line channel) | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; + List.iter (fun v -> Format.printf "%a@." Env.pp_print_value v) args_val; ) "File.read expects an in_channel. Actual arguments:"

@@ -414,7 +413,7 @@ let file_write loc _depth args_val = match args_val with (* FIXME: This should be the unit value! *) Vundefined) | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; + List.iter (fun v -> Format.printf "%a@." Env.pp_print_value v) args_val; ) "File.write expects an out_channel and a string. Actual arguments:"

@@ -488,7 +487,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value) =

and eval_var ctx lxp v = let ((sinfo, name as vname), idx) = v in - try get_rte_variable vname idx ctx with + try Env.find ~name:vname idx ctx with | _e -> Log.log_fatal ~loc:(Sexp.location sinfo) @@ -508,12 +507,12 @@ and eval_call loc unef i f args = -> let rec bindargs e vs ctx = match (vs, e) with | (v::vs, Lambda (x, e)) (* "Uncurry" on the fly. *) - -> bindargs e vs (add_rte_variable x v ctx) + -> bindargs e vs (Env.cons x v ctx) | ([], _) -> let trace = append_typer_trace i unef in eval e ctx trace | _ -> eval_call loc unef i (eval e ctx i) vs in - bindargs e vs (add_rte_variable x v ctx) + bindargs e vs (Env.cons x v ctx)

| Vbuiltin (name), args -> (try let (builtin, arity) = SMap.find name !builtin_functions in @@ -530,7 +529,7 @@ and eval_call loc unef i f args = else let rec buildctx args ctx = match args with | [] -> ctx - | arg::args -> buildctx args (add_rte_variable vdummy arg ctx) in + | arg::args -> buildctx args (Env.cons vdummy arg ctx) in let rec buildargs n = if n >= 0 then (Var (vdummy, n))::buildargs (n - 1) @@ -577,7 +576,7 @@ and eval_case ctx i loc target pat dflt = let rec fold2 nctx pats args = match pats, args with | pat::pats, arg::args - -> let nctx = add_rte_variable pat arg nctx in + -> let nctx = Env.cons pat arg nctx in fold2 nctx pats args (* Errors: those should not happen but they might *) (* List.fold2 would complain. we print more info *) @@ -592,7 +591,7 @@ and eval_case ctx i loc target pat dflt = (* Run default *) with Not_found -> (match dflt with | Some (var, lxp) - -> eval lxp (add_rte_variable var v ctx) i + -> eval lxp (Env.cons var v ctx) i | _ -> error loc "Match Failure")

and build_arg_list args ctx i = @@ -600,21 +599,20 @@ and build_arg_list args ctx i = let arg_val = List.map (fun (_k, e) -> eval e ctx i) args in

(* Add args inside context *) - List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val + List.fold_left (fun c v -> Env.cons vdummy v c) ctx arg_val

-and eval_decls (decls: (vname * elexp) list) - (ctx: runtime_env) i: runtime_env = +and eval_decls (decls: Elexp.decls) (ctx: runtime_env) i: runtime_env =

let n = (List.length decls) - 1 in

(* Read declarations once and push them *) let nctx = List.fold_left (fun ctx (name, _) -> - add_rte_variable name Vundefined ctx) ctx decls in + Env.cons name Vundefined ctx) ctx decls in

List.iteri (fun idx (name, lxp) -> let v = eval lxp nctx i in let offset = n - idx in - ignore (set_rte_variable offset name v nctx)) decls; + Env.find_entry ~name offset nctx := v) decls;

nctx

@@ -654,10 +652,8 @@ and sexp_dispatch loc depth args = eval_call blk [Vsexp b]

(* -------------------------------------------------------------------------- *) -and print_eval_result i lxp = - Printf.printf " Out[%02d] >> " i; - value_print lxp; - print_string "\n"; +and print_eval_result i = + Format.printf " Out[%02d] >> %a@." i Env.pp_print_value

and print_typer_trace' trace =

@@ -1104,7 +1100,7 @@ let debug_eval lxp ctx = let ectx = !global_eval_ctx in let eval_trace = fst (get_trace ()) in Log.log_info ~section:"EVAL" ~print_action:(fun _ -> - print_rte_ctx ectx; + Env.print_rctx ~start:(!Lexp.builtin_size) ectx; print_eval_trace (Some eval_trace) ) "Exception occured during evaluation in the following context:"; @@ -1112,7 +1108,7 @@ let debug_eval lxp ctx =

let eval_decls decls ctx = eval_decls decls ctx ([], [])

-let eval_decls_toplevel (decls: (vname * elexp) list list) ctx = +let eval_decls_toplevel (decls: Elexp.decls list) ctx = (* Add toplevel decls function *) List.fold_left (fun ctx decls -> eval_decls decls ctx) ctx decls @@ -1203,7 +1199,7 @@ class ast_interpreter lctx = object let elexp = Opslexp.erase_type lctx lexp in debug_eval elexp rctx

- method print_rte_ctx = Env.print_rte_ctx rctx + method print_rte_ctx = Env.print_rctx ~start:(!Lexp.builtin_size) rctx

- method dump_rte_ctx = Env.dump_rte_ctx rctx + method dump_rte_ctx = Env.print_rctx ~start:0 rctx end

===================================== src/gambit.ml ===================================== @@ -18,7 +18,6 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see http://www.gnu.org/licenses/. *)

-open Elexp open Lexp open Printf open Sexp @@ -143,7 +142,7 @@ module ScmContext = struct let name = gensym (Option.value ~default:"g" name) in (Myers.cons name sctx, name)

- let intro_binding (sctx : t) (name, elexp : vname * elexp) = + let intro_binding (sctx : t) (name, elexp : vname * Elexp.t) = let sctx, name = intro sctx name in (sctx, (name, elexp))

@@ -151,7 +150,7 @@ module ScmContext = struct Myers.nth_opt index sctx end

-let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = +let rec scheme_of_expr (sctx : ScmContext.t) (elexp : Elexp.t) : Scm.t = match elexp with | Elexp.Imm (Sexp.String (_, s)) -> Scm.String s

@@ -352,7 +351,7 @@ class pretty_printer = self#read_sized_string end

-let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * elexp) : Scm.t = +let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * Elexp.t) : Scm.t = Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp])

class gambit_compiler lctx output = object

===================================== src/heap.ml ===================================== @@ -80,7 +80,7 @@ let store_header | Env.Vcons (symbol, []) -> let constructor, _ = IMap.find address !heap in constructor := Some symbol - | _ -> error ~loc "not a data constructor: %s" (Env.value_string datacons) + | _ -> error ~loc "not a data constructor: %s" (Env.string_of_value datacons)

(** If [address] points to an object of at least [cell_index + 1] cells, mutates the value at that index. *)

===================================== src/lexp.ml ===================================== @@ -914,7 +914,8 @@ let rec pp_print (f : Format.formatter) (e, _ : lexp) : unit = pp_print_params params end; - SMap.iter pp_print_cons constructors + SMap.iter pp_print_cons constructors; + fprintf f ")@]"

| Case (_, e, _, branches, default) -> let pp_print_binding f (_, name) =

===================================== src/opslexp.ml ===================================== @@ -29,7 +29,6 @@ module P = Pexp (* open Myers *) (* open Grammar *) open Lexp -module E = Elexp module L = Lexp module M = Myers

@@ -1319,44 +1318,44 @@ let pos_of_label lctx label e : int = 0

-let rec erase_type (lctx : Lctx.t) (lxp: lexp) : E.elexp = +let rec erase_type (lctx : Lctx.t) (lxp: lexp) : Elexp.t = match lexp_lexp' lxp with - | L.Imm (s) -> E.Imm (s) - | L.Builtin (v, _) -> E.Builtin (v) - | L.Var (v) -> E.Var (v) + | L.Imm (s) -> Elexp.Imm (s) + | L.Builtin (v, _) -> Elexp.Builtin (v) + | L.Var (v) -> Elexp.Var (v) | L.Proj (l, exp, label) -> let t = get_type lctx exp in - E.Proj (Sexp.location l, erase_type lctx exp, pos_of_label lctx label t) - | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) + Elexp.Proj (Sexp.location l, erase_type lctx exp, pos_of_label lctx label t) + | L.Cons (ty, s) -> Elexp.Cons (arity_of_cons lctx ty s, s)

| L.Lambda (P.Aerasable, _, _, body) -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy))

| L.Lambda (_, vdef, ty, body) -> let lctx' = Lctx.cons lctx vdef Variable ty in - E.Lambda (vdef, erase_type lctx' body) + Elexp.Lambda (vdef, erase_type lctx' body)

| L.Let (l, decls, body) -> let lctx', edecls = clean_decls lctx decls in - E.Let (Sexp.location l, edecls, erase_type lctx' body) + Elexp.Let (Sexp.location l, edecls, erase_type lctx' body)

| L.Call (_, fct, args) - -> E.Call (erase_type lctx fct, List.filter_map (clean_arg lctx) args) + -> Elexp.Call (erase_type lctx fct, List.filter_map (clean_arg lctx) args)

| L.Case (location, target, _, branches, default) -> let etarget = erase_type lctx target in let ebranches = clean_branch_map lctx branches in - E.Case (Sexp.location location, etarget, ebranches, clean_default lctx default) + Elexp.Case (Sexp.location location, etarget, ebranches, clean_default lctx default)

| L.Susp (l, s) -> erase_type lctx (L.push_susp l s)

(* To be thrown out *) - | L.Arrow _ -> E.Type lxp - | L.SortLevel _ -> E.Type lxp - | L.Sort _ -> E.Type lxp + | L.Arrow _ -> Elexp.Type lxp + | L.SortLevel _ -> Elexp.Type lxp + | L.Sort _ -> Elexp.Type lxp

(* Still useful to some extent. *) - | L.Inductive (_, _, _, _) -> E.Type lxp + | L.Inductive (_, _, _, _) -> Elexp.Type lxp | L.Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type lctx (push_susp e s) @@ -1366,10 +1365,7 @@ and clean_arg lctx = function | (P.Aerasable, _) -> None | (_, lexp) -> Some (erase_type lctx lexp)

-and clean_decls - (lctx : Lctx.t) - (decls : ldecl list) - : Lctx.t * (vname * E.elexp) list = +and clean_decls (lctx : Lctx.t) (decls : ldecl list) : Lctx.t * Elexp.decls = let lctx' = Lctx.extend lctx decls in (lctx', List.map (fun (v, lexp, _) -> (v, erase_type lctx' lexp)) decls)

@@ -1417,11 +1413,7 @@ let erase_type lctx lxp =

(* Textually identical to the previous definition of `clean_decls`, but calls the new `erase_type`, which checks for metavars. *) -let clean_decls - (lctx : Lctx.t) - (decls : ldecl list) - : Lctx.t * (vname * E.elexp) list = - +let clean_decls (lctx : Lctx.t) (decls : ldecl list) : Lctx.t * Elexp.decls = let lctx' = Lctx.extend lctx decls in (lctx', List.map (fun (v, lexp, _) -> (v, erase_type lctx' lexp)) decls)

===================================== tests/env_test.ml ===================================== @@ -53,18 +53,18 @@ let _ = (add_test "ENV" "Set Variables" (fun () ->

let rctx = List.fold_left (fun ctx (n, _, _) -> - add_rte_variable n Vundefined ctx) + Env.cons n Vundefined ctx) rctx var in

- print_rte_ctx rctx; + Env.print_rctx ~start:0 rctx;

let rctx, _ = List.fold_left (fun (ctx, idx) (n, _, _) -> - (set_rte_variable idx n Vundefined ctx); + (Env.find_entry ~name:n idx ctx := Vundefined); (ctx, idx - 1)) (rctx, n) var in

- print_rte_ctx rctx); + Env.print_rctx ~start:0 rctx); success))

===================================== tests/eval_test.ml ===================================== @@ -468,7 +468,7 @@ let _ = (* The result should overflow *) try let result = (eval elxp rctx) in ut_string2 ("EXPECTED overflow for `" ^ str ^ "`\n"); - ut_string2 ("GOT: " ^ (value_string result) ^ "\n"); + ut_string2 ("GOT: " ^ (Env.string_of_value result) ^ "\n"); failure with | Log.Internal_error _ -> Log.clear_log (); success in

===================================== tests/utest_lib.ml ===================================== @@ -127,13 +127,13 @@ let _expect_equal_t equality_test to_string value expect = failure)

let print_value_list values = - List.fold_left (fun s v -> s ^ "\n" ^ Env.value_string v) "" values + List.fold_left (fun s v -> s ^ "\n" ^ Env.string_of_value v) "" values

let expect_equal_bool = _expect_equal_t Bool.equal string_of_bool let expect_equal_int = _expect_equal_t Int.equal string_of_int let expect_equal_float = _expect_equal_t Float.equal string_of_float let expect_equal_str = _expect_equal_t String.equal (fun g -> g) -let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list +let expect_equal_values = _expect_equal_t (List.equal Env.value_equal) print_value_list

let expect_equal_lexp = _expect_equal_t Lexp.eq Lexp.to_string let expect_conv_lexp ctx = _expect_equal_t (Opslexp.conv_p ctx) Lexp.to_string

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/b08bdf6a80c6c13770b4850f7e1b44db8...