examples/Demo.hs

   1 {-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables -fsimpleopt-before-flatten #-}
   2 module Demo (demo) where
   3
   4
   5 demo const mult =
   6  <{ \y ->
   7     let   foo  = ~~mult (~~mult foo (~~mult y foo)) (~~mult y ~~(const 3))
   8     in    foo }>
   9
  10
  11 {-
  12 demo const mult =
  13   <{ \y ->
  14      ~~mult
  15        (~~(const 1))
  16        (~~mult y y)
  17    }>
  18 -}
  19
  20
  21
  22
  23
  24
  25 {-
  26 demo const mult =
  27   <{ \y ->
  28      ~~mult
  29        (~~mult (~~mult y y) (~~mult y y))
  30        (~~mult (~~mult y y) (~~mult y y))
  31    }>
  32 -}
  33
  34
  35
  36 {-
  37 demo const mult =
  38     <{ \y -> ~~(foo 4) }>
  39         where
  40           foo 0 = const (12::Int)
  41           foo n = <{ let bar = ~~(foo (n-1))
  42                      in ~~mult bar bar
  43                    }>
  44
  45 -}
  46
  47
  48
  49 {-
  50 demo const mult =
  51     <{ \y -> ~~(foo 3) }>
  52         where
  53           foo 0 = const (12::Int)
  54           foo n = <{ let recurs = ~~(foo (n-1))
  55                      in  ~~mult recurs recurs
  56                    }>
  57
  58 -}
  59
  60
  61
  62
  63
  64
  65
  66
  67
  68
  69
  70
  71
  72
  73
  74 {-
  75 demo const mult =
  76     <{ \y -> ~~(foo 2 <{y}>) }>
  77         where
  78           foo 0 y = const (12::Int)
  79           foo n y = <{ let recurs = ~~(foo (n-1) y)
  80                        in  ~~mult recurs recurs
  81                      }>
  82 -}
  83
  84
  85
  86
  87
  88
  89
  90
  91
  92
  93
  94
  95
  96
  97
  98
  99
 100
 101
 102
 103
 104
 105
 106
 107
 108
 109
 110
 111
 112
 113
 114
 115
 116
 117
 118
 119
 120
 121
 122
 123
 124 -- demo const mult = <{ \(y::Int) -> ~~mult y ~~(const 12) }>
 125 -- demo' n = <{ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) }>
 126 -- golden
 127 {-
 128 demo const mult =
 129  <{ \y ->
 130     let   twelve  = ~~mult twelve y
 131     in    twelve }>
 132 -}
 133
 134 {-
 135 demo const mult =
 136    <{ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) }>
 137 -}
 138
 139 {-
 140 demo const mult =
 141    <{ \(y::Int) ->
 142       let four   = ~~mult four ~~(const  4)
 143 --          twelve = {- {- ~~mult four -}  ~~(const 12) -} four
 144       in  four
 145     }>
 146 -}
 147 demo ::
 148     forall c .
 149          (Int -> <{Int}>@c) ->
 150         <{Int -> Int -> Int}>@c ->
 151         <{Int -> Int}>@c
 152
 153 {-
 154 demo const mult =
 155  <{ let     twelve = ~~(const (12::Int))
 156     in let  four    = ~~(const (4::Int))
 157          in  ~~mult four twelve  }>
 158 -}
 159
 160 {-
 161 demo const mult = demo' 3
 162  where
 163   demo' 0 = const 12
 164   demo' 1 = const 12
 165   demo' n = <{ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) }>
 166 -}
 167
 168 -- BUG
 169 --demo const mult = <{ \y -> ~~(demo' 0) }>
 170 --  where
 171 --   demo' 0 = const 4
 172 --   demo' n = const 4