wip

src/Elaboration/Equation.hs

@@ -49,64 +49,67 @@ contextual1 f x = do
   lift $ f c x
 
 equateM :: Flexibility -> Domain.Value -> Domain.Value -> Equate v ()
-equateM flexibility value1 value2 = do
-  value1' <- contextual1 Context.forceHeadGlue value1
-  value2' <- contextual1 Context.forceHeadGlue value2
-  case (value1', value2') of
-    -- Same heads
-    (Domain.Neutral head1 spine1, Domain.Neutral head2 spine2)
-      | head1 == head2 -> do
-          let flexibility' = max (Domain.headFlexibility head1) flexibility
-          equateSpines flexibility' spine1 spine2
-    (Domain.Con con1 args1, Domain.Con con2 args2)
-      | con1 == con2
-      , map fst args1 == map fst args2 ->
-          Tsil.zipWithM_ (equateM flexibility `on` snd) args1 args2
-      | otherwise ->
-          throwIO Nope
-    (Domain.Lit lit1, Domain.Lit lit2)
-      | lit1 == lit2 ->
-          pure ()
-      | otherwise ->
-          throwIO Nope
-    (Domain.Glued head1 spine1 value1'', Domain.Glued head2 spine2 value2'')
-      | head1 == head2 ->
-          equateSpines Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error) ->
-            equateM flexibility value1'' value2''
-      | otherwise -> do
-          ordering <- lift $ compareHeadDepths head1 head2
-          case ordering of
-            LT -> equateM flexibility value1' value2''
-            GT -> equateM flexibility value1'' value2'
-            EQ -> equateM flexibility value1'' value2''
-    (Domain.Glued _ _ value1'', _) ->
-      equateM flexibility value1'' value2'
-    (_, Domain.Glued _ _ value2'') ->
-      equateM flexibility value1' value2''
-    (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2)
-      | plicity1 == plicity2 -> do
-          equateM flexibility domain2 domain1
-          equateM flexibility target1 target2
+equateM flexibility unforcedValue1 unforcedValue2 = go unforcedValue1 unforcedValue2
+  where
+    go value1 value2 = do
+      value1' <- contextual1 Context.forceHeadGlue value1
+      value2' <- contextual1 Context.forceHeadGlue value2
+      case (value1', value2') of
+        -- Glue
+        (Domain.Glued head1 spine1 value1'', Domain.Glued head2 spine2 value2'')
+          | head1 == head2 ->
+              equateSpines Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error) ->
+                go value1'' value2''
+          | otherwise -> do
+              ordering <- lift $ compareHeadDepths head1 head2
+              case ordering of
+                LT -> go value1' value2''
+                GT -> go value1'' value2'
+                EQ -> go value1'' value2''
+        (Domain.Glued _ _ value1'', _) ->
+          go value1'' value2'
+        (_, Domain.Glued _ _ value2'') ->
+          go value1' value2''
+        -- Same heads
+        (Domain.Neutral head1 spine1, Domain.Neutral head2 spine2)
+          | head1 == head2 -> do
+              let flexibility' = max (Domain.headFlexibility head1) flexibility
+              equateSpines flexibility' spine1 spine2
+        (Domain.Con con1 args1, Domain.Con con2 args2)
+          | con1 == con2
+          , map fst args1 == map fst args2 ->
+              Tsil.zipWithM_ (equateM flexibility `on` snd) args1 args2
+          | otherwise ->
+              throwIO Nope
+        (Domain.Lit lit1, Domain.Lit lit2)
+          | lit1 == lit2 ->
+              pure ()
+          | otherwise ->
+              throwIO Nope
+        (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2)
+          | plicity1 == plicity2 -> do
+              equateM flexibility domain2 domain1
+              equateM flexibility target1 target2
 
-    -- Neutrals
-    (Domain.Neutral head1 (Domain.Apps args1), Domain.Neutral head2 (Domain.Apps args2))
-      | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility
-      , Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility
-      , (fst <$> args1) == (fst <$> args2) -> do
-          -- TODO: check both directions?
-          ordering <- lift $ compareHeadDepths head1 head2
-          case ordering of
-            LT -> solve head2 args2 value1'
-            GT -> solve head1 args1 value2'
-            EQ -> solve head2 args2 value1'
-    (Domain.Neutral head1 (Domain.Apps args1), _)
-      | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility ->
-          solve head1 args1 value2
-    (_, Domain.Neutral head2 (Domain.Apps args2))
-      | Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility ->
-          solve head2 args2 value1
-    _ ->
-      throwIO Dunno
+        -- Neutrals
+        (Domain.Neutral head1 (Domain.Apps args1), Domain.Neutral head2 (Domain.Apps args2))
+          | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility
+          , Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility
+          , (fst <$> args1) == (fst <$> args2) -> do
+              -- TODO: check both directions?
+              ordering <- lift $ compareHeadDepths head1 head2
+              case ordering of
+                LT -> solve head2 args2 unforcedValue1
+                GT -> solve head1 args1 unforcedValue2
+                EQ -> solve head2 args2 unforcedValue1
+        (Domain.Neutral head1 (Domain.Apps args1), _)
+          | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility ->
+              solve head1 args1 unforcedValue2
+        (_, Domain.Neutral head2 (Domain.Apps args2))
+          | Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility ->
+              solve head2 args2 unforcedValue1
+        _ ->
+          throwIO Dunno
 
 solve :: Domain.Head -> Domain.Args -> Domain.Value -> Equate v ()
 solve head_ args value = do