wip

src/Elaboration.hs

@@ -759,11 +759,9 @@ elaborateLets context declaredNames undefinedVars definedVars lets body mode = d
               . Syntax.Let bindings Index.Zero boundTerm
               <$> lets''
         Just (previousSpan, var) -> do
-          case Context.lookupVarValue var context of
-            Just _ -> do
-              Context.report (Context.spanned span context) $ Error.DuplicateLetName surfaceName previousSpan
-              elaborateLets context declaredNames undefinedVars definedVars lets' body mode
-            Nothing -> do
+          value <- Context.forceHead context (Domain.Neutral (Domain.Var var) Domain.Empty)
+          case value of
+            (Domain.Neutral (Domain.Var sameVar) Domain.Empty) | var == sameVar -> do
               let type_ =
                     Context.lookupVarType var context
               boundTerm <- Clauses.check context clauses' type_
@@ -781,12 +779,15 @@ elaborateLets context declaredNames undefinedVars definedVars lets body mode = d
                 pure $ defines context values
               lets'' <- elaborateLets redefinedContext declaredNames undefinedVars' definedVars' lets' body mode
               pure $ Syntax.Let bindings index boundTerm <$> lets''
+            _ -> do
+              Context.report (Context.spanned span context) $ Error.DuplicateLetName surfaceName previousSpan
+              elaborateLets context declaredNames undefinedVars definedVars lets' body mode
   where
     defines :: Context v -> Tsil (Var, Domain.Value) -> Context v
     defines =
       foldr' \(var, value) context' ->
         if isJust $ Context.lookupVarIndex var context'
-          then Context.defineWellOrdered context' var value
+          then Context.defineWellOrdered context' (Domain.Var var) Domain.Empty value
           else context'
 
 forceExpectedTypeHead :: Context v -> Mode result -> M (Mode result)

src/Elaboration/Context.hs

@@ -30,6 +30,7 @@ import qualified Data.EnumSet as EnumSet
 import Data.HashMap.Lazy (HashMap)
 import qualified Data.HashMap.Lazy as HashMap
 import Data.HashSet (HashSet)
+import qualified Data.HashSet as HashSet
 import Data.IORef.Lifted
 import Data.IntSeq (IntSeq)
 import qualified Data.IntSeq as IntSeq
@@ -96,7 +97,27 @@ toEnvironment
 toEnvironment context =
   Environment
     { indices = context.indices
-    , values = mempty
+    , values =
+        EnumMap.fromList
+          $ mapMaybe
+            ( \(head_, spines) ->
+                case head_ of
+                  Domain.Var var -> do
+                    let emptySpineValues =
+                          mapMaybe
+                            ( \(spine, value) ->
+                                case spine of
+                                  Domain.Empty -> Just (var, value)
+                                  _ -> Nothing
+                            )
+                            spines
+                    case emptySpineValues of
+                      [value] -> Just value
+                      [] -> Nothing
+                      _ -> panic "multiple spine values"
+                  _ -> Nothing
+            )
+          $ HashMap.toList context.equations.equal
     , glueableBefore = Index.Zero
     }
 
@@ -166,6 +187,14 @@ coveredConstructors context head_ spine = fst <$> coveredConstructorsAndLiterals
 coveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Literal)
 coveredLiterals context head_ spine = snd <$> coveredConstructorsAndLiterals context head_ spine
 
+withCoveredConstructors :: Context v -> Domain.Head -> Domain.Spine -> HashSet Name.QualifiedConstructor -> Context v
+withCoveredConstructors context head spine constructors =
+  context {equations = context.equations {notEqual = HashMap.insertWith (<>) head [(spine, constructors, mempty)] context.equations.notEqual}}
+
+withCoveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> HashSet Literal -> Context v
+withCoveredLiterals context head spine literals =
+  context {equations = context.equations {notEqual = HashMap.insertWith (<>) head [(spine, mempty, literals)] context.equations.notEqual}}
+
 -------------------------------------------------------------------------------
 -- Extension
 
@@ -295,14 +324,15 @@ define :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> M (Context
 define context head_ spine value = do
   deps <- evalStateT (freeVars context value) mempty
   let context' = defineWellOrdered context head_ spine value
-      (pre, post) =
-        Tsil.partition (`EnumSet.member` deps) $
-          IntSeq.toTsil context'.boundVars
-  pure
-    context'
-      { boundVars =
-          IntSeq.fromTsil pre <> IntSeq.fromTsil post
-      }
+      context''
+        | EnumSet.null deps = context'
+        | otherwise =
+            context'
+              { boundVars =
+                  IntSeq.fromTsil pre <> IntSeq.fromTsil post
+              }
+      (pre, post) = Tsil.partition (`EnumSet.member` deps) $ IntSeq.toTsil context'.boundVars
+  pure context''
 
 -- TODO: Move
 freeVars