Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit b4474575 authored by MARCHE Claude's avatar MARCHE Claude

doc: finalize chapter 3 on API

parent 80cfd47a
......@@ -290,7 +290,7 @@ One can run provers on those tasks exactly as we did above.
\section{Operations on Terms and Formulas, Transformations}
The following code illustrates a simple recursive functions of
formulas. It explores the formula and when a negtion is found, it
formulas. It explores the formula and when a negation is found, it
tries to push it down below a conjunction, a disjunction or a
quantifier.
\lstinputlisting{transform__negate.ml}
......
......@@ -71,12 +71,14 @@ let param1 id ty = [Loc.dummy_position, Some id, false, Some ty]
let mk_tconst s =
mk_term
(Tconst
Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s }))
Number.(ConstInt { ic_negative = false ;
ic_abs = int_literal_dec s }))
let mk_econst s =
mk_expr
(Econst
Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s }))
Number.(ConstInt { ic_negative = false ;
ic_abs = int_literal_dec s }))
let mk_tapp f l = mk_term (Tidapp(f,l))
......@@ -118,7 +120,9 @@ let d1 : decl =
}
in
let body = mk_eapp mul_int [mk_evar id_x; mk_econst "7"] in
let f1 = Efun(param1 id_x int_type, None, Ity.MaskVisible, spec, body) in
let f1 =
Efun(param1 id_x int_type, None, Ity.MaskVisible, spec, body)
in
Dlet(mk_ident "f1",false,Expr.RKnone, mk_expr f1)
let () =
......@@ -246,7 +250,8 @@ let my_tasks : Task.task list =
let mods =
Wstdlib.Mstr.fold
(fun _ m acc ->
List.rev_append (Task.split_theory m.Pmodule.mod_theory None None) acc)
List.rev_append
(Task.split_theory m.Pmodule.mod_theory None None) acc)
mods []
in List.rev mods
......
......@@ -12,8 +12,8 @@ let rec negate (t:term) : term =
| Ttrue -> t_false
| Tfalse -> t_true
| Tnot t -> t
| Tbinop(Tand,t1,t2) -> t_and (negate t1) (negate t2)
| Tbinop(Tor,t1,t2) -> t_or (negate t1) (negate t2)
| Tbinop(Tand,t1,t2) -> t_or (negate t1) (negate t2)
| Tbinop(Tor,t1,t2) -> t_and (negate t1) (negate t2)
| Tquant(Tforall,tq) ->
let vars,triggers,t' = t_open_quant tq in
let tq' = t_close_quant vars triggers (negate t') in
......@@ -24,7 +24,10 @@ let rec negate (t:term) : term =
t_forall tq'
| _ -> t_not t
let traverse (t:term) : term = t_map negate t
let rec traverse (t:term) : term =
match t.t_node with
| Tnot t -> t_map traverse (negate t)
| _ -> t_map traverse t
(* END{negate} *)
(* BEGIN{register} *)
......@@ -33,6 +36,7 @@ let negate_goal pr t = [Decl.create_prop_decl Decl.Pgoal pr (traverse t)]
let negate_trans = Trans.goal negate_goal
let () = Trans.register_transform
"push_negation_down" negate_trans
~desc:"In the current goal, push negation down, across logical connectives."
"push_negations_down" negate_trans
~desc:"In the current goal,@ push negations down,@ \
across logical connectives."
(* END{register} *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment