From f63bce39f2b995e1a5bf2c76c6029fa537be5acb Mon Sep 17 00:00:00 2001
From: Alessio Ferrarini <alessio.ferrarini@imdea.org>
Date: Thu, 19 Dec 2024 10:52:22 +0100
Subject: [PATCH] Add some new examples

---
 resources/custom/liquidhaskell/config.js      | 17 +++-
 .../custom/liquidhaskell/demos/Compiler.hs    | 97 +++++++++++++++++++
 resources/custom/liquidhaskell/demos/Cont.hs  | 34 +++++++
 resources/custom/liquidhaskell/demos/List.hs  | 60 ++++++++++++
 .../custom/liquidhaskell/demos/MapFusion.hs   | 54 +++++++++++
 .../custom/liquidhaskell/demos/Reader.hs      | 38 ++++++++
 6 files changed, 296 insertions(+), 4 deletions(-)
 create mode 100644 resources/custom/liquidhaskell/demos/Compiler.hs
 create mode 100644 resources/custom/liquidhaskell/demos/Cont.hs
 create mode 100644 resources/custom/liquidhaskell/demos/List.hs
 create mode 100644 resources/custom/liquidhaskell/demos/MapFusion.hs
 create mode 100644 resources/custom/liquidhaskell/demos/Reader.hs

diff --git a/resources/custom/liquidhaskell/config.js b/resources/custom/liquidhaskell/config.js
index 1bfd8ac..5420e93 100644
--- a/resources/custom/liquidhaskell/config.js
+++ b/resources/custom/liquidhaskell/config.js
@@ -26,10 +26,11 @@ var showErrorBanners = false;
  
 /************** List of Demos **************************************************/
 
-var allCategories = [ { type : "basic"    , name: "Basics" }
-                    , { type : "measure"  , name: "Measures" }
-                    , { type : "absref"   , name: "Abstract Refinements" }
-                    , { type : "tutorial" , name: "HOPA Tutorial" }
+var allCategories = [ { type : "basic"      , name: "Basics" }
+                    , { type : "measure"    , name: "Measures" }
+                    , { type : "higherorder", name: "Higher Order" }
+                    , { type : "absref"     , name: "Abstract Refinements" }
+                    , { type : "tutorial"   , name: "HOPA Tutorial" }
                     ];
 
 var allDemos =
@@ -51,6 +52,14 @@ var allDemos =
     "UniqueZipper.hs"       : { name : "Unique Zippers"   , type : "measure"},
     "LambdaEval.hs"         : { name : "Lambda Eval"      , type : "measure"}, 
     "treesum.hs"            : { name : "List-Tree Sum"    , type : "measure"},
+
+    // Higher Order Demos
+    "MapFusion.hs"          : { name : "Map Fusion"        , type : "higherorder"},
+    "Reader.hs"             : { name : "Reader Monad"      , type : "higherorder"},
+    "List.hs"               : { name : "List Monad"        , type : "higherorder"},
+    "Cont.hs"               : { name : "Continutaion Monad", type : "higherorder"},
+    "Compiler.hs"           : { name : "Expr compiler"     , type : "higherorder"},
+
     // Abstract Refinement Demos
     "absref101.hs"          : { name : "Parametric Invariants", type : "absref" },
     "filter.hs"             : { name : "A Fine Filter"        , type : "absref" },
diff --git a/resources/custom/liquidhaskell/demos/Compiler.hs b/resources/custom/liquidhaskell/demos/Compiler.hs
new file mode 100644
index 0000000..08688b5
--- /dev/null
+++ b/resources/custom/liquidhaskell/demos/Compiler.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+
+{-@ LIQUID "--ple"           @-}
+{-@ LIQUID "--etabeta"       @-}
+{-@ LIQUID "--reflection"    @-}
+{-@ LIQUID "--dependantcase" @-}
+
+module Compiler where
+
+import Prelude hiding ((.))
+import Language.Haskell.Liquid.ProofCombinators
+
+{-@ reflect id @-}
+{-@ reflect $  @-}
+{-@ infix $    @-}
+
+{-@ reflect .  @-}
+{-@ infix .    @-}
+infixr 9 .
+(.) :: (b -> c) -> (a -> b) -> a -> c
+(.) f g x = f (g x)
+
+data Expr where
+  EConst :: Int -> Expr
+  EAdd   :: Expr -> Expr -> Expr
+  EMul   :: Expr -> Expr -> Expr
+  ENeg   :: Expr -> Expr
+
+{-@ reflect eval @-}
+eval :: Expr -> Int
+eval (EConst x) = x
+eval (EAdd e1 e2) = eval e1 + eval e2
+eval (EMul e1 e2) = eval e1 * eval e2
+eval (ENeg e)     = - (eval e)
+
+type Stack = [Int]
+
+data OpCode where
+  OpPush :: Int -> OpCode
+  OpAdd :: OpCode
+  OpMul :: OpCode
+  deriving Show
+
+
+{-@ reflect push @-}
+push :: Int -> Stack -> Stack
+push v s = v : s
+
+{-@ reflect execOpCode @-}
+{-@ execOpCode :: o:OpCode -> { v:Stack | len v >= minStackSize o } -> Stack @-}
+execOpCode :: OpCode -> Stack -> Stack
+execOpCode (OpPush x) = push x
+execOpCode OpAdd      = \case (x : y : xs) -> (y + x) : xs
+execOpCode OpMul      = \case (x : y : xs) -> (y * x) : xs
+
+{-@ reflect minStackSize @-}
+minStackSize :: OpCode -> Int
+minStackSize (OpPush x) = 0
+minStackSize _          = 2
+
+data Program where
+{-@ PNil :: Prop (Program id) @-}
+  PNil :: Program
+{-@ PCons :: op:OpCode
+          -> p:(Stack -> { v:Stack | len v >= minStackSize op }) -> Prop (Program p)
+          -> Prop (Program (execOpCode op . p)) @-}
+  PCons :: OpCode -> (Stack -> Stack) -> Program -> Program
+data PROGRAM = Program (Stack -> Stack)
+
+{-@ reflect compose @-}
+{-@ compose :: p1:(Stack -> Stack) -> p2:(Stack -> Stack)  
+            -> Prop (Program p1) -> Prop (Program p2)
+            -> Prop (Program (p2 . p1)) @-}
+compose :: (Stack -> Stack) -> (Stack -> Stack) -> Program -> Program -> Program
+compose s1 s2 p1 PNil                   = p1
+compose s1 s2 p1 (PCons cmd srest rest) =
+  PCons cmd (srest . s1) (compose s1 srest p1 rest)
+
+{-@ compile :: e:Expr -> Prop (Program (push $ eval e)) @-}
+compile :: Expr -> Program
+compile (EConst x)   = PCons (OpPush x) id PNil
+compile (EAdd e1 e2) =
+  PCons
+    OpAdd
+    ((push $ eval e1) . (push $ eval e2))
+    (compose (push $ eval e2) (push $ eval e1) (compile e2) (compile e1))
+compile (EMul e1 e2) =
+  PCons
+    OpMul
+    ((push $ eval e1) . (push $ eval e2))
+    (compose (push $ eval e2) (push $ eval e1) (compile e2) (compile e1))
+compile (ENeg e)     =
+  PCons
+    OpMul
+    ((push $ -1) . (push $ eval e))
+    (PCons (OpPush $ -1) (push $ eval e) (compile e))
\ No newline at end of file
diff --git a/resources/custom/liquidhaskell/demos/Cont.hs b/resources/custom/liquidhaskell/demos/Cont.hs
new file mode 100644
index 0000000..81e4a53
--- /dev/null
+++ b/resources/custom/liquidhaskell/demos/Cont.hs
@@ -0,0 +1,34 @@
+{-@ LIQUID "--reflection"                @-}
+{-@ LIQUID "--ple"                       @-}
+{-@ LIQUID "--etabeta"                   @-}
+
+module Cont where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+import Prelude hiding (return, (>>=))
+
+{-@ data Cont r a = Cont { runCont :: (a -> r) -> r } @-}
+data Cont r a     = Cont { runCont :: (a -> r) -> r }
+
+{-@ reflect return @-}
+return :: a -> Cont r a
+return x = Cont $ \k -> k x
+
+{-@ infix   >>= @-}
+{-@ reflect >>= @-}
+(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
+(Cont x) >>= f = Cont $ \k -> x (\a -> runCont (f a) k)
+
+{-@ leftIdentity :: x:a -> f:(a -> Cont r b) -> { return x >>= f = f x } @-}
+leftIdentity :: a -> (a -> Cont r b) -> Proof
+leftIdentity x f = case f x of Cont _ -> trivial
+
+{-@ rightIdentity :: x:Cont r a -> { (x >>= return) = x } @-}
+rightIdentity :: Cont r a -> Proof
+rightIdentity (Cont k) = trivial
+
+{-@ associativity :: x:Cont r a -> f:(a -> Cont r b) -> g:(b -> Cont r c)
+                  -> { (x >>= f) >>= g = x >>= (\r:a -> f r >>= g) } @-}
+associativity :: Cont r a -> (a -> Cont r b) -> (b -> Cont r c) -> Proof
+associativity (Cont k) f g = trivial
\ No newline at end of file
diff --git a/resources/custom/liquidhaskell/demos/List.hs b/resources/custom/liquidhaskell/demos/List.hs
new file mode 100644
index 0000000..009e3bc
--- /dev/null
+++ b/resources/custom/liquidhaskell/demos/List.hs
@@ -0,0 +1,60 @@
+{-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--ple"        @-}
+
+module List where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+import Prelude hiding (return, (>>=), (++))
+
+data List a = Nil | Cons a (List a)
+
+{-@ reflect return @-}
+return :: a -> List a
+return x = Cons x Nil
+
+{-@ infix   ++ @-}
+{-@ reflect ++ @-}
+(++) :: List a -> List a -> List a
+Nil         ++ ys = ys
+(Cons x xs) ++ ys = x `Cons` (xs ++ ys)
+
+{-@ infix   >>= @-}
+{-@ reflect >>= @-}
+(>>=) :: List a -> (a -> List b) -> List b
+Nil         >>= _ = Nil
+(Cons x xs) >>= f = f x ++ (xs >>= f)
+
+{-@ rightIdentity :: x:List a -> { x >>= return = x } @-}
+rightIdentity :: List a -> Proof
+rightIdentity Nil         = trivial
+rightIdentity (Cons x xs) = rightIdentity xs
+
+{-@ appendIdR :: xs:List a -> { xs ++ Nil = xs } @-}
+appendIdR :: List a -> Proof
+appendIdR Nil         = trivial
+appendIdR (Cons x xs) = appendIdR xs
+
+{-@ leftIdentity :: x:a -> f:(a -> List b) -> { return x >>= f = f x } @-}
+leftIdentity :: a -> (a -> List b) -> Proof
+leftIdentity x f = appendIdR $ f x
+
+{-@ appendAssoc :: xs:List a -> ys:List a -> zs:List a
+                -> { (xs ++ ys) ++ zs = xs ++ (ys ++ zs) } @-}
+appendAssoc :: List a -> List a -> List a -> Proof
+appendAssoc Nil         ys zs = trivial
+appendAssoc (Cons x xs) ys zs = appendAssoc xs ys zs
+
+{-@ rightDistributive :: xs:List a -> ys:List a -> f:(a -> List b)
+                      -> { xs ++ ys >>= f = (xs >>= f) ++ (ys >>= f) } @-}
+rightDistributive :: List a -> List a -> (a -> List b) -> Proof
+rightDistributive Nil         ys f = trivial
+rightDistributive (Cons x xs) ys f = rightDistributive xs ys f 
+                                 &&& appendAssoc (f x) (xs >>= f) (ys >>= f)
+
+{-@ associativity :: x:List a -> f:(a -> List a) -> g:(a -> List a) 
+                  -> { (x >>= f) >>= g = x >>= (\r:a -> f r >>= g) } @-}
+associativity :: List a -> (a -> List a) -> (a -> List a) -> Proof
+associativity Nil         _ _ = trivial
+associativity (Cons x xs) f g = associativity xs f g 
+                            &&& rightDistributive (f x) (xs >>= f) g
diff --git a/resources/custom/liquidhaskell/demos/MapFusion.hs b/resources/custom/liquidhaskell/demos/MapFusion.hs
new file mode 100644
index 0000000..975b89e
--- /dev/null
+++ b/resources/custom/liquidhaskell/demos/MapFusion.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE RankNTypes #-}
+
+{-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--ple"        @-}
+{-@ LIQUID "--etabeta"    @-}
+
+module MapFusion where
+
+import Prelude hiding (map, foldr)
+import Language.Haskell.Liquid.ProofCombinators
+
+-- When we allow the parser to accept : in refinements this wont be needed
+{-@ reflect append @-}
+append :: a -> [a] -> [a]
+append = (:)
+
+{-@ reflect map @-}
+map :: (a -> b) -> [a] -> [b]
+map _ []     = []
+map f (x:xs) = f x : map f xs
+
+{-@ reflect foldr @-}
+foldr :: (a -> b -> b) -> b -> [a] -> b
+foldr _ e []     = e
+foldr f e (x:xs) = f x (foldr f e xs)
+
+{-@ reflect build @-}
+build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
+build g = g (:) []
+
+{-@ reflect mapFB @-}
+mapFB :: forall elt lst a . (elt -> lst -> lst) -> (a -> elt) -> a -> lst -> lst
+mapFB c f = \x ys -> c (f x) ys
+
+
+{-@ rewriteMapList :: f:_ -> b:_ -> { foldr (mapFB append f) [] b = map f b } @-}
+rewriteMapList :: (a -> b) -> [a] -> ()
+rewriteMapList f []     = trivial
+rewriteMapList f (x:xs) = trivial ? (rewriteMapList f xs)
+
+{-@ rewriteMapFB :: c:_ -> f:_ -> g:_ -> { mapFB (mapFB c f) g = mapFB c (f . g) } @-}
+rewriteMapFB :: (a -> b -> b) -> (c -> a) -> (d -> c) -> Proof
+rewriteMapFB c f g = trivial
+
+{-@ rewriteMapFBid :: c:(a -> b -> b) -> { mapFB c (\x:a -> x) = c } @-}
+rewriteMapFBid :: (a -> b -> b) -> ()
+rewriteMapFBid c = trivial
+
+{-@ rewriteMap :: f:(a1 -> a2) -> xs:[a1] 
+               -> { build (\c:func(1, [a2, @(0), @(0)]) -> \n:@(0) -> foldr (mapFB c f) n xs) 
+                  = map f xs } @-}
+rewriteMap :: (a1 -> a2) -> [a1] -> ()
+rewriteMap f []     = trivial
+rewriteMap f (x:xs) = trivial ? rewriteMap f xs
diff --git a/resources/custom/liquidhaskell/demos/Reader.hs b/resources/custom/liquidhaskell/demos/Reader.hs
new file mode 100644
index 0000000..a255285
--- /dev/null
+++ b/resources/custom/liquidhaskell/demos/Reader.hs
@@ -0,0 +1,38 @@
+{-@ LIQUID "--reflection"                @-}
+{-@ LIQUID "--ple"                       @-}
+{-@ LIQUID "--etabeta"                   @-}
+
+module Reader where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+import Prelude hiding (return, (>>=))
+
+{-@ data Reader r a = Reader { runReader :: r -> a } @-}
+data Reader r a     = Reader { runReader :: r -> a }
+
+{-@ reflect return @-}
+return :: a -> Reader r a
+return x = Reader $ \y -> x
+
+{-@ infix   >>= @-}
+{-@ reflect >>= @-}
+(>>=) :: Reader r a -> (a -> Reader r b) -> Reader r b
+(Reader x) >>= f = Reader $ \r -> runReader (f $ x r) r
+
+{-@ readerId :: f:(Reader r a) -> { f = Reader (runReader f) } @-} 
+readerId :: (Reader r a) -> Proof 
+readerId (Reader _) = trivial
+
+{-@ rightIdentity :: x:Reader r a -> { x >>= return = x } @-}
+rightIdentity :: Reader r a -> Proof
+rightIdentity (Reader _) = trivial
+
+{-@ associativity :: x:Reader r a -> f:(a -> Reader r a) -> g:(a -> Reader r a) 
+                  -> { (x >>= f) >>= g = x >>= (\r:a -> f r >>= g) } @-}
+associativity :: Reader r a -> (a -> Reader r a) -> (a -> Reader r a) -> Proof
+associativity (Reader _) _ _ = trivial
+
+{-@ leftIdentity :: x:a -> f:(a -> Reader r b) -> { return x >>= f = f x } @-}
+leftIdentity :: a -> (a -> Reader r b) -> Proof
+leftIdentity x f = case f x of Reader _ -> trivial
\ No newline at end of file