{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Servant.GDP.ProveInIsolation (ProvableInIsolation, proveInIsolation) where

import Data.Text (Text)
import GDP (Proof, introAnd, introOrL, introOrR, (...), type (&&), type (:::), type (||), type (~~))
import Servant
  ( FromHttpApiData,
    parseUrlPiece,
  )

-- | Check if property P holds for value a or not.
-- Is used to parse a value from the request with a required proof
class ProvableInIsolation a p where
  proveInIsolation :: a -> Either Text (Proof p)

instance (ProvableInIsolation a p1, ProvableInIsolation a p2) => ProvableInIsolation a (p1 && p2) where
  proveInIsolation :: a -> Either Text (Proof (p1 && p2))
proveInIsolation a
x = do
    Proof p1
p1 <- a -> Either Text (Proof p1)
forall a p. ProvableInIsolation a p => a -> Either Text (Proof p)
proveInIsolation a
x
    Proof p2
p2 <- a -> Either Text (Proof p2)
forall a p. ProvableInIsolation a p => a -> Either Text (Proof p)
proveInIsolation a
x
    Proof (p1 && p2) -> Either Text (Proof (p1 && p2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof (p1 && p2) -> Either Text (Proof (p1 && p2)))
-> Proof (p1 && p2) -> Either Text (Proof (p1 && p2))
forall a b. (a -> b) -> a -> b
$ Proof p1 -> Proof p2 -> Proof (p1 && p2)
forall k1 k2 (p :: k1) (q :: k2).
Proof p -> Proof q -> Proof (p && q)
introAnd Proof p1
p1 Proof p2
p2

instance (ProvableInIsolation a p1, ProvableInIsolation a p2) => ProvableInIsolation a (p1 || p2) where
  proveInIsolation :: a -> Either Text (Proof (p1 || p2))
proveInIsolation a
x = do
    case (a -> Either Text (Proof p1)
forall a p. ProvableInIsolation a p => a -> Either Text (Proof p)
proveInIsolation a
x, a -> Either Text (Proof p2)
forall a p. ProvableInIsolation a p => a -> Either Text (Proof p)
proveInIsolation a
x) of
      (Right Proof p1
p1, Either Text (Proof p2)
_) -> Proof (p1 || p2) -> Either Text (Proof (p1 || p2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof (p1 || p2) -> Either Text (Proof (p1 || p2)))
-> Proof (p1 || p2) -> Either Text (Proof (p1 || p2))
forall a b. (a -> b) -> a -> b
$ Proof p1 -> Proof (p1 || p2)
forall k1 k2 (p :: k1) (q :: k2). Proof p -> Proof (p || q)
introOrL Proof p1
p1
      (Either Text (Proof p1)
_, Right Proof p2
p2) -> Proof (p1 || p2) -> Either Text (Proof (p1 || p2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof (p1 || p2) -> Either Text (Proof (p1 || p2)))
-> Proof (p1 || p2) -> Either Text (Proof (p1 || p2))
forall a b. (a -> b) -> a -> b
$ Proof p2 -> Proof (p1 || p2)
forall k1 k2 (q :: k1) (p :: k2). Proof q -> Proof (p || q)
introOrR Proof p2
p2
      (Left Text
e1, Left Text
e2) -> Text -> Either Text (Proof (p1 || p2))
forall a b. a -> Either a b
Left (Text -> Either Text (Proof (p1 || p2)))
-> Text -> Either Text (Proof (p1 || p2))
forall a b. (a -> b) -> a -> b
$ Text
e1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e2

instance
  ( FromHttpApiData (a ~~ n),
    FromHttpApiData a,
    ProvableInIsolation (a ~~ n) p
  ) =>
  FromHttpApiData (a ~~ n ::: p)
  where
  parseUrlPiece :: Text -> Either Text ((a ~~ n) ::: p)
parseUrlPiece Text
t =
    do
      (a ~~ n
j :: a ~~ n) <- Text -> Either Text (a ~~ n)
forall a. FromHttpApiData a => Text -> Either Text a
parseUrlPiece Text
t
      (a ~~ n
j (a ~~ n) -> Proof p -> (a ~~ n) ::: p
forall a p. a -> Proof p -> a ::: p
...) (Proof p -> (a ~~ n) ::: p)
-> Either Text (Proof p) -> Either Text ((a ~~ n) ::: p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a ~~ n) -> Either Text (Proof p)
forall a p. ProvableInIsolation a p => a -> Either Text (Proof p)
proveInIsolation a ~~ n
j