Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer

Commits: 5d4fb8bb by Soilih at 2022-03-27T23:18:29-04:00 -

- - - - - ae98da77 by Soilih at 2022-06-05T00:46:33-04:00 -

- - - - - 81c1ca9e by Soilih at 2022-06-05T00:50:07-04:00 -

- - - - - 032fc62f by Soilih at 2022-06-06T14:34:04-04:00 -

- - - - - 602b8227 by Soilih at 2022-06-06T16:19:42-04:00 -

- - - - - 32f64163 by Soilih at 2022-06-07T22:53:01-04:00 -

- - - - - 3a337c6f by Soilih at 2022-06-08T00:30:51-04:00 -

- - - - - f9226a12 by Soilih at 2022-06-08T01:59:54-04:00 -

- - - - - 31eb4679 by Soilih at 2022-06-09T01:22:35-04:00 -

- - - - - a8cf270f by Soilih at 2022-06-09T22:46:52-04:00 fixing hover, completion, path and the argument to start the server

- - - - - 7deace8b by Soilih at 2022-06-10T00:05:36-04:00 fixing merge conflicts

- - - - -

14 changed files:

- emacs/typer-mode.el - src/elab.ml - src/gambit.ml - src/listx.ml → src/list.ml - src/log.ml - src/lsp_server_test.ml - src/prelexer.ml - src/source.ml - src/typer_lsp_server.ml - tests/dune - tests/lexer_test.ml - + tests/prelexer_test.ml - tests/utest_lib.ml - typer.ml

Changes:

===================================== emacs/typer-mode.el ===================================== @@ -279,7 +279,7 @@ (easy-menu-add typer-mode-menu) )

- (defvar typer-lsp-server-command '("typer-lsp-server")) + (defvar typer-lsp-server-command '("typer" "--lsp")) (with-eval-after-load 'lsp-mode (lsp-register-client (make-lsp-client :new-connection

===================================== src/elab.ml ===================================== @@ -70,18 +70,15 @@ let elab_check = ref false let dloc = dummy_location

let parsing_internals = ref false -let btl_folder = - (* - let cwd = Sys.getcwd () in - let cdir = String.sub cwd 0 (String.length cwd) in - let canal_entree = open_in (cdir ^ "/.configuration.txt") in - let ligne1 = input_line canal_entree in - let l = String.split_on_char ':' ligne1 in - let m = String.split_on_char '"' (List.nth l 1) in - let filename = List.nth m 1 in*) - +let btl_folder = try Sys.getenv "TYPER_BUILTINS" - with Not_found -> "/home/soilih/Projet Maitrise/typer" (*filename*) ^ "/btl" + with Not_found -> let str_ref = ref "" in + let strl = String.split_on_char '/' Sys.executable_name in + for i = 1 to (List.length strl) -2 do + str_ref := !str_ref ^ "/" ^ (List.nth strl i) + done; + !str_ref ^ "/btl" +

let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt @@ -1843,10 +1840,16 @@ let sform_load usr_elctx loc sargs _ot =

(* read file as elab_context *) let ld_elctx = match sargs with - | [String (_,file_name)] -> if !in_pervasive then - read_file file_name usr_elctx + + | [String (_,file_name)] -> if !in_pervasive then ( + if (Filename.is_relative file_name) then + (read_file btl_folder usr_elctx) + else (read_file file_name usr_elctx) + ) else - read_file file_name !sform_default_ectx + if (Filename.is_relative file_name) then + (read_file btl_folder !sform_default_ectx) + else (read_file file_name !sform_default_ectx) | _ -> (error ~loc "argument to load should be one file name (String)"; !sform_default_ectx) in

===================================== src/gambit.ml ===================================== @@ -116,7 +116,7 @@ module Scm = struct 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 + | List ls, List rs -> List.equal equal ls rs | Integer l, Integer r -> Z.equal l r | Float l, Float r -> Float.equal l r | _ -> false

===================================== src/listx.ml → src/list.ml ===================================== @@ -1,4 +1,4 @@ -(* Copyright (C) 2021 Free Software Foundation, Inc. +(* Copyright (C) 2021-2022 Free Software Foundation, Inc. * * Author: Simon Génier simon.genier@umontreal.ca * Keywords: languages, lisp, dependent types. @@ -18,6 +18,8 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see http://www.gnu.org/licenses/. *)

+ include Stdlib.List + (* Backport from 4.12. *) let rec equal (p : 'a -> 'a -> bool) (ls : 'a list) (rs : 'a list) : bool = match ls, rs with

===================================== src/log.ml ===================================== @@ -252,7 +252,7 @@ let stop_on_error () = let count = error_count () in if 0 < count then ( - if !lsp_enabled then + if (not !lsp_enabled) then stop_compilation "Compiler stopped after: %d errors\n" count else () ) @@ -262,7 +262,7 @@ let stop_on_warning () = let count = warning_count () in if 0 < count then ( - if !lsp_enabled then + if (not !lsp_enabled) then stop_compilation "Compiler stopped after: %d warnings\n" count else () )

===================================== src/lsp_server_test.ml ===================================== @@ -38,6 +38,10 @@ let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in output_string oc content; close_out oc

+let test_hover_rapide () = + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let name = "/home/soilih/Bureau/test/test.txt" in + hoverTest ctx name "multiply x y = x * y ;\nm = multiply 2 3;" (2,1) "##Int"

let test_hover () = let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in

===================================== src/prelexer.ml ===================================== @@ -1,6 +1,6 @@ (* prelexer.ml --- First half of lexical analysis of Typer.

-Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2022 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -40,7 +40,7 @@ module Pretoken = struct | 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 + -> List.equal equal l_inner r_inner | _ -> false end

===================================== src/source.ml ===================================== @@ -162,7 +162,7 @@ end let read_buffer_length = 4096

class source_file file_name = object (self) - inherit t first_line_of_file first_column_of_line file_name + inherit t (first_line_of_file - 1) first_column_of_line file_name

val in_channel = open_in file_name val mutable end_of_line = false

===================================== src/typer_lsp_server.ml ===================================== @@ -46,21 +46,6 @@ type syntax_tree_elab_ctx = (syntax_tree * Debruijn.elab_context) type document_state = (log_entry list * (syntax_tree_elab_ctx option) * ((int * int) option ref))

- -(* -let last_pos = ref [(0,0)] - -let add_to_tab tab a = - if((List.length !tab) > 4) then - let l = List.tl(List.rev !tab) in - tab := a::(List.rev l) - else - tab := a::(!tab) - -let get_pos_tab tab = - List.hd !tab -*) - let lsp_pos_of_a_tuple (a,b) : Lsp.Types.Position.t = Lsp.Types.Position.create ~line:(a) ~character:(b)

@@ -303,10 +288,34 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De match tab with | [] -> failwith "Liste vide!" | [n] -> n - | [hd;tl] -> let (_, _, _, _, loc_hd, _) = hd in - let (_, _, _, _, loc_tl, _) = tl in - if (dist loc_hd cursor < dist loc_tl cursor ) then hd - else tl + | [hd;tl] -> let (_, _, lhd, _, loc_hd, _) = hd in + let (_, _, ltl, _, loc_tl, _) = tl in + let open Source.Location in + if ((Int.equal loc_hd.start_line cursor.start_line) + && (Int.equal loc_tl.start_line cursor.start_line)) + then ( + if (dist loc_hd cursor < dist loc_tl cursor ) then hd + else tl + ) + else ( + if ((Int.equal loc_hd.start_line cursor.start_line) + && (not (Int.equal loc_tl.start_line cursor.start_line))) + then ( + hd + ) + else( + if ((not (Int.equal loc_hd.start_line cursor.start_line)) + && (Int.equal loc_tl.start_line cursor.start_line)) + then ( + tl + ) + else ( + if (dist loc_hd cursor < dist loc_tl cursor ) then hd + else tl + ) + ) + ) + |hd::ml::tl -> let (_, _, _, _, loc_hd, _) = hd in let (_, _, _, _, loc_ml, _) = ml in if (dist loc_hd cursor < dist loc_ml cursor ) then (foo (hd::tl) cursor) @@ -595,6 +604,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De browse_lexp ctx e cursor lst_in | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, None, location, lst_in))

+ (*====================================Lexp parcourir===================================*)

(*=================================Meilleure impression==================================*) @@ -607,7 +617,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De | Mnil -> rlst | Mcons (((_, Lexp.LetDef (_, lxpv), _) as hd), tl, _, _ - ) -> if String.equal (Lexp.lexp_string lxp) (Lexp.lexp_string lxpv) then + ) -> if String.equal (Lexp.lexp_string_for_lsp lxp) (Lexp.lexp_string_for_lsp lxpv) then foo tl (comp + 1) ((hd,comp)::rlst) else foo tl (comp + 1) rlst | Mcons (_, tl, _, _) -> foo tl (comp + 1) rlst @@ -622,7 +632,7 @@ let use_search_name_in_ctx lctx lxp = match s with | None -> failwith "no name found !!!" | Some _-> let lx = Lexp.mkVar (vn,i) in - Lexp.lexp_string lx + Lexp.lexp_string_for_lsp lx

(*====================================Meilleure impression==================================*)

@@ -737,8 +747,7 @@ let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) = in List.filter (fun (x:Lsp.Types.CompletionItem.t) -> str_order str x.label - ) lst - + ) lst

(* List of separators that delimit a word *) @@ -763,8 +772,6 @@ let use_search_word (str:string) (char_list:char list) (pos:int) (ret:string) : | _ -> search_word_in_cursor str char_list (pos - 1) ret

- - (*====================================Completion helpers======================================*)

@@ -859,9 +866,6 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = ( let rec arg_loop args i ret_lst = match args with - (*| Inductive of U.location * label - * ((arg_kind * vname * ltype) list) (* formal Args *) - * ((arg_kind * vname * ltype) list) SMap.t *) | [] -> let lst = SMap.fold @@ -1209,17 +1213,17 @@ class lsp_server = end_line = typer_loc.start_line + 1 } in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - (* + let lexp = trans_list_in_list_to_let list_list in let (l_ctx,_,l_type,_,location,_) = browse_lexp ctx lexp typer_loc' [] in - *) + (* let (lctx,vx) = lexp_search ctx list_list typer_loc' in let ((lvn,_),lexp,ltyp) = vx in - + let (l_ctx_r,_,_,_,_,_) as ret = browse_lexp lctx lexp typer_loc' [] in let ret' = (l_ctx_r,None,ltyp,None,lvn,[]) in let (l_ctx,_,l_type,_,location,_) = browse_list_lexp [ret;ret'] typer_loc in - + *) let range = lsp_range_of_loc location in let range' = Lsp.Types.Range.{ start = { range.start with line = range.start.line - 1 } ; @@ -1244,9 +1248,9 @@ class lsp_server = let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in - let ((lvn,_),lexp,ltyp) = vx in - (*let lexp = trans_list_in_list_to_let list_list in*) + (*let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let ((lvn,_),lexp,ltyp) = vx in*) + let lexp = trans_list_in_list_to_let list_list in

(* let trans_string = Compl.tranform_string doc_state.content in @@ -1254,7 +1258,7 @@ class lsp_server = let word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in *)

- match browse_lexp lctx lexp typer_loc [] with + match browse_lexp ctx lexp typer_loc [] with

| (l_ctx,_,_, None,_,_) -> @@ -1383,11 +1387,12 @@ class lsp_server =

end

+ (* Main code This is the code that creates an instance of the lsp server class and runs it as a task. *) let run () = - ignore (Arg.Set Log.lsp_enabled); + ignore (Log.lsp_enabled := true); let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in

===================================== tests/dune ===================================== @@ -10,9 +10,10 @@ lexer_test macro_test positivity_test + prelexer_test sexp_test unify_test) (deps (alias %{project_root}/btl/typer_stdlib)) - (libraries typerlib) + (libraries typerlib unix) (action (chdir %{project_root} (run %{test}))))

===================================== tests/lexer_test.ml ===================================== @@ -1,4 +1,4 @@ -(* Copyright (C) 2021 Free Software Foundation, Inc. +(* Copyright (C) 2021-2022 Free Software Foundation, Inc. * * Author: Simon Génier simon.genier@umontreal.ca * Keywords: languages, lisp, dependent types. @@ -33,7 +33,7 @@ let test_lex name pretokens expected = | Sexp.Block (actual_location, actual_pretokens), Sexp.Block (expected_location, expected_pretokens) -> Location.equal actual_location expected_location - && Listx.equal Pretoken.equal actual_pretokens expected_pretokens + && List.equal Pretoken.equal actual_pretokens expected_pretokens | Sexp.Symbol (actual_location, actual_name), Sexp.Symbol (expected_location, expected_name) -> Location.equal actual_location expected_location @@ -41,18 +41,18 @@ let test_lex name pretokens expected = | 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 + && List.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 + if List.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 + List.equal Sexp.sexp_equal actual expected in let print_token token = Printf.printf "%s\n" (sexp_string ~print_locations token)

===================================== tests/prelexer_test.ml ===================================== @@ -0,0 +1,103 @@ +(* Copyright (C) 2022 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 Printf + + module AssertPretokenEq : AssertEq with type t = pretoken = struct + type t = pretoken + + let name = "pretoken" + + let rec to_string = function + | Pretoken (location, name) -> + sprintf "|%s|@%s" name (Source.Location.to_string location) + | Prestring (location, text) -> + sprintf {|"%s"@%s|} text (Source.Location.to_string location) + | Preblock (location, pretokens) -> + sprintf + {|{%s}@%s|} + (pretokens |> List.map to_string |> String.concat ", ") + (Source.Location.to_string location) + + let assert_equal ~expected ~actual = + match expected, actual with + | Pretoken (el, et), Pretoken (al, at) + | Prestring (el, et), Prestring (al, at) + when Source.Location.equal el al && et = at -> + () + + | _ -> + assert_failure + "Expected: %s%s%s\nActual: %s%s%s" + Fmt.red + (to_string expected) + Fmt.reset + Fmt.red + (to_string actual) + Fmt.reset + end + + module AssertPretokenListEq = AssertListEq(AssertPretokenEq) + + let test_prelex name source_text expected = + let test () = + let source_name, source_channel = Filename.open_temp_file name ".typer" in + let expected = expected source_name in + let actual = + Fun.protect + ~finally:(fun () -> Unix.unlink source_name) + (fun () -> + Fun.protect + ~finally:(fun () -> close_out source_channel) + (fun () -> output_string source_channel source_text); + + let source = new Source.source_file source_name in + Prelexer.prelex source) + in + + match AssertPretokenListEq.assert_equal ~actual ~expected with + | () -> success + | exception Assert_failure (message) -> + print_string message; + failure + in + add_test "PRELEXER" name test + + let l : Source.Location.t = + { + file = "test.typer"; + start_line = 1; + start_column = 1; + end_line = 1; + end_column = 1; + } + + let () = + test_prelex + "single token" + "asdf" + (fun source_name -> + [Pretoken ({l with file = source_name; start_column = 0; end_column = 4}, "asdf")]) + + let () = run_all () + \ No newline at end of file

===================================== tests/utest_lib.ml ===================================== @@ -34,6 +34,7 @@ open Typerlib

open Fmt open Util +open Printf

type test_fun = unit -> int type section = test_fun SMap.t * string list @@ -182,6 +183,81 @@ let expect_equal_decls = in _expect_equal_t decl_list_eq string_of_decl_list

+exception Assert_failure of string + +let assert_failure fmt = + ksprintf (fun message -> raise (Assert_failure message)) fmt + +module type AssertEq = sig + type t + + val name : string + + val to_string : t -> string + + val assert_equal : expected : t -> actual : t -> unit +end + +type 't elt_status = + | Ok of 't + | Fail of string + +module AssertListEq (Ae : AssertEq) : AssertEq with type t = Ae.t list = struct + type t = Ae.t list + + let name = "list of " ^ Ae.name + + let to_string ts = + ts + |> List.map Ae.to_string + |> String.concat "\n" + + let string_of_status = function + | Ok t -> sprintf "%s%s%s\n" Fmt.green (Ae.to_string t) Fmt.reset + | Fail message -> message + + let string_of_statuses statuses = + statuses + |> List.rev_map string_of_status + |> String.concat "\n" + + let assert_equal ~(expected : t) ~(actual : t) : unit = + let rec loop failed statuses expected actual = + match expected, actual with + | e :: ee, a :: aa -> + begin match Ae.assert_equal ~expected:e ~actual:a with + | () -> loop failed (Ok e :: statuses) ee aa + | exception Assert_failure message -> + loop true (Fail message :: statuses) ee aa + end + + | _ :: _, [] -> + assert_failure + "%sMissing %s:\n%s%s%s\n" + (string_of_statuses statuses) + Ae.name + Fmt.red + (to_string expected) + Fmt.reset + + | [], _ :: _ -> + assert_failure + "%sMissing %s:\n%s%s%s\n" + (string_of_statuses statuses) + Ae.name + Fmt.red + (to_string actual) + Fmt.reset + + | [], [] -> + if failed + then assert_failure "%s" (string_of_statuses statuses) + + in + loop false [] expected actual +end + + (* USAGE * * (add_test "LET" "Base Case" (fun () ->

===================================== typer.ml ===================================== @@ -25,7 +25,7 @@ open Debruijn

open Printf

-let arg_batch = ref false +let arg_batch = ref true

(* boolean used to start the LSP server. @@ -57,10 +57,8 @@ let arg_defs = let compile_main argv = let usage = Sys.executable_name ^ " compile [options] <file> …" in Arg.parse_argv argv arg_defs add_input_file usage; - let ectx = Elab.default_ectx in let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in - let _ = List.fold_left (Elab.process_file backend) ectx (list_input_files ()) in @@ -69,7 +67,6 @@ let compile_main argv = let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in Arg.parse_argv argv arg_defs add_input_file usage; - print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; print_newline (); @@ -102,7 +99,7 @@ let run_main argv =

let main () = if !lsp_server then Typer_lsp_server.run () - else + else (); let command, argv = if Array.length Sys.argv <= 1 then "repl", [||]

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/8ca46ab957849c09c5f4a099bfe2b5f97...