-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Extend the notion of invalid matches by disallowing matching of local…
…ly non-loose bvars
- Loading branch information
1 parent
c11041d
commit b2d3e98
Showing
6 changed files
with
152 additions
and
77 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,25 +1,43 @@ | ||
| import Egg | ||
|
|
||
| -- We have to disable β-reduction as part of normalization, as otherwise `thm` is useless. | ||
| -- We have to disable β-reduction as part of normalization, as otherwise `thm₁,₂` are useless, and | ||
| -- disable β-reduction in egg, as this interferes with the test cases. | ||
| set_option egg.betaReduceRws false | ||
| set_option egg.genBetaRw false | ||
|
|
||
| theorem thm : ∀ x : Nat, x = (fun _ => x) (nat_lit 0) := | ||
| fun _ => rfl | ||
| -- This theorem is only applicable in the forward direction. | ||
| theorem thm₁ : ∀ x y : Nat, (x, y).fst = (fun _ => x) (nat_lit 1) := | ||
| fun _ _ => rfl | ||
|
|
||
| -- In this example egg finds a proof, but we're not performing proof reconstruction (which would be | ||
| -- impossible) as a result of setting `exitPoint := some .beforeProof`. | ||
| set_option egg.shiftCapturedBVars false in | ||
| example : False := by | ||
| have h : (fun x => x) = (fun y : Nat => (fun x => x) 1) := by | ||
| egg (config := { exitPoint := some .beforeProof }) [thm] | ||
| have h : (fun x => (x, 5).fst) = (fun _ : Nat => (fun x => x) 1) := by | ||
| egg (config := { exitPoint := some .beforeProof }) [thm₁] | ||
| have : (fun x => x) 0 = (fun y => 1) 0 := by rw [h] | ||
| contradiction | ||
|
|
||
| -- BUG: This generates a completely broken e-graph. | ||
| -- For example, a number node becomes equivalent to an application node. | ||
| -- This seems to originate entirely from `replace_loose_bvars` though. | ||
| set_option egg.shiftCapturedBVars true in | ||
| example : True := by | ||
| have h : (fun x => x) = (fun y : Nat => (fun x => x) (nat_lit 1)) := by | ||
| sorry -- egg (config := { traceCapturedBVarShifting := true }) [thm] | ||
| fail_if_success -- This fails because egg could not find a proof. | ||
| have : (fun x => (x, 5).fst) = (fun _ : Nat => (fun x => x) 1) := by egg [thm₁] | ||
| constructor | ||
|
|
||
| theorem thm₂ : ∀ x : Nat, (fun _ => (fun _ => x) x) 0 = x := | ||
| fun _ => rfl | ||
|
|
||
| -- TODO: This seems to cause an infinite loop or at least extremely long runtime in | ||
| -- `shifted_subst_for_pat` or `subst`. I think what is happening is that `thm₂` is applied in | ||
| -- the backward direction over and over again which quickly blows up the e-graph. | ||
| -- Investigate further what's happening by somehow tracing `shifted_subst_for_pat`. | ||
| set_option egg.shiftCapturedBVars true in | ||
| example : True := by | ||
| have : (fun x => (fun a => (fun a => a) a) 0) = (fun x => x) := by sorry -- egg [thm₂] | ||
| constructor | ||
|
|
||
| -- Unrelated to capture avoidance: | ||
| -- | ||
| -- TODO: If we have a theorem like `(fun a b => a) x y = x`, it's only applicable in the forward | ||
| -- direction. But once we β-reduce it, it's applicable in both directions. I think that can | ||
| -- cause problems during reconstruction as we cannot reconstruct the assignment of `y`. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -21,6 +21,7 @@ mod rewrite; | |
| mod subst; | ||
| mod trace; | ||
| mod util; | ||
| mod valid_match; | ||
|
|
||
| #[repr(C)] | ||
| #[derive(PartialEq)] | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,93 @@ | ||
|
|
||
| use std::collections::HashMap; | ||
| use egg::*; | ||
| use crate::lean_expr::*; | ||
| use crate::analysis::*; | ||
|
|
||
| // An expression position is a sequence of coordinates which describe how to traverse nodes | ||
| // starting at a given root node. Each coordinate dictates which child of a node to visit. | ||
| // In an expression tree, each node has a unique position. | ||
| type ExprPos = Vec<usize>; | ||
| // A binder position of `None` indicates that the associated value does not appear under a binder. | ||
| type BinderPos = Option<ExprPos>; | ||
|
|
||
| // The given values are always used together in `match_is_valid_core`, so we given them a type. | ||
| struct Location { | ||
| pos: ExprPos, | ||
| parent_binder: BinderPos, | ||
| binder_depth: u64 | ||
| } | ||
|
|
||
| // Various data required for checking match validity. | ||
| struct Context<'a> { | ||
| pat: &'a PatternAst<LeanExpr>, | ||
| subst: &'a Subst, | ||
| graph: &'a LeanEGraph, | ||
| parent_binders: HashMap<Var, BinderPos> | ||
| } | ||
|
|
||
| // A match (a substitution and pattern) is valid if both: | ||
| // (1) No (non-loose) bound variables are matched. | ||
| // (2) For each variable v in the substitution which maps to an e-class with loose bvars, | ||
| // v only appears under the same binder. | ||
| // | ||
| // Example of invalid matches: | ||
| // (1) Pattern term `(lam _, ?x)` matching against `(lam _, (bvar 0))`. | ||
| // (2) Pattern term `(lam _ (lam _, ?x) ?x)` matching against `(lam _ (lam _, (bvar 2)) (bvar 2))`. | ||
| // | ||
| // The need for Condition (2) should be obvious. Condition (1) on the other hand only follows from | ||
| // the fact that our rewrites come from theorems of the form `forall x, y = z`. Thus, if a pattern | ||
| // variable appears, it can never refer to a (non-loose) bound variable, as `x` cannot refer to any | ||
| // bound variables in `y` or `z`. | ||
| pub fn match_is_valid(subst: &Subst, pat: &PatternAst<LeanExpr>, graph: &LeanEGraph) -> bool { | ||
| let mut ctx = Context { pat, subst, graph, parent_binders: HashMap::new() }; | ||
| let root_idx = pat.as_ref().len() - 1; | ||
| let loc = Location { pos: vec![], parent_binder: None, binder_depth: 0 }; | ||
| match_is_valid_core(root_idx, loc, &mut ctx) | ||
| } | ||
|
|
||
| fn match_is_valid_core(idx: usize, loc: Location, ctx: &mut Context) -> bool { | ||
| match &ctx.pat.as_ref()[idx] { | ||
| ENodeOrVar::Var(var) => { | ||
| let loose_bvars = &ctx.graph[ctx.subst[*var]].data.loose_bvars; | ||
| if loose_bvars.is_empty() { | ||
| // If the given variable does not map to an e-class containing loose bvars, if cannot cause any problems. | ||
| return true | ||
| } else { | ||
| // If the given variable maps to an e-class containing loose bvars, we need to check Conditions (1) and (2). | ||
|
|
||
| // For Condition (1): If the variable maps to an e-class containing bound variables whose indices are | ||
| // exceeded by the current binder depth, then those bound variables must be non-loose in the context | ||
| // of `ctx.pat`, and are not allowed to be matched. | ||
| if loose_bvars.iter().any(|b| *b < loc.binder_depth) { return false } | ||
|
|
||
| if let Some(required_parent) = ctx.parent_binders.get(var) { | ||
| // For Condition (2): If the variable has already occured elsewhere in the pattern, | ||
| // then the parent binder of that occurrence must be the same as the current parent binder. | ||
| return loc.parent_binder == *required_parent | ||
| } else { | ||
| // If the given variable has not been visited yet, record its parent binder. | ||
| ctx.parent_binders.insert(*var, loc.parent_binder); | ||
| return true | ||
| } | ||
| } | ||
| }, | ||
| ENodeOrVar::ENode(e) => { | ||
| for (i, child) in e.children().iter().enumerate() { | ||
| // If `e` is a binder, set the parent binder and increase the binder depth for its body. | ||
| let (parent_binder, binder_depth) = | ||
| if is_binder(&e) && i == 1 { | ||
| (Some(loc.pos.clone()), loc.binder_depth + 1) | ||
| } else { | ||
| (loc.parent_binder.clone(), loc.binder_depth) | ||
| }; | ||
| let mut pos = loc.pos.clone(); pos.push(i); | ||
| let child_loc = Location { pos, parent_binder, binder_depth }; | ||
|
|
||
| let child_idx = usize::from(*child); | ||
| if !match_is_valid_core(child_idx, child_loc, ctx) { return false } | ||
| } | ||
| true | ||
| } | ||
| } | ||
| } |