Simon Génier pushed to branch backend-object at Stefan / Typer

Commits: 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.

- - - - -

8 changed files:

- src/REPL.ml - + src/backend.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/listx.ml - src/option.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/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

===================================== typer.ml ===================================== @@ -51,22 +51,34 @@ let arg_defs = 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 = new Eval.ast_interpreter (Debruijn.ectx_to_lctx ectx) 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 i, ectx, rctx = + 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 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 +94,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/-/commit/252f603860736dd60a7775a167112d6df7...