Add 'dot' opcode (#18)

leanprover · Oct 9, 2024 · 038c38c · 038c38c
1 parent c7a3706
commit 038c38c
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1 @@
+/.lake/
diff --git a/SHerLOC/AST1.lean b/SHerLOC/AST1.lean
@@ -326,6 +326,7 @@ inductive OpCode where
 | countLeadingZeros
 | customCall
 | divide
+| dot
 | dotGeneral
 | dynamicBroadcastInDim
 | dynamicConv

diff --git a/SHerLOC/Parsing/Operations.lean b/SHerLOC/Parsing/Operations.lean
@@ -80,6 +80,7 @@ def parseOpCode : PState OpCode := do
   | "count_leading_zeros" => opCode := some OpCode.countLeadingZeros
   | "custom_call" => opCode := some OpCode.customCall
   | "divide" => opCode := some OpCode.divide
+  | "dot" => opCode := some OpCode.dot
   | "dot_general" => opCode := some OpCode.dotGeneral
   | "dynamic_broadcast_in_dim" => opCode := some OpCode.dynamicBroadcastInDim
   | "dynamic_conv" => opCode := some OpCode.dynamicConv
@@ -244,6 +245,7 @@ partial def parseStableHLO (opOutputs : List ValueId) : PState Operation := do
   | OpCode.countLeadingZeros => parseOperationBasic OpCode.countLeadingZeros opOutputs
   | OpCode.customCall => parseOperationBasic OpCode.customCall opOutputs
   | OpCode.divide => parseOperationBasic OpCode.divide opOutputs
+  | OpCode.dot => parseOperationBasic OpCode.dot opOutputs
   | OpCode.dotGeneral => parseOperationBasic OpCode.dotGeneral opOutputs
   | OpCode.dynamicBroadcastInDim => parseOperationBasic OpCode.dynamicBroadcastInDim opOutputs
   | OpCode.dynamicConv => parseOperationBasic OpCode.dynamicConv opOutputs