[Typer] [Git][monnier/typer][soilih] 5 commits: elab_check

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/8e4c57753af78736d6b0d58946e1a7421...