Skip to content

Commit 22978b4

Browse files
jackh726jackh726
committed
Undo this indent
1 parent 4b8f6bb commit 22978b4

File tree

1 file changed

+74
-74
lines changed

1 file changed

+74
-74
lines changed

‎chalk-engine/src/logic.rs‎

Lines changed: 74 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -1136,93 +1136,93 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
11361136
(AnswerMode::Ambiguous, _) => true,
11371137
}
11381138
};
1139-
// N.B. If we try to pursue a strand and it's found to be ambiguous,
1140-
// we know that isn't part of a cycle.
11411139
if forest.tables[table]
11421140
.strands_mut()
1143-
.any(|s| strand_is_participating(s))
1141+
.all(|s| !strand_is_participating(s))
11441142
{
1145-
let clock = self.stack.top().clock;
1146-
let cyclic_minimums = self.stack.top().cyclic_minimums;
1147-
if cyclic_minimums.positive >= clock && cyclic_minimums.negative >= clock {
1148-
debug!("cycle with no new answers");
1149-
1150-
if cyclic_minimums.negative < TimeStamp::MAX {
1151-
// This is a negative cycle.
1152-
self.unwind_stack();
1153-
return Err(RootSearchFail::NegativeCycle);
1143+
// If no strands are participating, then that means they are all
1144+
// ambiguous and we are in complete mode.
1145+
debug!("All strands would return ambiguous answers.");
1146+
match self.forest.tables[table].answer_mode {
1147+
AnswerMode::Complete => {
1148+
debug!("Allowing ambiguous answers.");
1149+
self.forest.tables[table].answer_mode = AnswerMode::Ambiguous;
1150+
return Err(RootSearchFail::QuantumExceeded);
1151+
}
1152+
AnswerMode::Ambiguous => {
1153+
unreachable!();
11541154
}
1155+
}
1156+
}
11551157

1156-
// If all the things that we recursively depend on have
1157-
// positive dependencies on things below us in the stack,
1158-
// then no more answers are forthcoming. We can clear all
1159-
// the strands for those things recursively.
1160-
let table = self.stack.top().table;
1161-
let cyclic_strands =
1162-
self.forest.tables[table].drain_strands(strand_is_participating);
1163-
self.clear_strands_after_cycle(cyclic_strands);
1158+
let clock = self.stack.top().clock;
1159+
let cyclic_minimums = self.stack.top().cyclic_minimums;
1160+
if cyclic_minimums.positive >= clock && cyclic_minimums.negative >= clock {
1161+
debug!("cycle with no new answers");
11641162

1165-
// Now we yield with `QuantumExceeded`
1163+
if cyclic_minimums.negative < TimeStamp::MAX {
1164+
// This is a negative cycle.
11661165
self.unwind_stack();
1167-
return Err(RootSearchFail::QuantumExceeded);
1168-
} else {
1169-
debug!("table part of a cycle");
1166+
return Err(RootSearchFail::NegativeCycle);
1167+
}
11701168

1171-
// This table resulted in a positive cycle, so we have
1172-
// to check what this means for the subgoal containing
1173-
// this strand
1174-
let caller_strand = match self.stack.pop_and_borrow_caller_strand() {
1175-
Some(s) => s,
1176-
None => {
1177-
panic!("nothing on the stack but cyclic result");
1178-
}
1179-
};
1169+
// If all the things that we recursively depend on have
1170+
// positive dependencies on things below us in the stack,
1171+
// then no more answers are forthcoming. We can clear all
1172+
// the strands for those things recursively.
1173+
let table = self.stack.top().table;
1174+
// N.B. If we try to pursue a strand and it's found to be ambiguous,
1175+
// we know that isn't part of a cycle.
1176+
let cyclic_strands = self.forest.tables[table].drain_strands(strand_is_participating);
1177+
self.clear_strands_after_cycle(cyclic_strands);
11801178

1181-
// We can't take this because we might need it later to clear the cycle
1182-
let caller_selected_subgoal = caller_strand.selected_subgoal.as_ref().unwrap();
1183-
match caller_strand.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] {
1184-
Literal::Positive(_) => {
1185-
self.stack
1186-
.top()
1187-
.cyclic_minimums
1188-
.take_minimums(&cyclic_minimums);
1189-
}
1190-
Literal::Negative(_) => {
1191-
// We depend on `not(subgoal)`. For us to continue,
1192-
// `subgoal` must be completely evaluated. Therefore,
1193-
// we depend (negatively) on the minimum link of
1194-
// `subgoal` as a whole -- it doesn't matter whether
1195-
// it's pos or neg.
1196-
let mins = Minimums {
1197-
positive: self.stack.top().clock,
1198-
negative: cyclic_minimums.minimum_of_pos_and_neg(),
1199-
};
1200-
self.stack.top().cyclic_minimums.take_minimums(&mins);
1201-
}
1202-
}
1179+
// Now we yield with `QuantumExceeded`
1180+
self.unwind_stack();
1181+
return Err(RootSearchFail::QuantumExceeded);
1182+
} else {
1183+
debug!("table part of a cycle");
12031184

1204-
// We can't pursue this strand anymore, so push it back onto the table
1205-
let active_strand = self.stack.top().active_strand.take().unwrap();
1206-
let table = self.stack.top().table;
1207-
let canonical_active_strand =
1208-
Forest::canonicalize_strand(self.context, active_strand);
1209-
self.forest.tables[table].enqueue_strand(canonical_active_strand);
1185+
// This table resulted in a positive cycle, so we have
1186+
// to check what this means for the subgoal containing
1187+
// this strand
1188+
let caller_strand = match self.stack.pop_and_borrow_caller_strand() {
1189+
Some(s) => s,
1190+
None => {
1191+
panic!("nothing on the stack but cyclic result");
1192+
}
1193+
};
12101194

1211-
// The strand isn't active, but the table is, so just continue
1212-
return Ok(());
1195+
// We can't take this because we might need it later to clear the cycle
1196+
let caller_selected_subgoal = caller_strand.selected_subgoal.as_ref().unwrap();
1197+
match caller_strand.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] {
1198+
Literal::Positive(_) => {
1199+
self.stack
1200+
.top()
1201+
.cyclic_minimums
1202+
.take_minimums(&cyclic_minimums);
1203+
}
1204+
Literal::Negative(_) => {
1205+
// We depend on `not(subgoal)`. For us to continue,
1206+
// `subgoal` must be completely evaluated. Therefore,
1207+
// we depend (negatively) on the minimum link of
1208+
// `subgoal` as a whole -- it doesn't matter whether
1209+
// it's pos or neg.
1210+
let mins = Minimums {
1211+
positive: self.stack.top().clock,
1212+
negative: cyclic_minimums.minimum_of_pos_and_neg(),
1213+
};
1214+
self.stack.top().cyclic_minimums.take_minimums(&mins);
1215+
}
12131216
}
1214-
}
12151217

1216-
debug!("All strands would return ambiguous answers.");
1217-
match self.forest.tables[table].answer_mode {
1218-
AnswerMode::Complete => {
1219-
debug!("Allowing ambiguous answers.");
1220-
self.forest.tables[table].answer_mode = AnswerMode::Ambiguous;
1221-
return Err(RootSearchFail::QuantumExceeded);
1222-
}
1223-
AnswerMode::Ambiguous => {
1224-
panic!();
1225-
}
1218+
// We can't pursue this strand anymore, so push it back onto the table
1219+
let active_strand = self.stack.top().active_strand.take().unwrap();
1220+
let table = self.stack.top().table;
1221+
let canonical_active_strand = Forest::canonicalize_strand(self.context, active_strand);
1222+
self.forest.tables[table].enqueue_strand(canonical_active_strand);
1223+
1224+
// The strand isn't active, but the table is, so just continue
1225+
return Ok(());
12261226
}
12271227
}
12281228

0 commit comments

Comments
 (0)