diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 45 |
1 files changed, 35 insertions, 10 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index ecc7162..5c89807 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -10,6 +10,13 @@ type variable = { lean_id : string; module Environ = Map.Make (String) type environ = variable Environ.t +let extend_environment (env : environ) (vars : (string * variable) list) = + Environ.of_alist_exn vars + |> Map.merge env ~f:(fun ~key:_key -> function + | `Right v -> Some v + | `Left v -> Some v + | `Both (_, v) -> Some v) + let term_of_object_key : object_key -> term = function | Scalar s -> Scalar s | Ref r -> Ref r @@ -117,6 +124,18 @@ let gensym : string -> string = counter := !counter + 1 ; Printf.sprintf "%s__%d" base number +let rec transform_rule_with_ref_head : rule -> rule list = function + (* Base case - this is a simple reference that we can deal with. *) + | { head = ((_, []), _); _ } | { head = ((_, [_]), _); _ } as rule -> + [rule] + | { head = ((tgt, xs), rhs); _ } as rule -> + let tail = List.last_exn xs in + let name = gensym "anonymous" in + [{ rule with head = ((Var name, [tail]), rhs) }] @ + transform_rule_with_ref_head { rule with head = ((tgt, List.drop_last_exn xs), Assignment (Assign, Var name)) } + +(* --- *) + let rec compile_term env : term -> lean_expression = function | Scalar s -> @@ -216,14 +235,11 @@ and compile_literal env : literal -> (environ * lean_expression) = function and compile_query env literals : (environ * lean_expression) = let { free; bound; _ } = extract_variables env literals in - let env' = List.map free ~f:(fun name -> (name, { lean_id = gensym name; complete = true; assigned = true })) - |> List.append - (List.map bound ~f:(fun name -> (name, { lean_id = gensym name; complete = true; assigned = false }))) - |> Environ.of_alist_exn - |> Map.merge env ~f:(fun ~key:_key -> function - | `Right v -> Some v - | `Left v -> Some v - | `Both (_, v) -> Some v) in + let env' = + List.append + (List.map free ~f:(fun name -> (name, { lean_id = gensym name; complete = true; assigned = true }))) + (List.map bound ~f:(fun name -> (name, { lean_id = gensym name; complete = true; assigned = false }))) + |> extend_environment env in let (env'', subterms) = map_with_environment_updates env' literals compile_literal in let compiled_terms = List.map subterms ~f:(fun x -> Application (Identifier "Ne", [x; Application (Identifier "Rego.Any.bool", [Bool false])])) in @@ -258,9 +274,9 @@ let compile_definition env (rules : rule list) = List.mapi rules ~f:(fun i -> function | { head = (_, Assignment (_, term)); body; _ } -> - let form = compile_term toplevel term in + let form = compile_term env term in (Printf.sprintf "rule%d" i, - compile_query toplevel body |> snd, + compile_query env body |> snd, [form]) | _ -> failwith "unimplemented")) in (env, form) @@ -288,7 +304,16 @@ let compile_policy env (rules : rule list) = let compile_package = function | { path; imports; policy } -> + let policy = List.map ~f:transform_rule_with_ref_head policy |> List.concat in + let env = toplevel in + let env = + List.map policy ~f:(function + | { head = ((Var name, _), _); _ } -> + (name, { lean_id = name ; complete = false; assigned = true }) + | _ -> failwith "policy rule head is not a variable") + |> extend_environment env in + let (_env', forms) = compile_policy env policy in [Comment (show_reference path |> String.escaped); Comment (List.map ~f:show_import imports |> String.concat |> String.escaped)] |