blob: fb0e80603f87530042a360e431952241e56bd806 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Patch (qc_prim) where
import Data.Kind (Type)
class PrimPatch (prim :: Type -> Type -> Type)
class PrimPatch (PrimOf p) => PrimPatchBase p where
type PrimOf (p :: Type -> Type -> Type) :: Type -> Type -> Type
type TestGenerator thing gen = (forall t ctx . (forall xx yy . thing xx yy -> t) -> (gen ctx -> t))
type family ModelOf (patch :: Type -> Type -> Type) :: Type -> Type
data WithState s p x y = WithState {
_wsStartState :: s x
, _wsPatch :: p x y
, _wsEndState :: s y
}
arbitraryThing :: x -> TestGenerator thing (thing x)
arbitraryThing _ f p = f p
qc_prim :: forall prim x y .
(PrimPatch prim
, PrimOf prim ~ prim
) => prim x y -> [()]
qc_prim _ =
concat
[
patch_repo_properties (undefined :: prim x a) "arbitrary" arbitraryThing'
]
where arbitraryThing' = arbitraryThing (undefined :: a)
patch_repo_properties :: p x y -> String -> TestGenerator (WithState (ModelOf (PrimOf p)) p) gen -> [()]
patch_repo_properties _ _genname _gen = undefined
|
