-
Notifications
You must be signed in to change notification settings - Fork 4
/
checkproof.ml
54 lines (48 loc) · 1.38 KB
/
checkproof.ml
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
open MParser
open MParser_PCRE
open Lib
open Parsers
open Soundcheck
let () = do_debug := true
let usage = "usage: " ^ Sys.argv.(0) ^ " [abstract proof]"
let parse_proof st =
let parse_node st =
( Tokens.parens (
Tokens.integer >>= (fun id ->
spaces >> Tokens.comma >> spaces >>
(parse_list Tokens.integer) >>= (fun tags ->
spaces >> Tokens.comma >> spaces >>
(parse_list (
Tokens.parens (
Tokens.integer >>= (fun target ->
spaces >> Tokens.comma >> spaces >>
(parse_list
(parse_pair Tokens.integer Tokens.integer)) >>= (fun all_pairs ->
spaces >> Tokens.comma >> spaces >>
(parse_list (parse_pair Tokens.integer Tokens.integer)) |>>
(fun prog_pairs -> (target, all_pairs, prog_pairs))))))) |>>
(fun children -> (id, tags, children))))) ) st in
( parse_list parse_node ) st
let () =
gc_setup() ;
Format.set_margin (Sys.command "exit $(tput cols)") ;
if Array.length Sys.argv <> 2 then
begin
print_endline usage ;
exit 1
end
else
let prf_string = Sys.argv.(1) in
let prf = handle_reply (parse_string parse_proof prf_string ()) in
let prf = build_proof prf in
let res = check_proof prf in
if res then
begin
print_endline "Proof is valid" ;
exit 0 ;
end
else
begin
print_endline "Proof is NOT valid" ;
exit 1 ;
end