X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FDemo.hs;h=fb8666f659c2fec0b3c14785d5d7ef9bd3f93d0f;hp=579bf4d2045d3c96cadce209cabb07b5f67d17e6;hb=c700f5a65d664d4c0a3e76d33aa3769266bf330c;hpb=9238cdac094f9be01ee8978ddb18b6404a6d9ade

diff --git a/examples/Demo.hs b/examples/Demo.hs
index 579bf4d..fb8666f 100644
--- a/examples/Demo.hs
+++ b/examples/Demo.hs
@@ -1,21 +1,33 @@
 {-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables -fsimpleopt-before-flatten #-}
-module Demo (demo) where
+module Demo ({-sample1,sample2,-}sample5,sample6) where
 
-
-demo const mult =
+sample5 :: forall c . (Int -> <{Int}>@c) ->  <{Int -> Int -> Int}>@c -> <{Int -> Int}>@c
+sample5 const <[ (*) ]> =
  <{ \y ->
-    let   foo  = ~~mult (~~mult foo (~~mult y foo)) (~~mult y ~~(const 3))
+    let   foo  = (~~(const 3) * foo) * y
     in    foo }>
 
+sample6 :: forall c . (Int -> <{Int}>@c) -> <{Int -> Int -> Int}>@c -> <{Int -> Int}>@c
+sample6 const <{ (*) }> = pow 6
+   where
+     --pow :: Int -> <{ Int -> Int }>@a
+     pow 0 = <{ \x -> ~~(const 1) }>
+     pow 1 = <{ \x -> x }>
+     pow n = <{ \x -> x * ~~(pow (n - 1)) x }>
 
-{-
-demo const mult =
+demo2 ::
+    forall c . 
+         (Int -> <{Int}>@c) -> 
+        <{Int -> Int -> Int}>@c ->
+        <{Int -> Int}>@c
+
+demo2 const mult =
   <{ \y ->
      ~~mult
        (~~(const 1))
        (~~mult y y)
    }>
--}
+
 
 
 
@@ -144,11 +156,6 @@ demo const mult =
       in  four
     }>
 -}
-demo ::
-    forall c . 
-         (Int -> <{Int}>@c) -> 
-        <{Int -> Int -> Int}>@c ->
-        <{Int -> Int}>@c
 
 {-
 demo const mult =