wip

src/Elaboration/Context.hs

@@ -321,6 +321,9 @@ skip context = do
 
 define :: Context v -> Domain.Head -> Domain.Args -> Domain.Value -> M (Context v)
 define context head_ args value = do
+  putText "define"
+  dumpValue context (Domain.Neutral head_ $ Domain.Apps args)
+  dumpValue context value
   deps <- evalStateT (freeVars context value) mempty
   let context' = defineWellOrdered context head_ args value
       context''
@@ -477,7 +480,6 @@ dumpTerm context term = do
   term' <- zonk context term
   doc <- prettyTerm context term'
   liftIO $ Prettyprinter.putDoc doc
-  putText ""
 
 prettyValue :: Context v -> Domain.Value -> M (Doc ann)
 prettyValue context term = do
@@ -486,8 +488,21 @@ prettyValue context term = do
 
 dumpValue :: Context v -> Domain.Value -> M ()
 dumpValue context value = do
-  term <- Readback.readback (toEnvironment context) value
+  let env = toEnvironment context
+  term <- Readback.readback env value
   dumpTerm context term
+  putText ""
+  unless (HashMap.null context.equations.equal) $
+    putText "  where"
+  forM_ (HashMap.toList context.equations.equal) \(head_, argValues) ->
+    forM_ argValues \(args, eqValue) -> do
+      lhsTerm <- Readback.readback env (Domain.Neutral head_ $ Domain.Apps args)
+      rhsTerm <- Readback.readback env eqValue
+      putStr ("    " :: Text)
+      dumpTerm context lhsTerm
+      putStr (" = " :: Text)
+      dumpTerm context rhsTerm
+      putText ""
 
 toPrettyableTerm :: Context v -> Syntax.Term v -> M Error.PrettyableTerm
 toPrettyableTerm context term = do

src/Elaboration/Unification.hs

@@ -28,6 +28,7 @@ import {-# SOURCE #-} qualified Elaboration
 import Elaboration.Context (Context)
 import qualified Elaboration.Context as Context
 import Elaboration.Depth (compareHeadDepths)
+import qualified Elaboration.Equation as Equation
 import qualified Elaboration.Meta as Meta
 import qualified Environment
 import qualified Error
@@ -355,8 +356,13 @@ withConstructorBranch
 withConstructorBranch context env head args constr constrArgs tele k =
   case tele of
     Telescope.Empty _ -> do
-      let context' = Context.defineWellOrdered context head args $ Domain.Con constr constrArgs
-      k context'
+      let constrValue = Domain.Con constr constrArgs
+      context' <- case constrValue of
+        Builtin.Refl _ value1 value2 ->
+          Equation.equate context Flexibility.Rigid value1 value2
+        _ -> pure context
+      let context'' = Context.defineWellOrdered context' head args $ Domain.Con constr constrArgs
+      k context''
     Telescope.Extend bindings type_ plicity tele' -> do
       type' <- Evaluation.evaluate env type_
       (context', var) <- Context.extend context (Bindings.toName bindings) type'