Djinn commands explained
========================

<sym> ? <type>
  Try to find a function of the specified type.  Djinn knows about the
function type, tuples, Either, Maybe, (), and can be given new type
definitions.  (Djinn also knows about the empty type, Void, but this
is less useful.)  Further functions, type synonyms, and data types can
be added by using the commands below.  If a function can be found it
is printed in a style suitable for inclusion in a Haskell program.  If
no function can be found this will be reported as well.  Examples:
  Djinn> f ? a->a
  f :: a -> a
  f x1 = x1
  Djinn> sel ? ((a,b),(c,d)) -> (b,c)
  sel :: ((a, b), (c, d)) -> (b, c)
  sel ((_, v5), (v6, _)) = (v5, v6)
  Djinn> cast ? a->b
  -- cast cannot be realized.
  Djinn will always find a (total) function if one exists.  (The worst
case complexity is bad, but unlikely for typical examples.)  If no
function exists Djinn will always terminate and say so.
  When multiple implementations of the type exists Djinn will only
give one of them.  Example:
  Djinn> f ? a->a->a
  f :: a -> a -> a
  f _ x2 = x2

Warning: The given type expression is not checked in any way (i.e., no
kind checking).


<sym> :: <type>
  Add a new function available for Djinn to construct the result.
Example:
  Djinn> foo :: Int -> Char
  Djinn> bar :: Char -> Bool
  Djinn> f ? Int -> Bool
  f :: Int -> Bool
  f x3 = bar (foo x3)
This feature is not as powerful as it first might seem.  Djinn does
*not* instantiate polymorphic function.  It will only use the function
with exactly the given type.  Example:
  Djinn> cast :: a -> b
  Djinn> f ? c->d
  -- f cannot be realized.

type <sym> <vars> = <type>
  Add a Haskell style type synonym.  Type synonyms are expanded before
Djinn starts looking for a realization.
  Example:
  Djinn> type Id a = a->a
  Djinn> f ? Id a
  f :: Id a
  f x1 = x1

data <sym> <vars> = <type>
  Add a Haskell style data type.
  Example:
  Djinn> data Foo a = C a a a
  Djinn> f ? a -> Foo a
  f :: a -> Foo a
  f x1 = C x1 x1 x1


:clear
  Set the environment to the start environment.


:delete <sym>
  Remove a symbol that has been added with the add command.


:environment
  List all added symbols and their types.


:help
  Show a short help message.


:load <file>
  Read and execute a file with commands.  The file may include Haskell
style -- comments.


:quit
  Quit Djinn.


:set
  Set runtime options.
     +multi    show multiple solutions
               This will not show all solutions since there might be
               infinitly many.
     -multi    show one solution
     +sorted   sort solutions according to a heuristic criterion
     -sorted   do not sort solutions
  The heuristic used to sort the solutions is that as many of the
bound variables as possible should be used.

:verbose-help
  Print this message.


Further examples
================
  calvin% djinn
  Welcome to Djinn version 2005-12-11.
  Type :h to get help.

  -- return, bind, and callCC in the continuation monad
  Djinn> data CD r a = CD ((a -> r) -> r)
  Djinn> returnCD ? a -> CD r a
  returnCD :: a -> CD r a
  returnCD x1 = CD (\ c15 -> c15 x1)

  Djinn> bindCD ? CD r a -> (a -> CD r b) -> CD r b
  bindCD :: CD r a -> (a -> CD r b) -> CD r b
  bindCD x1 x4 =
           case x1 of
           CD v3 -> CD (\ c49 ->
                        v3 (\ c50 ->
                            case x4 c50 of
                            CD c52 -> c52 c49))

  Djinn> callCCD ? ((a -> CD r b) -> CD r a) -> CD r a
  callCCD :: ((a -> CD r b) -> CD r a) -> CD r a
  callCCD x1 =
            CD (\ c68 ->
                case x1 (\ c69 -> CD (\ _ -> c68 c69)) of
                CD c72 -> c72 c68)


  -- return and bind in the state monad
  Djinn> type S s a = (s -> (a, s))
  Djinn> returnS ? a -> S s a
  returnS :: a -> S s a
  returnS x1 x2 = (x1, x2)
  Djinn> bindS ? S s a -> (a -> S s b) -> S s b
  bindS :: S s a -> (a -> S s b) -> S s b
  bindS x1 x2 x3 =
          case x1 x3 of
          (v4, v5) -> x2 v4 v5


Theory
======
  Djinn interprets a Haskell type as a logic formula using the
Curry-Howard isomorphism and then a decision procedure for
Intuitionistic Propositional Calculus.  This decision procedure is
based on Gentzen's LJ sequent calculus, but in a modified form, LJT,
that ensures termination.  This variation on LJ has a long history,
but the particular formulation used in Djinn is due to Roy Dyckhoff.
The decision procedure has been extended to generate a proof object
(i.e., a lambda term).  It is this lambda term (in normal form) that
constitutes the Haskell code.
  See http://www.dcs.st-and.ac.uk/~rd/publications/jsl57.pdf for more
on the exact method used by Djinn.

  Since Djinn handles propositional calculus it also knows about the
absurd proposition, corresponding to the empty set.  This set is
called Void in Haskell, and Djinn assumes an elimination rule for the
Void type:
  void :: Void -> a
Using Void is of little use for programming, but can be interesting
for theorem proving.  Example, the double negation of the law of
excluded middle:
  Djinn> f ? Not (Not (Either x (Not x)))
  f :: Not (Not (Either x (Not x)))
  f x1 = void (x1 (Right (\ c23 -> void (x1 (Left c23)))))