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

Commits: 9196759a by Soilih at 2022-02-02T00:03:01-05:00 -

- - - - - 45a943d0 by Soilih at 2022-02-05T20:35:06-05:00 -

- - - - - 939a01da by Soilih at 2022-02-05T22:23:21-05:00 fixing the fatal problem with the hover

- - - - -

7 changed files:

- src/elab.ml - src/elexp.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/typer_lsp_server.ml - src/unification.ml

Changes:

===================================== src/elab.ml ===================================== @@ -1750,16 +1750,20 @@ let sform_letin ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc

-let sform_proj ctx loc sargs ot = +let sform_proj ctx loc sargs _ = match sargs with | [lxp;(Symbol (loca,str))] -> let (ret,_) = infer lxp ctx in - let e = mkProj (loc,ret,(loca,str)) in + let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) - | _ -> sexp_error loc "Unrecognized proj expression"; + | [_;_] + -> sexp_error loc "Second argument is not a Symbol!"; + sform_dummy_ret ctx loc + | _ -> sexp_error loc "Wrong arg number!"; sform_dummy_ret ctx loc

+

let rec infer_level ctx se : lexp = match se with

===================================== src/elexp.ml ===================================== @@ -85,7 +85,7 @@ let rec elexp_location e = match e with | Imm s -> sexp_location s | Var ((l,_), _) -> l - | Proj (l,_,_) -> l + | Proj (l, _, _) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l | Lambda ((l,_),_) -> l @@ -140,8 +140,8 @@ and elexp_string lxp = | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" - | Proj (l,lxp,i) - -> "( _._ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )" + | Proj (_,lxp,i) + -> "( __.__ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )"

| Cons (_, (_, s)) -> "datacons(" ^ s ^")"

===================================== src/eval.ml ===================================== @@ -465,14 +465,12 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type)

(* Proj *) | Proj (loc, e, i) - -> let vt = eval' e ctx in - ( - match vt with - | Vcons (symbol, vtl) -> List.nth vtl i - | _ -> error - loc - "Connot find a value in position %d \n" i - ) + -> (match eval' e ctx with + | Vcons (_, vtl) -> List.nth vtl i + | _ -> error + loc + "Proj on a non-datatype constructor: %s \n" (elexp_string e)) +

(* Case *) | Case (loc, target, pat, dflt)

===================================== src/lexp.ml ===================================== @@ -248,7 +248,7 @@ let lexp'_hash (lp : lexp') = -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) | Proj (l,lxp,lbl) -> U.combine_hash 15 (U.combine_hash (Hashtbl.hash l) - (U.combine_hash (Hashtbl.hash lxp) (Hashtbl.hash lbl))) + (U.combine_hash (Hashtbl.hash lxp) (Hashtbl.hash lbl)))

(* Equality function for hash table @@ -661,7 +661,7 @@ let clean e = | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) - | Proj (l,lxp,lbl) -> mkProj (l,(clean s lxp),lbl) + | Proj (l, lxp, lbl) -> mkProj (l, clean s lxp, lbl) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with @@ -1016,8 +1016,8 @@ and lexp_str ctx (exp : lexp) : string =

| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;

- | Proj (l,lxp,(loc,str)) - -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + | Proj (_,lxp,(_,str)) + -> "( __.__ " ^ lexp_str' lxp ^ " " ^ str ^ " )"

| Metavar (idx, subst, (_loc, name)) (* print metavar result if any *)

===================================== src/opslexp.ml ===================================== @@ -774,11 +774,11 @@ and check'' erased ctx e = (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasalbe field: %s" label; etype) - | (ak, vdef, ftype)::fieldtypes + else (log_tc_error ~loc:l "Can't Proj an erasalbe field: %s" label; Lexp.impossible) + | (_, vdef, _)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with - |(l, Some n) -> mkProj (loc, e, lbl) + |(_, Some _) -> mkProj (loc, e, lbl) |_ -> Lexp.impossible in let fieldref = fvdef vdef e l (loc, label) in getfieldtype (S.cons fieldref s) fieldtypes in @@ -1141,11 +1141,11 @@ and get_type ctx e = (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasalbe field: %s" label; etype) - | (ak, vdef, ftype)::fieldtypes + else (log_tc_error ~loc:l "Can't Proj an erasalbe field: %s" label; Lexp.impossible) + | (_, vdef, _)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with - |(l, Some n) -> mkProj (loc, e, lbl) + |(_, Some _) -> mkProj (loc, e, lbl) |_ -> Lexp.impossible in let fieldref = fvdef vdef e l (loc, label) in getfieldtype (S.cons fieldref s) fieldtypes in @@ -1222,35 +1222,37 @@ let arity_of_cons ^^ {|because it is not an inductive type: %s|}) name (lexp_string ty)

-let pos_of_label lctx label t : int = - let call_split e = - match lexp_lexp' e with - | Call (f, args) -> (f, args) - | _ -> (e,[]) in - let it, aargs = call_split t in - match lexp'_whnf it lctx, aargs with - | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors = 1 - -> let bindings = SMap.bindings constructors in - let find_the_pos label (lst : (string * (arg_kind * vname * ltype) list) list) c = - match lst with - | [ls] -> let (_,l) = ls in - let rec foo label (l : (arg_kind * vname * ltype) list) c = +let pos_of_label lctx label e : int = + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + + let it, aargs = call_split (lexp_whnf e lctx) in + match lexp'_whnf it lctx, aargs with + | Inductive (_, _, _, constructors), _ + when SMap.cardinal constructors = 1 + -> let (_, st) = label in + (match SMap.bindings constructors with + | [(_,l)] -> let rec find_index label (l : (arg_kind * vname * ltype) list) (c: int) : int = match l with - | [] -> failwith "label not found!" - | hd::tl -> match hd with - | (ak, (loc, Some vn), ltp ) - -> let (_,st) = label in - if (String.equal vn st) then c - else foo label tl (c + 1) - | _ -> foo label tl (c + 1) + | [] + -> let (loc,st) = label in + Log.log_error ~loc:loc "Label Not Found: %s" st; 0 + | (_, (_, Some vn), _ )::_ when (String.equal vn st) + -> c + | _::tl -> find_index label tl (c + 1) in - foo label l c - | _ -> failwith "More than one element!" - in find_the_pos label bindings 0 - | Inductive _, _ - -> failwith "Proj on an inductive type that's not a tuple!" - | _,_ -> failwith "Proj on a non-inductive type!" + find_index label l 0 + | _ -> let (loc, _) = label in + Log.log_fatal ~loc:loc "Wrong arg number to inductive type!") + + | Inductive _, _ + -> let (loc,_) = label in + Log.log_error ~loc:loc "Proj on an inductive type that's not a tuple!"; 0 + | _,_ -> let (loc,_) = label in + Log.log_error ~loc:loc "Proj on a non-inductive type: %s" (Lexp.lexp_string it) ; 0 +

let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with

===================================== src/typer_lsp_server.ml ===================================== @@ -41,10 +41,13 @@ open Util

type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list

+type syntax_tree = (list_in_list * Debruijn.elab_context) + type state_after_processing = (log_entry list * - (list_in_list * Debruijn.elab_context) * ((int * int) option ref) + (syntax_tree option) * ((int * int) option ref) )

+ (* let last_pos = ref [(0,0)]

@@ -145,14 +148,40 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list) else nearest_lexp_of_the_list (ml::tl) cursor

+let construct_log_exec str s : Log.log_entry list = + let lst = String.split_on_char '\n' str in + let open Source.Location in + let l = { + file = ""; + start_line = 0; + start_column = 0; + end_line = ((List.length lst) - 1); + end_column = ((String.length str) - 1) + } + in + let open Log in + let log_entry = { + level = Log.Error; + kind = (Some "ERROR"); + section = None; + print_action = None ; + loc = (Some l); + msg = s; + } + in + [log_entry] +

(*compile a string and return the logs and ast*) let readstring (str:string) = Log.clear_log () ; let ectx = Elab.default_ectx in - (*let rctx = Elab.default_rctx in*) - let ast = Elab.lexp_decl_str str ectx in - (!Log.typer_log, ast, ref None) + match Elab.lexp_decl_str str ectx with + | (ast:syntax_tree) -> (!Log.typer_log, Some ast, ref None) + | exception Internal_error msg -> (construct_log_exec str msg, None, ref None) + | exception Stop_compilation msg -> (construct_log_exec str msg, None, ref None) + | exception User_error msg -> (construct_log_exec str msg, None, ref None) +

let process_some_input_file (_file_contents : string) : state_after_processing = readstring _file_contents @@ -741,22 +770,15 @@ class lsp_server = method! on_req_hover ~notify_back ~id ~uri ~pos doc_state = match Hashtbl.find buffers uri with | state_after_processing -> let (_,ast,_) = state_after_processing in - let (list_list, _) = ast in + let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in - let typer_loc' = { - typer_loc - with - start_line = typer_loc.start_line + 1; - end_line = typer_loc.end_line + 1 - } - in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let lexp = trans_list_in_list_to_let list_list in + (*let lexp = trans_list_in_list_to_let list_list in*)

let (lctx,vx) = lexp_search ctx list_list typer_loc in - let ((lvn,_),_,ltyp) = vx in + let ((lvn,_),lexp,ltyp) = vx in

- let (l_ctx_r,_,_,_) as ret = browse_lexp ctx lexp typer_loc' in + let (l_ctx_r,_,_,_) as ret = browse_lexp ctx lexp typer_loc in let ret' = (l_ctx_r,None,ltyp,lvn) in let (l_ctx,_,l_type,location) = browse_list_lexp [ret;ret'] typer_loc in let location' = { @@ -882,7 +904,6 @@ end and runs it as a task. *) let run () = ignore (Arg.Set Log.lsp_enabled); - (*test ();*) let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in

===================================== src/unification.ml ===================================== @@ -69,7 +69,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false | Var (_, _i) -> false - | Proj(_,lxp,_) -> oi lxp + | Proj (_,lxp,_) -> oi lxp | Susp (_e, _s) -> Log.internal_error "`e` should be "clean" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e)

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9745c8188a87aaf96da3f0c915dc2ea44...