X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FDemo.hs;h=fb8666f659c2fec0b3c14785d5d7ef9bd3f93d0f;hp=7a6aee8eaeec82b3aeecb7ba185a52d3ac42549f;hb=c700f5a65d664d4c0a3e76d33aa3769266bf330c;hpb=15696408ed7f683d0a6cc89f381867819a29c240

diff --git a/examples/Demo.hs b/examples/Demo.hs
index 7a6aee8..fb8666f 100644
--- a/examples/Demo.hs
+++ b/examples/Demo.hs
@@ -1,14 +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  = (~~(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 }>
+
+demo2 ::
+    forall c . 
+         (Int -> <{Int}>@c) -> 
+        <{Int -> Int -> Int}>@c ->
+        <{Int -> Int}>@c
+
+demo2 const mult =
   <{ \y ->
      ~~mult
-       (~~mult y y)
+       (~~(const 1))
        (~~mult y y)
    }>
--}
+
 
 
 
@@ -54,12 +73,6 @@ demo const mult =
 
 
 
-demo const mult =
- <{ \y ->
-    let   foo  = ~~mult (~~mult foo (~~mult y foo)) y
-    in    foo }>
-
-
 
 
 
@@ -143,11 +156,6 @@ demo const mult =
       in  four
     }>
 -}
-demo ::
-    forall c . 
-         (Int -> <{Int}>@c) -> 
-        <{Int -> Int -> Int}>@c ->
-        <{Int -> Int}>@c
 
 {-
 demo const mult =