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

Révision de la branche `type-macro-improvements`
by Jean-Alexandre Barszcz 31 Mai '21

31 Mai '21

Bonjour, J'apprécierais votre feedback avant de merger une nouvelle petite branche: https://gitlab.com/monnier/typer/-/compare/master...type-macro-improvements J'ai ajouté un peu de flexibilité à la macro `type` pour pouvoir: 1. Avoir des paramètres de type implicites. 2. Définir des types à d'autres TypeLevels que 0. 3. Garder les constructeurs dans le même ordre. Au passage, j'en profite pour corriger quelques petits détails avec Dune pour que ça fonctionne sur ma machine, en espérant que ça ne brise rien de votre côté. Merci, Jean-Alexandre

1 0

[Git][monnier/typer][type-macro-improvements] 3 commits: Fix nix shell and dune details
by Jean-Alexandre Barszcz (＠jabarszcz) 31 Mai '21

31 Mai '21

Jean-Alexandre Barszcz pushed to branch type-macro-improvements at Stefan / Typer Commits: 8e1be507 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 Fix nix shell and dune details - - - - - dc07e915 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 * btl/pervasive.typer (type-impl): Accept implicit type params. Also, allow type definitions at other type levels than 0, with an annotation. - - - - - b8d1df5b by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 * btl/pervasive.typer (type-impl): Keep the constructors in order. - - - - - 5 changed files: - GNUmakefile - README.md - btl/pervasive.typer - shell.nix - tests/elab_test.ml Changes: ===================================== GNUmakefile ===================================== @@ -9,7 +9,7 @@ DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG)) DUNE_PROFILE = dev # DUNE_PROFILE = release -# Set COMPILE_MODE to native to build ocaml code with ocamlopt. +# Set COMPILE_MODE to `exe` for native builds. COMPILE_MODE ?= bc # DEBUG ?= 1 @@ -28,7 +28,7 @@ debug: debug_util.$(COMPILE_MODE) # interactive typer typer.$(COMPILE_MODE): - $(DUNE) --profile $(DUNE_PROFILE) build ./typer.$(COMPILE_MODE) + $(DUNE) build ./typer.$(COMPILE_MODE) --profile $(DUNE_PROFILE) debug_util.$(COMPILE_MODE): $(DUNE) build ./debug_util.$(COMPILE_MODE) @@ -37,7 +37,7 @@ debug_util.$(COMPILE_MODE): # be confusing if you don't know Dune, so we pass the --force flag to rerun all # the tests no matter what. tests: - $(DUNE) --force test + $(DUNE) test --force # There is nothing here. I use this to test if opam integration works install: tests ===================================== README.md ===================================== @@ -17,7 +17,7 @@ Status [![Build Status](https://travis-ci.org/Delaunay/typer.svg?branch=master)] By default, Dune creates a '_build' folder which holds all the compiled files. * `make typer`: build Typer interpreter (`./typer_cli.bc`). -* `COMPILE_MODE=native make typer`: build Typer interpreter (`./typer_cli.exe`). +* `COMPILE_MODE=exe make typer`: build Typer interpreter (`./typer_cli.exe`). * `make debug`: build typer with debug info (`./debug_util.bc`). * `make tests`: run interpreter's tests. ===================================== btl/pervasive.typer ===================================== @@ -308,17 +308,34 @@ type-impl = lambda (x : List Sexp) -> (lambda _ -> (nil : List Sexp)) % Float (lambda _ -> (nil : List Sexp)); % List of Sexp - get-type : Sexp -> Sexp; - get-type sxp = - Sexp_dispatch sxp - (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) - | true => List_nth 1 ss Sexp_error - | false => sxp) - (lambda _ -> sxp) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error); + %% Takes an arrow type and a parameter (possibly named using + %% `:`/`::`/`:::`), and prepends the corresponding arrow + %% (`->`/`=>`/`≡>`) to the arrow type given as argument. + add-arg-arrow : Sexp -> Sexp -> Sexp; + add-arg-arrow arrow-type arg = + let default_arr = + Sexp_node (Sexp_symbol "_->_") (cons arg (cons arrow-type nil)) in + Sexp_dispatch arg + (lambda s ss -> + let single-colon-arg = + (Sexp_node (Sexp_symbol "_:_") + (cons (List_head Sexp_error ss) + (cons (List_nth 1 ss Sexp_error) nil))); + arrow-args = (cons single-colon-arg (cons arrow-type nil)) in + case (Sexp_eq s (Sexp_symbol "_:_")) + | true => Sexp_node (Sexp_symbol "_->_") arrow-args + | false => + (case (Sexp_eq s (Sexp_symbol "_::_")) + | true => Sexp_node (Sexp_symbol "_=>_") arrow-args + | false => + (case (Sexp_eq s (Sexp_symbol "_:::_")) + | true => Sexp_node (Sexp_symbol "_≡>_") arrow-args + | false => default_arr))) + (lambda _ -> default_arr) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error); get-head = List_head Sexp_error; @@ -328,24 +345,30 @@ type-impl = lambda (x : List Sexp) -> %% Expression is Sexp_node (Sexp_symbol "|") (list) %% we only care about the list bit lst = get-list expr; - - %% head is (Sexp_node type-name (arg list)) - name = get-head lst; ctor = List_tail lst; - type-name = get-name name; + %% head+ is (Sexp_node type-name (arg list)), optionally wrapped + %% with a type annotation (<head> : Type_ l) + head+ = get-head lst; + + %% head-pair is a 2-list, which adds a default type annotation to head+ + head-pair = case Sexp_eq (get-name head+) (Sexp_symbol "_:_") + | true => get-list head+ + | false => cons head+ (cons (Sexp_symbol "Type") nil); + + head = List_nth 0 head-pair Sexp_error; + type-type = List_nth 1 head-pair Sexp_error; + type-name = get-name head; + type-args = get-list head; %% Create the inductive type definition. inductive = Sexp_node (Sexp_symbol "typecons") - (cons name ctor); + (cons head ctor); %% Declare the inductive type as a function %% Useful for recursive type - type-decl = quote ((uquote (get-name name)) : (uquote ( - (List_foldl (lambda args arg -> - Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil))) - %% FIXME: Don't hardcode TypeLevel.z! - (Sexp_symbol "Type") (List_reverse (get-args name) nil)) + type-decl = quote ((uquote type-name) : (uquote ( + (List_foldl add-arg-arrow type-type (List_reverse type-args nil)) ))); decl = make-decl type-name inductive; @@ -354,9 +377,8 @@ type-impl = lambda (x : List Sexp) -> ctors = let for-each : List Sexp -> Sexp -> Sexp; for-each ctr acc = case ctr | cons hd tl => - let acc2 = chain-decl (make-cons (get-name hd) - type-name) - acc + let acc2 = chain-decl acc (make-cons (get-name hd) + type-name) in for-each tl acc2 | nil => acc in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil) ===================================== shell.nix ===================================== @@ -3,7 +3,7 @@ pkgs.mkShell { name = "typer"; buildInputs = with pkgs.ocamlPackages; [ - pkgs.gnumake ocaml ocamlbuild findlib utop # tooling + pkgs.gnumake ocaml dune_2 findlib utop # tooling zarith # ocaml libraries merlin # for emacs ]; ===================================== tests/elab_test.ml ===================================== @@ -217,4 +217,18 @@ test = (getProof (decideBoolEq : Decidable (Eq true true)) : Eq true true); |} +let _ = add_elab_test_decl + "Implicit type parameters" + {| +type Not (ℓ ::: TypeLevel) (prop : Type_ ℓ) : Type_ ℓ + | mkNot ((contra : prop) -> False); + +type Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ) : Type_ ℓ + | yes (p ::: prop) + | no (p ::: Not prop); + +type Lift (l ::: TypeLevel) (t :: Type_ l) (x : t) + | mkLift; + |} + let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ca9be4c284292ace1c4289a3c31ef843… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ca9be4c284292ace1c4289a3c31ef843… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch type-macro-improvements
by Jean-Alexandre Barszcz (＠jabarszcz) 31 Mai '21

31 Mai '21

Jean-Alexandre Barszcz pushed new branch type-macro-improvements at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/type-macro-improvements You're receiving this email because of your account on gitlab.com.

1 0

Rencontres demain mardi après-midi
by Stefan Monnier 31 Mai '21

31 Mai '21

Bonjour, Je dois annuler nos rencontres de demain. Je peux vous proposer en remplacement demain matin entre 10h et 12h, ou mercredi entre 9h et 14h. Laisser-moi savoir ce qui vous convient, Désolé, Stefan

1 0

Patch fraiche (Lexer)
by Simon Génier 29 Mai '21

29 Mai '21

Bonjour, Voici le nouvel opus de ma saga pour pour ajouter un point final à location. https://gitlab.com/monnier/typer/-/compare/master...lexer-with-source Stefan a suggéré garder le whitespace dans les Pretokens pour réduire le nombre de pretokens et déplacer le code qui gère les espaces dans Lexer. Je pense que c'est une bonne idée et j'ai l'intention de le faire, mais je suggère de le faire dans un deuxième temps une fois cette série de patch mergée. Simon

1 0

[Git][monnier/typer] Pushed new branch lexer-with-source
by Simon Génier (＠ilovemonoids) 29 Mai '21

29 Mai '21

Simon Génier pushed new branch lexer-with-source at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/lexer-with-source You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch source-tells-its-own-location
by Simon Génier (＠ilovemonoids) 29 Mai '21

29 Mai '21

Simon Génier deleted branch source-tells-its-own-location at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 3 commits: Have the source tell its own location.
by Simon Génier (＠ilovemonoids) 28 Mai '21

28 Mai '21

Simon Génier pushed to branch master at Stefan / Typer Commits: b8959e2f by Simon Génier at 2021-05-12T21:36:47-04:00 Have the source tell its own location. Move the code that keeps track of the current line and column inside of the source object. Not only does this make sense conceptually since the source is a kind of cursor, but it will allow us to simplify the lexer code. - - - - - e7d3ed86 by Simon Génier at 2021-05-28T19:51:54-04:00 Merge branch 'source-tells-its-own-location' - - - - - c5ef2f59 by Simon Génier at 2021-05-28T20:30:37-04:00 Oops, fix tests on Windows. The prelexer considered \r to be part of presymbols with catastrophic results. - - - - - 3 changed files: - src/lexer.ml - src/prelexer.ml - src/source.ml Changes: ===================================== src/lexer.ml ===================================== @@ -27,6 +27,10 @@ open Grammar (*************** The Lexer phase *********************) +let inc_cp (cp : charpos) (c : char) = + (* Count char positions in utf-8: don't count the non-leading bytes. *) + if utf8_head_p c then cp+1 else cp + let digit_p char = let code = Char.code char in Char.code '0' <= code && code <= Char.code '9' ===================================== src/prelexer.ml ===================================== @@ -60,41 +60,36 @@ end (* FIXME: Add syntax for char constants (maybe 'c'). *) (* FIXME: Handle multiline strings. *) -let inc_cp (cp:charpos) (c:char) = - (* Count char positions in utf-8: don't count the non-leading bytes. *) - if utf8_head_p c then cp+1 else cp - let rec consume_until_newline (source : #Source.t) : unit = match source#next_char with | None | Some ('\n') -> () | Some _ -> consume_until_newline source -let rec prelex (source : #Source.t) ln ctx acc (doc : string) - : pretoken list = +(* Splits a Typer source into pretokens, stopping when it is completely + consumed. *) +let prelex (source : #Source.t) : pretoken list = + let rec loop + (ctx : (Source.Location.t * pretoken list) list) + (acc : pretoken list) + (doc : string) + : pretoken list = - let nextline = prelex source (ln + 1) in - let rec prelex' ctx (cpos:charpos) acc doc = - let nexttok = prelex' ctx in match source#peek_char with | None -> (match ctx with | [] -> List.rev acc - | ((ln, cpos, _) :: _ctx) -> - (prelexer_error {file=source#file_name; line=ln; column=cpos; docstr=""} - "Unmatched opening brace"; List.rev acc)) - - | Some ('\n') - -> source#advance; - nextline ctx acc doc + | ((location, _) :: _ctx) + -> prelexer_error location "Unmatched opening brace"; + List.rev acc) | Some (c) when c <= ' ' -> source#advance; - nexttok (cpos+1) acc doc + loop ctx acc doc (* A comment. *) | Some ('%') -> consume_until_newline source; - nextline ctx acc doc + loop ctx acc doc (* line's bounds seems ok: String.sub line 1 0 == "" *) | Some ('@') @@ -102,118 +97,91 @@ let rec prelex (source : #Source.t) ln ctx acc (doc : string) let start_offset = source#current_offset in consume_until_newline source; let new_doc = String.trim (source#slice_from_offset start_offset) in - nextline ctx acc (doc ^ "\n" ^ new_doc) + loop ctx acc (doc ^ "\n" ^ new_doc) (* A string. *) | Some ('"') -> source#advance; - let rec prestring cp chars = + let rec prestring chars = match source#next_char with | None | Some ('\n') - -> let location = - let open Source.Location in - {file=source#file_name; line=ln; column=cpos; docstr=doc} - in + -> let location = source#current_location doc in prelexer_error location "Unterminated string"; - nextline ctx (Prestring (location, "") :: acc) "" + loop ctx (Prestring (location, "") :: acc) "" | Some ('"') - -> let location = - let open Source.Location in - {file=source#file_name; line=ln; column=cpos; docstr=doc} - in + -> let location = source#current_location doc in let pretoken = Prestring (location, string_implode (List.rev chars)) in - nexttok (cp + 1) (pretoken :: acc) "" + loop ctx (pretoken :: acc) "" | Some ('\\') -> (match source#next_char with | None | Some ('\n') - -> let location = - let open Source.Location in - {file=source#file_name; line=ln; column=cp; docstr=doc} - in + -> let location = source#current_location doc in prelexer_error location "Unterminated escape sequence"; - nextline ctx (Prestring (location, "") :: acc) "" - | Some ('t') -> prestring (cp + 2) ('\t' :: chars) - | Some ('n') -> prestring (cp + 2) ('\n' :: chars) - | Some ('r') -> prestring (cp + 2) ('\r' :: chars) + loop ctx (Prestring (location, "") :: acc) "" + | Some ('t') -> prestring ('\t' :: chars) + | Some ('n') -> prestring ('\n' :: chars) + | Some ('r') -> prestring ('\r' :: chars) | Some ('u') - -> let location = - let open Source.Location in - {file=source#file_name; line=ln; column=cp; docstr=doc} - in + -> let location = source#current_location doc in prelexer_error location "Unimplemented unicode escape"; - prestring (cp + 2) chars - | Some (c) -> prestring (cp + 2) (c :: chars)) + prestring chars + | Some (c) -> prestring (c :: chars)) - | Some (char) -> prestring (inc_cp cp char) (char :: chars) - in prestring (cpos + 1) [] + | Some (char) -> prestring (char :: chars) + in prestring [] | Some ('{') -> source#advance; - prelex' ((ln, cpos, acc) :: ctx) (cpos + 1) [] doc + let ctx' = (source#current_location doc, acc) :: ctx in + loop ctx' [] doc | Some ('}') -> source#advance; + let location = source#current_location doc in (match ctx with - | ((sln, scpos, sacc) :: ctx) -> - prelex' ctx (cpos+1) - (Preblock ({file=source#file_name; line=sln; column=scpos; docstr=doc}, - List.rev acc, - {file=source#file_name; line=ln; column=(cpos + 1); docstr=doc}) - :: sacc) "" - | _ -> (prelexer_error {file=source#file_name; line=ln; column=cpos; docstr=doc} - "Unmatched closing brace"; - prelex' ctx (cpos + 1) acc doc)) + | ((slocation, sacc) :: ctx) + -> let preblock = Preblock (slocation, List.rev acc, location) in + loop ctx (preblock :: sacc) "" + | _ + -> prelexer_error location "Unmatched closing brace"; + loop ctx acc doc) (* A pretoken. *) - | Some (c) + | Some _ -> let start_offset = source#current_offset in source#advance; - let rec pretok cp = + let rec pretok () = match source#peek_char with - | None | Some (' ' | '\t' | '%' | '"' | '{' | '}') - -> let location = - let open Source.Location in - {file=source#file_name; line=ln; column=cpos; docstr=doc} - in + | None | Some ('%' | '"' | '{' | '}') + -> let location = source#current_location doc in let text = source#slice_from_offset start_offset in - nexttok cp (Pretoken (location, text) :: acc) "" + loop ctx (Pretoken (location, text) :: acc) "" - | Some ('\n') - -> let location = - let open Source.Location in - {file=source#file_name; line=ln; column=cpos; docstr=doc} - in + | Some (c) when c <= ' ' + -> let location = source#current_location doc in let text = source#slice_from_offset start_offset in source#advance; - nextline ctx (Pretoken (location, text) :: acc) "" + loop ctx (Pretoken (location, text) :: acc) "" | Some ('\\') -> source#advance; (match source#next_char with - | Some (char) -> pretok (1 + inc_cp cp char) + | Some _ -> pretok () | None - -> let location = - let open Source.Location in - {file=source#file_name; line=ln; column=cpos; docstr=doc} - in + -> let location = source#current_location doc in source#advance; let text = source#slice_from_offset start_offset in prelexer_error location ("Unterminated escape sequence in: " ^ text); - nexttok (cp + 1) (Pretoken (location, text) :: acc) "") + loop ctx (Pretoken (location, text) :: acc) "") - | Some (c) + | Some _ -> source#advance; - pretok (inc_cp cp c) - in pretok (inc_cp cpos c) + pretok () + in pretok () in - (* Traditionally, column numbers start at 1 :-( *) - prelex' ctx 1 acc doc - -let prelex (source : #Source.t) : pretoken list = - (* Traditionally, line numbers start at 1 :-( *) - prelex source 1 [] [] "" + loop [] [] "" let pretoken_name pretok = match pretok with ===================================== src/source.ml ===================================== @@ -35,17 +35,30 @@ module Location = struct && String.equal l_doc r_doc end +(* Traditionally, line numbers start at 1… *) +let first_line_of_file = 1 +(* … and so do column numbers :-( *) +let first_column_of_line = 1 + (* A source object is text paired with a cursor. The text can be lazily loaded as it is accessed byte by byte, but it must be retained for future reference by error messages. *) -class virtual t = object (self) +class virtual t (base_line : int) (base_column : int) (file_name : string) = +object (self) + val mutable line = base_line + val mutable column = base_column + (* A path if the text comes from a file, otherwise a meaningful identifier. *) - method virtual file_name : string + method file_name : string = file_name (* Return the byte at the cursor, or None if the cursor is at the end of the text. *) method virtual peek_char : char option + (* The current location of the cursor. *) + method current_location (docstr : string) : Location.t = + {file = file_name; line; column; docstr} + (* The current offset of the cursor in the file, in bytes. *) method virtual current_offset : int @@ -58,8 +71,21 @@ class virtual t = object (self) method virtual slice_from_offset : int -> string (* Moves the cursor forward one byte *) - method virtual advance : unit - + method advance : unit = + let is_utf8_head c = Char.code c < 128 || Char.code c >= 192 in + let c = self#peek_char in + self#advance_impl; + match c with + | Some '\n' + -> line <- line + 1; + column <- 0; + | Some c when is_utf8_head c + -> column <- column + 1 + | _ -> () + + method private virtual advance_impl : unit + + (* Returns the char at the cursor, then advances it forward. *) method next_char : char option = let c = self#peek_char in self#advance; @@ -69,45 +95,49 @@ end let read_buffer_length = 4096 class source_file file_name = object (self) - inherit t + inherit t first_line_of_file first_column_of_line file_name val in_channel = open_in file_name val mutable end_of_line = false - val mutable line = "" + val mutable source_line = "" val mutable line_offset = 0 val mutable offset = 0 method private peek_char_unchecked = - if offset < String.length line - then line.[offset] + if offset < String.length source_line + then source_line.[offset] else '\n' method peek_char = - if offset <= String.length line + if offset <= String.length source_line then Some self#peek_char_unchecked else try - line_offset <- line_offset + 1 + String.length line; - line <- input_line in_channel; + line_offset <- line_offset + 1 + String.length source_line; + source_line <- input_line in_channel; offset <- 0; Some self#peek_char_unchecked with | End_of_file -> None - method advance = + method advance_impl = offset <- offset + 1 method current_offset = line_offset + offset method slice_from_offset start_offset = let relative_start_offset = start_offset - line_offset in - String.sub line relative_start_offset (offset - relative_start_offset) - - method file_name = file_name + String.sub source_line relative_start_offset (offset - relative_start_offset) end -class source_string source = object - inherit t +class source_string + ?(base_line : int = first_line_of_file) + ?(base_column : int = first_column_of_line) + ?(file_name : string = "<string>") + source + = +object + inherit t base_line base_column file_name val mutable offset = 0 @@ -116,13 +146,11 @@ class source_string source = object then Some (source.[offset]) else None - method advance = + method advance_impl = offset <- offset + 1 method current_offset = offset method slice_from_offset start_offset = String.sub source start_offset (offset - start_offset) - - method file_name = "<string>" end View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f2d6d5dfe1ce4ef19e5ce1f694b49469… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f2d6d5dfe1ce4ef19e5ce1f694b49469… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] browse lexp update
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 26 Mai '21

26 Mai '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: a1a11af5 by Soilih BEN SOILIH at 2021-05-26T02:37:49-06:00 browse lexp update - - - - - 3 changed files: - + samples/.#acc.typer - src/log.ml - src/typer_lsp_server.ml Changes: ===================================== samples/.#acc.typer ===================================== @@ -0,0 +1 @@ +soilih@soilih-HP-Laptop-15-db0xxx.11163:1621953914 \ No newline at end of file ===================================== src/log.ml ===================================== @@ -193,6 +193,7 @@ let log_fatal ?section ?print_action ?loc m = internal_error "Compiler Fatal Error" + let log_error = log_msg Error ?kind:None let log_warning = log_msg Warning ?kind:None let log_info = log_msg Info ?kind:None ===================================== src/typer_lsp_server.ml ===================================== @@ -103,7 +103,6 @@ let rec search_lexp_with_a_location (lexp_list: Lexp.lexp list) (location : Sour let readstring (str:string) = Log.clear_log () ; - Arg.Set Log.lsp_enabled; let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) let ast = Elab.lexp_decl_str str ectx in @@ -309,12 +308,13 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list args) in let tct = arg_loop ctx Debruijn.set_empty args in (tct, location) - ) + ) + | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> ( - + let call_split (e: Lexp.lexp) = match Lexp.lexp_lexp' e with | Call (f, args) -> (f, args) @@ -353,8 +353,10 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in (erased, nctx) in - let foo = - (fun name (l, vdefs, branch) + let brch = SMap.bindings branches in + let lst = + List.map + (fun (name, (l, vdefs, branch)) -> let fieldtypes = SMap.find name constructors in let rec mkctx erased ctx s hlxp vdefs fieldtypes = match vdefs, fieldtypes with @@ -375,15 +377,16 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list mkctx erased ctx s hctor vdefs fieldtypes in let subst = Subst.shift (List.length vdefs) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in - browse_lexp ctx branch cursor; + ignore (browse_lexp ctx branch cursor); (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1))) + ) - in - let lst = foo (Lexp.get_name branches) branches in - let brch = SMap.bindings lst in + brch + in - let diff = SMap.cardinal constructors - SMap.cardinal brch in - (match default with + let diff = SMap.cardinal constructors - List.length lst in + ( + match default with | Some (v, d) -> if diff <= 0 then (); let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in @@ -392,12 +395,14 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let hlxp = Lexp.mkVar ((l, None), 0) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in - (Lexp.mkSusp ret (Subst.shift 2)) + browse_lexp ctx d cursor | None - -> if diff > 0 then () ) - | _,_ -> ())); + -> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy) + ) + | _,_ -> (Lexp.impossible, Source.Location.dummy) ); + (ret,location) - + ) @@ -442,6 +447,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let lctx = Debruijn.ectx_to_lctx ctx in let location = Lexp.lexp_location e in (Opslexp.get_type lctx e , location) + (*====================================Lexp parcourir===================================*) @@ -585,6 +591,7 @@ end 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); let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a1a11af523dcfe97f455c4ccc37362793… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a1a11af523dcfe97f455c4ccc37362793… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] resolve completion, diagnostics problems...case still not working*
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 20 Mai '21

20 Mai '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: a3ccd6b2 by Soilih BEN SOILIH at 2021-05-20T19:39:18-06:00 resolve completion, diagnostics problems...case still not working* - - - - - 4 changed files: - src/elab.ml - src/lexp.ml - src/log.ml - src/typer_lsp_server.ml Changes: ===================================== src/elab.ml ===================================== @@ -170,21 +170,6 @@ let elab_check_proper_type (ctx : elab_context) ltp var = -> " of var `" ^ name ^ "`")); raise e -let elab_check_proper_type_lsp (ctx : elab_context) ltp var = -try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp -with e -> match e with - | _ -> - info - ~print_action:(fun _ -> - print_lexp_ctx (ectx_to_lctx ctx); print_newline () - ) - ~loc:(lexp_location ltp) - ("Exception while checking type `" ^ (lexp_string ltp) ^ "`" - ^ (match var with - | (_, None) -> "" - | (_, Some name) - -> " of var `" ^ name ^ "`")); - raise e let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in @@ -212,6 +197,8 @@ let elab_check_def (ctx : elab_context) var lxp ltype = then elab_check_proper_type ctx ltype var else + ( + if !Log.lsp_enabled then fatal ~print_action:(fun _ -> List.iter print_indent_line [ @@ -222,43 +209,8 @@ let elab_check_def (ctx : elab_context) var lxp ltype = ]) ~loc "Type check error: ¡¡ctx_define error!!" - -let elab_check_def_lsp (ctx : elab_context) var lxp ltype = - let lctx = ectx_to_lctx ctx in - let loc = lexp_location lxp in - - let ltype' = try OL.check lctx lxp - with e -> match e with - | _ -> - info - ~print_action:(fun _ -> - lexp_print_details lxp (); - print_lexp_ctx (ectx_to_lctx ctx); - print_newline () - ) - ~loc - "Error while type-checking"; - raise e in - if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' - with e -> - info ~print_action:(lexp_print_details lxp) - ~loc - ("Exception while conversion-checking types: " - ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); - raise e) - then - elab_check_proper_type ctx ltype var - else - fatal - ~print_action:(fun _ -> - List.iter print_indent_line [ - (match var with (_, Some n) -> n | _ -> "<anon>") - ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; - " because"; - lexp_string ltype' ^ " != " ^ lexp_string ltype - ]) - ~loc - "Type check error: ¡¡ctx_define error!!" + else () + ) let ctx_extend (ctx: elab_context) (var : vname) def ltype = elab_check_proper_type ctx ltype var; @@ -268,10 +220,6 @@ let ctx_define (ctx: elab_context) var lxp ltype = elab_check_def ctx var lxp ltype; ectx_extend ctx var (LetDef (0, lxp)) ltype -let ctx_define_lsp (ctx: elab_context) var lxp ltype = - elab_check_def_lsp ctx var lxp ltype; - ectx_extend ctx var (LetDef (0, lxp)) ltype - let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in let _ = List.fold_left (fun n (var, _lxp, ltp) @@ -1277,8 +1225,6 @@ and infer_and_generalize_def (ctx : elab_context) se = t in (e', t') -(*====================premier=========================*) - and lexp_decls_1 (sdecls : sexp list) (* What's already parsed *) (tokens : token list) (* Rest of input *) @@ -1418,151 +1364,6 @@ and lexp_decls_1 pending_decls pending_defs in (Log.stop_on_error (); res)) -(*====================premier=========================*) - -(*====================second=========================*) - -and lexp_decls_1_lsp -(sdecls : sexp list) (* What's already parsed *) -(tokens : token list) (* Rest of input *) -(ectx : elab_context) (* External ctx. *) -(nctx : elab_context) (* New context. *) -(pending_decls : Source.Location.t SMap.t) (* Pending type decls. *) -(pending_defs : (symbol * sexp) list) (* Pending definitions. *) -: (vname * lexp * ltype) list * sexp list * token list * elab_context = - - let rec lexp_decls_1_lsp sdecls tokens nctx pending_decls pending_defs = - let sdecl, sdecls, toks = - match (sdecls, tokens) with - | (s :: sdecls, _) -> Some s, sdecls, tokens - | ([], []) -> None, [], [] - | ([], _) -> - let (s, toks) = sexp_parse_all (ectx_get_grammar nctx) - tokens (Some ";") in - Some s, [], toks in - let recur prepend_sdecls nctx pending_decls pending_defs = - lexp_decls_1_lsp (List.append prepend_sdecls sdecls) - toks nctx pending_decls pending_defs in - match sdecl with - | None -> (if not (SMap.is_empty pending_decls) then - let (s, loc) = SMap.choose pending_decls in - error ~loc ("Variable `" ^ s ^ "` declared but not defined!") - else - assert (pending_defs == [])); - [], [], [], nctx - - | Some (Symbol (_, "")) - -> recur [] nctx pending_decls pending_defs - - | Some (Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls')) - -> recur sdecls' nctx pending_decls pending_defs - - | Some (Node (Symbol (loc, "_:_"), args) as thesexp) - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in - if SMap.mem vname pending_decls then - (* Don't burp: take'em all and unify! *) - let pt_idx = senv_lookup vname nctx in - (* Take the previous type annotation. *) - let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with - | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) - | _ -> Log.internal_error "Var not found at its index!" in - (* Unify it with the new one. *) - let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with - | (_::_) - -> lexp_error loc ltp - ("New type annotation `" - ^ lexp_string ltp ^ "` incompatible with previous `" - ^ lexp_string pt ^ "`") - | [] -> () in - recur [] nctx pending_decls pending_defs - else if List.exists (fun ((_, vname'), _) -> vname = vname') - pending_defs then - (error ~loc ("Variable `" ^ vname ^ "` already defined!"); - recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) - (SMap.add vname loc pending_decls) - pending_defs - | _ -> error ~loc ("Invalid type declaration syntax : `" ^ - (sexp_string thesexp) ^ "`"); - recur [] nctx pending_decls pending_defs) - - | Some (Node (Symbol (l, "_=_") as head, args) as thesexp) - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol ((l, vname)); sexp] - when SMap.is_empty pending_decls - -> assert (pending_defs == []); - (* Used to be true before we added define-operator. *) - (* assert (ectx == nctx); *) - let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (l, Some vname) in - (* Lexp decls are always recursive, so we have to shift by 1 to - * account for the extra var (ourselves). *) - [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, - ctx_define_lsp nctx var lexp ltp - - | [Symbol (l, vname); sexp] - -> if SMap.mem vname pending_decls then - let decl_loc = SMap.find vname pending_decls in - let v = - let doc = - match decl_loc.doc, l.doc with - | Some (doc), Some (doc') - -> Some (Printf.sprintf "%s\n%s" doc doc') - | Some (doc), None | None, Some (doc) -> Some (doc) - | None, None -> None; - in - ({l with doc}, vname) - in - let pending_decls = SMap.remove vname pending_decls in - let pending_defs = ((v, sexp) :: pending_defs) in - if SMap.is_empty pending_decls then - let nctx = ectx_new_scope nctx in - let decls, nctx = lexp_check_decls ectx nctx pending_defs in - decls, sdecls, toks, nctx - else - recur [] nctx pending_decls pending_defs - - else - (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); - recur [] nctx pending_decls pending_defs) - - | [Node (Symbol s, args) as d; body] - -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - recur [Node (head, - [Symbol s; - Node (Symbol (sexp_location d, "lambda_->_"), - [sexp_u_list args; body])])] - nctx pending_decls pending_defs - - | _ -> error ~loc:l ("Invalid definition syntax : `" ^ - (sexp_string thesexp) ^ "`"); - recur [] nctx pending_decls pending_defs) - - | Some (Node (Symbol (l, "define-operator"), args)) - (* FIXME: Move this to a "special form"! *) - -> recur [] (sdform_define_operator nctx l args None) - pending_decls pending_defs - - | Some (Node (Symbol ((_l, _) as v), sargs)) - -> (* expand macro and get the generated declarations *) - let sdecl' = lexp_decls_macro v sargs nctx in - recur [sdecl'] nctx pending_decls pending_defs - - | Some sexp - -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; - recur [] nctx pending_decls pending_defs - - in (EV.set_getenv nctx; - let res = lexp_decls_1_lsp sdecls tokens nctx - pending_decls pending_defs in - (Log.stop_on_error (); res)) - -(*====================second=========================*) - (* 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 @@ -1581,19 +1382,7 @@ and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) let declss, nnctx = impl sdecls tokens nctx in decls :: declss, nnctx in impl sdecls tokens ctx - -and lexp_p_decls_for_lsp (sdecls : sexp list) (tokens : token list) (ctx : elab_context) - : ((vname * lexp * ltype) list list * elab_context) = - let rec impl sdecls tokens ctx = - match (sdecls, tokens) with - | ([], []) -> [], ectx_new_scope ctx - | _ -> - let decls, sdecls, tokens, nctx = - lexp_decls_1_lsp sdecls tokens ctx ctx SMap.empty [] in - let declss, nnctx = impl sdecls tokens nctx in - decls :: declss, nnctx in - impl sdecls tokens ctx - + and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in (Log.stop_on_error (); res) @@ -2170,13 +1959,6 @@ let lexp_decl_str str ctx = let tokens = lex_source source tenv in lexp_p_decls [] tokens ctx -let lexp_decl_str_for_lsp str ctx = - let tenv = default_stt in - let source = new Source.source_string str in - let tokens = lex_source source tenv in - lexp_p_decls_for_lsp [] tokens ctx - - (* Eval String * --------------------------------------------------------- *) (* Because we cant include Elab in eval.ml *) ===================================== src/lexp.ml ===================================== @@ -827,6 +827,25 @@ let pretty_ppctx = ("print_implicit", Bool (false)); ("grammar" , Predtl (default_grammar))] +(*Pretty ppctx for lsp*) + +let pretty_ppctx_for_lsp = + List.fold_left (fun map (key, v) -> SMap.add key v map) + SMap.empty + [("pretty" , Bool (true) ); (* print with new lines and indents *) + ("print_type" , Bool (true) ); (* print inferred Type *) + ("print_dbi" , Bool (false)); (* print dbi index *) + ("indent_size" , Int (2) ); (* indent step *) + ("color" , Bool (false) ); (* use console color to display hints *) + ("separate_decl" , Bool (true) ); (* print newline between declarations *) + ("indent_level" , Int (0) ); (* current indent level *) + ("col_max" , Int (80) ); (* col_size + col_ofsset <= col_max *) + ("col_size" , Int (0) ); (* current column size *) + ("col_ofsset" , Int (0) ); (* if col does not start at 0 *) + ("print_erasable", Bool (false)); + ("print_implicit", Bool (false)); + ("grammar" , Predtl (default_grammar))] + (* debug_ppctx is a ref so we can modify it in the REPL *) let debug_ppctx = ref ( List.fold_left (fun map (key, v) -> SMap.add key v map) @@ -837,6 +856,16 @@ let debug_ppctx = ref ( ("print_implicit", Bool (true)); ("separate_decl" , Bool (false) );]) +(*debug ppctx for lsp*) + +let debug_ppctx_for_lsp = ref ( + List.fold_left (fun map (key, v) -> SMap.add key v map) + pretty_ppctx_for_lsp + [("pretty" , Bool (false) ); + ("print_dbi" , Bool (false) ); + ("print_erasable", Bool (true)); + ("print_implicit", Bool (true)); + ("separate_decl" , Bool (false) );]) let smap_bool s ctx = match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" and smap_int s ctx = @@ -1115,6 +1144,9 @@ and lexp_str_decls ctx decls = [] decls in List.rev ret +(*print string of a type in lsp *) +let lexp_string_for_lsp e = lexp_cstring (!debug_ppctx_for_lsp) e + (** Syntactic equality (i.e. without β). *******) let rec eq e1 e2 = ===================================== src/log.ml ===================================== @@ -22,6 +22,10 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util +(*lsp enabled or no*) + +let lsp_enabled = ref false + (* LOGGING LEVELS *) type log_level = Nothing | Fatal | Error | Warning | Info | Debug @@ -187,6 +191,8 @@ let log_fatal ?section ?print_action ?loc m = typer_log_config.print_at_log <- true; log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; internal_error "Compiler Fatal Error" + + let log_error = log_msg Error ?kind:None let log_warning = log_msg Warning ?kind:None let log_info = log_msg Info ?kind:None @@ -195,16 +201,22 @@ let log_debug = log_msg Debug ?kind:None let stop_on_error () = let count = error_count () in if (0 < count) then + ( + if !lsp_enabled then stop_compilation ("Compiler stopped after: "^(string_of_int count)^" errors\n") - + else () + ) let stop_on_warning () = stop_on_error (); let count = warning_count () in if (0 < count) then + ( + if !lsp_enabled then stop_compilation ("Compiler stopped after: "^(string_of_int count)^" warnings\n") - + else () + ) (* Compiler Internal Debug print *) let debug_msg expr = if Debug <= typer_log_config.level then (print_string expr; flush stdout) ===================================== src/typer_lsp_server.ml ===================================== @@ -103,9 +103,10 @@ let rec search_lexp_with_a_location (lexp_list: Lexp.lexp list) (location : Sour let readstring (str:string) = Log.clear_log () ; + Arg.Set Log.lsp_enabled; let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) - let ast = Elab.lexp_decl_str_for_lsp str ectx in + let ast = Elab.lexp_decl_str str ectx in (!Log.typer_log, ast) let process_some_input_file (_file_contents : string) : state_after_processing = @@ -263,14 +264,10 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | Call (f, args) -> ( - let ft = Opslexp.get_type ctx f in - - match Opslexp.lexp'_whnf ft ctx with - | Arrow (ak', _v, t1, _l, t2) -> let e = browse_list_lexp (List.map (fun (_, e) -> (e, Lexp.lexp_location e)) args) cursor in - let (e',_) = e in - browse_lexp ctx e' cursor - | _ -> browse_lexp ctx ft cursor - ) + let fonc = browse_lexp ctx f cursor in + let args_list = List.map (fun (_ , e) -> browse_lexp ctx e cursor) args in + browse_list_lexp (fonc::args_list) cursor + ) | Inductive (l, _label, args, cases) ->( @@ -312,12 +309,13 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list args) in let tct = arg_loop ctx Debruijn.set_empty args in (tct, location) - ) - (* + ) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) - -> ( - let call_split e = + -> + ( + + let call_split (e: Lexp.lexp) = match Lexp.lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in @@ -329,10 +327,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let elvl = match Opslexp.lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l | _ -> Debruijn.level0 in - let it, aargs = call_split etype in - let nerased = Opslexp.nerased_let defs Debruijn.set_empty in - let subst = Subst.shift 1 in let erased = Debruijn.set_empty in + let it, aargs = call_split etype in (match Opslexp.lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = @@ -344,7 +340,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list -> mksubst (Subst.cons aarg s) fargs aargs | _,_ -> s in let s = mksubst Subst.identity fargs aargs in - let ctx_extend_with_eq ctx subst hlxp nerased = + let ctx_extend_with_eq ctx subst hlxp = let tlxp = Lexp.mkSusp e subst in let tltp = Lexp.mkSusp etype subst in let tlvl = Lexp.mkSusp elvl subst in @@ -354,10 +350,10 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list (Lexp.Anormal, hlxp); (* Lexp of the branch head *) (Lexp.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = Opslexp.dbset_push Lexp.Aerasable nerased in let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in - (nerased, nctx) in - SMap.iter + (erased, nctx) in + + let foo = (fun name (l, vdefs, branch) -> let fieldtypes = SMap.find name constructors in let rec mkctx erased ctx s hlxp vdefs fieldtypes = @@ -368,36 +364,43 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (Opslexp.dbset_push ak erased) (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) - (ssink vdef s) - (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, mkVar (vdef, 0))])) + (Lexp.ssink vdef s) + (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) vdefs fieldtypes - | _,_ -> ((erased, ctx, hlxp)) in + | _,_ -> (erased, ctx, hlxp) in let hctor = Lexp.mkCall (Lexp.mkCons (it, (l, name)), List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in let subst = Subst.shift (List.length vdefs) in - let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in - (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1)))) - branches; - let diff = SMap.cardinal constructors - SMap.cardinal branches in + let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in + browse_lexp ctx branch cursor; + (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1))) + ) + in + let lst = foo (Lexp.get_name branches) branches in + let brch = SMap.bindings lst in + + let diff = SMap.cardinal constructors - SMap.cardinal brch in (match default with | Some (v, d) -> if diff <= 0 then (); let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = Debruijn.set_sink 1 erased in let subst = Subst.shift 1 in - let hlxp = mkVar ((l, None), 0) in + let hlxp = Lexp.mkVar ((l, None), 0) in let (nerased, nctx) = - ctx_extend_with_eq nctx subst hlxp nerased in + ctx_extend_with_eq nctx subst hlxp in (Lexp.mkSusp ret (Subst.shift 2)) | None -> if diff > 0 then () ) - | _,_ -> ()); + | _,_ -> ())); (ret,location) + ) - *) + + | Cons (t, (_l, name)) -> (match Opslexp.lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) @@ -518,7 +521,7 @@ class lsp_server = let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (l_type,location) = browse_lexp ctx lexp typer_loc in let range = lsp_range_of_loc location in - let s = Lexp.lexp_string l_type in + let s = Lexp.lexp_string_for_lsp l_type in let r = Lsp.Types.Hover.create ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) ~range:range () @@ -543,10 +546,15 @@ class lsp_server = let e = Linol_lwt.return h in e | _ -> assert false - method! config_modify_capabilities compl = - let t = Lsp.Types.CompletionOptions.create ~workDoneProgress:true ~resolveProvider:true () in - Lsp.Types.ServerCapabilities.create ~completionProvider:t () - + method! config_modify_capabilities arg = + let completionProvider = + (* TODO even if this re-enabled in general, it should stay disabled for + emacs. It makes completion too slow *) + Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; "\""; "'"; "/"; "@"; "<"] + ~resolveProvider:true () in + { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider } + + (* provisional, to be done later *) method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a3ccd6b24bc48f76e66d560c483222f51… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a3ccd6b24bc48f76e66d560c483222f51… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Mai 2021