Replace complete with more detailed description of variable usage

2 files changed, 27 insertions, 15 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index 5c89807..1cb325e 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -2,8 +2,14 @@ open Ast
 open Core
 open Lean
 
+type definition_kind = Complete
+                     | ScalarRule
+                     | SetRule
+                     | ObjectRule
+                     | FunctionRule
+
 type variable = { lean_id : string;
-                  complete : bool;
+                  kind : definition_kind;
                   assigned : bool;
                 }
 
@@ -40,8 +46,8 @@ let map_with_environment_updates env xs fn =
       (env', ys @ [ y ]))
 
 let toplevel = Environ.of_alist_exn [
-    ("eq",    { lean_id = "eq";    complete = true; assigned = true });
-    ("equal", { lean_id = "equal"; complete = true; assigned = true })
+    ("eq",    { lean_id = "eq";    kind = Complete; assigned = true });
+    ("equal", { lean_id = "equal"; kind = Complete; assigned = true })
   ]
 
 let rec uniq = function
@@ -99,7 +105,7 @@ let extract_variables (env : environ) (q : query) : analysis_result =
     | Term t -> handle_term env t
     | Every (Some _key, _value, _, _q) -> failwith "unimplemented"
     | Every (None, value, _, q) ->
-      let var = ({ lean_id = "unimportant"; complete = true; assigned = true }) in
+      let var = ({ lean_id = "unimportant"; kind = Complete; assigned = true }) in
       let env' = Map.set env ~key:value ~data:var in
       List.map q ~f:(handle_literal env') |> List.fold ~init:empty ~f:combine
   and handle_literal env : literal -> analysis_result = function
@@ -146,7 +152,7 @@ let rec compile_term env : term -> lean_expression =
       | Null     -> Application (Identifier "Rego.Any.null", []))
   | Var id ->
     (match Map.find env id with
-     | Some { lean_id; complete = true; assigned = true } -> Identifier lean_id
+     | Some { lean_id; kind = Complete; assigned = true } -> Identifier lean_id
      | Some { assigned = false; _ } ->
        failwith (Printf.sprintf "identifier %s used before definition" id)
      | Some _ -> failwith "unimplemented"
@@ -186,10 +192,10 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function
      (* Call is a special case, being the only kind of "term" that affects scope. *)
      | Call ((Var "assign", []), [ Var name; rhs ]) ->
        (* Assumption: `name' is in the `env' because of our up-front variable analysis, but we've marked it as unassigned. *)
-       let { lean_id; complete; assigned } = Map.find_exn env name in
+       let { lean_id; kind; assigned } = Map.find_exn env name in
        assert (not assigned) ;
 
-       let variable = { assigned = true; lean_id; complete } in
+       let variable = { assigned = true; lean_id; kind } in
        let env' = Map.set env ~key:name ~data:variable in
        (
          env',
@@ -199,8 +205,8 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function
   | Every (Some key, value, domain, query) ->
     let domain' = compile_term env domain in
     (* Extend the environment with the key and value. *)
-    let env' = Map.set env ~key:key ~data:{ lean_id = gensym key; complete = true; assigned = true }
-               |> Map.set ~key:value ~data:{ lean_id = gensym value; complete = true; assigned = true } in
+    let env' = Map.set env ~key:key ~data:{ lean_id = gensym key; kind = Complete; assigned = true }
+               |> Map.set ~key:value ~data:{ lean_id = gensym value; kind = Complete; assigned = true } in
     let (env'', query') = compile_query env' query in
     (env'',
      ForAll
@@ -214,7 +220,7 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function
   | Every (None, value, domain, query) ->
     let domain' = compile_term env domain in
     (* Extend the environment with the value. *)
-    let env' = Map.set env ~key:value ~data:{ lean_id = gensym value; complete = true; assigned = true } in
+    let env' = Map.set env ~key:value ~data:{ lean_id = gensym value; kind = Complete; assigned = true } in
     let (env'', query') = compile_query env' query in
     (env'',
      ForAll
@@ -237,8 +243,8 @@ and compile_query env literals : (environ * lean_expression) =
   let { free; bound; _ } = extract_variables env literals in
   let env' =
     List.append
-      (List.map free  ~f:(fun name -> (name, { lean_id = gensym name; complete = true; assigned = true })))
-      (List.map bound ~f:(fun name -> (name, { lean_id = gensym name; complete = true; assigned = false })))
+      (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 })))
     |> extend_environment env in
   let (env'', subterms) = map_with_environment_updates env' literals compile_literal in
   let compiled_terms = List.map subterms
@@ -309,8 +315,14 @@ let compile_package = function
     let env = toplevel in
     let env =
       List.map policy ~f:(function
-          | { head = ((Var name, _), _); _ } ->
-            (name, { lean_id = name ; complete = false; assigned = true })
+          | { head = ((Var name, []), Assignment _); _ } ->
+             (name, { lean_id = name ; kind = ScalarRule; assigned = true })
+          | { head = ((Var name, [_]), Assignment _); _ } ->
+             (name, { lean_id = name ; kind = ObjectRule; assigned = true })
+          | { head = ((Var name, []), Set _); _ } ->
+             (name, { lean_id = name ; kind = SetRule; assigned = true })
+          | { head = ((Var name, []), Function _); _ } ->
+             (name, { lean_id = name ; kind = FunctionRule; assigned = true })
           | _ -> failwith "policy rule head is not a variable")
       |> extend_environment env in
 
diff --git a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml b/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml
index 847f8c9..1d9d926 100644
--- a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml
+++ b/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml
@@ -98,7 +98,7 @@ let test_identifier () =
 
 let test_transform_simple_1 () =
   let open Compiler_rewrite.Ast in
-  let rule = { head = ((Var "fruit", [Var "apple"; Var "seeds"; Var "density"]), Assignment (Assign, (Scalar (Number 12.))));
+  let rule = { head = ((Var "fruit", [Var "apple"; Var "seeds"]), Assignment (Assign, (Scalar (Number 12.))));
                default = false;
                body = [Expr (Term (Scalar (Bool true)), None)];
                otherwise = None } in