Typer Janvier 2021

typer@iro.umontreal.ca

4 participants
5 discussions

Définitions mutuelles
by Génier Simon 28 Jan '21

28 Jan '21

Bonjour, J'ai un petit problème avec les définitions mutuelles et je me demandais si quelqu'un avait une idée. Le programme suivant est rejeté. type Nat | zero | succ (pred : Nat) ; even : Nat -> Bool; odd : Nat -> Bool; even n = case n | zero => true | succ p => odd p ; odd n = case n | zero => false | succ p => even p ; L'erreur est la suivante. [X] Fatal :(DEBRUIJN) Unexpected lexp_context shape! Ça vient de lctx_view qui ne gère que le cas où l'index est 1, et j'imagine que pour de telles définitions récursives, on a 2 par exemple. J'aimerais bien le déboguer moi-même, mais je suis embêté parce que je n'ai aucune idée de ce que fait lctx_view. Simon

1 0

Decidable comme type classe
by Stefan Monnier 21 Jan '21

21 Jan '21

D'après https://arxiv.org/abs/2003.01685, il semble qu'en Lean aussi, `Decidable` est défini comme une type classe. Ça vaudrait la peine de jeter un coup d'œil pour voir exactement comment ils l'utilisent. Stefan

2 1

Logique intuitionniste et les lois de la physique
by Archambault-Bouffard Vincent 11 Jan '21

11 Jan '21

Et vlan dans les dents « principe du tiers exclu » https://www.quantamagazine.org/does-time-really-flow-new-clues-come-from-a-…

2 1

[Git][monnier/typer] Deleted branch ja/various_fixes
by Jean-Alexandre Barszcz 04 Jan '21

04 Jan '21

Jean-Alexandre Barszcz deleted branch ja/various_fixes at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 4 commits: * src/opslexp.ml (clean_decls): Oops, make it check for metavars.
by Jean-Alexandre Barszcz 04 Jan '21

04 Jan '21

Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer Commits: 8741ee4f by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/opslexp.ml (clean_decls): Oops, make it check for metavars. - - - - - 14d0ad7a by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/elab.ml (sform_letin): Remove unnecessary scope_level bump. - - - - - 1c6e109b by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/elab.ml (sform_letin): Make `let` bidirectional. - - - - - fecec539 by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/opslexp.ml (fv): Check that the memoized value is still ok. - - - - - 2 changed files: - src/elab.ml - src/opslexp.ml Changes: ===================================== src/elab.ml ===================================== @@ -1690,11 +1690,16 @@ let rec sform_case ctx loc sargs ot = match sargs with let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in - (* FIXME: Use `elaborate`. *) - let bdy, ltp = infer sbody (ectx_new_scope nctx) in - let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in - (lexp_let_decls declss bdy nctx, - Inferred (mkSusp ltp s)) + let s, off = + List.fold_left (fun (s, off) decls -> + (OL.lexp_defs_subst loc s decls, off + List.length decls)) + (S.identity, 0) declss in + let ot = U.option_map (fun t -> mkSusp t (S.shift off)) ot in + let bdy, ot = elaborate nctx sbody ot in + let ot = match ot with + | Inferred t -> Inferred (mkSusp t s) + | _ -> ot in + (lexp_let_decls declss bdy nctx, ot) | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc ===================================== src/opslexp.ml ===================================== @@ -975,11 +975,22 @@ and fv (e : lexp) : (DB.set * mv_set) = -> let (fvs, mvs) = fv_erase (fv (push_susp t s)) in (fvs, mv_set_add mvs id (sl, t, cl, name))) in - (* FIXME: Flush the memoization table whenever the metavar table - * is modified, since that can affect the output of `fv`. *) - try LMap.find fv_memo e - with Not_found - -> let r = fv' e in + let ofvs = LMap.find_opt fv_memo e in + (* The memoized value depends on the metavariable table. When it + changes, we have to recompute the free variables. Instead of + flushing the table after every instantiation, we check that no + free metavars are actually instantiated. For this to work, we + assume that the table changes monotonously: metavariables can be + instantiated, but the instantiations cannot be undone. *) + match ofvs with + | Some ((_, (mvfs, _)) as fvs) + when IMap.for_all + (fun mv _ -> match metavar_lookup mv with + | MVar _ -> true + | MVal _ -> false) + mvfs + -> fvs + | _ -> let r = fv' e in LMap.add fv_memo e r; r @@ -1173,6 +1184,9 @@ and clean_map cases = (l, args, erase_type (L.push_susp expr subst)) in SMap.map clean_branch cases +(* The following entry points to erasure, `erase_type` and + `clean_decls`, check that no metavariables are left before + performing the erasure itself. *) let erase_type lxp = let _, (mvs, _) = fv lxp in if not (IMap.is_empty mvs) then @@ -1186,6 +1200,11 @@ let erase_type lxp = ("Metavariables in erase_type :"); erase_type lxp +(* Textually identical to the previous definition of `clean_decls`, + but calls the new `erase_type`, which checks for metavars. *) +let clean_decls decls = + List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls + (** Turning a set of declarations into an object. **) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/5335bac82a595ba73df6a49837bbc033… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/5335bac82a595ba73df6a49837bbc033… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Janvier 2021