Simon Génier pushed to branch simon-genier at Stefan / Typer Commits: 4bcb4b11 by Stefan Monnier at 2020-03-17T13:59:49-04:00 * src/env.ml (BI): Use `Z` rather than `Big_int` * GNUmakefile (OBFLAGS): Use Zarith rather than Num - - - - - 93c051db by Stefan Monnier at 2020-03-17T14:06:01-04:00 * samples/hott.typer: New file - - - - - b4bacaf0 by Stefan Monnier at 2020-03-17T14:26:41-04:00 * src/opslexp.ml (impredicative_erase): Disable it (impredicative_universe_poly): Rename from deep_universe_poly. - - - - - 93cb1223 by Stefan Monnier at 2020-03-18T23:30:00-04:00 Fix up various issues with universe levels * src/builtin.ml (type_eq): Use `mkVar`. * src/elab.ml (elaborate): Use `mkVar`. (infer_level): Add suport for ∪ in type level expressions. * src/lexp.ml (mkSLlub'): Add a crutch. (lexp_unparse, lexp_print): Clarify output of TypeLevel. * src/opslexp.ml (level_canon, level_leq): Move earlier. (conv_p'): Use to fix handling of `SLlub`. (mkSLlub): Fix thinko. (check'', get_type): Use `mkVar`. * src/unification.ml (unify): Improve unification of SLlub. - - - - - c081c586 by Stefan Monnier at 2020-03-20T11:28:31-04:00 - - - - - - 86d4a83d by Stefan Monnier at 2020-03-21T18:02:02-04:00 * unification.ml: Return just a list rather than an list option Additionally, keep track of the ctx and annotate whether there's a possibility unification could succeed at some other time. * src/lexp.ml (constraints): Move to unification.ml * src/unification.ml (constraint_kind): New type. (constraints): Rewrite. (unify_and): Remove, use `@` instead. - - - - - 402bdbe0 by Stefan Monnier at 2020-03-27T16:04:24-04:00 Infer type of `case` target from patterns * src/elab.ml (check_case): Infer the type of the target from the patterns when applicable. * src/opslexp.ml (check''): Be careful to always pass the inferred type and the expected type in the same order. * src/unification.ml (create_metavar_1): New function extracted from create_metavar. (create_metavar): Use it. (common_subset, s_offset): New functions. (unify_metavar): Use them to properly handle the case of unifying a metavar with itself where the two substitutions are different. * btl/builtins.typer (Eq_comm): Simplify type annotation a bit. * btl/pervasive.typer (List_head1, List_head, List_tail, List_concat) (I, List_map-fst, List_map-snd): Remove unnecessary type annotation. - - - - - 56ed1196 by Stefan Monnier at 2020-04-02T17:04:44-04:00 Misc tweaks; use a bit more universe polymorphism; improve some errors * btl/builtins.typer: Make better use of generalization to avoid `≡`. (List): * btl/pervasive.typer (Option, Not): Make them universe-polymorphic. * src/builtin.ml (register_builtin_csts): Add name `Type0`. * src/debruijn.ml (type_level_sort): Rename from `sort_level`. * src/elab.ml (check_inferred): Give more complete error info. (infer_level): Use `newMetalevel`. * src/lexp.ml (lexp_head): New function. (mkSLlub', lexp_name): Use it. (lexp_unparse, lexp_print): Fix printout of `type_level_sort`. * tests/eval_test.ml ("has-attribute", "Implicit Arguments"): Disable tests. - - - - - f2b81386 by Stefan Monnier at 2020-04-02T19:31:41-04:00 * src/elab.ml (meta_to_var): Fix debruijn error. * btl/pervasive.typer (Decidable): Make it universe-polymorphic. * src/builtin.ml (register_builtin_csts): Fix Type0 typo. - - - - - 85d12bf5 by Stefan Monnier at 2020-04-07T22:21:39-04:00 * src/elab.ml (infer_and_generalize_type): Add more exceptions Don't generalize over the level of the final return type if it doesn't appear elsewhere. * btl/builtins.typer (Eq_cast): Give a name to the proof arg. - - - - - 4993afa5 by Stefan Monnier at 2020-04-07T23:15:21-04:00 * src/lexp.ml (srename): New function * src/unification.ml (unify): * src/opslexp.ml (conv_p'): * src/elab.ml (sform_lambda): Use it. - - - - - 63f7644b by Stefan Monnier at 2020-04-07T23:21:05-04:00 * src/elab.ml (meta_to_var): Rework to be able to infer universe levels (generalize): Adjust for new calling convention of `meta_to_var` and also for the fact that `meta_to_var` now takes care of the S.shift for us. - - - - - 886a3589 by Stefan Monnier at 2020-04-08T18:07:18-04:00 Remove most uses of L.clean * src/elab.ml (elab_check_sort, elab_check_def, infer_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (track_fv): Skip `L.clean` since `fv` already cleans up on the fly. (lexp_eval): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. (sform_new_attribute, sform_add_attribute, sform_built_in): Explicitly call `clean` now that `lexp_close` doesn't do it any more. * src/eval.ml (from_lctx): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. * src/lexp.ml (print_context_value): Remove `Expr` constructor. (pretty_ppctx): Remove unused `parent` and now unused `metavar`. (smap_lexp, pp_parent, pp_meta, set_parent, set_parent): Remove functions.. (lexp_str): Don't call `set_parent` any more. Rewrite metavar case to use `metavar_lookup` rather than `clean`. * src/opslexp.ml (lexp_close): Don't call `clean` any more. (conv_p', mkSLlub): Skip `L.clean` since `level_canon` already cleans up on the fly. (check''.assert_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (erase_type): Clean up metavars on the fly. * src/unification.ml (unify_metavar): Skip `L.clean` since `lexp_string` already cleans up on the fly. - - - - - bf3c818e by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add a nix shell * shell.nix : When using nixpkgs/nixos, run `nix-shell` to get a shell with Typer's dependencies available. - - - - - c39ff3d5 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Improve the implementation of Sexp.dispatch * src/elab.ml (sexp_dispatch) : Sexp.dispatch assumed that its arguments were closures. Instead, we use eval_call and also accept constructors, builtins, etc. - - - - - 7b623a26 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add the inductive type `Sexp_wrapper` to match on sexps * btl/pervasive.typer : Add the inductive type `Sexp_wrapper` to wrap the Sexp values in typer code, and the function `Sexp_wrap` to do the wrapping. This makes possible the use of pattern matching to destructure Sexps instead of the more verbose calls to `Sexp_dispatch`. - - - - - 8419c419 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix lexp_whnf when the case scrutinee is a call * src/opslexp.ml (lexp_whnf) : Make sure that we take the WHNF of the function when the scrutinee of a case expression is a call, before checking that the function is a constructor. Otherwise, expressions like `case (let ... in (constructor ...))` fail to reduce, for example. - - - - - cc20d841 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix some lexp constructor calls where hash-consing has been forgotten - - - - - 2bd6aa15 by Stefan Monnier at 2020-08-10T23:52:31-04:00 * btl/builtins.typer (Eq_comm): Update FIXME - - - - - 28d16874 by irradiee at 2020-08-14T05:59:20-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp - - - - - f04cab52 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Delay parsing of declarations until elaboration for define-operator * elab.ml (lexp_p_decls): Add a parameter for unparsed tokens, so that later declarations can be parsed in a context with newly declared operators - - - - - 456370bc by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Remove the parsing error for tightly binding postfix operators - - - - - 8beb9266 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Dump the evaluation context when the variable names don't match - - - - - 2e00884b by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Assign the builtins Int.+, etc to suitable variables Int_+, etc. _+_ can be Int.+ by default, but we should also keep that value in Int_+ in case _+_ gets reassigned (with a num typeclass, for instance). - - - - - ac4cc3a5 by Jean-Alexandre Barszcz at 2020-08-20T15:01:14-04:00 Apply the instantiated metavariable substs when displaying lexps - - - - - f0b33b28 by Jean-Alexandre Barszcz at 2020-08-20T15:01:36-04:00 Replace instantiated metavars when checking syntactic equality - - - - - 68f25184 by irradiee at 2020-08-24T13:11:01-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp - - - - - 588b6327 by Jean-Alexandre Barszcz at 2020-09-04T23:06:53-04:00 Fix `lexp_whnf` for Case A substitution built with `cons`es happens all at once, in the sense that the terms in such a list are substituted independently, and thus should not be shifted one relative to another. This commit removes such a shift that was made by mistake in the computation of the WHNF of a `Case` redex. The shift caused debruijn indexing errors in the body of branches with multiple fields. Additionnally, this commit removes the arguments to the inductive type from the substitution applied to the branch, since they are not bound by the case. - - - - - 115d8b01 by Simon Génier at 2020-09-09T12:06:50-04:00 Make eval tests throw on a compilation failure. - - - - - e8257259 by Simon Génier at 2020-09-09T12:06:59-04:00 Remove commented eval test. - - - - - 940ade63 by Simon Génier at 2020-09-09T12:06:59-04:00 Do not print callstack of test handler. This line always print the same callstack, that of the handler, which gives no information about why the test failed. - - - - - 53c514f5 by Simon Génier at 2020-09-09T12:06:59-04:00 Actually record the backtrace of exceptions while testing. - - - - - e0d4964e by Simon Génier at 2020-09-09T12:06:59-04:00 Print compiler log on a compilation error in tests. - - - - - e290b701 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix implicit arguments test. - - - - - 5f740bf1 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix case test with generic types. - - - - - b6466a2b by Simon Génier at 2020-09-09T12:07:23-04:00 Fix the rest of the eval tests. - - - - - 2041b4dd by Simon Génier at 2020-09-09T12:07:34-04:00 Remove = at the end of the flags to the test driver. I think the intention was to have GNU style flags like --verbose=3, but that does not even work. - - - - - 56e4fbed by Simon Génier at 2020-09-09T13:24:41-04:00 Easier elaboration tests. I extracted these changes from another branch since I will need them for yet another. Ther should make elaboration tests easier to write. * New assertions reduce the amount of code to check the results. * Correctly restore state to be able to compare metavariables in two different code fragments. - - - - - 9d41029c by Simon Génier at 2020-09-09T13:24:48-04:00 Rework add_test to avoid warnings. - - - - - 10c27014 by Simon Génier at 2020-09-09T13:24:48-04:00 Make success and failure values. - - - - - 18f49df0 by Simon Génier at 2020-09-09T13:31:55-04:00 Make expected an optional argument in elaboration tests. - - - - - b7eb8f08 by Simon Génier at 2020-09-09T14:08:48-04:00 Fix safe head test. - - - - - a8e2af1a by Simon Génier at 2020-09-10T09:38:07-04:00 Oops: add back running tests in the order they were inserted. - - - - - 02dda30e by Simon Génier at 2020-09-10T10:01:43-04:00 Judge if an expression is positive in a variable. - - - - - 17 changed files: - GNUmakefile - btl/builtins.typer - btl/pervasive.typer - + samples/hott.typer - + shell.nix - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elab.ml - src/env.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - + src/list.ml - src/log.ml - src/opslexp.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6cbc6ee8be6553bde3bd14c471994101a... -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6cbc6ee8be6553bde3bd14c471994101a... You're receiving this email because of your account on gitlab.com.