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

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

- - - - - 965cc049 by Simon Génier at 2021-04-29T11:46:14-04:00 Merge branch 'gambit'

- - - - -

4 changed files:

- + src/gambit.ml - tests/dune - + tests/gambit_test.ml - typer.ml

Changes:

===================================== 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

===================================== tests/dune ===================================== @@ -4,6 +4,7 @@ (names elab_test env_test eval_test + gambit_test inverse_test lexp_test lexer_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 ()

===================================== 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,6 +50,10 @@ 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 () = @@ -53,7 +61,12 @@ let main () = Arg.parse arg_defs add_input_file usage;

let ectx = Elab.default_ectx in - let backend = new Eval.ast_interpreter (Debruijn.ectx_to_lctx 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

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9723f3cf5add3f4bda6a7dfaa2353f2fc...