cool / HACKING @ master
History  View  Annotate  Download (5.24 KB)
1 
// * mode: adoc; fillcolumn: 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/unittests`. 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 
`./cooltestsuite.native` and `./cool_unit_tests.native` respectively. 
24  
25 
If unit tests are not being build, use 
26  
27 
ocaml setup.ml configure enabletests 
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 mlifile. 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 nonexhaustive 
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 nonexhaustive 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 