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

Diff of /metaprl/theories/mc/README

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

revision 3563 by emre, Sun Mar 31 02:48:35 2002 UTC revision 3564 by emre, Fri Apr 5 07:07:58 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: 18 March 2002  Last update to this file: 4 April 2002
3    
4  THIS FILE IS REALLY INCOMPLETE!  THIS FILE IS REALLY INCOMPLETE!
5    
6  I describe the purpose of this theory and its implementation in this file.  I describe the purpose of this theory and its implementation in this file.
7  The sections here are:  
    -  Overview: what this theory is for  
    -  General notes: things to keep in mind while perusing the theory  
    -  Compilation issues: why some files are compiled and others aren't  
    -  Module descriptions  
8    
9  Overview:  Overview:
10  --------------------------------------------------------------------------  --------------------------------------------------------------------------
# Line 18  Line 14 
14  << more information should go here eventually >>  << more information should go here eventually >>
15    
16    
 General notes:  
 --------------------------------------------------------------------------  
 These are some points to keep in mind while reading through the code  
 and terms provided by this theory:  
    -  The majority of my comments will be in *.mli files.  Comments  
       in *.ml files will typically deal with my implementation of something,  
       or be there just to mark off general sections of the file.  
    -  I'm trying my best to keep comments up to date, but occasionally,  
       I may forget to update them (that includes this file).  Feel free  
       to ask me about anything that seems out of date and/or incorrect.  
   
   
17  Compilation issues:  Compilation issues:
18  --------------------------------------------------------------------------  --------------------------------------------------------------------------
19  If you're using make to build MetaPRL, this theory should build correctly.  While this theory is intended to compile with (as in, be linked with)
20  The only thing that may seem odd is that the code to "connect" to the  the Mojave compiler, though it will compile without as well.  In order
21  Mojave compiler will not be compiled in.  This is because the Mojave  to compile with MC, you must set the MC_ROOT environment variable to point to
22  compiler is built with cons.  So, for those using cons to build MetaPRL,  the the root directory of MC.
 the "connection" code will be compiled in, but only if the MC_ROOT  
 environment variable is defined.  (You'll probably want to define  
 that variable in order to sensibly use MC.)  Otherwise, the build  
 is the exact same as if the build was done with make.  
    Note that the Conscript is pretty messy since I don't know perl  
 at all.  Please tell me if you know of a better way to write the script.  
23    
24    
25  Mc_term_op:  Module -- Mp_mc_term_op:
26  --------------------------------------------------------------------------  --------------------------------------------------------------------------
27  This module provides basic term construction and deconstruction operations  This module provides basic term construction and deconstruction operations
28  similar to those in Refiner.Refiner.TermOp.  The most notable difference  similar to those in Refiner.Refiner.TermOp.  The most notable difference is my
29  is my naming scheme for the functions.  This scheme and other information  naming scheme for the functions.  This scheme and other information is
30  is documented in mc_term_op.mli.  documented in mp_mc_term_op.mli.

Legend:
Removed from v.3563  
changed lines
  Added in v.3564

  ViewVC Help
Powered by ViewVC 1.1.26