Factor out the parsing library

Russoul · Aug 10, 2024 · 29a4854 · 29a4854
1 parent 756df32
commit 29a4854
Show file tree

Hide file tree

Showing 32 changed files with 62 additions and 1,387 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "Just-a-Parser"]
+	path = Just-a-Parser
+	url = https://github.com/Russoul/Just-a-Parser.git
diff --git a/Just-a-Parser b/Just-a-Parser
diff --git a/nova-api.ipkg b/nova-api.ipkg
@@ -1,6 +1,6 @@
 package nova-api
 
-depends = contrib, just-a-monad
+depends = contrib, just-a-monad, just-a-parser
 
 modules =
           Control.Monad.IOEither
@@ -11,7 +11,6 @@ modules =
         , Data.AlternatingSnocList
         , Data.AlternatingSnocList1
         , Data.Interpolation
-        , Data.Location
         , Data.Util
 
         , Nova.Core.Context
@@ -60,11 +59,4 @@ modules =
         , Solver.CommutativeMonoid.Quotation
         , Solver.CommutativeMonoid.Value
 
-        , Text.Lexing.Token
-        , Text.Lexing.Tokeniser
-
-        , Text.Parsing.CharUtil
-        , Text.Parsing.Fork
-        , Text.Parsing.TokenUtil
-
 sourcedir = "src/idris"
diff --git a/nova-bin.ipkg b/nova-bin.ipkg
@@ -1,6 +1,6 @@
 package nova-bin
 
-depends = contrib, just-a-monad
+depends = contrib, just-a-monad, just-a-parser
 
 sourcedir = "src/idris"
 

diff --git a/src/idris/Data/Location.idr b/src/idris/Data/Location.idr
diff --git a/src/idris/Nova/Core/Unification.idr b/src/idris/Nova/Core/Unification.idr
@@ -1,12 +1,13 @@
 module Nova.Core.Unification
 
+import Me.Russoul.Data.Location
+
 import Data.List
 import Data.SnocList
 import Data.Util
 import Data.Maybe
 import Data.AVL
 import Data.Fin
-import Data.Location
 
 import Text.PrettyPrint.Prettyprinter.Render.Terminal
 import Text.PrettyPrint.Prettyprinter

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Common.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Common.idr
@@ -1,11 +1,12 @@
 module Nova.Surface.Elaboration.Implementation.Common
 
+import Me.Russoul.Data.Location
+
 import Data.AVL
 import Data.List
 import Data.List1
 import Data.SnocList
 import Data.Fin
-import Data.Location
 import Data.String
 
 import Text.PrettyPrint.Prettyprinter.Render.Terminal

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Elem.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Elem.idr
@@ -1,11 +1,12 @@
 module Nova.Surface.Elaboration.Implementation.Elem
 
+import Me.Russoul.Data.Location
+
 import Data.AVL
 import Data.List
 import Data.List1
 import Data.SnocList
 import Data.Fin
-import Data.Location
 import Data.String
 
 import Text.PrettyPrint.Prettyprinter.Render.Terminal

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Solve.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Solve.idr
@@ -1,11 +1,12 @@
 module Nova.Surface.Elaboration.Implementation.Solve
 
+import Me.Russoul.Data.Location
+
 import Data.AVL
 import Data.List
 import Data.List1
 import Data.SnocList
 import Data.Fin
-import Data.Location
 import Data.String
 
 import Text.PrettyPrint.Prettyprinter.Render.Terminal

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic.idr
@@ -1,11 +1,12 @@
 module Nova.Surface.Elaboration.Implementation.Tactic
 
+import Me.Russoul.Data.Location
+
 import Data.AVL
 import Data.List
 import Data.List1
 import Data.SnocList
 import Data.Fin
-import Data.Location
 import Data.String
 
 import Text.PrettyPrint.Prettyprinter.Render.Terminal

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/NormaliseCommutativeMonoid.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/NormaliseCommutativeMonoid.idr
@@ -1,15 +1,16 @@
 module Nova.Surface.Elaboration.Implementation.Tactic.NormaliseCommutativeMonoid
 
+import Me.Russoul.Data.Location
+import Me.Russoul.Text.Lexer.Token
+
 import Data.AVL
 import Data.Fin
 import Data.List1
-import Data.Location
 import Data.SnocList
 import Data.Util
 import Data.Either
 
 import Text.PrettyPrint.Prettyprinter
-import Text.Lexing.Token
 
 import Nova.Core.Context
 import Nova.Core.Conversion

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/TermLens.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/TermLens.idr
@@ -1,6 +1,7 @@
 module Nova.Surface.Elaboration.Implementation.Tactic.TermLens
 
-import Data.Location
+import Me.Russoul.Data.Location
+
 import Data.String
 
 import Text.PrettyPrint.Prettyprinter

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/Trivial.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/Trivial.idr
@@ -1,6 +1,7 @@
 module Nova.Surface.Elaboration.Implementation.Tactic.Trivial
 
-import Data.Location
+import Me.Russoul.Data.Location
+
 import Data.SnocList
 
 import Nova.Core.Context

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/Unfold.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/Unfold.idr
@@ -1,7 +1,8 @@
 module Nova.Surface.Elaboration.Implementation.Tactic.Unfold
 
+import Me.Russoul.Data.Location
+
 import Data.Fin
-import Data.Location
 import Data.SnocList
 import Data.Util
 

diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/TopLevel.idr b/src/idris/Nova/Surface/Elaboration/Implementation/TopLevel.idr
@@ -1,10 +1,11 @@
 module Nova.Surface.Elaboration.Implementation.TopLevel
 
+import Me.Russoul.Data.Location
+
 import Data.AVL
 import Data.List
 import Data.List1
 import Data.Fin
-import Data.Location
 import Data.String
 
 import Nova.Core.Context