Skip to content

Commit 6c44f05

Browse files
SaltyPeppermintSaltyPeppermint
committed
removed broken test
1 parent 0042f23 commit 6c44f05

3 files changed

Lines changed: 33 additions & 35 deletions

File tree

‎src/rewrite_system/rise/func.rs‎

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -325,15 +325,3 @@ fn vec_ty(expr: &RecExpr<Rise>, n: i32, id: Id) -> Option<RecExpr<Rise>> {
325325
// case ArrayType(_, _) => None
326326
// }
327327
// }
328-
329-
#[cfg(test)]
330-
mod tests {
331-
use super::*;
332-
333-
#[test]
334-
fn pat_rule_1() {
335-
pat(
336-
"(typeOf (app (typeOf (app (typeOf map (fun (fun ?dt0 ?dt0) (fun (arrT ?n0 ?dt0) (arrT ?n0 ?dt0)))) (typeOf (lam (typeOf %0 ?dt1)) (fun ?dt0 ?dt0))) (fun (arrT ?n0 ?dt0) (arrT ?n0 ?dt0))) (typeOf ?e0 (arrT ?n0 ?dt0))) (arrT ?n0 ?dt0))",
337-
);
338-
}
339-
}

‎src/rewrite_system/rise/rules.rs‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ pub fn mm_rules() -> Vec<Rewrite<Rise, RiseAnalysis>> {
4141
// rewrite!("map-par"; "(typeOf map (fun (fun ?dt0 ?dt1) (fun (arrT ?n0 ?dt0) (arrT ?n0 ?dt1))))" => { pat("(typeOf mapPar (fun (fun ?dt0 ?dt1) (fun (arrT ?n0 ?dt0) (arrT ?n0 ?dt1))))") }),
4242
];
4343
algorithmic.extend([
44-
// OLD: rewrite!("eta-reduction"; "(typeOf (lam (typeOf (app (typeOf ?0 ?tAny0) (typeOf %0 ?t0)) ?tAny1)) (fun ?t1 ?t2))" => { NotFreeIn::new("?0", 0, Shifted::new("?0", "?1", -1, 1, ShiftedCheck::new("?t1", "?t0", 1, 0, pat("(typeOf ?1 (fun ?t1 ?t2))")))) }),
44+
// OLD: rewrite!("eta-reduction"; "(typeOf (lam (typeOf (app (typeOf ?0 ?tAny0) (typeOf %e0 ?t0)) ?tAny1)) (fun ?t1 ?t2))" => { NotFreeIn::new("?0", 0, Shifted::new("?0", "?1", -1, 1, ShiftedCheck::new("?t1", "?t0", 1, 0, pat("(typeOf ?1 (fun ?t1 ?t2))")))) }),
4545
// OLD: rewrite!("beta"; "(app (lam ?body) ?e)" => { BetaExtractApplier::new("?body", "?e") }),
4646
// rewrite!("beta"; "(app (typeOf (lam (typeOf ?body ?bodyTy)) ?lamTy) (typeOf ?subs ?subsTy))" => { BetaExtractApplier::new("?body", "?subs", Kind::Expr) }),
4747
// rewrite!("beta-nat"; "(natApp (typeOf (natLam (typeOf ?body ?bodyTy)) ?lamTy) (typeOf ?subs ?subsTy))" => { BetaExtractApplier::new("?body", "?subs",Kind::Nat) }),
@@ -192,22 +192,22 @@ mod tests {
192192
}
193193
// (λ. (λ. ((λ. (0 1)) (0 1)))) --> (λ. (λ. ((0 1) 0)))
194194
// (λ. (0 1)) (0 1) --> (0 1) 0
195-
check("(app %0 %1)", "(app %0 %1)", "(app (app %0 %1) %0)");
196-
// r1 = (app (lam (app "%6" (app "%5" "%0"))) "%0")
197-
// r2 = (app (lam (app "%6" r1)) "%0")
198-
// r3 = (app (lam (app "%6" r2)) %0)
199-
// (app map (lam (app "%6" r3)))
200-
// --> (app map (lam (app "%6" (app "%5" (app "%4" (app "%3" (app "%2" "%0")))))))
201-
check("(app %6 (app %5 %0))", "%0", "(app %5 (app %4 %0))");
195+
check("(app %e0 %e1)", "(app %e0 %e1)", "(app (app %e0 %e1) %e0)");
196+
// r1 = (app (lam (app "%e6" (app "%e5" "%e0"))) "%e0")
197+
// r2 = (app (lam (app "%e6" r1)) "%e0")
198+
// r3 = (app (lam (app "%e6" r2)) %e0)
199+
// (app map (lam (app "%e6" r3)))
200+
// --> (app map (lam (app "%e6" (app "%e5" (app "%e4" (app "%e3" (app "%e2" "%e0")))))))
201+
check("(app %e6 (app %e5 %e0))", "%e0", "(app %e5 (app %e4 %e0))");
202202
check(
203-
"(app %6 (app %5 (app %4 %0)))",
204-
"%0",
205-
"(app %5 (app %4 (app %3 %0)))",
203+
"(app %e6 (app %e5 (app %e4 %e0)))",
204+
"%e0",
205+
"(app %e5 (app %e4 (app %e3 %e0)))",
206206
);
207207
check(
208-
"(app %6 (app %5 (app %4 (app %3 %0))))",
209-
"%0",
210-
"(app %5 (app %4 (app %3 (app %2 %0))))",
208+
"(app %e6 (app %e5 (app %e4 (app %e3 %e0))))",
209+
"%e0",
210+
"(app %e5 (app %e4 (app %e3 (app %e2 %e0))))",
211211
);
212212
}
213213

‎src/rewrite_system/rise/shifted.rs‎

Lines changed: 19 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -209,24 +209,34 @@ mod tests {
209209
);
210210
assert_eq!(&shifted, b);
211211
}
212-
check("(app %0 %1)", "(app %1 %2)", 0, 1);
213-
check("(typeOf (app %0 %1) f32)", "(typeOf (app %1 %2) f32)", 0, 1);
214-
check("(typeOf (app %0 %1) f32)", "(typeOf (app %0 %2) f32)", 1, 1);
212+
check("(app %e0 %e1)", "(app %e1 %e2)", 0, 1);
215213
check(
216-
"(typeOf (lam (typeOf (app %0 %2) f32)) f32)",
217-
"(typeOf (lam (typeOf (app %0 %3) f32)) f32)",
214+
"(typeOf (app %e0 %e1) f32)",
215+
"(typeOf (app %e1 %e2) f32)",
216+
0,
217+
1,
218+
);
219+
check(
220+
"(typeOf (app %e0 %e1) f32)",
221+
"(typeOf (app %e0 %e2) f32)",
222+
1,
223+
1,
224+
);
225+
check(
226+
"(typeOf (lam (typeOf (app %e0 %e2) f32)) f32)",
227+
"(typeOf (lam (typeOf (app %e0 %e3) f32)) f32)",
218228
1,
219229
1,
220230
);
221231
check(
222-
"(typeOf (lam (typeOf (app %0 %2) f32)) f32)",
223-
"(typeOf (lam (typeOf (app %0 %1) f32)) f32)",
232+
"(typeOf (lam (typeOf (app %e0 %e2) f32)) f32)",
233+
"(typeOf (lam (typeOf (app %e0 %e1) f32)) f32)",
224234
1,
225235
-1,
226236
);
227237
check(
228-
"(lam (typeOf (app (typeOf (app (typeOf mul (fun f32 (fun f32 f32))) (typeOf (app (typeOf fst (fun (pairT f32 f32) f32)) (typeOf %3 (pairT f32 f32))) f32)) (fun f32 f32)) (typeOf (app (typeOf snd (fun (pairT f32 f32) f32)) (typeOf %3 (pairT f32 f32))) f32)) f32))",
229-
"(lam (typeOf (app (typeOf (app (typeOf mul (fun f32 (fun f32 f32))) (typeOf (app (typeOf fst (fun (pairT f32 f32) f32)) (typeOf %5 (pairT f32 f32))) f32)) (fun f32 f32)) (typeOf (app (typeOf snd (fun (pairT f32 f32) f32)) (typeOf %5 (pairT f32 f32))) f32)) f32))",
238+
"(lam (typeOf (app (typeOf (app (typeOf mul (fun f32 (fun f32 f32))) (typeOf (app (typeOf fst (fun (pairT f32 f32) f32)) (typeOf %e3 (pairT f32 f32))) f32)) (fun f32 f32)) (typeOf (app (typeOf snd (fun (pairT f32 f32) f32)) (typeOf %e3 (pairT f32 f32))) f32)) f32))",
239+
"(lam (typeOf (app (typeOf (app (typeOf mul (fun f32 (fun f32 f32))) (typeOf (app (typeOf fst (fun (pairT f32 f32) f32)) (typeOf %e5 (pairT f32 f32))) f32)) (fun f32 f32)) (typeOf (app (typeOf snd (fun (pairT f32 f32) f32)) (typeOf %e5 (pairT f32 f32))) f32)) f32))",
230240
0,
231241
2,
232242
);

0 commit comments

Comments
 (0)