Checking Out dsolve
===================

To check out dsolve from git:

1. git clone goto.ucsd.edu:/git/dsolve
2. cd dsolve
3. ./init-submodules.sh

Compiling dsolve
================

dsolve requires OCaml 3.10+ and CamlIDL.

dsolve can only be compiled on Linux at the moment.

To compile dsolve:

1. If you downloaded dsolve from the web, see the section below on
   installing Z3 first.

2. Run ./configure && make libs && make

3. (Optional) Run the regression test suite via

     make tests

Installing Z3
=============

For legal reasons, we cannot distribute the Z3 SMT solver that dsolve
requires.  Instead, you must download Z3 2.4 for Linux from

  http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html

Untar the file in the external/ subdirectory; this will create the
directory external/z3.  You can now proceed to build dsolve.

Running dsolve
==============

To typecheck your program with dsolve, run

  ./dsolve.py [ML source file]

Example programs are included in tests/.
The inferred types are output in a .annot file.
For example,

  ./dsolve.py foo.ml

will produce the annotation file foo.annot

Sometimes the types have predicates like "(= V (+ __tmp0 1))".  This is due to
A-normalization.  To get around this, you can run without A-normalization:

  ./dsolve.py -no-anormal [ML source file]

Many programs will not typecheck without A-normalization, so it is on
by default.

For more options, run:

  ./dsolve.py -help

To add options "permanently" for an ML source file, add a line:

  (* DSOLVE [options] *)

at the start of the ML source file. See postests/mapreduce_hash.ml
for an example.



Defining Qualifiers
===================

Qualifiers are specified as patterns which match program identifiers,
literals, types, and operators.

When dsolve is invoked on a file path_to/foo.ml, it uses the
qualifiers specified in the file

  ./default_patterns

dsolve also uses the qualifiers specified in the file

  path_to/foo.hquals

if it exists.  Example hquals files can be found in examples/.

Syntax
------

Qualifiers can include the following constructs:

* Logical constants *
qualif A(v): true
qualif B(v): false

* Logical connectives *
qualif A(v): true && false
qualif B(v): true || false
qualif C(v): not true

* Boolean Variables *
qualif A(v): (? v)

  "v is a program variable of boolean type such that v is equal to true"

** Non-Boolean Variables and Expressions **

* Integer Literals, Identifiers, and Operators *
qualif IsXPlus3(v): v >= x + 3

* Condition expression (ifthenelse) *
qualif Max(v): v = if (x > y) then (x) else (y)
qualif Max(v): v = (x > y ? x : y)

* Sets of Integer Literals *
qualif A(v): v = [0,1,2]

* Sets of Identifiers *
qualif A(v) : v = [a, b, c]

* ^ - Integer Literal Wildcard *
qualif PlusSomething(v): a = b + ^

* Sets of Arithmetic Operators *
qualif A(v) : v {< +, - >} 5 > 0

* Sets of Relational Operators *
qualif A(v): v { <, <= } 5

* (* *) - Operator Wildcard *
qualif A(v): v { * * } 5
qualif A(v) : v {< * * >} 5 > 0 (possibly)

* Metavariables With Optional Type Annotations *
qualif A(v) : ~A + v = ^
qualif C(v)(A:int, B:int^) : ~A + v + ~B = ^

  Annotated types are matched to program types by unification.

  The type grammar can't handle ADTs or records.  However, you can
  define these as user types in the program source and then reference
  the type name in the pattern.

* Anonymous Metavariables *
qualif D(v) : v = _ + _

  Each instance of _ is a new anonymous, unique metavariable.



Defining Liquid Interfaces 
==========================

When running

  ./dsolve.py path_to/foo.ml

dsolve will attempt to use the interface file

  path_to/foo.mlq

if it exists.

This Liquid interface file can be used to specify the Liquid types of
program values as well as specify measure functions which can be
used to prove structural properties of sum types. Example Liquid 
interfaces can be found in Examples/.

Liquid interfaces can also be used to specify abstract data structures like
sets and arrays, together with their operations, axioms and dependent
types. Examples include:
	tests/myset.mlq
	tests/myarray.mlq

To include the interface file for an abstract data structure, ensure that:
	1. There are .mli and .mlq files for the corresponding module,
	2. There is a .cmi file 
		(e.g. ocamlc tests/myset.mli) 
	3. You include the path to the modules 
		(e.g. ./dsolve.py -I tests foo.ml)

Liquid Modules
==============

A source file foo.ml may depend on an external module. 
dsolve will try to read in a "module_name.mlq" file 
from the same directory as the source file if it does.

Interface Syntax
------

A Liquid interface consists of two lists, the first specifying
predicate abbreviations to be used in type definitions, the second
mapping values to Liquid types.


* Predicate Aliases *

First, there is a list of predicate aliases, used as abbreviations in
type specifications.  Example:

pred P = (v) v > 0

Note: predicate aliases cannot reference other predicate aliases.


* Value to Liquid Type Mappings *

Second, there is a list of value, type pairs.  Examples:

val program_ident : {v: int | v > 0 }

The type on the right hand side of the colon can take on several forms:

int == {int | true}

{v: int array | Array.length v > 0} == {v: {int | true} array | Array.length v > 0)

{int | P} == {v: int | v > 0}


Records are specified as follows:

{v: { lbl : int } | v.lbl = 0} == {v: { lbl : {int | true} | v.lbl = 0}

Tuples work similarly.

ADTs can be specified as follows:

{v: [[], [v: v > 0, v: true]] [t: list . || {e0: int | e0 > 10},
                                            e1: [[], [v: v > 1, v: true]] t] | len v = 2}

Note that || separates type constructors, and the first constructor,
[], has no parameters.

Measure Syntax
--------------

A measure is a function from a sum type to the integers which specifies some useful
structural property of that type. Measures can be recursive (allowing inductive reasoning),
but must be expressed in EUFA. Measures are defined in two parts:

1) A measure definition in the liquid interface file.

measure length =
| [] -> 0
| _ :: b -> 1 + length b

and ONE of:

2a) A matching function in the ml source code.

let length l =
  match l with
  | [] -> 0
  | _ :: b -> 1 + length b

OR

2b) An ML interface declaration in the mli file.

val length: 'a list -> int

Uninterpreted Functions
-----------------------

You can define an uninterpreted function

  foo :: x: 'a -> {v: int | v = foo x}

using the syntax

  uninterpreted foo: 'a -> int

The canonical example is

  uninterpreted valid: 'a -> int

  assume (valid x = 1);
  ...
  assert (valid x = 1);

Error Messages
--------------

Liquid interface files which contain identifiers not found in the
program will fail with an explicit error.

If the Liquid interface file and the ML typechecker disagree about the
ML type of an identifier, dsolve will fail with a somewhat cryptic
error*.  For example, if the Liquid interface specifies a (bool, int)
value but the actual type of the value is int, the error produced is

  Unsupported types for instantiation: {({bool | true}, {int | true}) | true}
    {int | k_1191}
  Fatal error: exception Assert_failure("qualifying/frame.ml", 168, 5)

* Other cryptic errors may also apply.

If your type annotation causes the program to not typecheck, 
the error message will have an inexplicable location.  Example:

  File "DML/bsearch.mlq", line 1, characters 0-1:
  {int | (V = __atmp30)} is not a subtype of {int | (v >= 0)}