diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 35 |
1 files changed, 22 insertions, 13 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 898ff51..21405a3 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -356,7 +356,7 @@ let lift_term (env : environ) (rule : rule) (f : environ -> term -> ('a * term) (side_info, Negate (expr', with_statement)) in let { body = q; head; _ } = rule in - + let (side_info, query) = List.map ~f:handle_literal q |> List.fold ~init:empty ~f:combine in let (side_info', head') = match head with | (rf, Assignment (op, term)) -> @@ -370,7 +370,7 @@ let lift_term (env : environ) (rule : rule) (f : environ -> term -> ('a * term) (side_info, (rf, Set term')) in (side_info @ side_info', { rule with body = query; head = head' }) - + let rewrite_with (env : environ) (q : query) : ((string * string) list * lean_expression list) = let empty = ([], []) in @@ -541,8 +541,6 @@ and compile_rule env subjects rule : (environ * lean_expression) list = (* | _ -> None) in *) - List.iter literals ~f:(fun lit -> show_literal lit |> print_endline); - let (new_identifiers, _with_statement_constraints) = rewrite_with env literals in let env = List.map new_identifiers ~f:(fun (old_name, anonymous_name) -> @@ -551,13 +549,20 @@ and compile_rule env subjects rule : (environ * lean_expression) list = let { free; bound; used } = extract_variables env literals in let (used', parameters, env_updates, subject_constraints) = + let explicit_parameters = match rule |> kind_and_args_of_rule with + | `FunctionRule (args, _) -> + List.filter_map args ~f:(function + | Var id -> Some id + | _ -> None) + | _ -> [] + in let candidates = match rule |> kind_and_args_of_rule with | `ScalarRule term | `SetRule term -> [term] | `ObjectRule (key, value) -> [key; value] | `FunctionRule (args, output) -> - List.map args ~f:(fun arg_name -> (Var arg_name : term)) @ [output] + args @ [output] in let env_updates_and_constraints = @@ -568,7 +573,7 @@ and compile_rule env subjects rule : (environ * lean_expression) list = function (* In this case, we're dealing with a formal parameter, so we want to have it be an alias of the lean_id for the subject. *) - | Var identifier when List.mem bound identifier ~equal:String.equal -> + | Var identifier when List.mem (bound @ explicit_parameters) identifier ~equal:String.equal -> (Some identifier, [(identifier, { lean_id = subject; kind = Parameter; assigned = true })], None) @@ -584,10 +589,7 @@ and compile_rule env subjects rule : (environ * lean_expression) list = let parameters = env_updates_and_constraints |> List.filter_map ~f:(fun (x, _, _) -> x) in let non_parameters = List.filter_map candidates ~f:(function - | Var id -> - if List.mem parameters id ~equal:String.equal then - None - else Some id + | Var id -> Some id | _ -> None) in (non_parameters, @@ -597,11 +599,18 @@ and compile_rule env subjects rule : (environ * lean_expression) list = in let env' = extend_environment env env_updates in let bound = List.filter bound ~f:(fun identifier -> not (List.mem parameters identifier ~equal:String.equal)) in + + let free = free |> + List.filter ~f:(fun name -> not (List.mem parameters name ~equal:String.equal)) in + let used = used @ used' in + let used = used |> + List.filter ~f:(fun name -> not (List.mem parameters name ~equal:String.equal)) in let used = used - |> List.filter ~f:(fun name -> match Map.find_exn env name with + |> List.filter ~f:(fun name -> match Map.find_exn env' name with | { kind = Complete; _ } -> false | _ -> true) in + let env' = List.concat [List.map free ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = true })); @@ -685,7 +694,7 @@ let compile_definition env (rules : rule list) = | `ObjectRule _ -> [gensym "k"; gensym "v"] | `FunctionRule (args, _) -> - List.map args ~f:(fun arg_name -> gensym arg_name) + List.map args ~f:(fun _ -> gensym "arg") @ [gensym "y"] in let conditional_rules = @@ -769,7 +778,7 @@ let compile_error_condition env = Identifier value_name])))) | _ -> None) |> fold_and - + let compile_package = let string_of_reference : reference -> string = function | (Var name, xs) -> |