Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

use_api.ml 3.58 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
(***************
MARCHE Claude's avatar
MARCHE Claude committed
2

MARCHE Claude's avatar
MARCHE Claude committed
3 4
This file builds some goals using the API and calls
the alt-ergo prover to check them
MARCHE Claude's avatar
MARCHE Claude committed
5

MARCHE Claude's avatar
MARCHE Claude committed
6
******************)
MARCHE Claude's avatar
MARCHE Claude committed
7

MARCHE Claude's avatar
MARCHE Claude committed
8
(* opening the Why3 library *)
MARCHE Claude's avatar
MARCHE Claude committed
9
open Why
MARCHE Claude's avatar
MARCHE Claude committed
10 11 12 13 14 15 16

(* a ground propositional goal: true or false *)
let fmla_true : Term.fmla = Term.f_true
let fmla_false : Term.fmla = Term.f_false
let fmla1 : Term.fmla = Term.f_or fmla_true fmla_false

(* printing it *)
MARCHE Claude's avatar
MARCHE Claude committed
17
open Format
MARCHE Claude's avatar
MARCHE Claude committed
18
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_fmla fmla1
MARCHE Claude's avatar
MARCHE Claude committed
19 20


MARCHE Claude's avatar
MARCHE Claude committed
21 22 23 24 25 26 27 28
(* a propositional goal: A and B implies A *)

let prop_var_A : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "B") []
let atom_A : Term.fmla = Term.f_app prop_var_A []
let atom_B : Term.fmla = Term.f_app prop_var_B []
let fmla2 : Term.fmla = Term.f_implies (Term.f_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_fmla fmla2
MARCHE Claude's avatar
MARCHE Claude committed
29 30


31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
(* building the task for formula 1 alone *)
let task1 : Task.task = None (* empty task *)
let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1") 
let task1 : Task.task = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1

(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1

(* task for formula 2 *)
let task2 = None
let task2 = Task.add_logic_decl task2 [prop_var_A, None] 
let task2 = Task.add_logic_decl task2 [prop_var_B, None] 
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2") 
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2

let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2



(* To call a prover, we need to access the Why configuration *)
MARCHE Claude's avatar
MARCHE Claude committed
51

MARCHE Claude's avatar
MARCHE Claude committed
52
(* reads the config file *)
MARCHE Claude's avatar
MARCHE Claude committed
53
let config = Whyconf.read_config None
MARCHE Claude's avatar
MARCHE Claude committed
54 55

(* the [main] section of the config file *)
MARCHE Claude's avatar
MARCHE Claude committed
56
let main = Whyconf.get_main config
MARCHE Claude's avatar
MARCHE Claude committed
57 58

(* builds the environment from the [loadpath] *)
59
let env = Env.create_env (Lexer.retrieve (Whyconf.loadpath main)) 
MARCHE Claude's avatar
MARCHE Claude committed
60

MARCHE Claude's avatar
MARCHE Claude committed
61
(* the [provers] of the config file *)
MARCHE Claude's avatar
MARCHE Claude committed
62 63
let provers = Whyconf.get_provers config

MARCHE Claude's avatar
MARCHE Claude committed
64
(* the [prover alt-ergo] section of the config file *)
MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68 69
let alt_ergo = 
  try
    Util.Mstr.find "alt-ergo" provers 
  with Not_found ->
    eprintf "Prover alt-ergo not installed or not configured@.";
MARCHE Claude's avatar
MARCHE Claude committed
70
    exit 0
MARCHE Claude's avatar
MARCHE Claude committed
71

MARCHE Claude's avatar
MARCHE Claude committed
72
(* loading the Alt-Ergo driver *)
MARCHE Claude's avatar
MARCHE Claude committed
73 74
let alt_ergo_driver = Driver.load_driver env alt_ergo.Whyconf.driver

MARCHE Claude's avatar
MARCHE Claude committed
75
(* call Alt-Ergo *)
MARCHE Claude's avatar
MARCHE Claude committed
76 77
let result1 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
78
    alt_ergo_driver task1 () ()
MARCHE Claude's avatar
MARCHE Claude committed
79

MARCHE Claude's avatar
MARCHE Claude committed
80
(* prints Alt-Ergo answer *)
MARCHE Claude's avatar
MARCHE Claude committed
81 82 83 84 85
let () = printf "@[On task 1, alt-ergo answers %a@."
  Call_provers.print_prover_result result1

let result2 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
86
    alt_ergo_driver task2 () ()
MARCHE Claude's avatar
MARCHE Claude committed
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114

let () = printf "@[On task 2, alt-ergo answers %a@."
  Call_provers.print_prover_result result2



(*

An arithmetic goal: 2+2 = 4

*)

let two = Term.t_const (Term.ConstInt "2")
let four = Term.t_const (Term.ConstInt "4")

let int_theory = Env.find_theory env ["int"] "Int"

let plus_symbol = Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]

let two_plus_two = Term.t_app plus_symbol [two;two] Ty.ty_int

let fmla3 = Term.f_equ two_plus_two four

let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3") 
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3

MARCHE Claude's avatar
MARCHE Claude committed
115
(*
MARCHE Claude's avatar
MARCHE Claude committed
116
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
MARCHE Claude's avatar
MARCHE Claude committed
117 118
*)
let () = printf "@[task 3 created@]@." 
MARCHE Claude's avatar
MARCHE Claude committed
119 120 121

let result3 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
122
    alt_ergo_driver task3 () ()
MARCHE Claude's avatar
MARCHE Claude committed
123 124 125 126 127 128 129 130

let () = printf "@[On task 3, alt-ergo answers %a@."
  Call_provers.print_prover_result result3


(* build a theory with all these goals *)