Hello everybody,
Recently I've been working on a toy implementation of HOL (theorem prover)
in Haskell, more specifically in Hugs. The logical parts are coming along
OK, but I'm not interested at all in writing an read-eval-print loop.
Currently I have to write (# = user input, > = hugs response)
# g (mk_imp (mk_var "p" bool) (mk_imp (mk_var "q" bool) (mk_var "p" bool)))
> Current goalstack = ... (*,see below)
or something like that, instead of the more concise (and HOL-like)
# g `p ==> (q ==> p)`
Would it be possible to supply a function of type String -> String
which is applied to every non-command input to Hugs? Of course, this
function should be the identity by default!
Here's a silly example of my intended use:
# setPreprocessor reverse
> :: IO ()
# x ni 3 = x tel
{- reverse returns "let x = 3 in x" -}
> 3 :: Int
More seriously, it would allow the programmer to parse user input
in an arbitrary way, process the syntax tree, and return a Haskell
expression which is (should be) related to the entered expression. You
could, for instance, turn all implicit applications into $!'s thereby
making Haskell quite strict, like this:
# setPreprocessor strictify
> :: IO ()
# (\x y -> x) 3 (1 `div` 0)
{- strictify returns "((\x y -> x) $! 3) $! ((div $! 1) $! 0)" -}
> Program Error: {PrimQrmInteger 1 0}
This would facilitate the development of domain-specific languages, without
burdening the programmer with having to write a full interpreter right
from the start, but 'only' a preprocessing function. In the end, she
probably will have to do this anyway, if the language is to be
compiled. I know you can do this by writing a Haskell program which does
just this preprocessing, compiling it, and supplying it as a '-F' parameter
but those preprocessors have to written and debugged as well...
As an aside, a way to make permanent variable bindings would be great too.
However, this conflicts with the script vs. session philosophy as laid out in
the 'The implementation of the Gofer functional programming system' by Mark P.
Jones. HBI has it, so why not Hugs?
Please tell me why my ideas don't make sense, or give me some
clues/ideas on how to do this (I've done some Hugs source hacking, so tips
like "Start looking at function foo() in input.c" are welcome too!). A third
option is to say "You've been using ML too much, stick to Haskell and you'll
be fine - who needs extensible interpreters anyway?" :-)
Cheers,
Jan de Wit
(*) = Before you start asking, I'm using IORefs and unsafePerformIO...
