From 6daa7be7b80dfff80bded0cc2edced432bc3655d Mon Sep 17 00:00:00 2001 From: Jakob L. Kreuze Date: Fri, 3 Nov 2023 13:03:01 -0400 Subject: Checkpoint --- rego-proofs/compiler-rewrite/lib/compiler.ml | 150 +++++++++++++-------------- 1 file changed, 75 insertions(+), 75 deletions(-) diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index f1cc462..2f9025d 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -92,6 +92,7 @@ type analysis_result = { bound : string list; free : string list; used : string list } +[@@deriving show] let extract_variables (env : environ) (q : query) : analysis_result = let empty = { bound = []; free = []; used = [] } in @@ -110,10 +111,8 @@ let extract_variables (env : environ) (q : query) : analysis_result = (match Map.find env name with | Some { kind = Parameter; _ } -> { used = [name] @ used; free; bound } - | None -> - { bound = [name] @ bound; free; used } | _ -> - assert false (* TODO *)) + { bound = [name] @ bound; free; used }) (* Variables that haven't previously been introduced to the scope are free. *) | Var name -> if Map.find env name |> Option.is_some then @@ -153,6 +152,7 @@ let extract_variables (env : environ) (q : query) : analysis_result = in let { free; bound; used } = List.map q ~f:(handle_literal env) |> List.fold ~init:empty ~f:combine in let free = List.filter free ~f:(fun x -> List.mem bound ~equal:String.equal x |> not) in + let used = List.filter used ~f:(fun x -> List.mem bound ~equal:String.equal x |> not) in let uniq = uniq String.equal in { free = free |> uniq; bound = bound |> uniq; @@ -337,7 +337,7 @@ and compile_query env literals : (environ * lean_expression) = | xs -> Application (Identifier "And", xs) in (env', form) -and compile_rule env rule : (environ * lean_expression) = +and compile_rule env subjects rule : (environ * lean_expression) = let { body = literals; _ } = rule in let (new_identifiers, _with_statement_constraints) = rewrite_with env literals in let env = List.map new_identifiers @@ -345,49 +345,69 @@ and compile_rule env rule : (environ * lean_expression) = (old_name, { lean_id = anonymous_name; kind = Parameter; assigned = true })) |> extend_environment env in - let subjects = - let identifier_pair_of_term default_name : term -> _ = function - | Var identifier - (* This variable is only an identifier if it's actually used in the - body. This is a pretty awful way of checking if that's the case, - but it means we have a less complex usage analysis. *) - when - let env' = [(identifier, { lean_id = "unimportant"; kind = Parameter; assigned = true })] - |> extend_environment env in - let { used; _ } = extract_variables env' literals in - List.mem used identifier ~equal:String.equal -> - let anon_name = gensym identifier in - (identifier, anon_name, Parameter, true, None) - | term -> - let anon_name = gensym default_name in - let assertion = (Call ((Var "eq", []), [Var anon_name; term]) : term) in - (anon_name, anon_name, Complete, true, Some assertion) - in - match rule |> kind_and_args_of_rule with + let literal_of_term t = Expr (Term t, None) in + (* let non_query_forms = 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] *) + (* in *) + (* let forms = (literals @ (List.map ~f:literal_of_term non_query_forms)) in *) + let { free; bound; used } = extract_variables env literals in + + + + let (used', parameters, env_updates, subject_constraints) = + let candidates = match rule |> kind_and_args_of_rule with | `ScalarRule term | `SetRule term -> - [term |> identifier_pair_of_term "x"] + [term] | `ObjectRule (key, value) -> - [key |> identifier_pair_of_term "k"; - value |> identifier_pair_of_term "v"] + [key; value] | `FunctionRule (args, output) -> - List.map args ~f:(fun arg_name -> (arg_name, gensym arg_name, Parameter, false, None)) - @ [output |> identifier_pair_of_term "y"] - in - let env' = - List.map subjects - ~f:(fun (subject, lean_id, kind, output, _) -> - match kind with - | Parameter -> (subject, { lean_id = lean_id; assigned = not output; kind }) - | _ -> (subject, { lean_id = lean_id; assigned = true; kind })) - |> extend_environment env - in + List.map args ~f:(fun arg_name -> (Var arg_name : term)) @ [output] + in - let { free; bound; used } = extract_variables env' literals in + let env_updates_and_constraints = + List.map2_exn + subjects + candidates + ~f:(fun subject -> + function + | Var identifier when List.mem bound identifier ~equal:String.equal -> + (* 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. *) + (Some identifier, + (identifier, { lean_id = subject; kind = Parameter; assigned = true }), + None) + | term -> + let anon_name = gensym "x" in + (None, + (anon_name, { lean_id = anon_name; kind = Parameter; assigned = true }), + Some (Call ((Var "eq", []), [Var anon_name; term]) : term))) + in + 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 + | _ -> None) in + + (non_parameters, + parameters, + env_updates_and_constraints |> List.map ~f:(fun (_, x, _) -> x), + env_updates_and_constraints |> List.filter_map ~f:(fun (_, _, x) -> x)) + 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 used = used @ used' in let used = used |> List.filter ~f:(fun name -> match Map.find_exn env name with | { kind = Complete; _ } -> false - | { kind = Parameter; _ } -> false (* At what cost? *) | _ -> true) in let env' = List.concat @@ -428,11 +448,10 @@ and compile_rule env rule : (environ * lean_expression) = let quantified_names = free @ bound @ used in let subject_constraints = - List.filter_map subjects ~f:(fun (_, _, _, _, x) -> x) - |> List.map ~f:(fun clause -> - let (_, compiled) = [Expr (Term clause, None)] |> compile_query env' in - compiled) in - + List.map subject_constraints + ~f:(fun clause -> + let (_, compiled) = [literal_of_term clause] |> compile_query env' in + compiled) in (env'', if List.is_empty quantified_names then @@ -467,41 +486,22 @@ let compile_definition env (rules : rule list) = assert (List.length default_rules <= 1); let subjects = - let rule = List.nth_exn rules 0 in - let identifier_pair_of_term default_name : term -> _ = function - | Var identifier when Map.find env identifier |> Option.is_none -> - let anon_name = gensym identifier in - (identifier, anon_name, Parameter, true, None) - | term -> - let anon_name = gensym default_name in - let assertion = (Call ((Var "eq", []), [Var anon_name; term]) : term) in - (anon_name, anon_name, Complete, true, Some assertion) - in - match rule |> kind_and_args_of_rule with - | `ScalarRule term | `SetRule term -> - [term |> identifier_pair_of_term "x"] - | `ObjectRule (key, value) -> - [key |> identifier_pair_of_term "k"; - value |> identifier_pair_of_term "v"] - | `FunctionRule (args, output) -> - List.map args ~f:(fun arg_name -> (arg_name, gensym arg_name, Parameter, false, None)) - @ [output |> identifier_pair_of_term "y"] - in - let env' = - List.map subjects - ~f:(fun (subject, lean_id, kind, output, _) -> - match kind with - | Parameter -> (subject, { lean_id = lean_id; assigned = not output; kind }) - | _ -> (subject, { lean_id = lean_id; assigned = true; kind })) - |> extend_environment env + match List.hd_exn rules |> kind_and_args_of_rule with + | `ScalarRule _ | `SetRule _ -> + [gensym "x"] + | `ObjectRule _ -> + [gensym "k"; gensym "v"] + | `FunctionRule (args, _) -> + List.map args ~f:(fun arg_name -> gensym arg_name) + @ [gensym "y"] in let conditional_arms = List.mapi conditional_rules ~f:(fun i rule -> - let (_env', body) = compile_rule env' rule in + let (_env', body) = compile_rule env subjects rule in (body, (Printf.sprintf "rule%d" i, [body], - List.map subjects ~f:(fun (_, x, _, _, _) -> Identifier x)))) in + List.map subjects ~f:(fun x -> Identifier x)))) in let default_arms = List.map default_rules ~f:(fun _ -> let other_rule_bodies = List.map ~f:fst conditional_arms in @@ -515,7 +515,7 @@ let compile_definition env (rules : rule list) = in ("rule_default", [body_form], - List.map subjects ~f:(fun (_, x, _, _, _) -> Identifier x))) in + List.map subjects ~f:(fun x -> Identifier x))) in let form = let string_of_reference : reference -> string = function @@ -525,7 +525,7 @@ let compile_definition env (rules : rule list) = in Inductive (string_of_reference variable_being_defined, - [(List.map subjects ~f:(fun (_, x, _, _, _) -> x), "Rego.Any")], + [(subjects, "Rego.Any")], List.append (List.map ~f:snd conditional_arms) default_arms) in (env, form) -- cgit v1.3