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

Commits: 39b3606a by Simon Génier at 2023-03-07T18:59:32-05:00 Cosmetic changes to Env.

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

- - - - - b08bdf6a by Simon Génier at 2023-03-07T19:21:51-05:00 Rename Elexp.elexp to Elexp.t.

Its shorter and nicer?

- - - - -

7 changed files:

- debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/gambit.ml - src/opslexp.ml - tests/env_test.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 @@ -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/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,7 +30,6 @@ * * --------------------------------------------------------------------------- *)

-open Elexp open Sexp

module M = Myers @@ -41,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 @@ -50,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 @@ -167,47 +164,41 @@ let pp_print_rctx let print_rctx ~(start : int) : runtime_env -> unit = Format.printf "%a" (pp_print_rctx ~start)

-let get_rte_size (ctx: runtime_env): int = M.length ctx - -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 () -> Format.printf "%a" (pp_print_rctx ~start:0) 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 [] +(** 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,7 +44,7 @@ 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 ([], []) @@ -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 @@ -114,7 +114,7 @@ let trace_value (value : value) : string = (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 @@ -487,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) @@ -507,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 @@ -529,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) @@ -576,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 *) @@ -591,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 = @@ -599,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

@@ -1111,7 +1110,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

===================================== 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/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,14 +53,14 @@ 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

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

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