Typer Août 2021

typer@iro.umontreal.ca

2 participants
6 discussions

[Git][monnier/typer][soilih] completion from buffer
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 17 Aoû '21

17 Aoû '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 98548aee by Soilih BEN SOILIH at 2021-08-17T23:00:07-06:00 completion from buffer - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -177,7 +177,7 @@ module Compl = struct label = label ; newText = newText ; detail = detail ; - kind = kind + kind = kind } in ret ) tup @@ -300,11 +300,11 @@ module Compl = struct Str.string_match reg x.label 0 ) liste - | _ -> List.filter (fun x -> - let reg = match_str str in - Str.string_match reg x.label 0 - ) - liste + | _ -> List.filter (fun x -> + let reg = match_str str in + Str.string_match reg x.label 0 + ) + liste end (*==============completion============================*) @@ -446,8 +446,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | Arrow (ak, v, t1, l, t2) -> ( + + let (_,_,k1,_) = browse_lexp ctx t1 cursor in let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in - match Opslexp.sort_compose ctx nctx l ak t1 t2 with + let (_,_,k2,_) = browse_lexp nctx t2 cursor in + match Opslexp.sort_compose ctx nctx l ak k1 k2 with | SortResult k -> (nctx, None, k, location) | SortInvalid -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) @@ -459,7 +462,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | 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 c = (ctx,None,t,l) in + let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,e),l) in browse_list_lexp ([a;b;c]) cursor | Call (f, args) @@ -718,6 +721,57 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte (*====================================Definition===================================*) +(*====================================Compl===================================*) + +let find_compl_location (*(ctx:Debruijn.lexp_context)*) (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Lsp.Types.CompletionItem.t list = + + let (_,vr,_,loc) = ret in + + match vr with + | None -> [] + | Some v -> let ((_,c),_) = v in + let cp = Option.get c in + let label = cp in + let range = Compl.lsp_range_of_a_tuple + (loc.start_line,(loc.end_column - String.length cp)) + (loc.end_line, loc.end_column) + in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:cp in + let kind = Lsp.Types.CompletionItemKind.Text in + let detail = "detail " ^ cp in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:detail () + in + [ci] + + let trans_listlist_l (ctx:Debruijn.lexp_context) (list_list:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let lst = update_the_context ctx list_list in + let nlst = List.map ( fun x -> + let (lctx,liste) = x in + let (_,lxp,_) = List.nth liste 0 in + browse_lexp lctx lxp cursor + ) lst in + List.filter (fun x -> + let (_,v,_,_) = x in + match v with + | None -> false + | Some v -> true + ) nlst + + + let complete_oth (str:string) (liste: (Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) list) = + match str with + | str -> List.filter (fun x -> + let (_,v,_,_) = x in + let ((_,s),_) = Option.get v in + let reg = Compl.match_str str in + Str.string_match reg (Option.get s) 0 + ) + liste + +(*====================================Compl===================================*) + (* Lsp server class This is the main point of interaction beetween the code checking documents @@ -803,7 +857,7 @@ class lsp_server = let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (lctx,lexp) = lexp_search ctx list_list typer_loc in - let (l_ctx,_, l_type,location) = browse_lexp lctx lexp typer_loc in + let (l_ctx,_,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 @@ -843,22 +897,43 @@ 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 trans_string = Compl.tranform_string doc_state.content in + | state_after_processing -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = typer_pos_of_lsp_pos pos in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let rlst = trans_listlist_l ctx list_list typer_loc in + 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.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in - let typer_loc = typer_pos_of_lsp_pos pos in - let path = "/home/soilih/Bureau/test/compl.txt" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 path in - let c = "-----------------\n mot:" ^ word ^ "\n-------------\n" in - - output_string oc (c); - close_out oc; - let range = Compl.lsp_range_of_a_tuple (typer_loc.start_line,(typer_loc.end_column - String.length word)) (typer_loc.end_line, typer_loc.end_column) in + let tab_comp = complete_oth word rlst in + let r = List.map ( fun x -> + let (_,v,_,_) = x in + let ((_,s),_) = Option.get v in + let st = Option.get s in + let label = st in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(st) in + let kind = Lsp.Types.CompletionItemKind.Text in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:st () + in + ci + ) tab_comp in + (* + let path = "/home/soilih/Bureau/test/compl.txt" in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 path in + let c = "-----------------\n mot:" ^ word ^ "\n-------------\n" in + output_string oc (c); + close_out oc; + *) + + + (* let tab_compl = Compl.complete word (Compl.t_from_tuple Compl.exemple_liste) in @@ -874,7 +949,7 @@ class lsp_server = ci ) tab_compl in - + *) let e = Some (`List r) in let f = Linol_lwt.return e in f @@ -909,10 +984,11 @@ let sep name s = output_string oc content; close_out oc + let test () = let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let name = "/home/soilih/Bureau/test/test.txt" in - (*sep name "INT"; + sep name "INT"; hoverTest ctx name "e = 12 ;" (1,1) "##Int"; hoverTest ctx name "e = 12 ;" (1,5) "##Int"; sep name "STRING"; @@ -953,7 +1029,7 @@ let test () = hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "##Type"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (a -> ((List ℓ a) -> (List ℓ a)))"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12) "##Int"; - hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)";*) + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)"; sep name "ARROW"; hoverTest ctx name "type Floo = bar Int Int ;" (1,1) ""; hoverTest ctx name "type Floo = bar Int Int ;" (1,7) ""; @@ -966,7 +1042,7 @@ let test () = hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,10) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,17) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,29) ""; - hoverTest ctx name "v = Int -> Int ;" (1,1) ""(*; + hoverTest ctx name "v = Int -> Int ;" (1,1) ""; sep name "INDUCTIVE"; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1) ""; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10) ""; @@ -1002,7 +1078,7 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (3,4) ""; hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (3,13) ""; hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,4) ""; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,14) ""*) + hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,14) "" (*=======================================Test======================================*) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/98548aee56fe1da1ddfe7fb0f815fa6f6… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/98548aee56fe1da1ddfe7fb0f815fa6f6… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/elab.ml (elaborate): `check_inferred` when a type is given.
by Stefan (＠monnier) 17 Aoû '21

17 Aoû '21

Stefan pushed to branch master at Stefan / Typer Commits: a7ac505a by Jean-Alexandre Barszcz at 2021-08-10T14:58:56-04:00 * src/elab.ml (elaborate): `check_inferred` when a type is given. Previously, `check_inferred` was mainly called from `check`, but some calls to `elaborate` play the same role as `check` (if an expected type is given), so we move this logic to `elaborate`. This allows implicit arguments to be instantiated in more places. For example, calls and variables are always inferred, but without `check_inferred`, the type provided to `elaborate` would be ignored. - - - - - 2 changed files: - src/elab.ml - tests/elab_test.ml Changes: ===================================== src/elab.ml ===================================== @@ -543,7 +543,7 @@ let elab_p_id ((l,name) : symbol) : vname = (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = - match se with + let (e, res_t) = match se with (* Rewrite SYM to `typer-identifier SYM`. *) | Symbol ((loc, name) as id) -> if not (name = "typer-identifier") then @@ -572,7 +572,17 @@ let rec elaborate ctx se ot = * Maybe I should only elaborate `func` above if it's a symbol * (and maybe even use `elab_varref` rather than indirecting * through `typer-identifier`)? *) - elab_call ctx ft args + elab_call ctx ft args in + match ot with + | Some t -> + (match res_t with + | Checked -> (e, res_t) + | _ -> let inferred_t = + match res_t with + | Inferred t -> t + | _ -> OL.get_type (ectx_to_lctx ctx) e in + (check_inferred ctx e inferred_t t, Checked)) + | _ -> (e, res_t) and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with @@ -663,12 +673,7 @@ and unify_with_arrow ctx tloc lxp kind var aty | [] -> arg, body and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = - let (e, ot) = elaborate ctx p (Some t) in - match ot with - | Checked -> e - | _ -> let inferred_t = match ot with Inferred t -> t - | _ -> OL.get_type (ectx_to_lctx ctx) e in - check_inferred ctx e inferred_t t + fst (elaborate ctx p (Some t)) and unify_or_error lctx lxp ?lxp_name expect actual = match Unif.unify expect actual lctx with ===================================== tests/elab_test.ml ===================================== @@ -231,4 +231,11 @@ type Lift (l ::: TypeLevel) (t :: Type_ l) (x : t) | mkLift; |} +let _ = add_elab_test_decl + "Check and instantiate implicit args when a type is given" + {| +test : Int -> ?a -> ?a; +test _ = I; + |} + let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a7ac505a8249a889aa1235f6823b1c707… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a7ac505a8249a889aa1235f6823b1c707… You're receiving this email because of your account on gitlab.com.

1 0

Bootstrap
by Stefan Monnier 16 Aoû '21

16 Aoû '21

Bonjour Soilihi et les autres, On parlait du problème du bootstrap d'un langage, dans le contexte de réécrire Typer en Typer. Voici le lien auquel je pensais: http://www.joyofsource.com/guix-reduces-bootstrap-seed-by-50.html En chemin je t'avais dis que le terme de "bootstrap" était une référence à certaines aventures du baron de Münchhausen (https://fr.wikipedia.org/wiki/Baron_de_M%C3%BCnchhausen), mais il semble que c'est pas si clair que ça: http://archive.boston.com/bostonglobe/ideas/theword/2009/01/bootstraps_and.… Voir aussi bien sûr https://en.wikipedia.org/wiki/Bootstrapping_(compilers) Stefan

1 0

[Git][monnier/typer][soilih] fixing context errors
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 15 Aoû '21

15 Aoû '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 31c030ee by Soilih BEN SOILIH at 2021-08-15T23:03:03-06:00 fixing context errors - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -313,7 +313,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp let rec foo (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp * Lexp.ltype) list list ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = match liste with - | [] -> failwith "No context to extend !!!" + | [] -> list_ret | hd::tl -> let lctx = Debruijn.lctx_extend_rec ctx hd in let elt = (lctx,hd) in foo lctx tl (elt::list_ret) @@ -438,9 +438,9 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp defs in - let lt = (ctx,None, Lexp.mkSusp (Opslexp.get_type ctx e) (Opslexp.lexp_defs_subst l Subst.identity defs),l) in + (*let lt = (ctx,None, Lexp.mkSusp (Opslexp.get_type ctx e) (Opslexp.lexp_defs_subst l Subst.identity defs),l) in*) - browse_list_lexp ((browse_lexp ctx' e cursor)::lt::tab) cursor + browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor @@ -459,7 +459,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | 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 c = (ctx,None,(Opslexp.get_type ctx e),l) in + let c = (ctx,None,t,l) in browse_list_lexp ([a;b;c]) cursor | Call (f, args) @@ -712,7 +712,8 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte match vr with | None -> loc | Some v -> let ((l,_),_,_) = Debruijn.lctx_lookup ctx v in - l + + {l with start_line = (l.start_line - 1); end_line = (l.end_line - 1)} (*====================================Definition===================================*) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/31c030ee1a6cddfaa2f8901b3467e0b9f… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/31c030ee1a6cddfaa2f8901b3467e0b9f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] fixing context
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 13 Aoû '21

13 Aoû '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 1d141dbd by Soilih BEN SOILIH at 2021-08-13T10:57:54-06:00 fixing context - - - - - 2 changed files: - src/elab.ml - src/typer_lsp_server.ml Changes: ===================================== src/elab.ml ===================================== @@ -1146,8 +1146,8 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return a IO sexp")) | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return an IO") - with _e -> - fatal ~loc ("Macro `" ^ mname ^ "` not found") + with _e -> Sexp.dummy_epsilon + (*fatal ~loc ("Macro `" ^ mname ^ "` not found")*) (* Elaborate a bunch of mutually-recursive definitions. * FIXME: Currently, we never apply generalization to recursive definitions, ===================================== src/typer_lsp_server.ml ===================================== @@ -240,7 +240,28 @@ module Compl = struct ) liste in - word + word + + let dist_compl (loc1:string * int * int) (loc2:int * int) = + let (_,loc1_sl,loc1_sc) = loc1 in + let (loc2_sl,loc2_sc) = loc2 in + int_of_float ( + sqrt ( + (((float_of_int (loc1_sl)) -. (float_of_int (loc2_sl))) ** 2.0 ) + +. (((float_of_int (loc1_sc)) -. (float_of_int (loc2_sc))) ** 2.0 ) + ) + ) + + let rec find_the_nearest_compl (liste:(string * int * int) list) (pos:int * int) : string = + + match liste with + | [] -> failwith "No Completion found!!!" + | [n] -> let (w,_,_) = n in w + | [hd;tl] -> if ((dist_compl hd pos) < (dist_compl tl pos)) then let (w,_,_) = hd in w + else let (w,_,_) = tl in w + |hd::ml::tl -> if ((dist_compl hd pos) < (dist_compl ml pos)) then (find_the_nearest_compl (hd::tl) pos) + else find_the_nearest_compl (ml::tl) pos + let match_str (str:string) : Str.regexp = str @@ -249,6 +270,7 @@ 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 @@ -262,11 +284,43 @@ module Compl = struct Str.string_match reg x.label 0 ) liste - + *) + let splt = String.split_on_char '.' str in + + match splt with + + | [] -> liste + | [n] -> List.filter (fun x -> + let reg = match_str n in + Str.string_match reg x.label 0 + ) + liste + | [hd;tl] when (hd == "List") -> List.filter (fun x -> + let reg = match_str tl in + Str.string_match reg x.label 0 + ) + liste + | _ -> List.filter (fun x -> + let reg = match_str str in + Str.string_match reg x.label 0 + ) + liste end (*==============completion============================*) +let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp * Lexp.ltype) list list ) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list = + + let rec foo (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp * Lexp.ltype) list list ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = + match liste with + | [] -> failwith "No context to extend !!!" + | hd::tl -> let lctx = Debruijn.lctx_extend_rec ctx hd in + let elt = (lctx,hd) in + foo lctx tl (elt::list_ret) + in + foo (ctx: Debruijn.lexp_context) liste [] + + (*====================================Lexp parcourir===================================*) (* find the nearest lexp using Euclidean distance @@ -280,18 +334,53 @@ end ) ) - 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 "No Lexp found!!!" - | [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 lexp_list cursor + let pos_in_lexp_interval (ctx: Debruijn.lexp_context) (lst: (vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + + let lstr = update_the_context ctx lst in + + let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : Debruijn.lexp_context * Lexp.lexp = + match ls with + | [] -> failwith "No Lexp found!" + | hd::tl -> let (lctx_hd, hdl) = hd in + let (_,lxp,_) = List.nth hdl 0 in + let location = Lexp.lexp_location lxp in + if ((location.start_line <= cursor.start_line && location.start_column <= cursor.start_column) + && + (location.end_line >= cursor.end_line && location.end_column >= cursor.end_column)) + then (lctx_hd,lxp) + else foo tl cursor + in foo lstr cursor + + let find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + + let lstr = update_the_context ctx lst in + + let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : Debruijn.lexp_context * Lexp.lexp = + + match ls with + | [] -> failwith "No Lexp found!" + | [n] -> let (lctx,l) = n in + let (_,lxp,_) = List.nth l 0 in + (lctx,lxp) + | [hd;tl] -> let (lctx_hd,hdl) = hd in + let (lctx_tl,tll) = tl in + let (_,lxp,_) = List.nth hdl 0 in + let (_,lxp',_) = List.nth tll 0 in + if (dist (Lexp.lexp_location lxp) cursor < dist (Lexp.lexp_location lxp') cursor ) + then (lctx_hd,lxp) + else + ( + (lctx_tl,lxp') + ) + | hd::ml::tl -> let (lctx_hd,hdl) = hd in + let (lctx_ml,mll) = ml in + let (_,lxp,_) = List.nth hdl 0 in + let (_,lxp',_) = List.nth mll 0 in + if (dist (Lexp.lexp_location lxp) cursor < dist (Lexp.lexp_location lxp') cursor ) + then (foo (hd::tl) cursor) + else foo (ml::tl) cursor + + in foo lstr cursor let browse_list_lexp (tab:(Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) = let rec foo tab cursor = @@ -307,33 +396,11 @@ end if (dist loc_hd cursor < dist loc_ml cursor ) then (foo (hd::tl) cursor) else foo (ml::tl) cursor in foo tab cursor - - 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 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) - && - (location.end_line >= cursor.end_line && location.end_column >= cursor.end_column)) - then hd - else foo tl 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) + try pos_in_lexp_interval ctx lst cursor + with exn -> find_the_nearest_lexp ctx lst cursor (* search the type of a lexp browsing a lexp*) let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t = @@ -364,17 +431,19 @@ end -> (Debruijn.lctx_extend ctx v ForwardRef t)) ctx defs in - let tab = List.map - (fun (vn,lxp,ltp) -> - browse_lexp ctx' lxp cursor - ) - defs - in - - let (ctx'',id, ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in - - (ctx'',id, Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc) + let tab = List.map + (fun (vn,lxp,ltp) -> + browse_lexp ctx' lxp cursor + ) + defs + in + + let lt = (ctx,None, Lexp.mkSusp (Opslexp.get_type ctx e) (Opslexp.lexp_defs_subst l Subst.identity defs),l) in + browse_list_lexp ((browse_lexp ctx' e cursor)::lt::tab) cursor + + + | Arrow (ak, v, t1, l, t2) -> ( let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in @@ -387,12 +456,11 @@ end | SortK2NotType -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) ) - | 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 c = (ctx,None,t,l) in - let (ctx'',id,ret,loc) = browse_list_lexp ([a;b;c]) cursor in - (ctx'',id, ret, 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 c = (ctx,None,(Opslexp.get_type ctx e),l) in + browse_list_lexp ([a;b;c]) cursor | Call (f, args) -> ( @@ -458,7 +526,7 @@ end -> let (level, tab) = SMap.fold (fun _ case (level,tab) -> - let ((level, rctx, _), tab) = + let ((level, _, _), tab) = List.fold_left ( fun ((level, ictx, n), tab) (ak, v, t) -> @@ -496,7 +564,6 @@ end ) | Case (l, e, ret, branches, default) - (* FIXME: Check that the return type isn't TypeLevel. *) -> ( let candidats = ref [] in @@ -644,8 +711,7 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte match vr with | None -> loc - | Some v -> let ((_,_), idx) = v in - let ((l,_),_,_) = Myers.nth idx ctx in + | Some v -> let ((l,_),_,_) = Debruijn.lctx_lookup ctx v in l @@ -679,7 +745,21 @@ class lsp_server = let new_state = process_some_input_file contents in Hashtbl.replace buffers uri new_state; let diags = diagnostics new_state in - notify_back#send_diagnostic diags + let diags2 = List.map ( fun (x: Linol_lwt.Diagnostic.t) -> + + let ls = x.range.start in + let le = x.range.end_ in + { + x + with + range = + { + start = { ls with line = ls.line - 1 }; + end_ = { le with line = le.line - 1 } + } + } + ) diags in + notify_back#send_diagnostic diags2 (* We now override the [on_notify_doc_did_open] method that will be called by the server each time a new document is opened. *) @@ -764,16 +844,23 @@ class lsp_server = | 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 word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in let typer_loc = typer_pos_of_lsp_pos pos in + let path = "/home/soilih/Bureau/test/compl.txt" in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 path in + let c = "-----------------\n mot:" ^ word ^ "\n-------------\n" in + + output_string oc (c); + close_out oc; let range = Compl.lsp_range_of_a_tuple - (typer_loc.start_line,(typer_loc.end_column - 2 - String.length word)) + (typer_loc.start_line,(typer_loc.end_column - 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 @@ -824,7 +911,7 @@ let sep name s = let test () = let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let name = "/home/soilih/Bureau/test/test.txt" in - sep name "INT"; + (*sep name "INT"; hoverTest ctx name "e = 12 ;" (1,1) "##Int"; hoverTest ctx name "e = 12 ;" (1,5) "##Int"; sep name "STRING"; @@ -865,7 +952,7 @@ let test () = hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "##Type"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (a -> ((List ℓ a) -> (List ℓ a)))"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12) "##Int"; - hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)"; + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)";*) sep name "ARROW"; hoverTest ctx name "type Floo = bar Int Int ;" (1,1) ""; hoverTest ctx name "type Floo = bar Int Int ;" (1,7) ""; @@ -878,7 +965,7 @@ let test () = hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,10) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,17) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,29) ""; - hoverTest ctx name "v = Int -> Int ;" (1,1) ""; + hoverTest ctx name "v = Int -> Int ;" (1,1) ""(*; sep name "INDUCTIVE"; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1) ""; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10) ""; @@ -914,7 +1001,7 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (3,4) ""; hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (3,13) ""; hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,4) ""; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,14) "" + hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,14) ""*) (*=======================================Test======================================*) @@ -926,7 +1013,7 @@ let test () = let run () = ignore (Arg.Set Log.lsp_enabled); Logs.set_level ~all:true (Some Logs.Debug); - test (); + (*test ();*) let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/1d141dbd6bd7cd1d96d47c10744915502… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/1d141dbd6bd7cd1d96d47c10744915502… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch check_inferred-more
by Jean-Alexandre Barszcz (＠jabarszcz) 10 Aoû '21

10 Aoû '21

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

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Août 2021