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

Commits: a1a11af5 by Soilih BEN SOILIH at 2021-05-26T02:37:49-06:00 browse lexp update

- - - - -

3 changed files:

- + samples/.#acc.typer - src/log.ml - src/typer_lsp_server.ml

Changes:

===================================== samples/.#acc.typer ===================================== @@ -0,0 +1 @@ +soilih@soilih-HP-Laptop-15-db0xxx.11163:1621953914 \ No newline at end of file

===================================== src/log.ml ===================================== @@ -193,6 +193,7 @@ let log_fatal ?section ?print_action ?loc m = internal_error "Compiler Fatal Error"

+ let log_error = log_msg Error ?kind:None let log_warning = log_msg Warning ?kind:None let log_info = log_msg Info ?kind:None

===================================== src/typer_lsp_server.ml ===================================== @@ -103,7 +103,6 @@ let rec search_lexp_with_a_location (lexp_list: Lexp.lexp list) (location : Sour

let readstring (str:string) = Log.clear_log () ; - Arg.Set Log.lsp_enabled; let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) let ast = Elab.lexp_decl_str str ectx in @@ -309,12 +308,13 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list 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 call_split (e: Lexp.lexp) = match Lexp.lexp_lexp' e with | Call (f, args) -> (f, args) @@ -353,8 +353,10 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in (erased, nctx) in

- let foo = - (fun name (l, vdefs, branch) + 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 @@ -375,15 +377,16 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list 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 - browse_lexp ctx branch cursor; + ignore (browse_lexp ctx branch cursor); (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1))) + ) - in - let lst = foo (Lexp.get_name branches) branches in - let brch = SMap.bindings lst in + brch + in

- let diff = SMap.cardinal constructors - SMap.cardinal brch in - (match default with + 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 @@ -392,12 +395,14 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let hlxp = Lexp.mkVar ((l, None), 0) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in - (Lexp.mkSusp ret (Subst.shift 2)) + browse_lexp ctx d cursor | None - -> if diff > 0 then () ) - | _,_ -> ())); + -> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy) + ) + | _,_ -> (Lexp.impossible, Source.Location.dummy) ); + (ret,location) - + )

@@ -442,6 +447,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let lctx = Debruijn.ectx_to_lctx ctx in let location = Lexp.lexp_location e in (Opslexp.get_type lctx e , location) + (*====================================Lexp parcourir===================================*)

@@ -585,6 +591,7 @@ end 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); 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/-/commit/a1a11af523dcfe97f455c4ccc373627931...