Move Veir data types to Veir/Data (#227)

This follows Lean's repository layout and implements @luisacicolini's
suggestion in #178.

Author: tobiasgrosser

Veir.lean

@@ -1,4 +1,4 @@
-import Veir.Dialects
+import Veir.Data
 
 import Veir.IR.Basic
 import Veir.IR.Fields

Veir/Data.lean

@@ -0,0 +1,3 @@
+module
+
+import Veir.Data.LLVM

Veir/Data/LLVM.lean

@@ -0,0 +1,4 @@
+module
+
+public import Veir.Data.LLVM.Int
+public import Veir.Data.LLVM.Byte

Veir/Data/LLVM/Byte.lean

@@ -0,0 +1,5 @@
+module
+
+public import Veir.Data.LLVM.Byte.Basic
+public import Veir.Data.LLVM.Byte.Lemmas
+public import Veir.Data.LLVM.Byte.Examples

Veir/Dialects/LLVM/Byte/Basic.lean Veir/Data/LLVM/Byte/Basic.leanVeir/Dialects/LLVM/Byte/Basic.lean renamed to Veir/Data/LLVM/Byte/Basic.lean

@@ -1,8 +1,8 @@
 module
 
-public import Veir.Dialects.LLVM.Int.Basic
+public import Veir.Data.LLVM.Int.Basic
 
-namespace Veir.Dialects.LLVM
+namespace Veir.Data.LLVM
 
 namespace Byte
 

Veir/Dialects/LLVM/Byte/Examples.lean Veir/Data/LLVM/Byte/Examples.leanVeir/Dialects/LLVM/Byte/Examples.lean renamed to Veir/Data/LLVM/Byte/Examples.lean

@@ -1,11 +1,11 @@
 module
 
 import Std.Tactic.BVDecide
-import Veir.Dialects.LLVM.Byte.Basic
-import all Veir.Dialects.LLVM.Byte.Lemmas
+import Veir.Data.LLVM.Byte.Basic
+import all Veir.Data.LLVM.Byte.Lemmas
 
 
-namespace Veir.Dialects.LLVM.Byte
+namespace Veir.Data.LLVM.Byte
 
 example (w : Nat) (x y : Byte w) : x ||| y = y ||| x := by
   simp only [or_eq]
@@ -14,4 +14,4 @@ example (w : Nat) (x y : Byte w) : x ||| y = y ||| x := by
 example (x y : Byte 8) : x ||| y = y ||| x := by
   bv_decide
 
-end Veir.Dialects.LLVM.Byte
+end Veir.Data.LLVM.Byte

Veir/Dialects/LLVM/Byte/Lemmas.lean Veir/Data/LLVM/Byte/Lemmas.leanVeir/Dialects/LLVM/Byte/Lemmas.lean renamed to Veir/Data/LLVM/Byte/Lemmas.lean

@@ -1,10 +1,10 @@
 module
 
-import all Veir.Dialects.LLVM.Byte.Basic
+import all Veir.Data.LLVM.Byte.Basic
 
-namespace Veir.Dialects.LLVM.Byte
+namespace Veir.Data.LLVM.Byte
 
-open Veir.Dialects.LLVM.Int
+open Veir.Data.LLVM.Int
 
 theorem toInt_fromInt {w : Nat} (x : Int w) (h : 0 < w) : (Byte.fromInt x).toInt = x := by
   simp only [Byte.toInt, fromInt]
@@ -74,4 +74,4 @@ theorem val_xor {w : Nat} (x y : Byte w) :
     (x ^^^ y).val = (x.val ^^^ y.val) &&& ~~~(x.poison ||| y.poison) := by
   simp [xor_eq]
 
-end Veir.Dialects.LLVM.Byte
+end Veir.Data.LLVM.Byte

Veir/Data/LLVM/Int.lean

@@ -0,0 +1,4 @@
+module
+
+public import Veir.Data.LLVM.Int.Basic
+public import Veir.Data.LLVM.Int.Lemmas

Veir/Dialects/LLVM/Int/Basic.lean Veir/Data/LLVM/Int/Basic.leanVeir/Dialects/LLVM/Int/Basic.lean renamed to Veir/Data/LLVM/Int/Basic.lean

@@ -1,6 +1,6 @@
 module
 
-namespace Veir.Dialects.LLVM
+namespace Veir.Data.LLVM
 
 public section
 
@@ -42,4 +42,4 @@ def cast {w₁ w₂ : Nat} (x : Int w₁) (h : w₁ = w₂) : Int w₂ :=
 
 end Int
 end
-end Veir.Dialects.LLVM
+end Veir.Data.LLVM

Veir/Dialects/LLVM/Int/Lemmas.lean Veir/Data/LLVM/Int/Lemmas.leanVeir/Dialects/LLVM/Int/Lemmas.lean renamed to Veir/Data/LLVM/Int/Lemmas.lean

@@ -1,10 +1,10 @@
 module
 
-import all Veir.Dialects.LLVM.Int.Basic
+import all Veir.Data.LLVM.Int.Basic
 
-open Veir.Dialects.LLVM
+open Veir.Data.LLVM
 
-namespace Veir.Dialects.LLVM.Int
+namespace Veir.Data.LLVM.Int
 
 /- # add -/