Simon Génier pushed to branch opt-inline at Stefan / Typer

Commits: 50eca407 by Simon Génier at 2021-03-14T22:34:09-04:00 Inline let-binding to vars and built-ins.

- - - - -

3 changed files:

- src/frontend.ml - + src/inline.ml - src/myers.ml

Changes:

===================================== src/frontend.ml ===================================== @@ -33,7 +33,13 @@ let decls_of_source 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') + let _, ldecls' = + Listx.fold_left_map + Inline.inline_decls + (Inline.InlContext.ictx_of_lctx (ectx_to_lctx ectx)) + ldecls + in + (ldecls', ectx')

(** Elaborate Typer source from an interactive session. The difference with normal Typer is that expressions are also accepted in addition to

===================================== src/inline.ml ===================================== @@ -0,0 +1,137 @@ +(* 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 Lexp + +type symbol = Sexp.symbol +module SMap = Util.SMap +let dummy_location = Util.dummy_location + +type inl_action = + | Opaque + | InlineBuiltin of lexp + | InlineVar of vname * int + +module InlContext = struct + type t = (vname * inl_action) Myers.myers + + let intro_opaque (ictx : t) (name : vname) : t = + Myers.cons (name, Opaque) ictx + + let intro (ictx : t) (name : vname) (lexp : lexp) : t = + match Lexp.nosusp lexp with + | (Lexp.Var (name', index), _) + -> Myers.cons (name, InlineVar (name', index)) ictx + | (Lexp.Builtin _, _ as lexp') + -> Myers.cons (name, InlineBuiltin lexp') ictx + | _ -> intro_opaque ictx name + + let intro_decl (ictx : t) (name, value, _ : ldecl) : t = + intro ictx name value + + let intro_decls (ictx : t) (ldecls : ldecls) : t = + List.fold_left intro_decl ictx ldecls + + let ictx_of_lctx (lctx : Debruijn.lexp_context) : t = + let rec loop lctx ictx = + match lctx with + | Myers.Mnil -> Myers.reverse ictx + | Myers.Mcons ((name, LetDef (offset, value), _), tail, _, _) + -> loop tail (intro ictx name (mkSusp value (S.shift (1 - offset)))) + | Myers.Mcons ((name, _, _), tail, _, _) + -> loop tail (intro_opaque ictx name) + in + loop lctx Myers.nil + + let lookup (ictx : t) ((_, expected_name), index : vref) : inl_action = + match Myers.nth_opt index ictx with + | Some ((_, actual_name), _) when actual_name <> expected_name + -> Log.log_fatal + (Printf.sprintf + {|expected "%s", but got "%s"\n|} + (maybename expected_name) + (maybename actual_name)) + | Some (_, action) -> action + | _ -> Opaque +end + +let rec inline (ictx : InlContext.t) (lexp : lexp) : lexp = + match Lexp.nosusp lexp with + | Lexp.Var (_, index as vref), _ + -> (match InlContext.lookup ictx vref with + | InlineBuiltin lexp' + -> lexp' + | InlineVar (name, index') + -> mkVar (name, index + index') + | _ -> lexp) + + | Lexp.Let (location, bindings, body), _ + -> let ictx' = InlContext.intro_decls ictx bindings in + let inline_binding (name, value, ty) = + let value' = inline ictx' value in + (name, value', ty) + in + let bindings' = List.map inline_binding bindings in + let body' = inline ictx' body in + Lexp.mkLet (location, bindings', body') + + | Lexp.Lambda (kind, arg_name, arg_ty, body), _ + -> let ictx' = InlContext.intro_opaque ictx arg_name in + let body' = inline ictx' body in + Lexp.mkLambda (kind, arg_name, arg_ty, body') + + | Lexp.Call (head, tail), _ + -> let inline_arg (kind, value) = (kind, inline ictx value) in + Lexp.mkCall (inline ictx head, List.map inline_arg tail) + + | Lexp.Case (location, subject, return_ty, branches, default), _ + -> let inline_branch (location, names, body) = + let branch_ictx = + InlContext.intro_opaque + (List.fold_left + (fun ictx (_, name) -> InlContext.intro_opaque ictx name) + ictx + names) + (dummy_location, None) + in + let body' = inline branch_ictx body in + (location, names, body') + in + let subject' = inline ictx subject in + let branches' = SMap.map inline_branch branches in + let default' = + match default with + | None -> None + | Some (default_name, default_body) + -> let ictx' = InlContext.intro ictx default_name subject' in + Some (default_name, inline ictx' default_body) + in + Lexp.mkCase (location, subject', return_ty, branches', default') + + | lexp' -> lexp' + +let inline_decls + (ictx : InlContext.t) + (ldecls : ldecls) + : InlContext.t * ldecls = + + let ictx' = InlContext.intro_decls ictx ldecls in + let inline_decl (name, lexp, ty) = (name, inline ictx' lexp, ty) in + (ictx', List.map inline_decl ldecls)

===================================== src/myers.ml ===================================== @@ -141,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 (m : 'a myers) : 'a myers = + fold_left (fun tail head -> cons head tail) nil m

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/50eca4074475daa5c450509ffd6d60175b...