April 2021 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][backend-object] Introduce swappable backends for Typer.
by Simon Génier (＠ilovemonoids) 26 Apr '21

26 Apr '21

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(a)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/252f603860736dd60a7775a167112d6df… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/252f603860736dd60a7775a167112d6df… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] kind of completion and command(still to fix)
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 26 Apr '21

26 Apr '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 7783aed8 by Soilih BEN SOILIH at 2021-04-26T14:08:17-06:00 kind of completion and command(still to fix) - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -117,6 +117,60 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list in diagnostic ) log_tab + + (*little method to test completion*) + let little_fonc el = + match el with + | "lambda" -> "lambda (pattern) -> pattern ;" + | "case" -> "case scrutinee \n | pattern -> pattern ;" + | "let" -> "let_in_ (_=_ x ()) x ;" + | "if" -> " if_then_else_ x \"x is true\" \"x is false\"" + | _ -> "" + + (* + type t = + | Text + | Method + | Function + | Constructor + | Field + | Variable + | Class + | Interface + | Module + | Property + | Unit + | Value + | Enum + | Keyword + | Snippet + | Color + | File + | Reference + | Folder + | EnumMember + | Constant + | Struct + | Event + | Operator + | TypeParameter + *) + + let little_kind el = + match el with + | "lambda" -> Lsp.Types.CompletionItemKind.Text + | "case" -> Lsp.Types.CompletionItemKind.Function + | "let" -> Lsp.Types.CompletionItemKind.Text + | "if" -> Lsp.Types.CompletionItemKind.Text + | _ -> Lsp.Types.CompletionItemKind.Text + + let little_detail el = + match el with + | "lambda" -> "define a function" + | "case" -> "pattern matching" + | "let" -> "let...in" + | "if" -> "if...condition" + | _ -> "" (* Lsp server class @@ -198,10 +252,45 @@ class lsp_server = let e = Some r in let f = Linol_lwt.return e in f - method! config_definition = Some (`Bool true) + method! config_definition = Some (`Bool true) - method! config_hover = Some (`Bool true) - + method! config_hover = Some (`Bool true) + + + method! on_req_execute_command ~notify_back _c _args = + match _c with + | "typer" -> let file = "command.txt" in + let message = _c in (* Write message to file *) + let oc = open_out file in (* create or truncate file, return channel *) + Printf.fprintf oc "%s\n" message; (* write something *) + close_out oc; (* flush and close the channel *) + let h = Lsp.Types.Command.yojson_of_t + (Lsp.Types.Command.create ~title:_c ~command:_c () ) in + let e = Linol_lwt.return h in e + | _ -> assert false + + method! on_req_completion ~notify_back ~uri ~pos ~ctx doc_state = + match Hashtbl.find buffers uri with + | state_after_processing -> (*let (log_list,ast) = state_after_processing in + let (list_list, ectx) = ast in*) + let tab = ["lambda";"case";"let";"if"] in + let (loc_start, _) = typer_pos_of_lsp_pos pos in + let range = lsp_range_of_loc loc_start in + let r = List.map (fun x -> + let label = x in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(little_fonc x) in + let kind = little_kind x in + let detail = little_detail x in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:detail () + in + ci + + ) tab in + let e = Some (`List r) in + let f = Linol_lwt.return e in f + end (* Main code View it on GitLab: https://gitlab.com/monnier/typer/-/commit/7783aed82009f2dd093029623ed1b3b7d… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/7783aed82009f2dd093029623ed1b3b7d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 4 commits: m
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 23 Apr '21

23 Apr '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 5ee099ae by Soilih BEN SOILIH at 2021-04-21T09:39:33-06:00 m - - - - - 79fc9315 by Soilih BEN SOILIH at 2021-04-21T09:50:16-06:00 -* - - - - - 8ad9bedf by Soilih BEN SOILIH at 2021-04-23T03:21:14-06:00 - - - - - - 3eb5e83e by Soilih BEN SOILIH at 2021-04-23T04:07:32-06:00 hover and definition update - - - - - 2 changed files: - samples/soilih.typer - src/typer_lsp_server.ml Changes: ===================================== samples/soilih.typer ===================================== @@ -1 +1,3 @@ -let a = 3 b = 4 in a + b ; \ No newline at end of file +add1 n = n + 1 ; +h = 2 ; +a = 2; ===================================== src/typer_lsp_server.ml ===================================== @@ -80,8 +80,16 @@ let rec search_a_vname_with_a_given_position (vname_list: Util.vname list) (loca | hd::tl -> let (loc, _) = hd in if (loc.line == location.line) && (loc.column == location.column) then hd else search_a_vname_with_a_given_position tl location + +let rec search_lexp_with_a_location (lexp_list: Lexp.lexp list) (location : Util.location): Lexp.lexp option = + match lexp_list with + | [] -> None + | hd::tl -> let r = Lexp.lexp_location hd in + if (r.line == location.line) && (r.column == location.column) then Some hd + else search_lexp_with_a_location tl location let readstring (str:string) = + (* Log.clear_log () ; *) let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) let ast = Elab.lexp_decl_str str ectx in @@ -155,19 +163,24 @@ class lsp_server = method on_notif_doc_did_close ~notify_back:_ d : unit Linol_lwt.t = Hashtbl.remove buffers d.uri; Linol_lwt.return () - + method! on_req_definition ~notify_back ~uri ~pos _st = match Hashtbl.find buffers uri with - | state_after_processing -> let (log_list,ast) = state_after_processing in - let (list_list, ectx) = ast in + | state_after_processing -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in - let pi = List.map (fun x -> let (a,b,c) = x in a ) tab in - let loc = List.map (fun x -> vname_to_lsp_loc ~vname:x ~uri:uri) pi in - let ret = `Location loc in - Some ret + let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in + let (loc_start,_) = typer_pos_of_lsp_pos pos in + let r = Option.get(search_lexp_with_a_location lexp_list loc_start) in + let loc = Lexp.lexp_location r in + let l = Lsp.Types.Location.create + ~uri:uri ~range:(lsp_range_of_loc loc) + in + let ret = `Location [l] in + let f = Linol_lwt.return (Some ret) in + f - method! on_req_hover ~notify_back ~uri ~pos doc_state = match Hashtbl.find buffers uri with | state_after_processing -> let (log_list,ast) = state_after_processing in @@ -181,8 +194,14 @@ class lsp_server = let r = Lsp.Types.Hover.create ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) ~range:range () - in Some r + in + let e = Some r in + let f = Linol_lwt.return e in f + + method! config_definition = Some (`Bool true) + method! config_hover = Some (`Bool true) + end (* Main code View it on GitLab: https://gitlab.com/monnier/typer/-/compare/98f2b0c694d714cf1d57c2553f948bcd… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/98f2b0c694d714cf1d57c2553f948bcd… You're receiving this email because of your account on gitlab.com.

1 0

Locations en tant qu'intervalles de caractères
by Génier Simon 22 Apr '21

22 Apr '21

Bonjour, Soilihi, j’ai parlé à Stefan hier et il m’a dit que tu aimerais avoir mes patchs qui transforment les locations en intervalles pour le serveur LSP. Je ne suis pas en ville et elles sont sur mon desktop. Je serai de retour demain et je te les enverrais à ce moment. Je voulais quand même écrire ce courriel pour donner un petit résumé de ce que j’ai fait, parce que ces patchs sont très préliminaires. La première chose évidente est d’ajouter une ligne et une colonne de fin au type location. Par contre ça amène déjà une question : est-ce que ce point est inclusif ou exclusif? J’ai choisi qu’il soir exclusif parce que ça permet de représenter des intervalles vide sans ajouter de complexité. J’ai aussi l’impression que ça correspond à ce que LSP fait parce que ça modélise en fait un intervalle entre deux « curseur » comme on aurait dans un éditeur, mais c’est juste une intuition. Est-ce que c’est le cas? Je pense que le reste est assez laborieux, mais pas très difficile : il suffit de changer la définition de location et de réparer toutes les erreurs. Sauf dans les phases de préanalyse et d’analyse lexicale, où on crée les locations. Pour ça, j’ai une patch presque prête qui déplace le traitement des locations dans l’objet source. Ça élimine les redondances entre ces deux phases et ça nous permet de garder tout le code qui gère les points dans les fichiers dans le même module source. Si je me rappelle bien, elle est presque prête et je la soumettrai demain à cette liste pour la faire réviser. Bonne journée Simon

1 0

[Git][monnier/typer][soilih] 2 commits: empty
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 20 Apr '21

20 Apr '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: d076d86b by Soilih BEN SOILIH at 2021-04-17T09:09:25-06:00 empty - - - - - 98f2b0c6 by Soilih BEN SOILIH at 2021-04-20T14:16:53-06:00 hover and definition - - - - - 3 changed files: - samples/acc.typer - src/typer_lsp_server.ml - typer.ml Changes: ===================================== samples/acc.typer ===================================== @@ -20,4 +20,4 @@ map = lambda (a : Type) ≡> list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); % main = accumulate _+_ 0 list; -% main = map list (lambda x -> (x + 1)); \ No newline at end of file +% main = map list (lambda x -> (x + 1)); ===================================== src/typer_lsp_server.ml ===================================== @@ -55,6 +55,32 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = | Info -> Lsp.Types.DiagnosticSeverity.Information | _ -> Lsp.Types.DiagnosticSeverity.Hint +let typer_pos_of_lsp_pos (p:Lsp.Types.Position.t) : Util.location * Util.location = + let start_pos = {file=""; line= p.line; column= p.character; docstr=""} in + let end_pos = {file=""; line= p.line; column= p.character + 1; docstr=""} in + (start_pos, end_pos) + +let lsp_pos_of_pos_start (p:Util.location) : Lsp.Types.Position.t = + Lsp.Types.Position.create ~line:(p.line) ~character:(p.column) + +let lsp_pos_of_pos_end (p:Util.location) : Lsp.Types.Position.t = + Lsp.Types.Position.create ~line:(p.line) ~character:(p.column + 1) +let lsp_range_of_loc (l:Util.location) : Lsp.Types.Range.t = + Lsp.Types.Range.create ~start:(lsp_pos_of_pos_start l) ~end_:(lsp_pos_of_pos_end l) + +let vname_to_lsp_loc ~(vname: Util.vname) ~uri : Lsp.Types.Location.t = + let (location, _) = vname in + Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc location) + +let rec search_a_vname_with_a_given_position (vname_list: Util.vname list) (location : Util.location): Util.vname = + match vname_list with + | [] -> let loc = Util.dummy_location in + let s = Some "null" in + (loc,s) + | hd::tl -> let (loc, _) = hd in + if (loc.line == location.line) && (loc.column == location.column) then hd + else search_a_vname_with_a_given_position tl location + let readstring (str:string) = let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) @@ -101,7 +127,6 @@ class lsp_server = (* one env per document *) val buffers: (Lsp.Types.DocumentUri.t, state_after_processing) Hashtbl.t = Hashtbl.create 96 - (* We define here a helper method that will: - process a document - store the state resulting from the processing @@ -130,8 +155,35 @@ class lsp_server = method on_notif_doc_did_close ~notify_back:_ d : unit Linol_lwt.t = Hashtbl.remove buffers d.uri; Linol_lwt.return () + + method! on_req_definition ~notify_back ~uri ~pos _st = + match Hashtbl.find buffers uri with + + | state_after_processing -> let (log_list,ast) = state_after_processing in + let (list_list, ectx) = ast in + let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in + let pi = List.map (fun x -> let (a,b,c) = x in a ) tab in + let loc = List.map (fun x -> vname_to_lsp_loc ~vname:x ~uri:uri) pi in + let ret = `Location loc in + Some ret + + + method! on_req_hover ~notify_back ~uri ~pos doc_state = + match Hashtbl.find buffers uri with + | state_after_processing -> let (log_list,ast) = state_after_processing in + let (list_list, ectx) = ast in + let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in + let pi = List.map (fun x -> let (a,b,c) = x in a ) tab in + let (loc_start, loc_end) = typer_pos_of_lsp_pos pos in + let vn = search_a_vname_with_a_given_position pi loc_start in + let range = lsp_range_of_loc loc_start in + let s = Util.get_vname_name vn in + let r = Lsp.Types.Hover.create + ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) + ~range:range () + in Some r - end +end (* Main code This is the code that creates an instance of the lsp server class ===================================== typer.ml ===================================== @@ -56,7 +56,7 @@ let arg_defs = let main () = let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in - Arg.parse arg_defs add_input_file usage; + Arg.parse arg_defs add_input_file usage; if !lsp_server then Typer_lsp_server.run () else (); let files = List.rev !arg_files in @@ -68,7 +68,6 @@ let main () = print_string welcome_msg; print_string (Fmt.make_sep '-'); flush stdout); - let i, ectx, rctx = try let ectx = Elab.default_ectx in @@ -89,7 +88,7 @@ let main () = -> REPL.handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 in - + if is_interactive then REPL.repl i ectx rctx View it on GitLab: https://gitlab.com/monnier/typer/-/compare/620fabd9f5c0134410051c22262882c1… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/620fabd9f5c0134410051c22262882c1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 2 commits: return the AST with the logs
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 15 Apr '21

15 Apr '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 4bd05656 by Soilih BEN SOILIH at 2021-04-14T21:19:06-06:00 return the AST with the logs - - - - - 620fabd9 by Soilih BEN SOILIH at 2021-04-15T14:09:36-06:00 resolving the exception - - - - - 5 changed files: - btl/pervasive.typer - + src/configuration.json - src/dune - src/elab.ml - src/typer_lsp_server.ml Changes: ===================================== btl/pervasive.typer ===================================== @@ -570,7 +570,7 @@ define-operator "<-" 80 96; %% %% `List` is the type and `list` is the module %% -list = load "btl/list.typer"; +list = load "/home/soilih/Projet Maitrise/typer/btl/list.typer"; %% %% Macro `do` for easier series of IO operation @@ -578,13 +578,13 @@ list = load "btl/list.typer"; %% e.g.: %% do { IO_return true; }; %% -do = let lib = load "btl/do.typer" in lib.do; +do = let lib = load "/home/soilih/Projet Maitrise/typer/btl/do.typer" in lib.do; %% %% Module containing various macros for tuple %% Used by `case_` %% -tuple-lib = load "btl/tuple.typer"; +tuple-lib = load "/home/soilih/Projet Maitrise/typer/btl/tuple.typer"; %% %% Get the nth element of a tuple @@ -615,7 +615,7 @@ Tuple = tuple-lib.tuple-type; %% %% Macro `case` for a some more complex pattern matching %% -case_ = let lib = load "btl/case.typer" in lib.case-macro; +case_ = let lib = load "/home/soilih/Projet Maitrise/typer/btl/case.typer" in lib.case-macro; %% %% plain-let @@ -632,7 +632,7 @@ define-operator "plain-let" () 3; %% define-operator "in" 3 67; %% -plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; +plain-let_in_ = let lib = load "/home/soilih/Projet Maitrise/typer/btl/plain-let.typer" in lib.plain-let-macro; %% %% `case` at function level @@ -642,7 +642,7 @@ plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; %% | true => false %% | false => true; %% -_|_ = let lib = load "btl/polyfun.typer" in lib._|_; +_|_ = let lib = load "/home/soilih/Projet Maitrise/typer/btl/polyfun.typer" in lib._|_; %% %% case_as_return_, case_return_ @@ -651,7 +651,7 @@ _|_ = let lib = load "btl/polyfun.typer" in lib._|_; define-operator "as" 42 42; define-operator "return" 42 42; -depelim = load "btl/depelim.typer"; +depelim = load "/home/soilih/Projet Maitrise/typer/btl/depelim.typer"; case_as_return_ = depelim.case_as_return_; case_return_ = depelim.case_return_; ===================================== src/configuration.json ===================================== @@ -0,0 +1,4 @@ +{ + "path": "/home/soilih/Projet Maitrise/typer", + "description" : "this path is the path from where we run Typer to the typer folder. We must change it to make it work !!!" +} \ No newline at end of file ===================================== src/dune ===================================== @@ -3,6 +3,6 @@ (name typerlib) (libraries zarith str linol linol-lwt - lsp jsonrpc + lsp jsonrpc yojson )) ===================================== src/elab.ml ===================================== @@ -64,9 +64,19 @@ module EL = Elexp let dloc = dummy_location let parsing_internals = ref false + +(* +(* Read the JSON file *) +let json = Yojson.Basic.from_file "../../configuration.json" + +(* take the path + it's make an exception now !! +*) +let exec_path = json |> Yojson.Basic.Util.member "path" |> Yojson.Basic.Util.to_string;; +*) let btl_folder = try Sys.getenv "TYPER_BUILTINS" - with Not_found -> "./btl" + with Not_found -> (*exec_path*) "/home/soilih/Projet Maitrise/typer" ^ "/btl" let fatal = Log.log_fatal ~section:"ELAB" let error = Log.log_error ~section:"ELAB" ===================================== src/typer_lsp_server.ml ===================================== @@ -39,8 +39,9 @@ open Log open Util -type state_after_processing = log_entry list - +type state_after_processing = (log_entry list * + ((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) + ) let log_entry_to_list (tab:log_entry list) : ((string * int * int * string) * log_level * string) list = List.map (fun x -> let location = Option.get x.loc in ((location.file,location.line,location.column,location.docstr) @@ -57,14 +58,15 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = let readstring (str:string) = let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) - ignore (Elab.lexp_decl_str str ectx); - !Log.typer_log + let ast = Elab.lexp_decl_str str ectx in + (!Log.typer_log, ast) let process_some_input_file (_file_contents : string) : state_after_processing = readstring _file_contents let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = - let log_tab = log_entry_to_list _state in + let (log, _) = _state in + let log_tab = log_entry_to_list log in List.map (fun x -> let (loc, lev, msg) = x in let (_ (* file *), line, column, _ (* docstr *) ) = loc in View it on GitLab: https://gitlab.com/monnier/typer/-/compare/fad7704ffe489fc4c984b96e5bd6253e… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/fad7704ffe489fc4c984b96e5bd6253e… You're receiving this email because of your account on gitlab.com.

1 0

Démarrer Typer
by Soilih BEN SOILIH 14 Apr '21

14 Apr '21

Bonjour tout le monde, J'espère que vous allez bien ! J'ai une petite question. En fait, avant, pour démarrer Typer dans le terminal, j'avais juste à le démarrer depuis le dossier _build avec la commande "_build/typer". Depuis qu'on utilise dune, je le démarrais de la même manière mais avec ce qui est présent dans "_build/default/...". Mais depuis que j'ai rajouté la fonction run() de mon serveur dans l'exécutable, quand je démarre l'exécutable, c'est le serveur qui démarre dans le shell et pas Typer. Quelqu'un aurait une idée? (branche "soilih") Merci beaucoup !

2 1

Re: [Typer] Update
by Stefan Monnier 11 Apr '21

11 Apr '21

[ Je mets typer@iro en Cc paske ça peut les intéresser. ] > Toutefois, je pense qu'il va falloir prendre l'erreur suivante au sérieux : > > Error:(ELAB) Compilation stopped in default context > Fatal error: exception Sys_error("./btl/builtins.typer: No such file or > directory") Oui, il faut clairement fixer ce problème. Pour ça il faudra voir comment l'exécutable peut trouver le répertoire `btl`. Il y en gros deux cas: 1- le cas où l'exécutable est "installé". Ce cas est le plus facile, vu que dans ce cas, `btl` doit être dans le répertoire qui a été désigné comme le repertoire où Typer sera installé, donc on peut le "hard-code" dans l'exécutable. Par contre, pour l'instant ce mode "installé" n'existe pas. 2- le cas où l'exécutable n'est pas installé et à la place on l'utilise tel quel depuis `_build/typer`. Dans ce cas il va falloir deviner où est ce `_build/typer` à partir typiquement d'heuristiques basées sur $PATH, argv[0], et autres. -- Stefan

1 0

[Git][monnier/typer][soilih] 2 commits: fix declaration order
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 11 Apr '21

11 Apr '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: a1b864fd by Soilih BEN SOILIH at 2021-04-09T19:45:28-06:00 fix declaration order - - - - - fad7704f by Soilih BEN SOILIH at 2021-04-11T21:01:01-06:00 linol update - - - - - 2 changed files: - emacs/typer-mode.el - src/typer_lsp_server.ml Changes: ===================================== emacs/typer-mode.el ===================================== @@ -281,7 +281,6 @@ (defvar typer-lsp-server-command '("typer-lsp-server")) -(add-to-list 'lsp-language-id-configuration '(typer-mode . "typer")) (with-eval-after-load 'lsp-mode (lsp-register-client (make-lsp-client :new-connection @@ -289,7 +288,9 @@ (lambda () typer-lsp-server-command)) :major-modes '(typer-mode) :priority -1 - :server-id 'typer-ls))) + :server-id 'typer-ls)) + (add-to-list 'lsp-language-id-configuration '(typer-mode . "typer")) + ) (provide 'typer-mode) ===================================== src/typer_lsp_server.ml ===================================== @@ -58,29 +58,30 @@ let readstring (str:string) = let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) ignore (Elab.lexp_decl_str str ectx); - !Log.typer_log - + !Log.typer_log + let process_some_input_file (_file_contents : string) : state_after_processing = - readstring _file_contents - + readstring _file_contents + let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = -let log_tab = log_entry_to_list _state in -List.map (fun x -> - let (loc, lev, msg) = x in - let (_ (* file *), line, column, _ (* docstr *) ) = loc in - let severity = log_level_to_severity lev in - let message = msg in - let start_pos = Lsp.Types.Position.create ~line:line ~character:column in - let end_pos = Lsp.Types.Position.create ~line:line ~character:(column + 1) in - let range = Lsp.Types.Range.create ~start:start_pos ~end_:end_pos in - let diagnostic = Lsp.Types.Diagnostic.create () - ~range:range - ~severity:severity - ~source:"typerlsp" - ~message:message - in - diagnostic -) log_tab + let log_tab = log_entry_to_list _state in + List.map (fun x -> + let (loc, lev, msg) = x in + let (_ (* file *), line, column, _ (* docstr *) ) = loc in + let severity = log_level_to_severity lev in + let message = msg in + let start_pos = Lsp.Types.Position.create ~line:line ~character:column in + let end_pos = Lsp.Types.Position.create ~line:line ~character:(column + 1) in + let range = Lsp.Types.Range.create ~start:start_pos ~end_:end_pos in + let diagnostic = Lsp.Types.Diagnostic.create () + ~range:range + ~severity:severity + ~source:"typerlsp" + ~message:message + in + diagnostic + ) log_tab + (* Lsp server class This is the main point of interaction beetween the code checking documents @@ -114,7 +115,7 @@ class lsp_server = (* We now override the [on_notify_doc_did_open] method that will be called by the server each time a new document is opened. *) - method on_notif_doc_did_open ~notify_back d ~content : unit Linol_lwt.Task.m = + method on_notif_doc_did_open ~notify_back d ~content : unit Linol_lwt.t = self#_on_doc ~notify_back d.uri content (* Similarly, we also override the [on_notify_doc_did_change] method that will be called @@ -124,33 +125,22 @@ class lsp_server = (* On document closes, we remove the state associated to the file from the global hashtable state, to avoid leaking memory. *) - method on_notif_doc_did_close ~notify_back:_ d : unit Linol_lwt.Task.m = + method on_notif_doc_did_close ~notify_back:_ d : unit Linol_lwt.t = Hashtbl.remove buffers d.uri; - Linol_lwt.Jsonrpc2.IO.return () + Linol_lwt.return () + end (* Main code This is the code that creates an instance of the lsp server class and runs it as a task. *) let run () = - let open Linol_lwt.Task.Infix in let s = new lsp_server in - (* TODO: the task is the LSP server *) - let task = - Linol_lwt.Task.start ~descr:"top task" - (fun _top_task -> - let server = Linol_lwt.Jsonrpc2.create_stdio s in - let* () = - Linol_lwt.Task.run_sub ~descr:"lsp server" ~parent:_top_task - (fun _ -> Linol_lwt.Jsonrpc2.run server _top_task) - >>= Linol_lwt.Task.unwrap - in - Linol_lwt.Task.return () - ) - in - match Linol_lwt.Task.run task with - | Ok () -> () - | Error e -> + let server = Linol_lwt.Jsonrpc2.create_stdio s in + let task = Linol_lwt.Jsonrpc2.run server in + match Linol_lwt.run task with + | () -> () + | exception e -> let e = Printexc.to_string e in Printf.eprintf "error: %s\n%!" e; exit 1 \ No newline at end of file View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6452296605b9317a616cca10b24c7c15… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6452296605b9317a616cca10b24c7c15… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] emacs file
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 09 Apr '21

09 Apr '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 64522966 by Soilih BEN SOILIH at 2021-04-09T14:17:59-06:00 emacs file - - - - - 1 changed file: - emacs/typer-mode.el Changes: ===================================== emacs/typer-mode.el ===================================== @@ -281,7 +281,7 @@ (defvar typer-lsp-server-command '("typer-lsp-server")) - +(add-to-list 'lsp-language-id-configuration '(typer-mode . "typer")) (with-eval-after-load 'lsp-mode (lsp-register-client (make-lsp-client :new-connection View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6452296605b9317a616cca10b24c7c157… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6452296605b9317a616cca10b24c7c157… You're receiving this email because of your account on gitlab.com.

2 1