From 9af1a41a58575508c8d2dff6e7b25a5caac8aadc Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 8 Jan 2023 00:56:11 +0000 Subject: Add box types. --- src/Obs/Syntax.idr | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Obs/Syntax.idr') 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" -- cgit v1.2.3