From 490603791bcd6f6d329ea37d3e523826ee5136b7 Mon Sep 17 00:00:00 2001
From: Olle Fredriksson <fredriksson.olle@gmail.com>
Date: Sun, 14 Jan 2024 01:07:27 +0100
Subject: [PATCH] wip

---
 src/Elaboration/Equation.hs |  6 +++---
 src/Elaboration/Matching.hs | 14 ++------------
 2 files changed, 5 insertions(+), 15 deletions(-)

diff --git a/src/Elaboration/Equation.hs b/src/Elaboration/Equation.hs
index 33ff969..9cf69d6 100644
--- 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
index 1addf26..c894cad 100644
--- 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 ->