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

Commits: 83744967 by Soilih BEN SOILIH at 2021-10-04T14:47:34-06:00 fix the case Case

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -610,99 +610,100 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp ) | 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 - + 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 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 nctx d cursor) :: !candidats; - browse_lexp nctx d cursor - | None - -> if diff > 0 then (); (ctx, None, Lexp.impossible, Source.Location.dummy) - ) + + | 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 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 nctx d cursor) :: !candidats; + + browse_lexp nctx d cursor + | None + -> if diff > 0 then (); (ctx, None, Lexp.impossible, Source.Location.dummy) + ) | _,_ -> (ctx, None, Lexp.impossible, Source.Location.dummy) ; - + ); browse_list_lexp !candidats cursor - ) - - | Cons (t, (_l, name)) -> (match Opslexp.lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) @@ -1089,9 +1090,13 @@ let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (posit let (list_list, _) = ast in let (l,c) = position in let pos = pos_of_tuple position in + let (lctx,vx) = lexp_search ctx list_list pos in - let (_,lexp,_) = vx in - let (_,_, l_type,_) = browse_lexp lctx lexp pos in + let ((lvn,_),lexp,ltyp) = vx in + let (l_ctx_r,_,_,_) as ret = browse_lexp lctx lexp pos in + let ret' = (l_ctx_r,None,ltyp,lvn) in + let (_,_,l_type,_) = browse_list_lexp [ret;ret'] pos in + let excpect = "excpected : " ^ expected ^ "\n" in let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\n\n" in let input = "input : " ^ content ^ "\n" in @@ -1123,10 +1128,16 @@ let test () = hoverTest ctx name "f = 12.3 ;" (1,6) "##Float"; sep name "LAMBDA"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1) "(x : ##Int) -> Int"; - hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "(x : ##Int) -> Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "##Int"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13) "##Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,23) ""; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19) "(Int -> (Int -> Int))"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21) "##Int"; + hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,20) "##Int"; + hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,24) "##Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,24) "##Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,26) "##Int"; + sep name "FUNCTION(LAMBDA)"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10) "##Int"; @@ -1144,7 +1155,7 @@ let test () = hoverTest ctx name "multiply x y z = x + y + z ;" (1,22) "##Int"; hoverTest ctx name "multiply x y z = x + y + z ;" (1,26) "##Int"; sep name "CALL"; - hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,1) "##Int"; hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,7) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,13) "##Int"; hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,15) "##Int"; @@ -1158,10 +1169,16 @@ let test () = hoverTest ctx name "foo = ##String ; \n\n\nv = foo ;" (4,1) "(##Type_ (##TypeLevel.succ ##TypeLevel.z))"; hoverTest ctx name "foo = ##Type ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; sep name "LIST"; - hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "##Type"; + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "(List ##TypeLevel.z ##Int)"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (a -> ((List ℓ a) -> (List ℓ a)))"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12) "##Int"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)"; + sep name "TUPLE"; + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ; \n\n\ntup = (1,2,"str",lst) ;" (4,1) "typecons (Tuple) (cons ##Int ##Int ##String (List ##TypeLevel.z ##Int))"; + hoverTest ctx name "tup = (1,2,"str",false) ;" (1,8) "##Int"; + hoverTest ctx name "tup = (1,2,"str",false) ;" (1,10) "##Int"; + hoverTest ctx name "tup = (1,2,"str",false) ;" (1,15) "##String"; + hoverTest ctx name "tup = (1,2,"str",false) ;" (1,21) "Bool"; sep name "ARROW"; hoverTest ctx name "type Floo = bar Int Int ;" (1,1) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,17) ""; @@ -1204,13 +1221,13 @@ let test () = hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,37) ""; hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,41) ""; sep name "CASE"; - hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (1,1) ""; - hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (1,5) ""; - hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (1,14) ""; - hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (3,4) ""; - hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (3,13) ""; - hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (5,4) ""; - hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (5,14) "" + hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (1,1) ""; + hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (1,5) ""; + hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (1,14) ""; + hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (3,4) ""; + hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (3,13) ""; + 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) ""

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