diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-07 21:10:30 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-07 21:58:30 +0000 |
| commit | ff65d1e285a97295708899bebdcc83ec214cd347 (patch) | |
| tree | 7a786ef895ff2dea0ba31b3c7cd7397024214a10 /src/Obs/Term.idr | |
| parent | f38761fd38207a6d9a6cc2134384cb7115a5e998 (diff) | |
Add containers types.
Containers are syntactic sugar. They are also completely untested.
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" |