From 8471b6061c72c3c4c8967b20d4ed755d391117e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Niklas=20Bu=CC=88low?= Date: Wed, 9 Feb 2022 01:32:29 +0100 Subject: [PATCH] feat: allow runAnalysis with custom Output --- LeanInk/Analysis/Basic.lean | 18 +++++++++++++----- LeanInk/Analysis/DataTypes.lean | 1 - LeanInk/Analysis/SemanticToken.lean | 1 + LeanInk/Annotation/Basic.lean | 5 +---- LeanInk/Annotation/DataTypes.lean | 28 ++++++++++++++++++++++++++++ LeanInk/Annotation/Util.lean | 20 +------------------- LeanInk/Configuration.lean | 25 +++++++++++-------------- 7 files changed, 55 insertions(+), 43 deletions(-) create mode 100644 LeanInk/Annotation/DataTypes.lean diff --git a/LeanInk/Analysis/Basic.lean b/LeanInk/Analysis/Basic.lean index 50c2211..43a0ded 100644 --- a/LeanInk/Analysis/Basic.lean +++ b/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,7 +35,7 @@ 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..." @@ -42,16 +43,23 @@ def runAnalysis : AnalysisM UInt32 := do 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" diff --git a/LeanInk/Analysis/DataTypes.lean b/LeanInk/Analysis/DataTypes.lean index 24bc1ea..cbbea22 100644 --- a/LeanInk/Analysis/DataTypes.lean +++ b/LeanInk/Analysis/DataTypes.lean @@ -1,5 +1,4 @@ import LeanInk.ListUtil -import LeanInk.Configuration import Lean.Elab import Lean.Data.Lsp diff --git a/LeanInk/Analysis/SemanticToken.lean b/LeanInk/Analysis/SemanticToken.lean index 7077e0b..e697351 100644 --- a/LeanInk/Analysis/SemanticToken.lean +++ b/LeanInk/Analysis/SemanticToken.lean @@ -1,4 +1,5 @@ import LeanInk.Analysis.DataTypes +import LeanInk.Configuration import LeanInk.ListUtil import Lean.Elab diff --git a/LeanInk/Annotation/Basic.lean b/LeanInk/Annotation/Basic.lean index 98ba27e..4cc6788 100644 --- a/LeanInk/Annotation/Basic.lean +++ b/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 => diff --git a/LeanInk/Annotation/DataTypes.lean b/LeanInk/Annotation/DataTypes.lean new file mode 100644 index 0000000..0dc0c99 --- /dev/null +++ b/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 := "" \ No newline at end of file diff --git a/LeanInk/Annotation/Util.lean b/LeanInk/Annotation/Util.lean index 5026296..47501eb 100644 --- a/LeanInk/Annotation/Util.lean +++ b/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 := "" - /- FRAGMENT INTERVAL -/ inductive FragmentInterval (a : Type u) where | head (pos: String.Pos) (fragment: a) (idx: Nat) diff --git a/LeanInk/Configuration.lean b/LeanInk/Configuration.lean index 77cf519..d9b0d34 100644 --- a/LeanInk/Configuration.lean +++ b/LeanInk/Configuration.lean @@ -1,20 +1,13 @@ +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 @@ -22,10 +15,14 @@ structure Configuration where 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 \ No newline at end of file +abbrev ExecM := ReaderT Configuration $ IO \ No newline at end of file