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

Commits: 2c45ce87 by Soilih BEN SOILIH at 2021-12-02T16:00:03-05:00 config

- - - - - 7080f329 by Soilih BEN SOILIH at 2021-12-05T02:12:52-05:00 add proj to my branch

- - - - - 495a8c88 by Soilih BEN SOILIH at 2021-12-10T10:12:48-05:00 resolve Proj errors

- - - - - ded4414a by Soilih BEN SOILIH at 2021-12-14T21:27:28-05:00 adding breadcrumbs, highlight and references

- - - - -

12 changed files:

- + .configuration.txt - btl/pervasive.typer - − configuration.txt - src/elab.ml - src/elexp.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/positivity.ml - src/typer_lsp_server.ml - src/unification.ml

Changes:

===================================== .configuration.txt ===================================== @@ -0,0 +1,3 @@ +"filename":"/home/soilih/Projet Maitrise/typer" +"description":"this filename is the absolute path from where we run Typer. +We must change it to make it work !!!"

===================================== btl/pervasive.typer ===================================== @@ -426,31 +426,6 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair;

-__.__ = - let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") - (cons (Sexp_symbol "?") - (cons (Sexp_symbol "cons") - nil)); - pattern = Sexp_node constructor - (cons (Sexp_node (Sexp_symbol "_:=_") - (cons f (cons (Sexp_symbol "v") - nil))) - nil); - branch = Sexp_node (Sexp_symbol "_=>_") - (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") - (cons (Sexp_node (Sexp_symbol "_|_") - (cons o (cons branch nil))) - nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error);

%% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type)

===================================== configuration.txt deleted ===================================== @@ -1,2 +0,0 @@ -"filename":"/Projet Maitrise/typer" -"description":"this filename is the place from where we run Typer. We must change it to make it work !!!"

===================================== src/elab.ml ===================================== @@ -72,23 +72,16 @@ let dloc = dummy_location let parsing_internals = ref false let btl_folder =

- (* - (* Read the JSON file *) - let json = Yojson.Basic.from_file "../configuration.json" in - let exec_path = json |> Yojson.Basic.Util.member "path" |> Yojson.Basic.Util.to_string in - *) - - (* - let canal_entree = open_in "../configuration.txt" in + let cwd = Sys.getcwd () in + let cdir = String.sub cwd 0 (String.length cwd) in + let canal_entree = open_in (cdir ^ "/.configuration.txt") in let ligne1 = input_line canal_entree in let l = String.split_on_char ':' ligne1 in let m = String.split_on_char '"' (List.nth l 1) in let filename = List.nth m 1 in - *) - - let env_var = Sys.getenv "HOME" in + try Sys.getenv "TYPER_BUILTINS" - with Not_found -> env_var ^ (*exec_path*) (*filename*) "/Projet Maitrise/typer" ^ "/btl" + with Not_found -> filename ^ "/btl"

let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt @@ -459,6 +452,7 @@ let meta_to_var ids (e : lexp) = | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl) | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in @@ -1756,6 +1750,17 @@ let sform_letin ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc

+let sform_proj ctx loc sargs ot = + match sargs with + | [lxp;(Symbol (loca,str))] + -> let (ret,_) = infer lxp ctx in + let e = mkProj (loc,ret,(loca,str)) in + (e, Lazy) + | _ -> sexp_error loc "Unrecognized proj expression"; + sform_dummy_ret ctx loc + + + let rec infer_level ctx se : lexp = match se with | Symbol (_, "z") -> mkSortLevel SLz @@ -1876,6 +1881,7 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("__.__", sform_proj); ("lambda_->_", sform_lambda Anormal); ("lambda_=>_", sform_lambda Aimplicit); ("lambda_≡>_", sform_lambda Aerasable);

===================================== src/elexp.ml ===================================== @@ -51,6 +51,8 @@ type elexp =

(* A variable reference, using deBruijn indexing. *) | Var of vref + (* A projection *) + | Proj of U.location * elexp * int

(* Recursive `let` binding. *) | Let of U.location * (vname * elexp) list * elexp @@ -83,6 +85,7 @@ let rec elexp_location e = match e with | Imm s -> sexp_location s | Var ((l,_), _) -> l + | Proj (l,_,_) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l | Lambda ((l,_),_) -> l @@ -96,6 +99,7 @@ let elexp_name e = match e with | Imm _ -> "Imm" | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "Let" | Call _ -> "Call" | Cons _ -> "Cons" @@ -136,6 +140,9 @@ and elexp_string lxp = | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" + | Proj (l,lxp,i) + -> "( _._ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )" + | Cons (_, (_, s)) -> "datacons(" ^ s ^")"

| Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b)

===================================== src/eval.ml ===================================== @@ -463,6 +463,17 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) (eval f ctx trace) (List.map (fun e -> eval e ctx trace) args)

+ (* Proj *) + | Proj (loc, e, i) + -> let vt = eval' e ctx in + ( + match vt with + | Vcons (symbol, vtl) -> List.nth vtl i + | _ -> error + loc + "Connot find a value in position %d \n" i + ) + (* Case *) | Case (loc, target, pat, dflt) -> (eval_case ctx trace loc target pat dflt)

===================================== src/inverse_subst.ml ===================================== @@ -264,6 +264,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl) | Susp (e, s') -> apply_inv_subst (push_susp e s') s | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in

===================================== src/lexp.ml ===================================== @@ -66,6 +66,7 @@ type ltype = lexp | Sort of U.location * sort | Builtin of symbol * ltype | Var of vref + | Proj of U.location * lexp * label | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp @@ -245,6 +246,10 @@ let lexp'_hash (lp : lexp') = args))) | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) + | Proj (l,lxp,lbl) + -> U.combine_hash 15 (U.combine_hash (Hashtbl.hash l) + (U.combine_hash (Hashtbl.hash lxp) (Hashtbl.hash lbl))) +

(* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) @@ -309,6 +314,7 @@ let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) +let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) let mkLet (l, ds, e) = hc (Let (l, ds, e)) let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) @@ -329,6 +335,7 @@ let lexp_head e = | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "let" | Arrow _ -> "Arrow" | Lambda _ -> "lambda" @@ -513,6 +520,7 @@ let rec lexp_location e = | SortLevel SLz -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l + | Proj (l,_,_) -> l | Builtin ((l, _), _) -> l | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l @@ -590,6 +598,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s) + | Proj (l,lxp,lbl) -> mkProj (l, mkSusp lxp s, lbl)

and nosusp e = (* Return `e` with no outermost `Susp`. *) match lexp_lexp' e with @@ -653,6 +662,7 @@ let clean e = | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) + | Proj (l,lxp,lbl) -> mkProj (l,(clean s lxp),lbl) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with @@ -671,6 +681,10 @@ let rec lexp_unparse lxp = | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Proj (l,lxp,(loc,str) ) + -> Node (Symbol (l, "__.__"), + [(lexp_unparse lxp);(Symbol (loc,str))]) + | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) @@ -1003,6 +1017,9 @@ and lexp_str ctx (exp : lexp) : string =

| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;

+ | Proj (l,lxp,(loc,str)) + -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + | Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with

===================================== src/opslexp.ml ===================================== @@ -747,6 +747,46 @@ and check'' erased ctx e = args) in let tct = arg_loop ctx erased args in tct + + | Proj (l, e, (loc, label)) + ->( let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (check erased ctx e) ctx in + let it, aargs = call_split etype in + match 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 (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let fieldtypes = SMap.find label constructors in + let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> 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) + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l "Proj on an inductive type that's not a tuple!"; etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -926,6 +966,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty) + | Proj (l,lxp,lbl) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in @@ -1072,6 +1113,47 @@ and get_type ctx e = arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct + + | Proj (l, e, (loc, label)) + ->( (*check'' DB.set_empty ctx e*) + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (get_type ctx e) ctx in + let it, aargs = call_split etype in + match 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 (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let fieldtypes = SMap.find label constructors in + let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> 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) + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l "Proj on an inductive type that's not a tuple!"; etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | Case (_l, _e, ret, _branches, _default) -> ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -1140,11 +1222,44 @@ let arity_of_cons ^^ {|because it is not an inductive type: %s|}) name (lexp_string ty)

+let pos_of_label lctx label t : int = + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let it, aargs = call_split t in + match lexp'_whnf it lctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let bindings = SMap.bindings constructors in + let find_the_pos label (lst : (string * (arg_kind * vname * ltype) list) list) c = + match lst with + | [ls] -> let (_,l) = ls in + let rec foo label (l : (arg_kind * vname * ltype) list) c = + match l with + | [] -> failwith "label not found!" + | hd::tl -> match hd with + | (ak, (loc, Some vn), ltp ) + -> let (_,st) = label in + if (String.equal vn st) then c + else foo label tl (c + 1) + | _ -> foo label tl (c + 1) + in + foo label l c + | _ -> failwith "More than one element!" + in find_the_pos label bindings 0 + | Inductive _, _ + -> failwith "Proj on an inductive type that's not a tuple!" + | _,_ -> failwith "Proj on a non-inductive type!" + let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) + | L.Proj (l, exp, label) + -> let t = get_type lctx exp in + E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)

| L.Lambda (P.Aerasable, _, _, body)

===================================== src/positivity.ml ===================================== @@ -117,6 +117,8 @@ and positive' index lexp = *) -> true

+ | Lexp.Proj _ -> false + | Lexp.Case _ | Lexp.Cons _ | Lexp.Let _ | Lexp.Sort _ | Lexp.SortLevel _ (* There are no rules that have these synctactic forms as a conclusion. *) -> false

===================================== src/typer_lsp_server.ml ===================================== @@ -625,8 +625,52 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D ) 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 = SMap.find label 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 + | Case (l, e, ret, branches, default) -> let candidats = ref [] in @@ -875,6 +919,35 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = () ) filtred_list

+let kind_bread (e: Lexp.lexp) : Lsp.Types.SymbolKind.t = + let open Elexp in + match Lexp.lexp_lexp' e with + | Lambda (ak, (l,_), t, e) -> Lsp.Types.SymbolKind.Function + | Cons (t, (_l, name)) -> Lsp.Types.SymbolKind.Constructor + | _ -> Lsp.Types.SymbolKind.Variable + + +let kind_ (element : Debruijn.env_elem ) : Lsp.Types.SymbolKind.t = + let (_,vrb,_) = element in + match vrb with + | Variable + | ForwardRef -> Lsp.Types.SymbolKind.Variable + | LetDef (_,lxp) -> kind_bread lxp + +let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol.t list = + List.map ( fun x -> + let ((l,s),_,_) = x in + let range = lsp_range_of_loc_for_symbol l in + let nm = Option.get s in + Lsp.Types.DocumentSymbol.create + ~name:nm + ~detail:nm + ~kind:(kind_ x) + ~range:range + ~selectionRange:range + () + ) lst + (*=====================================End Symbols=================================*)

(*====================================Compl===================================*) @@ -939,19 +1012,37 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list =

| None -> filter_lctx tl ret | Some _ -> filter_lctx tl (hd::ret) - - + + let construct_highlights (lst: Debruijn.env_elem list) : Lsp.Types.DocumentHighlight.t list = + List.map ( fun (x: Debruijn.env_elem) -> + let ((l,s),_,_) = x in + let range = Compl.lsp_range_of_a_tuple + (l.start_line,l.start_column) (l.end_line,l.end_column) + in + Lsp.Types.DocumentHighlight.create ~range:range () + ) lst + let construct_references uri (lst: Debruijn.env_elem list) : Lsp.Types.Location.t list = + List.map ( fun (x: Debruijn.env_elem) -> + let ((l,s),_,_) = x in + let range = Compl.lsp_range_of_a_tuple + (l.start_line,l.start_column) (l.end_line,l.end_column) + in + Lsp.Types.Location.create ~uri:uri ~range:range + ) lst (* Transform a context to a list of completion item *) - let ctx_to_ci_list (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = + let ctx_to_ci_list ctx (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = List.map ( fun (x: Debruijn.env_elem) -> let ((_,s),_,t) = x in let str = Option.get s in let label = str in + let s = try use_search_name_in_ctx ctx t + with exe -> Lexp.lexp_string_for_lsp t + in let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(str) in let kind = kind_of_a_varbind x in let ci = Lsp.Types.CompletionItem.create ~label:label ~kind:kind - ~textEdit:textEdit ~detail:(Lexp.lexp_string t) () + ~textEdit:textEdit ~detail:s () in ci

@@ -1044,7 +1135,7 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = *) class lsp_server = object(self) - inherit Linol_lwt.Jsonrpc2.server + inherit Linol_lwt.Jsonrpc2.server as super

(* one env per document *) val buffers: (Lsp.Types.DocumentUri.t, state_after_processing) Hashtbl.t @@ -1103,6 +1194,10 @@ class lsp_server = Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; """; "'"; "/"; "@"; "<"] ~resolveProvider:true () in + let referencesProvider = `Bool true + in + let documentHighlightProvider = `Bool true + in

let documentSymbol = Lsp.Types.DocumentSymbolOptions.create ~workDoneProgress:true () @@ -1119,6 +1214,8 @@ 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.referencesProvider = Some referencesProvider ; + Lsp.Types.ServerCapabilities.documentHighlightProvider = Some documentHighlightProvider; Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol) }

@@ -1163,22 +1260,8 @@ class lsp_server = in let e = Some r in let f = Linol_lwt.return e in f - - (* provisional, to be done later *) - method! on_req_execute_command ~notify_back ~id _c _args = - match _c with - | "typer" -> let file = "command.txt" in - let message = _c in (* Write message to file *) - let oc = open_out file in (* create or truncate file, return channel *) - Printf.fprintf oc "%s\n" message; (* write something *) - close_out oc; (* flush and close the channel *) - let h = Lsp.Types.Command.yojson_of_t - (Lsp.Types.Command.create ~title:_c ~command:_c () ) in - let e = Linol_lwt.return h in e - | _ -> assert false +

- - (* provisional, to be done later *) method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with

@@ -1205,21 +1288,70 @@ class lsp_server = in

let filtred_list = filter_lctx l_ctx [] in - let comp_list = ctx_to_ci_list filtred_list range in + let comp_list = ctx_to_ci_list l_ctx filtred_list range in let comp_list_ret = complete_oth word comp_list in

let e = Some (`List comp_list_ret) in let f = Linol_lwt.return e in f - (* + method! on_req_symbol ~notify_back ~id ~uri () =

match Hashtbl.find buffers uri with

- | state_after_processing -> let (_,(list_list, _)) = state_after_processing in - let r = create_symbols list_list in + | state_after_processing -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = pos_of_tuple (Int.max_int,Int.max_int) in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in + let filtred_list = filter_lctx l_ctx [] in + let r = create_breadcrumbs filtred_list in 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 = + fun req -> + + (match req with + | TextDocumentHighlight params + -> ( + match Hashtbl.find buffers params.textDocument.uri with + | state_after_processing + -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = pos_of_tuple + (params.position.line,params.position.character) in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in + let filtred_list = filter_lctx l_ctx [] in + let hi = construct_highlights filtred_list in + let e = Some hi in + let f = Linol_lwt.return e in f) + | TextDocumentReferences params + -> ( + match Hashtbl.find buffers params.textDocument.uri with + | state_after_processing + -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = pos_of_tuple + (params.position.line,params.position.character) in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in + let filtred_list = filter_lctx l_ctx [] in + let hi = construct_references (params.textDocument.uri) filtred_list in + let e = Some hi in + let f = Linol_lwt.return e in f) + | _ -> super#on_request_unhandled ~notify_back ~id req + ) + in f req + end

===================================== src/unification.ml ===================================== @@ -69,6 +69,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false | Var (_, _i) -> false + | Proj(_,lxp,_) -> oi lxp | Susp (_e, _s) -> Log.internal_error "`e` should be "clean" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e)

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9a5b03e0602a39243ff663c7564a634cc...