From ff65d1e285a97295708899bebdcc83ec214cd347 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 7 Jan 2023 21:10:30 +0000 Subject: Add containers types. Containers are syntactic sugar. They are also completely untested. --- src/Obs/Abstract.idr | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'src/Obs/Abstract.idr') diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr index 4ef3f43..25c4210 100644 --- a/src/Obs/Abstract.idr +++ b/src/Obs/Abstract.idr @@ -67,6 +67,28 @@ abstractSyntax ctx (First {arg}) = do abstractSyntax ctx (Second {arg}) = do arg <- abstractSyntaxBounds ctx arg pure (Second {arg}) +abstractSyntax ctx (Container {input, output, shapeSort, positionSort}) = do + input <- abstractSyntaxBounds ctx input + output <- abstractSyntaxBounds ctx output + pure (Container {input, output, shapeSort, positionSort}) +abstractSyntax ctx (MkContainer {shape, position, next}) = do + shape <- abstractSyntaxBounds ctx shape + position <- abstractSyntaxBounds ctx position + next <- abstractSyntaxBounds ctx next + pure (MkContainer {shape, position, next}) +abstractSyntax ctx (Shape {arg}) = do + arg <- abstractSyntaxBounds ctx arg + pure (Shape {arg}) +abstractSyntax ctx (Position {arg}) = do + arg <- abstractSyntaxBounds ctx arg + pure (Position {arg}) +abstractSyntax ctx (Next {arg}) = do + arg <- abstractSyntaxBounds ctx arg + pure (Next {arg}) +abstractSyntax ctx (Sem {pred, arg}) = do + pred <- abstractLambda ctx pred + arg <- abstractSyntaxBounds ctx arg + pure (Sem {pred, arg}) abstractSyntax ctx Bool = pure Bool abstractSyntax ctx True = pure True abstractSyntax ctx False = pure False -- cgit v1.2.3