api.tex 13.4 KB
 MARCHE Claude committed Jul 02, 2011 1 \chapter{The \why API} Jean-Christophe Filliâtre committed Aug 21, 2012 2 \label{chap:api}\index{API} MARCHE Claude committed Sep 06, 2010 3 Andrei Paskevich committed Dec 20, 2010 4 This chapter is a tutorial for the users who want to link their own MARCHE Claude committed Jul 02, 2011 5 OCaml code with the \why library. We progressively introduce the way MARCHE Claude committed Dec 08, 2010 6 7 one can use the library to build terms, formulas, theories, proof tasks, call external provers on tasks, and apply transformations on Andrei Paskevich committed Dec 20, 2010 8 tasks. The complete documentation for API calls is given MARCHE Claude committed Jul 02, 2011 9 at URL~\url{http://why3.lri.fr/api/}. MARCHE Claude committed Dec 08, 2010 10 MARCHE Claude committed Dec 16, 2010 11 We assume the reader has a fair knowledge of the OCaml MARCHE Claude committed Jul 02, 2011 12 language. Notice that the \why library must be installed, see MARCHE Claude committed Jul 02, 2011 13 14 Section~\ref{sec:installlib}. The OCaml code given below is available in the source distribution as \url{examples/use_api.ml}. MARCHE Claude committed Sep 06, 2010 15 MARCHE Claude committed Dec 08, 2010 16 17 18 19 20 21 \section{Building Propositional Formulas} The first step is to know how to build propositional formulas. The module \texttt{Term} gives a few functions for building these. Here is a piece of OCaml code for building the formula $true \lor false$. Guillaume Melquiond committed Sep 21, 2012 22 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 23 (* opening the Why3 library *) Andrei Paskevich committed Jul 02, 2011 24 open Why3 MARCHE Claude committed Dec 08, 2010 25 26 (* a ground propositional goal: true or false *) Andrei Paskevich committed Jun 18, 2011 27 28 29 let fmla_true : Term.term = Term.t_true let fmla_false : Term.term = Term.t_false let fmla1 : Term.term = Term.t_or fmla_true fmla_false Guillaume Melquiond committed Sep 21, 2012 30 \end{ocamlcode} Andrei Paskevich committed Jun 18, 2011 31 The library uses the common type \texttt{term} both for terms Guillaume Melquiond committed Oct 11, 2012 32 33 (\ie expressions that produce a value of some particular type) and formulas (\ie boolean-valued expressions). Andrei Paskevich committed Jun 18, 2011 34 35 36 37 % To distinguish terms from formulas, one can look at the % \texttt{t_ty} field of the \texttt{term} record: in formulas, % this field has the value \texttt{None}, and in terms, % \texttt{Some t}, where \texttt{t} is of type \texttt{Ty.ty}. MARCHE Claude committed Dec 08, 2010 38 39 40 Such a formula can be printed using the module \texttt{Pretty} providing pretty-printers. Guillaume Melquiond committed Sep 21, 2012 41 \begin{ocamlcode} Andrei Paskevich committed Jun 18, 2011 42 (* printing it *) MARCHE Claude committed Dec 08, 2010 43 open Format Andrei Paskevich committed Jun 18, 2011 44 let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1 Guillaume Melquiond committed Sep 21, 2012 45 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 46 47 48 49 50 51 52 53 54 Assuming the lines above are written in a file \texttt{f.ml}, it can be compiled using \begin{verbatim} ocamlc str.cma unix.cma nums.cma dynlink.cma \ -I +ocamlgraph -I +why3 graph.cma why.cma f.ml -o f \end{verbatim} Running the generated executable \texttt{f} results in the following output. \begin{verbatim} Andrei Paskevich committed Jun 30, 2011 55 formula 1 is: true \/ false MARCHE Claude committed Dec 08, 2010 56 57 58 59 60 \end{verbatim} Let's now build a formula with propositional variables: $A \land B \rightarrow A$. Propositional variables must be declared first before using them in formulas. This is done as follows. Guillaume Melquiond committed Sep 21, 2012 61 \begin{ocamlcode} Andrei Paskevich committed Dec 20, 2010 62 let prop_var_A : Term.lsymbol = MARCHE Claude committed Dec 08, 2010 63 Term.create_psymbol (Ident.id_fresh "A") [] Andrei Paskevich committed Dec 20, 2010 64 let prop_var_B : Term.lsymbol = MARCHE Claude committed Dec 08, 2010 65 Term.create_psymbol (Ident.id_fresh "B") [] Guillaume Melquiond committed Sep 21, 2012 66 \end{ocamlcode} Andrei Paskevich committed Jun 18, 2011 67 68 69 70 The type \texttt{lsymbol} is the type of function and predicate symbols (which we call logic symbols for brevity). Then the atoms $A$ and $B$ must be built by the general function for applying a predicate symbol to a list of terms. Here we just need the empty list of arguments. Guillaume Melquiond committed Sep 21, 2012 71 \begin{ocamlcode} Andrei Paskevich committed Jun 18, 2011 72 73 74 75 76 let atom_A : Term.term = Term.ps_app prop_var_A [] let atom_B : Term.term = Term.ps_app prop_var_B [] let fmla2 : Term.term = Term.t_implies (Term.t_and atom_A atom_B) atom_A let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2 Guillaume Melquiond committed Sep 21, 2012 77 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 78 79 80 As expected, the output is as follows. \begin{verbatim} Andrei Paskevich committed Jun 30, 2011 81 formula 2 is: A /\ B -> A MARCHE Claude committed Dec 08, 2010 82 \end{verbatim} Andrei Paskevich committed Jul 02, 2011 83 84 85 86 Notice that the concrete syntax of \why forbids function and predicate names to start with a capital letter (except for the algebraic type constructors which must start with one). This constraint is not enforced when building those directly using library calls. MARCHE Claude committed Dec 08, 2010 87 MARCHE Claude committed Dec 17, 2010 88 \section{Building Tasks} MARCHE Claude committed Dec 08, 2010 89 90 91 92 93 Let's see how we can call a prover to prove a formula. As said in previous chapters, a prover must be given a task, so we need to build tasks from our formulas. Task can be build incrementally from an empty task by adding declaration to it, using the functions Andrei Paskevich committed Dec 20, 2010 94 \texttt{add\_*\_decl} of module \texttt{Task}. For the formula $true \lor MARCHE Claude committed Dec 08, 2010 95 false$ above, this is done as follows. Guillaume Melquiond committed Sep 21, 2012 96 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 97 let task1 : Task.task = None (* empty task *) Andrei Paskevich committed Dec 20, 2010 98 99 100 let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1") let task1 : Task.task = MARCHE Claude committed Dec 08, 2010 101 Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1 Guillaume Melquiond committed Sep 21, 2012 102 \end{ocamlcode} Guillaume Melquiond committed Oct 30, 2012 103 To make the formula a goal, we must give a name to it, here goal1''. A MARCHE Claude committed Dec 08, 2010 104 105 goal name has type \texttt{prsymbol}, for identifiers denoting propositions in a theory or a task. Notice again that the concrete MARCHE Claude committed Jul 02, 2011 106 syntax of \why requires these symbols to be capitalized, but it is not MARCHE Claude committed Dec 08, 2010 107 108 mandatory when using the library. The second argument of \texttt{add\_prop\_decl} is the kind of the proposition: Andrei Paskevich committed Dec 20, 2010 109 110 111 \texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal} (notice, however, that lemmas are not allowed in tasks and can only be used in theories). MARCHE Claude committed Dec 08, 2010 112 113 Andrei Paskevich committed Dec 20, 2010 114 Once a task is built, it can be printed. Guillaume Melquiond committed Sep 21, 2012 115 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 116 117 (* printing the task *) let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1 Guillaume Melquiond committed Sep 21, 2012 118 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 119 Andrei Paskevich committed Dec 20, 2010 120 The task for our second formula is a bit more complex to build, because Guillaume Melquiond committed Oct 11, 2012 121 the variables A and B must be added as abstract (\ie not defined) Andrei Paskevich committed Mar 18, 2012 122 propositional symbols in the task. Guillaume Melquiond committed Sep 21, 2012 123 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 124 125 (* task for formula 2 *) let task2 = None Andrei Paskevich committed Mar 18, 2012 126 127 let task2 = Task.add_param_decl task2 prop_var_A let task2 = Task.add_param_decl task2 prop_var_B Andrei Paskevich committed Dec 20, 2010 128 let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2") MARCHE Claude committed Dec 08, 2010 129 130 let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2 let () = printf "@[task 2 is:@\n%a@]@." Pretty.print_task task2 Guillaume Melquiond committed Sep 21, 2012 131 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 132 133 134 135 136 Execution of our OCaml program now outputs: \begin{verbatim} task 1 is: theory Task Andrei Paskevich committed Jun 30, 2011 137 goal Goal1 : true \/ false MARCHE Claude committed Dec 08, 2010 138 139 140 141 end task 2 is: theory Task Andrei Paskevich committed Jun 30, 2011 142 predicate A Andrei Paskevich committed Dec 20, 2010 143 Andrei Paskevich committed Jun 30, 2011 144 predicate B Andrei Paskevich committed Dec 20, 2010 145 Andrei Paskevich committed Jun 30, 2011 146 goal Goal2 : A /\ B -> A MARCHE Claude committed Dec 08, 2010 147 148 149 150 end \end{verbatim} \section{Calling External Provers} MARCHE Claude committed Sep 06, 2010 151 MARCHE Claude committed Dec 08, 2010 152 To call an external prover, we need to access the Why configuration Andrei Paskevich committed Jul 02, 2011 153 file \texttt{why3.conf}, as it was built using the \texttt{why3config} MARCHE Claude committed Dec 08, 2010 154 155 156 command line tool or the \textsf{Detect Provers} menu of the graphical IDE. The following API calls allow to access the content of this configuration file. Guillaume Melquiond committed Sep 21, 2012 157 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 158 159 160 161 162 (* reads the config file *) let config : Whyconf.config = Whyconf.read_config None (* the [main] section of the config file *) let main : Whyconf.main = Whyconf.get_main config (* all the provers detected, from the config file *) François Bobot committed Jan 25, 2012 163 let provers : Whyconf.config_prover Whyconf.Mprover.t = MARCHE Claude committed Dec 08, 2010 164 Whyconf.get_provers config Guillaume Melquiond committed Sep 21, 2012 165 \end{ocamlcode} François Bobot committed Jan 25, 2012 166 167 168 169 170 The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A provers is a record with a name, a version and an alternative description (if someone want to compare different command line options of the same provers for example). It's definition is in the module \texttt{Whyconf} : Guillaume Melquiond committed Sep 21, 2012 171 \begin{ocamlcode} François Bobot committed Jan 25, 2012 172 173 174 175 176 type prover = { prover_name : string; (* "Alt-Ergo" *) prover_version : string; (* "2.95" *) prover_altern : string; (* "special" *) } Guillaume Melquiond committed Sep 21, 2012 177 \end{ocamlcode} François Bobot committed Jan 25, 2012 178 179 The map \texttt{provers} provides the set of existing provers. In the following, we directly MARCHE Claude committed Dec 16, 2010 180 181 attempt to access the prover Alt-Ergo, which is known to be identified with id \texttt{"alt-ergo"}. Guillaume Melquiond committed Sep 21, 2012 182 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 183 (* the [prover alt-ergo] section of the config file *) Andrei Paskevich committed Dec 20, 2010 184 let alt_ergo : Whyconf.config_prover = MARCHE Claude committed Dec 08, 2010 185 try François Bobot committed Jan 25, 2012 186 187 188 189 Whyconf.prover_by_id config "alt-ergo" with Whyconf.ProverNotFound _ -> eprintf "Prover alt-ergo not installed or not configured@."; exit 0 Guillaume Melquiond committed Sep 21, 2012 190 \end{ocamlcode} François Bobot committed Jan 25, 2012 191 We could also get a specific version with : Guillaume Melquiond committed Sep 21, 2012 192 \begin{ocamlcode} François Bobot committed Jan 25, 2012 193 194 195 196 197 198 let alt_ergo : Whyconf.config_prover = try let prover = {Whyconf.prover_name = "Alt-Ergo"; prover_version = "0.92.3"; prover_altern = ""} in Whyconf.Mprover.find prover provers MARCHE Claude committed Dec 08, 2010 199 200 201 with Not_found -> eprintf "Prover alt-ergo not installed or not configured@."; exit 0 Guillaume Melquiond committed Sep 21, 2012 202 \end{ocamlcode} MARCHE Claude committed Sep 06, 2010 203 MARCHE Claude committed Dec 16, 2010 204 205 206 The next step is to obtain the driver associated to this prover. A driver typically depends on the standard theories so these should be loaded first. Guillaume Melquiond committed Sep 21, 2012 207 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 208 (* builds the environment from the [loadpath] *) Andrei Paskevich committed Dec 20, 2010 209 let env : Env.env = Andrei Paskevich committed Sep 30, 2011 210 Env.create_env (Whyconf.loadpath main) MARCHE Claude committed Dec 08, 2010 211 (* loading the Alt-Ergo driver *) Andrei Paskevich committed Dec 20, 2010 212 let alt_ergo_driver : Driver.driver = MARCHE Claude committed Jul 02, 2011 213 214 215 216 217 218 try Driver.load_driver env alt_ergo.Whyconf.driver with e -> eprintf "Failed to load driver for alt-ergo: %a@." Exn_printer.exn_printer e; exit 1 Guillaume Melquiond committed Sep 21, 2012 219 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 220 221 222 We are now ready to call the prover on the tasks. This is done by a function call that launches the external executable and waits for its Andrei Paskevich committed Dec 20, 2010 223 termination. Here is a simple way to proceed: Guillaume Melquiond committed Sep 21, 2012 224 \begin{ocamlcode} Andrei Paskevich committed Dec 20, 2010 225 226 (* calls Alt-Ergo *) let result1 : Call_provers.prover_result = Jean-Christophe Filliâtre committed Feb 24, 2011 227 228 229 Call_provers.wait_on_call (Driver.prove_task ~command:alt_ergo.Whyconf.command alt_ergo_driver task1 ()) () MARCHE Claude committed Dec 08, 2010 230 (* prints Alt-Ergo answer *) Andrei Paskevich committed Dec 20, 2010 231 let () = printf "@[On task 1, alt-ergo answers %a@]@." MARCHE Claude committed Dec 08, 2010 232 Call_provers.print_prover_result result1 Guillaume Melquiond committed Sep 21, 2012 233 \end{ocamlcode} Andrei Paskevich committed Dec 20, 2010 234 This way to call a prover is in general too naive, since it may never MARCHE Claude committed Dec 16, 2010 235 236 237 238 239 return if the prover runs without time limit. The function \texttt{prove\_task} has two optional parameters: \texttt{timelimit} is the maximum allowed running time in seconds, and \texttt{memlimit} is the maximum allowed memory in megabytes. The type \texttt{prover\_result} is a record with three fields: MARCHE Claude committed Dec 08, 2010 240 \begin{itemize} Andrei Paskevich committed Dec 20, 2010 241 \item \texttt{pr\_answer}: the prover answer, explained below; Guillaume Melquiond committed Oct 11, 2012 242 \item \texttt{pr\_output}: the output of the prover, \ie both MARCHE Claude committed Dec 16, 2010 243 standard output and the standard error of the process Andrei Paskevich committed Jul 02, 2011 244 (a redirection in \texttt{why3.conf} is required); Andrei Paskevich committed Dec 20, 2010 245 \item \texttt{pr\_time} : the time taken by the prover, in seconds. MARCHE Claude committed Dec 08, 2010 246 \end{itemize} Andrei Paskevich committed Dec 20, 2010 247 A \texttt{pr\_answer} is a sum of several kind of answers: MARCHE Claude committed Dec 08, 2010 248 249 250 \begin{itemize} \item \texttt{Valid}: the task is valid according to the prover. \item \texttt{Invalid}: the task is invalid. Andrei Paskevich committed Dec 20, 2010 251 \item \texttt{Timeout}: the prover exceeds the time or memory limit. MARCHE Claude committed Dec 16, 2010 252 \item \texttt{Unknown} $msg$: the prover can't determine if the task Andrei Paskevich committed Dec 20, 2010 253 is valid; the string parameter $msg$ indicates some extra MARCHE Claude committed Dec 16, 2010 254 information. Guillaume Melquiond committed Oct 11, 2012 255 \item \texttt{Failure} $msg$: the prover reports a failure, \ie it MARCHE Claude committed Dec 16, 2010 256 257 was unable to read correctly its input task. \item \texttt{HighFailure}: an error occurred while trying to call the Guillaume Melquiond committed Oct 11, 2012 258 prover, or the prover answer was not understood (\ie none of the Andrei Paskevich committed Dec 20, 2010 259 260 given regular expressions in the driver file matches the output of the prover). MARCHE Claude committed Dec 08, 2010 261 \end{itemize} MARCHE Claude committed Dec 16, 2010 262 263 Here is thus another way of calling the Alt-Ergo prover, on our second task. Guillaume Melquiond committed Sep 21, 2012 264 \begin{ocamlcode} Andrei Paskevich committed Dec 20, 2010 265 let result2 : Call_provers.prover_result = Jean-Christophe Filliâtre committed Feb 24, 2011 266 267 Call_provers.wait_on_call (Driver.prove_task ~command:alt_ergo.Whyconf.command MARCHE Claude committed Dec 08, 2010 268 ~timelimit:10 Jean-Christophe Filliâtre committed Feb 24, 2011 269 alt_ergo_driver task2 ()) () MARCHE Claude committed Dec 08, 2010 270 Andrei Paskevich committed Dec 20, 2010 271 let () = MARCHE Claude committed Dec 08, 2010 272 printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@." Andrei Paskevich committed Dec 20, 2010 273 Call_provers.print_prover_answer MARCHE Claude committed Dec 08, 2010 274 275 result1.Call_provers.pr_answer result1.Call_provers.pr_time Guillaume Melquiond committed Sep 21, 2012 276 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 277 278 279 280 281 282 283 The output of our program is now as follows. \begin{verbatim} On task 1, alt-ergo answers Valid (0.01s) On task 2, alt-ergo answers Valid in 0.01 seconds \end{verbatim} \section{Building Terms} MARCHE Claude committed Dec 08, 2010 284 285 286 287 288 An important feature of the functions for building terms and formulas is that they statically guarantee that only well-typed terms can be constructed. Andrei Paskevich committed Dec 20, 2010 289 Here is the way we build the formula $2+2=4$. The main difficulty is to MARCHE Claude committed Dec 09, 2010 290 291 access the internal identifier for addition: it must be retrieved from the standard theory \texttt{Int} of the file \texttt{int.why} (see MARCHE Claude committed Dec 13, 2010 292 Chap~\ref{chap:library}). Guillaume Melquiond committed Sep 21, 2012 293 \begin{ocamlcode} MARCHE Claude committed Jun 20, 2012 294 295 let two : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "2")) let four : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "4")) Andrei Paskevich committed Dec 20, 2010 296 let int_theory : Theory.theory = MARCHE Claude committed Dec 08, 2010 297 Env.find_theory env ["int"] "Int" Andrei Paskevich committed Dec 20, 2010 298 let plus_symbol : Term.lsymbol = MARCHE Claude committed Dec 08, 2010 299 Theory.ns_find_ls int_theory.Theory.th_export ["infix +"] Andrei Paskevich committed Dec 20, 2010 300 301 let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two] Andrei Paskevich committed Jun 18, 2011 302 let fmla3 : Term.term = Term.t_equ two_plus_two four Guillaume Melquiond committed Sep 21, 2012 303 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 304 305 306 An important point to notice as that when building the application of $+$ to the arguments, it is checked that the types are correct. Indeed the constructor \texttt{t\_app\_infer} infers the type of the resulting MARCHE Claude committed Dec 09, 2010 307 term. One could also provide the expected type as follows. Guillaume Melquiond committed Sep 21, 2012 308 \begin{ocamlcode} Andrei Paskevich committed Dec 20, 2010 309 let two_plus_two : Term.term = Andrei Paskevich committed Jun 18, 2011 310 Term.fs_app plus_symbol [two;two] Ty.ty_int Guillaume Melquiond committed Sep 21, 2012 311 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 312 Andrei Paskevich committed Dec 20, 2010 313 314 When building a task with this formula, we need to declare that we use theory \texttt{Int}: Guillaume Melquiond committed Sep 21, 2012 315 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 316 317 let task3 = None let task3 = Task.use_export task3 int_theory Andrei Paskevich committed Dec 20, 2010 318 let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3") MARCHE Claude committed Dec 08, 2010 319 let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3 Guillaume Melquiond committed Sep 21, 2012 320 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 321 322 323 \section{Building Quantified Formulas} Andrei Paskevich committed Dec 20, 2010 324 325 326 To illustrate how to build quantified formulas, let us consider the formula $\forall x:int. x*x \geq 0$. The first step is to obtain the symbols from \texttt{Int}. Guillaume Melquiond committed Sep 21, 2012 327 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 328 let zero : Term.term = Term.t_const (Term.ConstInt "0") Andrei Paskevich committed Dec 20, 2010 329 let mult_symbol : Term.lsymbol = MARCHE Claude committed Dec 08, 2010 330 Theory.ns_find_ls int_theory.Theory.th_export ["infix *"] Andrei Paskevich committed Dec 20, 2010 331 let ge_symbol : Term.lsymbol = MARCHE Claude committed Dec 08, 2010 332 Theory.ns_find_ls int_theory.Theory.th_export ["infix >="] Guillaume Melquiond committed Sep 21, 2012 333 \end{ocamlcode} MARCHE Claude committed Dec 08, 2010 334 The next step is to introduce the variable $x$ with the type int. Guillaume Melquiond committed Sep 21, 2012 335 \begin{ocamlcode} Andrei Paskevich committed Dec 20, 2010 336 let var_x : Term.vsymbol = MARCHE Claude committed Dec 08, 2010 337 Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int Guillaume Melquiond committed Sep 21, 2012 338 \end{ocamlcode} Andrei Paskevich committed Dec 20, 2010 339 The formula $x*x \geq 0$ is obtained as in the previous example. Guillaume Melquiond committed Sep 21, 2012 340 \begin{ocamlcode} MARCHE Claude committed Dec 08, 2010 341 let x : Term.term = Term.t_var var_x Andrei Paskevich committed Dec 20, 2010 342 let x_times_x : Term.term = Term.t_app_infer mult_symbol [x;x] Andrei Paskevich committed Jun 18, 2011 343 let fmla4_aux : Term.term = Term.ps_app ge_symbol [x_times_x;zero] Guillaume Melquiond committed Sep 21, 2012 344 \end{ocamlcode} MARCHE Claude committed Jul 02, 2011 345 To quantify on $x$, we use the appropriate smart constructor as follows. Guillaume Melquiond committed Sep 21, 2012 346 \begin{ocamlcode} MARCHE Claude committed Jul 02, 2011 347 let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux Guillaume Melquiond committed Sep 21, 2012 348 \end{ocamlcode} Andrei Paskevich committed Dec 20, 2010 349 MARCHE Claude committed Dec 08, 2010 350 351 \section{Building Theories} MARCHE Claude committed Dec 15, 2010 352 [TO BE COMPLETED] MARCHE Claude committed Dec 08, 2010 353 MARCHE Claude committed Sep 06, 2010 354 355 \section{Applying transformations} MARCHE Claude committed Dec 15, 2010 356 [TO BE COMPLETED] MARCHE Claude committed Dec 08, 2010 357 358 359 \section{Writing new functions on term} MARCHE Claude committed Dec 15, 2010 360 361 362 363 364 [TO BE COMPLETED] % pattern-matching on terms, opening a quantifier MARCHE Claude committed Dec 08, 2010 365 MARCHE Claude committed Sep 06, 2010 366 367 368 369 370 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: