Add box types.

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index a95e725..28d66da 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -443,6 +443,7 @@ doCastHelper
     , second = second'
     }
 doCastHelper Bool Bool value = pure value
+doCastHelper (Box {prop = _}) (Box {prop = _}) value = pure $ Cnstr MkBox
 doCastHelper oldType newType value = pure $ Ntrl $ CastStuck {oldType, newType, value}
 
 doCast Irrelevant oldType newType value = pure Irrel
@@ -570,6 +571,12 @@ equalHelper
     , element = returnElement
     }
 equalHelper Bool Bool = pure (Cnstr Top)
+equalHelper (Box {prop}) (Box {prop = prop'}) = doEqual
+  { rel = Relevant
+  , type = Cnstr (Universe Prop)
+  , left = prop
+  , right = prop'
+  }
 equalHelper left right = pure $ Ntrl $ EqualStuck {left, right}
 
 doEqualType : (left, right : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx
@@ -689,6 +696,7 @@ doEqual Relevant (Cnstr Bool) left right = do
   whenLeftTrue <- doIf right (Cnstr Top) (Cnstr Bottom)
   whenLeftFalse <- doIf right (Cnstr Bottom) (Cnstr Top)
   doIf left whenLeftTrue whenLeftFalse
+doEqual Relevant (Cnstr (Box {prop})) left right = pure (Cnstr Top)
 doEqual Relevant (Cnstr t) left right = inScope "wrong constructor for equal" $ fatal t
 
 substDecl : DeclForm ~|> Hom (LogNormalForm' ann) (LogDeclForm ann)
@@ -714,6 +722,10 @@ substCnstr (Pair {indexRel, elementRel, prf, first, second}) f = do
 substCnstr Bool f = pure Bool
 substCnstr True f = pure True
 substCnstr False f = pure False
+substCnstr (Box {prop}) f = do
+  prop <- subst' prop f
+  pure (Box {prop})
+substCnstr MkBox f = pure MkBox
 substCnstr Top f = pure Top
 substCnstr Bottom f = pure Bottom