Typer

Download

typer@iro.umontreal.ca

February 2019

1 participants
2 discussions

[Git][monnier/typer][report/tcvi] Fix typos
by Nathaniel 20 Feb '19

20 Feb '19

Nathaniel pushed to branch report/tcvi at Stefan / Typer Commits: f58dee26 by nbos at 2019-02-20T20:24:18Z Fix typos - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -152,7 +152,7 @@ Université de Montréal - DIRO \\ \email{monnier(a)iro.umontreal.ca} \and - McGill University - SCS \\ + McGill University - SOCS \\ \email{nathaniel.bos(a)mail.mcgill.ca} } @@ -690,7 +690,7 @@ as well. \Jcic e \tau} {\Jcic{\Con{i}{e}}{\Subst{a_i}{x}{e}}} - \Infer{\forall i. \\ \Jtype {\tau_1} {\kw{Prop}}} + \Infer{\forall i. \\ \Jtype {\tau} {\tau_i} \\ \Jtype {\tau_i} {\kw{Prop}}} {\Jsmall {\vec \tau}} %% Actual typing rules View it on GitLab: https://gitlab.com/monnier/typer/commit/f58dee2620b7bb806e7fa8cadee3d978436… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/f58dee2620b7bb806e7fa8cadee3d978436… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/opslexp.ml (check'', get_type): Fix context confusion
by Stefan 16 Feb '19

16 Feb '19

Stefan pushed to branch master at Stefan / Typer Commits: 8061a7de by Stefan Monnier at 2019-02-16T15:15:19Z * src/opslexp.ml (check'', get_type): Fix context confusion When computing the level of an inductive type, we need to distinguish the current context of the current field and the external context in which the result is valid. - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps -Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2019 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -527,14 +527,16 @@ let rec check'' erased ctx e = (fun _ case level -> let (level, _, _, _) = List.fold_left - (fun (level, ctx, erased, n) (ak, v, t) -> - ((match lexp_whnf (check_type erased ctx t) - ctx with + (fun (level, ictx, erased, n) (ak, v, t) -> + ((match lexp_whnf (check_type erased ictx t) + ictx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') -> mkSLlub ctx level + (* FIXME: We shouldn't use Inverse_subst + * in the plain `check` code! *) (Inverse_subst.apply_inv_subst level' (S.shift n)) | tt -> U.msg_error "TC" (lexp_location t) @@ -542,10 +544,10 @@ let rec check'' erased ctx e = ^ lexp_string t ^ " is not a Type! (" ^ lexp_string tt ^")"); - DB.print_lexp_ctx ctx; + DB.print_lexp_ctx ictx; (* U.internal_error "Oops"; *) level), - DB.lctx_extend ctx v Variable t, + DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, n + 1)) (level, ctx, erased, 0) @@ -826,8 +828,8 @@ let rec get_type ctx e = (fun _ case level -> let (level, _, _) = List.fold_left - (fun (level, ctx, n) (ak, v, t) -> - ((match lexp_whnf (get_type ctx t) ctx with + (fun (level, ictx, n) (ak, v, t) -> + ((match lexp_whnf (get_type ictx t) ictx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -837,7 +839,7 @@ let rec get_type ctx e = (S.shift n) with _ -> level) | tt -> level), - DB.lctx_extend ctx v Variable t, + DB.lctx_extend ictx v Variable t, n + 1)) (level, ctx, 0) case in View it on GitLab: https://gitlab.com/monnier/typer/commit/8061a7de3449e4e867d523787c415755e35… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/8061a7de3449e4e867d523787c415755e35… You're receiving this email because of your account on gitlab.com.

1 0