diff options
| author | Jakob L. Kreuze | 2023-11-02 16:27:03 -0400 |
|---|---|---|
| committer | Jakob L. Kreuze | 2023-11-02 16:27:03 -0400 |
| commit | 686c6862c8c7c60ccb62da4bab89742c72180e03 (patch) | |
| tree | 5ca57d73f681f45c372260f83a261d6463b03a3f | |
| parent | eda0f85ece5d772a7c72d10baafa92f12a8d931f (diff) | |
Parse Negate properly
| -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 |