use_api.ml 3 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
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
115
116
117
118
119
120
121
122
123
124


(*
*)


open Why
open Format

(***************

This file builds some goals using the API and calls
the alt-ergo prover to check them

******************)

(* First, we need to access the Why configuration *)

let config = Whyconf.read_config None
let main = Whyconf.get_main config
let env = Env.create_env (Lexer.retrieve main.Whyconf.loadpath) 

let provers = Whyconf.get_provers config

let alt_ergo = 
  try
    Util.Mstr.find "alt-ergo" provers 
  with Not_found ->
    eprintf "Prover alt-ergo not installed or not configured@.";
    failwith "Cannot continue without alt-ergo installed"

let alt_ergo_driver = Driver.load_driver env alt_ergo.Whyconf.driver


(*

a ground propositional goal: True or False

*)

let fmla_true = Term.f_true
let fmla_false = Term.f_false
let fmla1 = Term.f_or fmla_true fmla_false
let () = printf "@[formula 1 created:@ %a@]@." Pretty.print_fmla fmla1

let task1 = None

let goal_id1 = Decl.create_prsymbol (Ident.id_fresh "goal1") 
let task1 = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1

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

let result1 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task1 ()

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

(*

a propositional goal: A and B implies B

*)

let prop_var_A = Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B = Term.create_psymbol (Ident.id_fresh "B") []
let fmla_A = Term.f_app prop_var_A []
let fmla_B = Term.f_app prop_var_B []
let fmla2 = Term.f_implies (Term.f_and fmla_A fmla_B) fmla_B
let () = printf "@[formula 2 created:@ %a@]@." Pretty.print_fmla fmla2

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

let result2 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task2 ()

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

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

let result3 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task3 ()

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


(* build a theory with all these goals *)