Décembre 2021 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer] Pushed new branch gambit-compiler-pp
by Simon Génier (＠ilovemonoids) 29 Déc '21

29 Déc '21

Simon Génier pushed new branch gambit-compiler-pp at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/gambit-compiler-pp You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] adding ctx and fixing line numbers in hover
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 26 Déc '21

26 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: dd13976d by Soilih BEN SOILIH at 2021-12-26T23:34:06-05:00 adding ctx and fixing line numbers in hover - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -837,7 +837,7 @@ let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) = | [] -> rlst | ((_, Some s) as vne, _, _)::tl -> if String.equal s str then - foo tl (comp + 1) str ((Some (vne,comp))::rlst) + foo tl (comp + 1) str ((Some (lctx,vne,comp))::rlst) else foo tl (comp + 1) str rlst | _::tl -> foo tl (comp + 1) str rlst in foo lctx_l 0 str [] @@ -858,23 +858,23 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc | Sort (_, StypeOmega) -> None | Builtin (_, t) -> None | Var (vn, idx) - -> Some (vn,idx) + -> Some (ctx, vn,idx) | Susp (e, s) -> None | 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 rec foo (ctx_list:Debruijn.env_elem list) cursor comp = + let rec foo ctx' (ctx_list:Debruijn.env_elem list) cursor comp = match ctx_list with | [] -> failwith "No Variable in the cursor" | ((l, (Some vn) as v),_,_)::tl - -> if (vn_on_the_cursor v cursor) then Some (v,comp) - else foo tl cursor (comp + 1) - | _::tl -> foo tl cursor (comp + 1) + -> if (vn_on_the_cursor v cursor) then Some (ctx',v,comp) + else foo ctx' tl cursor (comp + 1) + | _::tl -> foo ctx' tl cursor (comp + 1) in let ctx_list = Myers.list ctx' in - foo ctx_list cursor 0 + foo ctx' ctx_list cursor 0 | Arrow (ak, v, t1, l, t2) -> None @@ -1423,7 +1423,14 @@ class lsp_server = let (l_ctx_r,_,_,_) as ret = browse_lexp lctx 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 range = lsp_range_of_loc location in + let location' = { + location + with + start_line = location.start_line - 1; + end_line = location.end_line - 1 + } + in + let range = lsp_range_of_loc location' in let s = try use_search_name_in_ctx l_ctx l_type with exe -> Lexp.lexp_string_for_lsp l_type in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/dd13976d45936915f1cd9fb9446af0b22… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/dd13976d45936915f1cd9fb9446af0b22… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 24 Déc '21

24 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: 10732224 by Soilih BEN SOILIH at 2021-12-21T23:53:47-05:00 - - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -771,10 +771,9 @@ and check'' erased ctx e = | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> mkSusp ftype s - (*if ak = Aerasable - then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) + -> if ak = Aerasable + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -1080,10 +1079,9 @@ and get_type ctx e = | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> mkSusp ftype s - (*if ak = Aerasable - then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) + -> if ak = Aerasable + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with View it on GitLab: https://gitlab.com/monnier/typer/-/commit/1073222445b85a008370205a875a50b24… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/1073222445b85a008370205a875a50b24… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 4 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 24 Déc '21

24 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 6ff1e63e by Soilih BEN SOILIH at 2021-12-21T06:48:58-05:00 - - - - - - 42c504dc by Soilih BEN SOILIH at 2021-12-21T20:45:53-05:00 - - - - - - 3de98c1a by Soilih BEN SOILIH at 2021-12-21T23:24:10-05:00 - - - - - - 123f4ea2 by Soilih BEN SOILIH at 2021-12-24T19:46:51-05:00 browse_defs - - - - - 2 changed files: - src/opslexp.ml - src/typer_lsp_server.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -772,9 +772,9 @@ and check'' erased ctx e = | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> mkSusp ftype s (*if ak = Aerasable + -> if ak = Aerasable then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -1139,9 +1139,9 @@ and get_type ctx e = | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> mkSusp ftype s(*if ak = Aerasable + -> if ak = Aerasable then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with ===================================== src/typer_lsp_server.ml ===================================== @@ -42,9 +42,23 @@ open Util type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list type state_after_processing = (log_entry list * - (list_in_list * Debruijn.elab_context) + (list_in_list * Debruijn.elab_context) * ((int * int) option ref) ) +(* +let last_pos = ref [(0,0)] + +let add_to_tab tab a = + if((List.length !tab) > 4) then + let l = List.tl(List.rev !tab) in + tab := a::(List.rev l) + else + tab := a::(!tab) + +let get_pos_tab tab = + List.hd !tab +*) + (* transform a list of logs to a list of tuple to facilitate the manipulation *) @@ -135,14 +149,14 @@ let readstring (str:string) = 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) + (!Log.typer_log, ast, ref None) let process_some_input_file (_file_contents : string) : state_after_processing = readstring _file_contents (*Return the diagnostics of a document state *) let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = - let (log, _) = _state in + let (log, _, _) = _state in let log_tab = log_entry_to_list log in List.map (fun x -> let (loc, lev, msg) = x in @@ -626,11 +640,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D | [] -> () | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable - then - let a = Lexp.mkSusp ftype s in - candidats := (browse_lexp ctx a cursor):: !candidats; - else () + -> if ak = Aerasable + then + let a = Lexp.mkSusp ftype s in + candidats := (browse_lexp ctx a cursor):: !candidats; + else failwith "Fail Here!!!" | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -805,9 +819,29 @@ let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) = else tl |hd::ml::tl -> if (dist hd cursor < dist ml cursor ) then (foo (hd::tl) cursor) else foo (ml::tl) cursor -in foo tab cursor + in foo tab cursor + + let vn_on_the_cursor (vn:vname) (cursor:location) : bool = + let (l,_) = vn in + if ((cursor.start_column >= l.start_column) + && (cursor.end_column <= l.end_column)) + then true + else false + + let tup_browse_defs_in_ctx (lctx: Debruijn.lexp_context) (vn : vname) = + let lctx_l = Myers.list lctx in + let (_,so) = vn in + let str = Option.get so in + let rec foo lst comp str rlst = + match lst with + | [] -> rlst + | ((_, Some s) as vne, _, _)::tl + -> if String.equal s str then + foo tl (comp + 1) str ((Some (vne,comp))::rlst) + else foo tl (comp + 1) str rlst + | _::tl -> foo tl (comp + 1) str rlst + in foo lctx_l 0 str [] -(* let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) = match Lexp.lexp_lexp' e with @@ -824,164 +858,42 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc | Sort (_, StypeOmega) -> None | Builtin (_, t) -> None | Var (vn, idx) - -> Some (e,vn,idx) + -> Some (vn,idx) | Susp (e, s) -> None | 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 rec foo ctx defs cursor ret_list = - match defs with - | [] -> ret_list - | hd::tl -> let (vn,lxp,ltp) = hd in - foo ctx tl cursor ((browse_defs ctx lxp cursor)::ret_list) + let rec foo (ctx_list:Debruijn.env_elem list) cursor comp = + match ctx_list with + | [] -> failwith "No Variable in the cursor" + | ((l, (Some vn) as v),_,_)::tl + -> if (vn_on_the_cursor v cursor) then Some (v,comp) + else foo tl cursor (comp + 1) + | _::tl -> foo tl cursor (comp + 1) in - let tab = List.map - (fun (vn,lxp,ltp) -> - browse_defs ctx' lxp cursor - ) - defs - in - - (browse_defs ctx' e cursor)::tab + let ctx_list = Myers.list ctx' in + foo ctx_list cursor 0 | Arrow (ak, v, t1, l, t2) - -> ( - - let (_,_,k1,_) = browse_lexp ctx t1 cursor in - let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in - let (_,_,k2,_) = browse_lexp nctx t2 cursor in - match Opslexp.sort_compose ctx nctx l ak k1 k2 with - | SortResult k -> (nctx, None, k, location) - | SortInvalid - -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) - | SortK1NotType - -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) - | SortK2NotType - -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) - ) + -> None - | 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 etp = Opslexp.get_type ctx' e in - let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*) - let d = (ctx,None, t,l) in - browse_list_lexp ([a;b;d]) cursor + | Lambda (ak, ((l,_) as v), t, e) -> if (vn_on_the_cursor v cursor) then + try List.hd (tup_browse_defs_in_ctx ctx v) + with exe -> None + else None - | 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 - - browse_list_lexp (fonc::args_list) cursor - ) - - | Inductive (l, _label, args, cases) - -> - ( - let rec arg_loop ctx args = - - match args with - - | [] - -> let (level, tab) = - SMap.fold - (fun _ case (level,tab) -> - let ((level, _, _), 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 - ) - - | Proj (l, e, (loc, label)) - -> 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 - let it, aargs = call_split etype in - match Opslexp.lexp'_whnf it ctx, aargs with - | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors = 1 - -> let rec mksubst s fargs aargs = - match fargs, aargs with - | [], [] -> s - | _farg::fargs, (_ak, aarg)::aargs - -> mksubst (Subst.cons aarg s) fargs aargs - | _,_ -> s in - let s = mksubst Subst.identity fargs aargs in - let (_,fieldtypes) = List.hd (SMap.bindings constructors) in - let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) = - match fieldtypes with - | [] -> () - | (ak, (_, Some fn), ftype)::_ when fn = label - (* We found our field! *) - -> if ak = Aerasable - then - let a = Lexp.mkSusp ftype s in - candidats := (browse_lexp ctx a cursor):: !candidats; - else () - | (ak, vdef, ftype)::fieldtypes - -> let fvdef vdef e loc lbl = - match vdef with - |(l, Some n) -> Lexp.mkProj (loc, e, lbl) - |_ -> Lexp.impossible in - let fieldref = fvdef vdef e l (loc, label) in - getfieldtype (Subst.cons fieldref s) fieldtypes in - getfieldtype s fieldtypes; () - | Inductive _, _ - -> () - | _,_ -> ()); - browse_list_lexp !candidats cursor - + | Call (f, args) -> None + | Inductive (l, _label, args, cases) -> None + | Proj (l, e, (loc, label)) -> None | Case (l, e, ret, branches, default) - -> - let candidats = ref [] in - + -> 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; + (* 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 *) @@ -994,7 +906,7 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc 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 @@ -1019,7 +931,7 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc (erased, nctx) in let brch = SMap.bindings branches in - let lst = + let _ = List.map ( fun (name, (l, vdefs, branch)) @@ -1030,7 +942,8 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc (* 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) + -> candidats := ((Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)), vdef)::!candidats; + 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))])) @@ -1042,66 +955,33 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc 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 nctx branch cursor) :: !candidats; + ignore(ctx_extend_with_eq nctx subst hlxp) ) brch in - - 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 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) :: !candidats; - () - | None - -> if diff > 0 then (); () - ) + () + + | _,_ -> () ; ); - browse_list_lexp !candidats cursor + let rec cands (lst: (Debruijn.lexp_context * vname) list) = + match lst with + | [] -> failwith "No Valid Candidate" + | hd::tl -> let (ctx,(l,s)) = hd in + if (l.start_column <= cursor.start_column + && l.end_column >= cursor.end_column + ) + then hd + else cands tl + in + let (lctx,vn) = cands !candidats in + List.hd (tup_browse_defs_in_ctx lctx vn) + | 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 - (ctx, None, buildtype fargs, location) - with Not_found - -> (ctx, None, Debruijn.type_int, location) - ) - | _ -> (ctx, None, Debruijn.type_int, location)) - + -> None | 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, None, Lexp.push_susp t s, location)) -*) + -> None + (*==================================Parcourir les définitions==========================*) (* Search if the vname is in the context *) @@ -1485,6 +1365,7 @@ class lsp_server = Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; "\""; "'"; "/"; "@"; "<"] ~resolveProvider:true () in + (* let referencesProvider = `Bool true in let documentHighlightProvider = `Bool true @@ -1493,7 +1374,7 @@ class lsp_server = let documentSymbol = Lsp.Types.DocumentSymbolOptions.create ~workDoneProgress:true () in - + *) let hoverOption = Lsp.Types.HoverOptions.create ~workDoneProgress:true () in @@ -1504,16 +1385,17 @@ class lsp_server = { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider ; Lsp.Types.ServerCapabilities.hoverProvider = Some (`HoverOptions hoverOption); - Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption); + Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption)(*; Lsp.Types.ServerCapabilities.referencesProvider = Some referencesProvider ; Lsp.Types.ServerCapabilities.documentHighlightProvider = Some documentHighlightProvider; - Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol) + Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol)*) } method! on_req_definition ~notify_back ~id ~uri ~pos _st = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,ast) = state_after_processing in + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (pos.line,pos.character); let (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in @@ -1531,7 +1413,8 @@ 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 + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (pos.line,pos.character); let (list_list, ectx) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in @@ -1546,7 +1429,7 @@ class lsp_server = in (*let s = Lexp.lexp_string_for_lsp l_type in*) let r = Lsp.Types.Hover.create - ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) + ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=(Some "Typer")}) ~range:range () in let e = Some r in @@ -1556,7 +1439,8 @@ class lsp_server = method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,ast) = state_after_processing in + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (pos.line,pos.character); let (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in @@ -1601,7 +1485,7 @@ class lsp_server = let e = Some (`DocumentSymbol r) in let f = Linol_lwt.return e in f - + method! on_request_unhandled ~notify_back ~id req = let f :type r. r Lsp.Client_request.t -> r Linol_lwt.Jsonrpc2.IO.t = @@ -1643,7 +1527,7 @@ class lsp_server = | _ -> super#on_request_unhandled ~notify_back ~id req ) in f req - *) + *) end @@ -1654,7 +1538,7 @@ 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) = readstring content in + let (_, ast,_) = readstring content in let (list_list, _) = ast in let (l,c) = position in let pos = pos_of_tuple position in @@ -1796,7 +1680,13 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,4) ""; hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,14) "" - + +let time f a b = + let t = Sys.time() in + let fx = f a b in + Printf.printf "Execution time: %fs\n" (Sys.time() -. t); + fx + (*=======================================Test======================================*) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/39573a65cce99bb211b653fae49ce64d… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/39573a65cce99bb211b653fae49ce64d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] fixing...
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 21 Déc '21

21 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: ec783568 by Soilih BEN SOILIH at 2021-12-21T00:47:24-05:00 fixing... - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -765,15 +765,16 @@ and check'' erased ctx e = | _,_ -> (log_tc_error ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in - let fieldtypes = SMap.find label constructors in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable + -> mkSusp ftype s + (*if ak = Aerasable then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -1073,15 +1074,16 @@ and get_type ctx e = | _,_ -> (log_tc_error ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in - let fieldtypes = SMap.find label constructors in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable + -> mkSusp ftype s + (*if ak = Aerasable then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ec783568fd4831a158f2c0dc0afa836ef… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ec783568fd4831a158f2c0dc0afa836ef… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 3 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 20 Déc '21

20 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: c5a6a62d by Soilih BEN SOILIH at 2021-12-18T01:30:56-05:00 - - - - - - f498d2f1 by Soilih BEN SOILIH at 2021-12-18T13:20:12-05:00 - - - - - - 39573a65 by Soilih BEN SOILIH at 2021-12-20T21:21:00-05:00 fixing... - - - - - 4 changed files: - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/typer_lsp_server.ml Changes: ===================================== src/elab.ml ===================================== @@ -71,17 +71,17 @@ let dloc = dummy_location let parsing_internals = ref false let btl_folder = - + (* let cwd = Sys.getcwd () in let cdir = String.sub cwd 0 (String.length cwd) in let canal_entree = open_in (cdir ^ "/.configuration.txt") in let ligne1 = input_line canal_entree in let l = String.split_on_char ':' ligne1 in let m = String.split_on_char '"' (List.nth l 1) in - let filename = List.nth m 1 in + let filename = List.nth m 1 in*) try Sys.getenv "TYPER_BUILTINS" - with Not_found -> filename ^ "/btl" + with Not_found -> "/home/soilih/Projet Maitrise/typer" (*filename*) ^ "/btl" let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt ===================================== src/lexp.ml ===================================== @@ -530,7 +530,6 @@ let rec lexp_location e = | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e - (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l ===================================== src/opslexp.ml ===================================== @@ -766,15 +766,15 @@ and check'' erased ctx e = | _,_ -> (log_tc_error ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in - let fieldtypes = SMap.find label constructors in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable + -> mkSusp ftype s (*if ak = Aerasable then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -1133,15 +1133,15 @@ and get_type ctx e = | _,_ -> (log_tc_error ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in - let fieldtypes = SMap.find label constructors in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable + -> mkSusp ftype s(*if ak = Aerasable then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with ===================================== src/typer_lsp_server.ml ===================================== @@ -94,24 +94,6 @@ let lsp_pos_of_pos_end_for_symbol (p:Source.Location.t) : Lsp.Types.Position.t = let lsp_range_of_loc_for_symbol (l:Source.Location.t) : Lsp.Types.Range.t = Lsp.Types.Range.create ~start:(lsp_pos_of_pos_start_for_symbol l) ~end_:(lsp_pos_of_pos_end_for_symbol l) -let rec search_a_vname_with_a_given_position (vname_list: Util.vname list) (location : Source.Location.t): Util.vname = - match vname_list with - | [] -> let loc = Source.Location.dummy in - let s = Some "null" in - (loc,s) - | hd::tl -> - let (loc, _) = hd in - (* - let file = "position.txt" in - let oc = open_out file in (* create or truncate file, return channel *) - Printf.fprintf oc "loc.start_line = %d \n loc.start_column = %d \n location.start_line = %d \n location.start_column = %d \n " loc.start_line loc.start_column location.start_line location.start_column; (* write something *) - close_out oc; (* flush and close the channel *) - *) - if ((loc.start_line - 1) == location.start_line) - && ((loc.start_column - 1) == location.start_column) - then hd - else search_a_vname_with_a_given_position tl location - let vname_to_lsp_loc ~(vname: Util.vname) ~uri : Lsp.Types.Location.t = let (location, _) = vname in @@ -146,19 +128,6 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list) then (nearest_lexp_of_the_list (hd::tl) cursor) else nearest_lexp_of_the_list (ml::tl) cursor - - -let rec search_lexp_with_a_location (list_list: list_in_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 (*compile a string and return the logs and ast*) let readstring (str:string) = @@ -267,6 +236,7 @@ module Compl = struct | Event -> Lsp.Types.CompletionItemKind.Event | Operator -> Lsp.Types.CompletionItemKind.Operator | TypeParameter -> Lsp.Types.CompletionItemKind.TypeParameter + (* let tranform_string (content:string) : (string * int * int) list = Base.String.split content ~on:'\n' |> @@ -277,7 +247,7 @@ module Compl = struct pos+1, (word,line+1,pos-1)) |> Base.snd) |> List.concat - *) + let list_filter_by_line (liste: (string * int * int) list) (line:int) : (string * int * int) list = List.filter (fun (word,w_line,w_column) -> w_line == line) liste @@ -291,7 +261,7 @@ module Compl = struct liste in word - + let dist_compl (loc1:string * int * int) (loc2:int * int) = let (_,loc1_sl,loc1_sc) = loc1 in let (loc2_sl,loc2_sc) = loc2 in @@ -301,7 +271,8 @@ module Compl = struct +. (((float_of_int (loc1_sc)) -. (float_of_int (loc2_sc))) ** 2.0 ) ) ) - + + let rec find_the_nearest_compl (liste:(string * int * int) list) (pos:int * int) : string = match liste with @@ -312,7 +283,8 @@ module Compl = struct |hd::ml::tl -> if ((dist_compl hd pos) < (dist_compl ml pos)) then (find_the_nearest_compl (hd::tl) pos) else find_the_nearest_compl (ml::tl) pos - + *) + (* let match_str (str:string) : Str.regexp = str |> Str.quote @@ -355,6 +327,7 @@ module Compl = struct Str.string_match reg x.label 0 ) liste + *) end (*==============completion============================*) @@ -639,7 +612,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D let it, aargs = call_split etype in match Opslexp.lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors != 1 + when SMap.cardinal constructors = 1 -> let rec mksubst s fargs aargs = match fargs, aargs with | [], [] -> s @@ -647,7 +620,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D -> mksubst (Subst.cons aarg s) fargs aargs | _,_ -> s in let s = mksubst Subst.identity fargs aargs in - let fieldtypes = SMap.find label constructors in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) = match fieldtypes with | [] -> () @@ -800,20 +773,336 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D browse_lexp ctx e cursor | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, location)) - let lexp_parcourir ctx e = - let lctx = Debruijn.ectx_to_lctx ctx in - let location = Lexp.lexp_location e in - (Opslexp.get_type lctx e , location) - (*====================================Lexp parcourir===================================*) -(* Verify if there is a varbind *) -let verify_varbind (env: Debruijn.env_elem) : (int * Lexp.lexp) option = - let (_,vrbd,_) = env in - match vrbd with - | Variable - | ForwardRef-> None - | LetDef (idx,lxp) -> Some (idx,lxp) +(*==================================Parcourir les définitions==========================*) +let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) = + let ((loc, oename), dbi) = v in + try + let ((l,_),_,_) as ret = Myers.nth dbi ctx in + let _ = match (ret, oename) with + | (((_, Some name), _, _), Some ename) + -> if not (ename = name) then + Log.log_fatal + ~loc + ({|DeBruijn index %d refers to wrong name. |} + ^^ {|Expected: "%s" got "%s"|}) + dbi ename name + | _ -> () in + + l + with + | Not_found + -> Log.log_fatal + ~loc "DeBruijn index %d of `%s` out of bounds" dbi (Lexp.maybename oename) + + let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = + let rec foo tab cursor = + match tab with + | [] -> failwith "Liste vide!" + | [n] -> n + | [hd;tl] -> if (dist hd cursor < dist tl cursor ) then hd + else tl + |hd::ml::tl -> if (dist hd cursor < dist ml cursor ) then (foo (hd::tl) cursor) + else foo (ml::tl) cursor +in foo tab cursor + +(* +let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) = + + match Lexp.lexp_lexp' e with + + | Imm (Float (_, _)) + | Imm (Integer (_, _)) + | Imm (String (_, _)) -> None + | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> None + | SortLevel SLz -> None + | SortLevel (SLsucc e) -> None + | SortLevel (SLlub (e1, e2)) -> None + | Sort (l, Stype e) -> None + | Sort (_, StypeLevel) -> None + | Sort (_, StypeOmega) -> None + | Builtin (_, t) -> None + | Var (vn, idx) + -> Some (e,vn,idx) + | Susp (e, s) -> None + | 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 rec foo ctx defs cursor ret_list = + match defs with + | [] -> ret_list + | hd::tl -> let (vn,lxp,ltp) = hd in + foo ctx tl cursor ((browse_defs ctx lxp cursor)::ret_list) + in + let tab = List.map + (fun (vn,lxp,ltp) -> + browse_defs ctx' lxp cursor + ) + defs + in + + (browse_defs ctx' e cursor)::tab + + | Arrow (ak, v, t1, l, t2) + -> ( + + let (_,_,k1,_) = browse_lexp ctx t1 cursor in + let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in + let (_,_,k2,_) = browse_lexp nctx t2 cursor in + match Opslexp.sort_compose ctx nctx l ak k1 k2 with + | SortResult k -> (nctx, None, k, location) + | SortInvalid + -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) + | SortK1NotType + -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) + | SortK2NotType + -> (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 etp = Opslexp.get_type ctx' e in + let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*) + let d = (ctx,None, t,l) in + browse_list_lexp ([a;b;d]) cursor + + | 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 + + browse_list_lexp (fonc::args_list) cursor + ) + + | Inductive (l, _label, args, cases) + -> + ( + let rec arg_loop ctx args = + + match args with + + | [] + -> let (level, tab) = + SMap.fold + (fun _ case (level,tab) -> + let ((level, _, _), 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 + ) + + | Proj (l, e, (loc, label)) + -> 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 + let it, aargs = call_split etype in + match Opslexp.lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (Subst.cons aarg s) fargs aargs + | _,_ -> s in + let s = mksubst Subst.identity fargs aargs in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in + let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) = + match fieldtypes with + | [] -> () + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if ak = Aerasable + then + let a = Lexp.mkSusp ftype s in + candidats := (browse_lexp ctx a cursor):: !candidats; + else () + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> Lexp.mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (Subst.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes; () + | Inductive _, _ + -> () + | _,_ -> ()); + browse_list_lexp !candidats cursor + + | Case (l, e, ret, branches, default) + -> + 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 nctx branch cursor) :: !candidats; + ) + brch + in + + 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 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) :: !candidats; + () + | None + -> if diff > 0 then (); () + ) + | _,_ -> () ; + ); + 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 + (ctx, None, buildtype fargs, location) + with Not_found + -> (ctx, None, 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, None, Lexp.push_susp t s, location)) +*) +(*==================================Parcourir les définitions==========================*) (* Search if the vname is in the context *) let search_name_in_ctx (lctx: Debruijn.lexp_context) (lxp: Lexp.lexp) = @@ -873,13 +1162,13 @@ let search_the_key (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : string = (*====================================Definition===================================*) -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 rec find_def_location lctx cursor (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Source.Location.t = - let (ctx,vr,_,loc) = ret in + let (_,vr,_,_) = ret in match vr with - | None -> loc - | Some v -> let ((l,_),_,_) = Debruijn.lctx_lookup ctx v in + | None -> cursor + | Some v -> let ((l,_),_,_) = Debruijn.lctx_lookup lctx v in {l with start_line = (l.start_line - 1); end_line = (l.end_line - 1)} @@ -888,6 +1177,7 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte (*=====================================Symbols=====================================*) +(* let filter_the_list_list (list_list: (vname * Lexp.lexp * Lexp.lexp) list) : (vname * Lexp.lexp * Lexp.lexp) list = List.filter ( fun x -> let ((_,s),_,_) = x in @@ -918,7 +1208,7 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = ~selectionRange:range () ) filtred_list - + *) let kind_bread (e: Lexp.lexp) : Lsp.Types.SymbolKind.t = let open Elexp in match Lexp.lexp_lexp' e with @@ -951,7 +1241,7 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. (*=====================================End Symbols=================================*) (*====================================Compl===================================*) - + (* let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Lsp.Types.CompletionItem.t list = let (_,vr,_,loc) = ret in @@ -973,7 +1263,7 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. ~textEdit:textEdit ~detail:detail () in [ci] - + let trans_listlist_by_var (ctx:Debruijn.lexp_context) (list_list:list_in_list) (cursor:Source.Location.t) = let lst = update_the_context ctx list_list in let nlst = List.map ( fun x -> @@ -987,7 +1277,8 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. | None -> false | Some v -> true ) nlst - + *) + let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t = let open Elexp in match Lexp.lexp_lexp' e with @@ -1229,7 +1520,7 @@ class lsp_server = let (lctx,vx) = lexp_search ctx list_list typer_loc in let (_,lexp,_) = vx in let (l_ctx, idx,_ ,_ ) as ret = browse_lexp lctx lexp typer_loc in - let loc = find_def_location l_ctx ret in + let loc = find_def_location lctx typer_loc ret in let l = Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc loc) in @@ -1293,7 +1584,7 @@ class lsp_server = let e = Some (`List comp_list_ret) in let f = Linol_lwt.return e in f - + (* method! on_req_symbol ~notify_back ~id ~uri () = match Hashtbl.find buffers uri with @@ -1309,6 +1600,7 @@ class lsp_server = let r = create_breadcrumbs filtred_list in let e = Some (`DocumentSymbol r) in let f = Linol_lwt.return e in f + method! on_request_unhandled ~notify_back ~id req = @@ -1351,7 +1643,7 @@ class lsp_server = | _ -> super#on_request_unhandled ~notify_back ~id req ) in f req - + *) end @@ -1504,23 +1796,7 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,4) ""; hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,14) "" -let testSymbols (content:string) = - let (_, (list_list,_)) = readstring content in - (*let res = create_symbols list_list in*) - let res = take_all_list_el list_list in - let name = "/home/soilih/Bureau/test/symbol.txt" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in - (* - List.iteri (fun i (x : Lsp.Types.DocumentSymbol.t) -> - let st = "\n" ^ (string_of_int i) ^ " : " ^ (x.name) ^ "\n" in - output_string oc st - ) res; - *) - output_string oc (string_of_int (List.length res)); - close_out oc - - let testS () = - testSymbols "multiply x y z = _*_ x y ;" + (*=======================================Test======================================*) @@ -1532,7 +1808,6 @@ let run () = ignore (Arg.Set Log.lsp_enabled); Logs.set_level ~all:true (Some Logs.Debug); (*test ();*) - (*testS ();*) 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/ded4414a5b81adabe753ff09aa07cd02… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ded4414a5b81adabe753ff09aa07cd02… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 4 commits: config
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 14 Déc '21

14 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 2c45ce87 by Soilih BEN SOILIH at 2021-12-02T16:00:03-05:00 config - - - - - 7080f329 by Soilih BEN SOILIH at 2021-12-05T02:12:52-05:00 add proj to my branch - - - - - 495a8c88 by Soilih BEN SOILIH at 2021-12-10T10:12:48-05:00 resolve Proj errors - - - - - ded4414a by Soilih BEN SOILIH at 2021-12-14T21:27:28-05:00 adding breadcrumbs, highlight and references - - - - - 12 changed files: - + .configuration.txt - btl/pervasive.typer - − configuration.txt - src/elab.ml - src/elexp.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/positivity.ml - src/typer_lsp_server.ml - src/unification.ml Changes: ===================================== .configuration.txt ===================================== @@ -0,0 +1,3 @@ +"filename":"/home/soilih/Projet Maitrise/typer" +"description":"this filename is the absolute path from where we run Typer. +We must change it to make it work !!!" ===================================== btl/pervasive.typer ===================================== @@ -426,31 +426,6 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair; -__\.__ = - let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") - (cons (Sexp_symbol "?") - (cons (Sexp_symbol "cons") - nil)); - pattern = Sexp_node constructor - (cons (Sexp_node (Sexp_symbol "_:=_") - (cons f (cons (Sexp_symbol "v") - nil))) - nil); - branch = Sexp_node (Sexp_symbol "_=>_") - (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") - (cons (Sexp_node (Sexp_symbol "_|_") - (cons o (cons branch nil))) - nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); %% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type) ===================================== configuration.txt deleted ===================================== @@ -1,2 +0,0 @@ -"filename":"/Projet Maitrise/typer" -"description":"this filename is the place from where we run Typer. We must change it to make it work !!!" ===================================== src/elab.ml ===================================== @@ -72,23 +72,16 @@ let dloc = dummy_location let parsing_internals = ref false let btl_folder = - (* - (* Read the JSON file *) - let json = Yojson.Basic.from_file "../configuration.json" in - let exec_path = json |> Yojson.Basic.Util.member "path" |> Yojson.Basic.Util.to_string in - *) - - (* - let canal_entree = open_in "../configuration.txt" in + let cwd = Sys.getcwd () in + let cdir = String.sub cwd 0 (String.length cwd) in + let canal_entree = open_in (cdir ^ "/.configuration.txt") in let ligne1 = input_line canal_entree in let l = String.split_on_char ':' ligne1 in let m = String.split_on_char '"' (List.nth l 1) in let filename = List.nth m 1 in - *) - - let env_var = Sys.getenv "HOME" in + try Sys.getenv "TYPER_BUILTINS" - with Not_found -> env_var ^ (*exec_path*) (*filename*) "/Projet Maitrise/typer" ^ "/btl" + with Not_found -> filename ^ "/btl" let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt @@ -459,6 +452,7 @@ let meta_to_var ids (e : lexp) = | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl) | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in @@ -1756,6 +1750,17 @@ 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 = + match sargs with + | [lxp;(Symbol (loca,str))] + -> let (ret,_) = infer lxp ctx in + let e = mkProj (loc,ret,(loca,str)) in + (e, Lazy) + | _ -> sexp_error loc "Unrecognized proj expression"; + sform_dummy_ret ctx loc + + + let rec infer_level ctx se : lexp = match se with | Symbol (_, "z") -> mkSortLevel SLz @@ -1876,6 +1881,7 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("__.__", sform_proj); ("lambda_->_", sform_lambda Anormal); ("lambda_=>_", sform_lambda Aimplicit); ("lambda_≡>_", sform_lambda Aerasable); ===================================== src/elexp.ml ===================================== @@ -51,6 +51,8 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref + (* A projection *) + | Proj of U.location * elexp * int (* Recursive `let` binding. *) | Let of U.location * (vname * elexp) list * elexp @@ -83,6 +85,7 @@ let rec elexp_location e = match e with | Imm s -> sexp_location s | Var ((l,_), _) -> l + | Proj (l,_,_) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l | Lambda ((l,_),_) -> l @@ -96,6 +99,7 @@ let elexp_name e = match e with | Imm _ -> "Imm" | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "Let" | Call _ -> "Call" | Cons _ -> "Cons" @@ -136,6 +140,9 @@ 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) ^ " )" + | Cons (_, (_, s)) -> "datacons(" ^ s ^")" | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b) ===================================== src/eval.ml ===================================== @@ -463,6 +463,17 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) (eval f ctx trace) (List.map (fun e -> eval e ctx trace) args) + (* 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 + ) + (* Case *) | Case (loc, target, pat, dflt) -> (eval_case ctx trace loc target pat dflt) ===================================== src/inverse_subst.ml ===================================== @@ -264,6 +264,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl) | Susp (e, s') -> apply_inv_subst (push_susp e s') s | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in ===================================== src/lexp.ml ===================================== @@ -66,6 +66,7 @@ type ltype = lexp | Sort of U.location * sort | Builtin of symbol * ltype | Var of vref + | Proj of U.location * lexp * label | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp @@ -245,6 +246,10 @@ let lexp'_hash (lp : lexp') = args))) | Susp (lp, subst) -> 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))) + (* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) @@ -309,6 +314,7 @@ let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) +let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) let mkLet (l, ds, e) = hc (Let (l, ds, e)) let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) @@ -329,6 +335,7 @@ let lexp_head e = | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "let" | Arrow _ -> "Arrow" | Lambda _ -> "lambda" @@ -513,6 +520,7 @@ let rec lexp_location e = | SortLevel SLz -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l + | Proj (l,_,_) -> l | Builtin ((l, _), _) -> l | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l @@ -590,6 +598,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s) + | Proj (l,lxp,lbl) -> mkProj (l, mkSusp lxp s, lbl) and nosusp e = (* Return `e` with no outermost `Susp`. *) match lexp_lexp' e with @@ -653,6 +662,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) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with @@ -671,6 +681,10 @@ let rec lexp_unparse lxp = | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Proj (l,lxp,(loc,str) ) + -> Node (Symbol (l, "__.__"), + [(lexp_unparse lxp);(Symbol (loc,str))]) + | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) @@ -1003,6 +1017,9 @@ and lexp_str ctx (exp : lexp) : string = | Var ((_loc, name), idx) -> maybename name ^ (index idx) ; + | Proj (l,lxp,(loc,str)) + -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + | Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with ===================================== src/opslexp.ml ===================================== @@ -747,6 +747,46 @@ and check'' erased ctx e = args) in let tct = arg_loop ctx erased args in tct + + | Proj (l, e, (loc, label)) + ->( let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (check erased ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let fieldtypes = SMap.find label constructors in + let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if ak = Aerasable + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l "Proj on an inductive type that's not a tuple!"; etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -926,6 +966,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty) + | Proj (l,lxp,lbl) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in @@ -1072,6 +1113,47 @@ and get_type ctx e = arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct + + | Proj (l, e, (loc, label)) + ->( (*check'' DB.set_empty ctx e*) + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (get_type ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let fieldtypes = SMap.find label constructors in + let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if ak = Aerasable + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l "Proj on an inductive type that's not a tuple!"; etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | Case (_l, _e, ret, _branches, _default) -> ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -1140,11 +1222,44 @@ 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 = + 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) + 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!" + let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) + | L.Proj (l, exp, label) + -> let t = get_type lctx exp in + E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) | L.Lambda (P.Aerasable, _, _, body) ===================================== src/positivity.ml ===================================== @@ -117,6 +117,8 @@ and positive' index lexp = *) -> true + | Lexp.Proj _ -> false + | Lexp.Case _ | Lexp.Cons _ | Lexp.Let _ | Lexp.Sort _ | Lexp.SortLevel _ (* There are no rules that have these synctactic forms as a conclusion. *) -> false ===================================== src/typer_lsp_server.ml ===================================== @@ -625,8 +625,52 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D ) cursor in arg_loop ctx args - ) + + | Proj (l, e, (loc, label)) + -> 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 + let it, aargs = call_split etype in + match Opslexp.lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors != 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (Subst.cons aarg s) fargs aargs + | _,_ -> s in + let s = mksubst Subst.identity fargs aargs in + let fieldtypes = SMap.find label constructors in + let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) = + match fieldtypes with + | [] -> () + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if ak = Aerasable + then + let a = Lexp.mkSusp ftype s in + candidats := (browse_lexp ctx a cursor):: !candidats; + else () + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> Lexp.mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (Subst.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes; () + | Inductive _, _ + -> () + | _,_ -> ()); + browse_list_lexp !candidats cursor + | Case (l, e, ret, branches, default) -> let candidats = ref [] in @@ -875,6 +919,35 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = () ) filtred_list +let kind_bread (e: Lexp.lexp) : Lsp.Types.SymbolKind.t = + let open Elexp in + match Lexp.lexp_lexp' e with + | Lambda (ak, (l,_), t, e) -> Lsp.Types.SymbolKind.Function + | Cons (t, (_l, name)) -> Lsp.Types.SymbolKind.Constructor + | _ -> Lsp.Types.SymbolKind.Variable + + +let kind_ (element : Debruijn.env_elem ) : Lsp.Types.SymbolKind.t = + let (_,vrb,_) = element in + match vrb with + | Variable + | ForwardRef -> Lsp.Types.SymbolKind.Variable + | LetDef (_,lxp) -> kind_bread lxp + +let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol.t list = + List.map ( fun x -> + let ((l,s),_,_) = x in + let range = lsp_range_of_loc_for_symbol l in + let nm = Option.get s in + Lsp.Types.DocumentSymbol.create + ~name:nm + ~detail:nm + ~kind:(kind_ x) + ~range:range + ~selectionRange:range + () + ) lst + (*=====================================End Symbols=================================*) (*====================================Compl===================================*) @@ -939,19 +1012,37 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = | None -> filter_lctx tl ret | Some _ -> filter_lctx tl (hd::ret) - - + + let construct_highlights (lst: Debruijn.env_elem list) : Lsp.Types.DocumentHighlight.t list = + List.map ( fun (x: Debruijn.env_elem) -> + let ((l,s),_,_) = x in + let range = Compl.lsp_range_of_a_tuple + (l.start_line,l.start_column) (l.end_line,l.end_column) + in + Lsp.Types.DocumentHighlight.create ~range:range () + ) lst + let construct_references uri (lst: Debruijn.env_elem list) : Lsp.Types.Location.t list = + List.map ( fun (x: Debruijn.env_elem) -> + let ((l,s),_,_) = x in + let range = Compl.lsp_range_of_a_tuple + (l.start_line,l.start_column) (l.end_line,l.end_column) + in + Lsp.Types.Location.create ~uri:uri ~range:range + ) lst (* Transform a context to a list of completion item *) - let ctx_to_ci_list (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = + let ctx_to_ci_list ctx (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = List.map ( fun (x: Debruijn.env_elem) -> let ((_,s),_,t) = x in let str = Option.get s in let label = str in + let s = try use_search_name_in_ctx ctx t + with exe -> Lexp.lexp_string_for_lsp t + in let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(str) in let kind = kind_of_a_varbind x in let ci = Lsp.Types.CompletionItem.create ~label:label ~kind:kind - ~textEdit:textEdit ~detail:(Lexp.lexp_string t) () + ~textEdit:textEdit ~detail:s () in ci @@ -1044,7 +1135,7 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = *) class lsp_server = object(self) - inherit Linol_lwt.Jsonrpc2.server + inherit Linol_lwt.Jsonrpc2.server as super (* one env per document *) val buffers: (Lsp.Types.DocumentUri.t, state_after_processing) Hashtbl.t @@ -1103,6 +1194,10 @@ class lsp_server = Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; "\""; "'"; "/"; "@"; "<"] ~resolveProvider:true () in + let referencesProvider = `Bool true + in + let documentHighlightProvider = `Bool true + in let documentSymbol = Lsp.Types.DocumentSymbolOptions.create ~workDoneProgress:true () @@ -1119,6 +1214,8 @@ class lsp_server = { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider ; Lsp.Types.ServerCapabilities.hoverProvider = Some (`HoverOptions hoverOption); Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption); + Lsp.Types.ServerCapabilities.referencesProvider = Some referencesProvider ; + Lsp.Types.ServerCapabilities.documentHighlightProvider = Some documentHighlightProvider; Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol) } @@ -1163,22 +1260,8 @@ class lsp_server = in let e = Some r in let f = Linol_lwt.return e in f - - (* provisional, to be done later *) - method! on_req_execute_command ~notify_back ~id _c _args = - match _c with - | "typer" -> let file = "command.txt" in - let message = _c in (* Write message to file *) - let oc = open_out file in (* create or truncate file, return channel *) - Printf.fprintf oc "%s\n" message; (* write something *) - close_out oc; (* flush and close the channel *) - let h = Lsp.Types.Command.yojson_of_t - (Lsp.Types.Command.create ~title:_c ~command:_c () ) in - let e = Linol_lwt.return h in e - | _ -> assert false + - - (* provisional, to be done later *) method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with @@ -1205,21 +1288,70 @@ class lsp_server = in let filtred_list = filter_lctx l_ctx [] in - let comp_list = ctx_to_ci_list filtred_list range in + let comp_list = ctx_to_ci_list l_ctx filtred_list range in let comp_list_ret = complete_oth word comp_list in let e = Some (`List comp_list_ret) in let f = Linol_lwt.return e in f - (* + method! on_req_symbol ~notify_back ~id ~uri () = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,(list_list, _)) = state_after_processing in - let r = create_symbols list_list in + | state_after_processing -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = pos_of_tuple (Int.max_int,Int.max_int) in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in + let filtred_list = filter_lctx l_ctx [] in + let r = create_breadcrumbs filtred_list in let e = Some (`DocumentSymbol r) in let f = Linol_lwt.return e in f - *) + + method! on_request_unhandled ~notify_back ~id req = + + let f :type r. r Lsp.Client_request.t -> r Linol_lwt.Jsonrpc2.IO.t = + fun req -> + + (match req with + | TextDocumentHighlight params + -> ( + match Hashtbl.find buffers params.textDocument.uri with + | state_after_processing + -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = pos_of_tuple + (params.position.line,params.position.character) in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in + let filtred_list = filter_lctx l_ctx [] in + let hi = construct_highlights filtred_list in + let e = Some hi in + let f = Linol_lwt.return e in f) + | TextDocumentReferences params + -> ( + match Hashtbl.find buffers params.textDocument.uri with + | state_after_processing + -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = pos_of_tuple + (params.position.line,params.position.character) in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in + let filtred_list = filter_lctx l_ctx [] in + let hi = construct_references (params.textDocument.uri) filtred_list in + let e = Some hi in + let f = Linol_lwt.return e in f) + | _ -> super#on_request_unhandled ~notify_back ~id req + ) + in f req + end ===================================== src/unification.ml ===================================== @@ -69,6 +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 | 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/9a5b03e0602a39243ff663c7564a634c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9a5b03e0602a39243ff663c7564a634c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] 2 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 10 Déc '21

10 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: 5abc3040 by Soilih BEN SOILIH at 2021-12-09T10:29:50-05:00 - - - - - - 2929ef49 by Soilih BEN SOILIH at 2021-12-10T09:55:17-05:00 + - - - - - 3 changed files: - btl/pervasive.typer - src/elab.ml - src/opslexp.ml Changes: ===================================== btl/pervasive.typer ===================================== @@ -424,33 +424,7 @@ BoolMod = (##datacons (_ := Bool) (_ := true) (_ := false); Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); -pair = datacons Pair pair; - -__\.__ = - let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##__.__") - (cons (Sexp_symbol "?") - (cons (Sexp_symbol "cons") - nil)); - pattern = Sexp_node constructor - (cons (Sexp_node (Sexp_symbol "_:=_") - (cons f (cons (Sexp_symbol "v") - nil))) - nil); - branch = Sexp_node (Sexp_symbol "_=>_") - (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") - (cons (Sexp_node (Sexp_symbol "_|_") - (cons o (cons branch nil))) - nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); +pair = datacons Pair pair; %% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type) ===================================== src/elab.ml ===================================== @@ -1729,12 +1729,12 @@ let sform_letin ctx loc sargs ot = match sargs with let sform_proj ctx loc sargs ot = match sargs with - | [Node (Symbol (l, "__.__"), [lxp;(Symbol (loca,str))])] + | [lxp;(Symbol (loca,str))] -> let (ret,_) = infer lxp ctx in - let e = mkProj (l,ret,(loca,str)) in + let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) | _ -> sexp_error loc "Unrecognized proj expression"; - sform_dummy_ret ctx loc + sform_dummy_ret ctx loc let rec infer_level ctx se : lexp = match se with ===================================== src/opslexp.ml ===================================== @@ -756,7 +756,7 @@ and check'' erased ctx e = let it, aargs = call_split etype in match lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors != 1 + when SMap.cardinal constructors = 1 -> let rec mksubst s fargs aargs = match fargs, aargs with | [], [] -> s @@ -1064,7 +1064,7 @@ and get_type ctx e = let it, aargs = call_split etype in match lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors != 1 + when SMap.cardinal constructors = 1 -> let rec mksubst s fargs aargs = match fargs, aargs with | [], [] -> s @@ -1227,7 +1227,7 @@ let pos_of_label lctx label t : int = let it, aargs = call_split t in match lexp'_whnf it lctx, aargs with | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors != 1 + 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 View it on GitLab: https://gitlab.com/monnier/typer/-/compare/fd27756b4e6d5c378c070ef5a206a4ac… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/fd27756b4e6d5c378c070ef5a206a4ac… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] eval
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 02 Déc '21

02 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: fd27756b by Soilih BEN SOILIH at 2021-12-02T16:25:21-05:00 eval - - - - - 1 changed file: - src/eval.ml Changes: ===================================== src/eval.ml ===================================== @@ -463,8 +463,16 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) (eval f ctx trace) (List.map (fun e -> eval e ctx trace) args) (* Proj *) - | Proj (l, e, i) - -> eval' e ctx + | 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 + ) + (* Case *) | Case (loc, target, pat, dflt) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/fd27756b4e6d5c378c070ef5a206a4acb… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/fd27756b4e6d5c378c070ef5a206a4acb… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] 2 commits: +
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 02 Déc '21

02 Déc '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: f4662f03 by Soilih BEN SOILIH at 2021-12-02T09:55:19-05:00 + - - - - - 02545ba2 by Soilih BEN SOILIH at 2021-12-02T14:46:37-05:00 lexp to elexp - - - - - 4 changed files: - btl/pervasive.typer - src/elab.ml - src/eval.ml - src/opslexp.ml Changes: ===================================== btl/pervasive.typer ===================================== @@ -428,7 +428,7 @@ pair = datacons Pair pair; __\.__ = let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") + let constructor = Sexp_node (Sexp_symbol "##__.__") (cons (Sexp_symbol "?") (cons (Sexp_symbol "cons") nil)); ===================================== src/elab.ml ===================================== @@ -1732,7 +1732,7 @@ let sform_proj ctx loc sargs ot = | [Node (Symbol (l, "__.__"), [lxp;(Symbol (loca,str))])] -> let (ret,_) = infer lxp ctx in let e = mkProj (l,ret,(loca,str)) in - (e, Inferred e) + (e, Lazy) | _ -> sexp_error loc "Unrecognized proj expression"; sform_dummy_ret ctx loc ===================================== src/eval.ml ===================================== @@ -462,7 +462,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) -> eval_call (elexp_location f) f trace (eval f ctx trace) (List.map (fun e -> eval e ctx trace) args) - (* TODO: Proj *) + (* Proj *) | Proj (l, e, i) -> eval' e ctx ===================================== src/opslexp.ml ===================================== @@ -1219,12 +1219,44 @@ 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 = + 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) + 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!" + let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) - | L.Proj (l,lxp,lbl) -> failwith "cannot convert a lexp to elexp" + | L.Proj (l, exp, label) + -> let t = get_type lctx exp in + E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) | L.Lambda (P.Aerasable, _, _, body) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/291f6c305760ce184dcf3af611298435… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/291f6c305760ce184dcf3af611298435… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Décembre 2021