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/a1a11af523dcfe97f455c4ccc37362793...