Merge pull request #49 from semorrison/whitespace

chore: normalize whitespace

LeanInk.lean

@@ -5,4 +5,4 @@ import LeanInk.Configuration
 import LeanInk.FileHelper
 import LeanInk.ListUtil
 import LeanInk.Logger
-import LeanInk.Version
+import LeanInk.Version

LeanInk/Analysis.lean

@@ -3,4 +3,4 @@ import LeanInk.Analysis.Basic
 import LeanInk.Analysis.DataTypes
 import LeanInk.Analysis.LeanContext
 import LeanInk.Analysis.SemanticToken
-import LeanInk.Analysis.InfoTreeTraversal
+import LeanInk.Analysis.InfoTreeTraversal

LeanInk/Analysis/Basic.lean

@@ -29,8 +29,8 @@ private def _buildConfiguration (arguments: List ResolvedArgument) (file: FilePa
     experimentalTypeInfo := containsFlag arguments "--x-enable-type-info"
     experimentalDocString := containsFlag arguments "--x-enable-docStrings"
     experimentalSemanticType := containsFlag arguments "--x-enable-semantic-token"
-    experimentalSorryConfig := containsFlag arguments "--x-disable-sorry-info"  
-    experimentalCalcConfig := containsFlag arguments "--x-disable-calc-info"  
+    experimentalSorryConfig := containsFlag arguments "--x-disable-sorry-info"
+    experimentalCalcConfig := containsFlag arguments "--x-disable-calc-info"
   }
 where
   getLakeFile? (arguments : List ResolvedArgument) : Option FilePath :=

LeanInk/Analysis/DataTypes.lean

@@ -19,9 +19,9 @@ class Positional (α : Type u) where
 namespace Positional
   def length { α : Type u } [Positional α] (self : α) : String.Pos := (Positional.tailPos self) - (Positional.headPos self)
 
-  def smallest? { α : Type u } [Positional α] (list : List α) : Option α := List.foldl (λ a y => 
+  def smallest? { α : Type u } [Positional α] (list : List α) : Option α := List.foldl (λ a y =>
     let y : α := y -- We need to help the compiler a bit here otherwise it thinks `y : Option α`
-    match a with 
+    match a with
     | none => y
     | some x => if (Positional.length x) <= (Positional.length y) then x else y
   ) none list
@@ -74,7 +74,7 @@ instance : Positional TypeTokenInfo where
   headPos := (λ x => x.toFragment.headPos)
   tailPos := (λ x => x.toFragment.tailPos)
 
-/-- 
+/--
   A `Token` describes the metadata of a specific range of source text.
   E.g.: a `Token.type` describes for some variable `p` that it conforms to type `Nat`.
   For every category of metadata there should be an additonal constructor with specified `TokenInfo` to make sure the
@@ -167,4 +167,4 @@ def Info.isExpanded (self : Info) : Bool :=
   let stx := Info.stx self
   match stx.getHeadInfo, stx.getTailInfo with
   | SourceInfo.original .., SourceInfo.original .. => false
-  | _, _ => true
+  | _, _ => true

LeanInk/Analysis/InfoTreeTraversal.lean

@@ -19,39 +19,39 @@ open Lean.Elab
 open Lean.Meta
 open IO
 
-structure InfoTreeContext where 
-  hasSorry : Bool 
+structure InfoTreeContext where
+  hasSorry : Bool
   isCalcTatic : Bool
 deriving Repr
 
-partial def _hasSorry (t : InfoTree) : Bool := 
+partial def _hasSorry (t : InfoTree) : Bool :=
   let rec go (ci? : Option ContextInfo) (t : InfoTree) : Bool :=
     match t with
     | InfoTree.context ci t => go ci t
     | InfoTree.node i cs =>
-      if let (some _, .ofTermInfo ti) := (ci?, i) then 
+      if let (some _, .ofTermInfo ti) := (ci?, i) then
         ti.expr.hasSorry
-      else 
+      else
         cs.any (go ci?)
     | _ => false
   go none t
 
 partial def _isCalcTatic (tree: InfoTree) : Bool :=
   match tree with
   | .context _ _ => false
-  | .node i _ => 
-    if let .ofTacticInfo ti := i then 
+  | .node i _ =>
+    if let .ofTacticInfo ti := i then
       ti.stx.getKind == ``calcTactic
-    else 
+    else
       false
   | _ => false
 
-def _buildInfoTreeContext (config : Configuration) (tree : InfoTree) : InfoTreeContext := 
+def _buildInfoTreeContext (config : Configuration) (tree : InfoTree) : InfoTreeContext :=
   let hasSorry := config.experimentalSorryConfig && (_hasSorry tree)
   let isCalcTatic := config.experimentalCalcConfig && (_isCalcTatic tree)
   InfoTreeContext.mk hasSorry isCalcTatic
 
-def _updateIsCalcTatic (config : Configuration) (ctx : InfoTreeContext) (tree : InfoTree) : InfoTreeContext := 
+def _updateIsCalcTatic (config : Configuration) (ctx : InfoTreeContext) (tree : InfoTree) : InfoTreeContext :=
   { ctx with isCalcTatic := if config.experimentalCalcConfig then ctx.isCalcTatic || _isCalcTatic tree else false }
 
 structure ContextBasedInfo (β : Type) where
@@ -81,10 +81,10 @@ namespace TraversalFragment
     if Info.isExpanded info then
       pure (none, none)
     else
-      let mut semantic : Option SemanticTraversalInfo := none 
+      let mut semantic : Option SemanticTraversalInfo := none
       if (← read).experimentalSemanticType then
         semantic := some { node := info, stx := info.stx }
-      match info with 
+      match info with
       | Info.ofTacticInfo info => pure (tactic { info := info, ctx := ctx }, semantic)
       | Info.ofTermInfo info => pure (term { info := info, ctx := ctx }, semantic)
       | Info.ofFieldInfo info => pure (field { info := info, ctx := ctx }, semantic)
@@ -96,7 +96,7 @@ namespace TraversalFragment
   | tactic fragment => fragment.ctx.runMetaM {} (func (tactic fragment))
   | unknown fragment => fragment.ctx.runMetaM {} (func (unknown fragment))
 
-  /- 
+  /-
     Token Generation
   -/
   def inferType? : TraversalFragment -> MetaM (Option String)
@@ -144,28 +144,28 @@ namespace TraversalFragment
   /- Sentence Generation -/
   private def genGoal (goalType : Format) (hypotheses : List Hypothesis): Name -> MetaM (Goal)
     | Name.anonymous => do
-      return { 
+      return {
         name := ""
         conclusion := toString goalType
-        hypotheses := hypotheses 
+        hypotheses := hypotheses
       }
     | name => do
       let goalFormatName := format name.eraseMacroScopes
-      return { 
+      return {
         name := toString goalFormatName
         conclusion := toString goalType
-        hypotheses := hypotheses 
+        hypotheses := hypotheses
       }
 
-  /-- 
+  /--
   This method is a adjusted version of the Meta.ppGoal function. As we do need to extract the goal informations into seperate properties instead
   of a single formatted string to support the Alectryon.Goal datatype.
   -/
   private def evalGoal (mvarId : MVarId) (infoTreeCtx : InfoTreeContext) : MetaM (Option Goal) := do
     match (← getMCtx).findDecl? mvarId with
     | none => return none
     | some decl => do
-      if infoTreeCtx.hasSorry || infoTreeCtx.isCalcTatic then 
+      if infoTreeCtx.hasSorry || infoTreeCtx.isCalcTatic then
         return none
       else
         let ppAuxDecls := pp.auxDecls.get (← getOptions)
@@ -204,11 +204,11 @@ namespace TraversalFragment
               pure (varNames, prevType?, hypotheses)
             else
               evalVar varNames prevType? hypotheses localDecl
-          let hypotheses ← pushPending hypotheses type? varNames 
+          let hypotheses ← pushPending hypotheses type? varNames
           let typeFmt ← ppExpr (← instantiateMVars decl.type)
           return (← genGoal typeFmt hypotheses decl.userName)
 
-  private def _genGoals (contextInfo : ContextBasedInfo TacticInfo) (goals: List MVarId) (metaCtx: MetavarContext) (infoTreeCtx : InfoTreeContext) : AnalysisM (List Goal) := 
+  private def _genGoals (contextInfo : ContextBasedInfo TacticInfo) (goals: List MVarId) (metaCtx: MetavarContext) (infoTreeCtx : InfoTreeContext) : AnalysisM (List Goal) :=
     let ctx := { contextInfo.ctx with mctx := metaCtx }
     return (← ctx.runMetaM {} (goals.mapM (fun x => evalGoal x infoTreeCtx))).filterMap id
 
@@ -220,12 +220,12 @@ namespace TraversalFragment
 
   def genTactic? (self : TraversalFragment) (infoTreeCtx : InfoTreeContext) : AnalysisM (Option Tactic) := do
     match self with
-    | tactic fragment => do 
+    | tactic fragment => do
       let goalsBefore ← genGoals fragment true infoTreeCtx
       let goalsAfter ← genGoals fragment false infoTreeCtx
-      if infoTreeCtx.hasSorry || infoTreeCtx.isCalcTatic then do 
+      if infoTreeCtx.hasSorry || infoTreeCtx.isCalcTatic then do
         return some { headPos := self.headPos, tailPos := self.tailPos, goalsBefore := [], goalsAfter := [] }
-      if goalsAfter.isEmpty then  
+      if goalsAfter.isEmpty then
         return some { headPos := self.headPos, tailPos := self.tailPos, goalsBefore := goalsBefore, goalsAfter := [{ name := "", conclusion := "Goals accomplished! 🐙", hypotheses := [] }] }
       else
         return some { headPos := self.headPos, tailPos := self.tailPos, goalsBefore := goalsBefore, goalsAfter := goalsAfter }
@@ -307,13 +307,13 @@ namespace TraversalAux
       if self.allowsNewTerm then
         let newResult ← self.result.insertFragment fragment infoTreeCtx
         return { self with allowsNewTerm := false, result := newResult }
-      else 
+      else
         return self
     | TraversalFragment.field _ => do
       if self.allowsNewField then
         let newResult ← self.result.insertFragment fragment infoTreeCtx
         return { self with allowsNewField := false, result := newResult }
-      else 
+      else
         return self
     | TraversalFragment.tactic contextInfo => do
       let tacticChildren := self.result.sentences.filterMap (λ f => f.asTactic?)
@@ -335,18 +335,18 @@ end TraversalAux
 partial def _resolveTacticList (ctx?: Option ContextInfo := none) (aux : TraversalAux := {}) (tree : InfoTree) (infoTreeCtx : InfoTreeContext) : AnalysisM TraversalAux := do
   let config ← read
   match tree with
-  | InfoTree.context ctx tree => _resolveTacticList ctx aux tree (_updateIsCalcTatic config infoTreeCtx tree) 
+  | InfoTree.context ctx tree => _resolveTacticList ctx aux tree (_updateIsCalcTatic config infoTreeCtx tree)
   | InfoTree.node info children =>
     match ctx? with
     | some ctx => do
       let ctx? := info.updateContext? ctx
-      let resolvedChildrenLeafs ← children.toList.mapM (fun x => _resolveTacticList ctx? aux x (_updateIsCalcTatic config infoTreeCtx x)) 
+      let resolvedChildrenLeafs ← children.toList.mapM (fun x => _resolveTacticList ctx? aux x (_updateIsCalcTatic config infoTreeCtx x))
       let sortedChildrenLeafs := resolvedChildrenLeafs.foldl TraversalAux.merge {}
       match (← TraversalFragment.create ctx info) with
       | (some fragment, some semantic) => do
         let sortedChildrenLeafs ← sortedChildrenLeafs.insertSemanticInfo semantic
-        sortedChildrenLeafs.insertFragment fragment infoTreeCtx         
-      | (some fragment, none) => sortedChildrenLeafs.insertFragment fragment infoTreeCtx         
+        sortedChildrenLeafs.insertFragment fragment infoTreeCtx
+      | (some fragment, none) => sortedChildrenLeafs.insertFragment fragment infoTreeCtx
       | (none, some semantic) => sortedChildrenLeafs.insertSemanticInfo semantic
       | (_, _) => pure sortedChildrenLeafs
     | none => pure aux
@@ -367,7 +367,7 @@ def _resolveTask (tree : InfoTree) (infoTreeCtx : InfoTreeContext) : AnalysisM (
 
 def _resolve (trees: List InfoTree) : AnalysisM AnalysisResult := do
   let config ← read
-  let auxResults ← (trees.map (λ t => 
+  let auxResults ← (trees.map (λ t =>
     _resolveTacticList none {} t (_buildInfoTreeContext config t))).mapM (λ x => x)
   let results := auxResults.map (λ x => x.result)
   return results.foldl AnalysisResult.merge AnalysisResult.empty

LeanInk/Analysis/LeanContext.lean

@@ -55,7 +55,7 @@ def initializeLakeContext (lakeFile : FilePath) (header : Syntax) : AnalysisM Un
       | Except.ok val => match fromJson? val with
         | Except.error _ => throw <| IO.userError s!"Failed to decode lake output: {stdout}"
         | Except.ok paths => do
-          let paths : LeanPaths := paths 
+          let paths : LeanPaths := paths
           initializeLeanContext
           initSearchPath (← findSysroot) paths.oleanPath
           logInfo s!"{paths.oleanPath}"
@@ -65,6 +65,6 @@ def initializeLakeContext (lakeFile : FilePath) (header : Syntax) : AnalysisM Un
 
 def initializeSearchPaths (header : Syntax) (config : Configuration) : AnalysisM Unit := do
   match config.lakeFile with
-  | some lakeFile => do 
+  | some lakeFile => do
     initializeLakeContext lakeFile header
   | none => initializeLeanContext

LeanInk/Annotation/Alectryon.lean

@@ -56,7 +56,7 @@ structure Goal where
   deriving ToJson
 
 structure Message where
-  _type : String := "message"  
+  _type : String := "message"
   contents : String
   deriving ToJson
 
@@ -72,7 +72,7 @@ structure Text where
   contents : Contents
   deriving ToJson
 
-/-- 
+/--
 We need a custom ToJson implementation for Alectryons fragments.
 
 For example we have following fragment:
@@ -102,7 +102,7 @@ instance : ToJson Fragment where
     | Fragment.text v => toJson v
     | Fragment.sentence v => toJson v
 
-/- 
+/-
   Token Generation
 -/
 
@@ -111,7 +111,7 @@ def genTypeInfo? (getContents : String.Pos -> String.Pos -> Option String) (toke
   | some type => do
     let headPos := Positional.headPos token
     let tailPos := Positional.tailPos token
-    match getContents headPos tailPos with 
+    match getContents headPos tailPos with
     | none => pure none
     | "" => pure none
     | some x => return some { name := x, type := type }
@@ -136,12 +136,12 @@ def genToken (token : Compound Analysis.Token) (contents : Option String) (getCo
     let semanticToken := Positional.smallest? semanticTokens
     let semanticTokenType ← genSemanticTokenValue semanticToken
     match (Positional.smallest? typeTokens) with
-    | none => do 
+    | none => do
       return some { raw := contents, semanticType := semanticTokenType }
-    | some token => do 
+    | some token => do
       return some { raw := contents, typeinfo := ← genTypeInfo? getContents token, link := none, docstring := token.docString, semanticType := semanticTokenType }
 
-def extractContents (offset : String.Pos) (contents : String) (head tail: String.Pos) : Option String := 
+def extractContents (offset : String.Pos) (contents : String) (head tail: String.Pos) : Option String :=
   if head >= tail then
     none
   else
@@ -174,8 +174,8 @@ partial def genTokens (contents : String) (head : String.Pos) (offset : String.P
   match extractContents offset contents head (⟨contents.utf8ByteSize⟩ + offset) with
   | none => return tokens.reverse
   | some x => return ({ raw := x }::tokens).reverse
-  
-/- 
+
+/-
   Fragment Generation
 -/
 
@@ -191,15 +191,15 @@ def genGoal (goal : Analysis.Goal) : Goal := {
   hypotheses := (goal.hypotheses.map genHypothesis).toArray
 }
 
-def genGoals (beforeNode: Bool) (tactic : Analysis.Tactic) : List Goal := 
-  if beforeNode then 
+def genGoals (beforeNode: Bool) (tactic : Analysis.Tactic) : List Goal :=
+  if beforeNode then
     tactic.goalsBefore.map (λ g => genGoal g)
   else
     tactic.goalsAfter.map (λ g => genGoal g)
 
 def genMessages (message : Analysis.Message) : Message := { contents := message.msg }
 
-def isComment (contents : String) : Bool := 
+def isComment (contents : String) : Bool :=
   let contents := contents.trim
   contents.startsWith "--" || contents.startsWith "/-"
 
@@ -227,7 +227,7 @@ def genFragment (annotation : Annotation) (globalTailPos : String.Pos) (contents
       let headPos := annotation.sentence.headPos
       let tokens ← genTokens contents headPos headPos [] annotation.tokens
       fragmentContents := Contents.experimentalTokens tokens.toArray
-    return Fragment.sentence { 
+    return Fragment.sentence {
       contents := fragmentContents
       goals := goals.toArray
       messages := (messages.map genMessages).toArray

LeanInk/Annotation/Basic.lean

@@ -23,21 +23,21 @@ def tokensBetween (head : String.Pos) (tail : Option String.Pos) (compounds: Lis
     | (some tail, some tokenTail) =>
       if token.headPos <= tail && tokenTail > head then
         tokens ← tokens.push token
-    | (none, some tokenTail) => 
+    | (none, some tokenTail) =>
       if tokenTail > head then
         tokens ← tokens.push token
   return tokens.toList
 
 def matchTokenToAnalysis (tokens : List (Compound Token)) (aux : List Annotation) : List (Compound Sentence) -> List Annotation
   | [] => aux
-  | x::y::xs => 
+  | x::y::xs =>
     let tokens := (tokens.dropWhile (λ t => x.headPos > t.tailPos.getD t.headPos))
     matchTokenToAnalysis tokens (aux.append [{ sentence := x, tokens := tokensBetween x.headPos y.headPos tokens}]) (y::xs)
-  | x::xs => 
+  | x::xs =>
     let tokens := (tokens.dropWhile (λ t => x.headPos > t.tailPos.getD t.headPos))
     matchTokenToAnalysis tokens (aux.append [{ sentence := x, tokens := tokensBetween x.headPos none tokens}]) xs
 
 def annotateFile (analysis : AnalysisResult) : AnalysisM (List Annotation) := do
   let compounds ← matchCompounds (toFragmentIntervals analysis.sentences)
   let tokens ← matchCompounds (toFragmentIntervals analysis.tokens)
-  return matchTokenToAnalysis tokens [] compounds
+  return matchTokenToAnalysis tokens [] compounds

LeanInk/Annotation/DataTypes.lean

@@ -24,4 +24,4 @@ namespace Compound
 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 ++ ">"
+  toString (self : Compound a) : String := "<COMPOUND head:" ++ toString self.headPos ++ " fragments := " ++ toString self.getFragments ++ ">"

LeanInk/Annotation/Util.lean

@@ -85,7 +85,7 @@ def _insertCompound [Positional a] [ToString a] (e : FragmentInterval a) (compou
           let updatedCompound := { c with tailPos := none, fragments := newFragments}
           logInfo s!"FOUND COMPOUND {c} -> UPDATING CURRENT WITH TAIL AT {e.position} -> {updatedCompound}"
           return updatedCompound::cs
-        else 
+        else
           /-
             It may be the case that the newFragments list isEmpty. This is totally fine as we need to
             insert text spacers later for the text. No we can simply generate a text fragment whenever a compound is empty.
@@ -99,4 +99,4 @@ def matchCompounds [Positional a] [ToString a] (events : List (FragmentInterval
   let mut compounds : List (Compound a) := [{ headPos := 0, tailPos := none, fragments := [] }]
   for e in events do
     compounds ← _insertCompound e compounds
-  return compounds.reverse
+  return compounds.reverse