completed FP types

leanprover · Sep 13, 2024 · 5d66573 · 5d66573
1 parent f37a1f5
commit 5d66573
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 4 deletions.
diff --git a/SHerLOC/AST1.lean b/SHerLOC/AST1.lean
@@ -177,6 +177,8 @@ structure IntegerType where
   deriving Repr, Inhabited, Nonempty
 
 inductive FloatType where
+  | f8E3M4
+  | f8E4M3
   | f8E4M3FN
   | f8E5M2
   | f8E4M3FNUZ
@@ -273,7 +275,6 @@ mutual
     | func (literal : FuncId)
     | list (literal : List Literal)
     | dictionary (literal : List Attribute)
-    | use_global_device_ids
     | array (literal : ArrayLiteral)
 
     deriving Repr, Inhabited, Nonempty

diff --git a/SHerLOC/Parsing/Intermediate.lean b/SHerLOC/Parsing/Intermediate.lean
@@ -62,10 +62,9 @@ mutual
 
   partial def parseAttribute : PState Attribute := do
     push "parseAttribute"
-    if ← isParse "use_global_device_ids" then -- Review
+    if ← isParse "use_global_device_ids" then
       pop "parseAttribute"
-      throw <| ← error "use_global_device_ids"
-      -- return -- Attribute.mk "use_global_device_ids" { literal := Literal.use_global_device_ids, typ := none }}
+      return Attribute.mk "use_global_device_ids" <| Constant.mk (Literal.element (ElementLiteral.booleanLiteral BooleanLiteral.true)) none
     else
       let id ← parseId
       parseItem "="

diff --git a/SHerLOC/Parsing/Types.lean b/SHerLOC/Parsing/Types.lean
@@ -41,9 +41,11 @@ def tryParseFloatType : PState (Option FloatType) := do
     if ← isParse "f16" then r := some FloatType.f16
     if ← isParse "f32" then r := some FloatType.f32
     if ← isParse "f64" then r := some FloatType.f64
+    if ← isParse "f8E3M4" then r := some FloatType.f8E3M4
     if ← isParse "f8E4M3B11FNUZ" then r := some FloatType.f8E4M3B11FNUZ
     if ← isParse "f8E4M3FNUZ" then r := some FloatType.f8E4M3FNUZ
     if ← isParse "f8E4M3FN" then r := some FloatType.f8E4M3FN
+    if ← isParse "f8E4M3" then r := some FloatType.f8E4M3
     if ← isParse "f8E5M2FNUZ" then r := some FloatType.f8E5M2FNUZ
     if ← isParse "f8E5M2" then r := some FloatType.f8E5M2
   }