June 2022 - Typer - mailman.iro.umontreal.ca

Re: [Typer] REPL --> eval_interactive --> lexprs
by Stefan Monnier 16 Jun '22

16 Jun '22

>>> Pour `x = cons 1 nil;`, son type de retour est : >>> >>> ********************************************************************** >>> **************** REPL --> eval_interactive --> lexprs **************** >>> ********************************************************************** >>> >>> x[0] >>> --------------------------------------------------->>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> --------------------------------------------------->>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> (a : (##Type_ ##TypeLevel.z)) ≡> (inst : (let FromInteger : (α : >>> Type[247]) -> Type[248]; FromInteger = typecons (FromInteger (α : >>> Type[248])) (mkFromInteger (Integer[255] -> α[1])) in typecons >>> (FromInteger (α : Type[248])) (mkFromInteger (Integer[255] -> α[1])) a[0])) >>> => (List[158] ##TypeLevel.z a[1]) >>> >>> Vous pouvez m'expliquer la ligne suivante? >> >> J'ai pas vu de "ligne suivante", donc je vais expliquer la ligne >> précédente à la place: >> >> (a : (##Type_ ##TypeLevel.z)) >> ≡> (inst : (let FromInteger : (α : Type[247]) -> Type[248]; >> FromInteger = typecons (FromInteger (α : Type[248])) >> (mkFromInteger (Integer[255] -> α[1])) >> in (typecons (FromInteger (α : Type[248])) >> (mkFromInteger (Integer[255] -> α[1]))) >> a[0])) >> => (List[158] ##TypeLevel.z a[1]) >> >> (j'ai juste rajouté des retour à la ligne et des espaces, plus 1(!) paire >> de parenthèses (celle qui s'ouvre juste après le `in`) qui manquait). >> >> Donc, en gros: >> >> (a : Type) ≡> (inst : FromInteger a) => List a >> >> Ce qui signifie une liste de type `a` pour n'importe quel type `a` pour >> autant que c'est un type dans la type-classe `FromInteger`. > > Est-ce normalement d'avoir une liste de type `a` pour n'importe quel type `a` ? > > Vu que j'ai défini une liste d'entier. Le type de la liste doit être > de type `Int ou ##Int` non ? En fait, tu n'as pas défini une liste d'entiers. Tu a définis une liste qui contient un élément, cet élément étant représenté dans le code source par le litéral "1". Le litéral "1" peut être un `Int`, ou un `Integer` ou un `Float`, ou potentiellement plein d'autres choses. Il a type: (a : Type) ≡> (inst : FromInteger a) => a Si tu veux une liste de `int`, alors il faut le spécifier explicitement, e.g.: cons (1 : Int) nil ou (cons 1 nil) : List Int Ce problème apparaît rarement dans un vrai programme, parce que ce `cons 1 nil` va être utilisé quelque part et ce "quelque part" va finir par spécifier quel genre de nombres on veut, mais dans la "repl" ce n'est pas le cas. Il faudrait qu'on ajoute à la "repl" une règle qui prend un choix par défaut (e.g. ici on pourrait utiliser `Integer`) pour éviter ces situations, qui sont techniquement pas incorrectes mais n'en restent pas moins indésirables. Stefan

1 0

Le serveur LSP est disponible
by Soilih BEN SOILIH 13 Jun '22

13 Jun '22

Bonjour Typeriens, J'espère que vous allez bien ! Je voulais juste vous informer que le serveur LSP est disponible sur la branche minimal-server. J'ai mis à jour le README.md pour que vous voyez comment l'utiliser sur Emacs. Tout n'est pas encore parfait, mais il fonctionne déjà, et peut aider un peu si on veut écrire du code Typer. Si vous avez des retours à me faire, je serais ravi de vous lire. Merci beaucoup, bien à vous !

1 0

[Git][monnier/typer][minimal-server] -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 13 Jun '22

13 Jun '22

Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer Commits: 045b1f20 by Soilih at 2022-06-13T15:08:42-04:00 - - - - - - 1 changed file: - README.md Changes: ===================================== README.md ===================================== @@ -36,8 +36,10 @@ By default, Dune creates a '_build' folder which holds all the compiled files. # Use The LSP Server in Emacs To use the LSP server in Emacs, you have to do 2 things: * name the executable: **typer** + You can use the command: *ln -s /home/path/to/your/executable/typer.exe typer* -* Install Typer-mode in Emacs and use it. For, you can open - the file *typer-mode.el* in Emacs and do: - *M-x package-install-from-buffer* +* Install Typer-mode in Emacs and use it. + + For that, you can open the file *typer-mode.el* in Emacs and do: + *M-x package-install-from-buffer* View it on GitLab: https://gitlab.com/monnier/typer/-/commit/045b1f20ed9ddc6200ce04c7cc0d84fbd… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/045b1f20ed9ddc6200ce04c7cc0d84fbd… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][minimal-server] make the server available
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 13 Jun '22

13 Jun '22

Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer Commits: f995dc36 by Soilih at 2022-06-13T15:04:23-04:00 make the server available - - - - - 4 changed files: - README.md - btl/pervasive.typer - src/elab.ml - typer.ml Changes: ===================================== README.md ===================================== @@ -32,3 +32,12 @@ By default, Dune creates a '_build' folder which holds all the compiled files. # Emacs files /typer-mode.el + +# Use The LSP Server in Emacs +To use the LSP server in Emacs, you have to do 2 things: +* name the executable: **typer** + You can use the command: + *ln -s /home/path/to/your/executable/typer.exe typer* +* Install Typer-mode in Emacs and use it. For, you can open + the file *typer-mode.el* in Emacs and do: + *M-x package-install-from-buffer* ===================================== btl/pervasive.typer ===================================== @@ -567,7 +567,7 @@ define-operator "<-" 80 96; %% %% `List` is the type and `list` is the module %% -list = load "/home/soilih/Projet Maitrise/typer/btl/list.typer"; +list = load "btl/list.typer"; %% %% Macro `do` for easier series of IO operation @@ -575,13 +575,13 @@ list = load "/home/soilih/Projet Maitrise/typer/btl/list.typer"; %% e.g.: %% do { IO_return true; }; %% -do = let lib = load "/home/soilih/Projet Maitrise/typer/btl/do.typer" in lib.do; +do = let lib = load "btl/do.typer" in lib.do; %% %% Module containing various macros for tuple %% Used by `case_` %% -tuple-lib = load "/home/soilih/Projet Maitrise/typer/btl/tuple.typer"; +tuple-lib = load "btl/tuple.typer"; %% %% Get the nth element of a tuple @@ -612,7 +612,7 @@ Tuple = tuple-lib.tuple-type; %% %% Macro `case` for a some more complex pattern matching %% -case_ = let lib = load "/home/soilih/Projet Maitrise/typer/btl/case.typer" in lib.case-macro; +case_ = let lib = load "btl/case.typer" in lib.case-macro; %% %% plain-let @@ -629,7 +629,7 @@ define-operator "plain-let" () 3; %% define-operator "in" 3 67; %% -plain-let_in_ = let lib = load "/home/soilih/Projet Maitrise/typer/btl/plain-let.typer" in lib.plain-let-macro; +plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; %% %% `case` at function level @@ -639,7 +639,7 @@ plain-let_in_ = let lib = load "/home/soilih/Projet Maitrise/typer/btl/plain-let %% | true => false %% | false => true; %% -_|_ = let lib = load "/home/soilih/Projet Maitrise/typer/btl/polyfun.typer" in lib._|_; +_|_ = let lib = load "btl/polyfun.typer" in lib._|_; %% %% case_as_return_, case_return_ @@ -648,7 +648,7 @@ _|_ = let lib = load "/home/soilih/Projet Maitrise/typer/btl/polyfun.typer" in l define-operator "as" 42 42; define-operator "return" 42 42; -depelim = load "/home/soilih/Projet Maitrise/typer/btl/depelim.typer"; +depelim = load "btl/depelim.typer"; case_as_return_ = depelim.case_as_return_; case_return_ = depelim.case_return_; ===================================== src/elab.ml ===================================== @@ -70,14 +70,15 @@ let elab_check = ref false let dloc = dummy_location let parsing_internals = ref false + +let str_ref = ref "" let btl_folder = try Sys.getenv "TYPER_BUILTINS" - 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" + with Not_found -> 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 = @@ -1843,12 +1844,12 @@ let sform_load usr_elctx loc sargs _ot = | [String (_,file_name)] -> if !in_pervasive then ( if (Filename.is_relative file_name) then - (read_file btl_folder usr_elctx) + (read_file (Filename.concat !str_ref file_name) usr_elctx) else (read_file file_name usr_elctx) ) else if (Filename.is_relative file_name) then - (read_file btl_folder !sform_default_ectx) + (read_file (Filename.concat !str_ref file_name) !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 ===================================== typer.ml ===================================== @@ -43,7 +43,8 @@ let arg_defs = Arg.String Log.set_typer_log_level_str, "Set the logging level"); - ("--lsp", Arg.Set lsp_server, "Enable Typer LSP server"); + ("--lsp", Arg.Unit (fun _ -> let _ = lsp_server := true + in ()), "Enable Typer LSP server"); ("--check", Arg.Set Elab.elab_check, "Enable Checking"); @@ -67,6 +68,8 @@ 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; + if !lsp_server then Typer_lsp_server.run () + else (); print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; print_newline (); @@ -98,8 +101,6 @@ let run_main argv = Log.print_log () let main () = - if !lsp_server then Typer_lsp_server.run () - else (); let command, argv = if Array.length Sys.argv <= 1 then "repl", [||] View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f995dc362b84c3ea40b7f2bc5349da19c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f995dc362b84c3ea40b7f2bc5349da19c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][minimal-server] 11 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 10 Jun '22

10 Jun '22

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

1 0

[Git][monnier/typer] Pushed new branch open-module
by Jean-Alexandre Barszcz (＠jabarszcz) 03 Jun '22

03 Jun '22

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

1 0

[Git][monnier/typer][minimal-server] 3 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 01 Jun '22

01 Jun '22

Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer Commits: f7f9c37f by Soilih at 2022-06-01T10:08:42-04:00 - - - - - - 500b8fb7 by Soilih at 2022-06-01T13:42:10-04:00 - - - - - - 8ca46ab9 by Soilih at 2022-06-01T14:42:53-04:00 adding completion with Proj constructor - - - - - 2 changed files: - src/typer_lsp_server.ml - typer.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -459,11 +459,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De ) | Proj (l, lxp, (_, _)) - -> - let candidats = (browse_lexp ctx lxp cursor lst_in):: + -> + let candidats = (browse_lexp ctx lxp cursor lst_in):: (ctx, None, (Opslexp.get_type ctx e_in), Some (Opslexp.get_type ctx lxp), l, lst_in) :: [] in - browse_list_lexp candidats cursor + browse_list_lexp candidats cursor | Case (l, e, _, branches, default) -> @@ -742,7 +742,7 @@ let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) = (* List of separators that delimit a word *) -let sep_list = [';';',';'(';')';' ';'{';'}'] +let sep_list = [';';',';'(';')';' ';'{';'}';'.'] let split_string_line (content:string) (line:int) = @@ -1236,19 +1236,17 @@ class lsp_server = let e = Some r in let f = Linol_lwt.return e in f - method! on_req_completion ~notify_back:_ ~id:_ ~uri ~pos ~ctx:_ doc_state = + method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with - | document_state -> let (_,ast,cur) = document_state in - cur := Some (pos.line, pos.character); + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (pos.line,pos.character); 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 (_, lexp, _) = vx in - *) - let lexp = trans_list_in_list_to_let list_list 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 @@ -1256,14 +1254,14 @@ class lsp_server = let word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in *) - match browse_lexp ctx lexp typer_loc [] with + match browse_lexp lctx lexp typer_loc [] with | (l_ctx,_,_, None,_,_) -> let my_str = split_string_line doc_state.content (pos.line + 1) in let word = use_search_word my_str sep_list pos.character "" in let range = lsp_range_of_a_tuple - (typer_loc.start_line,(typer_loc.start_column - String.length word)) + (typer_loc.start_line,(typer_loc.end_column - String.length word)) (typer_loc.end_line, typer_loc.end_column) in let filtred_list = filter_lctx l_ctx [] in @@ -1273,10 +1271,10 @@ class lsp_server = let e = Some (`List comp_list_ret) in let f = Linol_lwt.return e in f - | (_, _, _, Some lxp, _, _) - -> ( - match Lexp.lexp_lexp' lxp with - | Inductive (_, (_, _label), _fargs, constructors) + | (lctx, _, _, Some lxp, _,_) + -> (let ret = Opslexp.lexp_whnf lxp lctx in + match Lexp.lexp_lexp' ret with + | Inductive (_, (_,label), fargs, constructors) when SMap.cardinal constructors = 1 -> let my_str = split_string_line doc_state.content (pos.line + 1) in let word = use_search_word my_str sep_list pos.character "" in @@ -1291,15 +1289,15 @@ class lsp_server = let str = Option.get s in let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(str) in let kind = Lsp.Types.CompletionItemKind.Function in - let ci = Lsp.Types.CompletionItem.create + let ci = Lsp.Types.CompletionItem.create ~label:str ~kind:kind ~textEdit:textEdit ~detail:(Lexp.lexp_string_for_lsp t) () in ci ) fieldtypes in - let e = Some (`List comp_list) in - let f = Linol_lwt.return e in f + let e = Some (`List comp_list) in + let f = Linol_lwt.return e in f | _ -> failwith "Our Lexp is not an Inductive Type!!!" ) ===================================== typer.ml ===================================== @@ -102,7 +102,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/8f23b3470dcd115470055142bcb399b8… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/8f23b3470dcd115470055142bcb399b8… You're receiving this email because of your account on gitlab.com.

1 0