diff options
Diffstat (limited to 'src/Obs/Term.idr')
| -rw-r--r-- | src/Obs/Term.idr | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr index 8dad72c..5126d99 100644 --- a/src/Obs/Term.idr +++ b/src/Obs/Term.idr @@ -44,6 +44,15 @@ data Term : Nat -> Type where Pair : (first, second : WithBounds (Term n)) -> Term n First : (arg : WithBounds (Term n)) -> Term n Second : (arg : WithBounds (Term n)) -> Term n + -- Containers + Container : (input, output : WithBounds (Term n)) -> + (shapeSort, positionSort : WithBounds Universe) -> + Term n + MkContainer : (shape, position, next : WithBounds (Term n)) -> Term n + Shape : (arg : WithBounds (Term n)) -> Term n + Position : (arg : WithBounds (Term n)) -> Term n + Next : (arg : WithBounds (Term n)) -> Term n + Sem : (pred : LambdaForm n) -> (arg : WithBounds (Term n)) -> Term n -- Booleans Bool : Term n True : Term n @@ -99,6 +108,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" |