README.txt

This directory contains the current samizdat version of OLEG, specifically

  src            the source code (still needs SML/NJ 0.93)
  bin            linux binaries compiled from the above
  examples       some demo scripts
  papers         related old drafts of papers now changed beyond recognition
                   (and generally for the better)
  emacs-hack.el  not so much an oleg mode; more a nightmare of comint and
                   font-lock


Things you might like to know


(1)  EMACS GADGETS

     Try adjusting the code in emacs-hack.el to point to your oleg binary,
     then run it when you start emacs (e.g. by pasting it into .emacs).
     Now, when you've just loaded an oleg script, do M-x run-lego and it'll
     start an oleg process for you. Moreover, the tab key in the script
     buffer will send a line to the oleg process. More moreover, most things
     will get coloured in properly.
  
     It's not even Proof Lance Corporal, but it's better than a poke in the
     eye.

     By the way, if things start going really slowly, try watching in black
     and white...


(2)  LIBRARY

     Er. Sorry about that. I can't quite remember how, but I seem to have
     broken the module system at some point---it's incompatible in some way
     with the labelling mechanism or something.

     Anyhow, the library as was isn't so useful for oleg development. On
     the other hand, you'll notice that each of the example files has the
     same prelude. More or less. I guess it could be an include file.


(3)  EXAMPLES

     BasicProg.l  demonstrates the basics of the exciting new programming
                    tactics
     TypeCheck.l  is the implementation of the typechecker from VfL version I
                    (the early funny one---see PAPERS)
     TYPES03.l    is the demo script used at TYPES 2003, in which we have
                    the joy of gcd
     Exception.l  is the code and correctness proof for my variation on the
                    theme of Hutton and Wright's compiler-with-exceptions;
                    as advertized in their paper
     Unify.l      if the code and correctness proof for first order unification
                    by structural recursion (see PAPERS)


(4)  PAPERS

     old-elim.ps  is the original no-you-can't-fit-all-that-in-19-pages
                    version of EwaM, which attempts to be forthcoming about
                    no confusion and no cycle proofs, and has some moderately
                    provocative ideas about what the gadgets might be good
                    for; most of which got censored, in favour of doing one
                    job well...
     view-I.ps    is the earlier funnier (and shorter) version of VfL; whilst
                    anonymous referees provoked significant improvements
                    and much useful work on elaboration, I do feel that the
                    official version has lost (a) the emphasis on interactive
                    programming (like we do it in oleg) and (b) the feeling
                    of how much fun it is to work this way, rather than how
                    hard you have to work to make a machine believe in it...
     unify.ps     is actually quite close to the real thing, and
     proof.ps     is the correctness proof which nobody read, but is actually
                    quite cool; the Unify.l file follows this pretty closely


(5)  EQUALITY

     The Elim, KJunify and Program X tactics all use John Major equality,
     but Qrepl (and its monster-in-the-basement chum Wave) still use
     Martin-Lof equality. Also, some of the gadget-makers expect to find
     M-L eq. So we need both. Sometimes we need to convert between the two.
     Not so hard.


(6)  GADGETS

     The brackets (!...!) enclose tags---the codes oleg tactics use to refer
     to constructions they exploit. The Generate tactic attempts to find a
     provider for the construction with a given tag. The Label tactic
     maps a tag to a given construction.

     Gadget generation is no longer automatically triggered when you
     declare an inductive datatype. Trigger it yourself, thus

       Inductive [Nat : Type] Constructors
         [zero : Nat]
         [suc  : {n:Nat}Nat];
       Generate (!Nat cases!);    (* the case analysis principle *)
       Generate (!Nat eduardo!);  (* the recursion principle *)

     Note that generating `eduardo' relies on finding

       Inductive [Unit  : Type] Constructors [void : Unit];
       Label (!unit!) Unit;
       Label (!unit void!) void;

     to provide the trivial memo structure.

     The gadgets which prove no confusion still generate the M-L equality
     version. Ugh! I never got around to automating the much simpler JM
     construction, although you can find the template in the example
     files. Here it is again

       [Absurd = {T:Type}T];

       Goal {x,y:Nat}Type;
       Program NatNoConfStmt x y;        (* compute matrix of statements *)
         Program Elim (!Nat cases!) x;
           Program Elim (!Nat cases!) y;
             Program Refine {Phi:Type}Phi->Phi;
             Program Refine Absurd;
           Program Elim (!Nat cases!) y;
             Program Refine Absurd;
             Program Names y x;
               Program Refine {Phi:Type}((x == y)->Phi)->Phi;
       Program Save;
        
       Goal {x,y:Nat}{q:x == y}{tg:Target q}NatNoConfStmt x y;
       Program NatNoConf x y q tg;       (* justify the injective diagonal *)
         Program Elim (!JM elim!) q;
           Program Elim (!Nat cases!) x;
             Program Refine [Phi:Type][phi:Phi]phi;
             Program Refine [Phi:Type][phi:(n == n)->Phi]phi (JMr n);
       Program Save;  
     
       Label (!Nat noConf!) NatNoConf;   (* tell KJunify *)

     Er, also, the effect of

       Label (!nat zero!) zero;
       Label (!nat suc!) suc;

     is to allow (!3!) to abbreviate suc (suc (suc zero)) and so on. Sadly
     only on the input side.


(7)  ELIMINATION

       Elim rule target ... target;

     eliminates with the given rule, after unifying the provided targets
     with the expressions marked as {tg:Target exp} in the rule's type;
     if the rule is not marked up in that way, Elim kind of guesses what
     to do with the targets you provide (in such a way that regular _elim
     rules are properly handled). Subgoal simplification by unification is
     automatic.


(8)  UNIFICATION

       KJunify;

     should actually be called JMunify

     relies on you providing (!Blah noConf!) for each family Blah you need
     to work with; see above recipe


(7)  NAMING HYPOTHESES

       Names x1 x2 x3 ...;

     (re)names the hyps in the goal without intros-ing them; long overdue


(8)  ABSTRACTION

       Abst x exp;

     abstracts every occurrence of exp from the goal as a new hyp called x;
     can cope with exp living under a prefix of hyps---x goes as far left as
     possible

       AbstEq x q exp;

     similar, but also keeps {q:x == exp} as a hyp; wot a larf!

     Examples can be found in Exception.l and Unify.l


(9)  REWRITING

       Wave > lawsProof;
       Wave < lawsProof;

     Wave is a multiple rewriting tactic. lawsProof is a term of type

       ({x:X}... (Eq l[x...] r[x...])) # ... # ({x:X}... (Eq l[x...] r[x...]))

     ie a tuple of universally quantified equations. Wave tries to
     rewrite like billyo, following these laws, in the direction you
     indicate. It's stupid, unsubtle (and potentially unsafe if you
     choose dangerous laws). But it doesn't lie to the typechecker.
     More safety is achievable via the gasoline-controlled version

       Wave n > lawsProof;
       Wave n < lawsProof;

     which limits the number of iterations allowed.

     Favourite applications include

       Wave > (plusAbsorbsZero,plusAssociative);

     Note the use of M-L Eq rather than JM ==. Also, Wave is not smart
     enough to rewrite under hypotheses.

     Examples in Unify.l


(10) PROGRAMMING

     Thrilling new programming tools!

     If your goal is

       ?0 : {x1:S1}...{xn:Sn}T

     and you say

       Program f x1 ... xn;

     you turn your goal into a programming problem! The new Program Blah
     tactics help you solve it! Read on...


(11) PROGRAMMING INFORMATION

     After the execution of each Program Blah tactic, you get not only the
     proof state, but the program state comprising

       (*) the type signatures of the programs currently under development
       (*) their code so far
       (*) information local to the bit of code you're supposed to write next

     All of this information is actually represented in the proof state,
     which comprises goals of form

       (*) {...}T_myFun p1 ... pn
             the unsolved programming problems
       (*) <myFun:{...}T>(myFun == [...]vomit[T_myFun goals])
             the ghastly proof term, so far
       (*) {...}U_myFun p1 ... pn
             one for each lhs, solved or not

     The program signatures are computed from the <myFun> goals; the
     program code is computed by running the ghastly term so far for each
     lhs given by the U_myFun goals.

     By the way, T_myFun is just a frozen function which computes the
     return type of your program. call_myFun and ret_myFun map between
     the two in the obvious (but frozen way). U_myFun is just a frozen
     function which computes a trivial Prop. Don't worry, they'll thaw
     out later.

       Program; (* with no args, note *)

     attempts to generate and print the program state, if you've
     lost it for some reason, eg hand-cranking a bit of the construction.


(12) PROGRAMMING TACTICS

       Program Elim rule target;

     splits a programming problem by rule on target;
     ie does elimination on the given target with the given rule to both the
     T_ goal and the U_ goal

       Program Refine blah;

     fills in blah as the right-hand side of the current goal;
     ie solves the relevant T_ goal (having first tried to extract recursive
     calls from T_ hypotheses); warning---sometimes the latter mechanism
     commits to a T_ hyp too early, leaving unsolvable equations as subgoals
     (hence the hand-cranking in gcd in TYPES03.l)

       Program Names x1 ... xn;

     renames pattern variables (often needed in induction-then-cases progs);
     warning---sometimes muddles the goals up, leaving no programming problem
     topmost, but nothing that Next can't cure.

       Program Abst myFriend arg ... arg;

     generates a programming problem for a helper function taking the given
     args, which are usually existing pattern vars or some (var as exp),
     where exp is an intermediate value you'd like abstracted, and var is
     what it gets called; by a miracle of modern technology, the helper
     function can still remember how to do recursive calls to the master
     function.


(13) KEEPING A PROGRAM

       Program Save;

     should be called when you've filled in all the bits of program and
     killed off any proof obligations apart from the <myFun> and U_ goals.
     It unfreezes what it needs to solve these goals, then after QED, it
     saves the big nasty term as the defined value of the function, freezes
     it, and gives it (iota) reduction rules instead. Freeze/Unfreeze toggles
     whether it's iota/delta reduction for that symbol.


(14) MYSTERIOUS Forget/KillRef PROBLEM

     I've got some sort of bureaucratic cockup in the lego-state/proof-state/
     twilight-zone, which means that retrograde steps sometimes throw away
     too much (e.g. KillRef discarding the reduction rules you just saved,
     or some such). I recommend ripping it all up and starting again.
     Computers are fast. OK, it's still a pain. Undo in proof state is still
     ok. Phew.


(15) SUPPORT

     Choke. Cough. Splutter.


(16) HAVE FUN

     No really, this is possible.