--------------------------------------------------------------------------------
::  Dependent JavaScript  ::  Ravi Chugh (rkc) ([email protected])           ::
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
Licenses

  1) LICENSE.DJS   : System !D + DJS
  2) LICENSE.LamJS : LambdaJS by Arjun Guha and Claudiu Saftoiu (in src/LamJS)
  3) LICENSE.Z3    : Z3 by Microsoft Research
  4) BNstats/      : BNstats.ml by Necula, McPeak, and Weimer

--------------------------------------------------------------------------------
Requirements

  1) Microsoft Z3 Theorem Prover
     http://research.microsoft.com/en-us/um/redmond/projects/z3/

     Use any version v2.17 or later. We used v3.2 to run our benchmarks.
     We've included a few versions for Linux and OSX in bin/.

  2) ocamlbuild

--------------------------------------------------------------------------------
Building System D

  1) make

  2) export DJS_DIR=/path/to/djs/

     Set and export this variable to the root of the DJS directory.
     Use the absolute path, not the path relative from your home directory (~).
     You'll probably want to add this to your shell startup script.

  3) Add the z3 executable somewhere accessible by PATH, and call it "z3".

     For example:
       ln -s $DJS_DIR/bin/z3-osx-3.2 SOMEWHERE_IN_PATH/z3

     Alternatively, add the following to your shell startup script:
       alias z3=$DJS_DIR/bin/z3-osx-3.2

--------------------------------------------------------------------------------
Examples

  The OOPSLA benchmarks (unannotated and annotated) are in:
    tests/apr-benchmarks/un/
    tests/djs/oopsla12/

  To generate stats for line counts and type checking, cd to the src/ directory 
  and run:

    ../scripts/gen-benchmark-linecounts-sep2012.py
    ../scripts/gen-benchmark-time-sep2012.py

  Additional examples can be found in the tests/djs/ directory.

--------------------------------------------------------------------------------
Standard Prelude

  A standard prelude of built-in System !D primitive functions and native
  JavaScript functions are in:

    prims/basics.dref
    prims/objects.dref
    prims/js_natvies.dref

  These three files are loaded along with every program.

--------------------------------------------------------------------------------
Running DJS

  # ./system-dref -djs ../tests/djs/objects/simple00.js
  ...
  OK! 24 queries.

  Each DJS program is desugared to System !D and then converted into A-normal
  form, stored in out/anfExp.dref. To run System !D on this file, which
  already contains the standard prelude from the previous run, use the -raw
  flag so that the file is processed directly.

  # ./system-dref -raw out/anfExp.dref
  ...
  OK! 24 queries.

  All of the queries dispatched to Z3 are saved in out/queries.smt2 in the
  SMT-LIB2 format, and can be run directly through z3.

  # z3 MBQI=false out/queries.smt2 | cat -n 

  The line numbers help match up queries with the query numbers (in comments)
  in queries.lisp.

  Examples written directly in !D can be found in the tests/functional/ and
  tests/imperative/ directories.

  # ./system-dref ../tests/imperative/objects/test00.dref
  ...
  OK! 5 queries.

  The following script runs all of the examples in a given directory:

  # ../scripts/run-tests.py imperative/objects