Skip to content

Commit e2dbf1b

Browse files
NoamDevNoamDev
committed
Fixed the type validation
1 parent a8c2471 commit e2dbf1b

File tree

1 file changed

+103
-210
lines changed

1 file changed

+103
-210
lines changed

‎src/par/types/definitions.rs‎

Lines changed: 103 additions & 210 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
use crate::location::Span;
22
use crate::par::language::{GlobalName, LocalName};
3-
use crate::par::types::{Type, TypeError};
3+
use crate::par::types::{visit, Type, TypeError};
44
use indexmap::{IndexMap, IndexSet};
55
use std::sync::Arc;
66

@@ -150,231 +150,124 @@ impl TypeDefs {
150150
}
151151

152152
pub fn validate_type(&self, typ: &Type) -> Result<(), TypeError> {
153-
self.validate_type_inner(
154-
typ,
155-
&IndexSet::new(),
156-
&IndexSet::new(),
157-
&IndexSet::new(),
158-
&IndexSet::new(),
159-
true,
160-
)
161-
}
162-
163-
fn validate_type_inner(
164-
&self,
165-
typ: &Type,
166-
self_pos: &IndexSet<Option<LocalName>>,
167-
self_neg: &IndexSet<Option<LocalName>>,
168-
unguarded_self_rec: &IndexSet<Option<LocalName>>,
169-
unguarded_self_iter: &IndexSet<Option<LocalName>>,
170-
check_self: bool,
171-
) -> Result<(), TypeError> {
172-
Ok(match typ {
173-
Type::Primitive(_, _) | Type::DualPrimitive(_, _) => (),
174-
175-
Type::Var(span, name) | Type::DualVar(span, name) => {
176-
if self.vars.contains(name) {
177-
()
178-
} else {
179-
return Err(TypeError::TypeVariableNotDefined(
180-
span.clone(),
181-
name.clone(),
182-
));
153+
#[derive(Clone)]
154+
struct Ctx {
155+
defs: TypeDefs,
156+
check_self: bool,
157+
self_polarity: IndexMap<Option<LocalName>, bool>,
158+
unguarded_self_rec: IndexSet<Option<LocalName>>,
159+
unguarded_self_iter: IndexSet<Option<LocalName>>,
160+
}
161+
fn inner(typ: &Type, positive: bool, mut ctx: Ctx) -> Result<(), TypeError> {
162+
match typ {
163+
Type::Name(_span, _name, args) | Type::DualName(_span, _name, args) => {
164+
for arg in args {
165+
inner(
166+
arg,
167+
positive,
168+
Ctx {
169+
defs: ctx.defs.clone(),
170+
check_self: false,
171+
self_polarity: IndexMap::new(),
172+
unguarded_self_rec: IndexSet::new(),
173+
unguarded_self_iter: IndexSet::new(),
174+
},
175+
)?;
176+
}
177+
visit::continue_deref_polarized(typ, positive, &ctx.defs, |typ, positive| {
178+
inner(typ, positive, ctx.clone())
179+
})?;
183180
}
184-
}
185-
Type::Name(span, name, args) => {
186-
// Dereference alias first so guarding/position checks happen in the body
187-
let t = self.get(span, name, args)?;
188-
self.validate_type_inner(
189-
&t,
190-
self_pos,
191-
self_neg,
192-
unguarded_self_rec,
193-
unguarded_self_iter,
194-
check_self,
195-
)?;
196-
// Separately validate arguments for existence/kind issues without self-guard checks
197-
for arg in args {
198-
self.validate_type_inner(
199-
arg,
200-
&IndexSet::new(),
201-
&IndexSet::new(),
202-
&IndexSet::new(),
203-
&IndexSet::new(),
204-
false,
205-
)?;
181+
Type::Exists(_span, name, _body) | Type::Forall(_span, name, _body) => {
182+
ctx.defs.vars.insert(name.clone());
183+
visit::continue_deref_polarized(typ, positive, &ctx.defs, |typ, positive| {
184+
inner(typ, positive, ctx.clone())
185+
})?;
206186
}
207-
}
208-
Type::DualName(span, name, args) => {
209-
// Dereference alias first so guarding/position checks happen in the body (with polarity swapped)
210-
let t = self.get(span, name, args)?;
211-
self.validate_type_inner(
212-
&t,
213-
self_neg,
214-
self_pos,
215-
unguarded_self_rec,
216-
unguarded_self_iter,
217-
check_self,
218-
)?;
219-
// Separately validate arguments for existence/kind issues without self-guard checks
220-
for arg in args {
221-
self.validate_type_inner(
222-
arg,
223-
&IndexSet::new(),
224-
&IndexSet::new(),
225-
&IndexSet::new(),
226-
&IndexSet::new(),
227-
false,
228-
)?;
187+
Type::Var(span, name) | Type::DualVar(span, name) => {
188+
if ctx.defs.vars.contains(name) {
189+
()
190+
} else {
191+
return Err(TypeError::TypeVariableNotDefined(
192+
span.clone(),
193+
name.clone(),
194+
));
195+
}
229196
}
230-
}
231-
232-
Type::Box(_, body) => self.validate_type_inner(
233-
body,
234-
self_pos,
235-
self_neg,
236-
unguarded_self_rec,
237-
unguarded_self_iter,
238-
check_self,
239-
)?,
240-
Type::DualBox(_, body) => self.validate_type_inner(
241-
body,
242-
self_neg,
243-
self_pos,
244-
unguarded_self_rec,
245-
unguarded_self_iter,
246-
check_self,
247-
)?,
248-
249-
Type::Pair(_, t, u) => {
250-
self.validate_type_inner(
251-
t,
252-
self_pos,
253-
self_neg,
254-
unguarded_self_rec,
255-
unguarded_self_iter,
256-
check_self,
257-
)?;
258-
self.validate_type_inner(
259-
u,
260-
self_pos,
261-
self_neg,
262-
unguarded_self_rec,
263-
unguarded_self_iter,
264-
check_self,
265-
)?;
266-
}
267-
Type::Function(_, t, u) => {
268-
self.validate_type_inner(
269-
t,
270-
self_neg,
271-
self_pos,
272-
unguarded_self_rec,
273-
unguarded_self_iter,
274-
check_self,
275-
)?;
276-
self.validate_type_inner(
277-
u,
278-
self_pos,
279-
self_neg,
280-
unguarded_self_rec,
281-
unguarded_self_iter,
282-
check_self,
283-
)?;
284-
}
285-
Type::Either(_, branches) => {
286-
let unguarded_self_rec = IndexSet::new();
287-
for (_, t) in branches {
288-
self.validate_type_inner(
289-
t,
290-
self_pos,
291-
self_neg,
292-
&unguarded_self_rec,
293-
unguarded_self_iter,
294-
check_self,
295-
)?;
197+
Type::Recursive { label, .. } if ctx.check_self => {
198+
ctx.unguarded_self_rec.insert(label.clone());
199+
ctx.unguarded_self_iter.shift_remove(label);
200+
ctx.self_polarity.insert(label.clone(), positive);
201+
visit::continue_deref_polarized(typ, positive, &ctx.defs, |typ, positive| {
202+
inner(typ, positive, ctx.clone())
203+
})?;
296204
}
297-
}
298-
Type::Choice(_, branches) => {
299-
let unguarded_self_iter = IndexSet::new();
300-
for (_, t) in branches {
301-
self.validate_type_inner(
302-
t,
303-
self_pos,
304-
self_neg,
305-
unguarded_self_rec,
306-
&unguarded_self_iter,
307-
check_self,
308-
)?;
205+
Type::Iterative { label, .. } if ctx.check_self => {
206+
ctx.unguarded_self_iter.insert(label.clone());
207+
ctx.unguarded_self_rec.shift_remove(label);
208+
ctx.self_polarity.insert(label.clone(), positive);
209+
visit::continue_deref_polarized(typ, positive, &ctx.defs, |typ, positive| {
210+
inner(typ, positive, ctx.clone())
211+
})?;
309212
}
310-
}
311-
Type::Break(_) | Type::Continue(_) => (),
312-
313-
Type::Recursive { label, body, .. } | Type::Iterative { label, body, .. } => {
314-
let (mut self_pos, mut self_neg) = (self_pos.clone(), self_neg.clone());
315-
self_pos.insert(label.clone());
316-
self_neg.shift_remove(label);
317-
let (mut unguarded_self_rec, mut unguarded_self_iter) =
318-
(unguarded_self_rec.clone(), unguarded_self_iter.clone());
319-
match typ {
320-
Type::Recursive { .. } => {
321-
unguarded_self_rec.insert(label.clone());
322-
unguarded_self_iter.shift_remove(label);
323-
}
324-
Type::Iterative { .. } => {
325-
unguarded_self_iter.insert(label.clone());
326-
unguarded_self_rec.shift_remove(label);
327-
}
328-
_ => unreachable!(),
213+
Type::Either(..) if ctx.check_self => {
214+
ctx.unguarded_self_rec = IndexSet::new();
215+
visit::continue_deref_polarized(typ, positive, &ctx.defs, |typ, positive| {
216+
inner(typ, positive, ctx.clone())
217+
})?;
329218
}
330-
self.validate_type_inner(
331-
body,
332-
&self_pos,
333-
&self_neg,
334-
&unguarded_self_rec,
335-
&unguarded_self_iter,
336-
check_self,
337-
)?;
338-
}
339-
Type::Self_(span, label) => {
340-
if check_self {
341-
if self_neg.contains(label) {
342-
return Err(TypeError::SelfUsedInNegativePosition(span.clone()));
343-
}
344-
if !self_pos.contains(label) {
219+
Type::Choice(..) if ctx.check_self => {
220+
ctx.unguarded_self_iter = IndexSet::new();
221+
visit::continue_deref_polarized(typ, positive, &ctx.defs, |typ, positive| {
222+
inner(typ, positive, ctx.clone())
223+
})?;
224+
}
225+
Type::Self_(span, label) if ctx.check_self => {
226+
if let Some(is_positive) = ctx.self_polarity.get(label) {
227+
if *is_positive != positive {
228+
return Err(TypeError::SelfUsedInNegativePosition(span.clone()));
229+
}
230+
} else {
345231
return Err(TypeError::NoMatchingRecursiveOrIterative(span.clone()));
346232
}
347-
if unguarded_self_rec.contains(label) {
233+
if ctx.unguarded_self_rec.contains(label) {
348234
return Err(TypeError::UnguardedRecursiveSelf(span.clone()));
349235
}
350-
if unguarded_self_iter.contains(label) {
236+
if ctx.unguarded_self_iter.contains(label) {
351237
return Err(TypeError::UnguardedIterativeSelf(span.clone()));
352238
}
353239
}
354-
}
355-
Type::DualSelf(span, label) => {
356-
if check_self {
357-
if self_pos.contains(label) {
358-
return Err(TypeError::SelfUsedInNegativePosition(span.clone()));
359-
}
360-
if !self_neg.contains(label) {
240+
Type::DualSelf(span, label) if ctx.check_self => {
241+
if let Some(is_positive) = ctx.self_polarity.get(label) {
242+
if *is_positive == positive {
243+
return Err(TypeError::SelfUsedInNegativePosition(span.clone()));
244+
}
245+
} else {
361246
return Err(TypeError::NoMatchingRecursiveOrIterative(span.clone()));
362247
}
248+
if ctx.unguarded_self_rec.contains(label) {
249+
return Err(TypeError::UnguardedRecursiveSelf(span.clone()));
250+
}
251+
if ctx.unguarded_self_iter.contains(label) {
252+
return Err(TypeError::UnguardedIterativeSelf(span.clone()));
253+
}
363254
}
255+
_ => visit::continue_deref_polarized(typ, positive, &ctx.defs, |typ, positive| {
256+
inner(typ, positive, ctx.clone())
257+
})?,
364258
}
365-
366-
Type::Exists(_, name, body) | Type::Forall(_, name, body) => {
367-
let mut with_var = self.clone();
368-
with_var.vars.insert(name.clone());
369-
with_var.validate_type_inner(
370-
body,
371-
self_pos,
372-
self_neg,
373-
unguarded_self_rec,
374-
unguarded_self_iter,
375-
check_self,
376-
)?;
377-
}
378-
})
259+
Ok(())
260+
}
261+
inner(
262+
typ,
263+
true,
264+
Ctx {
265+
defs: self.clone(),
266+
check_self: true,
267+
self_polarity: IndexMap::new(),
268+
unguarded_self_rec: IndexSet::new(),
269+
unguarded_self_iter: IndexSet::new(),
270+
},
271+
)
379272
}
380273
}

0 commit comments

Comments
 (0)