Support watching a single file using the new FSNotify library; allow 'key...

Support watching a single file using the new FSNotify library; allow 'key export' and 'key import' to attach metadata

curly-core/src/Curly/Core.hs

@@ -22,9 +22,9 @@ import Definitive
 import Language.Format
 import Curly.Core.Documentation
 import Control.DeepSeq
-import IO.Filesystem ((</>),dropFileName)
+import IO.Filesystem ((</>),takeFileName,dropFileName)
 import IO.Network.Socket (PortNumber,connect,getAddrInfo)
-import System.Directory (createDirectoryIfMissing)
+import System.Directory (createDirectoryIfMissing,doesDirectoryExist)
 import System.Environment (lookupEnv)
 import qualified System.FSNotify as FSNotify
 import System.IO (openFile,IOMode(AppendMode),hSetBuffering,BufferMode(LineBuffering))
@@ -316,7 +316,11 @@ inotify :: FSNotify.WatchManager
 inotify = FSNotify.startManager^.thunk
 -- | Sets a watch on the given file, on the usual signals
 watchFile :: FilePath -> IO () -> IO (IO ())
-watchFile s f = FSNotify.watchTree inotify s (const True) (\_ -> f)
+watchFile s f = do
+  isD <- doesDirectoryExist s
+  if isD then
+    FSNotify.watchTree inotify s (const True) (\_ -> f)
+    else FSNotify.watchTree inotify (dropFileName s) (\p -> takeFileName (FSNotify.eventPath p) == takeFileName s) (\_ -> f)
 
 -- | A utility function that opens a client socket to the given server and port
 connectTo :: String -> PortNumber -> IO Handle

curly-core/src/Curly/Core/Library.hs

@@ -568,9 +568,9 @@ availableLibs = do
   conn <- readIORef libraryVCS
   ks <- getKeyStore
   allLibs <- for (ks^.ascList) $ \(kn,(_,k,_,m,_)) -> forkValue $ do
-    case m^.from i'Metadata.at "follow-branches" of
-      Just (Pure bs) -> do
-        let branches = words bs
+    case m^.from i'Metadata.at "branches" of
+      Just (Join bs) -> do
+        let branches = [b | (b,m) <- bs^.ascList, lookup ["follow"] m == Just (Pure "true")]
         for branches $ \b -> forkValue $ do
           mcomm <- getBranch conn (Just (Left (k,b)))
           maybe (return zero) (getCommit conn) mcomm

curly-core/src/Curly/Core/Security.hs

@@ -139,6 +139,7 @@ data Signed a = Signed a Signature
               deriving (Eq,Ord,Show,Generic)
 instance Serializable a => Serializable (Signed a)
 instance Format a => Format (Signed a)
+
 unsafeExtractSigned :: Signed a -> a
 unsafeExtractSigned (Signed a _) = a
 extractSignedBy :: Serializable a => PublicKey -> Signed a -> Maybe a
@@ -147,6 +148,9 @@ extractSignedBy pub (Signed a s) | isValidSignatureFrom pub s (serialize a) = Ju
 signValue :: (MonadIO m,Serializable a) => PrivateKey -> a -> m (Signed a)
 signValue priv a = Signed a <$> signBytes priv (serialize a)
 
+signedDatum :: Format a => PublicKey -> Parser Bytes (Signed a)
+signedDatum pub = datum >>= maybe zero return . extractSignedBy pub
+
 timingRef :: IORef Seconds
 timingRef = thunk $^ newIORef 0
 
@@ -216,7 +220,7 @@ modifyKeyStore m = liftIO $ while $ trylog (threadDelay 1000 >> return True) $ F
     -- This little trick keeps GHC from prematurely closing the handle
     -- when the parser reaches the end of the byte stream
     sz <- between (hSeek h SeekFromEnd 0) (hSeek h AbsoluteSeek 0) (hTell h)
-    oldFile <- take (fromIntegral sz) <$> readHBytes h
+    oldFile <- readHNBytes h (fromIntegral sz)
     let ks = fromMaybe zero (matches Just datum oldFile)
         ks' = m ks
         newFile = serialize ks'

curly-core/src/Curly/Core/VCS.hs

@@ -216,11 +216,14 @@ getBranch conn = deepBranch'
           StampedBranches _ bs <-
             liftIO $ case [ts | (_,pub',_,meta,_) <- toList ks
                               , pub==pub'
-                              , Just (Pure ts) <- [meta^.mat "branch-expiry".at [b]]] of
+                              , Just (Pure ts) <- [meta^.mat "branches".at [b,"update-period"],
+                                                   Just (Pure "1s")]] of
               (ts:_) -> do
                 htime <- modTime headFile
                 now <- currentTime
-                if htime >= Since (now - 60*read ts)
+                let Just t = matches Just (liftA2 (*) number (suffixes $ zip "smhdwMy" (scanl (*) 1 [1,60,60,24,7,4,12]))) ts
+                    suffixes l = foldr1 (<+?) [n <$ single c | (c,n) <- l]
+                if htime >= Since (now - t)
                   then readFormat headFile
                   else getRemoteBranches
               _ -> getRemoteBranches

curly/doc/style.scss

@@ -24,7 +24,7 @@ body { width: 100%; }
     body { width: 65%; }
 }
 
-body { margin: auto; font-family: 'Titillium Web'; line-height: 180%; }
+body { margin: auto; font-family: 'Titillium Web'; line-height: 180%; font-size: 120%; }
 p, div, body { font-family: 'Titillium Web'; }
 p { text-indent: 0.7em; margin-left: 1em; }
 article { margin-left: 1em; margin-right: 1em; }

curly/src/Curly/Session.hs

@@ -40,7 +40,7 @@ data ClientPacket = BannerRequest Bool
                   | CompleteRequest String
                   | EditResponse Bytes
                   | EndOfTransmission
-                  | PubkeyResponse (Maybe PublicKey)
+                  | PubkeyResponse (Maybe KeyInfo)
                   | KeyListResponse [(String,KeyFingerprint,Bool)]
                   deriving Generic
 instance Serializable ClientPacket where
@@ -326,7 +326,7 @@ yesOrNo p = until $ do
 
 
 commonServerRequest clt (EditRequest ext (l,c) b) = writeChan clt . EditResponse =<< localEdit ext (l,c) b
-commonServerRequest clt (PubkeyRequest name) = writeChan clt . PubkeyResponse =<< map (by l'2) . lookup name <$> getKeyStore
+commonServerRequest clt (PubkeyRequest name) = writeChan clt . PubkeyResponse =<< map (\(_,pub,_,meta,_) -> KeyInfo pub meta Nothing) . lookup name <$> getKeyStore
 commonServerRequest _ (CommandOutput out) = liftIOLog (serialWriteHBytes stdout out)
 commonServerRequest _ (CommandLog msg) = logMessage msg
 commonServerRequest _ (KeyGenRequest True str) = do

curly/src/Curly/Session/Commands.hs

@@ -5,7 +5,7 @@ module Curly.Session.Commands(
   withSessionState,withStyle,getSession,
 
   -- * Commands
-  KeyOps(..),Interactive,Command,commands,commandNames,
+  KeyInfo(..),KeyOps(..),Interactive,Command,commands,commandNames,
 
   -- * Parsers
   interactiveSession,
@@ -151,7 +151,7 @@ killCmd = withDoc killDoc $ True <$ if ?access >= Admin then liftIOWarn (?quitSe
 interactiveSession :: Interactive (IO () -> OpParser IO ())
 interactiveSession ack = while sessionLine
   where sessionLine = do
-          (ws,ln) <- intercept $ option' Nothing (map Just line)
+          (ws,ln) <- intercept $ option' Nothing (map Just cmdLine)
           case ln of
             Just end -> liftIO ack >> return (not end)
             Nothing -> do
@@ -159,18 +159,22 @@ interactiveSession ack = while sessionLine
               liftIOWarn $ when (any (not . isSpace) err) $ throw (toException $ CurlyParserException Nothing ws)
               liftIOLog ack
               return True
-        line = withMountain $ do
+
+        cmdLine = do
+          s <- remaining
+          cmd <- hspace >> many1' (satisfy (\c -> not (isSpace c || c=='\'')))
+          let onCurlyCmd = runStreamState (put s) >> codeLine
+          maybe onCurlyCmd snd (foldMap snd commands^.at cmd) <* hspace <* (eol+eoi)
+
+        codeLine = withMountain $ do
           (ws,ln) <- listen $ muteOnSuccess $ option' Nothing (Just <$> withSessionLib curlyLine)
           case ln of
             Just _ -> return False
-            Nothing -> guard (empty ws) >> cmdLine
+            Nothing -> guard (empty ws) >> parseCmd
+
         parseCmd = hspace >> do
           (n,e) <- withParsedString (optimized =<< accessorExpr HorizSpaces)
           lookingAt (hspace >> eol)
           withPatterns $ withStyle $ showExprDefault (docTag' "call" [Pure "show-default"]) n e
           return False
-        cmdLine = do
-          s <- remaining
-          cmd <- hspace >> many1' (satisfy (\c -> not (isSpace c || c=='\'')))
-          maybe (runStreamState (put s) >> parseCmd) snd (foldMap snd commands^.at cmd) <* hspace <* (eol+eoi)
 

curly/src/Curly/Session/Commands/Common.hs

@@ -108,12 +108,18 @@ withPatterns m = getSession patterns >>= \ps -> let ?patterns = ps in m
 getSession :: (?sessionState :: IORef SessionState,MonadIO m) => Lens' SessionState a -> m a
 getSession l = liftIO (readIORef ?sessionState <&> by l)
 
+data KeyInfo = KeyInfo PublicKey Metadata (Maybe PrivateKey)
+instance Serializable KeyInfo where
+  encode (KeyInfo x y z) = encode (x,z,y)
+instance Format KeyInfo where
+  datum = (\x y z -> KeyInfo x z y) <$> datum <*> datum <*> (datum <+? fill (Metadata zero) (remaining >>= guard . (==0) . bytesSize))
+
 data KeyOps = KeyOps {
-  opsGetKey :: String -> IO (Maybe PublicKey),
+  opsGetKey :: String -> IO (Maybe KeyInfo),
   opsKeyGen :: Bool -> String -> IO (),
   opsListKeys :: IO [(String,KeyFingerprint,Bool)]
   }
-clientKey ::(?clientOps :: KeyOps) => String -> IO (Maybe PublicKey)
+clientKey ::(?clientOps :: KeyOps) => String -> IO (Maybe KeyInfo)
 clientKey = opsGetKey ?clientOps
 clientKeyGen ::(?clientOps :: KeyOps) => Bool -> String -> IO ()
 clientKeyGen = opsKeyGen ?clientOps
@@ -144,8 +150,9 @@ absPath :: (?sessionState :: IORef SessionState, MonadParser s m p, ParseStream
 absPath lim = (single '.' >> symPath lim)
               <+? (liftA2 subPath (getSession wd) (symPath lim))
 
+
 data CurlyDNSQuery = DomainVC (WithResponse (String,PortNumber))
-                   | DomainKey String (WithResponse (Zesty PublicKey))
+                   | DomainKey String (WithResponse (Zesty KeyInfo))
 dns_lookup :: (MonadIO m,Read a) => (WithResponse a -> CurlyDNSQuery) -> m (Maybe a)
 dns_lookup k = liftIO $ do
   p <- curlyDataFileName "dns-lookup.sh"

curly/src/Curly/Session/Commands/Key.hs

@@ -9,7 +9,7 @@ import Curly.Core.Parser
 import Language.Format hiding (space)
 import Curly.Session.Commands.Common
 import Curly.UI
-
+  
 keyCmd :: Interactive Command
 
 keyDoc = [q_string|
@@ -29,7 +29,8 @@ keyDoc = [q_string|
     {li {em key import <key-name> (<client-key-name>|#<export>)}: Imports an exported key under the given name}}
 |]
 keyCmd = withDoc keyDoc $ False <$ do
-  x <- expected "key command" (nbhspace >> dirArg)
+  x <- nbhspace >> dirArg
+  
   let setKey name v = do
         ks <- getKeyStore
         guardWarn Sev_Error (format "the key '%s' already exists" name) (not (name`isKeyIn`ks)) 
@@ -81,8 +82,11 @@ keyCmd = withDoc keyDoc $ False <$ do
       name <- expected "key name" (nbhspace >> dirArg)
       ph:pt <- expected "metadata path"  (many1' (nbhspace >> dirArg))
       if ?access >= Almighty
-        then modifyKeyStore $ at name.t'Just.l'4.at ph %~ maybe Nothing (\m -> let m' = delete pt m in
-                                                                          if empty m' then Nothing else Just m')
+        then
+        let purge_empty (Join m) | empty m = Nothing
+                                 | otherwise = Just (Join $ foldr (\k -> warp (at k) (>>=purge_empty)) m (keys m))
+            purge_empty x = Just x
+        in modifyKeyStore $ at name.t'Just.l'4.at ph %~ maybe Nothing (purge_empty . delete pt)
         else serveStrLn "Error: you are not authorized to unset key metadata"
     "meta" -> do
       name <- expected "key name" (nbhspace >> dirArg)
@@ -101,20 +105,22 @@ keyCmd = withDoc keyDoc $ False <$ do
       proof <- option' False (nbhspace >> True<$several "proof")
       v <- lookup name <$> getKeyStore
       case v of
-        Just (_,pub,priv,meta,_) -> serveStrLn (show (Zesty (pub,if proof && ?access >= Almighty then map (,meta) priv else Nothing)))
+        Just (_,pub,priv,meta,_) -> serveStrLn (show (Zesty (KeyInfo pub meta (if proof && ?access >= Almighty then priv else Nothing))))
         Nothing -> serveStrLn ("Error: Unknown key '"+name+"'")
     "import" -> do
+      let first = foldr1 (<+?)
       name <- expected "key name" (nbhspace >> dirArg)
       try (serveStrLn "Error: Invalid key") $ expected "client key name or raw key export" $ do
         nbhspace
-        Zesty (pub,priv) <- (single '#' >> dirArg) >*> readable
-                            <+? Zesty . (,Nothing) <$> do
-                              name' <- dirArg
-                              logLine Verbose $ format "Asking client for key '%s'" name'
-                              (maybe zero return =<< liftIO (clientKey name'))
-                                <+? (maybe zero (\(Zesty p) -> return p) =<< dns_lookup (DomainKey name'))
-                                <+? (warn Sev_Error (format "Error: unknown client key '%s'" name') >> zero)
+        Zesty (KeyInfo pub meta priv) <-
+          first [(single '#' >> dirArg) >*> readable
+                ,Zesty <$> do
+                    name' <- dirArg
+                    logLine Verbose $ format "Asking client for key '%s'" name'
+                    first [maybe zero return =<< liftIO (clientKey name')
+                          ,maybe zero (\(Zesty p) -> return p) =<< dns_lookup (DomainKey name')
+                          ,warn Sev_Error (format "Error: unknown client key '%s'" name') >> zero]]
         let keyType = maybe "claim" (const "proof") priv
         serveStrLn (format "Importing %s '%s'" keyType name)
-        setKey name (fingerprint pub,pub,map fst priv,maybe zero snd priv,zero)
+        setKey name (fingerprint pub,pub,priv,meta,zero)
     _ -> serveStrLn $ format "Error: unknown key command '%s'" x

curly/src/Curly/UI.hs

@@ -134,7 +134,7 @@ cacheCurly (src,cache) a ms = by thunk $ do
                   x -> f' & metadata.iso (\(Metadata m) -> m) Metadata
                        %~ insert "publisher" (maybe id (\x -> insert ["public-key"] (Pure (show (Zesty x)))) (fst <$> keyInfo x)
                                               $ withDate
-                                              $ Join (maybe zero snd (keyInfo x)))
+                                              $ maybe zero snd (keyInfo x) ^. at "publisher".l'Just (Join zero))
                        . insert "context" (mapF (\(ModDir d) -> fromAList d)
                                            $ shortZipWith (const . show . by flID) ?mountain (f'^.imports))
                 withDate x | x^?at ["timestamp"].t'Just.t'Pure == Just "date" = insert ["timestamp"] (Pure (show (floor (1000*time)))) x

definitive-base/src/Algebra/Core.hs

@@ -3,8 +3,8 @@ module Algebra.Core(
   -- * Raw data
   Handle,stdin,stdout,stderr,
   Packed(..),
-  Chunk,chunkSize,readChunk,writeChunk,readHChunk,writeHChunk,
-  Bytes,bytesSize,readBytes,writeBytes,readHBytes,writeHBytes,
+  Chunk,chunkSize,readChunk,writeChunk,readHChunk,readHNChunk,writeHChunk,
+  Bytes,bytesSize,readBytes,writeBytes,readHBytes,readHNBytes,writeHBytes,
   readString,writeString,readHString,writeHString,
   appendString,
   
@@ -150,8 +150,12 @@ writeString :: String -> String -> IO ()
 writeString = P.writeFile
 readHBytes :: Handle -> IO Bytes
 readHBytes = BSL.hGetContents
+readHNBytes :: Handle -> Int -> IO Bytes
+readHNBytes = BSL.hGet
 readHChunk :: Handle -> IO Chunk
 readHChunk = BSS.hGetContents
+readHNChunk :: Handle -> Int -> IO Chunk
+readHNChunk = BSS.hGet
 readHString :: Handle -> IO String
 readHString = hGetContents
 writeHBytes :: Handle -> Bytes -> IO ()

misc/exe/Misc.hs

+{-# LANGUAGE ImplicitParams, RankNTypes, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
 module Main where
 
 import Definitive
-import Curly.Core.Security
-import System.Environment (getArgs)
+
+data BindType = Lam | Prod
+              deriving (Eq,Show)
+data ApType = Ap Int | Delta Node
+            deriving (Show)
+data Node = Bind BindType String Node Node
+          | Shape ApType [Node]
+          | Uni Int
+          deriving Show
+
+par lvl d msg | d > lvl = "("+msg+")"
+              | otherwise = msg
+
+show_node = go 0 []
+  where go d env (Bind Prod x tx e) | not (0`isKeyIn`freevars e) = par 0 d $ go 1 env tx + " -> " + go 0 (fresh env x:env) e
+        go d env (Bind t x tx e) = par 0 d $ binder_prefix t+binder_body t env x tx e
+          where binder_prefix Lam = "λ"
+                binder_prefix Prod = "∀"
+        go d env (Shape (Ap i) args) = par lvl d $ intercalate " " (ni:map (go 2 env) args)
+          where lvl = if empty args then 1000 else 1 :: Int
+                ni = case drop i env of
+                       [] -> "#"+show i
+                       n:_ -> n
+        go d env (Shape (Delta v) args) = par 1 d $ "δ" + intercalate " " (map (go 2 env) (v:args))
+        go _ _ (Uni i) = "Set"+show i
+        fresh env x = head [y | y <- x:[x+show i | i <- [0..]], not (y`elem`env)]
+        binder_body t env x tx e = "("+x'+":"+go 0 env tx+")"+binder_tail t (x':env) e
+          where x' = fresh env x
+        binder_tail t env (Bind t' x tx e) | t==t' && (t'/=Prod || 0`isKeyIn`freevars e) = " "+binder_body t env x tx e
+        binder_tail _ env x = ", "+go 0 env x
+type InEnv t = (?env :: [String]) => t
+infixr 1 -=>, -->
+(-=>) :: InEnv ((String,Node) -> (InEnv Node) -> Node)
+(x,tx) -=> e = Bind Lam x tx (let ?env = x : ?env in e)
+(-->) :: InEnv ((String,Node) -> (InEnv Node) -> Node)
+(x,tx) --> e = Bind Prod x tx (let ?env = x : ?env in e)
+(-$) :: Node -> Node -> Node
+Shape (Ap i) args -$ b = Shape (Ap i) (args+[b])
+_ -$ _ = error "Not implemented"
+
+var :: String -> InEnv Node
+var s = case [i | (i,s') <- zip [0..] ?env, s==s'] of
+  i:_ -> Shape (Ap i) []
+  _ -> error $ "No variable named "+s+" in environment"
+
+adjust_vars_depth delta = go 0
+  where go d (Bind t x tx e) = Bind t x (go d tx) (go (d+1) e)
+        go d (Shape (Ap i) args) = Shape (Ap (if i<d then i else d+delta (i-d))) (map (go d) args)
+        go d (Shape (Delta v) args) = Shape (Delta (go d v)) (map (go d) args)
+        go _ (Uni u) = Uni u
+
+currentDepth :: MonadReader [Node] m => m Int
+currentDepth = length <$> ask
+
+hypotheses :: MonadReader [Node] m => m [Node]
+hypotheses = ask <&> zipWith (\i h -> adjust_vars_depth (+i) h) [1..]
+
+hypothesis :: MonadReader [Node] m => Int -> m Node
+hypothesis h = head . drop h <$> hypotheses
+
+freevars :: Node -> Set Int
+freevars (Bind _ _ tx e) = freevars tx + map (subtract 1) (delete 0 (freevars e))
+freevars (Shape (Ap i) args) = touch i (foldMap freevars args)
+freevars (Shape (Delta v) args) = freevars v + foldMap freevars args
+freevars _ = zero
+
+subst :: MonadReader [Node] m => Node -> Node -> m Node
+subst v node = do
+  d0 <- currentDepth
+  let go (Bind t x tx e) = Bind t x <$> go tx <*> local (tx:) (go e)
+      go (Shape (Ap 0) args) = do
+        d <- subtract d0 <$> currentDepth
+        foldl' (\mf x -> do
+                   f <- mf
+                   tx' <- type_of x
+                   case f of
+                     Bind Lam _ tx e -> subst x e
+                     _ -> error $ "Invalid application of non-product value:"+show f)
+          (pure (adjust_vars_depth (+d) v)) args
+      go (Shape (Ap i) args) = do
+        d <- subtract d0 <$> currentDepth
+        Shape (Ap (if i<d then i else i-1)) <$> traverse go args
+      go (Shape (Delta d) args) = liftA2 (\x y -> Shape (Delta x) y) (go d) (traverse go args)
+      go (Uni u) = return $ Uni u
+
+  go node
+
+type_of :: MonadReader [Node] m => Node -> m Node
+type_of = go
+  where go (Bind Lam x tx e) = Bind Prod x tx <$> (local (tx:) $ go e)
+        go (Bind Prod _ tx e) = do
+          Uni u <- go tx
+          Uni u' <- local (tx:) (go e)
+          return $ Uni (max u u')
+        go (Shape (Ap f) xs) =
+          foldl' (\mtf x -> do
+                     tf <- mtf
+                     tx' <- go x
+                     case tf of
+                       Bind Prod _ tx e | nonempty (convertible tx tx') -> subst x e
+                       _ -> error $ "Invalid type for application:"+show tf)
+          (hypothesis f) xs
+        go (Uni u) = pure $ Uni (u+1)
+        go x = ask >>= \env -> error $ "Cannot infer type for term: "+show (env,x)
+
+convertible (Bind t x tx e) (Bind t' _ tx' e') | t==t' = Bind t x <$> convertible tx' tx <*> convertible e e'
+convertible (Shape (Ap i) args) (Shape (Ap i') args') | i==i' = Shape (Ap i) <$> sequence (zipWith convertible args args')
+convertible (Uni u) (Uni u') | u<=u' = return $ Uni u'
+convertible _ _ = Nothing
+
+drop_last n l = take (length l-n) l
+
+instance MonadReader r m => MonadReader r (ListT m) where
+  ask = (pure <$> ask)^.listT
+  local f ma = ma & warp (from listT) (local f)
+
+list_patterns :: MonadReader [Node] m => Node -> ListT m ([Bool],Node)
+list_patterns node = do
+  d0 <- currentDepth
+  let candidate p (Bind _ _ _ e) = candidate (p+1) e
+      candidate p (Shape (Ap p') _) = p==p'
+      candidate _ _ = False
+      go stack (Bind Prod x tx e) = do
+        (parms,e') <- local (tx:) $ go stack e
+        return (parms,Bind Lam x tx e')
+      go stack (Shape (Ap p) _) = do
+        envsize <- subtract d0 <$> currentDepth
+        env <- drop_last d0 <$> ask
+        (i,hypi) <- choose . reverse . zip [0..] =<< hypotheses
+        guard (candidate p hypi)
+        let isrec d t = any (\x -> x-d<envsize && x>=d) (freevars t)
+            newparams d (Bind Prod x tx e) | isrec d tx = (True,x,foldl' (\tx' p' -> Bind Prod x p' tx') tx env) : newparams (d+1) e
+                                           | otherwise = (False,x,adjust_vars_depth (\i' -> if i'>=d then i'-envsize else i') tx) : newparams (d+1) e
+            newparams _ _ = []
+        let parms = newparams 0 hypi
+        return (parms,Shape (Ap i) [if isR then Shape (Ap j) [Shape (Ap k) [] | k <- reverse [0..envsize-1]]
+                                    else Shape (Ap j) []
+                                   | (j,(isR,_,_)) <- reverse $ zip [envsize..] (reverse parms)])
+      go _ _ = zero
+  (parms,node') <- go [] (adjust_vars_depth (+1000) node)
+  let np = length parms
+      adj i = adjust_vars_depth (\x -> if x+i>=np then subtract (i+1000-np) x else x)
+      node'' = foldl' (\e (i,(_,x,tx)) -> Bind Lam x (adj i tx) e) (adj 0 node') (zip [1..] parms)
+  return (map (by l'1) parms,node'')
+
+coc_identity = let ?env = [] in ("A",Uni 0) -=> ("x", var "A") -=> var "x"
+coc_nat = let ?env = ["B"] in ("A",Uni 0) --> ("x",var "A") --> ("f", ("y",var "A") --> var "A")
+                              --> var "A"
 
 main = do
-  [file] <- getArgs
-  a <- readString file
-  k <- genPrivateKey
-  sa <- signValue k a
-  case extractSignedBy (publicKey k) sa of
-    Just a' -> print a >> print a'
-    Nothing -> putStrLn "Invalid signature !"
+  print coc_identity
+  putStrLn (show_node coc_identity)
+  putStrLn (show_node (type_of coc_identity []))
+  putStrLn (show_node (type_of (type_of coc_identity []) []))
+  putStrLn (show_node coc_nat)
+  sequence_ [putStrLn (show i+": "+show rs+": "+show_node pat)
+            | (i,(rs,pat)) <- zip [0..] $ (list_patterns coc_nat^..listT) [Uni 0]]