diff options
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/ast.ml | 40 |
1 files changed, 25 insertions, 15 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/ast.ml b/rego-proofs/compiler-rewrite/lib/ast.ml index 71257dc..387e1eb 100644 --- a/rego-proofs/compiler-rewrite/lib/ast.ml +++ b/rego-proofs/compiler-rewrite/lib/ast.ml @@ -153,12 +153,16 @@ and parse_literal tree : literal = in match tree |> member "terms" with | `List (func :: args) -> - Expr - ( Term - (Call - ( func |> member "value" |> to_list |> parse_ref, - List.map ~f:parse_term args )), - with_expr ) + let term = + Term + (Call + ( func |> member "value" |> to_list |> parse_ref, + List.map ~f:parse_term args )) + in + if tree |> member "negated" |> to_bool_or_false then + Negate (term, with_expr) + else Expr (term, with_expr) + | `List _ -> failwith "ill-formed call" | x -> if not (x |> member "symbols" |> is_null) then @@ -167,16 +171,22 @@ and parse_literal tree : literal = |> List.map ~f:(fun x -> Term (parse_term x)), with_expr ) else if x |> member "domain" |> is_null then - Expr (Term (parse_term x), with_expr) + let term = Term (parse_term x) in + if tree |> member "negated" |> to_bool_or_false then + Negate (term, with_expr) + else Expr (term, with_expr) else - Expr - ( Every - ( (if x |> member "key" |> is_null then None - else Some (x |> member "key" |> member "value" |> to_string)), - x |> member "value" |> member "value" |> to_string, - x |> member "domain" |> parse_term, - List.map ~f:parse_literal (x |> member "body" |> to_list) ), - with_expr ) + let term = + Every + ( (if x |> member "key" |> is_null then None + else Some (x |> member "key" |> member "value" |> to_string)), + x |> member "value" |> member "value" |> to_string, + x |> member "domain" |> parse_term, + List.map ~f:parse_literal (x |> member "body" |> to_list) ) + in + if tree |> member "negated" |> to_bool_or_false then + Negate (term, with_expr) + else Expr (term, with_expr) and parse_ref_target tree : ref_target = let term = parse_term tree in |