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/29b5783adf187f83516e8b0381c2c2f50...