diff options
Diffstat (limited to 'src/Obs/Syntax.idr')
| -rw-r--r-- | src/Obs/Syntax.idr | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr index 74e15c2..868e761 100644 --- a/src/Obs/Syntax.idr +++ b/src/Obs/Syntax.idr @@ -38,6 +38,15 @@ data Syntax : Type where Pair : (first, second : WithBounds Syntax) -> Syntax First : (arg : WithBounds Syntax) -> Syntax Second : (arg : WithBounds Syntax) -> Syntax + -- Containers + Container : (input, output : WithBounds Syntax) -> + (shapeSort, positionSort : WithBounds Universe) -> + Syntax + MkContainer : (shape, position, next : WithBounds Syntax) -> Syntax + Shape : (arg : WithBounds Syntax) -> Syntax + Position : (arg : WithBounds Syntax) -> Syntax + Next : (arg : WithBounds Syntax) -> Syntax + Sem : (pred : LambdaForm) -> (arg : WithBounds Syntax) -> Syntax -- Booleans Bool : Syntax True : Syntax @@ -86,6 +95,24 @@ prettyPrec d (Pair {first, second}) = prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second) prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg] prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg] +prettyPrec d (Container {input, output, shapeSort, positionSort}) = + prettyApp d (pretty "Container") $ + [ prettyPrecBounds App input + , prettyPrecBounds App output + , prettyPrec App shapeSort.val + , prettyPrec App positionSort.val + ] +prettyPrec d (MkContainer {shape, position, next}) = + prettyApp d (pretty "MkContainer") $ + [ prettyPrecBounds App shape + , prettyPrecBounds App position + , prettyPrecBounds App next + ] +prettyPrec d (Shape {arg}) = prettyApp d (pretty "Shape") [prettyPrecBounds App arg] +prettyPrec d (Position {arg}) = prettyApp d (pretty "Position") [prettyPrecBounds App arg] +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 Bool = pretty "Bool" prettyPrec d True = pretty "True" prettyPrec d False = pretty "False" |