diff options
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/ast.ml | 2 | ||||
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 148 |
2 files changed, 88 insertions, 62 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/ast.ml b/rego-proofs/compiler-rewrite/lib/ast.ml index 1ac227d..71257dc 100644 --- a/rego-proofs/compiler-rewrite/lib/ast.ml +++ b/rego-proofs/compiler-rewrite/lib/ast.ml @@ -205,7 +205,7 @@ let parse_head tree = let rhs = if (tree |> member "key" |> is_null) && (not (tree |> member "key" |> is_null)) then Set (tree |> member "key" |> parse_term) - else if tree |> member "args" |> to_bool_or_false then + else if not (tree |> member "args" |> is_null) then Function ( assign_operator, tree |> member "args" |> to_list diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index bd9ef14..5e7d445 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -3,23 +3,31 @@ open Core open Lean type definition_kind = Complete + | Parameter | ScalarRule | SetRule | ObjectRule | FunctionRule [@@deriving eq, show] -let definition_kind_of_rule = function - | { head = ((_, []), Assignment (_, _)); _ } -> - ScalarRule - | { head = ((_, _), Set _); _ } -> - SetRule - | { head = ((_, [_]), Assignment (_, _)); _ } -> - ObjectRule - | { head = ((_, _), Function (_, _, _)); _ } -> - FunctionRule +let kind_and_args_of_rule = function + | { head = ((_, []), Assignment (_, term)); _ } -> + `ScalarRule term + | { head = ((_, _), Set term); _ } -> + `SetRule term + | { head = ((_, [key]), Assignment (_, value)); _ } -> + `ObjectRule (key, value) + | { head = ((_, _), Function (_, args, term)); _ } -> + `FunctionRule (args, term) | { head = ((_, _), Assignment (_, _)); _ } -> - failwith "unreachable" + assert false (* TODO *) + +let definition_kind_of_rule rule = + match kind_and_args_of_rule rule with + | `ScalarRule _ -> ScalarRule + | `SetRule _ -> SetRule + | `ObjectRule _ -> ObjectRule + | `FunctionRule _ -> FunctionRule type variable = { lean_id : string; kind : definition_kind; @@ -86,10 +94,16 @@ let extract_variables (env : environ) (q : query) : analysis_result = free = free' @ free''; used = used' @ used'' } in let rec handle_term env : term -> analysis_result = function - (* If we see a variable in an assignment, it's bound. *) + (* If we see a variable in an assignment, and it isn't a parameter, it's bound. *) | Call ((Var "assign", []), [ Var name; rhs ]) -> let { bound; free; used } = handle_term env rhs in - { bound = [name] @ bound; free; used } + (match Map.find env name with + | Some { kind = Parameter; _ } -> + { used = [name] @ used; free; bound } + | None -> + { bound = [name] @ bound; free; used } + | _ -> + assert false (* TODO *)) (* Variables that haven't previously been introduced to the scope are free. *) | Var name -> if Map.find env name |> Option.is_some then @@ -110,13 +124,13 @@ let extract_variables (env : environ) (q : query) : analysis_result = |> List.fold ~init:empty ~f:combine | Call (x, xs) -> List.map ((Ref x : term)::xs) ~f:(handle_term env) |> List.fold ~init:empty ~f:combine - | ArrayComprehension _ -> failwith "unimplemented" - | ObjectComprehension _ -> failwith "unimplemented" - | SetComprehension _ -> failwith "unimplemented" + | ArrayComprehension _ -> assert false (* TODO *) + | ObjectComprehension _ -> assert false (* TODO *) + | SetComprehension _ -> assert false (* TODO *) | _ -> empty and handle_expr env = function | Term t -> handle_term env t - | Every (Some _key, _value, _, _q) -> failwith "unimplemented" + | Every (Some _key, _value, _, _q) -> assert false (* TODO *) | Every (None, value, _, q) -> let var = ({ lean_id = "unimportant"; kind = Complete; assigned = true }) in let env' = Map.set env ~key:value ~data:var in @@ -143,6 +157,7 @@ let extract_variables_wrapper (q : query) : analysis_result = let gensym : string -> string = let counter = ref 0 in fun (base : string) -> + let base = String.filter base ~f:(fun c -> not (Char.equal c '$')) in let number = !counter in counter := !counter + 1 ; Printf.sprintf "%s__%d" base number @@ -171,10 +186,12 @@ 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; kind = Complete; assigned = true } -> Identifier lean_id + | Some { lean_id; kind = Complete; assigned = true } | + Some { lean_id; kind = Parameter; assigned = true } + -> Identifier lean_id | Some { assigned = false; _ } -> failwith (Printf.sprintf "identifier %s used before definition" id) - | Some _ -> failwith "unimplemented" + | Some _ -> assert false (* TODO *) | None -> failwith (Printf.sprintf "unbound variable %s" id)) | Ref (target, terms) -> let target' = compile_term env (term_of_ref_target target) in @@ -195,11 +212,11 @@ let rec compile_term env : term -> lean_expression = let kvs' = List.map ~f:compile_kv kvs in Application (Identifier "Rego.Any.object", kvs') | ArrayComprehension (_term, _query) -> - failwith "unimplemented" + assert false (* TODO *) | SetComprehension (_term, _query) -> - failwith "unimplemented" + assert false (* TODO *) | ObjectComprehension ((_key, _value), _query) -> - failwith "unimplemented" + assert false (* TODO *) | Call (fn, args) -> let fn' = compile_term env (Ref fn) in let args' = List.map ~f:(compile_term env) args in @@ -211,8 +228,8 @@ 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; kind; assigned } = Map.find_exn env name in - assert (not assigned) ; + let { lean_id; kind; _ } = Map.find_exn env name in + (* assert (not assigned) ; *) let variable = { assigned = true; lean_id; kind } in let env' = Map.set env ~key:name ~data:variable in @@ -256,10 +273,13 @@ and compile_literal env : literal -> (environ * lean_expression) = function 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" + | Negate (_expr, _) -> assert false (* TODO *) and compile_query env literals : (environ * lean_expression) = let { free; bound; used } = extract_variables env literals in + print_endline (List.to_string ~f:String.to_string free); + print_endline (List.to_string ~f:String.to_string bound); + print_endline (List.to_string ~f:String.to_string used); let used = used |> List.filter ~f:(fun name -> match Map.find_exn env name with | { kind = Complete; _ } -> false @@ -295,7 +315,7 @@ and compile_query env literals : (environ * lean_expression) = [Identifier lean_id; Identifier (lean_id_of_identifier name)]) | None -> failwith (Printf.sprintf "unbound variable %s" name) - | _ -> failwith "unreachable") in + | _ -> assert false) in let compiled_terms = constraints @ compiled_terms in let quantified_names = free @ bound @ used in @@ -332,50 +352,56 @@ let compile_definition env (rules : rule list) = (* There can be only one default rule. *) assert (List.length default_rules <= 1); - let subjects = match List.nth_exn rules 0 |> definition_kind_of_rule with - | ScalarRule | SetRule -> - [gensym "x"] - | ObjectRule -> - [gensym "k"; gensym "v"] - | FunctionRule -> - [gensym "xs"; gensym "y"] - | Complete -> - failwith "unreachable" + 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 -> - (subject, { lean_id = subject; kind = Complete; assigned = true })) + ~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 - - let mk_eq : rule -> term list = function - | { head = ((_, []), Assignment (_, term)); _ } | { head = (_, Set (term)); _ } -> - [Call ((Var "eq", []), [Var (List.nth_exn subjects 0); term])] - | { head = ((_, [key]), Assignment (_, value)); _ } -> - [Call ((Var "eq", []), [Var (List.nth_exn subjects 0); key]); - Call ((Var "eq", []), [Var (List.nth_exn subjects 1); value])] - (* | { head = ((_, _), Function (_, args, term)); _ } -> *) - (* [Call ((Var "eq", []), [Var (List.nth_exn subjects 0); Array args]); *) - (* Call ((Var "eq", []), [Var (List.nth_exn subjects 1); term])] *) - | _ -> failwith "unimplemented" - in - let conditional_arms = List.mapi conditional_rules ~f:(fun i rule -> - let query = mk_eq rule |> List.map ~f:(fun clause -> Expr (Term clause, None)) in - let (_, subject_constraint) = compile_query env' query in let { body; _ } = rule in - let (_, body_form) = compile_query env body in + let (_, body_form) = compile_query env' body 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 (body_form, (Printf.sprintf "rule%d" i, - [subject_constraint; body_form], - List.map subjects ~f:(fun x -> Identifier x)))) in + subject_constraints @ [body_form], + List.map subjects ~f:(fun (_, x, _, _, _) -> Identifier x)))) in let default_arms = - List.map default_rules ~f:(fun rule -> - let query = mk_eq rule |> List.map ~f:(fun clause -> Expr (Term clause, None)) in - let (_, subject_constraint) = compile_query env' query in + List.map default_rules ~f:(fun _ -> let other_rule_bodies = List.map ~f:fst conditional_arms 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 let body_form = let fold_or props = match List.reduce props ~f:(fun x y -> Application (Identifier "Or", [y; x])) with @@ -385,18 +411,18 @@ let compile_definition env (rules : rule list) = Application (Identifier "Not", [fold_or other_rule_bodies]) in ("rule_default", - [subject_constraint; body_form], - List.map subjects ~f:(fun x -> Identifier x))) in + subject_constraints @ [body_form], + List.map subjects ~f:(fun (_, x, _, _, _) -> Identifier x))) in let form = let string_of_reference : reference -> string = function | (Var name, []) -> name | (Var name, [_]) -> name - | _ -> failwith "unreachable" + | _ -> assert false (* unreachable *) in Inductive (string_of_reference variable_being_defined, - [(subjects, "Rego.Any")], + [(List.map subjects ~f:(fun (_, x, _, _, _) -> x), "Rego.Any")], List.append (List.map ~f:snd conditional_arms) default_arms) in (env, form) |