Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer

Commits: 6ff1e63e by Soilih BEN SOILIH at 2021-12-21T06:48:58-05:00 -

- - - - - 42c504dc by Soilih BEN SOILIH at 2021-12-21T20:45:53-05:00 -

- - - - - 3de98c1a by Soilih BEN SOILIH at 2021-12-21T23:24:10-05:00 -

- - - - - 123f4ea2 by Soilih BEN SOILIH at 2021-12-24T19:46:51-05:00 browse_defs

- - - - -

2 changed files:

- src/opslexp.ml - src/typer_lsp_server.ml

Changes:

===================================== src/opslexp.ml ===================================== @@ -772,9 +772,9 @@ and check'' erased ctx e = | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> mkSusp ftype s (*if ak = Aerasable + -> if ak = Aerasable then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -1139,9 +1139,9 @@ and get_type ctx e = | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> mkSusp ftype s(*if ak = Aerasable + -> if ak = Aerasable then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with

===================================== src/typer_lsp_server.ml ===================================== @@ -42,9 +42,23 @@ open Util type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list

type state_after_processing = (log_entry list * - (list_in_list * Debruijn.elab_context) + (list_in_list * Debruijn.elab_context) * ((int * int) option ref) )

+(* +let last_pos = ref [(0,0)] + +let add_to_tab tab a = + if((List.length !tab) > 4) then + let l = List.tl(List.rev !tab) in + tab := a::(List.rev l) + else + tab := a::(!tab) + +let get_pos_tab tab = + List.hd !tab +*) + (* transform a list of logs to a list of tuple to facilitate the manipulation *) @@ -135,14 +149,14 @@ let readstring (str:string) = 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) + (!Log.typer_log, ast, ref None)

let process_some_input_file (_file_contents : string) : state_after_processing = readstring _file_contents

(*Return the diagnostics of a document state *) let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = - let (log, _) = _state in + let (log, _, _) = _state in let log_tab = log_entry_to_list log in List.map (fun x -> let (loc, lev, msg) = x in @@ -626,11 +640,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D | [] -> () | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable - then - let a = Lexp.mkSusp ftype s in - candidats := (browse_lexp ctx a cursor):: !candidats; - else () + -> if ak = Aerasable + then + let a = Lexp.mkSusp ftype s in + candidats := (browse_lexp ctx a cursor):: !candidats; + else failwith "Fail Here!!!" | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -805,9 +819,29 @@ let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) = else tl |hd::ml::tl -> if (dist hd cursor < dist ml cursor ) then (foo (hd::tl) cursor) else foo (ml::tl) cursor -in foo tab cursor + in foo tab cursor + + let vn_on_the_cursor (vn:vname) (cursor:location) : bool = + let (l,_) = vn in + if ((cursor.start_column >= l.start_column) + && (cursor.end_column <= l.end_column)) + then true + else false + + let tup_browse_defs_in_ctx (lctx: Debruijn.lexp_context) (vn : vname) = + let lctx_l = Myers.list lctx in + let (_,so) = vn in + let str = Option.get so in + let rec foo lst comp str rlst = + match lst with + | [] -> rlst + | ((_, Some s) as vne, _, _)::tl + -> if String.equal s str then + foo tl (comp + 1) str ((Some (vne,comp))::rlst) + else foo tl (comp + 1) str rlst + | _::tl -> foo tl (comp + 1) str rlst + in foo lctx_l 0 str []

-(* let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) =

match Lexp.lexp_lexp' e with @@ -824,164 +858,42 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc | Sort (_, StypeOmega) -> None | Builtin (_, t) -> None | Var (vn, idx) - -> Some (e,vn,idx) + -> Some (vn,idx) | Susp (e, s) -> None | Let (l, defs, e) -> let ctx' = List.fold_left (fun ctx (v, _e, t) -> (Debruijn.lctx_extend ctx v ForwardRef t)) ctx defs in - let rec foo ctx defs cursor ret_list = - match defs with - | [] -> ret_list - | hd::tl -> let (vn,lxp,ltp) = hd in - foo ctx tl cursor ((browse_defs ctx lxp cursor)::ret_list) + let rec foo (ctx_list:Debruijn.env_elem list) cursor comp = + match ctx_list with + | [] -> failwith "No Variable in the cursor" + | ((l, (Some vn) as v),_,_)::tl + -> if (vn_on_the_cursor v cursor) then Some (v,comp) + else foo tl cursor (comp + 1) + | _::tl -> foo tl cursor (comp + 1) in - let tab = List.map - (fun (vn,lxp,ltp) -> - browse_defs ctx' lxp cursor - ) - defs - in - - (browse_defs ctx' e cursor)::tab + let ctx_list = Myers.list ctx' in + foo ctx_list cursor 0

| 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 - 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) - | SortK1NotType - -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) - | SortK2NotType - -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) - ) + -> None

- | 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 etp = Opslexp.get_type ctx' e in - let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*) - let d = (ctx,None, t,l) in - browse_list_lexp ([a;b;d]) cursor + | Lambda (ak, ((l,_) as v), t, e) -> if (vn_on_the_cursor v cursor) then + try List.hd (tup_browse_defs_in_ctx ctx v) + with exe -> None + else None

- | 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 - - browse_list_lexp (fonc::args_list) cursor - ) - - | Inductive (l, _label, args, cases) - -> - ( - let rec arg_loop ctx args = - - match args with - - | [] - -> let (level, tab) = - SMap.fold - (fun _ case (level,tab) -> - let ((level, _, _), tab) = - List.fold_left - ( - fun ((level, ictx, n), tab) (ak, v, t) -> - ( - ((let lwhnf = Opslexp.lexp_whnf (Opslexp.get_type ictx t) ictx in - match Lexp.lexp_lexp' lwhnf with - | Sort (_, Stype _) - when ak == Pexp.Aerasable - -> level - | Sort (_, Stype level') - -> Opslexp.mkSLlub ctx level - (Lexp.mkSusp level' (Lexp.sunshift n)) - | _tt -> level), - Debruijn.lctx_extend ictx v Variable t, - n + 1), - ((browse_lexp ictx t cursor)::tab) - ) - ) - ((level, ctx, 0), [] ) - case in - (level, tab) - ) - cases - (Lexp.mkSortLevel SLz, []) in - browse_list_lexp ((ctx, None,level,l)::tab) cursor - - | (ak, v, t)::args - -> let ctx' = Debruijn.lctx_extend ctx v Variable t in - browse_list_lexp - ( - (browse_lexp ctx' t cursor)::(arg_loop ctx' args)::[] - ) cursor - in - arg_loop ctx args - ) - - | Proj (l, e, (loc, label)) - -> let candidats = ref [] in - ( - let call_split (e: Lexp.lexp) = - match Lexp.lexp_lexp' e with - | Call (f, args) -> (f, args) - | _ -> (e,[]) in - candidats := (browse_lexp ctx e cursor):: !candidats; - let etype = Opslexp.get_type ctx e in - let it, aargs = call_split etype in - match Opslexp.lexp'_whnf it ctx, aargs with - | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors = 1 - -> let rec mksubst s fargs aargs = - match fargs, aargs with - | [], [] -> s - | _farg::fargs, (_ak, aarg)::aargs - -> mksubst (Subst.cons aarg s) fargs aargs - | _,_ -> s in - let s = mksubst Subst.identity fargs aargs in - let (_,fieldtypes) = List.hd (SMap.bindings constructors) in - let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) = - match fieldtypes with - | [] -> () - | (ak, (_, Some fn), ftype)::_ when fn = label - (* We found our field! *) - -> if ak = Aerasable - then - let a = Lexp.mkSusp ftype s in - candidats := (browse_lexp ctx a cursor):: !candidats; - else () - | (ak, vdef, ftype)::fieldtypes - -> let fvdef vdef e loc lbl = - match vdef with - |(l, Some n) -> Lexp.mkProj (loc, e, lbl) - |_ -> Lexp.impossible in - let fieldref = fvdef vdef e l (loc, label) in - getfieldtype (Subst.cons fieldref s) fieldtypes in - getfieldtype s fieldtypes; () - | Inductive _, _ - -> () - | _,_ -> ()); - browse_list_lexp !candidats cursor - + | Call (f, args) -> None + | Inductive (l, _label, args, cases) -> None + | Proj (l, e, (loc, label)) -> None | Case (l, e, ret, branches, default) - -> - let candidats = ref [] in - + -> let candidats = ref [] in let call_split (e: Lexp.lexp) = match Lexp.lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - candidats := (browse_lexp ctx e cursor):: !candidats; + (* 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 *) @@ -994,7 +906,7 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc let it, aargs = call_split etype in ( match Opslexp.lexp'_whnf it ctx, aargs with - + | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -1019,7 +931,7 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc (erased, nctx) in

let brch = SMap.bindings branches in - let lst = + let _ = List.map ( fun (name, (l, vdefs, branch)) @@ -1030,7 +942,8 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes - -> mkctx (Opslexp.dbset_push ak erased) + -> candidats := ((Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)), vdef)::!candidats; + mkctx (Opslexp.dbset_push ak erased) (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) (Lexp.ssink vdef s) (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) @@ -1042,66 +955,33 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc let (nerased, nctx, hlxp) = 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 - candidats := (browse_lexp nctx branch cursor) :: !candidats; + ignore(ctx_extend_with_eq nctx subst hlxp) ) brch in - - let diff = SMap.cardinal constructors - List.length lst in - ( - match default with - | Some (v, d) - -> if diff <= 0 then (); - let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in - let subst = Subst.shift 1 in - let hlxp = Lexp.mkVar ((l, None), 0) in - let (_, nctx) = - ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp nctx d cursor) :: !candidats; - () - | None - -> if diff > 0 then (); () - ) + () + + | _,_ -> () ; ); - browse_list_lexp !candidats cursor + let rec cands (lst: (Debruijn.lexp_context * vname) list) = + match lst with + | [] -> failwith "No Valid Candidate" + | hd::tl -> let (ctx,(l,s)) = hd in + if (l.start_column <= cursor.start_column + && l.end_column >= cursor.end_column + ) + then hd + else cands tl + in + let (lctx,vn) = cands !candidats in + List.hd (tup_browse_defs_in_ctx lctx vn) + | Cons (t, (_l, name)) - -> (match Opslexp.lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) - -> (try - let fieldtypes = Util.SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, Lexp.mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in - let rec fieldargs ftypes = - match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - Lexp.mkCall (Lexp.mkSusp t (Subst.shift nargs), - indtype fargs (nargs - 1)) - | (ak, vd, ftype) :: ftypes - -> Lexp.mkArrow (ak, vd, ftype, Lexp.lexp_location ftype, - fieldargs ftypes) in - let rec buildtype fargs = - match fargs with - | [] -> fieldargs fieldtypes - | (_ak, ((l,_) as vd), atype) :: fargs - -> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l, - buildtype fargs) in - (ctx, None, buildtype fargs, location) - with Not_found - -> (ctx, None, Debruijn.type_int, location) - ) - | _ -> (ctx, None, Debruijn.type_int, location)) - + -> None | Metavar (idx, s, _) - -> (match Lexp.metavar_lookup idx with - | MVal e -> let e = Lexp.push_susp e s in - browse_lexp ctx e cursor - | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, location)) -*) + -> None + (*==================================Parcourir les définitions==========================*)

(* Search if the vname is in the context *) @@ -1485,6 +1365,7 @@ class lsp_server = Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; """; "'"; "/"; "@"; "<"] ~resolveProvider:true () in + (* let referencesProvider = `Bool true in let documentHighlightProvider = `Bool true @@ -1493,7 +1374,7 @@ class lsp_server = let documentSymbol = Lsp.Types.DocumentSymbolOptions.create ~workDoneProgress:true () in - + *) let hoverOption = Lsp.Types.HoverOptions.create ~workDoneProgress:true () in @@ -1504,16 +1385,17 @@ class lsp_server =

{ arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider ; Lsp.Types.ServerCapabilities.hoverProvider = Some (`HoverOptions hoverOption); - Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption); + Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption)(*; Lsp.Types.ServerCapabilities.referencesProvider = Some referencesProvider ; Lsp.Types.ServerCapabilities.documentHighlightProvider = Some documentHighlightProvider; - Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol) + Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol)*) }

method! on_req_definition ~notify_back ~id ~uri ~pos _st = match Hashtbl.find buffers uri with

- | state_after_processing -> let (_,ast) = state_after_processing in + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (pos.line,pos.character); 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 @@ -1531,7 +1413,8 @@ class lsp_server = method! on_req_hover ~notify_back ~id ~uri ~pos doc_state = match Hashtbl.find buffers uri with

- | state_after_processing -> let (_,ast) = state_after_processing in + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (pos.line,pos.character); let (list_list, ectx) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in @@ -1546,7 +1429,7 @@ class lsp_server = in (*let s = Lexp.lexp_string_for_lsp l_type in*) let r = Lsp.Types.Hover.create - ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) + ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=(Some "Typer")}) ~range:range () in let e = Some r in @@ -1556,7 +1439,8 @@ 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 (_,ast) = state_after_processing in + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (pos.line,pos.character); 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 @@ -1601,7 +1485,7 @@ class lsp_server = let e = Some (`DocumentSymbol r) in let f = Linol_lwt.return e in f

- + method! on_request_unhandled ~notify_back ~id req =

let f :type r. r Lsp.Client_request.t -> r Linol_lwt.Jsonrpc2.IO.t = @@ -1643,7 +1527,7 @@ class lsp_server = | _ -> super#on_request_unhandled ~notify_back ~id req ) in f req - *) + *) end

@@ -1654,7 +1538,7 @@ let comp (a:string) (b:string) : string = else "/*******-----:-(:-(:-(:-(:-(:-(:-(____FAILED___:-(:-(:-(:-(:-(:-(:-(-----*******/\n\n\n"

let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) (expected:string) = - let (_, ast) = readstring content in + let (_, ast,_) = readstring content in let (list_list, _) = ast in let (l,c) = position in let pos = pos_of_tuple position in @@ -1796,7 +1680,13 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (5,4) ""; hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (5,14) ""

- + +let time f a b = + let t = Sys.time() in + let fx = f a b in + Printf.printf "Execution time: %fs\n" (Sys.time() -. t); + fx +

(*=======================================Test======================================*)

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/39573a65cce99bb211b653fae49ce64dc...