idris 0.9.11 → 0.9.11.1

raw patch · 5 files changed

+28/−1 lines, 5 files

Files

• idris.cabal +4/−1
• src/Idris/AbsSyntax.hs +11/−0
• test/reg033/expected +0/−0
• test/reg033/reg033.idr +10/−0
• test/reg033/run +3/−0

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.11+Version:        0.9.11.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -207,6 +207,9 @@                        test/reg032/run                        test/reg032/*.idr                        test/reg032/expected+                       test/reg033/run+                       test/reg033/*.idr+                       test/reg033/expected                         test/basic001/run                        test/basic001/*.idr

@@ -1744,6 +1744,17 @@   mkUniq (PPair fc p l r)          = do l' <- mkUniq l; r' <- mkUniq r               return $! PPair fc p l' r'+  mkUniq (PDPair fc (PRef fc' n) t sc)+      | t /= Placeholder+         = do env <- get+              (n', sc') <- if n `elem` env+                              then do let n' = uniqueName n (env ++ inScope)+                                      return (n', shadow n n' sc)+                              else return (n, sc)+              put (n' : env)+              t' <- mkUniq t+              sc'' <- mkUniq sc'+              return $! PDPair fc (PRef fc' n') t' sc''   mkUniq (PDPair fc l t r)          = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r               return $! PDPair fc l' t' r'

@@ -0,0 +1,10 @@+mapFilter : (alpha -> beta) ->+           (alpha -> Bool) -> +           Vect n alpha -> +           (n : Nat ** Vect n beta)+mapFilter f p Nil = (_ ** Nil)+mapFilter f p (a :: as) with (p a)+ | True  = (_  ** (f a) :: (getProof (mapFilter f p as)))+ | False = mapFilter f p as++

@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris $@ reg033.idr --check+rm -f reg033 *.ibc