diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 203 |
1 files changed, 82 insertions, 121 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 7f3e0af..0b22baf 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -46,12 +46,21 @@ let rec uniq = function let extract_variables (env : environ) (q : query) : (string list * string list) = let combine = fun (x, y) (x', y') -> (x @ x', y @ y') in let rec handle_term env : term -> (string list * string list) = function - | Call ((Var "assign", []), [ Var name; rhs ]) -> let (x, y) = handle_term env rhs in (x, [name] @ y) - | Var name -> if Map.find env name |> Option.is_some then ([], []) else ([name], []) + (* If we see a variable in an assignment, it's bound. *) + | Call ((Var "assign", []), [ Var name; rhs ]) -> + let (x, y) = handle_term env rhs in + (x, [name] @ y) + (* Variables that haven't previously been introduced to the scope are free. *) + | Var name -> + if Map.find env name |> Option.is_some then + ([], []) + else ([name], []) + (* Otherwise, we'll recurse on the term. *) | Ref (target, args) -> let terms = [term_of_ref_target target] @ args in List.map terms ~f:(handle_term env) |> List.fold ~init:([], []) ~f:combine - | Array xs | Set xs -> List.map xs ~f:(handle_term env) |> List.fold ~init:([], []) ~f:combine + | Array xs | Set xs -> + List.map xs ~f:(handle_term env) |> List.fold ~init:([], []) ~f:combine | Object kvs -> List.map ~f:snd kvs |> List.map ~f:(handle_term env) |> List.fold ~init:([], []) ~f:combine @@ -82,11 +91,6 @@ let extract_variables_wrapper (q : query) : (string list * string list) = (* --- *) -type compile_term_result = - { form : lean_expression; - toplevel : lean_expression list; - new_locals : (string * string) list } - let gensym : string -> string = let counter = ref 0 in fun (base : string) -> @@ -94,15 +98,7 @@ let gensym : string -> string = counter := !counter + 1 ; Printf.sprintf "%s__%d" base number -let rec compile_term env : term -> compile_term_result = - let result_of expr = - { form = expr; - toplevel = []; - new_locals = []; } in - let form = function | { form ; _ } -> form in - let toplevel = function | { toplevel ; _ } -> toplevel in - let new_locals = function | { new_locals ; _ } -> new_locals in - +let rec compile_term env : term -> lean_expression = function | Scalar s -> (match s with @@ -110,54 +106,29 @@ let rec compile_term env : term -> compile_term_result = | Number x -> Application (Identifier "Rego.Any.num", [Number x]) | Bool b -> Application (Identifier "Rego.Any.bool", [Bool b]) | Null -> Application (Identifier "Rego.Any.null", [])) - |> result_of | Var id -> - (match Map.find env id with - | Some { lean_id; complete = true } -> Identifier lean_id |> result_of - | Some { lean_id; complete = false } -> - let anonymous_id = gensym "anonymous" in - { form = Identifier anonymous_id; - toplevel = []; - new_locals = [(anonymous_id, lean_id)]; } - | None -> - failwith (Printf.sprintf "unbound variable %s" id)) + (match Map.find env id with + | Some { lean_id; complete = true } -> Identifier lean_id + | Some { lean_id = _; complete = false } -> failwith "unimplemented" + | None -> failwith (Printf.sprintf "unbound variable %s" id)) | Ref (target, terms) -> - List.fold - terms - ~init:(compile_term env (term_of_ref_target target)) - ~f:(fun x y -> - match x with - | { form = x'; toplevel = toplevel'; new_locals = new_locals' } -> - match compile_term env y with - | { form = y'; toplevel = toplevel''; new_locals = new_locals'' } -> - let toplevel = toplevel' @ toplevel'' in - let new_locals = new_locals' @ new_locals'' in - { form = (Application ((Identifier "Rego.Any.deref"), [x'; y'])); - toplevel; new_locals }) + let target' = compile_term env (term_of_ref_target target) in + let terms' = List.map ~f:(compile_term env) terms in + Application (Identifier "Rego.Any.deref", [target'] @ terms') | Array xs -> - let subterms = List.map ~f:(compile_term env) xs in - { form = Application (Identifier "Rego.Any.array", List.map ~f:form subterms); - toplevel = List.map ~f:toplevel subterms |> List.concat; - new_locals = List.map ~f:new_locals subterms |> List.concat } + let xs' = List.map ~f:(compile_term env) xs in + Application (Identifier "Rego.Any.array", xs') | Set xs -> - let subterms = List.map ~f:(compile_term env) xs in - { form = Application (Identifier "Rego.Any.set", List.map ~f:form subterms); - toplevel = List.map ~f:toplevel subterms |> List.concat; - new_locals = List.map ~f:new_locals subterms |> List.concat } + let xs' = List.map ~f:(compile_term env) xs in + Application (Identifier "Rego.Any.set", xs') | Object kvs -> let compile_kv = function | (key, value) -> - match compile_term env (term_of_object_key key) with - | { form = x'; toplevel = toplevel'; new_locals = new_locals' } -> - match compile_term env value with - | { form = y'; toplevel = toplevel''; new_locals = new_locals'' } -> - let toplevel = toplevel' @ toplevel'' in - let new_locals = new_locals' @ new_locals'' in - { form = Tuple [x'; y']; toplevel; new_locals } in - let subterms = List.map ~f:compile_kv kvs in - { form = Application (Identifier "Rego.Any.object", List.map ~f:form subterms); - toplevel = List.map ~f:toplevel subterms |> List.concat; - new_locals = List.map ~f:new_locals subterms |> List.concat } + let key' = compile_term env (term_of_object_key key) in + let value' = compile_term env value in + Tuple [key'; value'] in + let kvs' = List.map ~f:compile_kv kvs in + Application (Identifier "Rego.Any.object", kvs') | ArrayComprehension (_term, _query) -> failwith "unimplemented" | SetComprehension (_term, _query) -> @@ -165,86 +136,78 @@ let rec compile_term env : term -> compile_term_result = | ObjectComprehension ((_key, _value), _query) -> failwith "unimplemented" | Call (fn, args) -> - let head = compile_term env (Ref fn) in - let subterms = List.map ~f:(compile_term env) args in - { form = Application (form head, List.map ~f:form subterms); - toplevel = toplevel head @ (List.map ~f:toplevel subterms |> List.concat); - new_locals = new_locals head @ (List.map ~f:new_locals subterms |> List.concat) } + let fn' = compile_term env (Ref fn) in + let args' = List.map ~f:(compile_term env) args in + Application (fn', args') -let rec compile_expr env : expr -> (environ * compile_term_result) = function +let rec compile_expr env : expr -> (environ * lean_expression) = function | Term t -> (match t with - (* Special case of call; this is the only kind of term that affects scope. *) + (* 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 - (env', compile_term env' (Call ((Var "eq", []), [ Var name; rhs ]))) + ( + env', + compile_term env' (Call ((Var "eq", []), [ Var name; rhs ])) + ) | t -> (env, compile_term env t)) | Every (Some key, value, domain, query) -> - (match compile_term env domain with - | { form = domain'; toplevel; new_locals } -> - let (toplevel', query_compiled) = compile_query env query in - let form = ForAll - (([key; value], "Rego.Any"), - (Application - (Identifier "And", - [(Application - ((Identifier "Membership.mem"), - [Tuple [Identifier key; Identifier value]; domain'])); - query_compiled]))) - in (env, {form; toplevel = toplevel @ toplevel'; new_locals})) + 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'', query') = compile_query env' query in + (env'', + ForAll + (([key; value], "Rego.Any"), + (Application + (Identifier "And", + [(Application + ((Identifier "Membership.mem"), + [Tuple [Identifier key; Identifier value]; domain'])); + query'])))) | Every (None, value, domain, query) -> - (match compile_term env domain with - | { form = domain'; toplevel; new_locals } -> - let (toplevel', query_compiled) = compile_query env query in - let form = ForAll - (([value], "Rego.Any"), - (Application - (Identifier "And", - [(Application - ((Identifier "Membership.mem"), - [Identifier value; domain'])); - query_compiled]))) - in (env, {form; toplevel = toplevel @ toplevel'; new_locals})) + 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'', query') = compile_query env' query in + (env'', + ForAll + (([value], "Rego.Any"), + (Application + (Identifier "And", + [(Application + ((Identifier "Membership.mem"), + [Identifier value; domain'])); + query'])))) -and compile_literal env : literal -> (environ * compile_term_result) = function +and compile_literal env : literal -> (environ * lean_expression) = function | Exists (exprs, _) -> - let (toplevel, form) = compile_query env (List.map ~f:literal_of_expr exprs) in - (env, { form; toplevel; new_locals = [] }) + let (env', form) = compile_query env (List.map ~f:literal_of_expr exprs) in + (env', form) | Expr (expr, _) -> compile_expr env expr | Negate (_expr, _) -> failwith "unimplemented" -and compile_query env literals : (lean_expression list * lean_expression) = +and compile_query env literals : (environ * lean_expression) = let (free, bound) = extract_variables env literals in - let env' = List.map (free @ bound) ~f:(fun name -> (name, { lean_id = name; complete = true })) + let env' = List.map free ~f:(fun name -> (name, { lean_id = name; complete = true })) |> Environ.of_alist_exn |> Map.merge env ~f:(fun ~key:_key -> function | `Right v -> Some v | `Left v -> Some v | `Both (_, v) -> Some v) in - let (_env', subterms) = map_with_environment_updates env' literals compile_literal in - let (compiled_terms, toplevel, new_locals) = - List.fold subterms - ~init:([], [], []) - ~f:(fun (a, b, c) y -> - match y with - | { form; toplevel; new_locals } -> - let comparison = - Application (Identifier "Ne", [form; Application (Identifier "Rego.Any.bool", [Bool false])]) - in - (a @ [comparison], b @ toplevel, c @ new_locals)) - in - (toplevel, - if List.is_empty new_locals then + let (env'', subterms) = map_with_environment_updates env' literals compile_literal in + let compiled_terms = List.map subterms + ~f:(fun x -> Application (Identifier "Ne", [x; Application (Identifier "Rego.Any.bool", [Bool false])])) in + let quantified_names = free @ bound in + (env'', + if List.is_empty quantified_names then match compiled_terms with | [x] -> x | xs -> Application (Identifier "And", xs) else - Exists ((free @ bound @ (List.map ~f:fst new_locals), "Rego.Any"), - Application (Identifier "And", - List.map ~f:(fun (x, y) -> - Application (Identifier y, [Identifier x])) - new_locals - @ compiled_terms))) + Exists ((free @ bound, "Rego.Any"), + Application (Identifier "And", compiled_terms))) (* TODO: Probably get rid of this once we deal with nested definitions. *) let string_of_reference : reference -> string = function @@ -266,12 +229,10 @@ let compile_definition env (rules : rule list) = List.mapi rules ~f:(fun i -> function | { head = (_, Assignment (_, term)); body; _ } -> - (match compile_term toplevel term with - (* TODO: We need to pass this up.. not ignore it... *) - | { form; _ } -> - (Printf.sprintf "rule%d" i, - compile_query toplevel body |> snd, - [form])) + let form = compile_term toplevel term in + (Printf.sprintf "rule%d" i, + compile_query toplevel body |> snd, + [form]) | _ -> failwith "unimplemented")) in (env, form) |