Checkpoint

1 files 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)