Project

General

Profile

Statistics
| Branch: | Revision:

cool / HACKING @ master

History | View | Annotate | Download (5.24 KB)

1
// -*- mode: adoc; fill-column: 80; -*-
2
HACKING COOL
3
============
4

    
5
== Internal API Documentation
6

    
7
Run `ocaml setup.ml -doc` after `oasis setup`. It will generate HTML API
8
documentation for COOL's internal library in `cool_api.docdir/index.html`.
9

    
10
As most of the API currently doesn't have documentation comments, this is mainly
11
useful for getting hyperlinked `.mli`-files. But please feel free to add more
12
comments.
13

    
14
== Tests
15

    
16
There are two sets of tests: Integration tests in `src/testsuite` and unit tests
17
in `src/unit-tests`. The former can be used to test the whole reasoner on
18
example formulas with known satisfiability, the latter is for individual
19
functions.
20

    
21
To run all tests, run `make test`. You will need to install the additional
22
dependency `ounit`. The individual test suites can be run with
23
`./cool-testsuite.native` and `./cool_unit_tests.native` respectively.
24

    
25
If unit tests are not being build, use
26

    
27
  ocaml setup.ml -configure --enable-tests
28

    
29
Adding another Functor
30
----------------------
31

    
32
Extending Formula Syntax
33
~~~~~~~~~~~~~~~~~~~~~~~~
34
To add another functor, extend the algebraic type formula in CoAlgFormula.mli
35
*and* CoAlgFormula.ml in src/lib/ by adding another case. Note that normally,
36
you always need (at least) two constructors -- one for the negative and one for
37
the positive case. That is because in a later internal representation, the
38
assumption must hold that negations are only in front of atomic propositions
39
(i.e. variables). Concretely for implementation, every operator needs to have
40
its dual, as we convert to NNF later. For example:
41

    
42
  | CONST of string (* constant functor with value string *)
43
  | CONSTN of string (* constant functor with value string *)
44

    
45
[ This is the data type generated at parse time ]
46

    
47
Do the analogous thing for the type hcFormula_node in the same files!
48

    
49
  | HCONST of string (* constant functor w *)
50
  | HCONSTN of string (* constant functor w *)
51

    
52

    
53
Recall: edit both the ml and the mli-file. Do the analogous thing for
54
formulaType in CoAlgMisc.mli and CoAlgMisc.ml:
55

    
56
  | ConstF (* constant functor *)
57
  | ConstnF (* constant functor *)
58

    
59
[ This is the internal data type used by the reasoner ]
60

    
61
If you build now, you will see a lot of warnings concerning non-exhaustive
62
pattern matchings. We will fix them later.
63

    
64
Extending Functor Syntax
65
~~~~~~~~~~~~~~~~~~~~~~~~
66
Before being able to solve them, we have to extend the functor type.
67
Therefore, extend the type functor in CoAlgMisc.mli *and* CoAlgMisc.ml.
68

    
69
  | Constant
70

    
71
Furthermore, in CoAlgMisc.ml you should extend the unaryfunctor2name array:
72

    
73
  ; (NPa Identity, "Id")
74

    
75
for a functor (like identity) that doesn't take any parameters. For
76
functors that do take parameters, such as the constant functor, also add
77
a constructor to parametricFunctorName, such as
78
  
79
    | NameConstant
80

    
81
and reflect the fact that the functor takes parameters in the
82
addition of
83

    
84
    ; (Pa  NameConstant , "Const")
85
    ; (Pa  NameConstant , "Constant")
86

    
87
in unaryfunctor2name.
88

    
89

    
90
You are also allowed to give multiple names which can be used for parsing.
91

    
92
Extending Formula parsing
93
~~~~~~~~~~~~~~~~~~~~~~~~~~
94
Now, force the rebuild to get all non-exhaustive pattern matchings. You can
95
force it for example via:
96

    
97
  ocaml setup.ml -clean
98

    
99
And then rebuild with:
100

    
101
  ocaml setup.ml -build
102

    
103
You have to extend the parsing in the parse_rest function in CoAlgFormula.ml. If
104
you introduce another symbol that was not used before, you have to extend the
105
global variable lexer in CoAlgFormula.ml accordingly.
106

    
107
These contain:
108

    
109
In file CoAlgMisc.ml:
110

    
111
  - detClosure: Check that a formula has the correct sort and call detClosure if
112
    needed on subformulae. This is the first time where you should pick a
113
    concrete syntax for the operators of your new functor. (I.e. the syntax
114
    visible to the user may differ from the internal name of the constructor,
115
    and here it is the first time where the user sees it. So take care that the
116
    error message here fits the actual functor syntax)
117

    
118
    | C.HCCONST _ ->
119
      if func <> Constant || List.length sortlst <> 1
120
      then raise (C.CoAlgException "=-formula is used in wrong sort.")
121
      else ();
122
    | C.HCCONSTN _ ->
123
      if func <> Constant || List.length sortlst <> 1
124
        then raise (C.CoAlgException "=-formula is used in wrong sort.")
125
        else ();
126

    
127
  - in initTables: Destruct the algebraic datatype into its parts. 
128

    
129
    | C.HCCONST val ->
130
      !arrayType.(s).(n) <- ConstF;
131
      !arrayDest3.(s).(n) <- .... [see sourcecode ...]
132

    
133
In file CoAlgFormula.ml:
134

    
135
  - sizeFormula: determine the size of the tree representation of a
136
    formula
137

    
138
  - in iter: iter func formula lets the funciton func iterate over all
139
    subformulars of formula.
140

    
141
  - convert_post -- totally analogous to iter.
142
  - exportFormula_buffer: string representation of a formula
143
  - exportTatlFormula_buffer: used for ATL, you probably want to
144
    raise an exception here
145
  - nnfNeg -- return the negated formula in nnf.
146
  - nnf -- return the formula in nnf.
147
  - simplify -- simplifiy the formula
148
  - And other utility functions: equal_hcFormula_node, equal_hcFormula_node,
149
    hash_hcFormula_node (possibly extend the base value), toFml_hcFormula_node, negNde_hcFormula_node, hc_formula
150

    
151

    
152
In file CoAlgLogics.ml:
153

    
154
  - getExpandingFunctionProduce: this is where you need to implement
155
    the actual logical rule.
156
// vim: tw=80 ft=asciidoc