Typer Juillet 2021

typer@iro.umontreal.ca

1 participants
5 discussions

[Git][monnier/typer][soilih] 2 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 21 Jul '21

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

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

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) 02 Jul '21

02 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) 02 Jul '21

02 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

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Juillet 2021