Permalink
Browse files

Some helpers for Idris

Ignore-this: 73e53eeb853e51e4aeaa5a0aaf72c81e

darcs-hash:20100323151200-228f4-348dee3d35ff46425e213f1b21c0af143b597ef3.gz
  • Loading branch information...
1 parent bc6d9bc commit 613fef13a03781cbf0bc54b3b7b5ff4a72f90ba1 eb committed Mar 23, 2010
Showing with 11 additions and 6 deletions.
  1. +10 −5 Ivor/ViewTerm.lhs
  2. +1 −1 ivor.cabal
View
@@ -17,7 +17,8 @@
> -- * Terms
> Term(..), ViewTerm(..), Annot(..), apply,
> view, viewType, ViewConst, typeof,
-> freeIn, namesIn, occursIn, subst, getApp,
+> freeIn, namesIn, namesTypesIn, occursIn,
+> subst, getApp,
> Ivor.ViewTerm.getFnArgs, transform,
> getArgTypes, Ivor.ViewTerm.getReturnType,
> dbgshow,
@@ -54,7 +55,7 @@
> -- is for.
> data NameType = Bound | Free | DataCon | TypeCon | ElimOp
> | Unknown -- ^ Use for sending to typechecker.
-> deriving (Show, Enum)
+> deriving (Show, Enum, Eq)
> -- | Construct a term representing a variable
> mkVar :: String -- ^ Variable name
@@ -241,9 +242,13 @@
> -- | Return the names occurring free in a term
> namesIn :: ViewTerm -> [Name]
-> namesIn t = nub $ fi [] t where
-> fi ns (Ivor.ViewTerm.Name _ x) | x `elem` ns = []
-> | otherwise = [x]
+> namesIn t = nub $ (map fst (namesTypesIn t))
+
+> -- | Return the names occurring free in a term, and what kind of name they are
+> namesTypesIn :: ViewTerm -> [(Name, NameType)]
+> namesTypesIn t = nub $ fi [] t where
+> fi ns (Ivor.ViewTerm.Name t x) | x `elem` ns = []
+> | otherwise = [(x, t)]
> fi ns (Ivor.ViewTerm.App f a) = fi ns f ++ fi ns a
> fi ns (Ivor.ViewTerm.Lambda x ty sc) = fi (x:ns) sc
> fi ns (Forall x ty sc) = fi (x:ns) sc
View
@@ -1,5 +1,5 @@
Name: ivor
-Version: 0.1.12
+Version: 0.1.13
Author: Edwin Brady
License: BSD3
License-file: LICENSE

0 comments on commit 613fef1

Please sign in to comment.