diff options
Diffstat (limited to 'src/Obs/NormalForm')
| -rw-r--r-- | src/Obs/NormalForm/Normalise.idr | 12 |
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 |