/[mojave]/metaprl/theories/mc/TODO
ViewVC logotype

Diff of /metaprl/theories/mc/TODO

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3579 by emre, Fri Apr 12 05:37:53 2002 UTC revision 3580 by emre, Fri Apr 19 08:09:21 2002 UTC
# Line 1  Line 1 
1  Maintainer of this theory: Brian Emre Aydemir (emre@its.caltech.edu)  Maintainer of this theory: Brian Emre Aydemir (emre@its.caltech.edu)
2  Last update to this file: 23 March 2002  Last update to this file: 19 April 2002
3    
4  This file lists what I have remaining to do to complete this theory,  This file lists what I have remaining to do to complete this theory,
5  and some other miscellaneous notes to myself.  and some other miscellaneous notes to myself.
6    
7  Todo list:  Todo list:
8  --------------------------------------------------------------------------  --------------------------------------------------------------------------
9  -  Display forms: These need to be tested and improved so that  -  Notable omissions in FIR implementation:
10     things print in a reasonable fashion.     .  display forms - these are terrible at the moment.
11  -  FIR evaluation: This needs to be completed.     .  fir_ty - frame is missing.
12  -  Test cases: I've fallen way behind on these.  These cases need     .  evaluation:
13     to test display forms, rewrites, any tactic like things I define,        -  no where near complete.
14     and the MC FIR <--> MetaPRL connection code.        -  semantics of division seems wrong (prove deadcode elimination
15  -  Documentation: Other than making a decent README file, I also           of division by zero).
16     need to document code in a slightly more useful fashion.  It would     .  deadcode elim - needs work.
17     be nice if the same mechanism used to produce the docs for all     .  constant eliminatino - needs work.
18     the theories was used here as well.     .  connection to MC:
19  -  Deadcode elimination: Implement more forms of it. Prove the        -  float conversion just doesn't work.  I need someone in MC to
20     forms that aren't proven.           implement 80 bit float <--> int/string conversion.
21  -  Constant elimination: Same notes as for deadcode elim.        -  translating the fundef's only is just a hack.  I need a better,
22  -  Mp_mc_connect_base (special notes):           more robust way to represent an entire FIR program.
23     .  Check float conversion code. Specifically, this code     .  test cases - I need to test some of the "higher level"
24        DOES NOT WORK.  I need a way of going from the 80 bit internal        MetaPRL code (deadcode, const_elim).
25        representation of rawfloat's to some integral or string representation  -  Documentation: I need it. (-: Current ideas involve the use
26        w/o loss of information. This involves some work on the MC     of whatever mechanism generates theories.pdf.
       end I think.  
 -  Verify that Mp_mc_fir_eval actually is general enough now to prove  
    other things... . (It just occurred to me that I don't think I can  
    prove deadcode.)  Everything from "unary operations" down needs  
    to be checked I think.  
 -  fundef (Mp_mc_fir_exp) is a hack.  I need to come up with a term  
    representation for entire programs that is "convinient".  
 -  division: I'm not completely convinced I've expressed this in a  
    "safe and correct" manner.  
 -  Modify conscripts to get MC and MetaPRL compiling together...  
 -  Clean up all the MetaPRL conscripts...  
27    
28  Notes to myself:  Notes to myself:
29  --------------------------------------------------------------------------  --------------------------------------------------------------------------
 -  None at the moment.  
   
 Scratch space (random thoughts to myself):  
 --------------------------------------------------------------------------  
30  -  Checklist for when I need to add/remove/change a term:  -  Checklist for when I need to add/remove/change a term:
31     1) .mli file: term declaration, term operation function signatures     1) .mli file: term declaration, term operation function signatures
32     2) .ml file: term declaration, display form, term operation functions,     2) .ml file: term declaration, display form, term operation functions,
33     3) connect: change cases appropriately (2 directions to check)     3) connect: change cases appropriately (2 directions to check).
34        this could also involve defining new functions.        this could also involve defining new functions.
35     4) test: change cases appropriately     4) test: change cases appropriately
36     5) eval: change evaluation as needed     5) eval: change evaluation as needed
37  -  Checklist for when files are added/removed:  -  Checklist for when files are added/removed:
38     1) Conscript: 2 file lists to check!     1) Conscript:  2 file lists to check
39     2) Makefile: 1 file list to check!     2) Makefile:   1 file list to check
40    
41    Miscellaneous (non-pressing) todo list:
42    --------------------------------------------------------------------------
43    -  Clean up all the MetaPRL Conscripts.

Legend:
Removed from v.3579  
changed lines
  Added in v.3580

  ViewVC Help
Powered by ViewVC 1.1.26