Add box types.

8 files changed, 100 insertions, 0 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 16b0c92..94b208c 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -98,6 +98,15 @@ abstractSyntax ctx (If {returnType, discriminant, true, false}) = do
   true <- abstractSyntaxBounds ctx true
   false <- abstractSyntaxBounds ctx false
   pure (If {returnType, discriminant, true, false})
+abstractSyntax ctx (Box {prop}) = do
+  prop <- abstractSyntaxBounds ctx prop
+  pure (Box {prop})
+abstractSyntax ctx (MkBox {arg}) = do
+  arg <- abstractSyntaxBounds ctx arg
+  pure (MkBox {arg})
+abstractSyntax ctx (Unbox {arg}) = do
+  arg <- abstractSyntaxBounds ctx arg
+  pure (Unbox {arg})
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index d325f1a..b290240 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -49,6 +49,8 @@ data Constructor : Unsorted.Family Relevance where
   Bool : Constructor ctx
   True : Constructor ctx
   False : Constructor ctx
+  Box : (prop : TypeNormalForm ctx) -> Constructor ctx
+  MkBox : Constructor ctx
   Top : Constructor ctx
   Bottom : Constructor ctx
 
@@ -139,6 +141,8 @@ prettyPrecCnstr d (Pair {indexRel, elementRel, prf, first, second}) =
 prettyPrecCnstr d Bool = pretty "Bool"
 prettyPrecCnstr d True = pretty "True"
 prettyPrecCnstr d False = pretty "False"
+prettyPrecCnstr d (Box {prop}) = prettyApp d (pretty "Box") [prettyPrec App prop]
+prettyPrecCnstr d MkBox = pretty "box"
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
@@ -224,6 +228,8 @@ renameCnstr (Pair {indexRel, elementRel, prf, first, second}) f =
 renameCnstr Bool f = Bool
 renameCnstr True f = True
 renameCnstr False f = False
+renameCnstr (Box {prop}) f = Box {prop = rename prop f}
+renameCnstr MkBox f = MkBox
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
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
 
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index c1bd468..e59b2d7 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -40,6 +40,9 @@ data ObsTokenKind
   | OTPosition
   | OTNextIndex
   | OTExtension
+  | OTBox
+  | OTMkBox
+  | OTUnbox
   | OTAbsurd
   | OTRefl
   | OTTransp
@@ -91,6 +94,9 @@ Eq ObsTokenKind where
   OTPosition == OTPosition = True
   OTNextIndex == OTNextIndex = True
   OTExtension == OTExtension = True
+  OTBox == OTBox = True
+  OTMkBox == OTMkBox = True
+  OTUnbox == OTUnbox = True
   OTAbsurd == OTAbsurd = True
   OTRefl == OTRefl = True
   OTTransp == OTTransp = True
@@ -144,6 +150,9 @@ Show ObsTokenKind where
   show OTPosition = "Position"
   show OTNextIndex = "nextIndex"
   show OTExtension = "extension"
+  show OTBox = "Box"
+  show OTMkBox = "box"
+  show OTUnbox = "unbox"
   show OTAbsurd = "absurd"
   show OTRefl = "refl"
   show OTTransp = "transp"
@@ -199,6 +208,9 @@ TokenKind ObsTokenKind where
   tokValue OTPosition s = ()
   tokValue OTNextIndex s = ()
   tokValue OTExtension s = ()
+  tokValue OTBox s = ()
+  tokValue OTMkBox s = ()
+  tokValue OTUnbox s = ()
   tokValue OTAbsurd s = ()
   tokValue OTRefl s = ()
   tokValue OTTransp s = ()
@@ -256,6 +268,9 @@ keywords =
   , ("Position", OTPosition)
   , ("nextIndex", OTNextIndex)
   , ("extension", OTExtension)
+  , ("Box", OTBox)
+  , ("box", OTMkBox)
+  , ("unbox", OTUnbox)
   , ("absurd", OTAbsurd)
   , ("refl", OTRefl)
   , ("transp", OTTransp)
@@ -321,6 +336,9 @@ headForms =
   , (OTShape, (0 ** Shape))
   , (OTPosition, (0 ** Position))
   , (OTNextIndex, (0 ** Next))
+  , (OTBox, (0 ** Box))
+  , (OTMkBox, (0 ** MkBox))
+  , (OTUnbox, (0 ** Unbox))
   , (OTAbsurd, (0 ** Absurd))
   , (OTRefl, (0 ** Refl))
   , (OTTransp, (4 ** Transp))
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index ea7772e..bab23ac 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -52,6 +52,10 @@ data Syntax : Type where
   True : Syntax
   False : Syntax
   If : (returnType : LambdaForm) -> (discriminant, true, false : WithBounds Syntax) -> Syntax
+  -- Box Types
+  Box : (prop : WithBounds Syntax) -> Syntax
+  MkBox : (arg : WithBounds Syntax) -> Syntax
+  Unbox : (arg : WithBounds Syntax) -> Syntax
   -- True
   Top : Syntax
   Point : Syntax
@@ -119,6 +123,9 @@ prettyPrec d (Position {arg}) = prettyApp d (pretty "Position") [prettyPrecBound
 prettyPrec d (Next {arg}) = prettyApp d (pretty "nextIndex") [prettyPrecBounds App arg]
 prettyPrec d (Sem {pred, arg}) =
   prettyApp d (pretty "extension") [prettyPrecLambda App pred, prettyPrecBounds App arg]
+prettyPrec d (Box {prop}) = prettyApp d (pretty "Box") [prettyPrecBounds App prop]
+prettyPrec d (MkBox {arg}) = prettyApp d (pretty "box") [prettyPrecBounds App arg]
+prettyPrec d (Unbox {arg}) = prettyApp d (pretty "unbox") [prettyPrecBounds App arg]
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 8829038..8f03b5d 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -62,6 +62,10 @@ data Term : Nat -> Type where
   If : (returnType : LambdaForm n) ->
     (discriminant, true, false : WithBounds (Term n)) ->
     Term n
+  -- Box Types
+  Box : (prop : WithBounds (Term n)) -> Term n
+  MkBox : (arg : WithBounds (Term n)) -> Term n
+  Unbox : (arg : WithBounds (Term n)) -> Term n
   -- True
   Top : Term n
   Point : Term n
@@ -145,6 +149,9 @@ prettyPrec d (If {returnType, discriminant, true, false}) =
   , prettyPrecBounds App true
   , prettyPrecBounds App false
   ]
+prettyPrec d (Box {prop}) = prettyApp d (pretty "Box") [prettyPrecBounds App prop]
+prettyPrec d (MkBox {arg}) = prettyApp d (pretty "box") [prettyPrecBounds App arg]
+prettyPrec d (Unbox {arg}) = prettyApp d (pretty "unbox") [prettyPrecBounds App arg]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 50c4824..2a6aeaa 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -159,6 +159,15 @@ check' ctx sort type (MkContainer {shape, position, next}) = do
     , next
     }
 
+check' ctx (Set 0) (Cnstr (Box {prop})) (MkBox {arg}) = do
+  info "encountered box"
+
+  trace $ pretty {ann} "checking argument has type" <++> pretty prop
+  Irrel <- check ctx Prop prop arg
+  trace "argument is well typed"
+
+  pure (Cnstr MkBox)
+
 check' ctx sort type (Absurd {contradiction}) = do
   info "encountered absurd"
 
@@ -478,6 +487,34 @@ infer' ctx (If {returnType = MkLambda var returnType, discriminant, true, false}
 
     pure (returnSort ** (returnType, returnValue))
 
+infer' ctx (Box {prop}) = do
+  info "encountered Box"
+
+  trace "checking prop is a proposition"
+  prop <- check ctx (Set 0) (Cnstr (Universe Prop)) prop
+  trace "prop is well typed"
+
+  pure (Set 1 ** (cast (Set 0), Cnstr $ Box {prop}))
+
+infer' ctx (MkBox {arg}) = do
+  info "encountered box"
+
+  (Prop ** (prop, Irrel)) <- infer ctx arg
+    | (sort ** (type, _)) => universeMismatch (pretty "Prop") (pretty sort)
+
+  pure (Set 0 ** (Cnstr $ Box {prop}, Cnstr MkBox))
+
+infer' ctx (Unbox {arg}) = do
+  info "encountered unbox"
+
+  (sort ** (type, arg)) <- infer ctx arg
+  trace $ pretty {ann} "argument type is" <++> pretty type
+
+  let Cnstr (Box {prop}) = type
+    | _ => typeMismatch (pretty "box") (pretty type)
+
+  pure (Prop ** (prop, Irrel))
+
 infer' ctx Top = do
     info "encountered top"
     pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Top))
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index 28a3c18..0e65790 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -105,6 +105,9 @@ convertCnstr
 convertCnstr Bool Bool = pure True
 convertCnstr True True = pure True
 convertCnstr False False = pure True
+convertCnstr (Box {prop}) (Box {prop = prop'}) =
+  convert {rel = Relevant, type = cast Prop, left = prop, right = prop'}
+convertCnstr MkBox MkBox = pure True
 convertCnstr Top Top = pure True
 convertCnstr Bottom Bottom = pure True
 convertCnstr left right = pure False
@@ -200,6 +203,7 @@ convertEta (Pair {indexRel = Relevant, elementRel = Irrelevant, prf, first, seco
 convertEta (Pair {indexRel = Irrelevant, elementRel = Relevant, prf, first, second}) right = do
   let rightSecond = Second {firstRel = Relevant, arg = right}
   convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond}
+convertEta MkBox right = pure True
 convertEta left right = pure False
 
 convertUntyped Irrelevant left right = pure True