rego-proofs/compiler-rewrite/test/compiler_rewrite.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
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

open Core
open Compiler_rewrite

module To_test = struct
  let extract_locals = Compiler.extract_local_variables_wrapper
  let fmt = Lean.fmt_lean_expression
end

let strings =
  Alcotest.testable
    (Format.pp_print_list Format.pp_print_string)
    (List.equal String.equal)

let extract_query policy =
  match Ast.ast_of_string policy with
  | { policy = [ { body; _ } ]; _ } -> body
  | _ -> failwith "failed to parse"

let test_local_extraction_simple_1 () =
  let policy_code = {|
package test

q {
  x := 2
}
  |} in
  Alcotest.(check strings)
    "expected identifier list" [ "x" ]
    (To_test.extract_locals (extract_query policy_code))

let test_local_extraction_simple_2 () =
  let policy_code = {|
package test

q {
  x := 2
  y := 3
  z := 4
}
  |} in
  Alcotest.(check strings)
    "expected identifier list" [ "x"; "y"; "z" ]
    (To_test.extract_locals (extract_query policy_code))

let test_local_dependent_on_previously_defined_local () =
  let policy_code = {|
package test

q {
  x := 2
  y := x
}
  |} in
  Alcotest.(check strings)
    "expected identifier list" [ "x"; "y" ]
    (To_test.extract_locals (extract_query policy_code))

let test_local_not_ground_because_of_ordering () =
  let policy_code = {|
package test

q {
  y := x
  x := 2
}
  |} in
  Alcotest.(check strings)
    "expected identifier list" [ "x" ]
    (To_test.extract_locals (extract_query policy_code))

let test_identifier () =
  let open Compiler_rewrite.Lean in
  let ast = Identifier "test" in
  Alcotest.(check string) "expected string" "test" (To_test.fmt ast)

let () =
  let open Alcotest in
  run "Compiler"
    [
      ( "local extraction",
        [
          test_case "local extraction simple (1)" `Quick
            test_local_extraction_simple_1;
          test_case "local extraction simple (2)" `Quick
            test_local_extraction_simple_2;
          test_case
            "local extraction with local dependent on previously-defined local \
             (1)"
            `Quick test_local_dependent_on_previously_defined_local;
          test_case
            "local extraction with local dependent on previously-defined local \
             (2)"
            `Quick test_local_not_ground_because_of_ordering;
        ] );
      ( "ast formatting ",
        [ test_case "identifier compilation" `Quick test_identifier ] );
    ]