Permalink
Browse files

Added getAllInductives

darcs-hash:20090228195206-228f4-fb8ad57a6929a01659abe8eb4094ce9860f69513.gz
  • Loading branch information...
1 parent 6b7a51b commit 4ebcbecf8b0391a4aa317de9da41f469a20b17c3 eb committed Feb 28, 2009
Showing with 11 additions and 2 deletions.
  1. +10 −1 Ivor/TT.lhs
  2. +1 −1 Ivor/TTCore.lhs
View
@@ -35,7 +35,7 @@
> -- * Examining the Context
> eval, whnf, evalnew, evalCtxt, getDef, defined, getPatternDef,
> getAllTypes, getAllDefs, getAllPatternDefs, getConstructors,
-> getInductive, getType,
+> getInductive, getAllInductives, getType,
> Rule(..), getElimRule, nameType, getConstructorTag,
> getConstructorArity,
> Ivor.TT.freeze,Ivor.TT.thaw,
@@ -850,6 +850,15 @@ Give a parseable but ugly representation of a term.
> Just d -> (x,d):(getPD xs)
> _ -> getPD xs
+> -- |Get all the inductive type definitions in the context.
+> getAllInductives :: Context -> [(Name,Inductive)]
+> getAllInductives ctxt
+> = getI (map fst (getAllTypes ctxt))
+> where getI [] = []
+> getI (x:xs) = case (getInductive ctxt x) of
+> Just d -> (x,d):(getI xs)
+> _ -> getI xs
+
> getAllDefs :: Context -> [(Name, Term)]
> getAllDefs ctxt = let names = map fst (getAllTypes ctxt) in
> map (\ x -> (x, unJust (getDef ctxt x))) names
View
@@ -483,7 +483,7 @@ Return all the names used in a scope
> p' (P x) = [x]
> p' (App f' a) = (p' f')++(p' a)
> p' (Bind n b (Sc sc))
-> | scnames <- p' sc = (scnames \\ [n]) ++ pb' b
+> | scnames <- p' sc = ((nub scnames) \\ [n]) ++ pb' b
> p' (Proj _ i x) = p' x
> p' (Label t (Comp n cs)) = p' t ++ concat (map p' cs)
> p' (Call (Comp n cs) t) = concat (map p' cs) ++ p' t

0 comments on commit 4ebcbec

Please sign in to comment.