diff options
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 60 | ||||
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/lean.ml | 10 | ||||
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/lean.mli | 2 |
3 files changed, 54 insertions, 18 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 1cb325e..9044f50 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -240,24 +240,53 @@ and compile_literal env : literal -> (environ * lean_expression) = function | Negate (_expr, _) -> failwith "unimplemented" and compile_query env literals : (environ * lean_expression) = - let { free; bound; _ } = extract_variables env literals in + let { free; bound; used } = extract_variables env literals in + let used = used + |> List.filter ~f:(fun name -> match Map.find_exn env name with + | { kind = Complete; _ } -> false + | _ -> true) in let env' = - List.append - (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 }))) + List.concat + [List.map free ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = true })); + List.map used ~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 ~f:(fun x -> Application (Identifier "Ne", [x; Application (Identifier "Rego.Any.bool", [Bool false])])) in - let quantified_names = free @ bound in + + let lean_id_of_identifier k = (let { lean_id; _ } = Map.find_exn env'' k in lean_id) in + let constraints = + List.map bound ~f:(fun name -> + match Map.find env name with + | Some { lean_id; kind = ScalarRule; _ } -> + Application (Identifier "scalar_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)]) + | Some { lean_id; kind = SetRule; _ } -> + Application (Identifier "set_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)]) + | Some { lean_id; kind = ObjectRule; _ } -> + Application (Identifier "object_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)]) + | Some { lean_id; kind = FunctionRule; _ } -> + Application (Identifier "function_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)]) + | None -> failwith (Printf.sprintf "unbound variable %s" name) + | _ -> failwith "unreachable") in + let compiled_terms = constraints @ compiled_terms in + + let quantified_names = free @ bound @ used in (env'', if List.is_empty quantified_names then match compiled_terms with | [x] -> x | xs -> Application (Identifier "And", xs) else - let lean_id_of_identifier k = (let { lean_id; _ } = Map.find_exn env'' k in lean_id) in - Exists ((List.map (free @ bound) ~f:lean_id_of_identifier , "Rego.Any"), + Exists ((List.map quantified_names ~f:lean_id_of_identifier , "Rego.Any"), Application (Identifier "And", compiled_terms))) (* TODO: Probably get rid of this once we deal with nested definitions. *) @@ -273,17 +302,21 @@ let compile_definition env (rules : rule list) = | { head = (rf, _); _ } -> rf in + let subject = gensym "x" in let form = Inductive (string_of_reference variable_being_defined, - [([gensym "x"], "Rego.Any")], + [([subject], "Rego.Any")], List.mapi rules ~f:(fun i -> function | { head = (_, Assignment (_, term)); body; _ } -> - let form = compile_term env term in - (Printf.sprintf "rule%d" i, - compile_query env body |> snd, - [form]) + let eq : term = Call ((Var "eq", []), [Var subject; term]) in + let env' = [(subject, { lean_id = subject; kind = Complete; assigned = true })] + |> extend_environment env in + let (_, form) = compile_query env' [Expr (Term eq, None)] in + (Printf.sprintf "rule%d" i, + [form; compile_query env body |> snd], + [Identifier subject]) | _ -> failwith "unimplemented")) in (env, form) @@ -312,7 +345,6 @@ 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, []), Assignment _); _ } -> @@ -324,7 +356,7 @@ let compile_package = function | { head = ((Var name, []), Function _); _ } -> (name, { lean_id = name ; kind = FunctionRule; assigned = true }) | _ -> failwith "policy rule head is not a variable") - |> extend_environment env in + |> extend_environment toplevel in let (_env', forms) = compile_policy env policy in [Comment (show_reference path |> String.escaped); diff --git a/rego-proofs/compiler-rewrite/lib/lean.ml b/rego-proofs/compiler-rewrite/lib/lean.ml index f43c5c3..41abee3 100644 --- a/rego-proofs/compiler-rewrite/lib/lean.ml +++ b/rego-proofs/compiler-rewrite/lib/lean.ml @@ -10,7 +10,7 @@ type lean_expression = | Tuple of lean_expression list | Application of lean_expression * lean_expression list | Define of string * lean_expression - | Inductive of string * judgement list * (string * lean_expression * lean_expression list) list + | Inductive of string * judgement list * (string * lean_expression list * lean_expression list) list | ForAll of judgement * lean_expression | Exists of judgement * lean_expression @@ -41,14 +41,18 @@ let rec fmt_lean_expression : lean_expression -> string = function | Exists (j, expr) -> Printf.sprintf "∃ %s, %s" (fmt_judgement j) (fmt_lean_expression expr) | Inductive (name, judgements, arms) -> - let fmt_arm (arm_name, expr, values) = + let fmt_arm (arm_name, exprs, values) = let head = Printf.sprintf "%s %s" name (List.map ~f:fmt_lean_expression values |> String.concat ~sep:" ") in - Printf.sprintf " | %s : %s → %s" arm_name (fmt_lean_expression expr) head + let body = + List.map ~f:fmt_lean_expression exprs + |> String.concat ~sep:" → " + in + Printf.sprintf " | %s : %s → %s" arm_name body head in Printf.sprintf "inductive %s %s where\n%s" name (List.map ~f:fmt_judgement judgements |> String.concat ~sep:" ") diff --git a/rego-proofs/compiler-rewrite/lib/lean.mli b/rego-proofs/compiler-rewrite/lib/lean.mli index 1626dfa..990ab5f 100644 --- a/rego-proofs/compiler-rewrite/lib/lean.mli +++ b/rego-proofs/compiler-rewrite/lib/lean.mli @@ -8,7 +8,7 @@ type lean_expression = | Tuple of lean_expression list | Application of lean_expression * lean_expression list | Define of string * lean_expression - | Inductive of string * judgement list * (string * lean_expression * lean_expression list) list + | Inductive of string * judgement list * (string * lean_expression list * lean_expression list) list | ForAll of judgement * lean_expression | Exists of judgement * lean_expression |