diff options
Diffstat (limited to 'rego-proofs')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 72 |
1 files changed, 41 insertions, 31 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 5e7d445..185752a 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -19,8 +19,8 @@ let kind_and_args_of_rule = function `ObjectRule (key, value) | { head = ((_, _), Function (_, args, term)); _ } -> `FunctionRule (args, term) - | { head = ((_, _), Assignment (_, _)); _ } -> - assert false (* TODO *) + | { head = ((_, _), Assignment (_, _)); _ } as rule -> + failwith (Printf.sprintf "unknown rule form: %s" (show_rule rule)) let definition_kind_of_rule rule = match kind_and_args_of_rule rule with @@ -33,6 +33,7 @@ type variable = { lean_id : string; kind : definition_kind; assigned : bool; } +[@@deriving eq, show] module Environ = Map.Make (String) type environ = variable Environ.t @@ -115,7 +116,7 @@ let extract_variables (env : environ) (q : query) : analysis_result = if List.is_empty args then handle_term env target else - let terms = [] @ args in + let terms = [target] @ args in List.map terms ~f:(handle_term env) |> List.fold ~init:empty ~f:combine | Array xs | Set xs -> List.map xs ~f:(handle_term env) |> List.fold ~init:empty ~f:combine @@ -191,7 +192,10 @@ let rec compile_term env : term -> lean_expression = -> Identifier lean_id | Some { assigned = false; _ } -> failwith (Printf.sprintf "identifier %s used before definition" id) - | Some _ -> assert false (* TODO *) + | Some var -> + failwith (Printf.sprintf + "variable found in environment but of unknown form %s" + (show_variable var)) | None -> failwith (Printf.sprintf "unbound variable %s" id)) | Ref (target, terms) -> let target' = compile_term env (term_of_ref_target target) in @@ -272,14 +276,15 @@ and compile_literal env : literal -> (environ * lean_expression) = function | Exists (exprs, _) -> let (env', form) = compile_query env (List.map ~f:literal_of_expr exprs) in (env', form) - | Expr (expr, _) -> compile_expr env expr - | Negate (_expr, _) -> assert false (* TODO *) + | Expr (expr, _) -> + let (env', inner) = compile_expr env expr in + (env', Application (Identifier "Ne", [inner; Application (Identifier "Rego.Any.bool", [Bool false])])) + | Negate (expr, _) -> + let (env', form) = compile_literal env (Expr (expr, None)) in + (env', Application (Identifier "Not", [form])) and compile_query env literals : (environ * lean_expression) = let { free; bound; used } = extract_variables env literals in - print_endline (List.to_string ~f:String.to_string free); - print_endline (List.to_string ~f:String.to_string bound); - print_endline (List.to_string ~f:String.to_string used); let used = used |> List.filter ~f:(fun name -> match Map.find_exn env name with | { kind = Complete; _ } -> false @@ -291,42 +296,47 @@ and compile_query env literals : (environ * lean_expression) = 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 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 -> + List.filter_map used ~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 + (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 + (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 + (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) - | _ -> assert false) in - let compiled_terms = constraints @ compiled_terms in + Some + (Application (Identifier "function_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)])) + | Some _ -> None + | None -> failwith (Printf.sprintf "unbound variable %s" name)) in + let compiled_terms = constraints @ subterms in + + let form = match compiled_terms with + | [x] -> x + | xs -> Application (Identifier "And", xs) + 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) + form else Exists ((List.map quantified_names ~f:lean_id_of_identifier , "Rego.Any"), - Application (Identifier "And", compiled_terms))) + form)) let compile_definition env (rules : rule list) = assert (not (List.is_empty rules)); |