Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits: 395d075f by Soilih BEN SOILIH at 2021-05-12T10:24:19-06:00 update hover
- - - - -
4 changed files:
- src/configuration.json → configuration.json - + configuration.txt - src/elab.ml - src/typer_lsp_server.ml
Changes:
===================================== src/configuration.json → configuration.json ===================================== @@ -1,4 +1,4 @@ { "path": "/Projet Maitrise/typer", "description" : "this path is the path from where we run Typer to the typer folder. We must change it to make it work !!!" -} \ No newline at end of file +}
===================================== configuration.txt ===================================== @@ -0,0 +1,2 @@ +"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 ===================================== @@ -65,21 +65,25 @@ let dloc = Source.Location.dummy
let parsing_internals = ref false
-(* -(* Read the JSON file *) -let json = Yojson.Basic.from_file "../../configuration.json" +let btl_folder =
-(* take the path - it's make an exception now !! -*) -let exec_path = json |> Yojson.Basic.Util.member "path" |> Yojson.Basic.Util.to_string;; -*) + (* + (* 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 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 btl_folder = let env_var = Sys.getenv "HOME" in try Sys.getenv "TYPER_BUILTINS" - with Not_found -> (*exec_path*) env_var ^ "/Projet Maitrise/typer" ^ "/btl" + with Not_found -> env_var ^ (*exec_path*) (*filename*) "/Projet Maitrise/typer" ^ "/btl"
let fatal = Log.log_fatal ~section:"ELAB" let error = Log.log_error ~section:"ELAB"
===================================== src/typer_lsp_server.ml ===================================== @@ -169,36 +169,36 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list ) )
- let list_nearest_to (tab:Lexp.lexp list) (loc:Source.Location.t) = - let rec foo tab loc = + let browse_list_lexp (tab:Lexp.lexp list) (cursor:Source.Location.t) = + let rec foo tab cursor = match tab with | [] -> failwith "Liste vide!" | [n] -> n - | [hd;tl] -> if (dist (Lexp.lexp_location hd) loc < dist (Lexp.lexp_location tl) loc ) then hd + | [hd;tl] -> if (dist (Lexp.lexp_location hd) cursor < dist (Lexp.lexp_location tl) cursor ) then hd else tl - |hd::ml::tl -> if (dist (Lexp.lexp_location hd) loc < dist (Lexp.lexp_location ml) loc ) then (foo (hd::tl) loc) - else foo (ml::tl) loc - in foo tab loc + |hd::ml::tl -> if (dist (Lexp.lexp_location hd) cursor < dist (Lexp.lexp_location ml) cursor ) then (foo (hd::tl) cursor) + else foo (ml::tl) cursor + in foo tab cursor
- let pos_in_lexp_interval (tab:Lexp.lexp list) (loc:Source.Location.t) = + let pos_in_lexp_interval (tab:Lexp.lexp list) (cursor:Source.Location.t) = let open Source.Location in - let rec foo tab loc = + let rec foo tab cursor = match tab with | [] -> failwith "Liste vide!" | hd::tl -> let location = Lexp.lexp_location hd in - if ((location.start_line <= loc.start_line && location.start_column <= loc.start_column) + if ((location.start_line <= cursor.start_line && location.start_column <= cursor.start_column) && - (location.end_line >= loc.end_line && location.end_column >= loc.end_column)) + (location.end_line >= cursor.end_line && location.end_column >= cursor.end_column)) then hd - else foo tl loc - in foo tab loc + else foo tl cursor + in foo tab cursor
- let lexp_search (tab:Lexp.lexp list) (loc:Source.Location.t) = - try pos_in_lexp_interval tab loc - with exn -> list_nearest_to tab loc + let lexp_search (tab:Lexp.lexp list) (cursor:Source.Location.t) = + try pos_in_lexp_interval tab cursor + with exn -> browse_list_lexp tab cursor
(* search the type of a lexp browsing a lexp*) - let rec browse_lexp ctx e = + let rec browse_lexp ctx e cursor =
let open Elexp in let location = Lexp.lexp_location e in @@ -242,142 +242,138 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | Lambda (ak, ((l,_) as v), t, e) -> (Lexp.mkArrow (ak, v, t, l,e), location)
| Call (f, args) - -> ((List.fold_left - (fun ft (ak,arg) - -> match Opslexp.lexp'_whnf ft ctx with - | Arrow (ak', _v, t1, _l, t2) - -> Lexp.mkSusp t2 (Subst.substitute arg) - | _ -> ft + -> ( + let ft = Opslexp.get_type ctx f in + + match Opslexp.lexp'_whnf ft ctx with + | Arrow (ak', _v, t1, _l, t2) -> let e = browse_list_lexp (List.map (fun (_, e) -> e) args) cursor in + browse_lexp ctx e cursor + | _ -> browse_lexp ctx ft cursor ) - f args), location) + (* | Inductive (l, _label, args, cases) - -> let rec arg_loop ctx erased args = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _, _) = - List.fold_left - (fun (level, ictx, erased, n) (ak, v, t) -> - ((let lwhnf = Opslexp.lexp_whnf t ictx in - match Lexp.lexp_lexp' lwhnf with - | Sort (_, Stype _) - when ak == Pexp.Aerasable - -> level - | Sort (_, Stype level') - -> Opslexp.mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (* FIXME: If it does refer, - * we get an ugly error! *) - (Lexp.mkSusp level' (Lexp.sunshift n)) - | _tt -> level), - Debruijn.lctx_extend ictx v Variable t, - Debruijn.set_sink 1 erased, - n + 1)) - (level, ctx, erased, 0) - case in - level) - cases (Lexp.mkSortLevel SLz) in - (Lexp.mkSort (l, Stype level), location) - | (ak, v, t)::args - -> let _k = t in - Lexp.mkArrow (ak, v, t, Lexp.lexp_location t, - arg_loop (Debruijn.lctx_extend ctx v Variable t) - (Opslexp.dbset_push ak erased) - args) in - let tct = arg_loop ctx erased args in - tct + ->( + let rec arg_loop ctx erased args = + match args with + | [] + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _, _) = + List.fold_left + (fun (level, ictx, erased, n) (ak, v, t) -> + ((let lwhnf = Opslexp.lexp_whnf t ictx in + match Lexp.lexp_lexp' lwhnf with + | Sort (_, Stype _) + when ak == Pexp.Aerasable (*&& impredicative_erase*) + -> level + | Sort (_, Stype level') + -> Opslexp.mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (* FIXME: If it does refer, + * we get an ugly error! *) + (Lexp.mkSusp level' (Lexp.sunshift n)) + | _tt -> level), + Debruijn.lctx_extend ictx v Variable t, + Debruijn.set_sink 1 erased, + n + 1)) + (level, ctx, erased, 0) + case in + level) + cases (Lexp.mkSortLevel SLz) in + (Lexp.mkSort (l, Stype level), location) + | (ak, v, t)::args + -> let _k = t in + Lexp.mkArrow (ak, v, t, Lexp.lexp_location t, + arg_loop (Debruijn.lctx_extend ctx v Variable t) + (Opslexp.dbset_push ak erased) + args) in + let tct = arg_loop ctx erased args in + (tct, location) + )
| Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> 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 - (* FIXME save the type in the case lexp instead of recomputing - it over and over again *) - let ekind = get_type ctx etype in - let elvl = match lexp'_whnf ekind ctx with - | Sort (_, Stype l) -> l - | _ -> Log.log_error ~loc:(lexp_location ekind) - "Target lexp's kind is not a sort"; DB.level0 in - let it, aargs = call_split etype in - (match 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 (S.cons aarg s) fargs aargs - | _,_ -> (error_tc ~loc:l - "Wrong arg number to inductive type!"; s) in - let s = mksubst S.identity fargs aargs in - let ctx_extend_with_eq ctx subst hlxp nerased = - let tlxp = mkSusp e subst in - let tltp = mkSusp etype subst in - let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, - [(L.Aerasable, tlvl); (* Typelevel *) - (L.Aerasable, tltp); (* Inductive type *) - (L.Anormal, hlxp); (* Lexp of the branch head *) - (L.Anormal, tlxp)]) in (* Target lexp *) - (* The eq proof is erasable. *) - let nerased = dbset_push L.Aerasable nerased in - let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in - (nerased, nctx) in - SMap.iter - (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 (dbset_push ak erased) - (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) - (ssink vdef s) - (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) - vdefs fieldtypes - | _,_ -> (error_tc ~loc:l - "Wrong number of args to constructor!"; - (erased, ctx, hlxp)) in - let hctor = - mkCall (mkCons (it, (l, name)), - List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in - let (nerased, nctx, hlxp) = - mkctx erased ctx s hctor vdefs fieldtypes in - let subst = S.shift (List.length vdefs) in - let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in - assert_type nctx branch - (check nerased nctx branch) - (mkSusp ret (S.shift ((List.length fieldtypes) + 1)))) - branches; - let diff = SMap.cardinal constructors - SMap.cardinal branches in - (match default with - | Some (v, d) - -> if diff <= 0 then - warning_tc ~loc:l "Redundant default clause"; - let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in - let nerased = DB.set_sink 1 erased in - let subst = S.shift 1 in - let hlxp = mkVar ((l, None), 0) in - let (nerased, nctx) = - ctx_extend_with_eq nctx subst hlxp nerased in - assert_type nctx d (check nerased nctx d) - (mkSusp ret (S.shift 2)) - | None - -> if diff > 0 then - error_tc ~loc:l ("Non-exhaustive match: " - ^ string_of_int diff ^ " cases missing")) - | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); - ret*) + match Lexp.lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = Opslexp.lexp_whnf e ctx 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 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 (S.cons aarg s) fargs aargs + | _,_ -> (s) in + let s = mksubst Subst.identity fargs aargs in + let ctx_extend_with_eq ctx subst hlxp nerased = + 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 nerased = Opslexp.dbset_push Lexp.Aerasable nerased in + let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in + (nerased, nctx) in + SMap.iter + (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 (dbset_push ak erased) + (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) + (ssink vdef s) + (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, 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) = Elab.ctx_extend_with_eq nctx subst hlxp nerased in + Opslexp.assert_type nctx branch branch + (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1)))) + branches; + let diff = SMap.cardinal constructors - SMap.cardinal branches in + (match default with + | Some (v, d) + -> if diff <= 0 then (); + let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in + let nerased = Debruijn.set_sink 1 erased in + let subst = Subst.shift 1 in + let hlxp = mkVar ((l, None), 0) in + let (nerased, nctx) = + Elab.ctx_extend_with_eq nctx subst hlxp nerased in + assert_type nctx d d + (Lexp.mkSusp ret (Subst.shift 2)) + | None + -> if diff > 0 then () ) + | _,_ -> ()); + (ret,location) + *) | Cons (t, (_l, name)) -> (match Opslexp.lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) @@ -493,8 +489,8 @@ class lsp_server = let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in let typer_loc = typer_pos_of_lsp_pos pos in let lexp = lexp_search lexp_list typer_loc in - let ctx = Elab.default_ectx in - let (l_type,location) = browse_lexp ctx lexp in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (l_type,location) = browse_lexp ctx lexp typer_loc in let range = lsp_range_of_loc location in let s = Lexp.lexp_string l_type in let r = Lsp.Types.Hover.create
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/395d075f02de1e44dbe51850a0e77d27c5...