Novembre 2021 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][add-proj] 5 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 27 Nov '21

27 Nov '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: 9d4d090d by Soilih BEN SOILIH at 2021-11-21T21:35:01-05:00 - - - - - - 91edf98c by Soilih BEN SOILIH at 2021-11-23T23:58:29-05:00 Proj in check - - - - - 4f5c69fc by Soilih BEN SOILIH at 2021-11-24T18:54:10-05:00 - - - - - - f609101d by Soilih BEN SOILIH at 2021-11-25T09:37:14-05:00 - - - - - - 1f077559 by Soilih BEN SOILIH at 2021-11-25T13:49:08-05:00 get_type, check'' - - - - - 3 changed files: - src/elexp.ml - src/eval.ml - src/opslexp.ml Changes: ===================================== src/elexp.ml ===================================== @@ -52,7 +52,7 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref - | Proj of U.location * elexp * symbol + | Proj of U.location * elexp * int (* Recursive `let` binding. *) | Let of U.location * (vname * elexp) list * elexp @@ -140,8 +140,8 @@ 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,(loc,str)) - -> "( _._ " ^ elexp_string lxp ^ " " ^ str ^ " )" + | 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 ===================================== @@ -462,6 +462,9 @@ 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 (l, e, i) + -> failwith "" (* Case *) | Case (loc, target, pat, dflt) ===================================== src/opslexp.ml ===================================== @@ -747,6 +747,45 @@ 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 = @@ -761,7 +800,7 @@ and check'' erased ctx e = | 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 + let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = @@ -1015,7 +1054,45 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v - | Proj (l,lxp,lbl) -> mkProj (l,lxp,lbl) + | 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) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1147,7 +1224,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) - | L.Proj (l,lxp,lbl) -> E.Proj (l, erase_type lctx lxp,lbl) + | L.Proj (l,lxp,lbl) -> failwith "cannot convert a lexp to elexp" | 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/13cf6a0ec06b3e4b6ec0a99ebb81bd82… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/13cf6a0ec06b3e4b6ec0a99ebb81bd82… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 39 commits: Introduce swappable backends for Typer.
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 27 Nov '21

27 Nov '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 252f6038 by Simon Génier at 2021-04-26T16:33:24-04:00 Introduce swappable backends for Typer. The backends themselves are objects which must implement the new backend abstract class. I also shuffled some code, mostly in the module REPL, so that is it more focused on evaluating interactive code. Finally, I moved code that was more concerned with loading regular Typer code in typer.ml and elab.ml. - - - - - 33b205c5 by Simon Génier at 2021-04-26T16:34:24-04:00 Add tests for the lexer. In addition to the tests themselves, added a few functions that were necessary. In particular there is now Pretoken.equal in Prelexer and Location.equal in Source that are equality predicates on pretokens and locations. I also added in Sexp.sexp_string support for printing the location along with its associated sexp. This is useful in tests, when we check that the locations are correct, otherwise we would print two identical sexps! - - - - - ea5cae0f by Simon Génier at 2021-04-28T13:29:47-04:00 Merge branch 'lexer-tests' - - - - - 9723f3cf by Simon Génier at 2021-04-28T13:30:29-04:00 Merge branch 'backend-object' - - - - - 73ae25a9 by Simon Génier at 2021-04-28T13:34:46-04:00 Add a backend to compile Typer to Scheme. - - - - - f8c0ef45 by Simon Génier at 2021-04-28T13:53:58-04:00 Consolidate location related code into Source. The purpose of this changeset is to take all the Location related code and to move it into the Source module. I kept the aliases in Util for now to reduce the size of this changeset, but it was inevitable that I had to add a few `let open Source.Location in` because of how fields work in OCaml (not great). Fortunately, most of these will disappear as I move more and more location related code inside the source object. I rewrote a few places to use printf instead of a series of prints, which I think are clearer. The only externally visible change is that I merged two functions that printed location in a different way. Some debug code used to print something like "Ln 32, cl 1", but now prints "foo.typer:32:1" like everywhere else. - - - - - 965cc049 by Simon Génier at 2021-04-29T11:46:14-04:00 Merge branch 'gambit' - - - - - 8ce3d27f by Simon Génier at 2021-05-10T15:14:17-04:00 Add code to check if a type declaration is positive. - - - - - 4d0dff15 by Simon Génier at 2021-05-12T15:55:42-04:00 Merge branch 'origin/consolidate-location' - - - - - f2d6d5df by Simon Génier at 2021-05-12T15:56:34-04:00 Merge branch positivity - - - - - b8959e2f by Simon Génier at 2021-05-12T21:36:47-04:00 Have the source tell its own location. Move the code that keeps track of the current line and column inside of the source object. Not only does this make sense conceptually since the source is a kind of cursor, but it will allow us to simplify the lexer code. - - - - - e7d3ed86 by Simon Génier at 2021-05-28T19:51:54-04:00 Merge branch 'source-tells-its-own-location' - - - - - c5ef2f59 by Simon Génier at 2021-05-28T20:30:37-04:00 Oops, fix tests on Windows. The prelexer considered \r to be part of presymbols with catastrophic results. - - - - - f289b62a by Simon Génier at 2021-05-29T12:12:42-04:00 Rewrite the Lexer module in terms of source objects. This might not look useful, but it will simplify a great deal our next change of add and end point to location records since all the location related code will be in there source objects. I ended up rewriting most of the Lexer. I tried to avoid doing that, but the offset handling code was so mixed up with the rest than that turned out to give worse code and a diff as unreadable. I'm pretty confident that that the changes are OK since we are still able to load pervasives.typer and I wrote a few tests for the trickier inner operators. - - - - - 8e1be507 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 Fix nix shell and dune details - - - - - dc07e915 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 * btl/pervasive.typer (type-impl): Accept implicit type params. Also, allow type definitions at other type levels than 0, with an annotation. - - - - - b8d1df5b by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 * btl/pervasive.typer (type-impl): Keep the constructors in order. - - - - - 8d9a2367 by Simon Génier at 2021-06-09T12:28:31-04:00 Merge branch 'lexer-with-source' - - - - - 4fb0ccd3 by Simon Génier at 2021-06-09T12:40:18-04:00 Shorten the names of a few methods on source objects. These names were redundants. For instance in `current_offset`, the `current` part is already hinted at by the fact that source objects are a kind of cursor. Overall I think the new names a clearer since they are more concise. - - - - - a7ac505a by Jean-Alexandre Barszcz at 2021-08-10T14:58:56-04:00 * src/elab.ml (elaborate): `check_inferred` when a type is given. Previously, `check_inferred` was mainly called from `check`, but some calls to `elaborate` play the same role as `check` (if an expected type is given), so we move this logic to `elaborate`. This allows implicit arguments to be instantiated in more places. For example, calls and variables are always inferred, but without `check_inferred`, the type provided to `elaborate` would be ignored. - - - - - aff91a51 by Simon Génier at 2021-09-28T17:16:11-04:00 Merge branch 'shorten-source-methods' - - - - - e8a59f86 by Simon Génier at 2021-09-28T17:25:19-04:00 Replace raw offsets with points which also track line and column. - - - - - 87882dea by Simon Génier at 2021-09-28T17:45:35-04:00 Compute location inside the source from the given point. - - - - - fce0fac4 by Simon Génier at 2021-09-28T18:16:00-04:00 Upgrade to OCaml 4.11. * Update the README * Remove a few functions that are now part of the standard library. - - - - - 01e6295a by Simon Génier at 2021-09-29T11:09:53-04:00 Remove doc strings from Typer. Doc strings are a good idea, but the implementation that was in Typer was not. They should not be hardcoded in the syntax of the langague, but rather a good implementation would use the metaprogramming capabilities of Typer to make them part of the standard library. - - - - - 8cfa2243 by Simon Génier at 2021-09-30T11:39:27-04:00 Locations now track their end points. - - - - - db1cf4da by Stefan Monnier at 2021-10-06T09:38:32-04:00 Merge remote-tracking branch 'gitlab/ocaml-4.11' into trunk - - - - - 8efdff37 by Stefan Monnier at 2021-10-06T10:01:02-04:00 Merge remote-tracking branch 'gitlab/purge-docstr' into trunk - - - - - 89cc2432 by Stefan Monnier at 2021-10-06T10:01:55-04:00 Merge remote-tracking branch 'gitlab/source-spans-2' into trunk - - - - - 0f4e9461 by Soilih BEN SOILIH at 2021-10-28T09:50:01-04:00 - - - - - - f832b339 by Simon Génier at 2021-10-28T10:43:05-04:00 Remove artisanal formatting functions in favour of printf. - - - - - 7f6f32dd by Simon Génier at 2021-10-28T10:43:38-04:00 Printfify log functions. - - - - - edf888bc by Simon Génier at 2021-10-28T11:00:18-04:00 Typer accepts subcommands (repl, compile, run) like git. This will hopefully simplify option handling as I add more modes of operation with their own option for running Typer code in a Gambit subprocess. - - - - - 16eab611 by Soilih BEN SOILIH at 2021-11-05T19:17:24-04:00 merge - - - - - e26aeaa6 by Soilih BEN SOILIH at 2021-11-09T13:30:08-05:00 untouched - - - - - 65076856 by Soilih BEN SOILIH at 2021-11-14T17:16:38-05:00 - - - - - - 39ec2f05 by Soilih BEN SOILIH at 2021-11-27T23:24:15-05:00 upgrade to current state of typer - - - - - bf1bb921 by Soilih BEN SOILIH at 2021-11-27T23:25:22-05:00 Merge branch 'soilih-merge' into soilih-test-avec-ast - - - - - 9a5b03e0 by Soilih BEN SOILIH at 2021-11-27T23:30:00-05:00 config files - - - - - 30 changed files: - GNUmakefile - README.md - btl/builtins.typer - btl/pervasive.typer - debug_util.ml - dune - emacs/typer-mode.el - − extract - − linol - samples/acc.typer - − samples/soilih.typer - shell.nix - src/REPL.ml - src/backend.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/dune - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - − src/float.ml - src/fmt.ml - + src/gambit.ml - src/heap.ml - − src/int.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/c71f00d07f0ced128c0ae047b5dd8665… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/c71f00d07f0ced128c0ae047b5dd8665… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] elexp, lexp, opslexp, positivity, unification
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 18 Nov '21

18 Nov '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: 13cf6a0e by Soilih BEN SOILIH at 2021-11-18T02:55:29-05:00 elexp, lexp, opslexp, positivity, unification - - - - - 5 changed files: - src/elexp.ml - src/lexp.ml - src/opslexp.ml - src/positivity.ml - src/unification.ml Changes: ===================================== src/elexp.ml ===================================== @@ -52,6 +52,8 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref + | Proj of U.location * elexp * symbol + (* 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,8 @@ 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,(loc,str)) + -> "( _._ " ^ elexp_string lxp ^ " " ^ str ^ " )" | Cons (_, (_, s)) -> "datacons(" ^ s ^")" | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b) ===================================== src/lexp.ml ===================================== @@ -986,7 +986,7 @@ and lexp_str ctx (exp : lexp) : string = | Var ((_loc, name), idx) -> maybename name ^ (index idx) ; | Proj (l,lxp,(loc,str)) - -> "( __.__ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )" | Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) ===================================== src/opslexp.ml ===================================== @@ -1015,7 +1015,7 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v - | Proj (l,lxp,lbl) -> get_type ctx lxp + | Proj (l,lxp,lbl) -> mkProj (l,lxp,lbl) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1147,7 +1147,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) - | L.Proj (l,lxp,lbl) -> erase_type lctx lxp + | L.Proj (l,lxp,lbl) -> E.Proj (l, erase_type lctx lxp,lbl) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) | L.Lambda (P.Aerasable, _, _, body) ===================================== src/positivity.ml ===================================== @@ -116,6 +116,7 @@ and positive' index lexp = * as the Call applies as a degenerate case with no arguments. *) -> 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. *) ===================================== 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/-/commit/13cf6a0ec06b3e4b6ec0a99ebb81bd82c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/13cf6a0ec06b3e4b6ec0a99ebb81bd82c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] fixing p.m in opslexp
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 15 Nov '21

15 Nov '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: 61f50b42 by Soilih BEN SOILIH at 2021-11-14T21:22:37-05:00 fixing p.m in opslexp - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -926,6 +926,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 @@ -1014,6 +1015,7 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v + | Proj (l,lxp,lbl) -> get_type ctx lxp | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1145,6 +1147,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) + | L.Proj (l,lxp,lbl) -> erase_type lctx lxp | 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/-/commit/61f50b4202e0c8fa583d914bd5247e563… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/61f50b4202e0c8fa583d914bd5247e563… You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][soilih] 6 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 14 Nov '21

14 Nov '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 9a56ef06 by Soilih BEN SOILIH at 2021-11-04T09:51:17-04:00 - - - - - - c136a43a by Soilih BEN SOILIH at 2021-11-05T17:13:24-04:00 - - - - - - e43859b8 by Soilih BEN SOILIH at 2021-11-05T20:12:15-04:00 value in ctx - - - - - 615c5f4a by Soilih BEN SOILIH at 2021-11-10T22:27:14-05:00 - - - - - - b91bb767 by Soilih BEN SOILIH at 2021-11-14T08:28:41-05:00 fixing type printing - - - - - c71f00d0 by Soilih BEN SOILIH at 2021-11-14T08:30:04-05:00 - - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -772,18 +772,46 @@ let verify_varbind (env: Debruijn.env_elem) : (int * Lexp.lexp) option = | ForwardRef-> None | LetDef (idx,lxp) -> Some (idx,lxp) +(* Search if the vname is in the context *) +let search_name_in_ctx (lctx: Debruijn.lexp_context) (lxp: Lexp.lexp) = + let lctx_l = Myers.list lctx in + let rec foo lst comp rlst = + match lst with + | [] -> rlst + | ((vn, Lexp.LetDef (idx, lxpv), _) as hd)::tl + -> if String.equal (Lexp.lexp_string lxp) (Lexp.lexp_string lxpv) then + foo tl (comp + 1) ((hd,comp)::rlst) + else foo tl (comp + 1) rlst + | _::tl -> foo tl (comp + 1) rlst + in foo lctx_l 0 [] + +(* use search_name_in_ctx *) +let use_search_name_in_ctx lctx lxp = + let rlst = search_name_in_ctx lctx lxp in + match rlst with + | [] -> failwith "no name found !!!" + | hd::_ -> let (((l,s) as vn,vrbd,ltp),i) = hd in + match s with + | None -> failwith "no name found !!!" + | Some _-> let lx = Lexp.mkVar (vn,i) in + Lexp.lexp_string lx + + (* Search if the is the given value in the context *) let value_in_ctx (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : Debruijn.env_elem * int = let (_, _, lctxm, _) = ectx in let lctx = Myers.list lctxm in + (*let rlctx = List.rev lctx in*) let rec foo (lctx: Debruijn.env_elem list) (lxp: Lexp.lexp) (comp:int)= match lctx with | [] -> failwith "The value is not in ectx !" - | hd::tl -> match verify_varbind hd with - | None -> foo tl lxp (comp + 1) - | Some (idx,lxpv) -> if String.equal (Lexp.lexp_string lxp) (Lexp.lexp_string lxpv) then (hd, comp) - else foo tl lxp (comp + 1) - in foo lctx lxp 1 + | ((vn, LetDef (idx, lxpv), _) as hd)::tl + -> let lx = Lexp.mkVar (vn,comp) in + if Opslexp.conv_p lctxm lx lxp then (hd, comp) + else foo tl lxp (comp + 1) + | _::tl -> foo tl lxp (comp + 1) + + in foo lctx lxp 0 (* Search the key of a varbind in senv_type *) let key_of_varbind (ectx: Debruijn.elab_context) (el: Debruijn.env_elem) (idx: int): string = @@ -817,28 +845,25 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte (*=====================================Symbols=====================================*) -let filter_the_list_list (list_list: list_in_list) : list_in_list = +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),_,_) = List.nth x 0 in + let ((_,s),_,_) = x in match s with | None -> false | Some _ -> true ) list_list -let take_all_list_el (list_list: list_in_list) = +let take_all_list_el (list_list: list_in_list) : (vname * Lexp.lexp * Lexp.lexp) list = let rec foo (ll:list_in_list) ret_list = match list_list with | [] -> ret_list - | [n] -> List.append n ret_list - | [hd;tl] -> let apl = List.append hd tl in - List.append apl ret_list - | hd::ml::tl -> let apl = List.append hd ml in - foo tl (List.append apl ret_list) + | hd::tl -> foo tl (List.append hd ret_list) in foo list_list [] + let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = - let filtred_list = filter_the_list_list list_list in - let lst = take_all_list_el filtred_list in + let lst = take_all_list_el list_list in + let filtred_list = filter_the_list_list lst in List.map ( fun x -> let ((l,s),_,_) = x in let range = lsp_range_of_loc_for_symbol l in @@ -849,7 +874,7 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = ~range:range ~selectionRange:range () - ) lst + ) filtred_list (*=====================================End Symbols=================================*) @@ -1129,8 +1154,8 @@ class lsp_server = 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 s = try search_the_key ectx l_type - with exe -> Lexp.lexp_string_for_lsp l_type + let s = try use_search_name_in_ctx l_ctx l_type + with exe -> Lexp.lexp_string_for_lsp l_type in (*let s = Lexp.lexp_string_for_lsp l_type in*) let r = Lsp.Types.Hover.create @@ -1186,7 +1211,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 @@ -1195,7 +1220,7 @@ class lsp_server = let r = create_symbols list_list in let e = Some (`DocumentSymbol r) in let f = Linol_lwt.return e in f - + *) end @@ -1348,6 +1373,23 @@ 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======================================*) @@ -1359,6 +1401,7 @@ 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/4e3f9651133236b3213e12cd2b326a08… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/4e3f9651133236b3213e12cd2b326a08… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] 4 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 11 Nov '21

11 Nov '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: 11f83513 by Soilih BEN SOILIH at 2021-11-10T09:00:02-05:00 - - - - - - 83c17570 by Soilih BEN SOILIH at 2021-11-11T02:00:16-05:00 - - - - - - 4d2bb66c by Soilih BEN SOILIH at 2021-11-11T09:56:49-05:00 - - - - - - 58600d02 by Soilih BEN SOILIH at 2021-11-11T20:16:17-05:00 fixing p.m problems in lexp, elab, inverse_subst - - - - - 3 changed files: - src/elab.ml - src/inverse_subst.ml - src/lexp.ml Changes: ===================================== src/elab.ml ===================================== @@ -429,6 +429,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 ===================================== 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,7 +66,7 @@ type ltype = lexp | Sort of U.location * sort | Builtin of symbol * ltype | Var of vref - | Proj of U.location * string * lexp + | 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 @@ -246,6 +246,9 @@ 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`. *) @@ -310,6 +313,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)) @@ -330,6 +334,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" @@ -592,6 +597,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 @@ -655,6 +661,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 @@ -673,6 +680,9 @@ 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)]) @@ -975,6 +985,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 View it on GitLab: https://gitlab.com/monnier/typer/-/compare/16eab6116a4d9414d2a0b4e9eb64af46… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/16eab6116a4d9414d2a0b4e9eb64af46… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] 103 commits: connexion du serveur lsp et typer
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 05 Nov '21

05 Nov '21

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: cb44bcd4 by Soilih BEN SOILIH at 2021-03-10T18:43:05-07:00 connexion du serveur lsp et typer - - - - - 62dad551 by Soilih BEN SOILIH at 2021-03-11T18:50:46-07:00 Licence specifications - - - - - 91c0bb50 by Soilih BEN SOILIH at 2021-03-13T22:36:05-07:00 commit - - - - - 74b6b623 by Soilih BEN SOILIH at 2021-03-22T09:15:37-06:00 first commit - - - - - a4a9cf9e by Soilih BEN SOILIH at 2021-03-26T21:48:38-06:00 fonction readstring - - - - - cc0bd4d8 by Soilih BEN SOILIH at 2021-03-30T20:58:46-06:00 diagnostics - - - - - bde2d9b9 by Soilih BEN SOILIH at 2021-03-30T21:05:26-06:00 Merge branch 'master' of https://gitlab.com/monnier/typer - - - - - 1b7204e3 by Soilih BEN SOILIH at 2021-03-31T10:23:12-06:00 Errors handling - - - - - 7abb48c5 by Soilih BEN SOILIH at 2021-04-03T08:12:45-06:00 little bug resolution - - - - - be768c34 by Soilih BEN SOILIH at 2021-04-08T16:52:39-06:00 h - - - - - c0f859bc by Soilih BEN SOILIH at 2021-04-08T17:03:41-06:00 update - - - - - 94ab822b by Soilih BEN SOILIH at 2021-04-08T17:14:00-06:00 Merge branch 'extract-args-from-repl' of https://gitlab.com/monnier/typer into extract - - - - - f847a4c1 by Soilih BEN SOILIH at 2021-04-08T17:17:15-06:00 extract - - - - - f9f40536 by Soilih BEN SOILIH at 2021-04-08T18:18:36-06:00 commit - - - - - e58ae4ad by Soilih BEN SOILIH at 2021-04-08T18:28:48-06:00 bugs - - - - - 2941d939 by Soilih BEN SOILIH at 2021-04-09T13:38:10-06:00 fix merge conflict - - - - - 9836b205 by Soilih BEN SOILIH at 2021-04-09T13:40:42-06:00 merge conflict - - - - - 7ad32eb9 by Soilih BEN SOILIH at 2021-04-09T13:44:17-06:00 lsp args - - - - - 6add7c68 by Soilih BEN SOILIH at 2021-04-09T13:48:40-06:00 lsp - - - - - b2fe2a90 by Soilih BEN SOILIH at 2021-04-09T13:50:10-06:00 readstring - - - - - 64522966 by Soilih BEN SOILIH at 2021-04-09T14:17:59-06:00 emacs file - - - - - a1b864fd by Soilih BEN SOILIH at 2021-04-09T19:45:28-06:00 fix declaration order - - - - - fad7704f by Soilih BEN SOILIH at 2021-04-11T21:01:01-06:00 linol update - - - - - 4bd05656 by Soilih BEN SOILIH at 2021-04-14T21:19:06-06:00 return the AST with the logs - - - - - 620fabd9 by Soilih BEN SOILIH at 2021-04-15T14:09:36-06:00 resolving the exception - - - - - d076d86b by Soilih BEN SOILIH at 2021-04-17T09:09:25-06:00 empty - - - - - 98f2b0c6 by Soilih BEN SOILIH at 2021-04-20T14:16:53-06:00 hover and definition - - - - - 5ee099ae by Soilih BEN SOILIH at 2021-04-21T09:39:33-06:00 m - - - - - 79fc9315 by Soilih BEN SOILIH at 2021-04-21T09:50:16-06:00 -* - - - - - 8ad9bedf by Soilih BEN SOILIH at 2021-04-23T03:21:14-06:00 - - - - - - 3eb5e83e by Soilih BEN SOILIH at 2021-04-23T04:07:32-06:00 hover and definition update - - - - - 7783aed8 by Soilih BEN SOILIH at 2021-04-26T14:08:17-06:00 kind of completion and command(still to fix) - - - - - 69a3e9ff by Simon Génier at 2021-04-26T16:46:56-04:00 Add tests for the lexer. In addition to the tests themselves, added a few functions that were necessary. In particular there is now Pretoken.equal in Prelexer and Location.equal in Source that are equality predicates on pretokens and locations. I also added in Sexp.sexp_string support for printing the location along with its associated sexp. This is useful in tests, when we check that the locations are correct, otherwise we would print two identical sexps! - - - - - edbb3f90 by Simon Génier at 2021-04-26T16:47:10-04:00 Introduce swappable backends for Typer. The backends themselves are objects which must implement the new backend abstract class. I also shuffled some code, mostly in the module REPL, so that is it more focused on evaluating interactive code. Finally, I moved code that was more concerned with loading regular Typer code in typer.ml and elab.ml. - - - - - f578df6d by Simon Génier at 2021-04-26T20:46:21-04:00 Consolidate location related code in Source. The purpose of this changeset is to take all the Location related code and to move it into the Source module. There are many changed lines, but most of them are simple renaming. I rewrote a few places to use printf instead of a series of prints, which I think are clearer. The only externally visible change is that I merged two functions that printed location in a different way. Some debug code used to print something like "Ln 32, cl 1", but now prints "foo.typer:32:1" like everywhere else. - - - - - 0e18db2e by Simon Génier at 2021-04-26T21:33:57-04:00 Have the source tell its own location. Move the code that keeps track of the current line and column inside of the source object. Not only does this make sense conceptually since the source is a kind of cursor, but it will allow us to simplify the lexer code. - - - - - 396bafa3 by Simon Génier at 2021-04-26T21:39:40-04:00 Rename Pretoken -> Presymbol. - - - - - bdfe5646 by Simon Génier at 2021-04-27T13:09:13-04:00 Rewrite the Lexer module in terms of source objects. This might not look useful, but it will simplify a great deal our next change of add and end point to location records since all the location related code will be in there source objects. I ended up rewriting most of the Lexer. I tried to avoid doing that, but the offset handling code was so mixed up with the rest than that turned out to give worse code and a diff as unreadable. I'm pretty confident that that the changes are OK since we are still able to load pervasives.typer and I wrote a few tests for the trickier inner operators. - - - - - eab63fcc by Simon Génier at 2021-04-27T13:19:17-04:00 Shorten the names of a few methods on Source.t. - - - - - ee0b598c by Simon Génier at 2021-04-27T13:29:38-04:00 Replace raw offsets with points which also track line and column. - - - - - 46e3a82a by Simon Génier at 2021-04-27T13:48:29-04:00 Compute location inside the source from the given point. - - - - - 1ed0a82a by Simon Génier at 2021-04-27T14:00:42-04:00 Documentation comments are now an optional. - - - - - 3818bc2a by Simon Génier at 2021-04-27T15:25:04-04:00 Locations track their end point. - - - - - d15507ff by Soilih BEN SOILIH at 2021-04-27T21:17:21-06:00 - - - - - - 63f44e8e by Soilih BEN SOILIH at 2021-04-27T21:23:44-06:00 - - - - - - 84e4416b by Soilih BEN SOILIH at 2021-04-27T22:58:33-06:00 + - - - - - b22e1c28 by Soilih BEN SOILIH at 2021-04-28T08:48:54-06:00 - - - - - - 1e9c5748 by Soilih BEN SOILIH at 2021-04-28T09:16:21-06:00 - - - - - - cdfecb61 by Soilih BEN SOILIH at 2021-04-30T18:56:48-06:00 - - - - - - 502b6879 by Soilih BEN SOILIH at 2021-05-01T12:59:04-06:00 - - - - - - b613f361 by Soilih BEN SOILIH at 2021-05-01T13:49:37-06:00 - - - - - - 981d60fe by Soilih BEN SOILIH at 2021-05-07T04:45:37-06:00 update location and hover - - - - - bad1664f by Soilih BEN SOILIH at 2021-05-07T04:50:32-06:00 resolve merge conflict - - - - - cfc76735 by Soilih BEN SOILIH at 2021-05-08T16:55:49-06:00 update the hover - - - - - ee628865 by Soilih BEN SOILIH at 2021-05-08T16:56:09-06:00 Merge branch 'soilih-alpha' into soilih - - - - - 16b2a6b5 by Soilih BEN SOILIH at 2021-05-08T17:50:59-06:00 - - - - - - 9d8bd5d9 by Soilih BEN SOILIH at 2021-05-10T10:31:41-06:00 update the function browse_lexp - - - - - 395d075f by Soilih BEN SOILIH at 2021-05-12T10:24:19-06:00 update hover - - - - - 85a05e35 by Soilih BEN SOILIH at 2021-05-12T10:27:02-06:00 - - - - - - 10ccddf1 by Soilih BEN SOILIH at 2021-05-14T09:33:40-06:00 - - - - - - c3aa818e by Soilih BEN SOILIH at 2021-05-15T18:49:23-06:00 browse_lexp update - - - - - fde849c9 by Soilih BEN SOILIH at 2021-05-17T14:24:34-06:00 update completion, diagnostics - - - - - a3ccd6b2 by Soilih BEN SOILIH at 2021-05-20T19:39:18-06:00 resolve completion, diagnostics problems...case still not working* - - - - - a1a11af5 by Soilih BEN SOILIH at 2021-05-26T02:37:49-06:00 browse lexp update - - - - - 8cc99a68 by Soilih BEN SOILIH at 2021-05-31T23:30:38-06:00 improve print and log error - - - - - 9abad61f by Soilih BEN SOILIH at 2021-06-12T13:16:16-06:00 completion, readstring, check, log - - - - - 8e4c5775 by Soilih BEN SOILIH at 2021-06-15T07:07:01-06:00 a better way to complete - - - - - 0a79b565 by Soilih BEN SOILIH at 2021-06-16T20:53:17-06:00 elab_check - - - - - 170bef61 by Soilih BEN SOILIH at 2021-06-17T09:50:42-06:00 - - - - - - 859393dd by Soilih BEN SOILIH at 2021-06-21T23:54:06-06:00 - - - - - - 79ab4063 by Soilih BEN SOILIH at 2021-06-22T20:09:28-06:00 - - - - - - bb0904ae by Soilih BEN SOILIH at 2021-06-29T15:58:45-06:00 fixing context - - - - - d83e49da by Soilih BEN SOILIH at 2021-07-02T23:07:13-06:00 fixing let, adding got to definition - - - - - 8e377da2 by Soilih BEN SOILIH at 2021-07-02T23:22:44-06:00 remove unecessary try with - - - - - ba970f5c by Soilih BEN SOILIH at 2021-07-03T00:29:12-06:00 fixing the case Case - - - - - 5025a06d by Soilih BEN SOILIH at 2021-07-13T10:53:05-06:00 test hover - - - - - 29b5783a by Soilih BEN SOILIH at 2021-07-13T10:55:44-06:00 test hover. - - - - - 06a6ffa3 by Soilih BEN SOILIH at 2021-07-16T21:57:52-06:00 - - - - - - 3ed77305 by Soilih BEN SOILIH at 2021-07-21T00:49:17-06:00 definition with the identification and update the Inductive - - - - - 1d141dbd by Soilih BEN SOILIH at 2021-08-13T10:57:54-06:00 fixing context - - - - - 31c030ee by Soilih BEN SOILIH at 2021-08-15T23:03:03-06:00 fixing context errors - - - - - 98548aee by Soilih BEN SOILIH at 2021-08-17T23:00:07-06:00 completion from buffer - - - - - 8190e3c3 by Soilih BEN SOILIH at 2021-08-28T23:44:36-06:00 complete_oth - - - - - 6a99c654 by Soilih BEN SOILIH at 2021-09-02T09:32:47-06:00 list myers and completions - - - - - d0cf7df3 by Soilih BEN SOILIH at 2021-09-02T11:13:18-06:00 fix completion - - - - - da59e1c2 by Soilih BEN SOILIH at 2021-09-03T11:16:21-06:00 - - - - - - 1339b2e0 by Soilih BEN SOILIH at 2021-09-03T12:55:17-06:00 fixing completion - - - - - b178ecb3 by Soilih BEN SOILIH at 2021-09-03T12:56:45-06:00 fixing Myers.list - - - - - 6c5dfc8b by Soilih BEN SOILIH at 2021-09-03T15:25:55-06:00 considering the order in the completion suggestions - - - - - 7e546235 by Soilih BEN SOILIH at 2021-09-12T23:52:44-06:00 fixing some order issues in completions - - - - - 9d9ea020 by Soilih BEN SOILIH at 2021-09-27T15:05:21-06:00 considerate vname loc and ltype - - - - - 83744967 by Soilih BEN SOILIH at 2021-10-04T14:47:34-06:00 fix the case Case - - - - - 1403fe8b by Soilih BEN SOILIH at 2021-10-13T17:33:39-06:00 fix warnings - - - - - 645d3261 by Soilih BEN SOILIH at 2021-10-14T00:39:33-06:00 - - - - - - 09aacbad by Soilih BEN SOILIH at 2021-10-14T22:37:00-06:00 fix the completion problem at the end of the file - - - - - 53c2f370 by Soilih BEN SOILIH at 2021-10-16T20:13:25-04:00 - - - - - - acf01ebf by Soilih BEN SOILIH at 2021-10-17T03:06:02-04:00 adding symbols - - - - - 2910ba93 by Soilih BEN SOILIH at 2021-10-18T21:54:10-04:00 my symbol - - - - - 00d0160e by Soilih BEN SOILIH at 2021-10-18T23:57:07-04:00 fixing on_req_symbol method - - - - - 4e3f9651 by Soilih BEN SOILIH at 2021-10-19T00:02:06-04:00 - - - - - - 9a56ef06 by Soilih BEN SOILIH at 2021-11-04T09:51:17-04:00 - - - - - - c136a43a by Soilih BEN SOILIH at 2021-11-05T17:13:24-04:00 - - - - - - 16eab611 by Soilih BEN SOILIH at 2021-11-05T19:17:24-04:00 merge - - - - - 2 changed files: - + .vscode/launch.json - src/lexp.ml Changes: ===================================== .vscode/launch.json ===================================== @@ -0,0 +1,15 @@ +{ + // Use IntelliSense to learn about possible attributes. + // Hover to view descriptions of existing attributes. + // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387 + "version": "0.2.0", + "configurations": [ + { + "type": "pwa-chrome", + "request": "launch", + "name": "Launch Chrome against localhost", + "url": "http://localhost:8080", + "webRoot": "${workspaceFolder}" + } + ] +} \ No newline at end of file ===================================== 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 * string * lexp | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp @@ -524,6 +525,7 @@ let rec lexp_location e = | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l + | Proj (l,_,_) -> l (********* Normalizing a term *********) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/edf888bcde814fd010f53b4cf94501c0… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/edf888bcde814fd010f53b4cf94501c0… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch add-proj
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 05 Nov '21

05 Nov '21

Soilihi BEN SOILIHI BOINA pushed new branch add-proj at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/add-proj You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch remove-artisanal-printing
by Simon Génier (＠ilovemonoids) 02 Nov '21

02 Nov '21

Simon Génier deleted branch remove-artisanal-printing at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch typer-subcommands
by Simon Génier (＠ilovemonoids) 02 Nov '21

02 Nov '21

Simon Génier deleted branch typer-subcommands at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Novembre 2021