Assigned field for variable records

1 files changed, 12 insertions, 10 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index cfafd8d..540b094 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -4,6 +4,7 @@ open Lean
 
 type variable = { lean_id : string;
                   complete : bool;
+                  assigned : bool;
                 }
 
 module Environ = Map.Make (String)
@@ -32,8 +33,8 @@ let map_with_environment_updates env xs fn =
       (env', ys @ [ y ]))
 
 let toplevel = Environ.of_alist_exn [
-    ("eq",    { lean_id = "eq";    complete = true });
-    ("equal", { lean_id = "equal"; complete = true })
+    ("eq",    { lean_id = "eq";    complete = true; assigned = true });
+    ("equal", { lean_id = "equal"; complete = true; assigned = true })
   ]
 
 let rec uniq = function
@@ -87,7 +88,8 @@ 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 env' = Map.set env ~key:value ~data:({ lean_id = "test"; complete = true }) in
+      let var = ({ lean_id = "unimportant"; complete = true; 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
     | Exists (exprs, _) ->
@@ -121,8 +123,8 @@ 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 } -> Identifier lean_id
-     | Some { lean_id = _; complete = false } -> failwith "unimplemented"
+     | Some { lean_id; complete = true; assigned = true } -> Identifier lean_id
+     | Some _ -> failwith "unimplemented"
      | None -> failwith (Printf.sprintf "unbound variable %s" id))
   | Ref (target, terms) ->
     let target' = compile_term env (term_of_ref_target target) in
@@ -158,7 +160,7 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function
     (match t with
      (* Call is a special case, being the only kind of "term" that affects scope. *)
      | Call ((Var "assign", []), [ Var name; rhs ]) ->
-       let env' = Map.set env ~key:name ~data:{ lean_id = name; complete = true } in
+       let env' = Map.set env ~key:name ~data:{ lean_id = name; complete = true; assigned = true } in
        (
          env',
          compile_term env' (Call ((Var "eq", []), [ Var name; rhs ]))
@@ -167,8 +169,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 = key; complete = true }
-               |> Map.set ~key:value ~data:{ lean_id = value; complete = true } in
+    let env' = Map.set env ~key:key ~data:{ lean_id = key; complete = true; assigned = true }
+               |> Map.set ~key:value ~data:{ lean_id = value; complete = true; assigned = true } in
     let (env'', query') = compile_query env' query in
     (env'',
      ForAll
@@ -182,7 +184,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 = value; complete = true } in
+    let env' = Map.set env ~key:value ~data:{ lean_id = value; complete = true; assigned = true } in
     let (env'', query') = compile_query env' query in
     (env'',
      ForAll
@@ -203,7 +205,7 @@ and compile_literal env : literal -> (environ * lean_expression) = function
 
 and compile_query env literals : (environ * lean_expression) =
   let { free; bound; _ } = extract_variables env literals in
-  let env' = List.map free ~f:(fun name -> (name, { lean_id = name; complete = true }))
+  let env' = List.map free ~f:(fun name -> (name, { lean_id = name; complete = true; assigned = true }))
              |> Environ.of_alist_exn
              |> Map.merge env ~f:(fun ~key:_key -> function
                  | `Right v -> Some v