wip

ollef · Jan 14, 2024 · 4906037 · 4906037
1 parent c0410e7
commit 4906037
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 15 deletions.
diff --git a/src/Elaboration/Equation.hs b/src/Elaboration/Equation.hs
@@ -36,9 +36,9 @@ type Equate v = StateT (Context v) M
 
 equate :: Context v -> Flexibility -> Domain.Value -> Domain.Value -> M (Context v)
 equate context flexibility value1 value2 = do
-  putText "Equating"
-  Context.dumpValue context value1
-  Context.dumpValue context value2
+  -- putText "Equating"
+  -- Context.dumpValue context value1
+  -- Context.dumpValue context value2
   execStateT
     (equateM flexibility value1 value2)
     context

diff --git a/src/Elaboration/Matching.hs b/src/Elaboration/Matching.hs
@@ -441,14 +441,11 @@ simplifyMatch context canPostpone match@(Match value forcedValue plicity pat typ
           simplifyMatch context canPostpone $ Match value forcedValue plicity (Pattern span unspannedPattern) type_
     Pattern span unspannedPattern -> do
       forcedValue' <- lift $ Context.forceHead context forcedValue
-      putText "forced value"
-      lift $ Context.dumpValue context forcedValue'
       let match' =
             Match value forcedValue' plicity pat type_
       case (forcedValue', unspannedPattern) of
         (Domain.Con constr args, Con _ constr' pats)
           | constr == constr' -> do
-              putText $ "matching con" <> show constr
               matches' <- lift $ do
                 constrType <- fetch $ Query.ConstructorType constr
                 (patsType, patSpine) <-
@@ -792,7 +789,6 @@ splitConstructor outerContext config scrutineeValue scrutineeHead scrutineeSpine
           tele <- goConstrFields context' constr conArgs' target patterns'
           pure $ Telescope.Extend bindings domain'' plicity tele
         _ -> do
-          putText "Equating con"
           context' <- Equation.equate context Flexibility.Rigid scrutineeValue $ Domain.Con constr conArgs
           result <- check context' config Postponement.CanPostpone
           pure $ Telescope.Empty result
@@ -897,24 +893,19 @@ splitEqualityOr context config matches k =
       case match of
         Match
           scrutineeValue
-          scrutineeValue'
+          scrutineeValue'@Domain.Neutral {}
           _
           (Pattern _ Wildcard)
           (Builtin.Equals type_ value1 value2) -> do
-            unificationResult <- try $ do
-              putText "equating equality"
+            unificationResult <- try do
               context' <- Equation.equate context Flexibility.Rigid value1 value2
-              putText "equating equality refl"
               Equation.equate context' Flexibility.Rigid scrutineeValue' $ Builtin.Refl type_ value1 value2
             case unificationResult of
               Left Equation.Nope -> do
-                putText "nope"
                 check context config {clauses = drop 1 config.clauses} Postponement.CanPostpone
               Left Equation.Dunno -> do
-                putText "dunno"
                 splitEqualityOr context config matches' k
               Right context' -> do
-                putText "yes"
                 result <- check context' config Postponement.CanPostpone
                 scrutinee <- Elaboration.readback context' scrutineeValue
                 pure $
@@ -968,7 +959,6 @@ uninhabitedType context fuel covered type_ = do
   type' <- Context.forceHead context type_
   case type' of
     Builtin.Equals _ value1 value2 -> do
-      putText "equating for uninhabited type"
       result <- try $ Equation.equate context Flexibility.Rigid value1 value2
       pure $ case result of
         Left Equation.Nope ->