Permalink
Browse files

Update BUGS, TODO, remove needless putStrLn in Plugin.lhs

darcs-hash:20070805221644-228f4-fb4aace10c23ad2a69f8b81048a93f6857d4bb87.gz
  • Loading branch information...
1 parent e15c837 commit da259b89097d46fb922186adc0830461dbf85175 eb committed Aug 5, 2007
Showing with 6 additions and 9 deletions.
  1. +4 −2 BUGS
  2. +1 −3 Ivor/Plugin.lhs
  3. +1 −4 TODO
View
6 BUGS
@@ -1,3 +1,7 @@
+* Pattern matching RHS doesn't deal with bindings properly (if there
+ are names bound on the RHS, anything could happen...)
+* Higher order recursive datatypes do not have induction hypothesis
+ generated for the higher order arguments.
* Non-termination if trying to parse an expression with no closing bracket.
* Tactics should know what level they operate at; currently we need to
allow escapes at the top level in the typechecker as a hack, and
@@ -15,8 +19,6 @@
some of the arguments explicitly.
* No check for strict positivity.
Workaround: Don't use non positive types :).
-* Higher order recursive datatypes do not have induction hypothesis
- generated for the higher order arguments.
Recently fixed:
View
@@ -25,10 +25,8 @@
> load :: FilePath -> Context -> IO (Context, Maybe (Parser ViewTerm))
> load fn ctxt = do
-> putStrLn "Loading"
> mv <- Plugins.load_ fn [] "initialise"
-> -- mv <- Plugins.load fn [] ["/home/eb/.ghc/i386-linux-6.4.1/package.conf"] "initialise"
-> putStrLn "Loaded"
+> -- mv <- Plugins.load fn [] ["/Users/edwin/.ghc/i386-darwin-6.6.1/package.conf"] "initialise"
> initialise <- case mv of
> LoadFailure msg -> fail $ "Plugin loading failed: " ++ (show msg)
> LoadSuccess _ v -> return v
View
5 TODO
@@ -1,15 +1,12 @@
Short term things to do:
+* Ability to add commands as well as tactics would be useful.
* 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)
* Improve error messages!
* Recursive functions shouldn't reduce at type level.
* Either better than Monad m? Define an Error type.
-* Pattern matching compiler with totality checker would be very
- useful, as a stop gap in place of elimination with a motive. This
- probably involves adding a 'TotallyImpossible' construct to TT, and
- an axiom (A:*)->(Eq _ _ x TotallyImpossible)->A.
* Fix naming bug --- terms of form t1 -> t2 automatically give t1 the
name X, which can clash. Particularly a problem in data type declarations.
* Current naive proof state representation is far too slow. Come up

0 comments on commit da259b8

Please sign in to comment.