From c3a952a020cfe1763f94e193e28e9f3a83846c30 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 24 Sep 2024 15:13:23 -0500
Subject: [PATCH] refactor: rename `Reflect` folder to `Sym`, move `SymContext`
 to `Sym/Context`

The new name makes more sense, since this is where I've been storing various components of the `sym_n` tactic implementation, even if they're not really doing reflection
---
 Tactics/StepThms.lean                         | 2 +-
 Tactics/Sym.lean                              | 2 +-
 Tactics/{Reflect => Sym}/AxEffects.lean       | 0
 Tactics/{SymContext.lean => Sym/Context.lean} | 4 ++--
 Tactics/{Reflect => Sym}/FetchAndDecode.lean  | 2 +-
 Tactics/{Reflect => Sym}/ProgramInfo.lean     | 0
 Tests/Tactics/ReduceFetchInst.lean            | 2 +-
 7 files changed, 6 insertions(+), 6 deletions(-)
 rename Tactics/{Reflect => Sym}/AxEffects.lean (100%)
 rename Tactics/{SymContext.lean => Sym/Context.lean} (99%)
 rename Tactics/{Reflect => Sym}/FetchAndDecode.lean (98%)
 rename Tactics/{Reflect => Sym}/ProgramInfo.lean (100%)

diff --git a/Tactics/StepThms.lean b/Tactics/StepThms.lean
index af788dd2..53dd2e56 100644
--- a/Tactics/StepThms.lean
+++ b/Tactics/StepThms.lean
@@ -8,7 +8,7 @@ import Arm.Map
 import Arm.Decode
 import Tactics.Common
 import Tactics.Simp
-import Tactics.Reflect.ProgramInfo
+import Tactics.Sym.ProgramInfo
 
 open Lean Lean.Expr Lean.Meta Lean.Elab Lean.Elab.Command
 open SymContext (h_pc_type h_program_type h_err_type)
diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
index 8cff86e3..1f44168f 100644
--- a/Tactics/Sym.lean
+++ b/Tactics/Sym.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel, Alex Keizer
 import Arm.Exec
 import Arm.Memory.MemoryProofs
 import Tactics.FetchAndDecode
-import Tactics.SymContext
+import Tactics.Sym.Context
 
 import Lean
 
diff --git a/Tactics/Reflect/AxEffects.lean b/Tactics/Sym/AxEffects.lean
similarity index 100%
rename from Tactics/Reflect/AxEffects.lean
rename to Tactics/Sym/AxEffects.lean
diff --git a/Tactics/SymContext.lean b/Tactics/Sym/Context.lean
similarity index 99%
rename from Tactics/SymContext.lean
rename to Tactics/Sym/Context.lean
index bba913f6..e80aab08 100644
--- a/Tactics/SymContext.lean
+++ b/Tactics/Sym/Context.lean
@@ -9,8 +9,8 @@ import Lean.Meta
 import Arm.Exec
 import Tactics.Common
 import Tactics.Attr
-import Tactics.Reflect.ProgramInfo
-import Tactics.Reflect.AxEffects
+import Tactics.Sym.ProgramInfo
+import Tactics.Sym.AxEffects
 import Tactics.Simp
 
 /-!
diff --git a/Tactics/Reflect/FetchAndDecode.lean b/Tactics/Sym/FetchAndDecode.lean
similarity index 98%
rename from Tactics/Reflect/FetchAndDecode.lean
rename to Tactics/Sym/FetchAndDecode.lean
index c9583f20..d584648b 100644
--- a/Tactics/Reflect/FetchAndDecode.lean
+++ b/Tactics/Sym/FetchAndDecode.lean
@@ -5,7 +5,7 @@ Author(s): Alex Keizer
 -/
 import Arm.State
 import Tactics.Common
-import Tactics.Reflect.ProgramInfo
+import Tactics.Sym.ProgramInfo
 
 open Lean Meta
 open Elab.Tactic Elab.Term
diff --git a/Tactics/Reflect/ProgramInfo.lean b/Tactics/Sym/ProgramInfo.lean
similarity index 100%
rename from Tactics/Reflect/ProgramInfo.lean
rename to Tactics/Sym/ProgramInfo.lean
diff --git a/Tests/Tactics/ReduceFetchInst.lean b/Tests/Tactics/ReduceFetchInst.lean
index 630bcbbc..7ff5ae13 100644
--- a/Tests/Tactics/ReduceFetchInst.lean
+++ b/Tests/Tactics/ReduceFetchInst.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Alex Keizer
 -/
-import Tactics.Reflect.FetchAndDecode
+import Tactics.Sym.FetchAndDecode
 import Tests.«AES-GCM».GCMGmultV8Program
 import Tests.SHA2.SHA512Program