New test files (#8)

.github/workflows/ci.yml

@@ -13,4 +13,6 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
-      - uses: leanprover/lean-action@v1
+      - uses: leanprover/lean-action@v1
+      - name: Run tests
+        run: lake exe sherloc

Main.lean

@@ -5,13 +5,49 @@ Authors: Jean-Baptiste Tristan
 -/
 import SHerLOC
 
-open List System IO FS FilePath
+open System IO FilePath Process FS Std
 
-def main (args : List String) : IO Unit := do
-  if args.length != 1 then
-    IO.println "Expected 1 argument"
-    IO.Process.exit 1
-  let file : FilePath := args[0]!
-  let content ← readFile file
-  let content := StableHLO.parse content.data
-  IO.println s!"{repr content}"
+def main (args : List String) : IO UInt32 := do
+  if args.length = 0 then
+    let o ← output { cmd := "ls", args := #["Tests"] }
+    let files := o.stdout.splitOn "\n"
+    let files := files.filter fun s => s.takeRight 5 = ".mlir"
+    let mut passed := []
+    let mut failed := []
+    for file in files do
+      let fp : FilePath := System.mkFilePath ["Tests", file]
+      let content ← readFile fp
+      let content := StableHLO.parse content.data
+      match content with
+      | .ok _ =>
+        passed := file :: passed
+      | .error _ =>
+        failed := file :: failed
+    IO.println "\nPassed:\n"
+    for file in passed do
+      IO.println file
+    IO.println "\nFailed:\n"
+    for file in failed do
+      IO.println file
+    IO.println ""
+    if failed.length > 0 then
+      return 1
+    else
+      return 0
+  else if args.length = 1 then
+    if let some _ := args[0]!.toNat? then
+      let file : String := "test" ++ args[0]! ++ ".mlir"
+      let fp : FilePath := System.mkFilePath ["Tests", file]
+      let content ← readFile fp
+      let content := StableHLO.parse content.data
+      match content with
+      | .ok p =>
+        IO.println s!"{repr p}"
+        return 0
+      | .error e =>
+        IO.println s!"{e.2.2}"
+        IO.println s!"{e.2.1}"
+        IO.println s!"{e.1}"
+        return 1
+    else panic! s!"Unexpected argument {args[0]!}, expected natural number"
+  else panic! s!"Unexpected number of arguments: {args.length}"

SHerLOC/AST/Basic.lean

@@ -9,4 +9,5 @@ import SHerLOC.AST.Identifiers
 import SHerLOC.AST.Constants
 import SHerLOC.AST.Operations
 import SHerLOC.AST.Functions
+import SHerLOC.AST.Modules
 import SHerLOC.AST.Programs

SHerLOC/AST/Functions.lean

@@ -14,10 +14,15 @@ import SHerLOC.AST.Operations
 
 namespace StableHLO
 
+structure FuncOutput where
+  typ : ValueType
+  attrs : List Attribute
+  deriving Repr, Inhabited, Nonempty
+
 structure Function where
   funcId : FuncId
   funcInputs : List FuncInput
-  funcOutputs : List ValueType
+  funcOutputs : List FuncOutput
   funcBody : List Operation
   deriving Repr, Inhabited, Nonempty
 

SHerLOC/AST/Modules.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jean-Baptiste Tristan
+-/
+import SHerLOC.AST.Functions
+
+/-!
+# Modules
+
+-/
+
+namespace StableHLO
+
+structure Module where
+  modId : FuncId
+  modAttrs : List Attribute
+  modFuncs : List Function
+  deriving Repr, Inhabited, Nonempty
+
+end StableHLO

SHerLOC/AST/Operations.lean

@@ -130,6 +130,7 @@ inductive OpName where
 structure FuncInput where
   id : FuncId
   typ : ValueType
+  attrs : List Attribute
   deriving Repr, Inhabited, Nonempty
 
 mutual
@@ -151,6 +152,9 @@ mutual
     | return
       (operands : List ValueId)
       (signature : FunctionType)
+    | constant
+      (outputs : List ValueId)
+      (value : Constant)
     deriving Repr, Inhabited, Nonempty
 
 end

SHerLOC/AST/Programs.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.
 Authors: Jean-Baptiste Tristan
 -/
-import SHerLOC.AST.Functions
+import SHerLOC.AST.Modules
 
 /-!
 # Programs
@@ -12,7 +12,7 @@ import SHerLOC.AST.Functions
 
 namespace StableHLO
 
-def Program := List Function
+def Program := Module
   deriving Repr, Inhabited, Nonempty
 
 end StableHLO

SHerLOC/AST/Types.lean

@@ -55,9 +55,9 @@ inductive ValueType where
   | tupleType (elements : List ValueType)
   deriving Repr, Inhabited, Nonempty
 
-structure FunctionType where
-  --domain : List ValueType
-  range : ValueType
+inductive FunctionType where
+  | short (range : List ValueType)
+  | long (domain range : List ValueType)
   deriving Repr, Inhabited, Nonempty
 
 inductive NonValueType where