Stefan pushed to branch master at Stefan / Typer

Commits: 49ca7fdb by Stefan Monnier at 2017-07-18T18:09:10-04:00 Try and document the universe hierarchy

- - - - -

3 changed files:

- doc/manual.texi - src/elab.ml - src/opslexp.ml

Changes:

===================================== doc/manual.texi ===================================== --- a/doc/manual.texi +++ b/doc/manual.texi @@ -6,7 +6,7 @@ @copying .

-Copyright @copyright{} 2012-2016 Free Software Foundation, Inc. +Copyright @copyright{} 2012-2017 Free Software Foundation, Inc.

@quotation Permission is granted to copy, distribute and/or modify this document @@ -195,6 +195,44 @@ type2)}. @c @c Get fdl.texi from http://www.gnu.org/licenses/fdl.html @c @include fdl.texi

+@node Universe Hierarchy +@subsection Universe Hierarchy + +The PTS used in Typer looks as follows: + +@example +S = { SortL, Sortω, Type l } ∀ l : TypeLevel +A = { TypeLevel : SortL, + TypeLevel.z : TypeLevel + TypeLevel.s : TypeLevel → TypeLevel, + TypeLevel.∪ : TypeLevel → TypeLevel → TypeLevel. + Type l : Type (TypeLevel.s l), ∀ l : TypeLevel + } +R = { (SortL, Type l, Sortω), ∀ l : TypeLevel + (SortL, Sortω, Sortω), + (Type l, Sortω, Sortω), ∀ l : TypeLevel + (Type l₁, Type l₂, Type (TypeLevel.∪ l₁ l₂)) ∀ l₁,l₂ : TypeLevel + } +@end example + +@c Another way to look at it is: + +@c @example +@c S = { SortType, Sortω } ∪ { s | s : Sort } +@c A = { Sort : SortType, +@c TypeZ : Sort +@c TypeS : Sort → Sort, +@c Type∪ : Sort → Sort → Sort +@c } +@c R = { (Sort, s, Sortω), +@c (Sort, Sortω, Sortω), +@c (s, Sortω, Sortω), +@c (s₁, s₂, Type∪ s₁ s₂) +@c } +@c @end example +@c But now we have the problem that TypeZ has type Sort but Type0 should +@c have type Type1 so we can't have TypeZ = Type0. + @node Index @unnumbered Index

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -30,6 +30,11 @@ * Elaborate Sexp expression into Lexp. * This includes type inference, and macro expansion. * + * While elaboration will discover most type errors, strictly speaking + * this phase does not need to perform any checks, and it can instead presume + * that the code is well-behaved. The real type checks (and totality + * checks) are performed later in OL.check. + * * -------------------------------------------------------------------------- *)

open Util @@ -493,8 +498,7 @@ and check_inferred ctx e inferred_t t =

(* Lexp.case can sometimes be inferred, but we prefer to always check. *) and check_case rtype (loc, target, ppatterns) ctx = - (* FIXME: check if case is exhaustive *) - (* Helpers *) + (* Helpers *)

let pat_string p = sexp_string (pexp_u_pat p) in

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -508,6 +508,7 @@ let rec check' meta_ctx erased ctx e = let tct = arg_loop args ctx in tct | Case (l, e, ret, branches, default) + (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = match e with | Call (f, args) -> (f, args) | _ -> (e,[]) in

View it on GitLab: https://gitlab.com/monnier/typer/commit/49ca7fdbd3a79287a905e8201cd792f5fc3b...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/49ca7fdbd3a79287a905e8201cd792f5fc3b... You're receiving this email because of your account on gitlab.com.