Project

General

Profile

Statistics
| Branch: | Revision:

cool / HACKING @ master

History | View | Annotate | Download (5.24 KB)

1 2bda8737 Hans-Peter Deifel
// -*- mode: adoc; fill-column: 80; -*-
2 69a71d22 Thorsten Wißmann
HACKING COOL
3
============
4
5 7198f96f Hans-Peter Deifel
== 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 c2233aff Hans-Peter Deifel
== 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 69a71d22 Thorsten Wißmann
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 c49eea11 Thorsten Wißmann
  | CONSTN of string (* constant functor with value string *)
44 69a71d22 Thorsten Wißmann
45 bbfe7b6e Dirk Pattinson
[ This is the data type generated at parse time ]
46
47 69a71d22 Thorsten Wißmann
Do the analogous thing for the type hcFormula_node in the same files!
48
49 c49eea11 Thorsten Wißmann
  | HCONST of string (* constant functor w *)
50
  | HCONSTN of string (* constant functor w *)
51 69a71d22 Thorsten Wißmann
52 bbfe7b6e Dirk Pattinson
53 69a71d22 Thorsten Wißmann
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 c49eea11 Thorsten Wißmann
  | ConstnF (* constant functor *)
58 69a71d22 Thorsten Wißmann
59 bbfe7b6e Dirk Pattinson
[ 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 69a71d22 Thorsten Wißmann
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 bbfe7b6e Dirk Pattinson
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 69a71d22 Thorsten Wißmann
89
90
You are also allowed to give multiple names which can be used for parsing.
91
92 bbfe7b6e Dirk Pattinson
Extending Formula parsing
93 69a71d22 Thorsten Wißmann
~~~~~~~~~~~~~~~~~~~~~~~~~~
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 c49eea11 Thorsten Wißmann
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 69a71d22 Thorsten Wißmann
These contain:
108
109 bbfe7b6e Dirk Pattinson
In file CoAlgMisc.ml:
110
111 69a71d22 Thorsten Wißmann
  - 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 c49eea11 Thorsten Wißmann
    | C.HCCONSTN _ ->
123
      if func <> Constant || List.length sortlst <> 1
124
        then raise (C.CoAlgException "=-formula is used in wrong sort.")
125
        else ();
126 69a71d22 Thorsten Wißmann
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 bbfe7b6e Dirk Pattinson
In file CoAlgFormula.ml:
134
135
  - sizeFormula: determine the size of the tree representation of a
136
    formula
137
138 69a71d22 Thorsten Wißmann
  - 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 bbfe7b6e Dirk Pattinson
  - exportFormula_buffer: string representation of a formula
143
  - exportTatlFormula_buffer: used for ATL, you probably want to
144
    raise an exception here
145 69a71d22 Thorsten Wißmann
  - nnfNeg -- return the negated formula in nnf.
146 c49eea11 Thorsten Wißmann
  - nnf -- return the formula in nnf.
147
  - simplify -- simplifiy the formula
148
  - And other utility functions: equal_hcFormula_node, equal_hcFormula_node,
149 bbfe7b6e Dirk Pattinson
    hash_hcFormula_node (possibly extend the base value), toFml_hcFormula_node, negNde_hcFormula_node, hc_formula
150
151
152
In file CoAlgLogics.ml:
153 69a71d22 Thorsten Wißmann
154 bbfe7b6e Dirk Pattinson
  - getExpandingFunctionProduce: this is where you need to implement
155
    the actual logical rule.
156 69a71d22 Thorsten Wißmann
// vim: tw=80 ft=asciidoc