Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Juillet 2021
- 1 participants
- 5 discussions
21 Jul '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
06a6ffa3 by Soilih BEN SOILIH at 2021-07-16T21:57:52-06:00
-
- - - - -
3ed77305 by Soilih BEN SOILIH at 2021-07-21T00:49:17-06:00
definition with the identification and update the Inductive
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
=====================================
src/typer_lsp_server.ml
=====================================
@@ -120,7 +120,7 @@ let readstring (str:string) =
(!Log.typer_log, ast)
let process_some_input_file (_file_contents : string) : state_after_processing =
- Logs.err (fun k->k " %s" @@ "TEST TEST TEST");
+ (*Logs.err (fun k->k " %s" @@ "TEST TEST TEST");*)
readstring _file_contents
let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list =
@@ -293,17 +293,17 @@ end
else foo (ml::tl) cursor
in foo lexp_list cursor
- let browse_list_lexp (tab:(Debruijn.lexp_context * Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) =
+ 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 =
match tab with
| [] -> failwith "Liste vide!"
| [n] -> n
- | [hd;tl] -> let (_,_,loc_hd) = hd in
- let (_,_,loc_tl) = tl in
+ | [hd;tl] -> let (_,_,_,loc_hd) = hd in
+ let (_,_,_,loc_tl) = tl in
if (dist loc_hd cursor < dist loc_tl cursor ) then hd
else tl
- |hd::ml::tl -> let (_,_,loc_hd) = hd in
- let (_,_,loc_ml) = ml in
+ |hd::ml::tl -> let (_,_,_,loc_hd) = hd in
+ let (_,_,_,loc_ml) = ml in
if (dist loc_hd cursor < dist loc_ml cursor ) then (foo (hd::tl) cursor)
else foo (ml::tl) cursor
in foo tab cursor
@@ -336,27 +336,27 @@ end
(lctx,lexp)
(* 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 * Lexp.lexp * Source.Location.t =
+ 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 =
let open Elexp in
let location = Lexp.lexp_location e in
match Lexp.lexp_lexp' e with
- | Imm (Float (_, _)) -> (ctx, Debruijn.type_float, location)
- | Imm (Integer (_, _)) -> (ctx, Debruijn.type_int, location)
- | Imm (String (_, _)) -> (ctx, Debruijn.type_string, location)
- | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (ctx, Debruijn.type_string, location)
- | SortLevel SLz -> (ctx, Debruijn.type_level, location)
+ | Imm (Float (_, _)) -> (ctx, None, Debruijn.type_float, location)
+ | Imm (Integer (_, _)) -> (ctx, None, Debruijn.type_int, location)
+ | Imm (String (_, _)) -> (ctx, None, Debruijn.type_string, location)
+ | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (ctx, None, Debruijn.type_string, location)
+ | SortLevel SLz -> (ctx, None, Debruijn.type_level, location)
| SortLevel (SLsucc e)
- -> (ctx, Debruijn.type_level, location)
+ -> (ctx, None, Debruijn.type_level, location)
| SortLevel (SLlub (e1, e2))
- -> (ctx, Debruijn.type_level, location)
+ -> (ctx, None, Debruijn.type_level, location)
| Sort (l, Stype e)
- -> (ctx, Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location)
- | Sort (_, StypeLevel) -> (ctx, Debruijn.sort_omega, location)
- | Sort (_, StypeOmega) -> (ctx, Debruijn.sort_omega, location)
- | Builtin (_, t)-> (ctx, t, location)
+ -> (ctx, None, Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location)
+ | Sort (_, StypeLevel) -> (ctx, None, Debruijn.sort_omega, location)
+ | Sort (_, StypeOmega) -> (ctx, None, Debruijn.sort_omega, location)
+ | Builtin (_, t)-> (ctx, None, t, location)
| Var (((l, name), idx) as v) ->
- (ctx, Debruijn.lctx_lookup_type ctx v, location)
+ (ctx, Some v, Debruijn.lctx_lookup_type ctx v, location)
| Susp (e, s) -> browse_lexp ctx (Lexp.push_susp e s) cursor
| Let (l, defs, e)
-> let ctx' =
@@ -371,28 +371,28 @@ end
defs
in
- let (ctx'', ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in
+ let (ctx'',id, ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in
- (ctx'', Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc)
+ (ctx'',id, Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc)
| Arrow (ak, v, t1, l, t2)
-> (
let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in
match Opslexp.sort_compose ctx nctx l ak t1 t2 with
- | SortResult k -> (nctx, k, location)
+ | SortResult k -> (nctx, None, k, location)
| SortInvalid
- -> (nctx, Lexp.mkSort (l, StypeOmega), location)
+ -> (nctx, None, Lexp.mkSort (l, StypeOmega), location)
| SortK1NotType
- -> (nctx, Lexp.mkSort (l, StypeOmega), location)
+ -> (nctx, None, Lexp.mkSort (l, StypeOmega), location)
| SortK2NotType
- -> (nctx, Lexp.mkSort (l, StypeOmega), location)
+ -> (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,t,l) in
- let (ctx'',ret,loc) = browse_list_lexp (a::b::c::[]) cursor in
- (ctx'', ret, loc)
+ let c = (ctx,None,t,l) in
+ let (ctx'',id,ret,loc) = browse_list_lexp ([a;b;c]) cursor in
+ (ctx'',id, ret, loc)
| Call (f, args)
-> (
@@ -406,10 +406,13 @@ end
)
| Inductive (l, _label, args, cases)
- ->(
-
+ ->
+ (*
+ (
let rec arg_loop ctx erased args =
+
match args with
+
| []
-> let level
= SMap.fold
@@ -417,7 +420,7 @@ end
let (level, rctx, _, _) =
List.fold_left
(fun (level, ictx, erased, n) (ak, v, t) ->
- ((let lwhnf = Opslexp.lexp_whnf t ictx in
+ ((let lwhnf = Opslexp.lexp_whnf (Opslexp.get_type ictx t) ictx in
match Lexp.lexp_lexp' lwhnf with
| Sort (_, Stype _)
when ak == Pexp.Aerasable
@@ -431,9 +434,11 @@ end
n + 1))
(level, ctx, erased, 0)
case in
- level)
+ level
+ )
cases (Lexp.mkSortLevel SLz) in
Lexp.mkSort (l, Stype level)
+
| (ak, v, t)::args
-> let _k = t in
Lexp.mkArrow (ak, v, t, Lexp.lexp_location t,
@@ -443,7 +448,53 @@ end
let tct = arg_loop ctx Debruijn.set_empty args in
(ctx, tct, location)
)
-
+ *)
+ (
+ let rec arg_loop ctx args =
+
+ match args with
+
+ | []
+ -> let (level, tab) =
+ SMap.fold
+ (fun _ case (level,tab) ->
+ let ((level, rctx, _), 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
+
+ )
| Case (l, e, ret, branches, default)
(* FIXME: Check that the return type isn't TypeLevel. *)
->
@@ -532,9 +583,9 @@ end
candidats := (browse_lexp nctx d cursor) :: !candidats;
browse_lexp nctx d cursor
| None
- -> if diff > 0 then (); (ctx, Lexp.impossible, Source.Location.dummy)
+ -> if diff > 0 then (); (ctx, None, Lexp.impossible, Source.Location.dummy)
)
- | _,_ -> (ctx, Lexp.impossible, Source.Location.dummy) ;
+ | _,_ -> (ctx, None, Lexp.impossible, Source.Location.dummy) ;
browse_list_lexp !candidats cursor
@@ -565,17 +616,17 @@ end
| (_ak, ((l,_) as vd), atype) :: fargs
-> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l,
buildtype fargs) in
- (ctx, buildtype fargs, location)
+ (ctx, None, buildtype fargs, location)
with Not_found
- -> (ctx, Debruijn.type_int, location)
+ -> (ctx, None, Debruijn.type_int, location)
)
- | _ -> (ctx, Debruijn.type_int, location))
+ | _ -> (ctx, None, Debruijn.type_int, location))
| 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, Lexp.push_susp t s, location))
+ | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, location))
let lexp_parcourir ctx e =
let lctx = Debruijn.ectx_to_lctx ctx in
@@ -587,34 +638,16 @@ end
(*====================================Definition===================================*)
-let rec find_def_location (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Source.Location.t =
+let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Source.Location.t =
- let open Elexp in
- (*let location = Lexp.lexp_location e in*)
- match Lexp.lexp_lexp' e with
- | Imm (Float (l, _)) -> l
- | Imm (Integer (l, _)) -> l
- | Imm (String (l, _)) -> l
- | Imm (Block (l, _)) -> l
- | Imm (Symbol (l,_)) -> l
- | Imm (Node (_, _)) -> Source.Location.dummy
- | SortLevel SLz -> Source.Location.dummy
- | SortLevel (SLsucc e) -> Source.Location.dummy
- | SortLevel (SLlub (e1, e2)) -> Source.Location.dummy
- | Sort (l, Stype e) -> l
- | Sort (l, StypeLevel) -> l
- | Sort (l, StypeOmega) -> l
- | Builtin ((l,_), t) -> l
- | Var (((l, name), idx) as v) -> l
- | Susp (e, s) -> Source.Location.dummy
- | Let (l, defs, e) -> Source.Location.dummy
- | Arrow (ak, v, t1, l, t2) -> let (l,_) = v in l
- | Lambda (ak, ((l,_) as v), t, e) -> l
- | Call (f, args) -> Source.Location.dummy
- | Inductive (l, _label, args, cases) -> l
- | Case (l, e, ret, branches, default) -> l
- | Cons (t, (_l, name)) -> _l
- | Metavar (idx, s, (l,_)) -> l
+ let (ctx,vr,_,loc) = ret in
+
+ match vr with
+ | None -> loc
+ | Some v -> let ((_,_), idx) = v in
+ let ((l,_),_,_) = Myers.nth idx ctx in
+ l
+
(*====================================Definition===================================*)
@@ -670,13 +703,10 @@ class lsp_server =
| 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 r = Option.get(search_lexp_with_a_location list_list typer_loc) 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_lexp,_) = browse_lexp lctx lexp typer_loc in
- let (_, db_index) = lexp in(*let loc = find_def_location lctx lexp typer_loc in*)
- (*failwith (string_of_int (Myers.length l_ctx));*)
- let ((loc,_),_,_) = Myers.nth db_index l_ctx in
+ let (l_ctx, idx,_ ,_ ) as ret = browse_lexp lctx lexp typer_loc in
+ let loc = find_def_location l_ctx ret in
let l = Lsp.Types.Location.create
~uri:uri ~range:(lsp_range_of_loc loc)
in
@@ -692,7 +722,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
@@ -764,23 +794,29 @@ end
(*=======================================Test======================================*)
-let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) =
+
+let comp (a:string) (b:string) : string =
+ if (String.equal a b) then "/*******-----:-):-):-):-):-):-):-)__________SUCCESS_______:-):-):-):-):-):-):-)-----*******/\n\n\n"
+ 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 (list_list, _) = ast in
let (l,c) = position in
let pos = pos_of_tuple position in
let (lctx,lexp) = lexp_search ctx list_list pos in
- let (_, l_type,_) = browse_lexp lctx lexp pos in
- let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\n" in
+ let (_,_, l_type,_) = browse_lexp lctx lexp pos in
+ let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\n\n" in
let input = "input : " ^ content ^ "\n" in
+ let res = "result : " ^ (comp expected (Lexp.lexp_string_for_lsp l_type)) in
let pos = "position : line " ^ (string_of_int l) ^ " character " ^ (string_of_int c) ^ "\n" in
let sep = "################################################\n" in
let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in
- output_string oc (sep ^ input ^ pos ^ output ^ sep);
+ output_string oc (sep ^ input ^ pos ^ output ^ res ^ sep );
close_out oc
let sep name s =
- let content = "/*-----------------------------" ^ s ^ "-----------------------------------*/\n\n\n" in
+ let content = "\n\n\n/*-----------------------------" ^ s ^ "-----------------------------------*/\n\n\n" in
let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in
output_string oc content;
close_out oc
@@ -789,94 +825,96 @@ let test () =
let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
let name = "/home/soilih/Bureau/test/test.txt" in
sep name "INT";
- hoverTest ctx name "e = 12 ;" (1,1);
- hoverTest ctx name "e = 12 ;" (1,5);
+ hoverTest ctx name "e = 12 ;" (1,1) "##Int";
+ hoverTest ctx name "e = 12 ;" (1,5) "##Int";
sep name "STRING";
- hoverTest ctx name "s = \"hejej\" ;" (1,1);
- hoverTest ctx name "s = \"hejej\" ;" (1,8);
+ hoverTest ctx name "s = \"hejej\" ;" (1,1) "##String";
+ hoverTest ctx name "s = \"hejej\" ;" (1,8) "##String";
sep name "FLOAT";
- hoverTest ctx name "f = 12.3 ;" (1,1);
- hoverTest ctx name "f = 12.3 ;" (1,6);
+ hoverTest ctx name "f = 12.3 ;" (1,1) "##Float";
+ hoverTest ctx name "f = 12.3 ;" (1,6) "##Float";
sep name "LAMBDA";
- hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1);
- hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8);
- hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13);
- hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19);
- hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21);
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1) "##Type";
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "##Int";
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13) "##Int";
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19) "(Int -> (Int -> Int))";
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21) "##Int";
sep name "FUNCTION(LAMBDA)";
- hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1);
- hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10);
- hoverTest ctx name "multiply x y z = _*_ x y ;" (1,12);
- hoverTest ctx name "multiply x y z = _*_ x y ;" (1,17);
- hoverTest ctx name "multiply x y z = _*_ x y ;" (1,19);
- hoverTest ctx name "multiply x y z = _*_ x y ;" (1,22);
- hoverTest ctx name "multiply x y z = _*_ x y ;" (1,24);
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "##TypeLevel";
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10) "##Int";
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,12) "##Int";
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,14) "τ";
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,19) "(Int -> (Int -> Int))";
+ hoverTest ctx name "multiply x y z = x + y + z ;" (1,19) "##Int";
+ hoverTest ctx name "multiply x y z = x + y + z ;" (1,23) "##Int";
+ hoverTest ctx name "multiply x y z = x + y + z ;" (1,28) "##Int";
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,26) "##Int";
sep name "CALL";
- hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,1);
- hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,7);
- hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,13);
- hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,15);
- hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,19);
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int";
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,7) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int";
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,13) "##Int";
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,15) "##Int";
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,19) "##String";
sep name "BUILTIN";
- hoverTest ctx name "foo = ##Int ;" (1,1);
- hoverTest ctx name "foo = ##Int ;" (1,9);
+ hoverTest ctx name "foo = ##Int ;" (1,1) "##Type";
+ hoverTest ctx name "foo = ##Int ;" (1,9) "##Type";
sep name "SUSP";
- hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,1);
- hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,6);
+ hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)";
+ hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,6) "(##Type_ ##TypeLevel.z)";
sep name "LIST";
- hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1);
- hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8);
- hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12);
- hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27);
+ 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)";
sep name "ARROW";
- hoverTest ctx name "type Floo = bar Int Int ;" (1,1);
- hoverTest ctx name "type Floo = bar Int Int ;" (1,7);
- hoverTest ctx name "type Floo = bar Int Int ;" (1,18);
- hoverTest ctx name "type Floo = bar Int Int ;" (1,22);
- hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,1);
- hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,19);
- hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,26);
- hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,1);
- 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);
- sep name "INDUCTIVE";
- hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1);
- hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10);
- hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,18);
- hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,24);
- hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,32);
+ hoverTest ctx name "type Floo = bar Int Int ;" (1,1) "";
+ hoverTest ctx name "type Floo = bar Int Int ;" (1,7) "";
+ hoverTest ctx name "type Floo = bar Int Int ;" (1,18) "";
+ hoverTest ctx name "type Floo = bar Int Int ;" (1,22) "";
+ hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,1) "";
+ hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,19) "";
+ hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,26) "";
+ hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,1) "";
+ 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) "";
+ sep name "INDUCTIVE";
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1) "";
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10) "";
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,18) "";
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,24) "";
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,32) "";
sep name "METAVAR";
- hoverTest ctx name "x : ?t = 3 ;" (1,1);
- hoverTest ctx name "x : ?t = 3 ;" (1,6);
- hoverTest ctx name "f x = _+_ ?y x ;" (1,1);
- hoverTest ctx name "f x = _+_ ?y x ;" (1,3);
- hoverTest ctx name "f x = _+_ ?y x ;" (1,12);
- hoverTest ctx name "f x = _+_ ?y x ;" (1,14);
- hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,1);
- hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,6);
- hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,10);
- hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,1);
- hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,11);
- hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,15);
- hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,24);
+ hoverTest ctx name "x : ?t = 3 ;" (1,1) "";
+ hoverTest ctx name "x : ?t = 3 ;" (1,6) "";
+ hoverTest ctx name "f x = _+_ ?y x ;" (1,1) "";
+ hoverTest ctx name "f x = _+_ ?y x ;" (1,3) "";
+ hoverTest ctx name "f x = _+_ ?y x ;" (1,12) "";
+ hoverTest ctx name "f x = _+_ ?y x ;" (1,14) "";
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,1) "";
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,6) "";
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,10) "";
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,1) "";
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,11) "";
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,15) "";
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,24) "";
sep name "LET";
- hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,1);
- hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,10);
- hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,18);
- hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,26);
- hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,35);
- hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,37);
- hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,41);
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,1) "";
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,10) "";
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,18) "";
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,26) "";
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,35) "";
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,37) "";
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,41) "";
sep name "CASE";
- hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,1);
- hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,5);
- hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,14);
- 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\" ;" (1,1) "";
+ hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,5) "";
+ hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,14) "";
+ 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) ""
(*=======================================Test======================================*)
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/29b5783adf187f83516e8b0381c2c2f5…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/29b5783adf187f83516e8b0381c2c2f5…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][soilih] 2 commits: test hover
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 13 Jul '21
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 13 Jul '21
13 Jul '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
5025a06d by Soilih BEN SOILIH at 2021-07-13T10:53:05-06:00
test hover
- - - - -
29b5783a by Soilih BEN SOILIH at 2021-07-13T10:55:44-06:00
test hover.
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
=====================================
src/typer_lsp_server.ml
=====================================
@@ -55,6 +55,12 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t =
| Info -> Lsp.Types.DiagnosticSeverity.Information
| _ -> Lsp.Types.DiagnosticSeverity.Hint
+let pos_of_tuple (p:int * int) : Source.Location.t =
+ let (line,col) = p in
+ let open Source.Location in
+ let dc = Some "" in
+ let typer_pos = {file = ""; start_line = line; start_column = col; end_line = line; end_column = col; doc = dc } in
+ typer_pos
let typer_pos_of_lsp_pos (p:Lsp.Types.Position.t) : Source.Location.t =
let open Source.Location in
@@ -287,17 +293,17 @@ end
else foo (ml::tl) cursor
in foo lexp_list cursor
- let browse_list_lexp (tab:(Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) =
+ let browse_list_lexp (tab:(Debruijn.lexp_context * Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) =
let rec foo tab cursor =
match tab with
| [] -> failwith "Liste vide!"
| [n] -> n
- | [hd;tl] -> let (_,loc_hd) = hd in
- let (_,loc_tl) = tl in
+ | [hd;tl] -> let (_,_,loc_hd) = hd in
+ let (_,_,loc_tl) = tl in
if (dist loc_hd cursor < dist loc_tl cursor ) then hd
else tl
- |hd::ml::tl -> let (_,loc_hd) = hd in
- let (_,loc_ml) = ml in
+ |hd::ml::tl -> let (_,_,loc_hd) = hd in
+ let (_,_,loc_ml) = ml in
if (dist loc_hd cursor < dist loc_ml cursor ) then (foo (hd::tl) cursor)
else foo (ml::tl) cursor
in foo tab cursor
@@ -330,26 +336,27 @@ end
(lctx,lexp)
(* search the type of a lexp browsing a lexp*)
- let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Lexp.lexp * Source.Location.t =
+ let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Debruijn.lexp_context * Lexp.lexp * Source.Location.t =
let open Elexp in
let location = Lexp.lexp_location e in
match Lexp.lexp_lexp' e with
- | Imm (Float (_, _)) -> (Debruijn.type_float, location)
- | Imm (Integer (_, _)) -> (Debruijn.type_int, location)
- | Imm (String (_, _)) -> (Debruijn.type_string, location)
- | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (Debruijn.type_string, location)
- | SortLevel SLz -> (Debruijn.type_level, location)
+ | Imm (Float (_, _)) -> (ctx, Debruijn.type_float, location)
+ | Imm (Integer (_, _)) -> (ctx, Debruijn.type_int, location)
+ | Imm (String (_, _)) -> (ctx, Debruijn.type_string, location)
+ | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (ctx, Debruijn.type_string, location)
+ | SortLevel SLz -> (ctx, Debruijn.type_level, location)
| SortLevel (SLsucc e)
- -> (Debruijn.type_level, location)
+ -> (ctx, Debruijn.type_level, location)
| SortLevel (SLlub (e1, e2))
- -> (Debruijn.type_level, location)
+ -> (ctx, Debruijn.type_level, location)
| Sort (l, Stype e)
- -> (Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location)
- | Sort (_, StypeLevel) -> (Debruijn.sort_omega, location)
- | Sort (_, StypeOmega) -> (Debruijn.sort_omega, location)
- | Builtin (_, t)-> (t, location)
- | Var (((l, name), idx) as v) -> (Debruijn.lctx_lookup_type ctx v, location)
+ -> (ctx, Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location)
+ | Sort (_, StypeLevel) -> (ctx, Debruijn.sort_omega, location)
+ | Sort (_, StypeOmega) -> (ctx, Debruijn.sort_omega, location)
+ | Builtin (_, t)-> (ctx, t, location)
+ | Var (((l, name), idx) as v) ->
+ (ctx, Debruijn.lctx_lookup_type ctx v, location)
| Susp (e, s) -> browse_lexp ctx (Lexp.push_susp e s) cursor
| Let (l, defs, e)
-> let ctx' =
@@ -364,31 +371,32 @@ end
defs
in
- let (ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in
+ let (ctx'', ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in
- (Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc)
+ (ctx'', Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc)
| Arrow (ak, v, t1, l, t2)
-> (
let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in
match Opslexp.sort_compose ctx nctx l ak t1 t2 with
- | SortResult k -> (k, location)
+ | SortResult k -> (nctx, k, location)
| SortInvalid
- -> (Lexp.mkSort (l, StypeOmega), location)
+ -> (nctx, Lexp.mkSort (l, StypeOmega), location)
| SortK1NotType
- -> (Lexp.mkSort (l, StypeOmega), location)
+ -> (nctx, Lexp.mkSort (l, StypeOmega), location)
| SortK2NotType
- -> (Lexp.mkSort (l, StypeOmega), location)
+ -> (nctx, 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 (ret,loc) = browse_list_lexp (a::b::[]) cursor in
- (Lexp.mkArrow (ak, v, t, l,ret), loc)
+ let c = (ctx,t,l) in
+ let (ctx'',ret,loc) = browse_list_lexp (a::b::c::[]) cursor in
+ (ctx'', ret, loc)
| Call (f, args)
-> (
- let fonc = browse_lexp ctx f cursor in
+ let fonc = browse_lexp ctx f cursor in
let args_list = List.map
(fun (_ , e) -> browse_lexp ctx e cursor)
args
@@ -398,14 +406,15 @@ end
)
| Inductive (l, _label, args, cases)
- ->(
+ ->(
+
let rec arg_loop ctx erased args =
match args with
| []
-> let level
= SMap.fold
(fun _ case level ->
- let (level, _, _, _) =
+ let (level, rctx, _, _) =
List.fold_left
(fun (level, ictx, erased, n) (ak, v, t) ->
((let lwhnf = Opslexp.lexp_whnf t ictx in
@@ -415,10 +424,6 @@ end
-> level
| Sort (_, Stype level')
-> Opslexp.mkSLlub ctx level
- (* We need to unshift because the final type
- * cannot refer to the fields! *)
- (* FIXME: If it does refer,
- * we get an ugly error! *)
(Lexp.mkSusp level' (Lexp.sunshift n))
| _tt -> level),
Debruijn.lctx_extend ictx v Variable t,
@@ -428,7 +433,7 @@ end
case in
level)
cases (Lexp.mkSortLevel SLz) in
- Lexp.mkSort (l, Stype level)
+ Lexp.mkSort (l, Stype level)
| (ak, v, t)::args
-> let _k = t in
Lexp.mkArrow (ak, v, t, Lexp.lexp_location t,
@@ -436,7 +441,7 @@ end
(Opslexp.dbset_push ak erased)
args) in
let tct = arg_loop ctx Debruijn.set_empty args in
- (tct, location)
+ (ctx, tct, location)
)
| Case (l, e, ret, branches, default)
@@ -524,12 +529,12 @@ end
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;
+ candidats := (browse_lexp nctx d cursor) :: !candidats;
browse_lexp nctx d cursor
| None
- -> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy)
+ -> if diff > 0 then (); (ctx, Lexp.impossible, Source.Location.dummy)
)
- | _,_ -> (Lexp.impossible, Source.Location.dummy) ;
+ | _,_ -> (ctx, Lexp.impossible, Source.Location.dummy) ;
browse_list_lexp !candidats cursor
@@ -560,18 +565,17 @@ end
| (_ak, ((l,_) as vd), atype) :: fargs
-> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l,
buildtype fargs) in
- (buildtype fargs, location)
+ (ctx, buildtype fargs, location)
with Not_found
- -> (Debruijn.type_int, location)
+ -> (ctx, Debruijn.type_int, location)
)
- | _ -> (Debruijn.type_int, location))
+ | _ -> (ctx, Debruijn.type_int, location))
| Metavar (idx, s, _)
-> (match Lexp.metavar_lookup idx with
| MVal e -> let e = Lexp.push_susp e s in
- let (e', loc) = browse_lexp ctx e cursor in
- (e',loc)
- | MVar (_, t, _) -> (Lexp.push_susp t s, location))
+ browse_lexp ctx e cursor
+ | MVar (_, t, _) -> (ctx, Lexp.push_susp t s, location))
let lexp_parcourir ctx e =
let lctx = Debruijn.ectx_to_lctx ctx in
@@ -588,27 +592,29 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Sour
let open Elexp in
(*let location = Lexp.lexp_location e in*)
match Lexp.lexp_lexp' e with
- | Imm (Float (_, _)) -> Source.Location.dummy
- | Imm (Integer (_, _)) -> Source.Location.dummy
- | Imm (String (_, _)) -> Source.Location.dummy
- | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> Source.Location.dummy
+ | Imm (Float (l, _)) -> l
+ | Imm (Integer (l, _)) -> l
+ | Imm (String (l, _)) -> l
+ | Imm (Block (l, _)) -> l
+ | Imm (Symbol (l,_)) -> l
+ | Imm (Node (_, _)) -> Source.Location.dummy
| SortLevel SLz -> Source.Location.dummy
| SortLevel (SLsucc e) -> Source.Location.dummy
| SortLevel (SLlub (e1, e2)) -> Source.Location.dummy
- | Sort (l, Stype e) -> Source.Location.dummy
- | Sort (_, StypeLevel) -> Source.Location.dummy
- | Sort (_, StypeOmega) -> Source.Location.dummy
- | Builtin (_, t) -> Source.Location.dummy
- | Var (((l, name), idx) as v) -> Source.Location.dummy
+ | Sort (l, Stype e) -> l
+ | Sort (l, StypeLevel) -> l
+ | Sort (l, StypeOmega) -> l
+ | Builtin ((l,_), t) -> l
+ | Var (((l, name), idx) as v) -> l
| Susp (e, s) -> Source.Location.dummy
| Let (l, defs, e) -> Source.Location.dummy
- | Arrow (ak, v, t1, l, t2) -> Source.Location.dummy
- | Lambda (ak, ((l,_) as v), t, e) -> Source.Location.dummy
+ | Arrow (ak, v, t1, l, t2) -> let (l,_) = v in l
+ | Lambda (ak, ((l,_) as v), t, e) -> l
| Call (f, args) -> Source.Location.dummy
- | Inductive (l, _label, args, cases) -> Source.Location.dummy
- | Case (l, e, ret, branches, default) -> Source.Location.dummy
- | Cons (t, (_l, name)) -> Source.Location.dummy
- | Metavar (idx, s, _) -> Source.Location.dummy
+ | Inductive (l, _label, args, cases) -> l
+ | Case (l, e, ret, branches, default) -> l
+ | Cons (t, (_l, name)) -> _l
+ | Metavar (idx, s, (l,_)) -> l
(*====================================Definition===================================*)
@@ -667,7 +673,10 @@ class lsp_server =
(*let r = Option.get(search_lexp_with_a_location list_list typer_loc) in*)
let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
let (lctx,lexp) = lexp_search ctx list_list typer_loc in
- let loc = find_def_location lctx lexp typer_loc in
+ let (l_ctx, l_lexp,_) = browse_lexp lctx lexp typer_loc in
+ let (_, db_index) = lexp in(*let loc = find_def_location lctx lexp typer_loc in*)
+ (*failwith (string_of_int (Myers.length l_ctx));*)
+ let ((loc,_),_,_) = Myers.nth db_index l_ctx in
let l = Lsp.Types.Location.create
~uri:uri ~range:(lsp_range_of_loc loc)
in
@@ -675,7 +684,6 @@ class lsp_server =
let f = Linol_lwt.return (Some ret) in
f
-
method! on_req_hover ~notify_back ~id ~uri ~pos doc_state =
match Hashtbl.find buffers uri with
@@ -684,7 +692,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_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
@@ -717,7 +725,7 @@ class lsp_server =
emacs. It makes completion too slow *)
Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; "\""; "'"; "/"; "@"; "<"]
~resolveProvider:true () in
- { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider }
+ { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider}
(* provisional, to be done later *)
@@ -754,12 +762,133 @@ class lsp_server =
end
+
+(*=======================================Test======================================*)
+let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) =
+ let (_, ast) = readstring content in
+ let (list_list, _) = ast in
+ let (l,c) = position in
+ let pos = pos_of_tuple position in
+ let (lctx,lexp) = lexp_search ctx list_list pos in
+ let (_, l_type,_) = browse_lexp lctx lexp pos in
+ let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\n" in
+ let input = "input : " ^ content ^ "\n" in
+ let pos = "position : line " ^ (string_of_int l) ^ " character " ^ (string_of_int c) ^ "\n" in
+ let sep = "################################################\n" in
+ let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in
+ output_string oc (sep ^ input ^ pos ^ output ^ sep);
+ close_out oc
+
+let sep name s =
+ let content = "/*-----------------------------" ^ s ^ "-----------------------------------*/\n\n\n" in
+ let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in
+ 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";
+ hoverTest ctx name "e = 12 ;" (1,1);
+ hoverTest ctx name "e = 12 ;" (1,5);
+ sep name "STRING";
+ hoverTest ctx name "s = \"hejej\" ;" (1,1);
+ hoverTest ctx name "s = \"hejej\" ;" (1,8);
+ sep name "FLOAT";
+ hoverTest ctx name "f = 12.3 ;" (1,1);
+ hoverTest ctx name "f = 12.3 ;" (1,6);
+ sep name "LAMBDA";
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1);
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8);
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13);
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19);
+ hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21);
+ sep name "FUNCTION(LAMBDA)";
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1);
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10);
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,12);
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,17);
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,19);
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,22);
+ hoverTest ctx name "multiply x y z = _*_ x y ;" (1,24);
+ sep name "CALL";
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,1);
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,7);
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,13);
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,15);
+ hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,19);
+ sep name "BUILTIN";
+ hoverTest ctx name "foo = ##Int ;" (1,1);
+ hoverTest ctx name "foo = ##Int ;" (1,9);
+ sep name "SUSP";
+ hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,1);
+ hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,6);
+ sep name "LIST";
+ hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1);
+ hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8);
+ hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12);
+ hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27);
+ sep name "ARROW";
+ hoverTest ctx name "type Floo = bar Int Int ;" (1,1);
+ hoverTest ctx name "type Floo = bar Int Int ;" (1,7);
+ hoverTest ctx name "type Floo = bar Int Int ;" (1,18);
+ hoverTest ctx name "type Floo = bar Int Int ;" (1,22);
+ hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,1);
+ hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,19);
+ hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,26);
+ hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,1);
+ 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);
+ sep name "INDUCTIVE";
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1);
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10);
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,18);
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,24);
+ hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,32);
+ sep name "METAVAR";
+ hoverTest ctx name "x : ?t = 3 ;" (1,1);
+ hoverTest ctx name "x : ?t = 3 ;" (1,6);
+ hoverTest ctx name "f x = _+_ ?y x ;" (1,1);
+ hoverTest ctx name "f x = _+_ ?y x ;" (1,3);
+ hoverTest ctx name "f x = _+_ ?y x ;" (1,12);
+ hoverTest ctx name "f x = _+_ ?y x ;" (1,14);
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,1);
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,6);
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,10);
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,1);
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,11);
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,15);
+ hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,24);
+ sep name "LET";
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,1);
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,10);
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,18);
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,26);
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,35);
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,37);
+ hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,41);
+ sep name "CASE";
+ hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,1);
+ hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,5);
+ hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,14);
+ 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)
+
+
+(*=======================================Test======================================*)
+
+
(* Main code
This is the code that creates an instance of the lsp server class
and runs it as a task. *)
let run () =
ignore (Arg.Set Log.lsp_enabled);
Logs.set_level ~all:true (Some Logs.Debug);
+ 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/-/compare/ba970f5cec20dca8236971c1352bfeaf…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ba970f5cec20dca8236971c1352bfeaf…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][soilih] fixing the case Case
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 03 Jul '21
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 03 Jul '21
03 Jul '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
ba970f5c by Soilih BEN SOILIH at 2021-07-03T00:29:12-06:00
fixing the case Case
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
=====================================
src/typer_lsp_server.ml
=====================================
@@ -508,7 +508,7 @@ end
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 ctx branch cursor) :: !candidats;
+ candidats := (browse_lexp nctx branch cursor) :: !candidats;
)
brch
in
@@ -525,7 +525,7 @@ end
let (nerased, nctx) =
ctx_extend_with_eq nctx subst hlxp in
candidats := (browse_lexp ctx d cursor) :: !candidats;
- browse_lexp ctx d cursor
+ browse_lexp nctx d cursor
| None
-> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy)
)
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ba970f5cec20dca8236971c1352bfeaf8…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ba970f5cec20dca8236971c1352bfeaf8…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][soilih] remove unecessary try with
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 03 Jul '21
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 03 Jul '21
03 Jul '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
8e377da2 by Soilih BEN SOILIH at 2021-07-02T23:22:44-06:00
remove unecessary try with
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
=====================================
src/typer_lsp_server.ml
=====================================
@@ -279,7 +279,7 @@ end
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!"
+ | [] -> 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
@@ -394,9 +394,7 @@ end
args
in
- try
browse_list_lexp (fonc::args_list) cursor
- with exe -> failwith "Exeption sur ce call !!!"
)
| Inductive (l, _label, args, cases)
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8e377da2a811e4eead746c3beab8d3b4c…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8e377da2a811e4eead746c3beab8d3b4c…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][soilih] fixing let, adding got to definition
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 03 Jul '21
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 03 Jul '21
03 Jul '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
d83e49da by Soilih BEN SOILIH at 2021-07-02T23:07:13-06:00
fixing let, adding got to definition
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
=====================================
src/typer_lsp_server.ml
=====================================
@@ -94,12 +94,17 @@ let vname_to_lsp_loc ~(vname: Util.vname) ~uri : Lsp.Types.Location.t =
Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc location)
-let rec search_lexp_with_a_location (lexp_list: Lexp.lexp list) (location : Source.Location.t): Lexp.lexp option =
- match lexp_list with
- | [] -> None
- | hd::tl -> let r = Lexp.lexp_location hd in
- if ((r.start_line - 1) == location.start_line) && ((r.start_column - 1) == location.start_column) then Some hd
- else search_lexp_with_a_location tl location
+let rec search_lexp_with_a_location (list_list: (vname * Lexp.lexp * Lexp.ltype) list list) (location : Source.Location.t): Lexp.lexp option =
+ 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 rec foo (tab:Lexp.lexp list) (loc:Source.Location.t) =
+ match tab with
+ | [] -> None
+ | hd::tl -> let r = Lexp.lexp_location hd in
+ if ((r.start_line - 1) == loc.start_line) && ((r.start_column - 1) == loc.start_column) then Some hd
+ else foo tl loc
+ in
+ foo lexp_list location
let readstring (str:string) =
Log.clear_log () ;
@@ -325,245 +330,250 @@ end
(lctx,lexp)
(* search the type of a lexp browsing a lexp*)
- let rec browse_lexp ctx e cursor =
+ let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Lexp.lexp * Source.Location.t =
- let open Elexp in
- let location = Lexp.lexp_location e in
- match Lexp.lexp_lexp' e with
- | Imm (Float (_, _)) -> (Debruijn.type_float, location)
- | Imm (Integer (_, _)) -> (Debruijn.type_int, location)
- | Imm (String (_, _)) -> (Debruijn.type_string, location)
- | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (Debruijn.type_string, location)
- | SortLevel SLz -> (Debruijn.type_level, location)
- | SortLevel (SLsucc e)
- -> (Debruijn.type_level, location)
- | SortLevel (SLlub (e1, e2))
- -> (Debruijn.type_level, location)
- | Sort (l, Stype e)
- -> (Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location)
- | Sort (_, StypeLevel) -> (Debruijn.sort_omega, location)
- | Sort (_, StypeOmega) -> (Debruijn.sort_omega, location)
- | Builtin (_, t)-> (t, location)
- | Var (((l, name), idx) as v) -> (Debruijn.lctx_lookup_type ctx v, location)
- | Susp (e, s) -> browse_lexp ctx (Lexp.push_susp e s) cursor
- | Let (l, defs, e)
- -> let _ =
- List.fold_left (fun ctx (v, _e, t)
- -> (Debruijn.lctx_extend ctx v ForwardRef t))
- ctx defs in
- (* FIXME: Termination checking! Positivity-checker! *)
- let _ = List.fold_left (fun n (_v, e, t)
- -> n - 1)
- (List.length defs) defs in
- let (e',loc) = browse_lexp ctx e cursor in
- (Lexp.mkSusp e' (Opslexp.lexp_defs_subst l Subst.identity defs),loc)
-
- | Arrow (ak, v, t1, l, t2)
- -> (
- let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in
- match Opslexp.sort_compose ctx nctx l ak t1 t2 with
- | SortResult k -> (k, location)
- | SortInvalid
- -> (Lexp.mkSort (l, StypeOmega), location)
- | SortK1NotType
- -> (Lexp.mkSort (l, StypeOmega), location)
- | SortK2NotType
- -> (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 (ret,loc) = browse_list_lexp (a::b::[]) cursor in
- (Lexp.mkArrow (ak, v, t, l,ret), loc)
-
- | 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
-
- try
- browse_list_lexp (fonc::args_list) cursor
- with exe -> failwith "Exeption sur ce call !!!"
- )
-
- | Inductive (l, _label, args, cases)
- ->(
- let rec arg_loop ctx erased args =
- match args with
- | []
- -> let level
- = SMap.fold
- (fun _ case level ->
- let (level, _, _, _) =
- List.fold_left
- (fun (level, ictx, erased, n) (ak, v, t) ->
- ((let lwhnf = Opslexp.lexp_whnf t ictx in
- match Lexp.lexp_lexp' lwhnf with
- | Sort (_, Stype _)
- when ak == Pexp.Aerasable
- -> level
- | Sort (_, Stype level')
- -> Opslexp.mkSLlub ctx level
- (* We need to unshift because the final type
- * cannot refer to the fields! *)
- (* FIXME: If it does refer,
- * we get an ugly error! *)
- (Lexp.mkSusp level' (Lexp.sunshift n))
- | _tt -> level),
- Debruijn.lctx_extend ictx v Variable t,
- Debruijn.set_sink 1 erased,
- n + 1))
- (level, ctx, erased, 0)
- case in
- level)
- cases (Lexp.mkSortLevel SLz) in
- Lexp.mkSort (l, Stype level)
- | (ak, v, t)::args
- -> let _k = t in
- Lexp.mkArrow (ak, v, t, Lexp.lexp_location t,
- arg_loop (Debruijn.lctx_extend ctx v Variable t)
- (Opslexp.dbset_push ak erased)
- args) in
- 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
- 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
- let elvl = match Opslexp.lexp'_whnf ekind ctx with
- | Sort (_, Stype l) -> l
- | _ -> Debruijn.level0 in
- let erased = Debruijn.set_empty in
- 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
- | [], [] -> s
- | _farg::fargs, (_ak, aarg)::aargs
- (* We don't check aarg's type, because we assume that `check`
- * returns a valid type. *)
- -> mksubst (Subst.cons aarg s) fargs aargs
- | _,_ -> s in
- let s = mksubst Subst.identity fargs aargs in
- let ctx_extend_with_eq ctx subst hlxp =
- let tlxp = Lexp.mkSusp e subst in
- let tltp = Lexp.mkSusp etype subst in
- let tlvl = Lexp.mkSusp elvl subst in
- let eqty = Lexp.mkCall (Debruijn.type_eq,
- [(Lexp.Aerasable, tlvl); (* Typelevel *)
- (Lexp.Aerasable, tltp); (* Inductive type *)
- (Lexp.Anormal, hlxp); (* Lexp of the branch head *)
- (Lexp.Anormal, tlxp)]) in (* Target lexp *)
- (* The eq proof is erasable. *)
- let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in
- (erased, nctx) in
-
- let brch = SMap.bindings branches in
- let lst =
- List.map
+ let open Elexp in
+ let location = Lexp.lexp_location e in
+ match Lexp.lexp_lexp' e with
+ | Imm (Float (_, _)) -> (Debruijn.type_float, location)
+ | Imm (Integer (_, _)) -> (Debruijn.type_int, location)
+ | Imm (String (_, _)) -> (Debruijn.type_string, location)
+ | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (Debruijn.type_string, location)
+ | SortLevel SLz -> (Debruijn.type_level, location)
+ | SortLevel (SLsucc e)
+ -> (Debruijn.type_level, location)
+ | SortLevel (SLlub (e1, e2))
+ -> (Debruijn.type_level, location)
+ | Sort (l, Stype e)
+ -> (Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location)
+ | Sort (_, StypeLevel) -> (Debruijn.sort_omega, location)
+ | Sort (_, StypeOmega) -> (Debruijn.sort_omega, location)
+ | Builtin (_, t)-> (t, location)
+ | Var (((l, name), idx) as v) -> (Debruijn.lctx_lookup_type ctx v, location)
+ | Susp (e, s) -> browse_lexp ctx (Lexp.push_susp e s) cursor
+ | 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 tab = List.map
+ (fun (vn,lxp,ltp) ->
+ browse_lexp ctx' lxp cursor
+ )
+ defs
+ in
+
+ let (ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in
+
+ (Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc)
+
+ | Arrow (ak, v, t1, l, t2)
+ -> (
+ let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in
+ match Opslexp.sort_compose ctx nctx l ak t1 t2 with
+ | SortResult k -> (k, location)
+ | SortInvalid
+ -> (Lexp.mkSort (l, StypeOmega), location)
+ | SortK1NotType
+ -> (Lexp.mkSort (l, StypeOmega), location)
+ | SortK2NotType
+ -> (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 (ret,loc) = browse_list_lexp (a::b::[]) cursor in
+ (Lexp.mkArrow (ak, v, t, l,ret), loc)
+
+ | 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
+
+ try
+ browse_list_lexp (fonc::args_list) cursor
+ with exe -> failwith "Exeption sur ce call !!!"
+ )
+
+ | Inductive (l, _label, args, cases)
+ ->(
+ let rec arg_loop ctx erased args =
+ match args with
+ | []
+ -> let level
+ = SMap.fold
+ (fun _ case level ->
+ let (level, _, _, _) =
+ List.fold_left
+ (fun (level, ictx, erased, n) (ak, v, t) ->
+ ((let lwhnf = Opslexp.lexp_whnf t ictx in
+ match Lexp.lexp_lexp' lwhnf with
+ | Sort (_, Stype _)
+ when ak == Pexp.Aerasable
+ -> level
+ | Sort (_, Stype level')
+ -> Opslexp.mkSLlub ctx level
+ (* We need to unshift because the final type
+ * cannot refer to the fields! *)
+ (* FIXME: If it does refer,
+ * we get an ugly error! *)
+ (Lexp.mkSusp level' (Lexp.sunshift n))
+ | _tt -> level),
+ Debruijn.lctx_extend ictx v Variable t,
+ Debruijn.set_sink 1 erased,
+ n + 1))
+ (level, ctx, erased, 0)
+ case in
+ level)
+ cases (Lexp.mkSortLevel SLz) in
+ Lexp.mkSort (l, Stype level)
+ | (ak, v, t)::args
+ -> let _k = t in
+ Lexp.mkArrow (ak, v, t, Lexp.lexp_location t,
+ arg_loop (Debruijn.lctx_extend ctx v Variable t)
+ (Opslexp.dbset_push ak erased)
+ args) in
+ 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
+ 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
+ let elvl = match Opslexp.lexp'_whnf ekind ctx with
+ | Sort (_, Stype l) -> l
+ | _ -> Debruijn.level0 in
+ let erased = Debruijn.set_empty in
+ 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
+ | [], [] -> s
+ | _farg::fargs, (_ak, aarg)::aargs
+ (* We don't check aarg's type, because we assume that `check`
+ * returns a valid type. *)
+ -> mksubst (Subst.cons aarg s) fargs aargs
+ | _,_ -> s in
+ let s = mksubst Subst.identity fargs aargs in
+ let ctx_extend_with_eq ctx subst hlxp =
+ let tlxp = Lexp.mkSusp e subst in
+ let tltp = Lexp.mkSusp etype subst in
+ let tlvl = Lexp.mkSusp elvl subst in
+ let eqty = Lexp.mkCall (Debruijn.type_eq,
+ [(Lexp.Aerasable, tlvl); (* Typelevel *)
+ (Lexp.Aerasable, tltp); (* Inductive type *)
+ (Lexp.Anormal, hlxp); (* Lexp of the branch head *)
+ (Lexp.Anormal, tlxp)]) in (* Target lexp *)
+ (* The eq proof is erasable. *)
+ let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in
+ (erased, nctx) in
+
+ let brch = SMap.bindings branches in
+ let lst =
+ List.map
+ (
+ 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
+ | [], [] -> (erased, ctx, hlxp)
+ (* 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)
+ (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))]))
+ vdefs fieldtypes
+ | _,_ -> (erased, ctx, hlxp) in
+ let hctor =
+ Lexp.mkCall (Lexp.mkCons (it, (l, name)),
+ List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in
+ 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 ctx branch cursor) :: !candidats;
+ )
+ brch
+ in
+
+ let diff = SMap.cardinal constructors - List.length lst in
(
- 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
- | [], [] -> (erased, ctx, hlxp)
- (* 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)
- (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))]))
- vdefs fieldtypes
- | _,_ -> (erased, ctx, hlxp) in
- let hctor =
- Lexp.mkCall (Lexp.mkCons (it, (l, name)),
- List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in
- 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 ctx branch cursor) :: !candidats;
+ match default with
+ | Some (v, d)
+ -> if diff <= 0 then ();
+ let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in
+ let nerased = Debruijn.set_sink 1 erased in
+ let subst = Subst.shift 1 in
+ 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)
)
- brch
- in
+ | _,_ -> (Lexp.impossible, Source.Location.dummy) ;
- 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 nerased = Debruijn.set_sink 1 erased in
- let subst = Subst.shift 1 in
- 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) ;
-
- browse_list_lexp !candidats cursor
+ browse_list_lexp !candidats cursor
- )
-
+ )
+
+
+ | 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
+ (buildtype fargs, location)
+ with Not_found
+ -> (Debruijn.type_int, location)
+ )
+ | _ -> (Debruijn.type_int, location))
- | 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
- (buildtype fargs, location)
- with Not_found
- -> (Debruijn.type_int, location)
- )
- | _ -> (Debruijn.type_int, location))
-
- | Metavar (idx, s, _)
- -> (match Lexp.metavar_lookup idx with
- | MVal e -> let e = Lexp.push_susp e s in
- let (e', loc) = browse_lexp ctx e cursor in
- (e',loc)
- | MVar (_, t, _) -> (Lexp.push_susp t s, location))
+ | Metavar (idx, s, _)
+ -> (match Lexp.metavar_lookup idx with
+ | MVal e -> let e = Lexp.push_susp e s in
+ let (e', loc) = browse_lexp ctx e cursor in
+ (e',loc)
+ | MVar (_, t, _) -> (Lexp.push_susp t s, location))
let lexp_parcourir ctx e =
let lctx = Debruijn.ectx_to_lctx ctx in
@@ -573,6 +583,37 @@ end
(*====================================Lexp parcourir===================================*)
+(*====================================Definition===================================*)
+
+let rec find_def_location (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Source.Location.t =
+
+ let open Elexp in
+ (*let location = Lexp.lexp_location e in*)
+ match Lexp.lexp_lexp' e with
+ | Imm (Float (_, _)) -> Source.Location.dummy
+ | Imm (Integer (_, _)) -> Source.Location.dummy
+ | Imm (String (_, _)) -> Source.Location.dummy
+ | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> Source.Location.dummy
+ | SortLevel SLz -> Source.Location.dummy
+ | SortLevel (SLsucc e) -> Source.Location.dummy
+ | SortLevel (SLlub (e1, e2)) -> Source.Location.dummy
+ | Sort (l, Stype e) -> Source.Location.dummy
+ | Sort (_, StypeLevel) -> Source.Location.dummy
+ | Sort (_, StypeOmega) -> Source.Location.dummy
+ | Builtin (_, t) -> Source.Location.dummy
+ | Var (((l, name), idx) as v) -> Source.Location.dummy
+ | Susp (e, s) -> Source.Location.dummy
+ | Let (l, defs, e) -> Source.Location.dummy
+ | Arrow (ak, v, t1, l, t2) -> Source.Location.dummy
+ | Lambda (ak, ((l,_) as v), t, e) -> Source.Location.dummy
+ | Call (f, args) -> Source.Location.dummy
+ | Inductive (l, _label, args, cases) -> Source.Location.dummy
+ | Case (l, e, ret, branches, default) -> Source.Location.dummy
+ | Cons (t, (_l, name)) -> Source.Location.dummy
+ | Metavar (idx, s, _) -> Source.Location.dummy
+
+(*====================================Definition===================================*)
+
(* Lsp server class
This is the main point of interaction beetween the code checking documents
@@ -624,11 +665,11 @@ class lsp_server =
| state_after_processing -> let (_,ast) = state_after_processing 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
- let r = Option.get(search_lexp_with_a_location lexp_list typer_loc) in
- let loc = Lexp.lexp_location r in
+ (*let r = Option.get(search_lexp_with_a_location list_list typer_loc) in*)
+ let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
+ let (lctx,lexp) = lexp_search ctx list_list typer_loc in
+ let loc = find_def_location lctx lexp typer_loc in
let l = Lsp.Types.Location.create
~uri:uri ~range:(lsp_range_of_loc loc)
in
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/d83e49da8e6622a58d40f6a330ee7311f…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/d83e49da8e6622a58d40f6a330ee7311f…
You're receiving this email because of your account on gitlab.com.
1
0