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

Commits: c3aa818e by Soilih BEN SOILIH at 2021-05-15T18:49:23-06:00 browse_lexp update

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -223,14 +223,17 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | 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) + | 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) -> (Lexp.push_susp e s, 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) @@ -240,7 +243,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let _ = List.fold_left (fun n (_v, e, t) -> n - 1) (List.length defs) defs in - (Lexp.mkSusp e (Opslexp.lexp_defs_subst l Subst.identity defs), location) + let (e',_) = browse_lexp ctx e cursor in + (Lexp.mkSusp e' (Opslexp.lexp_defs_subst l Subst.identity defs), Lexp.lexp_location e')

| Arrow (ak, v, t1, l, t2) -> ( @@ -254,7 +258,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | SortK2NotType -> (Lexp.mkSort (l, StypeOmega), location) ) - | Lambda (ak, ((l,_) as v), t, e) -> (Lexp.mkArrow (ak, v, t, l,e), location) + | Lambda (ak, ((l,_) as v), t, e) -> let (e',_) = browse_lexp ctx e cursor in + (Lexp.mkArrow (ak, v, t, l,e'), Lexp.lexp_location e')

| Call (f, args) -> ( @@ -266,8 +271,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list browse_lexp ctx e' cursor | _ -> browse_lexp ctx ft cursor ) - - (* + | Inductive (l, _label, args, cases) ->( let rec arg_loop ctx erased args = @@ -299,24 +303,26 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list case in level) cases (Lexp.mkSortLevel SLz) in - (Lexp.mkSort (l, Stype level), location) + 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 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 call_split e = + -> ( + let call_split e = match Lexp.lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = Opslexp.lexp_whnf e ctx in + let (e',_) = browse_lexp ctx e cursor 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 @@ -324,6 +330,9 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | Sort (_, Stype l) -> l | _ -> Debruijn.level0 in let it, aargs = call_split etype in + let nerased = Opslexp.nerased_let defs Debruijn.set_empty in + let subst = Subst.shift 1 in + let erased = Debruijn.set_empty in (match Opslexp.lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = @@ -332,8 +341,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | _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 + -> 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 nerased = let tlxp = Lexp.mkSusp e subst in @@ -357,7 +366,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list (* 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) + -> mkctx (Opslexp.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))])) @@ -369,9 +378,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list 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)))) + let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in + (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1)))) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -382,14 +390,13 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list 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 + ctx_extend_with_eq nctx subst hlxp nerased in (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) @@ -422,7 +429,9 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list

| Metavar (idx, s, _) -> (match Lexp.metavar_lookup idx with - | MVal e -> let e = Lexp.push_susp e s in (e,location) + | MVal e -> let e = Lexp.push_susp e s in + let (e',_) = browse_lexp ctx e cursor in + (e',Lexp.lexp_location e') | MVar (_, t, _) -> (Lexp.push_susp t s, location))

let lexp_parcourir ctx e =

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