Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Add 'displayName'

darcs-hash:20080201125007-228f4-c506a638a5ec510e24ce8fe6cbf899d97011902c.gz
  • Loading branch information...
commit 6687a338d18e20c10e5e3c0759f5cca1da96f20b 1 parent 715f766
eb authored
View
2  Ivor/Plugin.lhs
@@ -71,7 +71,7 @@ files
> compilePlugin :: FilePath -> IO (Either String FilePath)
> compilePlugin hs
> | isExt ".hs" hs || isExt ".lhs" hs =
-> do status <- make hs []
+> do status <- makeAll hs []
> case status of
> MakeSuccess c out -> return $ Right out
> MakeFailure errs -> return $ Left (concat (map (++"\n") errs))
View
3  Ivor/Shell.lhs
@@ -98,7 +98,8 @@
outputLn st x = output st (x++"\n")
> runCommand :: (Monad m) => Command -> ShellState -> m ShellState
-> runCommand (Def nm tm) st = do ctxt <- addDef (context st) (name nm) tm
+> runCommand (Def nm tm) st = do let (_, tm') = addImplicit (context st) tm
+> ctxt <- addDef (context st) (name nm) tm'
> return st { context = ctxt }
> runCommand (TypedDef nm tm ty) st = do
> ctxt <- addTypedDef (context st) (name nm) tm ty
View
2  Ivor/TT.lhs
@@ -195,8 +195,10 @@
> arguments :: [ViewTerm],
> returnval :: ViewTerm
> }
+> deriving Show
> data Patterns = Patterns [PClause]
+> deriving Show
> mkRawClause :: PClause -> RawScheme
> mkRawClause (PClause args ret) =
View
2  Ivor/Typecheck.lhs
@@ -299,6 +299,8 @@ Insert inferred values into the term
checkbinder :: Monad m => Gamma Name -> Env Name -> Level ->
Name -> Binder Raw -> m (Binder (TT Name))
+-- FIXME: Should convert here rather than assert it must be *
+
> checkbinder gamma env lvl n (B Lambda t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
> let ttnf = normaliseEnv env gamma (Ind tt)
View
6 Ivor/ViewTerm.lhs
@@ -13,7 +13,7 @@
> -- implicitly by "Ivor.TT".
> module Ivor.ViewTerm(-- * Variable names
-> Name,name,NameType(..),mkVar,
+> Name,name,displayName,NameType(..),mkVar,
> -- * Terms
> Term(..), ViewTerm(..), apply,
> view, viewType, ViewConst, typeof,
@@ -33,6 +33,10 @@
> name :: String -> Name
> name = UN
+> displayName :: Name -> String
+> displayName (UN x) = x
+> displayName (MN (x,i)) = "_" ++ x ++ "_" ++ show i
+
> -- | Abstract type representing a TT term and its type.
> newtype Term = Term (Indexed Name, Indexed Name)
View
2  Makefile
@@ -4,7 +4,7 @@ PREFIX = /usr/local
# PREFIX = $(HOME)
# Set this to -p for profiling libraries too
-PROFILE =
+PROFILE =
GHCOPTS =
View
2  TODO
@@ -1,6 +1,6 @@
Short term things to do:
-* Ability to add commands as well as tactics would be useful.
+* Allow holes in pattern matching definitions
* Need an easier way of updating a context with an input file
(currently have to create a shell, then load, then create a new
shell if you want to modify the context further)
Please sign in to comment.
Something went wrong with that request. Please try again.