diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 54 |
1 files changed, 53 insertions, 1 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 57b93e7..fbf5ceb 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -1,5 +1,6 @@ open Ast open Core +open Lean module Environ = Map.Make (String) type environ = string Environ.t @@ -33,7 +34,7 @@ let extract_local_variables (env : environ) (q : query) : string list = | Every (Some _key, _value, _, _q) -> failwith "unimplemented" | Every (None, _value, _, _q) -> failwith "unimplemented" in - let handle_literal env = function + let handle_literal env : literal -> (environ * string list) = function | Exists (exprs, _) -> let env', ys = map_with_environment_updates env exprs handle_expr in (env', ys |> List.concat) @@ -46,3 +47,54 @@ let extract_local_variables (env : environ) (q : query) : string list = let extract_local_variables_wrapper (q : query) : string list = extract_local_variables Environ.empty q + +(* --- *) + +let term_of_object_key : object_key -> term = function + | Scalar s -> Scalar s + | Ref r -> Ref r + | Var v -> Var v + +let term_of_ref_target : ref_target -> term = function + | Var s -> Var s + | Array xs -> Array xs + | Object kvs -> Object kvs + | Set xs -> Set xs + | ArrayComprehension (key, q) -> ArrayComprehension (key, q) + | ObjectComprehension (key, q) -> ObjectComprehension (key, q) + | SetComprehension (key, q) -> SetComprehension (key, q) + | Call (fn, args) -> Call (fn, args) + +let rec compile_term env : term -> lean_expression = function + | Scalar s -> + (match s with + | String s -> Application (Identifier "Rego.Any.str", [String s]) + | Number x -> Application (Identifier "Rego.Any.num", [Number x]) + | Bool b -> Application (Identifier "Rego.Any.bool", [Bool b]) + | Null -> Application (Identifier "Rego.Any.null", [])) + | Var id -> Identifier (Map.find_exn env id) + | Ref (target, terms) -> + List.fold + terms + ~init:(compile_term env (term_of_ref_target target)) + ~f:(fun x y -> (Application ((Identifier "Rego.Any.deref"), [x; compile_term env y]))) + | Array xs -> + Application (Identifier "Rego.Any.array", List.map ~f:(compile_term env) xs) + | Set xs -> + Application (Identifier "Rego.Any.set", List.map ~f:(compile_term env) xs) + | Object kvs -> + let compile_kv = function + | (key, value) -> + Tuple [compile_term env (term_of_object_key key); + compile_term env value] + in + Application (Identifier "Rego.Any.object", List.map ~f:compile_kv kvs) + | ArrayComprehension (_term, _query) -> + failwith "unimplemented" + | SetComprehension (_term, _query) -> + failwith "unimplemented" + | ObjectComprehension ((_key, _value), _query) -> + failwith "unimplemented" + | Call (fn, args) -> + let head = compile_term env (Ref fn) in + Application (head, List.map ~f:(compile_term env) args) |