-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
81 lines (50 loc) · 1.55 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
Compiling Without Z3
====================
To build on on platforms WITHOUT Z3, do this:
% cp tpNull.ml.noz3 tpNull.ml
and then
% make
To build on the mac (no Z3), do
% make -f Makefile.mac
To build on platforms WITH Z3, do this:
% cp tpNull.ml.z3 tpNull.ml
% make
Constraint Files
================
The general format of a constraint file is:
[SUBTYPING CONSTRAINTS]
[WELL-FORMEDNESS CONSTRAINTS]
[SOLUTIONS]
Subtyping Constraints
---------------------
A subtyping constraint has the form
constraint:
env[BINDINGS]
grd PREDICATE
lhs REFTYPE
rhs REFTYPE
id INT tag INT_LIST
The BINDINGS are a list of semicolon-separated name, REFTYPE
pairs. The guard PREDICATE is a standard predicate. The integer ID is
used to identify this constraint in error messages, etc. The INT_LIST
is used as a hook into constraint ordering: if two constraints are
equal according to the predicate variable dependency graph, the tie is
broken by comparing the tags in lexicographic order.
Refined Types
-------------
A refined type has the form
{VALUE_VAR : SORT | [PREDICATE_OR_KVARS]}
The VALUE_VAR is an identifier. The SORT is one of int, bool, or ptr.
The list PREDICATE_OR_KVARS is a semicolon-separated list of
predicates and/or kvars (identifiers).
Well-Formedness Constraints
---------------------------
A well-formedness constraint has the form
wf:
env[BINDINGS]
reft REFTYPE
Solutions
---------
A solution assigns a predicate variable to a semicolon-separated list
of predicates:
solution: KVAR := [PREDICATES]