Typer Juin 2021

typer@iro.umontreal.ca

3 participants
9 discussions

[Git][monnier/typer][soilih] 5 commits: elab_check
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 29 Jui '21

29 Jui '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 0a79b565 by Soilih BEN SOILIH at 2021-06-16T20:53:17-06:00 elab_check - - - - - 170bef61 by Soilih BEN SOILIH at 2021-06-17T09:50:42-06:00 - - - - - - 859393dd by Soilih BEN SOILIH at 2021-06-21T23:54:06-06:00 - - - - - - 79ab4063 by Soilih BEN SOILIH at 2021-06-22T20:09:28-06:00 - - - - - - bb0904ae by Soilih BEN SOILIH at 2021-06-29T15:58:45-06:00 fixing context - - - - - 7 changed files: - dune - src/dune - src/elab.ml - src/log.ml - src/opslexp.ml - src/typer_lsp_server.ml - typer.ml Changes: ===================================== dune ===================================== @@ -12,4 +12,4 @@ (promote (until-clean)) (modules debug_util) (libraries typerlib) - (modes byte native)) + (modes byte native)) \ No newline at end of file ===================================== src/dune ===================================== @@ -5,4 +5,3 @@ linol linol-lwt lsp jsonrpc yojson base )) - ===================================== src/elab.ml ===================================== @@ -60,6 +60,9 @@ module Unif = Unification module OL = Opslexp module EL = Elexp +(*boolean used to enable checking*) +let elab_check = ref false + (* dummies *) let dloc = Source.Location.dummy @@ -214,24 +217,32 @@ let elab_check_def (ctx : elab_context) var lxp ltype = ) let ctx_extend (ctx: elab_context) (var : vname) def ltype = - elab_check_proper_type ctx ltype var; + if !elab_check then + elab_check_proper_type ctx ltype var + else (); ectx_extend ctx var def ltype let ctx_define (ctx: elab_context) var lxp ltype = - elab_check_def ctx var lxp ltype; + if !elab_check then + elab_check_def ctx var lxp ltype + else (); 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) - -> elab_check_proper_type - nctx (push_susp ltp (S.shift n)) var; + -> if !elab_check then + elab_check_proper_type + nctx (push_susp ltp (S.shift n)) var + else (); n - 1) (List.length decls) decls in let _ = List.fold_left (fun n (var, lxp, ltp) - -> elab_check_def nctx var lxp - (push_susp ltp (S.shift n)); + -> if !elab_check then + elab_check_def nctx var lxp + (push_susp ltp (S.shift n)) + else (); n - 1) (List.length decls) decls in ===================================== src/log.ml ===================================== @@ -204,16 +204,20 @@ 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 = ===================================== src/opslexp.ml ===================================== @@ -583,22 +583,18 @@ and check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () - else ( if !Log.lsp_enabled then - (error_tc ~loc:(lexp_location e) + else (error_tc ~loc:(lexp_location e) ("Type mismatch for " ^ lexp_string e ^ " : " ^ lexp_string t ^ " != " - ^ lexp_string t')) - else (); + ^ lexp_string t'); (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in (match lexp'_whnf s ctx with | Sort _ -> () - | _ -> if !Log.lsp_enabled then - error_tc ~loc:(lexp_location t) - ("Not a proper type: " ^ lexp_string t) - else () + | _ -> error_tc ~loc:(lexp_location t) + ("Not a proper type: " ^ lexp_string t) ); (* FIXME: return the `sort` rather than the surrounding `lexp`! *) s in @@ -607,8 +603,7 @@ and check'' erased ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) - -> ( if !Log.lsp_enabled then - error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; + -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -638,10 +633,9 @@ and check'' erased ctx e = (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) -> if DB.set_mem idx erased then - ( if !Log.lsp_enabled then error_tc ~loc:l ("Var `" ^ maybename name ^ "`" - ^ " can't be used here, because it's `erasable`")); + ^ " can't be used here, because it's `erasable`"); lookup_type ctx v | Susp (e, s) -> check erased ctx (push_susp e s) | Let (l, defs, e) @@ -672,17 +666,14 @@ and check'' erased ctx e = match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | SortInvalid - -> if !Log.lsp_enabled then - error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; + -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; mkSort (l, StypeOmega) | SortK1NotType - -> ( if !Log.lsp_enabled then - error_tc ~loc:(lexp_location t1) + -> ( error_tc ~loc:(lexp_location t1) "Not a proper type"; mkSort (l, StypeOmega)) | SortK2NotType - -> ( if !Log.lsp_enabled then - error_tc ~loc:(lexp_location t2) + -> ( error_tc ~loc:(lexp_location t2) "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) @@ -700,14 +691,12 @@ and check'' erased ctx e = match lexp'_whnf ft ctx with | Arrow (ak', _v, t1, _l, t2) -> if not (ak == ak') then - ( if !Log.lsp_enabled then - error_tc ~loc:(lexp_location arg) - "arg kind mismatch"; ()) - else (); + error_tc ~loc:(lexp_location arg) + "arg kind mismatch"; () + ; assert_type ctx arg at t1; mkSusp t2 (S.substitute arg) - | _ -> ( if !Log.lsp_enabled then - error_tc ~loc:(lexp_location arg) + | _ -> ( error_tc ~loc:(lexp_location arg) ("Calling a non function (type = " ^ lexp_string ft ^ ")!"); ft)) @@ -734,15 +723,14 @@ and check'' erased ctx e = (* FIXME: If it does refer, * we get an ugly error! *) (mkSusp level' (L.sunshift n)) - | _tt -> if !Log.lsp_enabled then - (error_tc ~loc:(lexp_location t) + | _tt -> error_tc ~loc:(lexp_location t) ~print_action:(fun _ -> DB.print_lexp_ctx ictx; print_newline () ) ("Field type " ^ lexp_string t ^ " is not a Type! (" - ^ lexp_string lwhnf ^")")); + ^ lexp_string lwhnf ^")"); level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, @@ -785,8 +773,7 @@ and check'' erased ctx e = (* We don't check aarg's type, because we assume that `check` * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> ( if !Log.lsp_enabled then - error_tc ~loc:l + | _,_ -> ( error_tc ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = @@ -816,8 +803,7 @@ and check'' erased ctx e = (ssink vdef s) (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes - | _,_ -> ( if !Log.lsp_enabled then - error_tc ~loc:l + | _,_ -> ( error_tc ~loc:l "Wrong number of args to constructor!"; (erased, ctx, hlxp)) in let hctor = @@ -835,9 +821,9 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 then - ( if !Log.lsp_enabled then + ( warning_tc ~loc:l "Redundant default clause" - else ()); + ); let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -849,16 +835,12 @@ and check'' erased ctx e = | None -> if diff > 0 then ( - if !Log.lsp_enabled then - (error_tc ~loc:l ("Non-exhaustive match: " + error_tc ~loc:l ("Non-exhaustive match: " ^ string_of_int diff ^ " cases missing") - ) - else () + ) ) - | _,_ -> if !Log.lsp_enabled then - error_tc ~loc:l "Case on a non-inductive type!" - else () + | _,_ -> error_tc ~loc:l "Case on a non-inductive type!" ); ret | Cons (t, (_l, name)) @@ -887,12 +869,10 @@ and check'' erased ctx e = buildtype fargs) in buildtype fargs with Not_found - -> ( if !Log.lsp_enabled then - error_tc ~loc:l + -> ( error_tc ~loc:l ("Constructor \"" ^ name ^ "\" does not exist"); DB.type_int)) - | _ -> ( if !Log.lsp_enabled then - error_tc ~loc:(lexp_location e) + | _ -> ( error_tc ~loc:(lexp_location e) ("Cons of a non-inductive type: " ^ lexp_string t); DB.type_int)) ===================================== src/typer_lsp_server.ml ===================================== @@ -36,11 +36,11 @@ Diagnostics includes all the warnings, errors and messages that the processing of a document are expected to be able to return. *) -open Log +open Log open Util type state_after_processing = (log_entry list * - (((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) option) + ((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) ) let log_entry_to_list (tab:log_entry list) : ((string * int * int * int * int) * log_level * string) list = List.map (fun x -> let location = Option.get x.loc in @@ -105,15 +105,8 @@ let readstring (str:string) = Log.clear_log () ; let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) - let oast = - try - Some (Elab.lexp_decl_str str ectx) - with - | Log.Stop_Compilation msg - | Log.Internal_error msg - | Log.User_error msg -> None - in - (!Log.typer_log, oast) + let ast = Elab.lexp_decl_str str ectx in + (!Log.typer_log, ast) let process_some_input_file (_file_contents : string) : state_after_processing = Logs.err (fun k->k " %s" @@ "TEST TEST TEST"); @@ -159,12 +152,17 @@ module Compl = struct kind:k } + let lsp_pos_of_a_tuple (a,b) : Lsp.Types.Position.t = + Lsp.Types.Position.create ~line:(a) ~character:(b) + + let lsp_range_of_a_tuple (a,b) (x,y) : Lsp.Types.Range.t = + Lsp.Types.Range.create ~start:(lsp_pos_of_a_tuple (a,b)) ~end_:(lsp_pos_of_a_tuple (x,y)) let t_from_tuple (tup : (int * string * string * string * k) list) : t list = List.map (fun x -> let (id,label,newText,detail,kind) = x in let ret = { - id = id; + id = id ; label = label ; newText = newText ; detail = detail ; @@ -181,6 +179,7 @@ module Compl = struct (1, "add", "add()", "add a element to a list", Method); (1, "pop", "pop()", "remove a element from a list", Method); ] + let createKind (element:t) = match element.kind with | Text -> Lsp.Types.CompletionItemKind.Text @@ -241,20 +240,19 @@ module Compl = struct let rec complete (str:string) (liste: t list) = match str with | "List." -> let lst = List.filter (fun x -> - Int.equal x.id 1 - ) - liste - in - let m = String.split_on_char '.' str in - complete (List.nth m 1) lst - + Int.equal x.id 1 + ) + liste + in + let m = String.split_on_char '.' str in + complete (List.nth m 1) lst | str -> List.filter (fun x -> let reg = match_str str in Str.string_match reg x.label 0 ) liste - end +end (*==============completion============================*) @@ -271,16 +269,18 @@ module Compl = struct ) ) - let find_the_nearest_lexp (tab:Lexp.lexp list) (cursor:Source.Location.t) = - let rec foo tab cursor = - match tab with + let find_the_nearest_lexp (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) lst in + let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in + let rec foo lexp_list cursor = + match lexp_list with | [] -> failwith "Liste vide!" | [n] -> n | [hd;tl] -> if (dist (Lexp.lexp_location hd) cursor < dist (Lexp.lexp_location tl) cursor ) then hd else tl |hd::ml::tl -> if (dist (Lexp.lexp_location hd) cursor < dist (Lexp.lexp_location ml) cursor ) then (foo (hd::tl) cursor) else foo (ml::tl) cursor - in foo tab cursor + in foo lexp_list cursor let browse_list_lexp (tab:(Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) = let rec foo tab cursor = @@ -297,10 +297,12 @@ module Compl = struct else foo (ml::tl) cursor in foo tab cursor - let pos_in_lexp_interval (tab:Lexp.lexp list) (cursor:Source.Location.t) = + let pos_in_lexp_interval (lst: (vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) lst in + let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in let open Source.Location in - let rec foo tab cursor = - match tab with + let rec foo lexp_list cursor = + match lexp_list with | [] -> failwith "Liste vide!" | hd::tl -> let location = Lexp.lexp_location hd in if ((location.start_line <= cursor.start_line && location.start_column <= cursor.start_column) @@ -308,11 +310,19 @@ module Compl = struct (location.end_line >= cursor.end_line && location.end_column >= cursor.end_column)) then hd else foo tl cursor - in foo tab cursor - - let lexp_search (tab:Lexp.lexp list) (cursor:Source.Location.t) = - try pos_in_lexp_interval tab cursor - with exn -> find_the_nearest_lexp tab cursor + in foo lexp_list cursor + + let lexp_search (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let lctx = List.fold_left + (fun x y -> + Debruijn.lctx_extend_rec x y + ) + ctx lst + in + let lexp = try pos_in_lexp_interval lst cursor + with exn -> find_the_nearest_lexp lst cursor + in + (lctx,lexp) (* search the type of a lexp browsing a lexp*) let rec browse_lexp ctx e cursor = @@ -360,8 +370,11 @@ module Compl = struct | SortK2NotType -> (Lexp.mkSort (l, StypeOmega), location) ) - | Lambda (ak, ((l,_) as v), t, e) -> let (e',loc) = browse_lexp ctx e cursor in - (Lexp.mkArrow (ak, v, t, l,e'), loc) + | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in + let a = browse_lexp ctx' e cursor in + let b = browse_lexp ctx t cursor in + let (ret,loc) = browse_list_lexp (a::b::[]) cursor in + (Lexp.mkArrow (ak, v, t, l,ret), loc) | Call (f, args) -> ( @@ -417,18 +430,18 @@ module Compl = struct 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 candidats = ref [] in let call_split (e: Lexp.lexp) = match Lexp.lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let (e',_) = browse_lexp ctx e cursor in - let etype = Opslexp.lexp_whnf e' ctx in + candidats := (browse_lexp ctx e cursor):: !candidats; + let etype = Opslexp.get_type ctx e in (* FIXME save the type in the case lexp instead of recomputing it over and over again *) let ekind = Opslexp.get_type ctx etype in @@ -437,7 +450,8 @@ module Compl = struct | _ -> Debruijn.level0 in let erased = Debruijn.set_empty in let it, aargs = call_split etype in - (match Opslexp.lexp'_whnf it ctx, aargs with + + match Opslexp.lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -464,7 +478,8 @@ module Compl = struct let brch = SMap.bindings branches in let lst = List.map - (fun (name, (l, vdefs, branch)) + ( + 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 @@ -485,9 +500,7 @@ module Compl = struct 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 - ignore (browse_lexp ctx branch cursor); - (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1))) - + candidats := (browse_lexp ctx branch cursor) :: !candidats; ) brch in @@ -503,13 +516,14 @@ module Compl = struct let hlxp = Lexp.mkVar ((l, None), 0) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in + candidats := (browse_lexp ctx d cursor) :: !candidats; browse_lexp ctx d cursor | None -> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy) ) - | _,_ -> (Lexp.impossible, Source.Location.dummy) ); + | _,_ -> (Lexp.impossible, Source.Location.dummy) ; - (ret,location) + browse_list_lexp !candidats cursor ) @@ -609,7 +623,7 @@ class lsp_server = match Hashtbl.find buffers uri with | state_after_processing -> let (_,ast) = state_after_processing in - let (list_list, _) = Option.get ast in + let (list_list, _) = ast in let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in let typer_loc = typer_pos_of_lsp_pos pos in @@ -627,13 +641,11 @@ class lsp_server = match Hashtbl.find buffers uri with | state_after_processing -> let (_,ast) = state_after_processing in - let (list_list, _) = Option.get ast in - let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in - let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in + let (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos pos in - let lexp = lexp_search lexp_list typer_loc in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (l_type,location) = browse_lexp ctx lexp typer_loc in + let (lctx,lexp) = lexp_search ctx list_list typer_loc in + let (l_type,location) = browse_lexp lctx lexp typer_loc in let range = lsp_range_of_loc location in let s = Lexp.lexp_string_for_lsp l_type in let r = Lsp.Types.Hover.create @@ -677,21 +689,25 @@ class lsp_server = let fbyline = Compl.list_filter_by_line trans_string (pos.line + 1) in let word = Compl.list_filter_by_character fbyline ((pos.line + 1),pos.character) in let typer_loc = typer_pos_of_lsp_pos pos in - let range = lsp_range_of_loc typer_loc in + + let range = Compl.lsp_range_of_a_tuple + (typer_loc.start_line,(typer_loc.end_column - 2 - String.length word)) + (typer_loc.end_line, typer_loc.end_column) + in let tab_compl = Compl.complete word (Compl.t_from_tuple Compl.exemple_liste) in let r = List.map (fun (x:Compl.t) -> - let label = x.label in - let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(x.newText) in - let kind = Compl.createKind x in - let detail = x.detail in - let ci = Lsp.Types.CompletionItem.create - ~label:label ~kind:kind - ~preselect:(true) - ~textEdit:textEdit ~detail:detail () - in - ci + let label = x.label in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(x.newText) in + let kind = Compl.createKind x in + let detail = x.detail in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:detail () + in + ci + ) tab_compl in let e = Some (`List r) in @@ -713,4 +729,4 @@ let run () = | exception e -> let e = Printexc.to_string e in Printf.eprintf "error: %s\n%!" e; - exit 1 \ No newline at end of file + exit 1 ===================================== typer.ml ===================================== @@ -31,11 +31,9 @@ let welcome_msg = let arg_batch = ref false (* -booléen utilisé pour démarrer le serveur. -mis true pour les tests +boolean used to start the LSP server. +made true for testing *) - - let lsp_server = ref true let arg_files = ref [] @@ -45,7 +43,7 @@ let add_input_file file = let arg_defs = [("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); ("--lsp", Arg.Set lsp_server, "Enable Typer LSP server"); - + ("--check", Arg.Set Elab.elab_check, "Enable internal checking"); ("--verbosity", Arg.String Log.set_typer_log_level_str, "Set the logging level"); View it on GitLab: https://gitlab.com/monnier/typer/-/compare/8e4c57753af78736d6b0d58946e1a742… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/8e4c57753af78736d6b0d58946e1a742… You're receiving this email because of your account on gitlab.com.

1 0

Module problem
by Soilih BEN SOILIH 16 Jui '21

16 Jui '21

Bonjour tout le monde, J'espère que vous allez bien ! J'ai un petit problème que je n'arrive pas à fixer là qui commence à me prendre du temps. En soit, j'ai une référence définie comme suit dans le fichier typer.ml : elab_check = ref false Je veux y accéder depuis le fichier typer_lsp_server.ml qui est dans src/ Si je fais !Typer.elab_check, il trouve pas le module Typer, si je rajoute typerlib au fichier dune qui est dans src, ça me dit qu'il y'a une erreur cyclique. Comment résoudre ce problème ? Merci beaucoup, bien à vous !

2 1

[Git][monnier/typer][soilih] a better way to complete
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 15 Jui '21

15 Jui '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 8e4c5775 by Soilih BEN SOILIH at 2021-06-15T07:07:01-06:00 a better way to complete - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -152,6 +152,7 @@ module Compl = struct | TypeParameter type t = { + id:int; label:string; newText:string;(*the text the completion will send*) detail:string; @@ -159,10 +160,11 @@ module Compl = struct } - let t_from_tuple (tup : (string * string * string * k) list) : t list = + let t_from_tuple (tup : (int * string * string * string * k) list) : t list = List.map (fun x - -> let (label,newText,detail,kind) = x in + -> let (id,label,newText,detail,kind) = x in let ret = { + id = id; label = label ; newText = newText ; detail = detail ; @@ -172,13 +174,13 @@ module Compl = struct ) tup let exemple_liste = [ - ("lambda", "lambda (pattern) -> pattern ", "define a function", Text); - ("case", "case scrutinee \n | pattern -> pattern ", "pattern matching", Function); - ("let", "let_in_ (_=_ x ()) x ", "let...in", Text); - ("if", " if_then_else_ x \"x is true\" \"x is false\"", "if...condition", Text); - ("add", "add()", "add a element to a list", Method); + (0, "lambda", "lambda (pattern) -> pattern ", "define a function", Text); + (0, "case", "case scrutinee \n | pattern -> pattern ", "pattern matching", Function); + (0, "let", "let_in_ (_=_ x ()) x ", "let...in", Text); + (0, "if", " if_then_else_ x \"x is true\" \"x is false\"", "if...condition", Text); + (1, "add", "add()", "add a element to a list", Method); + (1, "pop", "pop()", "remove a element from a list", Method); ] - let createKind (element:t) = match element.kind with | Text -> Lsp.Types.CompletionItemKind.Text @@ -236,12 +238,16 @@ module Compl = struct |> Str.regexp - let complete (str:string) (liste: t list) = + let rec complete (str:string) (liste: t list) = match str with - | "List." -> List.filter (fun x -> - String.equal x.label "add" + | "List." -> let lst = List.filter (fun x -> + Int.equal x.id 1 ) - liste + liste + in + let m = String.split_on_char '.' str in + complete (List.nth m 1) lst + | str -> List.filter (fun x -> let reg = match_str str in Str.string_match reg x.label 0 @@ -682,6 +688,7 @@ class lsp_server = let detail = x.detail in let ci = Lsp.Types.CompletionItem.create ~label:label ~kind:kind + ~preselect:(true) ~textEdit:textEdit ~detail:detail () in ci View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8e4c57753af78736d6b0d58946e1a7421… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8e4c57753af78736d6b0d58946e1a7421… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 2 commits: improve print and log error
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 12 Jui '21

12 Jui '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 8cc99a68 by Soilih BEN SOILIH at 2021-05-31T23:30:38-06:00 improve print and log error - - - - - 9abad61f by Soilih BEN SOILIH at 2021-06-12T13:16:16-06:00 completion, readstring, check, log - - - - - 11 changed files: - debug_util.ml - − samples/.#acc.typer - src/debruijn.ml - src/debug.ml - src/dune - src/elab.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/typer_lsp_server.ml - typer.ml Changes: ===================================== debug_util.ml ===================================== @@ -91,7 +91,7 @@ let format_dest = ref "" let write_file = ref false let mod_ctx name v = let f ctx = ctx := SMap.add name v !ctx in - f ppctx; f debug_ppctx + f ppctx; f (if !Log.lsp_enabled then debug_ppctx else debug_ppctx_for_lsp) let set_print_type v () = mod_ctx "print_type" (Bool v) let set_print_index v () = mod_ctx "print_dbi" (Bool v) ===================================== samples/.#acc.typer deleted ===================================== @@ -1 +0,0 @@ -soilih@soilih-HP-Laptop-15-db0xxx.11163:1621953914 \ No newline at end of file ===================================== src/debruijn.ml ===================================== @@ -292,7 +292,7 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = (match lexp with | None -> print_string "<var>" | Some lexp - -> (let str = lexp_str (!debug_ppctx) lexp in + -> (let str = lexp_str (if !Log.lsp_enabled then (!debug_ppctx) else (!debug_ppctx_for_lsp)) lexp in let strs = match String.split_on_char '\n' str with | hd :: tl -> print_string hd; tl ===================================== src/debug.ml ===================================== @@ -124,7 +124,7 @@ let debug_lexp_decls decls = lalign_print_string (lexp_name lxp) 15; Printf.printf "[%s]" (Source.Location.to_string loc); - let str = lexp_str_decls (!debug_ppctx) [e] in + let str = lexp_str_decls (if !Log.lsp_enabled then (!debug_ppctx) else (!debug_ppctx_for_lsp)) [e] in (* First col size = 15 + 1 + 2 + 3 + 5 + 6 * = 32 *) ===================================== src/dune ===================================== @@ -3,6 +3,6 @@ (name typerlib) (libraries zarith str linol linol-lwt - lsp jsonrpc yojson + lsp jsonrpc yojson base )) ===================================== src/elab.ml ===================================== @@ -187,6 +187,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = ~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) @@ -198,18 +199,18 @@ let elab_check_def (ctx : elab_context) var lxp ltype = elab_check_proper_type ctx ltype var else ( - if !Log.lsp_enabled then - 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 () + (*if !Log.lsp_enabled then*) + (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 = ===================================== src/lexp.ml ===================================== @@ -929,7 +929,7 @@ let rec get_precedence expr ctx = * ========================================== *) let rec lexp_print e = print_string (lexp_string e) -and lexp_string e = lexp_cstring (!debug_ppctx) e +and lexp_string e = lexp_cstring (if !Log.lsp_enabled then (!debug_ppctx) else (!debug_ppctx_for_lsp)) e (* Context Print *) and lexp_cprint ctx e = print_string (lexp_cstring ctx e) ===================================== src/log.ml ===================================== @@ -79,8 +79,8 @@ type log_config = { } let typer_log_config = { - level = Warning; - print_at_log = false; + level = Debug; + print_at_log = true; print_in_reverse = false; color = true; } @@ -189,8 +189,9 @@ let stop_compilation s = raise (Stop_Compilation s) let log_fatal ?section ?print_action ?loc m = typer_log_config.print_at_log <- true; + typer_log_config.level <- Debug; log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; - internal_error "Compiler Fatal Error" + internal_error (*"Compiler Fatal Error"*) m @@ -203,20 +204,16 @@ 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 = ===================================== src/opslexp.ml ===================================== @@ -583,18 +583,23 @@ and check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () - else (error_tc ~loc:(lexp_location e) - ("Type mismatch for " - ^ lexp_string e ^ " : " - ^ lexp_string t ^ " != " - ^ lexp_string t'); + else ( if !Log.lsp_enabled then + (error_tc ~loc:(lexp_location e) + ("Type mismatch for " + ^ lexp_string e ^ " : " + ^ lexp_string t ^ " != " + ^ lexp_string t')) + else (); (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in (match lexp'_whnf s ctx with | Sort _ -> () - | _ -> error_tc ~loc:(lexp_location t) - ("Not a proper type: " ^ lexp_string t)); + | _ -> if !Log.lsp_enabled then + error_tc ~loc:(lexp_location t) + ("Not a proper type: " ^ lexp_string t) + else () + ); (* FIXME: return the `sort` rather than the surrounding `lexp`! *) s in match lexp_lexp' e with @@ -602,7 +607,8 @@ and check'' erased ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) - -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; + -> ( if !Log.lsp_enabled then + error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -632,9 +638,10 @@ and check'' erased ctx e = (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) -> if DB.set_mem idx erased then - error_tc ~loc:l - ("Var `" ^ maybename name ^ "`" - ^ " can't be used here, because it's `erasable`"); + ( if !Log.lsp_enabled then + error_tc ~loc:l + ("Var `" ^ maybename name ^ "`" + ^ " can't be used here, because it's `erasable`")); lookup_type ctx v | Susp (e, s) -> check erased ctx (push_susp e s) | Let (l, defs, e) @@ -665,15 +672,18 @@ and check'' erased ctx e = match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | SortInvalid - -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; + -> if !Log.lsp_enabled then + error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; mkSort (l, StypeOmega) | SortK1NotType - -> (error_tc ~loc:(lexp_location t1) - "Not a proper type"; + -> ( if !Log.lsp_enabled then + error_tc ~loc:(lexp_location t1) + "Not a proper type"; mkSort (l, StypeOmega)) | SortK2NotType - -> (error_tc ~loc:(lexp_location t2) - "Not a proper type"; + -> ( if !Log.lsp_enabled then + error_tc ~loc:(lexp_location t2) + "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in @@ -690,12 +700,14 @@ and check'' erased ctx e = match lexp'_whnf ft ctx with | Arrow (ak', _v, t1, _l, t2) -> if not (ak == ak') then - (error_tc ~loc:(lexp_location arg) + ( if !Log.lsp_enabled then + error_tc ~loc:(lexp_location arg) "arg kind mismatch"; ()) else (); assert_type ctx arg at t1; mkSusp t2 (S.substitute arg) - | _ -> (error_tc ~loc:(lexp_location arg) + | _ -> ( if !Log.lsp_enabled then + error_tc ~loc:(lexp_location arg) ("Calling a non function (type = " ^ lexp_string ft ^ ")!"); ft)) @@ -722,14 +734,15 @@ and check'' erased ctx e = (* FIXME: If it does refer, * we get an ugly error! *) (mkSusp level' (L.sunshift n)) - | _tt -> error_tc ~loc:(lexp_location t) - ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline () - ) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string lwhnf ^")"); + | _tt -> if !Log.lsp_enabled then + (error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string lwhnf ^")")); level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, @@ -759,7 +772,8 @@ and check'' erased ctx e = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_error ~loc:(lexp_location ekind) + | _ -> if !Log.lsp_enabled then + Log.log_error ~loc:(lexp_location ekind) "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with @@ -771,7 +785,8 @@ and check'' erased ctx e = (* We don't check aarg's type, because we assume that `check` * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (error_tc ~loc:l + | _,_ -> ( if !Log.lsp_enabled then + error_tc ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = @@ -801,7 +816,8 @@ and check'' erased ctx e = (ssink vdef s) (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes - | _,_ -> (error_tc ~loc:l + | _,_ -> ( if !Log.lsp_enabled then + error_tc ~loc:l "Wrong number of args to constructor!"; (erased, ctx, hlxp)) in let hctor = @@ -819,7 +835,9 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 then - warning_tc ~loc:l "Redundant default clause"; + ( if !Log.lsp_enabled then + warning_tc ~loc:l "Redundant default clause" + else ()); let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -830,9 +848,18 @@ and check'' erased ctx e = (mkSusp ret (S.shift 2)) | None -> if diff > 0 then - error_tc ~loc:l ("Non-exhaustive match: " - ^ string_of_int diff ^ " cases missing")) - | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); + ( + if !Log.lsp_enabled then + (error_tc ~loc:l ("Non-exhaustive match: " + ^ string_of_int diff ^ " cases missing") + ) + else () + ) + ) + | _,_ -> if !Log.lsp_enabled then + error_tc ~loc:l "Case on a non-inductive type!" + else () + ); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -860,10 +887,12 @@ and check'' erased ctx e = buildtype fargs) in buildtype fargs with Not_found - -> (error_tc ~loc:l + -> ( if !Log.lsp_enabled then + error_tc ~loc:l ("Constructor \"" ^ name ^ "\" does not exist"); DB.type_int)) - | _ -> (error_tc ~loc:(lexp_location e) + | _ -> ( if !Log.lsp_enabled then + error_tc ~loc:(lexp_location e) ("Cons of a non-inductive type: " ^ lexp_string t); DB.type_int)) ===================================== src/typer_lsp_server.ml ===================================== @@ -39,8 +39,8 @@ open Log open Util -type state_after_processing = (log_entry list * - ((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) +type state_after_processing = (log_entry list * + (((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) option) ) let log_entry_to_list (tab:log_entry list) : ((string * int * int * int * int) * log_level * string) list = List.map (fun x -> let location = Option.get x.loc in @@ -105,10 +105,18 @@ let readstring (str:string) = Log.clear_log () ; let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) - let ast = Elab.lexp_decl_str str ectx in - (!Log.typer_log, ast) + let oast = + try + Some (Elab.lexp_decl_str str ectx) + with + | Log.Stop_Compilation msg + | Log.Internal_error msg + | Log.User_error msg -> None + in + (!Log.typer_log, oast) let process_some_input_file (_file_contents : string) : state_after_processing = + Logs.err (fun k->k " %s" @@ "TEST TEST TEST"); readstring _file_contents let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = @@ -131,30 +139,118 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list diagnostic ) log_tab - (*little method to test completion*) - let little_fonc el = - match el with - | "lambda" -> "lambda (pattern) -> pattern ;" - | "case" -> "case scrutinee \n | pattern -> pattern ;" - | "let" -> "let_in_ (_=_ x ()) x ;" - | "if" -> " if_then_else_ x \"x is true\" \"x is false\"" - | _ -> "" - - let little_kind el = - match el with - | "lambda" -> Lsp.Types.CompletionItemKind.Text - | "case" -> Lsp.Types.CompletionItemKind.Function - | "let" -> Lsp.Types.CompletionItemKind.Text - | "if" -> Lsp.Types.CompletionItemKind.Text - | _ -> Lsp.Types.CompletionItemKind.Text - - let little_detail el = - match el with - | "lambda" -> "define a function" - | "case" -> "pattern matching" - | "let" -> "let...in" - | "if" -> "if...condition" - | _ -> "" +(*==============completion============================*) + +module Compl = struct + + type k = Text | Method | Function | Constructor + | Field | Variable | Class | Interface + | Module | Property | Unit | Value + | Enum | Keyword | Snippet | Color + | File | Reference | Folder | EnumMember + | Constant | Struct | Event | Operator + | TypeParameter + + type t = { + label:string; + newText:string;(*the text the completion will send*) + detail:string; + kind:k + } + + + let t_from_tuple (tup : (string * string * string * k) list) : t list = + List.map (fun x + -> let (label,newText,detail,kind) = x in + let ret = { + label = label ; + newText = newText ; + detail = detail ; + kind = kind + } in + ret + ) tup + + let exemple_liste = [ + ("lambda", "lambda (pattern) -> pattern ", "define a function", Text); + ("case", "case scrutinee \n | pattern -> pattern ", "pattern matching", Function); + ("let", "let_in_ (_=_ x ()) x ", "let...in", Text); + ("if", " if_then_else_ x \"x is true\" \"x is false\"", "if...condition", Text); + ("add", "add()", "add a element to a list", Method); + ] + + let createKind (element:t) = + match element.kind with + | Text -> Lsp.Types.CompletionItemKind.Text + | Method -> Lsp.Types.CompletionItemKind.Method + | Function -> Lsp.Types.CompletionItemKind.Function + | Constructor -> Lsp.Types.CompletionItemKind.Constructor + | Field -> Lsp.Types.CompletionItemKind.Field + | Variable -> Lsp.Types.CompletionItemKind.Variable + | Class -> Lsp.Types.CompletionItemKind.Class + | Interface -> Lsp.Types.CompletionItemKind.Interface + | Module -> Lsp.Types.CompletionItemKind.Module + | Property -> Lsp.Types.CompletionItemKind.Property + | Unit -> Lsp.Types.CompletionItemKind.Unit + | Value -> Lsp.Types.CompletionItemKind.Value + | Enum -> Lsp.Types.CompletionItemKind.Enum + | Keyword -> Lsp.Types.CompletionItemKind.Keyword + | Snippet -> Lsp.Types.CompletionItemKind.Snippet + | Color -> Lsp.Types.CompletionItemKind.Color + | File -> Lsp.Types.CompletionItemKind.File + | Reference -> Lsp.Types.CompletionItemKind.Reference + | Folder -> Lsp.Types.CompletionItemKind.Folder + | EnumMember -> Lsp.Types.CompletionItemKind.EnumMember + | Constant -> Lsp.Types.CompletionItemKind.Constant + | Struct -> Lsp.Types.CompletionItemKind.Struct + | Event -> Lsp.Types.CompletionItemKind.Event + | Operator -> Lsp.Types.CompletionItemKind.Operator + | TypeParameter -> Lsp.Types.CompletionItemKind.TypeParameter + + let tranform_string (content:string) : (string * int * int) list = + Base.String.split content ~on:'\n' |> + Base.List.mapi ~f:(fun line data -> + Base.String.split data ~on:' ' |> + Base.List.fold_map ~init:1 ~f:(fun pos word -> + let pos = pos + String.length word in + pos+1, (word,line+1,pos-1)) |> + Base.snd) |> + List.concat + + let list_filter_by_line (liste: (string * int * int) list) (line:int) : (string * int * int) list = + List.filter (fun (word,w_line,w_column) -> w_line == line) liste + + let list_filter_by_character (liste: (string * int * int) list) (pos:int * int) : string = + let (word,_,_) = + List.find (fun (word,w_line,w_column) -> + let (cursor_line,cursor_column) = pos in + w_line == cursor_line && w_column == cursor_column + ) + liste + in + word + + let match_str (str:string) : Str.regexp = + str + |> Str.quote + |> Str.regexp + + + let complete (str:string) (liste: t list) = + match str with + | "List." -> List.filter (fun x -> + String.equal x.label "add" + ) + liste + | str -> List.filter (fun x -> + let reg = match_str str in + Str.string_match reg x.label 0 + ) + liste + + end + +(*==============completion============================*) (*====================================Lexp parcourir===================================*) @@ -264,8 +360,14 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | Call (f, args) -> ( let fonc = browse_lexp ctx f cursor in - let args_list = List.map (fun (_ , e) -> browse_lexp ctx e cursor) args in + let args_list = List.map + (fun (_ , e) -> browse_lexp ctx e cursor) + args + in + + try browse_list_lexp (fonc::args_list) cursor + with exe -> failwith "Exeption sur ce call !!!" ) | Inductive (l, _label, args, cases) @@ -282,7 +384,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list ((let lwhnf = Opslexp.lexp_whnf t ictx in match Lexp.lexp_lexp' lwhnf with | Sort (_, Stype _) - when ak == Pexp.Aerasable (*&& impredicative_erase*) + when ak == Pexp.Aerasable -> level | Sort (_, Stype level') -> Opslexp.mkSLlub ctx level @@ -501,7 +603,7 @@ class lsp_server = match Hashtbl.find buffers uri with | state_after_processing -> let (_,ast) = state_after_processing in - let (list_list, _) = ast in + let (list_list, _) = Option.get ast in let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in let typer_loc = typer_pos_of_lsp_pos pos in @@ -519,7 +621,7 @@ class lsp_server = match Hashtbl.find buffers uri with | state_after_processing -> let (_,ast) = state_after_processing in - let (list_list, _) = ast in + let (list_list, _) = Option.get ast in let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in let typer_loc = typer_pos_of_lsp_pos pos in @@ -534,7 +636,7 @@ class lsp_server = in let e = Some r in let f = Linol_lwt.return e in f - + method! config_hover = Some (`Bool true) method! config_definition = Some (`Bool true) @@ -565,23 +667,26 @@ class lsp_server = method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with - | state_after_processing -> (*let (log_list,ast) = state_after_processing in - let (list_list, ectx) = ast in*) - let tab = ["lambda";"case";"let";"if"] in + | state_after_processing -> let trans_string = Compl.tranform_string doc_state.content in + let fbyline = Compl.list_filter_by_line trans_string (pos.line + 1) in + let word = Compl.list_filter_by_character fbyline ((pos.line + 1),pos.character) in let typer_loc = typer_pos_of_lsp_pos pos in let range = lsp_range_of_loc typer_loc in - let r = List.map (fun x -> - let label = x in - let textEdit = `TextEdit (Lsp.Types.TextEdit.create ~range:range ~newText:(little_fonc x)) in - let kind = little_kind x in - let detail = little_detail x in - let ci = Lsp.Types.CompletionItem.create - ~label:label ~kind:kind - ~textEdit:textEdit ~detail:detail () - in - ci - - ) tab in + + let tab_compl = Compl.complete word (Compl.t_from_tuple Compl.exemple_liste) in + + let r = List.map (fun (x:Compl.t) -> + let label = x.label in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(x.newText) in + let kind = Compl.createKind x in + let detail = x.detail in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:detail () + in + ci + ) tab_compl in + let e = Some (`List r) in let f = Linol_lwt.return e in f @@ -592,6 +697,7 @@ end and runs it as a task. *) let run () = ignore (Arg.Set Log.lsp_enabled); + Logs.set_level ~all:true (Some Logs.Debug); let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in ===================================== typer.ml ===================================== @@ -30,9 +30,12 @@ let welcome_msg = let arg_batch = ref false -(*booléen utilisé pour démarrer le serveur. - je l'ai mis true pour les tests +(* +booléen utilisé pour démarrer le serveur. +mis true pour les tests *) + + let lsp_server = ref true let arg_files = ref [] View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a1a11af523dcfe97f455c4ccc3736279… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a1a11af523dcfe97f455c4ccc3736279… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch lexer-with-source
by Simon Génier (＠ilovemonoids) 09 Jui '21

09 Jui '21

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

1 0

[Git][monnier/typer][master] 2 commits: Rewrite the Lexer module in terms of source objects.
by Simon Génier (＠ilovemonoids) 09 Jui '21

09 Jui '21

Simon Génier pushed to branch master at Stefan / Typer Commits: f289b62a by Simon Génier at 2021-05-29T12:12:42-04:00 Rewrite the Lexer module in terms of source objects. This might not look useful, but it will simplify a great deal our next change of add and end point to location records since all the location related code will be in there source objects. I ended up rewriting most of the Lexer. I tried to avoid doing that, but the offset handling code was so mixed up with the rest than that turned out to give worse code and a diff as unreadable. I'm pretty confident that that the changes are OK since we are still able to load pervasives.typer and I wrote a few tests for the trickier inner operators. - - - - - 8d9a2367 by Simon Génier at 2021-06-09T12:28:31-04:00 Merge branch 'lexer-with-source' - - - - - 3 changed files: - src/lexer.ml - src/option.ml - src/source.ml Changes: ===================================== src/lexer.ml ===================================== @@ -27,16 +27,6 @@ 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' - -type num_part = | NPint | NPfrac | NPexp - let unescape str = let rec split b = if b >= String.length str then [] @@ -45,108 +35,198 @@ let unescape str = string_sub str b e :: split (e + 1) in String.concat "" (split 0) -let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos - (* The returned Sexp may not be a Node. *) - : sexp * pretoken list * bytepos * charpos = - match pts with - | [] -> (Log.internal_error "No next token!") - | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0) - | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0) - | (Pretoken ({file;line;column;docstr}, name) :: pts') - -> let char = name.[bpos] in - if digit_p char - || (char = '-' (* FIXME: Handle '+' as well! *) - && bpos + 1 < String.length name - && digit_p (name.[bpos + 1])) then - let rec lexnum bp cp (np : num_part) = - if bp >= String.length name then - ((if np == NPint then - Integer ({file;line;column=column+cpos;docstr=docstr}, - Z.of_string (string_sub name bpos bp)) - else - Float ({file;line;column=column+cpos;docstr=docstr}, - float_of_string (string_sub name bpos bp))), - pts', 0, 0) - else - match name.[bp] with - | ('0'|'1'|'2'|'3'|'4'|'5'|'6'|'7'|'8'|'9') - -> lexnum (bp+1) (cp+1) np - | '.' when np == NPint -> lexnum (bp+1) (cp+1) NPfrac - | ('e'|'E') when not (np == NPexp) -> lexnum (bp+1) (cp+1) NPexp - | ('+'|'-') - when np == NPexp && (name.[bp-1] == 'e' || name.[bp-1] == 'E') - -> lexnum (bp+1) (cp+1) NPexp - | _ - -> ((if np == NPint then - Integer ({file;line;column=column+cpos;docstr=docstr}, - Z.of_string (string_sub name bpos bp)) - else - Float ({file;line;column=column+cpos;docstr=docstr}, - float_of_string (string_sub name bpos bp))), - pts, bp, cp) - in lexnum (bpos+1) (cpos+1) NPint - else if bpos + 1 >= String.length name then - (hSymbol ({file;line;column=column+cpos;docstr=docstr}, - string_sub name bpos (String.length name)), - pts', 0, 0) - else if stt.(Char.code name.[bpos]) = CKseparate then - (hSymbol ({file;line;column=column+cpos;docstr=docstr}, - string_sub name bpos (bpos + 1)), - pts, bpos+1, cpos+1) - else - let rec lexsym bpos cpos = - let mksym epos escaped - = if epos = bpos then epsilon {file;line;column=column+cpos;docstr=docstr} else - let rawstr = string_sub name bpos epos in - let str = if escaped then unescape rawstr else rawstr in - hSymbol ({file;line;column=column+cpos;docstr=docstr}, str) in - let rec lexsym' prec lf bp cp escaped = - if bp >= String.length name then - (lf (mksym (String.length name) escaped), pts', 0, 0) - else - let char = name.[bp] in - let bp' = bp + 1 in - let is_last = bp' >= String.length name in - match stt.(Char.code char) with - | _ when char == '\\' && not is_last - (* Skip next char, in case it's a special token. *) - (* For utf-8, this cp+2 is risky but actually works: \ counts - * as 1 and if the input is valid utf-8 the next byte has to - * be a leading byte, so it has to count as 1 as well ;-) *) - -> lexsym' prec lf (bp+2) (cp+2) true - | CKseparate -> (lf (mksym bp escaped), pts, bp, cp) - (* Turn `inner` infix operators, such as the "." of - * "Module.elem" into the equivalent of (__.__ Module elem). *) - | CKinner prec' - (* To be considered `inner`, an operator char needs to have - * something on its LHS or its RHS, otherwise, treat it as - * a normal char, `.` can be a normal operator as well. *) - when bpos != bp - || (not is_last - && CKseparate != (stt.(Char.code name.[bp']))) - || not (lf dummy_epsilon = dummy_epsilon) - -> let left = mksym bp escaped in - let op = hSymbol ({file;line;column=column+cp;docstr=docstr}, - "__" ^ String.sub name bp 1 ^ "__") in - let bpos = bp' in - let cpos = inc_cp cp char in - let lf' = if prec' > prec then - (fun s -> lf (Node (op, [left; s]))) - else - (fun s -> Node (op, [lf left; s])) in - lexsym bpos cpos prec' lf' - bpos cpos false - | _ -> lexsym' prec lf (bp+1) (inc_cp cp char) escaped - in lexsym' - in lexsym bpos cpos 0 (fun s -> s) bpos cpos false - -let lex tenv (pts : pretoken list) : sexp list = - let rec gettokens pts bpos cpos acc = - match pts with +let lex_number + (source : #Source.t) + (start_location : Source.Location.t) + (start_offset : int) + : sexp = + + let rec lex_exponent () = + match source#peek_char with + | Some ('0' .. '9') + -> source#advance; + lex_exponent () + + | _ + -> let source = source#slice_from_offset start_offset in + Float (start_location, float_of_string source) + in + + let lex_exponent_sign () = + match source#peek_char with + | Some ('0' .. '9' | '+' | '-') + -> source#advance; + lex_exponent () + + (* TODO: error if there are no signs or digits after the 'e'? *) + | _ + -> let source = source#slice_from_offset start_offset in + Float (start_location, float_of_string source) + in + + let rec lex_fractional () = + match source#peek_char with + | Some ('0' .. '9') + -> source#advance; + lex_fractional () + + | Some ('e' | 'E') + -> source#advance; + lex_exponent_sign () + + | _ + -> let source = source#slice_from_offset start_offset in + Float (start_location, float_of_string source) + in + + let rec lex_integer () = + match source#peek_char with + | Some ('0' .. '9') + -> source#advance; + lex_integer () + + | Some ('.') + -> source#advance; + lex_fractional () + + | Some ('e' | 'E') + -> source#advance; + lex_exponent_sign () + + | _ + -> let source = source#slice_from_offset start_offset in + Integer (start_location, Z.of_string source) + in + + lex_integer () + +(* Splits one symbol from the beginning of the source. *) +let lex_symbol + (token_env : token_env) + (source : #Source.t) + (doc : string) + (start_location : Source.Location.t) + (start_offset : int) + : sexp = + + let mksym start_location start_offset escaped = + if Int.equal start_offset source#current_offset + then epsilon start_location + else + let raw_name = source#slice_from_offset start_offset in + let name = if escaped then unescape raw_name else raw_name in + hSymbol (start_location, name) + in + + let rec loop start_location start_offset prec lf (escaped : bool) = + match source#peek_char with + | None + -> lf (mksym start_location start_offset escaped) + + | Some c + -> (match token_env.(Char.code c) with + | CKseparate + -> lf (mksym start_location start_offset escaped) + + | CKinner prec' + -> let left = mksym start_location start_offset escaped in + let op_location = source#current_location doc in + + (* To be considered `inner`, an operator char needs to have + something on its LHS or its RHS, otherwise, treat it as a + normal char. `.` can be the normal function composition + operator as well. *) + let lhs_p = start_offset != source#current_offset in + source#advance; + let rhs_p = + (match source#peek_char with + | None -> false + | Some c' -> CKseparate != token_env.(Char.code c')) + in + if lhs_p || rhs_p || lf dummy_epsilon <> dummy_epsilon + then + let op = hSymbol (op_location, Printf.sprintf "__%c__" c) in + let lf' = + if prec' > prec + then fun s -> lf (Node (op, [left; s])) + else fun s -> Node (op, [lf left; s]) + in + loop (source#current_location doc) source#current_offset prec' lf' false + else + loop start_location start_offset prec lf escaped + + | CKnormal + -> (source#advance; + let is_last = Option.is_none source#peek_char in + match c with + (* Skip next char, in case it's a special token. For utf-8, + simply advancing is risky but actually works: '\' counts as 1 + and if the input is valid utf-8 the next byte has to be a + leading byte, so it has to count as 1 as well ;-) *) + | '\\' when not is_last + -> source#advance; + loop start_location start_offset prec lf true + + | _ -> loop start_location start_offset prec lf escaped)) + in + loop start_location start_offset 0 (fun s -> s) false + +let split_presymbol + (token_env : token_env) + (source : #Source.t) + (doc : string) + : sexp list = + + let rec loop (acc : sexp list) : sexp list = + match source#peek_char with + | None -> List.rev acc + | Some (c) + -> let start_offset = source#current_offset in + let start_location = source#current_location doc in + let token = + match c with + (* A negative number literal, or a symbol starting with '-'. *) + | '-' + -> (source#advance; + match source#peek_char with + | Some ('0' .. '9') + -> lex_number source start_location start_offset + | _ + -> lex_symbol token_env source doc start_location start_offset) + + | '0' .. '9' + -> (source#advance; + lex_number source start_location start_offset) + + | _ when token_env.(Char.code c) = CKseparate + -> source#advance; + let name = source#slice_from_offset start_offset in + hSymbol (start_location, name) + + | _ + -> lex_symbol token_env source doc start_location start_offset + in + loop (token :: acc) + in + loop [] + +let lex (token_env : token_env) (pretokens : pretoken list) : sexp list = + let rec loop pretokens acc = + match pretokens with | [] -> List.rev acc - | _ -> let (tok, pts, bpos, cpos) = nexttoken tenv pts bpos cpos - in gettokens pts bpos cpos (tok :: acc) in - gettokens pts 0 0 [] + + | Preblock (start_location, block_pretokens, end_location) :: pretokens' + -> loop pretokens' (Block (start_location, block_pretokens, end_location) :: acc) + + | Prestring (location, text) :: pretokens' + -> loop pretokens' (String (location, text) :: acc) + + | Pretoken ({file; line; column; docstr}, name) :: pretokens' + -> let source = new Source.source_string ~file ~line ~column name in + let tokens = split_presymbol token_env source docstr in + loop pretokens' (List.rev_append tokens acc) + in + loop pretokens [] let lex_source (source : #Source.t) tenv = let pretoks = prelex source in @@ -155,4 +235,3 @@ let lex_source (source : #Source.t) tenv = let sexp_parse_source (source : #Source.t) tenv grm limit = let toks = lex_source source tenv in sexp_parse_all_to_list grm toks limit - ===================================== src/option.ml ===================================== @@ -40,3 +40,8 @@ let is_some (o : 'a option) : bool = match o with | Some _ -> true | None -> false + +let is_none (o : 'a option) : bool = + match o with + | Some _ -> false + | None -> true ===================================== src/source.ml ===================================== @@ -131,13 +131,13 @@ class source_file file_name = object (self) end class source_string - ?(base_line : int = first_line_of_file) - ?(base_column : int = first_column_of_line) - ?(file_name : string = "<string>") + ?(file : string = "<string>") + ?(line : int = first_line_of_file) + ?(column : int = first_column_of_line) source = object - inherit t base_line base_column file_name + inherit t line column file val mutable offset = 0 View it on GitLab: https://gitlab.com/monnier/typer/-/compare/b8d1df5b6886203e354594b2096aec7b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/b8d1df5b6886203e354594b2096aec7b… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch type-macro-improvements
by Jean-Alexandre Barszcz (＠jabarszcz) 07 Jui '21

07 Jui '21

Jean-Alexandre Barszcz deleted branch type-macro-improvements at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 3 commits: Fix nix shell and dune details
by Jean-Alexandre Barszcz (＠jabarszcz) 07 Jui '21

07 Jui '21

Jean-Alexandre Barszcz pushed to branch master 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/c5ef2f59f36e51ab6c709193a01bb355… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/c5ef2f59f36e51ab6c709193a01bb355… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch instance-args
by Jean-Alexandre Barszcz (＠jabarszcz) 01 Jui '21

01 Jui '21

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

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Juin 2021