diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 40 |
1 files changed, 26 insertions, 14 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 5c89807..1cb325e 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -2,8 +2,14 @@ open Ast open Core open Lean +type definition_kind = Complete + | ScalarRule + | SetRule + | ObjectRule + | FunctionRule + type variable = { lean_id : string; - complete : bool; + kind : definition_kind; assigned : bool; } @@ -40,8 +46,8 @@ let map_with_environment_updates env xs fn = (env', ys @ [ y ])) let toplevel = Environ.of_alist_exn [ - ("eq", { lean_id = "eq"; complete = true; assigned = true }); - ("equal", { lean_id = "equal"; complete = true; assigned = true }) + ("eq", { lean_id = "eq"; kind = Complete; assigned = true }); + ("equal", { lean_id = "equal"; kind = Complete; assigned = true }) ] let rec uniq = function @@ -99,7 +105,7 @@ let extract_variables (env : environ) (q : query) : analysis_result = | Term t -> handle_term env t | Every (Some _key, _value, _, _q) -> failwith "unimplemented" | Every (None, value, _, q) -> - let var = ({ lean_id = "unimportant"; complete = true; assigned = true }) in + let var = ({ lean_id = "unimportant"; kind = Complete; assigned = true }) in let env' = Map.set env ~key:value ~data:var in List.map q ~f:(handle_literal env') |> List.fold ~init:empty ~f:combine and handle_literal env : literal -> analysis_result = function @@ -146,7 +152,7 @@ let rec compile_term env : term -> lean_expression = | Null -> Application (Identifier "Rego.Any.null", [])) | Var id -> (match Map.find env id with - | Some { lean_id; complete = true; assigned = true } -> Identifier lean_id + | Some { lean_id; kind = Complete; assigned = true } -> Identifier lean_id | Some { assigned = false; _ } -> failwith (Printf.sprintf "identifier %s used before definition" id) | Some _ -> failwith "unimplemented" @@ -186,10 +192,10 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function (* Call is a special case, being the only kind of "term" that affects scope. *) | Call ((Var "assign", []), [ Var name; rhs ]) -> (* Assumption: `name' is in the `env' because of our up-front variable analysis, but we've marked it as unassigned. *) - let { lean_id; complete; assigned } = Map.find_exn env name in + let { lean_id; kind; assigned } = Map.find_exn env name in assert (not assigned) ; - let variable = { assigned = true; lean_id; complete } in + let variable = { assigned = true; lean_id; kind } in let env' = Map.set env ~key:name ~data:variable in ( env', @@ -199,8 +205,8 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function | Every (Some key, value, domain, query) -> let domain' = compile_term env domain in (* Extend the environment with the key and value. *) - let env' = Map.set env ~key:key ~data:{ lean_id = gensym key; complete = true; assigned = true } - |> Map.set ~key:value ~data:{ lean_id = gensym value; complete = true; assigned = true } in + let env' = Map.set env ~key:key ~data:{ lean_id = gensym key; kind = Complete; assigned = true } + |> Map.set ~key:value ~data:{ lean_id = gensym value; kind = Complete; assigned = true } in let (env'', query') = compile_query env' query in (env'', ForAll @@ -214,7 +220,7 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function | Every (None, value, domain, query) -> let domain' = compile_term env domain in (* Extend the environment with the value. *) - let env' = Map.set env ~key:value ~data:{ lean_id = gensym value; complete = true; assigned = true } in + let env' = Map.set env ~key:value ~data:{ lean_id = gensym value; kind = Complete; assigned = true } in let (env'', query') = compile_query env' query in (env'', ForAll @@ -237,8 +243,8 @@ and compile_query env literals : (environ * lean_expression) = let { free; bound; _ } = extract_variables env literals 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 }))) + (List.map free ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = true }))) + (List.map bound ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = false }))) |> extend_environment env in let (env'', subterms) = map_with_environment_updates env' literals compile_literal in let compiled_terms = List.map subterms @@ -309,8 +315,14 @@ let compile_package = function let env = toplevel in let env = List.map policy ~f:(function - | { head = ((Var name, _), _); _ } -> - (name, { lean_id = name ; complete = false; assigned = true }) + | { head = ((Var name, []), Assignment _); _ } -> + (name, { lean_id = name ; kind = ScalarRule; assigned = true }) + | { head = ((Var name, [_]), Assignment _); _ } -> + (name, { lean_id = name ; kind = ObjectRule; assigned = true }) + | { head = ((Var name, []), Set _); _ } -> + (name, { lean_id = name ; kind = SetRule; assigned = true }) + | { head = ((Var name, []), Function _); _ } -> + (name, { lean_id = name ; kind = FunctionRule; assigned = true }) | _ -> failwith "policy rule head is not a variable") |> extend_environment env in |