Typer Mai 2024

typer@iro.umontreal.ca

3 participants
2 discussions

[Git][monnier/typer][main] 4 commits: Move internal representations to a separate module, named Ir.
by Stefan (＠monnier) 28 Mai '24

28 Mai '24

Stefan pushed to branch main at Stefan / Typer Commits: 4919a2ab by Maxim Bernard at 2024-05-18T16:48:18-04:00 Move internal representations to a separate module, named Ir. Import Ir in all relevant modules, and remove unneeded imports. Move all datatypes representing context (lexp_context, elab_context, typeclass_context, runtime_env) and code (sexp, lexp, elexp, value) and their related types to the same mutually-recursive block. Rename `set` to `db_set` for clarity. Rename `value_type` to simply `value` for consistency with the naming convention used in the rest of the project. Rename all `elexp` constructors by prefixing them with an "E", to avoid clashes with `lexp`. Change `Imm` constructor so it contains a `sinfo * value` pair instead of an `sexp`. Similar change to `Eimm`. * src/sexp.ml : Replace `Sym.t` with `symbol` for clarity, and remove `t` for the same reason. Replace certain `sexp`s in function types to `token` when appropriate. Replace certain `sexp`s in function types to `token` when appropriate. * src/lexp.ml : `lexp_head` can't return the exact Imm name for now; can be fixed later (needs further refactoring). Remove unsued `pred_imm`. * src/inverse_subst.ml: Improve code clarity. * src/elab.ml (elab_macro_call) : Replace `token` with `sexp` in argument type for clarity. - - - - - 7fc20e58 by Maxim Bernard at 2024-05-21T01:57:01-04:00 Move all pretty-printing functions to the same module. * src/fmt.ml: Move printing functions from all over the project to here. Define them all in the same mutually recursive block (required to print `Imm` values). Polymorphic functions in that block require explicit type variables, otherwise OCaml attempts to assign them a non polymorphic type. Fix bug in `pp_print_lexp` (formerly `Lexp.pp_print`) in `Inductive` branch where a formatting block was opened without being closed. * src/ir.ml: Move `pretoken` from Prelexer to here. Re-arrange type definitions to minimise recursive definitions. Replace uses of `Source.Location.t` with `location` for clarity. * src/pexp.ml: Remove obsolete ArgKind module, since functions have been moved to Fmt. * src/util.ml: Move `maybename` from Lexp to here (required by Fmt). - - - - - 7b0ff399 by Maxim Bernard at 2024-05-22T01:54:10-04:00 Improve message formatting thoughout the project. Print log messages using pretty-printing functions when available and the Format module instead of string conversions, which allow for appropriate indentation to be generated. Perform a `clean` on all lexps prior to printing them, for performance reasons (otherwise, all memory would be consumed). * src/fmt.ml: Reactivate printing lexps in substitutions (since they can now be printed safely, see above). * src/lexp.ml: Define functions to be used elsewhere in the project when printing lexps. * src/log.ml: Change type of `log_msg` to allow for `%a` conversion specifications in format strings. * src/opslexp.ml: Cleanup dead code and re-organize module imports for cleanness. - - - - - 2e478c82 by Maxim Bernard at 2024-05-22T17:24:07-04:00 Rearrange definitions in Ir. * src/ir.ml: Reduce size of mutually recursive `type` block to a minimum, by extracting types that don't need to be there. Transfer a couple of definitions from Util for consistency. * src/util.ml: Transfer several definitions from here to Ir. - - - - - 30 changed files: - src/REPL.ml - src/backend.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/instargs.ml - src/inverse_subst.ml - + src/ir.ml - src/lexer.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/pexp.ml - src/positivity.ml - src/prelexer.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/env_test.ml - tests/eval_test.ml - tests/instargs_test.ml - tests/lexer_test.ml - tests/macro_test.ml - tests/positivity_test.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/476b8241874c55883ab2ee370813646c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/476b8241874c55883ab2ee370813646c… You're receiving this email because of your account on gitlab.com.

1 0

Types quotient et égalité définitionnelle
by Stefan Monnier 02 Mai '24

02 Mai '24

Salut James, T'avais raison de rester avec une égalité propositionnelle pour tes types quotient: renforcer l'égalité définitionnelle pour les types quotients pose des problèmes. Soit le type quotient A/F où A est le type de base et F est une fonction qui prend un argument de type A et renvoie la classe d'équivalence à laquel il appartient. Soit une élimination comme: Qrec: ?A/?F → (f : ?A → ?t) → (P : ∀ x,y . ?F x = ?F y → f x = f y) → ?t; qui dit que tu peux appliquer `f` au "contenu" d'un quotient ?A/?F pour autant que tu prouves avec `P` que `f` traite tous les éléments d'une même classe de la même manière. Le problème est que l'élimination ne garanti que l'égalité propositionnelle du résultat. Donc si tu permets à deux valeurs différentes de type A/F d'être définitionnellement égales, t'as un problème, parce que tu casses le principe que e₁ ≃ e₂ => E[e₁] ≃ E[e₂] Plus concrètement, disons que le constructeur des quotients est Qin, si tu as e₁ ≄ e₂ ∧ Qin e₁ ≃ Qin e₂ tu peux montrer que E[Qin e₁] = E[Qin e₂] parce que ton `Qrec` te donne cette `=` (i.e. égalité propositionnelle), mais tu ne peux pas montrer que cette égalité est vraie définitionnellement (`≃`), et en effet elle n'est pas vraie définitionnellement si le `f` de l'éliminateur est la fonction identité (qui est un cas possible si le contexte nous fournit la preuve `P`). Donc à moins de faire attention que `Qrec` renvoie toujours une valeur "normalisée", on perd la propriété de "subject reduction". 🙁 Étonnement, je n'ai encore pas vu une telle explication dans mes lectures. Toi? Stefan

2 1

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Mai 2024