Soilihi BEN SOILIHI BOINA pushed to branch wop-server at Stefan / Typer
Commits: 715e3ba7 by Soilih at 2022-08-26T13:24:02-04:00 -
- - - - -
5 changed files:
- dune - src/dune - src/typer_lsp_server.ml - typer.ml - + typer_server.ml
Changes:
===================================== dune ===================================== @@ -13,3 +13,10 @@ (modules debug_util) (libraries typerlib) (modes byte native)) + +(executable + (name typer_server) + (promote (until-clean)) + (modules typer_server) + (libraries typerlib typerserver) + (modes byte native)) \ No newline at end of file
===================================== src/dune ===================================== @@ -1,7 +1,12 @@ ;; -*- lisp-data -*-
(library + (modules typer) (name typerlib) - (libraries zarith str linol linol-lwt - lsp jsonrpc)) + (libraries zarith str))
+(library + (modules typer_server) + (name typerserver) + (libraries linol linol-lwt + lsp jsonrpc)) \ No newline at end of file
===================================== src/typer_lsp_server.ml ===================================== @@ -511,8 +511,6 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De | _ -> (e,[]) in candidats := (browse_lexp ctx e cursor lst_in):: !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 @@ -528,8 +526,6 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De 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 @@ -547,7 +543,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De (erased, nctx) in
let brch = SMap.bindings branches in - let lst = + let _ = List.map ( fun (name, (l, vdefs, branch)) @@ -558,8 +554,12 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De (* 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)) + -> let (loc, _) = vdef in + let ctx' = Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s) in + let _ = candidats := (ctx', None, ftype, Expression ctx', loc, lst_in):: !candidats + in + mkctx (Opslexp.dbset_push ak erased) + ctx' (Lexp.ssink vdef s) (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) vdefs fieldtypes @@ -576,20 +576,21 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De brch in
- let diff = SMap.cardinal constructors - List.length lst in ( match default with | Some (v, d) - -> if diff <= 0 then (); + -> + let (loc, _) = v in let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in let subst = Subst.shift 1 in let hlxp = Lexp.mkVar ((l, None), 0) in let (_, nctx) = ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp nctx d cursor lst_in) :: !candidats; + let ret = (nctx, None, etype, Expression nctx, loc, lst_in) in + candidats := ret :: (browse_lexp nctx d cursor lst_in) :: !candidats; () | None - -> if diff > 0 then (); () + -> () ) | _,_ -> () ; ); @@ -1478,10 +1479,10 @@ let comp (a:string) (b:string) : string = else "-------*******__________FAILED__________*******-------\n\n\n"
let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) (expected:string) = -let (_, ast, _) = compile_string content in -let (list_list, _) = Option.get ast in -let (l,c) = position in -let pos = pos_of_tuple position in + let (_, ast, _) = compile_string content in + let (list_list, _) = Option.get ast in + let (l,c) = position in + let pos = pos_of_tuple position in
(* let (lctx, vx) = lexp_search ctx list_list pos in
===================================== typer.ml ===================================== @@ -68,8 +68,6 @@ let compile_main argv = let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in Arg.parse_argv argv arg_defs add_input_file usage; - if !lsp_server then Typer_lsp_server.run () - else (); print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; print_newline ();
===================================== typer_server.ml ===================================== @@ -0,0 +1,30 @@ +(* +* Copyright (C) 2020, 2021 Free Software Foundation, Inc. +* +* Author: Soilihi BEN SOILIHI BOINA ben.soilihi.boina.soilihi@umontreal.ca +* Keywords: languages, lisp, dependent types. +* Description: this file define the entry of the server +* +* This file is part of Typer. +* +* Typer is free software; you can redistribute it and/or modify it under the +* terms of the GNU General Public License as published by the Free Software +* Foundation, either version 3 of the License, or (at your option) any +* later version. +* +* Typer is distributed in the hope that it will be useful, but WITHOUT ANY +* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +* FOR A PARTICULAR PURPOSE. See the GNU General Public License for +* more details. +* +* You should have received a copy of the GNU General Public License along +* with this program. If not, see http://www.gnu.org/licenses/. +* *) + +open Typerlib + +open Typerserver + +let () = + if !Typer.lsp_server then Typer_lsp_server.run () + else (); \ No newline at end of file
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/715e3ba7b190b71b19d402dcc95236e203...