Stefan pushed to branch master at Stefan / Typer
Commits: 7868f806 by Stefan Monnier at 2016-11-19T10:39:30-05:00 * src/opslexp.ml (check): Fix minor issues with hierarchy checks.
- - - - -
1 changed file:
- src/opslexp.ml
Changes:
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -276,15 +276,19 @@ let rec check meta_ctx ctx e = | Imm (Epsilon | Block (_, _, _) | Symbol _ | Node (_, _)) -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; B.type_int) - | SortLevel (_) -> B.type_level - | Sort (l, Stype (SortLevel l1 as sl1)) - -> Sort (l, Stype (SortLevel (SLsucc sl1))) - | Sort (_, (StypeOmega|StypeLevel)) + | SortLevel SLz -> B.type_level + | SortLevel (SLsucc e) + -> let t = check ctx e in + assert_type ctx e t B.type_level; + B.type_level + | Sort (l, Stype e) + -> let t = check ctx e in + assert_type ctx e t B.type_level; + Sort (l, Stype (SortLevel (SLsucc t))) + | Sort (_, StypeLevel) -> B.type_omega + | Sort (_, StypeOmega) -> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sorts!"; B.type_omega) - | Sort (_, (Stype _)) - -> (U.msg_error "TC" (lexp_location e) "Non-level arg to Type!"; - B.type_omega) | Builtin (_, t) -> t (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v
View it on GitLab: https://gitlab.com/monnier/typer/commit/7868f806ead4941d35ada06e4c618ef99a08...
Afficher les réponses par date