|
1 | 1 | use std::iter::zip;
|
2 | 2 |
|
3 | 3 | use formality_core::{judgment_fn, Fallible, Map, Upcast};
|
4 |
| -use formality_prove::{prove_normalize, Constraints, Decls, Env}; |
5 |
| -use formality_core::{Fallible, Map, Upcast}; |
6 |
| -use formality_prove::{AdtDeclBoundData, AdtDeclVariant, Env}; |
| 4 | +use formality_prove::{prove_normalize, AdtDeclBoundData, AdtDeclVariant, Constraints, Decls, Env}; |
7 | 5 | use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
|
8 | 6 | use formality_rust::grammar::minirust::PlaceExpression::*;
|
9 | 7 | use formality_rust::grammar::minirust::ValueExpression::{Constant, Fn, Load, Struct};
|
10 | 8 | use formality_rust::grammar::minirust::{
|
11 | 9 | self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression,
|
12 | 10 | };
|
13 | 11 | use formality_rust::grammar::FnBoundData;
|
14 |
| -use formality_types::grammar::{CrateId, FnId}; |
15 |
| -use formality_types::grammar::{Relation, Ty, VariantId, Wcs}; |
| 12 | +use formality_types::grammar::{ |
| 13 | + CrateId, FnId, Parameter, Relation, RigidName, RigidTy, Ty, VariantId, Wcs, |
| 14 | +}; |
16 | 15 |
|
17 | 16 | use crate::{Check, CrateItem};
|
18 | 17 | use anyhow::bail;
|
@@ -494,3 +493,34 @@ struct TypeckEnv {
|
494 | 493 | /// LocalId of function argument.
|
495 | 494 | fn_args: Vec<LocalId>,
|
496 | 495 | }
|
| 496 | + |
| 497 | +judgment_fn! { |
| 498 | + fn ty_is_int( |
| 499 | + _decls: Decls, |
| 500 | + env: Env, |
| 501 | + assumptions: Wcs, |
| 502 | + ty: Parameter, |
| 503 | + ) => Constraints { |
| 504 | + debug(assumptions, ty, env) |
| 505 | + // If the type that we are currently checking is rigid, check if it is an int. |
| 506 | + // If the type can be normalized, normalize until rigid then check if it is an int. |
| 507 | + // For the rest of the case, it should fail. |
| 508 | + |
| 509 | + ( |
| 510 | + (prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))! |
| 511 | + (let assumptions = c1.substitution().apply(&assumptions)) |
| 512 | + (ty_is_int(&decl, &env, assumptions, p) => c2) |
| 513 | + ----------------------------- ("alias_ty is int") |
| 514 | + (ty_is_int(decl, env, assumptions, ty) => c2) |
| 515 | + ) |
| 516 | + |
| 517 | + ( |
| 518 | + (if id.is_int()) |
| 519 | + ----------------------------- ("rigid_ty is int") |
| 520 | + (ty_is_int(_decls, _env, _assumptions, RigidTy {name: RigidName::ScalarId(id), parameters: _}) => Constraints::none(env)) |
| 521 | + ) |
| 522 | + |
| 523 | + } |
| 524 | +} |
| 525 | + |
| 526 | +mod test; |
0 commit comments