Split Elaboration into multiple files. That didn't fix performance th…

…ough.
Russoul · Dec 24, 2023 · c5efe76 · c5efe76
1 parent 32034b0
commit c5efe76
Show file tree

Hide file tree

Showing 17 changed files with 2,090 additions and 1,742 deletions.
diff --git a/nova-api.ipkg b/nova-api.ipkg
@@ -27,6 +27,16 @@ modules =
         , Nova.Core.Unification
 
         , Nova.Surface.Elaboration
+        , Nova.Surface.Elaboration.Implementation
+        , Nova.Surface.Elaboration.Implementation.Common
+        , Nova.Surface.Elaboration.Implementation.Elem
+        , Nova.Surface.Elaboration.Implementation.Solve
+        , Nova.Surface.Elaboration.Implementation.Tactic
+        , Nova.Surface.Elaboration.Implementation.Tactic.Trivial
+        , Nova.Surface.Elaboration.Implementation.Tactic.Unfold
+        , Nova.Surface.Elaboration.Implementation.TopLevel
+        , Nova.Surface.Elaboration.Implementation.Typ
+        , Nova.Surface.Elaboration.Interface
         , Nova.Surface.Language
         , Nova.Surface.ModuleSystem
         , Nova.Surface.Operator
@@ -36,9 +46,6 @@ modules =
         , Nova.Surface.SemanticToken
         , Nova.Surface.Shunting
 
-        , Nova.Surface.Tactic.Trivial
-        , Nova.Surface.Tactic.Unfold
-
         , Nova.Test.Test
 
         , Text.Lexing.Token

diff --git a/src/idris/Data/AVL.idr b/src/idris/Data/AVL.idr
@@ -10,6 +10,8 @@ import public Data.Util
 -- Original source is a haskell implementation:
 -- https://gist.github.com/timjb/8292342
 
+%hide Prelude.ord
+
 data Balance = MinusOne | Zero | PlusOne
 
 infixl 5 `unite`

diff --git a/src/idris/Nova/Core/Context.idr b/src/idris/Nova/Core/Context.idr
@@ -110,6 +110,18 @@ namespace Index
     (_, (x, ty), _) <- mbIndex idx ctx
     pure (x, ContextSubstElim ty (Context.WkN (S idx)))
 
+namespace VarName
+  ||| Γ₀ (xᵢ : A) Γ₁ ⊦ xᵢ : A
+  public export
+  lookupContext : Context -> VarName -> Maybe (Elem, Typ)
+  lookupContext [<] x = Nothing
+  lookupContext (ctx :< (x, ty)) y = M.do
+    case x == y of
+      True => Just (ContextVarElim 0, ContextSubstElim ty Wk)
+      False => do
+        (t, ty) <- lookupContext ctx y
+        Just (ContextSubstElim t Wk, ContextSubstElim ty Wk)
+
 ||| In case the entry is an element entry, return the context and the type.
 public export
 mbElemSignature : SignatureEntry -> Maybe (Context, Typ)