-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathOneArg.hs
48 lines (36 loc) · 1.43 KB
/
OneArg.hs
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
44
45
46
47
48
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Main where
import Data.Generic.Diff
data OneArg = None | One Int
-- The second step is creating the family datatype. Each constructor
-- in the datatypes above gets a constructor in a family GADT:
data OneArgFamily :: * -> * -> * where
None' :: OneArgFamily OneArg Nil
One' :: OneArgFamily OneArg (Cons Int Nil)
Int' :: Int -> OneArgFamily Int Nil
instance Family OneArgFamily where
decEq None' None' = Just (Refl, Refl)
decEq One' One' = Just (Refl, Refl)
decEq (Int' i) (Int' j) | i == j = Just (Refl, Refl)
| otherwise = Just (Refl, Refl)
decEq _ _ = Nothing
fields None' None = Just CNil
fields One' (One i) = Just (CCons i CNil)
fields (Int' _) _ = Just CNil
fields _ _ = Nothing
apply None' CNil = None
apply One' (CCons i CNil) = One i
apply (Int' i) CNil = i
string None' = "None"
string One' = "One"
string (Int' i) = show i
instance Type OneArgFamily OneArg where
constructors = [ Concr None'
, Concr One'
]
instance Type OneArgFamily Int where
constructors = [ Abstr Int' ]
test :: EditScript OneArgFamily OneArg OneArg
test = diff None (One 1)