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
leanprover · Sep 24, 2024 · c3a952a · c3a952a
1 parent 33d9069
commit c3a952a
Show file tree

Hide file tree

Showing 7 changed files with 6 additions and 6 deletions.
diff --git 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
@@ -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 → Tactics/Sym/AxEffects.lean b/Tactics/Reflect/AxEffects.lean → Tactics/Sym/AxEffects.lean
diff --git a/Tactics/SymContext.lean → Tactics/Sym/Context.lean b/Tactics/SymContext.lean → 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 → Tactics/Sym/FetchAndDecode.lean b/Tactics/Reflect/FetchAndDecode.lean → 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 → Tactics/Sym/ProgramInfo.lean b/Tactics/Reflect/ProgramInfo.lean → Tactics/Sym/ProgramInfo.lean
diff --git 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