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@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/24c7c74bd31922c87c01b6718549adbc25...