wip

src/Core/Domain.hs

@@ -9,12 +9,12 @@ module Core.Domain where
 
 import Core.Binding (Binding)
 import Core.Bindings (Bindings)
+import {-# SOURCE #-} qualified Core.Environment (Environment)
 import qualified Core.Syntax as Syntax
 import Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import Data.Tsil (Tsil)
 import qualified Data.Tsil as Tsil
-import qualified Environment
 import Flexibility (Flexibility)
 import qualified Flexibility
 import Index
@@ -44,14 +44,14 @@ data Head
   | Meta !Meta.Index
   deriving (Show, Eq, Generic, Hashable)
 
-type Environment = Environment.Environment Value
-
 data Closure where
   Closure :: Environment v -> Scope Syntax.Term v -> Closure
 
 data Branches where
   Branches :: Environment v -> Syntax.Branches v -> Maybe (Syntax.Term v) -> Branches
 
+type Environment = Core.Environment.Environment
+
 var :: Var -> Value
 var v = Neutral (Var v) mempty
 

src/Core/Environment.hs

@@ -0,0 +1,90 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module Core.Environment where
+
+import qualified Core.Domain as Domain
+import Data.HashMap.Lazy (HashMap)
+import qualified Data.HashMap.Lazy as HashMap
+import Data.HashSet (HashSet)
+import Data.IORef
+import qualified Data.Kind
+import qualified Elaboration.Meta as Meta
+import Index
+import qualified Index.Map
+import qualified Index.Map as Index (Map)
+import Literal (Literal)
+import Monad
+import qualified Name
+import Protolude
+import Var (Var)
+
+data Environment (v :: Data.Kind.Type) = Environment
+  { indices :: Index.Map v Var
+  , equal :: HashMap Domain.Head [(Domain.Spine, Domain.Value)]
+  , notEqual :: HashMap Domain.Head [(Domain.Spine, HashSet Name.QualifiedConstructor, HashSet Literal)]
+  , glueableBefore :: !(Index (Succ v))
+  }
+
+empty :: Environment Void
+empty =
+  Environment
+    { indices = Index.Map.Empty
+    , equal = mempty
+    , notEqual = mempty
+    , glueableBefore = Index.Zero
+    }
+
+extend
+  :: Environment v
+  -> M (Environment (Succ v), Var)
+extend env = do
+  var <- freshVar
+  pure (extendVar env var, var)
+
+extendVar
+  :: Environment v
+  -> Var
+  -> Environment (Succ v)
+extendVar env v =
+  env
+    { indices = env.indices Index.Map.:> v
+    , glueableBefore = Index.Succ env.glueableBefore
+    }
+
+extendValue
+  :: Environment v
+  -> Domain.Value
+  -> M (Environment (Succ v), Var)
+extendValue env value = do
+  var <- freshVar
+  pure
+    ( env
+        { indices = env.indices Index.Map.:> var
+        , equal = HashMap.insert (Domain.Var var) [(mempty, value)] env.equal
+        , glueableBefore = Index.Succ env.glueableBefore
+        }
+    , var
+    )
+
+define :: Environment v -> Domain.Head -> Domain.Spine -> Domain.Value -> Environment v
+define env head_ spine value =
+  env {equal = HashMap.insertWith (<>) head_ [(spine, value)] env.equal}
+
+lookupVarIndex :: Var -> Environment v -> Maybe (Index v)
+lookupVarIndex var env =
+  Index.Map.elemIndex var env.indices
+
+lookupIndexVar :: Index v -> Environment v -> Var
+lookupIndexVar index env =
+  Index.Map.index (indices env) index
+
+lookupIndexValue :: Index v -> Environment v -> Maybe Domain.Value
+lookupIndexValue index env =
+  lookupVarValue (lookupIndexVar index env) env
+
+lookupVarValue :: Var -> Environment v -> Maybe Domain.Value
+lookupVarValue v env =
+  case HashMap.lookup (Domain.Var v) env.equal of
+    Just [(Domain.Empty, value)] -> Just value
+    _ -> Nothing

src/Core/Environment.hs-boot

@@ -0,0 +1,9 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RoleAnnotations #-}
+
+module Core.Environment where
+
+import qualified Data.Kind
+
+type role Environment phantom
+data Environment (v :: Data.Kind.Type)

src/Core/Evaluation.hs

@@ -13,13 +13,13 @@ import Core.Bindings (Bindings)
 import qualified Core.Domain as Domain
 import qualified Core.Domain.Telescope as Domain (Telescope)
 import qualified Core.Domain.Telescope as Domain.Telescope
+import qualified Core.Environment as Environment
 import qualified Core.Syntax as Syntax
 import Data.OrderedHashMap (OrderedHashMap)
 import qualified Data.OrderedHashMap as OrderedHashMap
 import Data.Some (Some)
 import Data.Tsil (Tsil)
 import qualified Data.Tsil as Tsil
-import qualified Environment
 import qualified Index
 import Literal (Literal)
 import Monad
@@ -130,7 +130,7 @@ evaluateLets env boundTerms lets =
     defines =
       foldr' \(var, value) env' ->
         if isJust $ Environment.lookupVarIndex var env'
-          then Environment.define env' var value
+          then Environment.define env' (Domain.Var var) Domain.Empty value
           else env'
 
 chooseConstructorBranch

src/Core/Readback.hs

@@ -5,10 +5,10 @@ module Core.Readback where
 
 import Core.Bindings (Bindings)
 import qualified Core.Domain as Domain
+import qualified Core.Environment as Environment
 import qualified Core.Evaluation as Evaluation
 import qualified Core.Syntax as Syntax
 import qualified Data.OrderedHashMap as OrderedHashMap
-import qualified Environment
 import Index
 import Monad
 import Protolude hiding (IntMap, Seq, evaluate, force, head)

src/Core/Zonking.hs

@@ -5,11 +5,11 @@ module Core.Zonking where
 import Core.Binding (Binding)
 import Core.Bindings (Bindings)
 import qualified Core.Domain as Domain
+import qualified Core.Environment as Environment
 import qualified Core.Evaluation as Evaluation
 import qualified Core.Readback as Readback
 import qualified Core.Syntax as Syntax
 import qualified Data.OrderedHashMap as OrderedHashMap
-import qualified Environment
 import qualified Meta
 import Monad
 import qualified Postponement

src/Elaboration.hs-boot

@@ -1,12 +1,8 @@
 module Elaboration where
 
-import Protolude
-
-import Data.HashSet (HashSet)
-import Prettyprinter (Doc)
-
 import qualified Core.Domain as Domain
 import qualified Core.Syntax as Syntax
+import Data.HashSet (HashSet)
 import Elaboration.Context (Context)
 import Literal (Literal)
 import qualified Meta
@@ -15,26 +11,24 @@ import Name (Name)
 import qualified Name
 import Plicity
 import qualified Postponement
+import Prettyprinter (Doc)
+import Protolude
 import qualified Surface.Syntax as Surface
 
 check
   :: Context v
   -> Surface.Term
   -> Domain.Type
   -> M (Syntax.Term v)
-
 inferLiteral :: Literal -> Domain.Type
-
 evaluate
   :: Context v
   -> Syntax.Term v
   -> M Domain.Value
-
 readback
   :: Context v
   -> Domain.Value
   -> M (Syntax.Term v)
-
 getExpectedTypeName
   :: Context v
   -> Domain.Type
@@ -50,7 +44,6 @@ resolveConstructor
   -> HashSet Name.Qualified
   -> M (Maybe (Either Meta.Index Name.Qualified))
   -> M (Either Meta.Index ResolvedConstructor)
-
 inferenceFailed
   :: Context v
   -> M (Syntax.Term v, Domain.Type)
@@ -65,9 +58,7 @@ insertMetas
   -> InsertUntil
   -> Domain.Type
   -> M ([(Plicity, Domain.Value)], Domain.Type)
-
 prettyValue :: Context v -> Domain.Value -> M (Doc ann)
-
 postpone
   :: Context v
   -> Domain.Type