1 files changed, 37 insertions, 0 deletions
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))