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

Commits: d83e49da by Soilih BEN SOILIH at 2021-07-02T23:07:13-06:00 fixing let, adding got to definition

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -94,12 +94,17 @@ let vname_to_lsp_loc ~(vname: Util.vname) ~uri : Lsp.Types.Location.t = Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc location)

-let rec search_lexp_with_a_location (lexp_list: Lexp.lexp list) (location : Source.Location.t): Lexp.lexp option = - match lexp_list with - | [] -> None - | hd::tl -> let r = Lexp.lexp_location hd in - if ((r.start_line - 1) == location.start_line) && ((r.start_column - 1) == location.start_column) then Some hd - else search_lexp_with_a_location tl location +let rec search_lexp_with_a_location (list_list: (vname * Lexp.lexp * Lexp.ltype) list 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

let readstring (str:string) = Log.clear_log () ; @@ -325,245 +330,250 @@ end (lctx,lexp)

(* search the type of a lexp browsing a lexp*) - let rec browse_lexp ctx e cursor = + let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Lexp.lexp * Source.Location.t =

- let open Elexp in - let location = Lexp.lexp_location e in - match Lexp.lexp_lexp' e with - | Imm (Float (_, _)) -> (Debruijn.type_float, location) - | Imm (Integer (_, _)) -> (Debruijn.type_int, location) - | Imm (String (_, _)) -> (Debruijn.type_string, location) - | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (Debruijn.type_string, location) - | SortLevel SLz -> (Debruijn.type_level, location) - | SortLevel (SLsucc e) - -> (Debruijn.type_level, location) - | SortLevel (SLlub (e1, e2)) - -> (Debruijn.type_level, location) - | Sort (l, Stype e) - -> (Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location) - | Sort (_, StypeLevel) -> (Debruijn.sort_omega, location) - | Sort (_, StypeOmega) -> (Debruijn.sort_omega, location) - | Builtin (_, t)-> (t, location) - | Var (((l, name), idx) as v) -> (Debruijn.lctx_lookup_type ctx v, location) - | Susp (e, s) -> browse_lexp ctx (Lexp.push_susp e s) cursor - | Let (l, defs, e) - -> let _ = - List.fold_left (fun ctx (v, _e, t) - -> (Debruijn.lctx_extend ctx v ForwardRef t)) - ctx defs in - (* FIXME: Termination checking! Positivity-checker! *) - let _ = List.fold_left (fun n (_v, e, t) - -> n - 1) - (List.length defs) defs in - let (e',loc) = browse_lexp ctx e cursor in - (Lexp.mkSusp e' (Opslexp.lexp_defs_subst l Subst.identity defs),loc) - - | Arrow (ak, v, t1, l, t2) - -> ( - let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in - match Opslexp.sort_compose ctx nctx l ak t1 t2 with - | SortResult k -> (k, location) - | SortInvalid - -> (Lexp.mkSort (l, StypeOmega), location) - | SortK1NotType - -> (Lexp.mkSort (l, StypeOmega), location) - | SortK2NotType - -> (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 (ret,loc) = browse_list_lexp (a::b::[]) cursor in - (Lexp.mkArrow (ak, v, t, l,ret), loc) - - | 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 - - try - browse_list_lexp (fonc::args_list) cursor - with exe -> failwith "Exeption sur ce call !!!" - ) - - | 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) - | (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 Debruijn.set_empty args in - (tct, location) - ) - - | Case (l, e, ret, branches, default) - (* FIXME: Check that the return type isn't TypeLevel. *) - -> - ( - 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 + let open Elexp in + let location = Lexp.lexp_location e in + match Lexp.lexp_lexp' e with + | Imm (Float (_, _)) -> (Debruijn.type_float, location) + | Imm (Integer (_, _)) -> (Debruijn.type_int, location) + | Imm (String (_, _)) -> (Debruijn.type_string, location) + | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (Debruijn.type_string, location) + | SortLevel SLz -> (Debruijn.type_level, location) + | SortLevel (SLsucc e) + -> (Debruijn.type_level, location) + | SortLevel (SLlub (e1, e2)) + -> (Debruijn.type_level, location) + | Sort (l, Stype e) + -> (Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location) + | Sort (_, StypeLevel) -> (Debruijn.sort_omega, location) + | Sort (_, StypeOmega) -> (Debruijn.sort_omega, location) + | Builtin (_, t)-> (t, location) + | Var (((l, name), idx) as v) -> (Debruijn.lctx_lookup_type ctx v, location) + | Susp (e, s) -> browse_lexp ctx (Lexp.push_susp e s) cursor + | 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 tab = List.map + (fun (vn,lxp,ltp) -> + browse_lexp ctx' lxp cursor + ) + defs + in + + let (ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in + + (Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc) + + | Arrow (ak, v, t1, l, t2) + -> ( + let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in + match Opslexp.sort_compose ctx nctx l ak t1 t2 with + | SortResult k -> (k, location) + | SortInvalid + -> (Lexp.mkSort (l, StypeOmega), location) + | SortK1NotType + -> (Lexp.mkSort (l, StypeOmega), location) + | SortK2NotType + -> (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 (ret,loc) = browse_list_lexp (a::b::[]) cursor in + (Lexp.mkArrow (ak, v, t, l,ret), loc) + + | 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 + + try + browse_list_lexp (fonc::args_list) cursor + with exe -> failwith "Exeption sur ce call !!!" + ) + + | 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) + | (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 Debruijn.set_empty args in + (tct, location) + ) + + | Case (l, e, ret, branches, default) + (* FIXME: Check that the return type isn't TypeLevel. *) + -> + ( + 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 ctx branch cursor) :: !candidats; + ) + brch + in + + let diff = SMap.cardinal constructors - List.length lst in ( - 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 ctx branch cursor) :: !candidats; + 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 = Lexp.mkVar ((l, None), 0) in + let (nerased, nctx) = + ctx_extend_with_eq nctx subst hlxp in + candidats := (browse_lexp ctx d cursor) :: !candidats; + browse_lexp ctx d cursor + | None + -> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy) ) - brch - in + | _,_ -> (Lexp.impossible, Source.Location.dummy) ;

- 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 nerased = Debruijn.set_sink 1 erased in - let subst = Subst.shift 1 in - let hlxp = Lexp.mkVar ((l, None), 0) in - let (nerased, nctx) = - ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp ctx d cursor) :: !candidats; - browse_lexp ctx d cursor - | None - -> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy) - ) - | _,_ -> (Lexp.impossible, Source.Location.dummy) ; - - browse_list_lexp !candidats cursor + 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 + (buildtype fargs, location) + with Not_found + -> (Debruijn.type_int, location) + ) + | _ -> (Debruijn.type_int, location))

- | 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 - (buildtype fargs, location) - with Not_found - -> (Debruijn.type_int, location) - ) - | _ -> (Debruijn.type_int, location)) - - | Metavar (idx, s, _) - -> (match Lexp.metavar_lookup idx with - | MVal e -> let e = Lexp.push_susp e s in - let (e', loc) = browse_lexp ctx e cursor in - (e',loc) - | MVar (_, t, _) -> (Lexp.push_susp t s, location)) + | Metavar (idx, s, _) + -> (match Lexp.metavar_lookup idx with + | MVal e -> let e = Lexp.push_susp e s in + let (e', loc) = browse_lexp ctx e cursor in + (e',loc) + | MVar (_, t, _) -> (Lexp.push_susp t s, location))

let lexp_parcourir ctx e = let lctx = Debruijn.ectx_to_lctx ctx in @@ -573,6 +583,37 @@ end (*====================================Lexp parcourir===================================*)

+(*====================================Definition===================================*) + +let rec find_def_location (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Source.Location.t = + + let open Elexp in + (*let location = Lexp.lexp_location e in*) + match Lexp.lexp_lexp' e with + | Imm (Float (_, _)) -> Source.Location.dummy + | Imm (Integer (_, _)) -> Source.Location.dummy + | Imm (String (_, _)) -> Source.Location.dummy + | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> Source.Location.dummy + | SortLevel SLz -> Source.Location.dummy + | SortLevel (SLsucc e) -> Source.Location.dummy + | SortLevel (SLlub (e1, e2)) -> Source.Location.dummy + | Sort (l, Stype e) -> Source.Location.dummy + | Sort (_, StypeLevel) -> Source.Location.dummy + | Sort (_, StypeOmega) -> Source.Location.dummy + | Builtin (_, t) -> Source.Location.dummy + | Var (((l, name), idx) as v) -> Source.Location.dummy + | Susp (e, s) -> Source.Location.dummy + | Let (l, defs, e) -> Source.Location.dummy + | Arrow (ak, v, t1, l, t2) -> Source.Location.dummy + | Lambda (ak, ((l,_) as v), t, e) -> Source.Location.dummy + | Call (f, args) -> Source.Location.dummy + | Inductive (l, _label, args, cases) -> Source.Location.dummy + | Case (l, e, ret, branches, default) -> Source.Location.dummy + | Cons (t, (_l, name)) -> Source.Location.dummy + | Metavar (idx, s, _) -> Source.Location.dummy + +(*====================================Definition===================================*) +

(* Lsp server class This is the main point of interaction beetween the code checking documents @@ -624,11 +665,11 @@ class lsp_server =

| state_after_processing -> let (_,ast) = state_after_processing in let (list_list, _) = ast in - 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 typer_loc = typer_pos_of_lsp_pos pos in - let r = Option.get(search_lexp_with_a_location lexp_list typer_loc) in - let loc = Lexp.lexp_location r in + (*let r = Option.get(search_lexp_with_a_location list_list typer_loc) in*) + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (lctx,lexp) = lexp_search ctx list_list typer_loc in + let loc = find_def_location lctx lexp typer_loc in let l = Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc loc) in

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/d83e49da8e6622a58d40f6a330ee7311f0...