Septembre 2022 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][gambit-compile-pervasives] Compile (a trimmed-down version of) the pervasives to Scheme.
by Simon Génier (＠ilovemonoids) 22 Sep '22

22 Sep '22

Simon Génier pushed to branch gambit-compile-pervasives at Stefan / Typer Commits: 17519ff3 by Simon Génier at 2022-09-22T14:55:27-04:00 Compile (a trimmed-down version of) the pervasives to Scheme. - - - - - 17 changed files: - + btl/pervasive-light.typer - debug_util.ml - samples/nat.typer - src/REPL.ml - + src/array.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/instargs.ml - src/inverse_subst.ml - src/lexer.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/commit/17519ff310d3c13fb3b10bcb873b2a800… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/17519ff310d3c13fb3b10bcb873b2a800… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit-compile-pervasives] Compile (a trimmed-down version of) the pervasives to Scheme.
by Simon Génier (＠ilovemonoids) 22 Sep '22

22 Sep '22

Simon Génier pushed to branch gambit-compile-pervasives at Stefan / Typer Commits: 0382e776 by Simon Génier at 2022-09-22T04:21:39-04:00 Compile (a trimmed-down version of) the pervasives to Scheme. - - - - - 18 changed files: - + btl/pervasive-light.typer - debug_util.ml - samples/nat.typer - src/REPL.ml - + src/array.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/instargs.ml - src/inverse_subst.ml - src/lexer.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/commit/0382e776a37a8f83c7d824fddc8f15658… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/0382e776a37a8f83c7d824fddc8f15658… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit-compile-pervasives] Compile calls with no arguments to just the function.
by Simon Génier (＠ilovemonoids) 22 Sep '22

22 Sep '22

Simon Génier pushed to branch gambit-compile-pervasives at Stefan / Typer Commits: 6a087502 by Simon Génier at 2022-09-22T03:25:33-04:00 Compile calls with no arguments to just the function. - - - - - 3 changed files: - src/elab.ml - src/gambit.ml - typer.ml Changes: ===================================== src/elab.ml ===================================== @@ -2221,3 +2221,20 @@ let process_file ectx' with | Sys_error _ -> Log.user_error {|file %s does not exist.|} path + +class lexp_compiler channel = object + inherit Backend.compiler + + method process_decls ldecls = + let f = formatter_of_out_channel channel in + List.iter (fprintf f "%a@." Lexp.pp_print_decl) ldecls +end + +class elexp_compiler lctx channel = object + inherit Backend.compiler + + method process_decls ldecls = + let f = formatter_of_out_channel channel in + let _, eldecls = Opslexp.clean_decls lctx ldecls in + List.iter (fprintf f "%a@." Elexp.pp_print_decl) eldecls +end ===================================== src/gambit.ml ===================================== @@ -18,7 +18,7 @@ * 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 Printf +open Format open Debruijn open Elexp @@ -139,29 +139,52 @@ let gensym : string -> string = Scm.escape_symbol name module ScmContext = struct + type entry = + | Var of string * string option + | Poison of string option + (* Maps Debruijn indices to Scheme variable names. *) - type t = string Myers.myers + type t = entry Myers.myers let nil : t = Myers.nil let of_lctx (lctx : lexp_context) : t = - let f ((_, name), _, _) = Option.get name in + let f ((_, name), _, _) = + match name with + | Some name -> Var (name, Some name) + | None -> Poison (name) + in Myers.map f lctx let intro (sctx : t) (_, name : vname) : t * string = - let name = + let scm_name = match name with | Some name -> name - | None -> gensym "g" + | None -> gensym "" in - (Myers.cons name sctx, name) + (Myers.cons (Var (scm_name, name)) sctx, scm_name) + + (** Introduces a variable, that must not be used. *) + let poison (sctx : t) (_, name : vname) : t = + Myers.cons (Poison (name)) sctx let intro_binding (sctx : t) (name, elexp : vname * elexp) = let sctx, name = intro sctx name in (sctx, (name, elexp)) - let lookup (sctx : t) (index : int) : string option = - Myers.nth_opt index sctx + let lookup (sctx : t) ((_, expected_name), index : vref) : string = + match Myers.nth index sctx with + | Var (scm_name, actual_name) when expected_name = actual_name -> scm_name + | Var (_, actual_name) -> + trace_fatal + __POS__ "Debruijn strikes again (expected = “%a”, actual = “%a”)" + (pp_print_option pp_print_string) expected_name + (pp_print_option pp_print_string) actual_name + | Poison (actual_name) -> + trace_fatal + __POS__ "Attempted to reference deleted variable (expected = “%a”, actual = “%a”)" + (pp_print_option pp_print_string) expected_name + (pp_print_option pp_print_string) actual_name end let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = @@ -202,11 +225,8 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = location "builtin is not supported on the Gambit backend: %s" name; Scm.Symbol "error" - | Elexp.Var (_, index) -> - begin match ScmContext.lookup sctx index with - | None -> Scm.Symbol "TODO" - | Some name -> Scm.Symbol name - end + | Elexp.Var (vref) -> + Scm.Symbol (ScmContext.lookup sctx vref) | Elexp.Let (_, bindings, body) -> if List.length bindings = 0 @@ -228,6 +248,9 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = Scm.List [Scm.Symbol name]; scheme_of_expr sctx' body] + | Elexp.Call (head, []) + -> scheme_of_expr sctx head + | Elexp.Call (head, tail) -> let scm_head = scheme_of_expr sctx head in let scm_tail = List.map (scheme_of_expr sctx) tail in @@ -254,66 +277,40 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = in make_curried_lambda vars vector_expr + | Elexp.Case (_, target, branches, None) when SMap.cardinal branches = 1 + -> let _, branch = SMap.choose branches in + uncall_by_namify + sctx target (fun scm_target -> + scheme_of_branch sctx scm_target branch) + | Elexp.Case (_, target, branches, default_branch) - -> let target_name = - match target with - | Elexp.Var _ -> scheme_of_expr sctx target - | _ -> Scm.Symbol (gensym "target") - in - let scm_default_branch = - match default_branch with - | None -> [] - | Some (name, body) - -> let sctx, name = ScmContext.intro sctx name in - (* (else => (lambda (name) body)) *) - [Scm.List [Scm.else'; - Scm.double_right_arrow; - Scm.List [Scm.lambda; - Scm.List [Scm.Symbol name]; - scheme_of_expr sctx body]]] - in - let add_branch cons_name (_, field_names, branch_body) scm_branches = - let make_binding (sctx, bindings, i) (location, name) = - match name with - | Some "_" -> sctx, bindings, Z.succ i - | _ - -> let sctx, name = ScmContext.intro sctx (location, name) in - let binding = Scm.List [Scm.Symbol name; - Scm.List [Scm.prim_vector_ref; - target_name; - Scm.Integer i]] - in - sctx, binding :: bindings, Z.succ i - in - let sctx, bindings, _ = List.fold_left make_binding (sctx, [], Z.one) field_names in - let scm_branch = - Scm.List [Scm.List [Scm.symbol cons_name]; - if Int.equal (List.length bindings) 0 - then scheme_of_expr sctx branch_body - else - Scm.List [Scm.let'; - Scm.List (List.rev bindings); - scheme_of_expr sctx branch_body]] - in - scm_branch :: scm_branches - in - let scm_branches = - List.rev_append (SMap.fold add_branch branches []) scm_default_branch - in - let scm_case = - Scm.List (Scm.case - :: Scm.List [Scm.prim_vector_ref; - target_name; - Scm.Integer Z.zero] - :: scm_branches) - in - (match target with - | Elexp.Var _ -> scm_case - | _ - -> Scm.List [Scm.let'; - Scm.List [Scm.List [target_name; - scheme_of_expr sctx target]]; - scm_case]) + -> uncall_by_namify + sctx target (fun scm_target -> + let scm_default_branch = + match default_branch with + | None -> [] + | Some (name, body) + -> let sctx, name = ScmContext.intro sctx name in + (* (else => (lambda (name) body)) *) + [Scm.List [Scm.else'; + Scm.double_right_arrow; + Scm.List [Scm.lambda; + Scm.List [Scm.Symbol name]; + scheme_of_expr sctx body]]] + in + let add_branch cons_name branch scm_branches = + Scm.List [Scm.List [Scm.symbol cons_name]; + scheme_of_branch sctx scm_target branch] + :: scm_branches + in + let scm_branches = + List.rev_append (SMap.fold add_branch branches []) scm_default_branch + in + Scm.List (Scm.case + :: Scm.List [Scm.prim_vector_ref; + scm_target; + Scm.Integer Z.zero] + :: scm_branches)) | Elexp.Type (expr) -> diagnostic_error @@ -327,6 +324,42 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = ~context:[Elexp.display_context ~label:"elexp" elexp] __POS__ "[gambit] unsupported elexp" +and scheme_of_branch sctx (target : Scm.t) (_, field_names, branch_body) = + let make_binding (sctx, bindings, i) (_, name as vname) = + let sctx', bindings' = + match name with + | None -> + ScmContext.poison sctx vname, bindings + | Some _ -> + let sctx', scm_name = ScmContext.intro sctx vname in + let binding = + Scm.List [Scm.Symbol scm_name; + Scm.List [Scm.prim_vector_ref; target; Scm.Integer i]] + in + sctx', binding :: bindings + in + sctx', bindings', Z.succ i + in + let sctx, bindings, _ = List.fold_left make_binding (sctx, [], Z.one) field_names in + if Int.equal (List.length bindings) 0 + then scheme_of_expr sctx branch_body + else + Scm.List [Scm.let'; + Scm.List (List.rev bindings); + scheme_of_expr sctx branch_body] + +(** Wraps the body in a let-binding to avoid repeated evaluation because of + call-by-name, but only if necessary. *) +and uncall_by_namify + (sctx : ScmContext.t) (expr : Elexp.t) (make_body : Scm.t -> Scm.t) + : Scm.t = + let scm_expr = scheme_of_expr sctx expr in + match expr with + | Elexp.Var _ | Elexp.Builtin _ -> make_body scm_expr + | _ -> + let name = Scm.Symbol (gensym "") in + Scm.List [Scm.let'; Scm.List [Scm.List [name; scm_expr]]; make_body name] + class inferior script_path = let _ = trace_info __POS__ "Starting inferior Gambit" in let down_reader, down_writer = Unix.pipe ~cloexec:true () in @@ -414,7 +447,13 @@ let scheme_of_decl | Elexp.Type _ -> None | Elexp.Builtin (_, ("Eq" | "Int" | "IO" | "String" | "Sexp" | "TypeLevel")) -> None | _ -> - Some (Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp])) + let scm_expr = scheme_of_expr sctx elexp in + begin match scm_expr with + | Scm.List (Scm.Symbol ("lambda") :: Scm.List args :: body) -> + Some + (Scm.List (Scm.define :: Scm.List (Scm.Symbol (name) :: args) :: body)) + | _ -> Some (Scm.List ([Scm.define; Scm.Symbol (name); scm_expr])) + end class gambit_compiler lctx output = object inherit Backend.compiler ===================================== typer.ml ===================================== @@ -33,6 +33,21 @@ let add_input_file, list_input_files = let preload_pervasives : bool ref = ref true +type target = + | Gambit + | Lexp + | Elexp + +let arg_target = ref Lexp + +let set_target name = + arg_target := + match name with + | "gambit" -> Gambit + | "lexp" -> Lexp + | "elexp" -> Elexp + | _ -> failwith "invalid target" + let generic_arg_spec = [("--verbosity", Arg.String (fun s -> Log.Diagnostics.Config.level := Log.Level.parse s), @@ -58,6 +73,9 @@ let compile_arg_spec = ("--no-pervasives", Arg.Clear preload_pervasives, "Do not load the pervasives.") + :: ("--target", + Arg.Symbol (["gambit"; "lexp"; "elexp"], set_target), + "Select the target, i.e. which kind of code to generate.") :: generic_arg_spec let parse_args spec argv usage = @@ -78,17 +96,29 @@ let compile_main argv = Elab.load_special_forms Debruijn.empty_elab_context end in - let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in - let _ = - Fun.protect - ~finally:(fun () -> - backend#stop; - Log.Diagnostics.print_log ()) - (fun () - -> List.fold_left (Elab.process_file backend) ectx (list_input_files ())) + let compile backend = + let _ = + Fun.protect + ~finally:Log.Diagnostics.print_log + (fun () + -> List.fold_left + (Elab.process_file backend) + ectx + (list_input_files ())) + in + () in - () + + let lctx = ectx_to_lctx ectx in + match !arg_target with + | Gambit + -> let backend = new Gambit.gambit_compiler lctx stdout in + Fun.protect + ~finally:(fun () -> backend#stop) + (fun () -> compile (backend :> Backend.compiler)) + | Lexp -> compile (new Elab.lexp_compiler stdout) + | Elexp -> compile (new Elab.elexp_compiler lctx stdout) let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in @@ -151,4 +181,6 @@ let main () = -> eprintf {|unknown command "%s"|} command; exit 1) -let () = main () +let () = + try main () with + | Arg.Bad (message) -> print_string message View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6a0875023133ca2515c1c3c45aa3c4729… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6a0875023133ca2515c1c3c45aa3c4729… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit-compile-pervasives] Compile calls with no arguments to just the function.
by Simon Génier (＠ilovemonoids) 21 Sep '22

21 Sep '22

Simon Génier pushed to branch gambit-compile-pervasives at Stefan / Typer Commits: cff22dd5 by Simon Génier at 2022-09-21T14:05:55-04:00 Compile calls with no arguments to just the function. - - - - - 3 changed files: - src/elab.ml - src/gambit.ml - typer.ml Changes: ===================================== src/elab.ml ===================================== @@ -2221,3 +2221,20 @@ let process_file ectx' with | Sys_error _ -> Log.user_error {|file %s does not exist.|} path + +class lexp_compiler channel = object + inherit Backend.compiler + + method process_decls ldecls = + let f = formatter_of_out_channel channel in + List.iter (fprintf f "%a@." Lexp.pp_print_decl) ldecls +end + +class elexp_compiler lctx channel = object + inherit Backend.compiler + + method process_decls ldecls = + let f = formatter_of_out_channel channel in + let _, eldecls = Opslexp.clean_decls lctx ldecls in + List.iter (fprintf f "%a@." Elexp.pp_print_decl) eldecls +end ===================================== src/gambit.ml ===================================== @@ -228,6 +228,9 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = Scm.List [Scm.Symbol name]; scheme_of_expr sctx' body] + | Elexp.Call (head, []) + -> scheme_of_expr sctx head + | Elexp.Call (head, tail) -> let scm_head = scheme_of_expr sctx head in let scm_tail = List.map (scheme_of_expr sctx) tail in @@ -254,66 +257,40 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = in make_curried_lambda vars vector_expr + | Elexp.Case (_, target, branches, None) when SMap.cardinal branches = 1 + -> let _, branch = SMap.choose branches in + uncall_by_namify + sctx target (fun scm_target -> + scheme_of_branch sctx scm_target branch) + | Elexp.Case (_, target, branches, default_branch) - -> let target_name = - match target with - | Elexp.Var _ -> scheme_of_expr sctx target - | _ -> Scm.Symbol (gensym "target") - in - let scm_default_branch = - match default_branch with - | None -> [] - | Some (name, body) - -> let sctx, name = ScmContext.intro sctx name in - (* (else => (lambda (name) body)) *) - [Scm.List [Scm.else'; - Scm.double_right_arrow; - Scm.List [Scm.lambda; - Scm.List [Scm.Symbol name]; - scheme_of_expr sctx body]]] - in - let add_branch cons_name (_, field_names, branch_body) scm_branches = - let make_binding (sctx, bindings, i) (location, name) = - match name with - | Some "_" -> sctx, bindings, Z.succ i - | _ - -> let sctx, name = ScmContext.intro sctx (location, name) in - let binding = Scm.List [Scm.Symbol name; - Scm.List [Scm.prim_vector_ref; - target_name; - Scm.Integer i]] - in - sctx, binding :: bindings, Z.succ i - in - let sctx, bindings, _ = List.fold_left make_binding (sctx, [], Z.one) field_names in - let scm_branch = - Scm.List [Scm.List [Scm.symbol cons_name]; - if Int.equal (List.length bindings) 0 - then scheme_of_expr sctx branch_body - else - Scm.List [Scm.let'; - Scm.List (List.rev bindings); - scheme_of_expr sctx branch_body]] - in - scm_branch :: scm_branches - in - let scm_branches = - List.rev_append (SMap.fold add_branch branches []) scm_default_branch - in - let scm_case = - Scm.List (Scm.case - :: Scm.List [Scm.prim_vector_ref; - target_name; - Scm.Integer Z.zero] - :: scm_branches) - in - (match target with - | Elexp.Var _ -> scm_case - | _ - -> Scm.List [Scm.let'; - Scm.List [Scm.List [target_name; - scheme_of_expr sctx target]]; - scm_case]) + -> uncall_by_namify + sctx target (fun scm_target -> + let scm_default_branch = + match default_branch with + | None -> [] + | Some (name, body) + -> let sctx, name = ScmContext.intro sctx name in + (* (else => (lambda (name) body)) *) + [Scm.List [Scm.else'; + Scm.double_right_arrow; + Scm.List [Scm.lambda; + Scm.List [Scm.Symbol name]; + scheme_of_expr sctx body]]] + in + let add_branch cons_name branch scm_branches = + Scm.List [Scm.List [Scm.symbol cons_name]; + scheme_of_branch sctx scm_target branch] + :: scm_branches + in + let scm_branches = + List.rev_append (SMap.fold add_branch branches []) scm_default_branch + in + Scm.List (Scm.case + :: Scm.List [Scm.prim_vector_ref; + scm_target; + Scm.Integer Z.zero] + :: scm_branches)) | Elexp.Type (expr) -> diagnostic_error @@ -327,6 +304,39 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = ~context:[Elexp.display_context ~label:"elexp" elexp] __POS__ "[gambit] unsupported elexp" +and scheme_of_branch sctx (target : Scm.t) (_, field_names, branch_body) = + let make_binding (sctx, bindings, i) (location, name) = + match name with + | None -> sctx, bindings, Z.succ i + | Some _ + -> let sctx, name = ScmContext.intro sctx (location, name) in + let binding = Scm.List [Scm.Symbol name; + Scm.List [Scm.prim_vector_ref; + target; + Scm.Integer i]] + in + sctx, binding :: bindings, Z.succ i + in + let sctx, bindings, _ = List.fold_left make_binding (sctx, [], Z.one) field_names in + if Int.equal (List.length bindings) 0 + then scheme_of_expr sctx branch_body + else + Scm.List [Scm.let'; + Scm.List (List.rev bindings); + scheme_of_expr sctx branch_body] + +(** Wraps the body in a let-binding to avoid repeated evaluation because of + call-by-name, but only if necessary. *) +and uncall_by_namify + (sctx : ScmContext.t) (expr : Elexp.t) (make_body : Scm.t -> Scm.t) + : Scm.t = + let scm_expr = scheme_of_expr sctx expr in + match expr with + | Elexp.Var _ | Elexp.Builtin _ -> make_body scm_expr + | _ -> + let name = Scm.Symbol (gensym "") in + Scm.List [Scm.let'; Scm.List [Scm.List [name; scm_expr]]; make_body name] + class inferior script_path = let _ = trace_info __POS__ "Starting inferior Gambit" in let down_reader, down_writer = Unix.pipe ~cloexec:true () in ===================================== typer.ml ===================================== @@ -33,6 +33,21 @@ let add_input_file, list_input_files = let preload_pervasives : bool ref = ref true +type target = + | Gambit + | Lexp + | Elexp + +let arg_target = ref Lexp + +let set_target name = + arg_target := + match name with + | "gambit" -> Gambit + | "lexp" -> Lexp + | "elexp" -> Elexp + | _ -> failwith "invalid target" + let generic_arg_spec = [("--verbosity", Arg.String (fun s -> Log.Diagnostics.Config.level := Log.Level.parse s), @@ -58,6 +73,9 @@ let compile_arg_spec = ("--no-pervasives", Arg.Clear preload_pervasives, "Do not load the pervasives.") + :: ("--target", + Arg.Symbol (["gambit"; "lexp"; "elexp"], set_target), + "Select the target, i.e. which kind of code to generate.") :: generic_arg_spec let parse_args spec argv usage = @@ -78,17 +96,29 @@ let compile_main argv = Elab.load_special_forms Debruijn.empty_elab_context end in - let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in - let _ = - Fun.protect - ~finally:(fun () -> - backend#stop; - Log.Diagnostics.print_log ()) - (fun () - -> List.fold_left (Elab.process_file backend) ectx (list_input_files ())) + let compile backend = + let _ = + Fun.protect + ~finally:Log.Diagnostics.print_log + (fun () + -> List.fold_left + (Elab.process_file backend) + ectx + (list_input_files ())) + in + () in - () + + let lctx = ectx_to_lctx ectx in + match !arg_target with + | Gambit + -> let backend = new Gambit.gambit_compiler lctx stdout in + Fun.protect + ~finally:(fun () -> backend#stop) + (fun () -> compile (backend :> Backend.compiler)) + | Lexp -> compile (new Elab.lexp_compiler stdout) + | Elexp -> compile (new Elab.elexp_compiler lctx stdout) let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in @@ -151,4 +181,6 @@ let main () = -> eprintf {|unknown command "%s"|} command; exit 1) -let () = main () +let () = + try main () with + | Arg.Bad (message) -> print_string message View it on GitLab: https://gitlab.com/monnier/typer/-/commit/cff22dd57eccaf291fed2b3709845004f… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/cff22dd57eccaf291fed2b3709845004f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit-compile-pervasives] Compile (a trimmed-down version of) the pervasives to Scheme.
by Simon Génier (＠ilovemonoids) 21 Sep '22

21 Sep '22

Simon Génier pushed to branch gambit-compile-pervasives at Stefan / Typer Commits: 071738ae by Simon Génier at 2022-09-21T10:07:25-04:00 Compile (a trimmed-down version of) the pervasives to Scheme. - - - - - 20 changed files: - + btl/pervasive-light.typer - debug_util.ml - samples/nat.typer - src/REPL.ml - + src/array.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/instargs.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/listx.ml → src/list.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/commit/071738ae521309d943ca11ed2065d0b17… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/071738ae521309d943ca11ed2065d0b17… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit-compile-pervasives] Compile (a trimmed-down version of) the pervasives to Scheme.
by Simon Génier (＠ilovemonoids) 18 Sep '22

18 Sep '22

Simon Génier pushed to branch gambit-compile-pervasives at Stefan / Typer Commits: 24c7c74b by Simon Génier at 2022-09-18T12:32:40-04:00 Compile (a trimmed-down version of) the pervasives to Scheme. - - - - - 5 changed files: - + btl/pervasive-light.typer - src/elab.ml - src/gambit.ml - src/prelexer.ml - typer.ml Changes: ===================================== btl/pervasive-light.typer ===================================== @@ -0,0 +1,36 @@ +%%% pervasive-light --- Always available definitions, trimmed-down version. + +%% Copyright (C) 2011-2022 Free Software Foundation, Inc. +%% +%% Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> +%% Keywords: languages, lisp, dependent types. +%% +%% This file is part of Typer. +%% +%% Typer is free software; you can redistribute it and/or modify it under the +%% terms of the GNU General Public License as published by the Free Software +%% Foundation, either version 3 of the License, or (at your option) any +%% later version. +%% +%% Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%% WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%% FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%% more details. +%% +%% You should have received a copy of the GNU General Public License along +%% with this program. If not, see <http://www.gnu.org/licenses/>. + +%%% This file is a trimmed-down version of pervasive.typer. The goal is to have +%%% some basic definitions so we can compile Typer programs with the Gambit +%%% backend, which is much less sophisticated than the interpreter. + +Unit = typecons Unit unit; +unit = datacons Unit unit; + +%% Void = typecons Void; + +%% Eq/refl : (x : ?t) ≡> Eq x x; +%% Eq/refl = Built-in "Eq.refl"; + +%% Eq/cast : (x : ?) ≡> (y : ?) ≡> (f : ? -> ?) ≡> f x -> f y; +%% Eq/cast = Built-in "Eq.cast"; ===================================== src/elab.ml ===================================== @@ -78,9 +78,12 @@ let display_lexp_details lexp channel _ = let display_value_details value channel _ = fprintf channel "\t > %s : %s\n" (value_name value) (value_string value) +let {trace_debug; trace_info; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions "ELAB" + let {diagnostic_fatal; diagnostic_error; diagnostic_warning; diagnostic_info; _} : Log.Diagnostics.diagnostic_functions = - Log.Diagnostics.make_diagnostic_functions "EVAL" + Log.Diagnostics.make_diagnostic_functions "ELAB" let {diagnostic_info = macro_diagnostic_info; _} : Log.Diagnostics.diagnostic_functions = @@ -598,7 +601,8 @@ let elab_p_id ((l,name) : symbol) : vname = (Symbol (l, name), match name with "_" -> None | _ -> Some name) (* Infer or check, as the case may be. *) -let rec elaborate ctx se ot = +let rec elaborate (ctx : elab_context) (se : sexp) (ot : ltype option) = + trace_debug __POS__ "Elaborating: %a" Sexp.output se; let (e, res_t) = match se with (* Rewrite SYM to `typer-identifier SYM`. *) | Symbol ((loc, name) as _id) @@ -1334,7 +1338,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = -> mkArrow (Symbol(l,""), Aerasable, name, t, e)) t -and infer_and_generalize_def (ctx : elab_context) se = +and infer_and_generalize_def (ctx : elab_context) (se : sexp) = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in let g = resolve_instances_and_generalize nctx e in @@ -1428,6 +1432,7 @@ and lexp_decls_1 -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) + trace_debug __POS__ "processing definition of “%s”" vname; let (lexp, ltp) = infer_and_generalize_def nctx sexp in let var = (thesexp, Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to @@ -2173,11 +2178,16 @@ let process_file (path : string) : elab_context = + trace_info __POS__ "processing file at path: %s" path; try let source = Source.of_path path in let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in let ldecls, ectx' = lexp_p_decls [] tokens ectx in + trace_info + __POS__ + "found %d declarations in file: %s" + (List.length ldecls) path; List.iter backend#process_decls ldecls; ectx' with ===================================== src/gambit.ml ===================================== @@ -380,7 +380,9 @@ class gambit_compiler lctx output = object sctx <- sctx'; lctx <- lctx'; List.iter - (fun sdecl -> sdecl |> pretty_printer#pp |> output_string output) + (fun sdecl + -> sdecl |> pretty_printer#pp |> output_string output; + flush output) sdecls method stop = ===================================== src/prelexer.ml ===================================== @@ -44,6 +44,16 @@ module Pretoken = struct | Preblock (_, l_inner), Preblock (_, r_inner) -> List.equal equal l_inner r_inner | _ -> false + + let rec pp (f : Format.formatter) (pretoken : t) : unit = + let open Format in + match pretoken with + | Pretoken (_, name) -> pp_print_string f name + | Prestring (_, text) -> fprintf f "%S" text + | Preblock (_, pretokens) + -> pp_print_char f '{'; + pp_print_list ~pp_sep:pp_print_space pp f pretokens; + pp_print_char f '}' end (*************** The Pre-Lexer phase *********************) ===================================== typer.ml ===================================== @@ -31,7 +31,9 @@ let add_input_file, list_input_files = let files = ref [] in (fun file -> files := file :: !files), (fun () -> List.rev !files) -let arg_defs = +let preload_pervasives : bool ref = ref true + +let generic_arg_spec = [("--verbosity", Arg.String (fun s -> Log.Diagnostics.Config.level := Log.Level.parse s), "Set the logging level"); @@ -48,17 +50,27 @@ let arg_defs = "Print the full lexp context on error"); ] -let parse_args argv usage = - try Arg.parse_argv argv arg_defs add_input_file usage with +let compile_arg_spec = + ("--no-pervasives", + Arg.Clear preload_pervasives, + "Do not load the pervasives.") + :: generic_arg_spec + +let parse_args spec argv usage = + try Arg.parse_argv argv spec add_input_file usage with | Arg.Help (message) -> print_string message; exit 0 let compile_main argv = let usage = Sys.executable_name ^ " compile [options] <file> …" in - parse_args argv usage; + parse_args compile_arg_spec argv usage; - let ectx = Elab.default_ectx in + let ectx = + if !preload_pervasives + then Elab.default_ectx + else Debruijn.empty_elab_context + in let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in let _ = @@ -71,7 +83,7 @@ let compile_main argv = let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in - parse_args argv usage; + parse_args generic_arg_spec argv usage; print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; @@ -94,7 +106,7 @@ let repl_main argv = let run_main argv = let usage = Sys.executable_name ^ " run [options] <file> …" in - parse_args argv usage; + parse_args generic_arg_spec argv usage; let ectx = Elab.default_ectx in let backend = new Eval.ast_interpreter (ectx_to_lctx ectx) in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/24c7c74bd31922c87c01b6718549adbc2… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/24c7c74bd31922c87c01b6718549adbc2… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/hmdup] -
by Stefan (＠monnier) 16 Sep '22

16 Sep '22

Stefan pushed to branch report/hmdup at Stefan / Typer Commits: 4cce113f by Stefan Monnier at 2022-09-16T23:31:21-04:00 - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -1191,6 +1191,10 @@ our language is extended as follows: \cite{Odersky96} %System-F inference via type annotations +%% Apparently uses a "worklist" approach, like I'd like to use for +%% Typer. +\cite{Zhao19} %Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. A Mechanical Formalization of Higher-ranked Polymorphic Type Inference. Proc. ACM Program. Lang. 3, ICFP, Article 112 (July 2019), 29 pages. https://doi.org/10.1145/3341716 + \section{Conclusion} View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4cce113f1602169d73ab0e6dec9ea645d… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4cce113f1602169d73ab0e6dec9ea645d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch gambit-compile-pervasives
by Simon Génier (＠ilovemonoids) 16 Sep '22

16 Sep '22

Simon Génier pushed new branch gambit-compile-pervasives at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/gambit-compile-pervasives You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][trace-vs-diagnose] Logging overhaul.
by Simon Génier (＠ilovemonoids) 16 Sep '22

16 Sep '22

Simon Génier pushed to branch trace-vs-diagnose at Stefan / Typer Commits: 6b99004e by Simon Génier at 2022-09-16T15:48:52-04:00 Logging overhaul. This changeset splits logging into two different concepts. - Diagnostics are meant for users of the compiler working on Typer code. - Tracing are meant for developers of the compiles working on Ocaml code. (I know the Venn diagram of these two kinds of people is a perfect circle… for now.) The practical difference between the two is that tracing does not expect the compiler to finish. Messages are printed right away and the channel is flushed after every message. It can also be enabled on per module basis so you don't get the full firehose. For example, setting TYPER_TRACE="TC=debug,EVAL=info,error" will show only error trace messages, except for EVAL where info messages will be shown too and TC where messages down to the debug level will be. Diagnostics are similar to the logs we had: they are collected and printed at the end. Their presence can make the compilation fail. - - - - - 28 changed files: - samples/nat.typer - src/REPL.ml - + src/array.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/instargs.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/listx.ml → src/list.ml - src/log.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - src/source.ml - + src/string.ml - src/unification.ml - tests/dune - tests/eval_test.ml - tests/instargs_test.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6b99004eccd5947105d22213bb716dfdf… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6b99004eccd5947105d22213bb716dfdf… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][trace-vs-diagnose] Logging overhaul.
by Simon Génier (＠ilovemonoids) 16 Sep '22

16 Sep '22

Simon Génier pushed to branch trace-vs-diagnose at Stefan / Typer Commits: a1c5194c by Simon Génier at 2022-09-16T09:56:24-04:00 Logging overhaul. This changeset splits logging into two different concepts. - Diagnostics are meant for users of the compiler working on Typer code. - Tracing are meant for developers of the compiles working on Ocaml code. (I know the Venn diagram of these two kinds of people is a perfect circle… for now.) The practical difference between the two is that tracing does not expect the compiler to finish. Messages are printed right away and the channel is flushed after every message. It can also be enabled on per module basis so you don't get the full firehose. For example, setting TYPER_TRACE="TC=debug,EVAL=info,error" will show only error trace messages, except for EVAL where info messages will be shown too and TC where messages down to the debug level will be. Diagnostics are similar to the logs we had: they are collected and printed at the end. Their presence can make the compilation fail. - - - - - 30 changed files: - samples/nat.typer - src/REPL.ml - + src/array.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/instargs.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/listx.ml → src/list.ml - src/log.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - src/source.ml - + src/string.ml - src/unification.ml - tests/dune - tests/eval_test.ml - tests/instargs_test.ml - tests/lexer_test.ml - tests/samples_test.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a1c5194c7cbc9f5b9fb3fc64e8cdd3b1a… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a1c5194c7cbc9f5b9fb3fc64e8cdd3b1a… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Septembre 2022