Simon Génier pushed to branch gambit at Stefan / Typer

Commits: 952f92e3 by Simon Génier at 2021-03-19T09:45:17-04:00 [Myers] Add nth_opt and reverse.

- - - - - b3875d28 by Simon Génier at 2021-03-22T15:59:01-04:00 Introduce source objects.

Source objects abstract over the text of Typer code. Does it come from a file? A string? Only the source object knows.

I extracted it from my Typer to Scheme compiler patch. By itself, I think it makes for slightly nicer code, but the real advantages are * We no longer process source text line by line. Supporting multi-line string is now as easy as removing the error. * We keep the full source text around. We can add it to locations so we are able to print the original source along an error message.

- - - - - e3fb3f5e by Simon Génier at 2021-03-24T19:54:15-04:00 [Source] Do not buffer more than one line.

- - - - - bf44f885 by Simon Génier at 2021-03-25T12:10:43-04:00 Add a backend to compile Typer to Scheme.

- - - - - bf91885c by Simon Génier at 2021-03-25T13:51:05-04:00 Backends maintain their lctx as mutable attributes.

- - - - -

16 changed files:

- GNUmakefile - src/REPL.ml - + src/backend.ml - src/debug_util.ml - src/dune - src/elab.ml - src/eval.ml - + src/frontend.ml - + src/gambit.ml - src/lexer.ml - src/lexp.ml - + src/main.ml - src/myers.ml - src/option.ml - src/prelexer.ml - + src/source.ml

Changes:

===================================== GNUmakefile ===================================== @@ -54,8 +54,8 @@ typer: # ============================ # Build typer # ============================ - $(OCAMLBUILD) src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) - @$(MV) $(BUILDDIR)/src/REPL.$(COMPILE_MODE) $(BUILDDIR)/typer + $(OCAMLBUILD) src/main.$(COMPILE_MODE) -I src $(OBFLAGS) + @$(MV) $(BUILDDIR)/src/main.$(COMPILE_MODE) $(BUILDDIR)/typer

tests-build: # ============================

===================================== src/REPL.ml ===================================== @@ -36,300 +36,171 @@ this program. If not, see http://www.gnu.org/licenses/. *) * * -------------------------------------------------------------------------- *)

-open Util -open Fmt - -open Prelexer -open Lexer -open Sexp -open Lexp +open Printf

+open Backend +open Debruijn open Eval +open Lexp

-open Grammar +let error = Log.log_error ~section:"REPL"

-open Env -open Debruijn -module OL = Opslexp -module EL = Elexp +let print_and_clear_log () = + Log.print_and_clear_log (); + flush stdout

-let arg_batch = ref false +let handle_stopped_compilation msg = + Log.print_and_clear_log (); + print_endline msg; + flush stdout

let print_input_line i = - print_string " In["; - ralign_print_int i 2; - print_string "] >> " - -let ieval_error = Log.log_error ~section:"IEVAL" + printf " In[%02d] >> " i

-let print_and_clear_log () = - if (not Log.typer_log_config.Log.print_at_log) then - Log.print_and_clear_log () +(* Read stdin for input.

-let handle_stopped_compilation msg = - print_and_clear_log (); - print_string msg; print_newline (); - flush stdout - -(* Read stdin for input. Returns only when the last char is ';' - * We can use '%' to prevent parsing - * If return is pressed and the last char is not ';' then - * indentation will be added *) + Returns only when the last char is ';'. We can use '%' to prevent parsing. If + return is pressed and the last char is not ';' then indentation will be + added. *) let rec read_input i = - print_input_line i; - flush stdout; + print_input_line i; + flush stdout;

- let rec loop str i = - flush stdout; - let line = input_line stdin in - let s = String.length str in - let n = String.length line in - if s = 0 && n = 0 then read_input i else - (if n = 0 then ( - print_string " . "; - print_string (make_line ' ' (i * 4)); - loop str (i + 1)) - else - let str = if s > 0 then String.concat "\n" [str; line] else line in - if line.[n - 1] = ';' || line.[0] = '%' then - str - else ( - print_string " . "; - print_string (make_line ' ' (i * 4)); - loop str (i + 1))) in - - loop "" i - -(* Interactive mode is not usual typer - It makes things easier to test out code *) -type lexpr = lexp - -(* Grouping declaration together will enable us to support mutually recursive - * declarations while bringing us closer to normal typer *) -let ipexp_parse (sxps: sexp list): (sexp list * sexp list) = - let rec pxp_parse sxps dacc pacc = - match sxps with - | [] -> (List.rev dacc), (List.rev pacc) - | sxp::tl -> match sxp with - (* Declaration *) - | Node (Symbol (_, ("_=_" | "_:_")), [Symbol _s; _t]) -> - pxp_parse tl (sxp :: dacc) pacc - - (* f arg1 arg2 = function body; *) - | Node (Symbol (_, "_=_"), [Node (Symbol _s, _args); _t]) -> - pxp_parse tl (sxp :: dacc) pacc - - (* Expression *) - | _ -> pxp_parse tl dacc (sxp::pacc) in - pxp_parse sxps [] [] - - -let ierase_type - (lctx : DB.lexp_context) - (ldecls, lexprs : ldecl list list * lexpr list) - : (vname * EL.elexp) list list * EL.elexp list = - - let lctx', eldecls = Listx.fold_left_map OL.clean_decls lctx ldecls in - let elexprs = List.map (OL.erase_type lctx') lexprs in - eldecls, elexprs - -let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = - let pdecls, pexprs = pexps in - (* FIXME We take the parsed input here but we should take the - unparsed tokens directly instead *) - let ldecls, lctx = Elab.lexp_p_decls pdecls [] lctx in - let lexprs = Elab.lexp_parse_all pexprs lctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) - lexprs; - (ldecls, lexprs), lctx - -let ieval f str ectx rctx = - let ieval' lexps rctx = - let (ldecls, lexprs) = lexps in - let rctx = eval_decls_toplevel ldecls rctx in - let vals = eval_all lexprs rctx false in - vals, rctx in - - let pres = (f str) in - let sxps = lex default_stt pres in - (* FIXME: This is too eager: it prevents one declaration from changing - * the grammar used in subsequent declarations. *) - let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in - - (* Different from usual typer *) - let pxps = ipexp_parse nods in - let lxps, ectx' = ilexp_parse pxps ectx in - let elxps = ierase_type (ectx_to_lctx ectx) lxps in - let v, rctx = ieval' elxps rctx in - v, ectx', rctx - -let raw_eval f str ectx rctx = - let pres = (f str) in - let sxps = lex default_stt pres in - let lxps, ectx' = Elab.lexp_p_decls [] sxps ectx in - let _, elxps = Listx.fold_left_map OL.clean_decls (ectx_to_lctx ectx) 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 *) - [], ectx', rctx - -let ieval_string = ieval prelex_string -let ieval_file = ieval prelex_file - -let eval_string = raw_eval prelex_string -let eval_file = raw_eval prelex_file - - -let welcome_msg = -" Typer 0.0.0 - Interpreter - (c) 2016 - - %quit (%q) : leave REPL - %help (%h) : print help -" - -let help_msg = + let rec loop str i = + flush stdout; + let line = input_line stdin in + let s = String.length str in + let n = String.length line in + if s = 0 && n = 0 then read_input i else + (if n = 0 then ( + print_string " . "; + print_string (String.make (i * 4) ' '); + loop str (i + 1)) + else + let str = if s > 0 then String.concat "\n" [str; line] else line in + if line.[n - 1] = ';' || line.[0] = '%' then + str + else ( + print_string " . "; + print_string (String.make (i * 4) ' '); + loop str (i + 1))) in + + loop "" i + +let help_message = " %quit (%q) : leave REPL %who (%w) : print runtime environment %info (%i) : print elaboration environment %calltrace (%ct): print eval trace of last call - %elabtrace (%et): print elaboration trace %typertrace (%tt): print typer trace %readfile : read a Typer file %help (%h) : print help "

- -let readfiles files (i, lctx, rctx) prt = - (* Read specified files *) - List.fold_left (fun (i, lctx, rctx) file -> - - (if prt then ( - print_string " In["; ralign_print_int i 2; print_string "] >> "; - print_string ("%readfile " ^ file); print_string "\n";)); - - try let (ret, lctx, rctx) = eval_file file lctx rctx in - (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) - with - Sys_error _ -> ( - ieval_error ("file "" ^ file ^ "" does not exist."); - (i, lctx, rctx)) - ) - (i, lctx, rctx) files - - -(* Specials commands %[command-name] [args] *) -let rec repl i clxp rctx = - let repl = repl (i + 1) in - let ipt = try read_input i with End_of_file -> "%quit" in - match ipt with - (* Check special keywords *) - | "%quit" | "%q" -> () - | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) - | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) - | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) - | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table)) - - (* command with arguments *) - | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( - match (str_split ipt ' ') with - | "%readfile"::args -> - let (_i, clxp, rctx) = - try - readfiles args (i, clxp, rctx) false - with Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; (i,clxp,rctx)) - in - repl clxp rctx; - | "%who"::args | "%w"::args -> ( - let _ = match args with - | ["all"] -> dump_rte_ctx rctx - | _ -> print_rte_ctx rctx in - repl clxp rctx) - | "%info"::args | "%i"::args -> ( - let _ = match args with - | ["all"] -> dump_lexp_ctx (ectx_to_lctx clxp) - | _ -> print_lexp_ctx (ectx_to_lctx clxp) in - repl clxp rctx) - - | cmd::_ -> - ieval_error (" "" ^ cmd ^ "" is not a correct repl command"); - repl clxp rctx - | _ -> repl clxp rctx) - - (* eval input *) - | _ -> - try let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in - print_and_clear_log (); - List.iter (print_eval_result i) ret; - repl clxp rctx +let process_file + (backend : #backend) + (ectx : elab_context) + (file_name : string) + : elab_context = + + try + let source = new Source.source_file file_name in + let decls, ectx' = Frontend.decls_of_source source ectx in + List.iter backend#process_decls decls; + ectx' + with + | Sys_error _ + -> (error ("file "" ^ file_name ^ "" does not exist."); + ectx) + +let process_interactive + (interactive : #interactive_backend) + (i : int) + (ectx : elab_context) + (input : string) + : elab_context = + + let source = new Source.source_string input in + let decls, exprs, ectx' = Frontend.decls_of_interactive source ectx in + + List.iter interactive#process_decls decls; + print_and_clear_log (); + + let values = List.map interactive#eval_expr exprs in + List.iter (print_eval_result i) values; + print_and_clear_log (); + + ectx' + +let rec repl + (i : int) + (interactive : interactive_backend) + (ectx : elab_context) + : unit = + + let input = try read_input i with End_of_file -> "%quit" in + + let ectx = + match input with + (* Check special keywords *) + | "%quit" | "%q" + -> exit 0 + | "%help" | "%h" + -> print_string help_message; + ectx + | "%calltrace" | "%ct" + -> print_eval_trace None; + ectx + | "%typertrace" | "%tt" + -> print_typer_trace None; + ectx + | "%lcollisions" | "%cl" + -> Util.get_stats_hashtbl (WHC.stats hc_table); + ectx + + (* command with arguments *) + | _ when input.[0] = '%' && input.[1] != ' ' + -> (match String.split_on_char ' ' input with + | "%readfile" :: args + -> (try + let ectx = + List.fold_left (process_file interactive) ectx args + in + print_and_clear_log (); + ectx with - | Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; repl clxp rctx) - | Log.Internal_error msg -> - (handle_stopped_compilation ("Internal error: " ^ msg); - repl clxp rctx) - | Log.User_error msg -> - (handle_stopped_compilation ("Fatal user error: " ^ msg); - repl clxp rctx) - -let arg_files = ref [] - - -(* ./typer [options] files *) -let arg_defs = [ - ("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); - ("--verbosity", - Arg.String Log.set_typer_log_level_str, "Set the logging level"); - ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); - ("-Vfull-lctx", - Arg.Set Debruijn.log_full_lctx, - "Print the full lexp context on error."); - (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) - (*"-I", - Arg.String (fun f -> searchpath := f::!searchpath), - "Append a directory to the search path"*) -] - -let parse_args () = - Arg.parse arg_defs (fun s -> arg_files:= s::!arg_files) "" - -let main () = - parse_args (); - - let ectx = Elab.default_ectx in - let rctx = Elab.default_rctx in - - 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) = ( - try - let res = - readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in - print_and_clear_log (); res - with - | Log.Stop_Compilation msg -> - handle_stopped_compilation msg; exit 1 - | (Log.Internal_error msg) as e -> - handle_stopped_compilation ("Internal error: " ^ msg); - raise e - | Log.User_error msg -> - handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 - ) in - - flush stdout; - - if not !arg_batch then - (* Initiate REPL. This will allow us to inspect interpreted code *) - repl i ectx rctx - - -let _ = main () + | Log.Stop_Compilation msg + -> handle_stopped_compilation msg; + ectx) + | "%who" :: args | "%w" :: args + -> (match args with + | ["all"] -> interactive#dump_rte_ctx + | _ -> interactive#print_rte_ctx); + ectx + | "%info" :: args | "%i" :: args + -> (match args with + | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) + | _ -> print_lexp_ctx (ectx_to_lctx ectx)); + ectx + + | cmd :: _ + -> error (""" ^ cmd ^ "" is not a correct repl command"); + ectx + + | _ + -> ectx) + + (* eval input *) + | _ + -> (try process_interactive interactive i ectx input with + | Log.Stop_Compilation msg + -> handle_stopped_compilation msg; + ectx + | Log.Internal_error msg + -> handle_stopped_compilation ("Internal error: " ^ msg); + ectx + | Log.User_error msg + -> handle_stopped_compilation ("Fatal user error: " ^ msg); + ectx) + + in repl (i + 1) interactive ectx

===================================== src/backend.ml ===================================== @@ -0,0 +1,81 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.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/. *) + +(* A backend is a consumer of fully eleborated and checked lexps. This module + provides a superclass for all backends as well their implementations. *) + +open Lexp + +type value = Env.value_type + +class virtual backend = object + (* Processes (interpret or compile, depending on the backend) a block of + mutually recursive declarations. *) + method virtual process_decls : ldecls -> unit + + method interactive : interactive_backend option = None +end + +(* Backends may optionaly allow interactive evaluation, i.e. lexps can be + immediately evaluated as opposed compiled for evaluation later. *) +and virtual interactive_backend = object (self) + inherit backend + + method! interactive = Some (self :> interactive_backend) + + method virtual eval_expr : lexp -> value + + method virtual print_rte_ctx : unit + + method virtual dump_rte_ctx : unit +end + +class ast_interpreter lctx = object + inherit interactive_backend + + val mutable rctx = Eval.from_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + rctx <- Eval.eval_decls eldecls rctx; + lctx <- lctx' + + method eval_expr lexp = + let elexp = Opslexp.erase_type lctx lexp in + Eval.debug_eval elexp rctx + + method print_rte_ctx = Env.print_rte_ctx rctx + + method dump_rte_ctx = Env.dump_rte_ctx rctx +end + +class gambit_compiler lctx output = object + inherit backend + + val mutable sctx = Gambit.ScmContext.of_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', sctx', sdecls = Gambit.scheme_of_decls lctx sctx ldecls in + sctx <- sctx'; + lctx <- lctx'; + Gambit.Scm.print output sdecls; +end

===================================== src/debug_util.ml ===================================== @@ -277,7 +277,7 @@ let main () = let clean_lxp = List.map OL.clean_decls lexps in

(* Eval declaration *) - let rctx = Elab.default_rctx in + let rctx = Eval.from_ectx Elab.default_ectx in print_string yellow; let rctx = (try eval_decls_toplevel clean_lxp rctx; with e ->

===================================== src/dune ===================================== @@ -1,6 +1,6 @@ ;; -*- lisp-data -*- (executable - (name REPL) + (name main) ;; (public_name typer) (libraries "zarith" "str") )

===================================== src/elab.ml ===================================== @@ -1772,8 +1772,9 @@ let in_pervasive = ref true let sform_load usr_elctx loc sargs _ot =

let read_file file_name elctx = + let source = new Source.source_file file_name in let pres = - try prelex_file file_name with + try prelex source with | Sys_error _ -> error ~loc ("Could not load `" ^ file_name ^ "`: file not found."); [] in @@ -1858,7 +1859,8 @@ let default_ectx

(* Read BTL files *) let read_file file_name elctx = - let pres = prelex_file file_name in + let source = new Source.source_file file_name in + let pres = prelex source in let sxps = lex default_stt pres in let _, lctx = lexp_p_decls [] sxps elctx in lctx in @@ -1903,8 +1905,6 @@ let default_ectx Log.print_and_clear_log (); raise e

-let default_rctx = EV.from_ectx default_ectx - (* String Parsing * --------------------------------------------------------- *)

@@ -1912,7 +1912,8 @@ let lexp_expr_str str ctx = let tenv = default_stt in let grm = ectx_get_grammar ctx in let limit = Some ";" in - let pxps = sexp_parse_str str tenv grm limit in + let source = new Source.source_string str in + let pxps = sexp_parse_source source tenv grm limit in let lexps = lexp_parse_all pxps ctx in List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; @@ -1920,7 +1921,8 @@ let lexp_expr_str str ctx =

let lexp_decl_str str ctx = let tenv = default_stt in - let tokens = lex_str str tenv in + let source = new Source.source_string str in + let tokens = lex_source source tenv in lexp_p_decls [] tokens ctx

===================================== src/eval.ml ===================================== @@ -353,7 +353,9 @@ let make_float loc _depth args_val = match args_val with

let make_block loc _depth args_val = match args_val with (* From what would we like to make a block? *) - | [Vstring str] -> Vsexp (Block (loc, (Prelexer.prelex_string str), loc)) + | [Vstring str] + -> let source = new Source.source_string str in + Vsexp (Block (loc, (Prelexer.prelex source), loc)) | _ -> error loc "Sexp.block expects one string as argument"

let reader_parse loc _depth args_val = match args_val with @@ -487,7 +489,14 @@ and eval_var ctx lxp v = ("Variable: " ^ L.maybename (snd name) ^ (str_idx idx) ^ " was not found ")

(* unef: unevaluated function (to make the trace readable) *) -and eval_call loc unef i f args = +and eval_call + loc + (unef : elexp) + (i : eval_debug_info) + (f : value_type) + (args : value_type list) + : value_type = + match f, args with (* return result of eval *) | _, [] -> f @@ -1145,14 +1154,13 @@ let from_lctx (lctx: lexp_context): runtime_env = | CVempty -> Myers.nil | CVlet (loname, def, _, lctx) -> let rctx = from_lctx lctx in - Myers.cons (loname, - ref (match def with - | LetDef (_, e) - -> if closed_p rctx (OL.fv e) then - eval (OL.erase_type lctx e) rctx - else Vundefined - | _ -> Vundefined)) - rctx + let value = + match def with + | LetDef (_, e) when closed_p rctx (OL.fv e) + -> eval (OL.erase_type lctx e) rctx + | _ -> Vundefined + in + Myers.cons (loname, ref value) rctx | CVfix (defs, lctx) -> let fvs = List.fold_left (fun fvs (_, e, _)

===================================== src/frontend.ml ===================================== @@ -0,0 +1,75 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.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/. *) + +open Debruijn +open Lexer +open Lexp +open Opslexp +open Prelexer +open Sexp + +let decls_of_source + (source : Source.t) + (ectx : elab_context) + : ldecls list * elab_context = + + let pretokens = prelex source in + let tokens = lex Grammar.default_stt pretokens in + let ldecls, ectx' = Elab.lexp_p_decls [] tokens ectx in + (ldecls, ectx') + +(** Elaborate Typer source from an interactive session. The difference with + normal Typer is that expressions are also accepted in addition to + declarations. + + Note that all declarations are hoisted before expressions. *) +let decls_of_interactive + (source : Source.t) + (ectx : elab_context) + : ldecls list * lexp list * elab_context = + + let classify_sexps nodes = + let rec loop sexps decls exprs = + match sexps with + | [] -> (List.rev decls, List.rev exprs) + | sexp :: sexps + -> (match sexp with + | Node (Symbol (_, ("_=_" | "_:_")), [Symbol _; _]) + -> loop sexps (sexp :: decls) exprs + | Node (Symbol (_, ("_=_")), [Node _; _]) + -> loop sexps (sexp :: decls) exprs + | _ + -> loop sexps decls (sexp :: exprs)) + in loop nodes [] [] + in + + let pretokens = prelex source in + let tokens = lex Grammar.default_stt pretokens in + (* FIXME: This is too eager: it prevents one declaration from changing + * the grammar used in subsequent declarations. *) + let sexps = sexp_parse_all_to_list (ectx_to_grm ectx) tokens (Some ";") in + let decls, exprs = classify_sexps sexps in + + let ldecls, ectx' = Elab.lexp_p_decls decls [] ectx in + + let lexprs = Elab.lexp_parse_all exprs ectx' in + List.iter (fun lexpr -> ignore (check (ectx_to_lctx ectx') lexpr)) lexprs; + + (ldecls, lexprs, ectx')

===================================== src/gambit.ml ===================================== @@ -0,0 +1,278 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.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/. *) + +open Printf + +open Debruijn +open Elexp + +type ldecls = Lexp.ldecls +type lexp = Lexp.lexp + +module Scm = struct + type t = + | Symbol of string + | List of t list + | String of string + | Integer of Z.t + | Float of float + + let begin' : t = Symbol "begin" + let case : t = Symbol "case" + let define : t = Symbol "define" + let double_right_arrow : t = Symbol "=>" + let else' : t = Symbol "else" + let lambda : t = Symbol "lambda" + let let' : t = Symbol "let" + let letrec : t = Symbol "letrec" + let quote : t = Symbol "quote" + let prim_vector : t = Symbol "##vector" + let prim_vector_ref : t = Symbol "##vector-ref" + + let is_valid_bare_symbol (name : string) : bool = + let length = String.length name in + let rec loop i = + if Int.equal length i + then true + else + match name.[i] with + | '|' | ''' | ' ' | '(' | ')' -> false + | _ -> loop (i + 1) + in loop 0 + + let escape_symbol (name : string) : string = + if is_valid_bare_symbol name + then name + else + let buffer = Buffer.create (String.length name) in + Buffer.add_char buffer '|'; + let encode_char = function + | '|' -> Buffer.add_string buffer {|||} + | c -> Buffer.add_char buffer c + in + String.iter encode_char name; + Buffer.add_char buffer '|'; + Buffer.contents buffer + + let symbol (name : string) : t = + Symbol (escape_symbol name) + + let rec string_of_exp (exp : t) : string = + match exp with + | Symbol (name) -> name + | List (elements) + -> "(" ^ String.concat " " (List.map string_of_exp elements) ^ ")" + | String (value) + -> let length = String.length value in + let buffer = Buffer.create length in + let encode_char = function + | '\x00' .. '\x06' as c + -> (Buffer.add_string buffer "\x"; + Buffer.add_string buffer (Printf.sprintf "%02d" (Char.code c))) + | '\x07' -> Buffer.add_string buffer "\a" + | '\x08' -> Buffer.add_string buffer "\b" + | '\x09' -> Buffer.add_string buffer "\t" + | '\' -> Buffer.add_string buffer "\\" + | '"' -> Buffer.add_string buffer "\"" + | c -> Buffer.add_char buffer c + in + String.iter encode_char value; + Buffer.contents buffer + | Integer (value) -> Z.to_string value + | Float (value) -> string_of_float value + + let print (output : out_channel) (exp : t) : unit = + output_string output (string_of_exp exp); + output_char output '\n' +end + +let gensym : string -> string = + let counter = ref 0 in + fun name -> + let i = !counter in + counter := i + 1; + let name = sprintf "%s%%%d" name i in + Scm.escape_symbol name + +module ScmContext = struct + (* Maps Debruijn indices to Scheme variable names. *) + type t = string Myers.myers + + let nil : t = Myers.nil + + let of_lctx (lctx : lexp_context) : t = + let f ((_, name), _, _) = Option.get name in + Myers.map f lctx + + let intro (sctx : t) (_, name : vname) : t * string = + let name = gensym (Option.value ~default:"g" name) in + (Myers.cons name sctx, name) + + 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 +end + +let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = + match elexp with + | Elexp.Imm (Sexp.String (_, s)) -> Scm.String s + + | Elexp.Imm (Sexp.Integer (_, i)) -> Scm.Integer i + + | Elexp.Imm (Sexp.Float (_, f)) -> Scm.Float f + + | Elexp.Builtin (_, "Sexp.node") -> Scm.Symbol "cons" + + | Elexp.Builtin (_, "Sexp.symbol") -> Scm.Symbol "string->symbol" + + | Elexp.Builtin (_, name) -> failwith ("TODO: Built-in "" ^ name ^ """) + + | Elexp.Var (_, index) + -> (match ScmContext.lookup sctx index with + | None -> Scm.Symbol "TODO" + | Some name -> Scm.Symbol name) + + | Elexp.Let (_, bindings, body) + -> if List.length bindings = 0 + then scheme_of_expr sctx body + else + let sctx, bindings = + Listx.fold_left_map ScmContext.intro_binding sctx bindings + in + let scheme_of_binding (name, elexp) = + Scm.List [Scm.Symbol name; scheme_of_expr sctx elexp] + in + Scm.List [Scm.letrec; + Scm.List (List.map scheme_of_binding bindings); + scheme_of_expr sctx body] + + | Elexp.Lambda (name, body) + -> let sctx', name = ScmContext.intro sctx name in + Scm.List [Scm.lambda; + Scm.List [Scm.Symbol name]; + scheme_of_expr sctx' body] + + | Elexp.Call (head, tail) + -> let scm_head = scheme_of_expr sctx head in + let scm_tail = List.map (scheme_of_expr sctx) tail in + Scm.List (scm_head :: scm_tail) + + | Elexp.Cons (arity, (_, name)) + -> let rec make_vars i vars = + match i with + | 0 -> vars + | _ -> make_vars (i - 1) (Scm.Symbol (gensym "") :: vars) + in + let vars = make_vars arity [] in + let vector_expr = + Scm.List (Scm.prim_vector + :: Scm.List [Scm.quote; Scm.symbol name] + :: List.rev vars) + in + let rec make_curried_lambda vars body = + match vars with + | [] -> body + | var :: vars' + -> let body' = Scm.List [Scm.lambda; Scm.List [var]; body] in + make_curried_lambda vars' body' + in + make_curried_lambda vars vector_expr + + | 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]) + + | Elexp.Type _ -> Scm.Symbol "lets-hope-its-ok-if-i-erase-this" + + | _ -> failwith ("[gambit] unsupported elexp: " ^ elexp_string elexp) + +let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * elexp) : Scm.t = + Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp]) + +let scheme_of_decls + (lctx : lexp_context) + (sctx : ScmContext.t) + (ldecls : ldecls) + : lexp_context * ScmContext.t * Scm.t = + + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + let sctx', eldecls = Listx.fold_left_map ScmContext.intro_binding sctx eldecls in + let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in + (lctx', sctx', sdecls)

===================================== src/lexer.ml ===================================== @@ -1,6 +1,6 @@ (* lexer.ml --- Second half of lexical analysis of Typer.

-Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2021 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -144,11 +144,11 @@ let lex tenv (pts : pretoken list) : sexp list = in gettokens pts bpos cpos (tok :: acc) in gettokens pts 0 0 []

-let lex_str (str: string) tenv = - let pretoks = prelex_string str in - lex tenv pretoks +let lex_source (source : #Source.t) tenv = + let pretoks = prelex source in + lex tenv pretoks

-let sexp_parse_str (str: string) tenv grm limit = - let toks = lex_str str tenv in - sexp_parse_all_to_list grm toks limit +let sexp_parse_source (source : #Source.t) tenv grm limit = + let toks = lex_source source tenv in + sexp_parse_all_to_list grm toks limit

===================================== src/lexp.ml ===================================== @@ -118,6 +118,7 @@ type ltype = lexp | SLlub of lexp * lexp

type ldecl = vname * lexp * ltype +type ldecls = ldecl list

type varbind = | Variable

===================================== src/main.ml ===================================== @@ -0,0 +1,109 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.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/. *) + +open Printf + +open Backend +open Debruijn +open Elab +open Fmt + +let arg_batch = ref false +let arg_files = ref [] +let backend_name = ref "interpreter" + +(* ./typer [options] files *) +let arg_defs = + [("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + + ("--verbosity", + Arg.String Log.set_typer_log_level_str, + "Set the logging level"); + + ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); + + ("--backend", + Arg.Symbol (["interpreter"; "gambit"], fun name -> backend_name := name), + "Select the backend"); + ] + +let welcome_message = +" Typer 0.0.0 - Interpreter - (c) 2016-2021 + + %quit (%q) : leave REPL + %help (%h) : print help +" + +let main () = + Arg.parse arg_defs (fun file -> arg_files := file :: !arg_files) ""; + + let is_batch = !arg_batch in + let file_names = List.rev !arg_files in + let backend = + match !backend_name with + | "interpreter" + -> (new ast_interpreter (ectx_to_lctx default_ectx) :> backend) + | "gambit" + -> (new gambit_compiler (ectx_to_lctx default_ectx) stdout :> backend) + | backend_name + -> (print_string ("unknown backend: " ^ backend_name); + exit 1) + in + + let interactive = backend#interactive in + let process_file = + if is_batch && Option.is_some interactive + then + fun (ectx, i) file_name + -> let ectx = REPL.process_file backend ectx file_name in + ectx, i + else + (print_string (make_title " TYPER REPL "); + print_string welcome_message; + print_string (make_sep '='); + flush stdout; + fun (ectx, i) file_name + -> printf " In[%02d] >> %%readfile %s\n" i file_name; + let ectx = REPL.process_file backend ectx file_name in + ectx, i + 1) + in + + let ectx, i = + try + let ectx, i = List.fold_left process_file (default_ectx, 0) file_names in + REPL.print_and_clear_log (); + ectx, i + with + | Log.Stop_Compilation msg + -> REPL.handle_stopped_compilation msg; + exit 1 + | Log.Internal_error msg as e + -> REPL.handle_stopped_compilation ("Internal error: " ^ msg); + raise e + | Log.User_error msg + -> REPL.handle_stopped_compilation ("Fatal user error: " ^ msg); + exit 1 + in + + match is_batch, backend#interactive with + | false, Some interactive -> REPL.repl i interactive ectx + | _ -> () + +let _ = main ()

===================================== src/myers.ml ===================================== @@ -75,6 +75,11 @@ let rec nthcdr n l =

let nth n l = car (nthcdr n l)

+let nth_opt (n : int) (l : 'a myers) : 'a option = + match nthcdr n l with + | Mnil -> None + | Mcons (x, _, _, _) -> Some x + (* While `nth` is O(log N), `set_nth` is O(N)! :-( *) let rec set_nth n v l = match (n, l) with | 0, Mcons (_, cdr, s, tail) -> Mcons (v, cdr, s, tail) @@ -136,3 +141,6 @@ let rec fold_right f l i = match l with let map f l = fold_right (fun x l' -> cons (f x) l') l nil

let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l + +let reverse (l : 'a myers) : 'a myers = + fold_left (fun cdr car -> cons car cdr) nil l

===================================== src/option.ml ===================================== @@ -30,3 +30,13 @@ let get (o : 'a option) : 'a = match o with | Some v -> v | None -> invalid_arg "expected Some" + +let value ~(default : 'a) (o : 'a option) : 'a = + match o with + | Some v -> v + | None -> default + +let is_some (o : 'a option) : bool = + match o with + | Some _ -> true + | None -> false

===================================== src/prelexer.ml ===================================== @@ -1,6 +1,6 @@ (* prelexer.ml --- First half of lexical analysis of Typer.

-Copyright (C) 2011-2020 Free Software Foundation, Inc. +Copyright (C) 2011-2021 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -50,114 +50,135 @@ let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) if utf8_head_p c then cp+1 else cp

-let rec prelex (file : string) (getline : unit -> string) ln ctx acc (doc : string) +let rec consume_until_newline (source : #Source.t) : unit = + match source#next_char with + | None | Some ('\n') -> () + | Some _ -> consume_until_newline source + +let rec prelex (source : #Source.t) ln ctx acc (doc : string) : pretoken list = - try - (* let fin = open_in file in *) - let line = getline () in - let limit = String.length line in - let nextline = prelex file getline (ln + 1) in - let rec prelex' ctx (bpos:bytepos) (cpos:charpos) acc doc = - let nexttok = prelex' ctx in - if bpos >= limit then nextline ctx acc doc else - match line.[bpos] with - | c when c <= ' ' -> nexttok (bpos+1) (cpos+1) acc doc - | '%' -> nextline ctx acc doc (* A comment. *) - (* line's bounds seems ok: String.sub line 1 0 == "" *) - | '@' -> nextline ctx acc (String.concat "\n" [doc; (String.sub line 1 (limit - 1))]) - | '"' (* A string. *) - -> let rec prestring bp cp chars = - if bp >= limit then - (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unterminated string"; - nextline ctx - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, "") - :: acc) "") - else - match line.[bp] with - | '"' -> - nexttok (bp+1) (cp+1) - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, - string_implode (List.rev chars)) - :: acc) "" - | '\' -> - (if bpos + 1 >= limit then - (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unterminated string"; - nextline ctx - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, - "") - :: acc) "") - else - match line.[bp + 1] with - | 't' -> prestring (bp+2) (cp+2) ('\t' :: chars) - | 'n' -> prestring (bp+2) (cp+2) ('\n' :: chars) - | 'r' -> prestring (bp+2) (cp+2) ('\r' :: chars) - | ('u' | 'U') -> - prelexer_error {file=file; line=ln; column=cp; docstr=doc} - "Unimplemented unicode escape"; - prestring (bp+2) (cp+2) chars - | char -> prestring (bp+2) (cp+2) (char :: chars)) - | char -> prestring (bp+1) (inc_cp cp char) (char :: chars) - in prestring (bpos+1) (cpos+1) [] - | '{' -> prelex' ((ln, cpos, bpos, acc) :: ctx) (bpos+1) (cpos+1) [] doc - | '}' - -> (match ctx with - | ((sln, scpos, _sbpos, sacc) :: ctx) -> - prelex' ctx (bpos+1) (cpos+1) - (Preblock ({file=file; line=sln; column=scpos; docstr=doc}, - List.rev acc, - {file=file; line=ln; column=(cpos + 1); docstr=doc}) - :: sacc) "" - | _ -> (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unmatched closing brace"; - prelex' ctx (bpos+1) (cpos+1) acc doc)) - | char (* A pretoken. *) - -> let rec pretok bp cp = - if bp >= limit then - nextline ctx (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, - string_sub line bpos bp) - :: acc) "" - else - match line.[bp] with - | (' '|'\t'|'\n'|'\r'|'%'|'"'|'{'|'}' ) - -> nexttok bp cp - (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, - string_sub line bpos bp) - :: acc) "" - | '\' when bp+1 < limit - -> let char = line.[bp + 1] in - pretok (bp + 2) (1 + inc_cp cp char) - | char -> pretok (bp+1) (inc_cp cp char) - in pretok (bpos+1) (inc_cp cpos char) - in prelex' ctx 0 1 acc doc (* Traditionally, column numbers start at 1 :-( *) - with End_of_file -> - match ctx with + + let nextline = prelex source (ln + 1) in + let rec prelex' ctx (cpos:charpos) acc doc = + let nexttok = prelex' ctx in + match source#peek_char with + | None + -> (match ctx with | [] -> List.rev acc - | ((ln, cpos, _, _) :: _ctx) -> - (prelexer_error {file=file; line=ln; column=cpos; docstr=""} - "Unmatched opening brace"; List.rev acc) - - -let prelex_file file = - let fin = open_in file - in prelex file (fun _ -> input_line fin) - (* Traditionally, line numbers start at 1 :-( *) - 1 [] [] "" - -let prelex_string str = - let pos = ref 0 in - let getline () = - let start = !pos in - if start >= String.length str then raise End_of_file else - let i = try String.index_from str start '\n' - with Not_found -> String.length str - 1 in - let npos = i + 1 in - pos := npos; - let line = string_sub str start npos in - (* print_string ("Read line: " ^ line); *) - line - in prelex "<string>" getline 1 [] [] "" + | ((ln, cpos, _) :: _ctx) -> + (prelexer_error {file=source#file_name; line=ln; column=cpos; docstr=""} + "Unmatched opening brace"; List.rev acc)) + + | Some ('\n') + -> source#advance; + nextline ctx acc doc + + | Some (c) when c <= ' ' + -> source#advance; + nexttok (cpos+1) acc doc + + (* A comment. *) + | Some ('%') + -> consume_until_newline source; + nextline ctx acc doc + + (* line's bounds seems ok: String.sub line 1 0 == "" *) + | Some ('@') + -> source#advance; + let start_offset = source#current_offset in + consume_until_newline source; + let new_doc = String.trim (source#slice_from_offset start_offset) in + nextline ctx acc (doc ^ "\n" ^ new_doc) + + (* A string. *) + | Some ('"') + -> source#advance; + let rec prestring cp chars = + match source#next_char with + | None | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + prelexer_error location "Unterminated string"; + nextline ctx (Prestring (location, "") :: acc) "" + + | Some ('"') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let pretoken = Prestring (location, string_implode (List.rev chars)) in + nexttok (cp + 1) (pretoken :: acc) "" + + | Some ('\') + -> (match source#next_char with + | None | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cp; docstr=doc} in + prelexer_error location "Unterminated escape sequence"; + nextline ctx (Prestring (location, "") :: acc) "" + | Some ('t') -> prestring (cp + 2) ('\t' :: chars) + | Some ('n') -> prestring (cp + 2) ('\n' :: chars) + | Some ('r') -> prestring (cp + 2) ('\r' :: chars) + | Some ('u') + -> let location = {file=source#file_name; line=ln; column=cp; docstr=doc} in + prelexer_error location "Unimplemented unicode escape"; + prestring (cp + 2) chars + | Some (c) -> prestring (cp + 2) (c :: chars)) + + | Some (char) -> prestring (inc_cp cp char) (char :: chars) + in prestring (cpos + 1) [] + + | Some ('{') + -> source#advance; + prelex' ((ln, cpos, acc) :: ctx) (cpos + 1) [] doc + + | Some ('}') + -> source#advance; + (match ctx with + | ((sln, scpos, sacc) :: ctx) -> + prelex' ctx (cpos+1) + (Preblock ({file=source#file_name; line=sln; column=scpos; docstr=doc}, + List.rev acc, + {file=source#file_name; line=ln; column=(cpos + 1); docstr=doc}) + :: sacc) "" + | _ -> (prelexer_error {file=source#file_name; line=ln; column=cpos; docstr=doc} + "Unmatched closing brace"; + prelex' ctx (cpos + 1) acc doc)) + + (* A pretoken. *) + | Some (c) + -> let start_offset = source#current_offset in + source#advance; + let rec pretok cp = + match source#peek_char with + | None | Some (' ' | '\t' | '%' | '"' | '{' | '}') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let text = source#slice_from_offset start_offset in + nexttok cp (Pretoken (location, text) :: acc) "" + + | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let text = source#slice_from_offset start_offset in + source#advance; + nextline ctx (Pretoken (location, text) :: acc) "" + + | Some ('\') + -> source#advance; + (match source#next_char with + | Some (char) -> pretok (1 + inc_cp cp char) + | None + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + source#advance; + let text = source#slice_from_offset start_offset in + prelexer_error location ("Unterminated escape sequence in: " ^ text); + nexttok (cp + 1) (Pretoken (location, text) :: acc) "") + + | Some (c) + -> source#advance; + pretok (inc_cp cp c) + in pretok (inc_cp cpos c) + in + (* Traditionally, column numbers start at 1 :-( *) + prelex' ctx 1 acc doc + +let prelex (source : #Source.t) : pretoken list = + (* Traditionally, line numbers start at 1 :-( *) + prelex source 1 [] [] ""

let pretoken_name pretok = match pretok with

===================================== src/source.ml ===================================== @@ -0,0 +1,113 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.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/. *) + +type location = Util.location + +(* A source object is text paired with a cursor. The text can be lazily loaded + as it is accessed byte by byte, but it must be retained for future reference + by error messages. *) +class virtual t = object (self) + (* A path if the text comes from a file, otherwise a meaningful identifier. *) + method virtual file_name : string + + (* Return the byte at the cursor, or None if the cursor is at the end of + the text. *) + method virtual peek_char : char option + + (* The current offset of the cursor in the file, in bytes. *) + method virtual current_offset : int + + (* Slices the text, from (and including) a starting offset and to (and + excluding) the curent cursor offset. + + Note that the source is required only to buffer the last line read and may + raise an Invalid_argument if the slice extends before the start of the + line. *) + method virtual slice_from_offset : int -> string + + (* Moves the cursor forward one byte *) + method virtual advance : unit + + method next_char : char option = + let c = self#peek_char in + self#advance; + c +end + +let read_buffer_length = 4096 + +class source_file file_name = object (self) + inherit t + + val in_channel = open_in file_name + val mutable end_of_line = false + val mutable line = "" + val mutable line_offset = 0 + val mutable offset = 0 + + method private peek_char_unchecked = + if offset < String.length line + then line.[offset] + else '\n' + + method peek_char = + if offset <= String.length line + then Some self#peek_char_unchecked + else + try + line_offset <- line_offset + 1 + String.length line; + line <- input_line in_channel; + offset <- 0; + Some self#peek_char_unchecked + with + | End_of_file -> None + + method advance = + offset <- offset + 1 + + method current_offset = line_offset + offset + + method slice_from_offset start_offset = + let relative_start_offset = start_offset - line_offset in + String.sub line relative_start_offset (offset - relative_start_offset) + + method file_name = file_name +end + +class source_string source = object + inherit t + + val mutable offset = 0 + + method peek_char = + if offset < String.length source + then Some (source.[offset]) + else None + + method advance = + offset <- offset + 1 + + method current_offset = offset + + method slice_from_offset start_offset = + String.sub source start_offset (offset - start_offset) + + method file_name = "<string>" +end

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