Merge pull request #141 from opencompl/scf-for-fusion

Scf for fusion
opencompl · Jan 22, 2024 · 5311207 · 5311207
2 parents a1d8513 + d703e6b
commit 5311207
Show file tree

Hide file tree

Showing 3 changed files with 235 additions and 152 deletions.
diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean
@@ -250,6 +250,16 @@ theorem Valuation.snoc_toSnoc {Γ : Ctxt Ty} {t t' : Ty} (s : Γ.Valuation) (x :
     (v : Γ.Var t') : (s.snoc x) v.toSnoc = s v := by
   simp [Ctxt.Valuation.snoc]
 
+/-!
+# Helper to simplify context manipulation with toSnoc and variable access.
+-/
+/--  (ctx.snoc v₁) ⟨n+1, _⟩ = ctx ⟨n, _⟩ -/
+@[simp]
+theorem Valuation.snoc_eval {ty : Ty} (Γ : Ctxt Ty) (V : Γ.Valuation) (v : ⟦ty⟧)
+    (hvar : Ctxt.get? (Ctxt.snoc Γ ty) (n+1) = some var_val) :
+    (V.snoc v) ⟨n+1, hvar⟩ = V ⟨n, by simp [Ctxt.get?,Ctxt.snoc] at hvar; exact hvar⟩ :=
+  rfl
+
 /-- Make a a valuation for a singleton value -/
 def Valuation.singleton {t : Ty} (v : toType t) : Ctxt.Valuation [t] :=
   Ctxt.Valuation.nil.snoc v

diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean
@@ -1244,16 +1244,17 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident :
         Ctxt.DerivedCtxt.ofCtxt_empty, Ctxt.Valuation.snoc_last,
         Com.denote, Expr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc,
         Ctxt.empty, Ctxt.empty_eq, Ctxt.snoc, Ctxt.Valuation.nil, Ctxt.Valuation.snoc_last,
-        Ctxt.ofList, Ctxt.Valuation.snoc_toSnoc,
+        Ctxt.Valuation.snoc_eval, Ctxt.ofList, Ctxt.Valuation.snoc_toSnoc,
         HVector.map, HVector.toPair, HVector.toTuple, OpDenote.denote, Expr.op_mk, Expr.args_mk,
         DialectMorphism.mapOp, DialectMorphism.mapTy, List.map, Ctxt.snoc, List.map,
+        Function.comp, Ctxt.Valuation.ofPair, Ctxt.Valuation.ofHVector, Function.uncurry,
         $ts,*]
-      generalize $ll { val := 0, property := _ } = a;
-      generalize $ll { val := 1, property := _ } = b;
-      generalize $ll { val := 2, property := _ } = c;
-      generalize $ll { val := 3, property := _ } = d;
-      generalize $ll { val := 4, property := _ } = e;
-      generalize $ll { val := 5, property := _ } = f;
+      try generalize $ll { val := 0, property := _ } = a;
+      try generalize $ll { val := 1, property := _ } = b;
+      try generalize $ll { val := 2, property := _ } = c;
+      try generalize $ll { val := 3, property := _ } = d;
+      try generalize $ll { val := 4, property := _ } = e;
+      try generalize $ll { val := 5, property := _ } = f;
       try simp (config := {decide := false}) [Goedel.toType] at a b c d e f;
       try clear f;
       try clear e;