diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 22 |
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 |