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

Commits: e229996a by Simon Génier at 2021-04-09T13:41:26-04:00 Merge branch 'extract-args-from-repl'

- - - - - 252f6038 by Simon Génier at 2021-04-26T16:33:24-04:00 Introduce swappable backends for Typer.

The backends themselves are objects which must implement the new backend abstract class. I also shuffled some code, mostly in the module REPL, so that is it more focused on evaluating interactive code. Finally, I moved code that was more concerned with loading regular Typer code in typer.ml and elab.ml.

- - - - - 33b205c5 by Simon Génier at 2021-04-26T16:34:24-04:00 Add tests for the lexer.

In addition to the tests themselves, added a few functions that were necessary. In particular there is now Pretoken.equal in Prelexer and Location.equal in Source that are equality predicates on pretokens and locations.

I also added in Sexp.sexp_string support for printing the location along with its associated sexp. This is useful in tests, when we check that the locations are correct, otherwise we would print two identical sexps!

- - - - - ea5cae0f by Simon Génier at 2021-04-28T13:29:47-04:00 Merge branch 'lexer-tests'

- - - - - 9723f3cf by Simon Génier at 2021-04-28T13:30:29-04:00 Merge branch 'backend-object'

- - - - - 73ae25a9 by Simon Génier at 2021-04-28T13:34:46-04:00 Add a backend to compile Typer to Scheme.

- - - - -

15 changed files:

- src/REPL.ml - + src/backend.ml - src/elab.ml - src/eval.ml - + src/gambit.ml - src/lexp.ml - src/listx.ml - src/option.ml - src/prelexer.ml - src/sexp.ml - src/source.ml - tests/dune - + tests/gambit_test.ml - + tests/lexer_test.ml - typer.ml

Changes:

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

-open Util +open Backend +open Debruijn +open Eval open Fmt - -open Prelexer open Lexer -open Sexp open Lexp +open Prelexer +open Sexp +open Util

-open Eval - -open Grammar - -open Env -open Debruijn module OL = Opslexp module EL = Elexp

@@ -58,7 +54,7 @@ let print_input_line i = ralign_print_int i 2; print_string "] >> "

-let ieval_error = Log.log_error ~section:"IEVAL" +let error = Log.log_error ~section:"REPL"

let print_and_clear_log () = if (not Log.typer_log_config.Log.print_at_log) then @@ -98,84 +94,6 @@ let rec read_input i =

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 source 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 = prelex source 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 source ectx rctx = - let pres = prelex source 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 help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment @@ -187,80 +105,103 @@ let help_msg = %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 source = new Source.source_file file in - let (ret, lctx, rctx) = raw_eval source 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 - +(* Elaborate Typer source from an interactive session. Like "normal" Typer, + declarations are grouped in blocks that are mutually recursive, but unlike + "normal" Typer, expressions are also accepted in addition to declarations. + + Note that all declarations are pulled before expressions, i.e. an expression + can refer to variable introduced by later declarations. *) +let eval_interactive + (interactive : #interactive_backend) + (i : int) + (ectx : elab_context) + (input : string) + : 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 source = new Source.source_string input 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 + + (* FIXME We take the parsed input here but we should take the unparsed tokens + directly instead *) + let ldecls, ectx' = Elab.lexp_p_decls decls [] ectx in + + let lexprs = Elab.lexp_parse_all exprs ectx' in + List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs; + + List.iter interactive#process_decls ldecls; + print_and_clear_log (); + + let values = List.map interactive#eval_expr lexprs in + List.iter (Eval.print_eval_result i) values; + print_and_clear_log (); + + ectx'

(* Specials commands %[command-name] [args] *) -let rec repl i clxp rctx = - let repl = repl (i + 1) in +let rec repl i (interactive : #interactive_backend) (ectx : elab_context) = let ipt = try read_input i with End_of_file -> "%quit" in + let ectx = 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)) + | "%quit" | "%q" -> exit 0 + | "%help" | "%h" -> (print_string help_msg; ectx) + | "%calltrace" | "%ct" -> (print_eval_trace None; ectx) + | "%typertrace" | "%tt" -> (print_typer_trace None; ectx) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table); ectx)

(* 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; + let ectx = List.fold_left (Elab.eval_file interactive) ectx args in + print_and_clear_log (); + ectx | "%who"::args | "%w"::args -> ( let _ = match args with - | ["all"] -> dump_rte_ctx rctx - | _ -> print_rte_ctx rctx in - repl clxp rctx) + | ["all"] -> interactive#dump_rte_ctx + | _ -> interactive#print_rte_ctx in + ectx) | "%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) + | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) + | _ -> print_lexp_ctx (ectx_to_lctx ectx) in + ectx)

| cmd::_ -> - ieval_error (" "" ^ cmd ^ "" is not a correct repl command"); - repl clxp rctx - | _ -> repl clxp rctx) + error (" "" ^ cmd ^ "" is not a correct repl command"); + ectx + | _ -> ectx)

(* eval input *) | _ -> - try - let source = new Source.source_string ipt in - let (ret, clxp, rctx) = (ieval source clxp rctx) in - print_and_clear_log (); - List.iter (print_eval_result i) ret; - repl clxp rctx - with + try eval_interactive interactive i ectx ipt with | Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; repl clxp rctx) + (handle_stopped_compilation msg; ectx) | Log.Internal_error msg -> (handle_stopped_compilation ("Internal error: " ^ msg); - repl clxp rctx) + ectx) | Log.User_error msg -> (handle_stopped_compilation ("Fatal user error: " ^ msg); - repl clxp rctx) + ectx) + in + repl (i + 1) interactive ectx

===================================== src/backend.ml ===================================== @@ -0,0 +1,48 @@ +(* 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. *) + +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

===================================== src/elab.ml ===================================== @@ -1338,6 +1338,12 @@ and lexp_decls_1 pending_decls pending_defs in (Log.stop_on_error (); res))

+(* Why is the return value a list of list? + - each `(vname * lexp * ltype)` is a definition + - each `(vname * lexp * ltype) 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. *) and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = let rec impl sdecls tokens ctx = @@ -1943,3 +1949,21 @@ let eval_decl_str str ectx rctx = let lctx = ectx_to_lctx ectx in let _, elxps = Listx.fold_left_map (OL.clean_decls) lctx lxps in (EV.eval_decls_toplevel elxps rctx), ectx' + +let eval_file + (backend : #Backend.backend) + (ectx : elab_context) + (file_name : string) + : elab_context = + + try + let source = new Source.source_file file_name in + let pretokens = prelex source in + let tokens = lex Grammar.default_stt pretokens in + let ldecls, ectx' = lexp_p_decls [] tokens ectx in + List.iter backend#process_decls ldecls; + ectx' + with + | Sys_error _ + -> (error (Printf.sprintf {|file %s does not exist.|} file_name); + ectx)

===================================== src/eval.ml ===================================== @@ -1187,3 +1187,23 @@ let from_lctx (lctx: lexp_context): runtime_env = (* build a rctx from a ectx. *) let from_ectx (ctx: elab_context): runtime_env = from_lctx (ectx_to_lctx ctx) + +class ast_interpreter lctx = object + inherit Backend.interactive_backend + + val mutable rctx = from_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + rctx <- eval_decls eldecls rctx; + lctx <- lctx' + + method eval_expr lexp = + let elexp = Opslexp.erase_type lctx lexp in + debug_eval elexp rctx + + method print_rte_ctx = Env.print_rte_ctx rctx + + method dump_rte_ctx = Env.dump_rte_ctx rctx +end

===================================== src/gambit.ml ===================================== @@ -0,0 +1,302 @@ +(* 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 + Buffer.add_char buffer '"'; + 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.add_char buffer '"'; + 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' + + let describe (exp : t) : string = + match exp with + | Symbol _ -> "a symbol" + | List _ -> "a list" + | String _ -> "a string" + | Integer _ -> "an integer" + | Float _ -> "a float" + + let rec equal (l : t) (r : t) : bool = + match l, r with + | Symbol l, Symbol r | String l, String r + -> String.equal l r + | List ls, List rs -> Listx.equal equal ls rs + | Integer l, Integer r -> Z.equal l r + | Float l, Float r -> Float.equal l r + | _ -> false +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]) + +class gambit_compiler lctx output = object + inherit Backend.backend + + val mutable sctx = ScmContext.of_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + 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 + + sctx <- sctx'; + lctx <- lctx'; + Scm.print output sdecls; +end

===================================== 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/listx.ml ===================================== @@ -44,3 +44,10 @@ let fold_left_map loop fold_acc (new_element :: map_acc) bs in loop i [] bs + +(* Backport from 4.12. *) +let rec equal (p : 'a -> 'a -> bool) (ls : 'a list) (rs : 'a list) : bool = + match ls, rs with + | l :: ls', r :: rs' -> p l r && equal p ls' rs' + | _ :: _, [] | [], _ :: _ -> false + | [], [] -> true

===================================== src/option.ml ===================================== @@ -35,3 +35,8 @@ 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 ===================================== @@ -27,9 +27,23 @@ let prelexer_error loc = Log.log_error ~section:"PRELEXER" ~loc type pretoken = | Pretoken of location * string | Prestring of location * string - (* | Preerror of location * string *) | Preblock of location * pretoken list * location

+module Pretoken = struct + type t = pretoken + + (* Equality up to location, i.e. the location is not considered. *) + let rec equal (l : t) (r : t) = + match l, r with + | Pretoken (_, l_name), Pretoken (_, r_name) + -> String.equal l_name r_name + | Prestring (_, l_text), Prestring (_, r_text) + -> String.equal l_text r_text + | Preblock (_, l_inner, _), Preblock (_, r_inner, _) + -> Listx.equal equal l_inner r_inner + | _ -> false +end + (*************** The Pre-Lexer phase *********************)

(* In order to allow things like "module Toto { open Titi; ... }" where

===================================== src/sexp.ml ===================================== @@ -67,8 +67,24 @@ let emptyString = hString ""

(*************** The Sexp Printer *********************)

-let rec sexp_string sexp = - match sexp with +let rec sexp_location (s : sexp) : location = + match s with + | Block (l, _, _) -> l + | Symbol (l, _) -> l + | String (l, _) -> l + | Integer (l, _) -> l + | Float (l, _) -> l + | Node (s, _) -> sexp_location s + +(* Converts a sexp to a string, optionally printing locations as a list preceded + by a Racket-style reader comment (#;). *) +let rec sexp_string ?(print_locations = false) sexp = + (if print_locations + then + let {file; line; column; _} = sexp_location sexp in + Printf.sprintf "#;("%s" %d %d) " file line column + else "") + ^ match sexp with | Block(_,pts,_) -> "{" ^ (pretokens_string pts) ^ " }" | Symbol(_, "") -> "()" (* Epsilon *) | Symbol(_, name) -> name @@ -76,21 +92,12 @@ let rec sexp_string sexp = | Integer(_, n) -> Z.to_string n | Float(_, x) -> string_of_float x | Node(f, args) -> - let str = "(" ^ (sexp_string f) in - (List.fold_left (fun str sxp -> - str ^ " " ^ (sexp_string sxp)) str args) ^ ")" + let str = "(" ^ (sexp_string ~print_locations f) in + (List.fold_left (fun str sxp -> + str ^ " " ^ (sexp_string ~print_locations sxp)) str args) ^ ")"

let sexp_print sexp = print_string (sexp_string sexp)

-let rec sexp_location s = - match s with - | Block (l, _, _) -> l - | Symbol (l, _) -> l - | String (l, _) -> l - | Integer (l, _) -> l - | Float (l, _) -> l - | Node (s, _) -> sexp_location s - let sexp_name s = match s with | Block _ -> "Block"

===================================== src/source.ml ===================================== @@ -20,6 +20,19 @@

type location = Util.location

+module Location = struct + type t = location + + let equal (l : t) (r : t) = + let open Util in + let {file = l_file; line = l_line; column = l_column; docstr = l_doc} = l in + let {file = r_file; line = r_line; column = r_column; docstr = r_doc} = r in + String.equal l_file r_file + && Int.equal l_line r_line + && Int.equal l_column r_column + && String.equal l_doc r_doc +end + (* 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. *)

===================================== tests/dune ===================================== @@ -4,8 +4,10 @@ (names elab_test env_test eval_test + gambit_test inverse_test lexp_test + lexer_test macro_test sexp_test unify_test)

===================================== tests/gambit_test.ml ===================================== @@ -0,0 +1,190 @@ +(* 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/. *) + +(** Tests for the compilation of Lexps to Gambit Scheme code. + + There is more support code in this file than I would have liked. This is due + to the fact that there is a lot of α-renaming and gensymming so we can't + directly compare s-expressions. Instead, I defined predicates for lists, + strings, known symbols, unknown gensymmed symbols, etc. *) + +open Typerlib + +open Utest_lib + +open Gambit + +let fail_on_exp exp = + Printf.printf "in %s\n" (Scm.string_of_exp exp); + false + +let type_error expected actual = + Printf.printf + "%sExpected %s, but got %s%s\n" + Fmt.red + expected + (Scm.describe actual) + Fmt.reset; + fail_on_exp actual + +let string expected actual = + match actual with + | Scm.String value when String.equal expected value -> true + | Scm.String _ + -> Printf.printf + "%sExpected a string equal to "%s"%s\n" + Fmt.red + expected + Fmt.reset; + fail_on_exp actual + | _ -> type_error "a string" actual + +let sym expected actual = + match actual with + | Scm.Symbol value when String.equal expected value -> true + | Scm.Symbol _ + -> Printf.printf + "%sExpected a symbol equal to |%s|%s\n" + Fmt.red + expected + Fmt.reset; + fail_on_exp actual + | _ -> type_error "a symbol" actual + +let has_prefix prefix value = + String.length prefix < String.length value + && String.equal prefix (String.sub value 0 (String.length prefix)) + +type var = Var of string | UniqueVar of string + +let make_var prefix = ref (Var prefix) + +let gensym var actual = + match actual with + | Scm.Symbol value + -> (match !var with + | UniqueVar prev when String.equal value prev -> true + | UniqueVar prev + -> Printf.printf + "%sExpected a symbol equal to |%s|%s\n" + Fmt.red + prev + Fmt.reset; + fail_on_exp actual + | Var prefix when has_prefix (prefix ^ "%") value + -> var := UniqueVar value; + true + | Var prefix + -> Printf.printf + "%sExpected a symbol starting with |%s|%s\n" + Fmt.red + prefix + Fmt.reset; + fail_on_exp actual) + | _ -> type_error "a symbol" actual + +(* Returns whether the s-expression is list and that that the element at an + index satifies the predicate at the same index. *) +let list (expected : (Scm.t -> bool) list) (actual : Scm.t) : bool = + match actual with + | Scm.List value + -> let rec loop i es xs = + match es, xs with + | e :: es, x :: xs + -> if e x + then loop (i + 1) es xs + else fail_on_exp actual + | _ :: _, [] | [], _ :: _ + -> Printf.printf + "%sExpected a list of %d elements, but got %d elements%s\n" + Fmt.red + (List.length expected) + (List.length value) + Fmt.reset; + fail_on_exp actual + | [], [] -> true + in + loop 0 expected value + | _ -> type_error "a list" actual + +let test_compile name source predicate = + let compile () = + let ectx = Elab.default_ectx in + let lctx = Debruijn.ectx_to_lctx ectx in + let lexps = Elab.lexp_expr_str source ectx in + let elexps = List.map (Opslexp.erase_type lctx) lexps in + let sctx = ScmContext.of_lctx lctx in + let actual = List.map (scheme_of_expr sctx) elexps in + match actual with + | head :: [] + -> if predicate head + then success + else failure + | _ + -> Printf.printf "expected 1 expression, but got %d" (List.length actual); + failure + in + Utest_lib.add_test "GAMBIT" name compile + +let () = + test_compile + "Typer string to Scheme string" + {|"Hello"|} + (string "Hello") + +let () = + let var = make_var "x" in + test_compile + "Typer lambda to Scheme lambda" + {|lambda (x : Int) -> x|} + (list [sym "lambda"; list [gensym var]; gensym var]) + +let () = + test_compile + "Typer data cons of 0 arguments to Scheme vector" + {|datacons (typecons T V) V|} + (list [sym "##vector"; list [sym "quote"; sym "V"]]) + +let () = + let var = make_var "" in + test_compile + "Typer data cons of 1 argument to Scheme function" + {|datacons (typecons T (V Int)) V|} + (list [sym "lambda"; + list [gensym var]; + list [sym "##vector"; + list [sym "quote"; sym "V"]; + gensym var]]) + +let () = + let var_0 = make_var "" in + let var_1 = make_var "" in + test_compile + "Typer data cons of 2 arguments to Scheme function" + {|datacons (typecons T (V Int Int)) V|} + (list [sym "lambda"; + list [gensym var_0]; + list [sym "lambda"; + list [gensym var_1]; + list [sym "##vector"; + list [sym "quote"; sym "V"]; + gensym var_0; + gensym var_1]]]) + +let () = Utest_lib.run_all ()

===================================== tests/lexer_test.ml ===================================== @@ -0,0 +1,102 @@ +(* 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 Typerlib + +open Utest_lib + +open Prelexer +open Sexp +open Source + +let test_lex name pretokens expected = + (* Unlike the version in the Sexp module, this version of equality considers + locations. *) + let rec sexp_equal actual expected = + match actual, expected with + | Sexp.Block (actual_start, actual_pretokens, actual_end), + Sexp.Block (expected_start, expected_pretokens, expected_end) + -> Location.equal actual_start expected_start + && Listx.equal Pretoken.equal actual_pretokens expected_pretokens + && Location.equal actual_end expected_end + | Sexp.Symbol (actual_location, actual_name), + Sexp.Symbol (expected_location, expected_name) + -> Location.equal actual_location expected_location + && String.equal actual_name expected_name + | Sexp.Node (actual_head, actual_tail), + Sexp.Node (expected_head, expected_tail) + -> sexp_equal actual_head expected_head + && Listx.equal sexp_equal actual_tail expected_tail + | _, _ -> false + in + let lex () = + let actual = Lexer.lex Grammar.default_stt pretokens in + if Listx.equal sexp_equal actual expected + then success + else + ((* Only print locations if the Sexp are otherwise identical so its easier + to spot the problem. *) + let print_locations = + Listx.equal Sexp.sexp_equal actual expected + in + let print_token token = + Printf.printf "%s\n" (sexp_string ~print_locations token) + in + Printf.printf "%sExpected:%s\n" Fmt.red Fmt.reset; + List.iter print_token expected; + Printf.printf "%sActual:%s\n" Fmt.red Fmt.reset; + List.iter print_token actual; + failure) + in + add_test "LEXER" name lex + +let l : location = + {file = "test.typer"; line = 1; column = 1; docstr = ""} + +let () = + test_lex + "Inner operator inside a presymbol" + [Pretoken (l, "a.b")] + [Node (Symbol ({l with column = 2}, "__.__"), + [Symbol ({l with column = 1}, "a"); + Symbol ({l with column = 3}, "b")])] + +let () = + test_lex + "Inner operators at the beginning of a presymbol" + [Pretoken (l, ".b")] + [Node (Symbol ({l with column = 1}, "__.__"), + [epsilon {l with column = 1}; + Symbol ({l with column = 2}, "b")])] + +let () = + test_lex + "Inner operators at the end of a presymbol" + [Pretoken (l, "a.")] + [Node (Symbol ({l with column = 2}, "__.__"), + [Symbol ({l with column = 1}, "a"); + epsilon {l with column = 3}])] + +let () = + test_lex + "An inner operator by itself is a simple symbol" + [Pretoken (l, ".")] + [Symbol ({l with column = 1}, ".")] + +let () = run_all ()

===================================== typer.ml ===================================== @@ -21,6 +21,9 @@

open Typerlib

+open Backend +open Debruijn + let welcome_msg = " Typer 0.0.0 - Interpreter - (c) 2016-2021

@@ -29,6 +32,7 @@ let welcome_msg = "

let arg_batch = ref false +let arg_backend_name = ref "interpreter"

let arg_files = ref [] let add_input_file file = @@ -46,27 +50,48 @@ let arg_defs = ("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, "Print the full lexp context on error."); + + ("--backend", + Arg.Symbol (["interpreter"; "gambit"], fun name -> arg_backend_name := name), + "Select the backend"); ]

let main () = let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in Arg.parse arg_defs add_input_file usage; - let files = List.rev !arg_files in - let is_interactive = not !arg_batch in

- if is_interactive - then - (print_string (Fmt.make_title " TYPER REPL "); - print_string welcome_msg; - print_string (Fmt.make_sep '-'); - flush stdout); + let ectx = Elab.default_ectx in + let backend = + let lctx = ectx_to_lctx ectx in + match !arg_backend_name with + | "gambit" -> (new Gambit.gambit_compiler lctx stdout :> backend) + | _ -> (new Eval.ast_interpreter lctx :> backend) + in + let interactive = backend#interactive in + let file_names = List.rev !arg_files in + let is_interactive = not !arg_batch && Option.is_some interactive in + + let process_file = + if is_interactive + then + (print_string (Fmt.make_title " TYPER REPL "); + print_string welcome_msg; + print_string (Fmt.make_sep '-'); + flush stdout; + fun ectx i file_name + -> Printf.printf " In[%02d] >> %%readfile %s\n" i file_name; + Elab.eval_file backend ectx file_name) + else + fun ectx _ file_name -> Elab.eval_file backend ectx file_name + in

- let i, ectx, rctx = + let ectx, i = try - let ectx = Elab.default_ectx in - let rctx = Elab.default_rctx in let res = - REPL.readfiles files (1, ectx, rctx) is_interactive + List.fold_left + (fun (ectx, i) file_name -> (process_file ectx i file_name, i + 1)) + (ectx, 0) + file_names in REPL.print_and_clear_log (); res @@ -82,7 +107,8 @@ let main () = exit 1 in

- if is_interactive - then REPL.repl i ectx rctx + match is_interactive, interactive with + | true, Some (interactive) -> REPL.repl i interactive ectx + | _ -> ()

let () = main ()

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