feat: allow runAnalysis with custom Output

Author: insightmind

LeanInk/Analysis/Basic.lean

@@ -1,6 +1,7 @@
 import LeanInk.Configuration
 import LeanInk.FileHelper
-import LeanInk.Annotation
+import LeanInk.Annotation.DataTypes
+import LeanInk.Annotation.Alectryon
 import LeanInk.Logger
 import LeanInk.CLI
 
@@ -10,6 +11,7 @@ import Lean.Util.Path
 
 namespace LeanInk.Analysis
 
+open LeanInk.Annotation
 open LeanInk.CLI
 open Lean
 open System
@@ -21,7 +23,6 @@ private def _buildConfiguration (arguments: List ResolvedArgument) (file: FilePa
   return { 
     inputFilePath := file
     inputFileContents := contents
-    outputType := OutputType.alectryonFragments
     lakeFile := getLakeFile? arguments
     verbose := containsFlag arguments "--verbose"
     experimentalTypeInfo := containsFlag arguments "--x-enable-type-info"
@@ -34,24 +35,31 @@ where
     | none => none
     | some string => some (FilePath.mk string)
 
-def runAnalysis : AnalysisM UInt32 := do
+def runAnalysis (output : Output) : AnalysisM UInt32 := do
   let config ← read
   logInfo s!"Starting process with lean file: {config.inputFileName}"
   logInfo "Analyzing..."
   let result ← analyzeInput config
   logInfo "Annotating..."
   let annotation ← Annotation.annotateFile result
   logInfo "Outputting..."
-  return ← Annotation.Alectryon.genOutput annotation
+  return ← output.genOutput annotation
 
 -- EXECUTION
+def execAuxM : AnalysisM UInt32 := do
+  return ← runAnalysis { 
+    name := "Alectryon"
+    genOutput := Alectryon.genOutput
+  } 
+
 def execAux (args: List ResolvedArgument) (file: String) : IO UInt32 := do
   if not (_validateInputFile file) then do
     Logger.logError s!"Provided file \"{file}\" is not lean file."
   else
     IO.println s!"Starting Analysis for: \"{file}\""
     let config ← _buildConfiguration args file
-    return ← (runAnalysis.run config)
+    return ← (execAuxM.run config)
+    
 
 def exec (args: List ResolvedArgument) : List String -> IO UInt32
   | [] => do Logger.logError s!"No input files provided"

LeanInk/Analysis/DataTypes.lean

@@ -1,5 +1,4 @@
 import LeanInk.ListUtil
-import LeanInk.Configuration
 
 import Lean.Elab
 import Lean.Data.Lsp

LeanInk/Analysis/SemanticToken.lean

@@ -1,4 +1,5 @@
 import LeanInk.Analysis.DataTypes
+import LeanInk.Configuration
 import LeanInk.ListUtil
 
 import Lean.Elab

LeanInk/Annotation/Basic.lean

@@ -3,6 +3,7 @@ import LeanInk.ListUtil
 import LeanInk.Logger
 
 import LeanInk.Annotation.Util
+import LeanInk.Annotation.DataTypes
 
 import LeanInk.Analysis.DataTypes
 import LeanInk.Analysis.Analysis
@@ -14,10 +15,6 @@ open LeanInk.Analysis
 /-
   Annotation
 -/
-structure Annotation where
-  sentence : Compound Sentence
-  tokens : List (Compound Token)
-
 def tokensBetween (aux : List (Compound Token)) (head : String.Pos) (tail : Option String.Pos) : List (Compound Token) -> List (Compound Token)
   | [] => aux
   | x::xs =>

LeanInk/Annotation/DataTypes.lean

@@ -0,0 +1,28 @@
+import LeanInk.Analysis.DataTypes
+
+namespace LeanInk.Annotation
+
+open LeanInk.Analysis
+
+universe u
+
+/- COMPOUND -/
+structure Compound (β : Type u) where
+  headPos : String.Pos
+  fragments : List (Nat × β)
+  deriving Inhabited
+
+structure Annotation where
+  sentence : Compound Sentence
+  tokens : List (Compound Token)
+
+namespace Compound
+  def getFragments (self : Compound b) : List b := self.fragments.map (λ f => f.2)
+
+  def tailPos { x : Type u } [Positional x] (self : Compound x) : Option String.Pos := (self.getFragments.map (λ f => Positional.tailPos f)).maximum?
+
+  def empty { x : Type u } (headPos : String.Pos) : Compound x := { headPos := headPos, fragments := [] }
+end Compound
+
+instance {a : Type u} [ToString a] : ToString (Compound a) where
+  toString (self : Compound a) : String := "<COMPOUND head:" ++ toString self.headPos ++ " fragments := " ++ toString self.getFragments ++ ">"

LeanInk/Annotation/Util.lean

@@ -2,30 +2,12 @@ import LeanInk.Configuration
 import LeanInk.Logger
 
 import LeanInk.Analysis.Analysis
+import LeanInk.Analysis.DataTypes
 
 namespace LeanInk.Annotation
 
 open LeanInk.Analysis
 
-universe u
-
-/- COMPOUND -/
-structure Compound (β : Type u) where
-  headPos : String.Pos
-  fragments : List (Nat × β)
-  deriving Inhabited
-
-namespace Compound
-  def getFragments (self : Compound b) : List b := self.fragments.map (λ f => f.2)
-
-  def tailPos { x : Type u } [Positional x] (self : Compound x) : Option String.Pos := (self.getFragments.map (λ f => Positional.tailPos f)).maximum?
-
-  def empty { x : Type u } (headPos : String.Pos) : Compound x := { headPos := headPos, fragments := [] }
-end Compound
-
-instance {a : Type u} [ToString a] : ToString (Compound a) where
-  toString (self : Compound a) : String := "<COMPOUND head:" ++ toString self.headPos ++ " fragments := " ++ toString self.getFragments ++ ">"
-
 /- FRAGMENT INTERVAL -/
 inductive FragmentInterval (a : Type u) where
   | head (pos: String.Pos) (fragment: a) (idx: Nat)

LeanInk/Configuration.lean

@@ -1,31 +1,28 @@
+import LeanInk.Annotation.DataTypes
+
 namespace LeanInk
 
 open System
+open LeanInk.Annotation
 
--- The `OutputType` specifies in which format the result of
--- leanInks analysis gets returned.
-inductive OutputType where
-  -- alectryonFragments describes the format used by Alectryon which basically is a list
-  -- of fragments. Each fragment is either a `Text` or `Sentence`. TODO: specify further
-  | alectryonFragments : OutputType 
-
--- The analyze `Configuration` describes all input specifications and infos for
--- the LeanInk analysis execution context. It contains the list of input file paths, etc.
 structure Configuration where
   inputFilePath : FilePath
   inputFileContents : String
-  outputType : OutputType
   lakeFile : Option FilePath
   verbose : Bool
   experimentalTypeInfo : Bool
   experimentalDocString : Bool
   experimentalSemanticType : Bool
 
 namespace Configuration
+  def inputFileName (self : Configuration) : String :=
+    self.inputFilePath.toString
+end Configuration
 
-def inputFileName (self : Configuration) : String :=
-  self.inputFilePath.toString
+abbrev AnalysisM := ReaderT Configuration $ IO
 
-end Configuration
+structure Output where
+  name : String
+  genOutput : List Annotation -> AnalysisM UInt32
 
-abbrev AnalysisM := ReaderT Configuration $ IO
+abbrev ExecM := ReaderT Configuration $ IO