From 336721ceac669f983adf3ff7cbfa8ecca445412b Mon Sep 17 00:00:00 2001 From: sneeker Date: Sat, 11 Mar 2017 21:32:00 +0000 Subject: [PATCH] Derive scalar changes and composition laws --- src/change.ml | 262 ++++++++++++++++++++++++++++++++++++++++++ src/change.mli | 24 ++++ src/parse.ml | 2 +- src/util.ml | 10 +- src/util.mli | 1 + src/value.ml | 14 ++- test/test_change.ml | 194 +++++++++++++++++++++++++++++++ test/test_harness.ml | 14 +++ test/test_harness.mli | 8 ++ test/test_main.ml | 1 + 10 files changed, 527 insertions(+), 3 deletions(-) create mode 100644 src/change.ml create mode 100644 src/change.mli create mode 100644 test/test_change.ml diff --git a/src/change.ml b/src/change.ml new file mode 100644 index 0000000..2ca1c6b --- /dev/null +++ b/src/change.ml @@ -0,0 +1,262 @@ +type keyed = + | CInsert of int * Value.t + | CRemove of int * Value.t + | CReplace of int * Value.t * Value.t + +type change = + | CEmpty + | CInt of int + | CBool of bool + | CString of string + | CUnit + | CTuple of change list + | CRecord of string * (string * change) list + | CCollection of keyed list + +let rec is_empty change = + match change with + | CEmpty -> true + | CInt 0 -> true + | CTuple items -> List.for_all is_empty items + | CRecord (_, fields) -> List.for_all (fun (_, item) -> is_empty item) fields + | CCollection items -> items = [] + | CInt _ | CBool _ | CString _ | CUnit -> false + +let empty _ty = CEmpty + +let int_of span value = + match value with + | Value.VInt number -> number + | other -> Diagnostic.error span "runtime error: expected an integer but got %s" (Value.to_string other) + +let bool_of span value = + match value with + | Value.VBool truth -> truth + | other -> Diagnostic.error span "runtime error: expected a boolean but got %s" (Value.to_string other) + +let string_of_value span value = + match value with + | Value.VString text -> text + | other -> Diagnostic.error span "runtime error: expected a string but got %s" (Value.to_string other) + +let scalar_mismatch span expected value = + Diagnostic.error span "this change replaces a %s value but is applied to %s" expected + (Value.to_string value) + +let rec apply value change = + match change with + | CEmpty -> value + | CInt delta -> ( + match value with + | Value.VInt current -> Value.VInt (current + delta) + | other -> scalar_mismatch Location.none "integer" other) + | CBool truth -> ( + match value with Value.VBool _ -> Value.VBool truth | other -> scalar_mismatch Location.none "boolean" other) + | CString text -> ( + match value with Value.VString _ -> Value.VString text | other -> scalar_mismatch Location.none "string" other) + | CUnit -> ( + match value with Value.VUnit -> Value.VUnit | other -> scalar_mismatch Location.none "unit" other) + | CTuple items -> ( + match value with + | Value.VTuple values when List.length values = List.length items -> + Value.VTuple (List.map2 apply values items) + | _ -> Diagnostic.error Location.none "change does not match the value it is applied to") + | CRecord (name, fields) -> ( + match value with + | Value.VRecord (_, values) -> + let updated = + List.map + (fun (label, field_value) -> + match Util.assoc_opt label fields with + | Some field_change -> (label, apply field_value field_change) + | None -> (label, field_value)) + values + in + Value.VRecord (name, updated) + | _ -> Diagnostic.error Location.none "change does not match the value it is applied to") + | CCollection items -> ( + match value with + | Value.VCollection map -> + Value.VCollection (apply_keyed map items) + | _ -> Diagnostic.error Location.none "change does not match the value it is applied to") + +and apply_keyed map items = + List.fold_left + (fun map item -> + match item with + | CInsert (key, value) -> Delta_runtime.Pure_map.add key value map + | CRemove (key, _) -> Delta_runtime.Pure_map.remove key map + | CReplace (key, _, value) -> Delta_runtime.Pure_map.add key value map) + map items + +let rec compose first second = + match (first, second) with + | CEmpty, other | other, CEmpty -> other + | CInt left, CInt right -> CInt (left + right) + | CBool _, CBool right -> CBool right + | CString _, CString right -> CString right + | CUnit, CUnit -> CUnit + | CTuple left, CTuple right -> + if List.length left <> List.length right then + Diagnostic.error Location.none "cannot compose tuple changes of different sizes" + else CTuple (List.map2 compose left right) + | CRecord (left_name, left_fields), CRecord (right_name, right_fields) -> + if left_name <> right_name then + Diagnostic.error Location.none "cannot compose changes of different record types" + else + CRecord + ( left_name, + List.map + (fun (label, left_change) -> + match Util.assoc_opt label right_fields with + | Some right_change -> (label, compose left_change right_change) + | None -> (label, left_change)) + left_fields ) + | CCollection left, CCollection right -> + CCollection (normalize_keyed (left @ right)) + | _ -> Diagnostic.error Location.none "cannot compose changes of different types" + +and normalize_keyed items = + let order = ref [] in + let table = Hashtbl.create 16 in + List.iter + (fun item -> + let key = + match item with CInsert (key, _) | CRemove (key, _) | CReplace (key, _, _) -> key + in + match Util.hashtbl_find_opt table key with + | None -> + Hashtbl.replace table key (old_of item, new_of item); + order := key :: !order + | Some (old_value, _) -> Hashtbl.replace table key (old_value, new_of item)) + items; + let entries = List.rev !order in + Util.filter_map + (fun key -> + match Util.hashtbl_find_opt table key with + | None -> None + | Some (old_value, new_value) -> ( + match (old_value, new_value) with + | None, None -> None + | None, Some value -> Some (CInsert (key, value)) + | Some value, None -> Some (CRemove (key, value)) + | Some old_value, Some new_value -> + if old_value = new_value then None else Some (CReplace (key, old_value, new_value)))) + entries + +and old_of item = + match item with CInsert _ -> None | CRemove (_, value) | CReplace (_, value, _) -> Some value + +and new_of item = + match item with CInsert (_, value) | CReplace (_, _, value) -> Some value | CRemove _ -> None + +let rec of_values records ty old_value new_value = + match Types.repr ty with + | Types.TInt -> CInt (int_of Location.none new_value - int_of Location.none old_value) + | Types.TBool -> if old_value = new_value then CEmpty else CBool (bool_of Location.none new_value) + | Types.TString -> + if old_value = new_value then CEmpty else CString (string_of_value Location.none new_value) + | Types.TUnit -> CEmpty + | Types.TTuple components -> ( + match (old_value, new_value) with + | Value.VTuple old_items, Value.VTuple new_items + when List.length old_items = List.length new_items + && List.length components = List.length old_items -> + CTuple (List.map2 (fun ty (old_item, new_item) -> of_values records ty old_item new_item) + components (List.combine old_items new_items)) + | _ -> Diagnostic.error Location.none "internal error: tuple change of incompatible values") + | Types.TRecord name -> ( + let fields = + match Types.record_info records name with + | Some info -> info.Types.ri_fields + | None -> Diagnostic.error Location.none "internal error: unknown record %s" name + in + match (old_value, new_value) with + | Value.VRecord (_, old_fields), Value.VRecord (_, new_fields) -> + CRecord + ( name, + List.map + (fun (label, field_ty) -> + match (Util.assoc_opt label old_fields, Util.assoc_opt label new_fields) with + | Some old_field, Some new_field -> (label, of_values records field_ty old_field new_field) + | _ -> Diagnostic.error Location.none "internal error: record fields do not match") + fields ) + | _ -> Diagnostic.error Location.none "internal error: record change of incompatible values") + | Types.TCollection _ -> ( + match (old_value, new_value) with + | Value.VCollection old_map, Value.VCollection new_map -> + CCollection (collection_diff old_map new_map) + | _ -> Diagnostic.error Location.none "internal error: collection change of incompatible values") + | Types.TArrow _ | Types.TVar _ -> + Diagnostic.error Location.none "changes are not defined for this type" + +and collection_diff old_map new_map = + let keys = + List.sort_uniq compare + (Delta_runtime.Pure_map.keys old_map @ Delta_runtime.Pure_map.keys new_map) + in + Util.filter_map + (fun key -> + match + (Delta_runtime.Pure_map.find_opt key old_map, Delta_runtime.Pure_map.find_opt key new_map) + with + | None, None -> None + | None, Some value -> Some (CInsert (key, value)) + | Some value, None -> Some (CRemove (key, value)) + | Some old_value, Some new_value -> + if old_value = new_value then None else Some (CReplace (key, old_value, new_value))) + keys + +let rec equal left right = + match (left, right) with + | CEmpty, other | other, CEmpty -> is_empty other + | CInt a, CInt b -> a = b + | CBool a, CBool b -> a = b + | CString a, CString b -> a = b + | CUnit, CUnit -> true + | CTuple a, CTuple b -> List.length a = List.length b && List.for_all2 (fun x y -> equal x y) a b + | CRecord (a, fields_a), CRecord (b, fields_b) -> + a = b + && List.length fields_a = List.length fields_b + && List.for_all2 (fun (la, ca) (lb, cb) -> la = lb && equal ca cb) fields_a fields_b + | CCollection a, CCollection b -> + List.length a = List.length b + && List.for_all2 + (fun x y -> + match (x, y) with + | CInsert (k1, v1), CInsert (k2, v2) -> k1 = k2 && Value.equal v1 v2 + | CRemove (k1, v1), CRemove (k2, v2) -> k1 = k2 && Value.equal v1 v2 + | CReplace (k1, o1, n1), CReplace (k2, o2, n2) -> + k1 = k2 && Value.equal o1 o2 && Value.equal n1 n2 + | _ -> false) + a b + | _ -> false + +let to_string change = + let rec render change = + match change with + | CEmpty -> "empty" + | CInt delta -> Printf.sprintf "+%d" delta + | CBool truth -> Printf.sprintf "bool %b" truth + | CString text -> Printf.sprintf "string %S" text + | CUnit -> "unit" + | CTuple items -> "(" ^ Util.join ", " (List.map render items) ^ ")" + | CRecord (name, fields) -> + name ^ " { " + ^ Util.join ", " (List.map (fun (label, item) -> label ^ " = " ^ render item) fields) + ^ " }" + | CCollection items -> + "collection [" + ^ Util.join "; " + (List.map + (fun item -> + match item with + | CInsert (key, value) -> Printf.sprintf "insert %d %s" key (Value.to_string value) + | CRemove (key, value) -> Printf.sprintf "remove %d %s" key (Value.to_string value) + | CReplace (key, old_value, new_value) -> + Printf.sprintf "replace %d %s %s" key (Value.to_string old_value) + (Value.to_string new_value)) + items) + ^ "]" + in + render change diff --git a/src/change.mli b/src/change.mli new file mode 100644 index 0000000..e74c9cb --- /dev/null +++ b/src/change.mli @@ -0,0 +1,24 @@ +type keyed = + | CInsert of int * Value.t + | CRemove of int * Value.t + | CReplace of int * Value.t * Value.t + +type change = + | CEmpty + | CInt of int + | CBool of bool + | CString of string + | CUnit + | CTuple of change list + | CRecord of string * (string * change) list + | CCollection of keyed list + +val empty : Types.t -> change +val is_empty : change -> bool +val apply : Value.t -> change -> Value.t +val apply_keyed : Value.t Delta_runtime.Pure_map.t -> keyed list -> Value.t Delta_runtime.Pure_map.t +val compose : change -> change -> change +val normalize_keyed : keyed list -> keyed list +val of_values : Types.records -> Types.t -> Value.t -> Value.t -> change +val equal : change -> change -> bool +val to_string : change -> string diff --git a/src/parse.ml b/src/parse.ml index 27be4a1..cb33946 100644 --- a/src/parse.ml +++ b/src/parse.ml @@ -1,5 +1,5 @@ let one_line text = - match String.index_opt text '\n' with + match Util.index_of_char text '\n' with | Some index -> String.sub text 0 index | None -> text diff --git a/src/util.ml b/src/util.ml index 491d59e..9aa34e3 100644 --- a/src/util.ml +++ b/src/util.ml @@ -34,8 +34,16 @@ let rec drop count items = let contains value items = List.exists (fun item -> item = value) items +let index_of_char text character = + let rec search index = + if index >= String.length text then None + else if text.[index] = character then Some index + else search (index + 1) + in + search 0 + let string_before_char text character = - match String.index_opt text character with + match index_of_char text character with | Some index -> String.sub text 0 index | None -> text diff --git a/src/util.mli b/src/util.mli index eb19b5d..0570559 100644 --- a/src/util.mli +++ b/src/util.mli @@ -6,6 +6,7 @@ val list_init : int -> (int -> 'a) -> 'a list val take : int -> 'a list -> 'a list val drop : int -> 'a list -> 'a list val contains : 'a -> 'a list -> bool +val index_of_char : string -> char -> int option val string_before_char : string -> char -> string val starts_with : string -> string -> bool val join : string -> string list -> string diff --git a/src/value.ml b/src/value.ml index 7fa2d93..c0fe9e4 100644 --- a/src/value.ml +++ b/src/value.ml @@ -35,7 +35,19 @@ let collection_of_list entries = let collection_to_list map = Delta_runtime.Pure_map.bindings map -let equal (left : t) (right : t) = left = right +let rec equal (left : t) (right : t) = + match (left, right) with + | VUnit, VUnit -> true + | VInt a, VInt b -> a = b + | VBool a, VBool b -> a = b + | VString a, VString b -> a = b + | VTuple a, VTuple b -> List.length a = List.length b && List.for_all2 equal a b + | VRecord (name_a, fields_a), VRecord (name_b, fields_b) -> + name_a = name_b + && List.length fields_a = List.length fields_b + && List.for_all2 (fun (label_a, value_a) (label_b, value_b) -> label_a = label_b && equal value_a value_b) fields_a fields_b + | VCollection map_a, VCollection map_b -> Delta_runtime.Pure_map.equal equal map_a map_b + | _ -> false let field record label = match record with diff --git a/test/test_change.ml b/test/test_change.ml new file mode 100644 index 0000000..7169598 --- /dev/null +++ b/test/test_change.ml @@ -0,0 +1,194 @@ +open Test_harness + +let records () = + (infer + "type order = { customer : string; total : int }\ninput rows : collection order\nquery q = rows\n") + .Typed.tp_records + +let word rng = + let length = range rng 4 + 1 in + String.init length (fun index -> Char.chr (97 + ((range rng 3 + index) mod 3))) + +let rec value_of_type rng ty = + match Types.repr ty with + | Types.TInt -> Value.VInt (range rng 41 - 20) + | Types.TBool -> Value.VBool (range rng 2 = 0) + | Types.TString -> Value.VString (word rng) + | Types.TUnit -> Value.VUnit + | Types.TTuple components -> Value.VTuple (List.map (value_of_type rng) components) + | Types.TRecord "order" -> + Value.VRecord ("order", [ ("customer", Value.VString (word rng)); ("total", Value.VInt (range rng 41 - 20)) ]) + | Types.TRecord name -> + fail "generator" ("no generator for record " ^ name); + Value.VUnit + | Types.TCollection _ -> + fail "generator" "collections are generated separately"; + Value.VUnit + | Types.TArrow _ | Types.TVar _ -> + fail "generator" "no generator for this type"; + Value.VUnit + +let collection_value rng element_ty = + let count = range rng 5 in + let entries = Util.list_init count (fun index -> (index + 1, value_of_type rng element_ty)) in + Value.VCollection (Value.collection_of_list entries) + +let sample_types = + [ Types.TInt; Types.TBool; Types.TString; Types.TUnit; Types.TTuple [ Types.TInt; Types.TString ]; Types.TRecord "order" ] + +let change_of_values records ty old_value new_value = Change.of_values records ty old_value new_value + +let law_cases = + let records_ctx = records () in + let seeds = Util.list_init 120 (fun index -> index) in + [ + ( "the empty change leaves every value unchanged", + fun () -> + List.iter + (fun seed -> + let rng = rng seed in + List.iter + (fun ty -> + let value = value_of_type rng ty in + let applied = Change.apply value (Change.empty ty) in + if not (Value.equal applied value) then + fail "identity" (Printf.sprintf "seed %d type %s" seed (Types.pp ty))) + sample_types) + seeds ); + ( "a replacement change reaches the new value", + fun () -> + List.iter + (fun seed -> + let rng = rng seed in + List.iter + (fun ty -> + let old_value = value_of_type rng ty in + let new_value = value_of_type rng ty in + let change = change_of_values records_ctx ty old_value new_value in + let applied = Change.apply old_value change in + if not (Value.equal applied new_value) then + fail "replacement" + (Printf.sprintf "seed %d type %s change %s" seed (Types.pp ty) + (Change.to_string change))) + sample_types) + seeds ); + ( "composition matches sequential application", + fun () -> + List.iter + (fun seed -> + let rng = rng seed in + List.iter + (fun ty -> + let first = value_of_type rng ty in + let middle = value_of_type rng ty in + let last = value_of_type rng ty in + let step_one = change_of_values records_ctx ty first middle in + let step_two = change_of_values records_ctx ty middle last in + let composed = Change.compose step_one step_two in + let sequential = Change.apply (Change.apply first step_one) step_two in + let direct = Change.apply first composed in + if not (Value.equal sequential direct) then + fail "composition" + (Printf.sprintf "seed %d type %s" seed (Types.pp ty))) + sample_types) + seeds ); + ( "composition with the empty change is neutral", + fun () -> + List.iter + (fun seed -> + let rng = rng seed in + List.iter + (fun ty -> + let old_value = value_of_type rng ty in + let new_value = value_of_type rng ty in + let change = change_of_values records_ctx ty old_value new_value in + let empty = Change.empty ty in + if not (Change.equal (Change.compose change empty) change) then + fail "right neutral" (Printf.sprintf "seed %d" seed); + if not (Change.equal (Change.compose empty change) change) then + fail "left neutral" (Printf.sprintf "seed %d" seed)) + sample_types) + seeds ); + ( "composition is associative", + fun () -> + List.iter + (fun seed -> + let rng = rng seed in + List.iter + (fun ty -> + let a = value_of_type rng ty in + let b = value_of_type rng ty in + let c = value_of_type rng ty in + let d = value_of_type rng ty in + let ab = change_of_values records_ctx ty a b in + let bc = change_of_values records_ctx ty b c in + let cd = change_of_values records_ctx ty c d in + let left = Change.compose (Change.compose ab bc) cd in + let right = Change.compose ab (Change.compose bc cd) in + if not (Change.equal left right) then + fail "associativity" (Printf.sprintf "seed %d type %s" seed (Types.pp ty))) + sample_types) + seeds ); + ( "integer changes add", + fun () -> + List.iter + (fun seed -> + let rng = rng seed in + let value = Value.VInt (range rng 100 - 50) in + let first = Change.CInt (range rng 21 - 10) in + let second = Change.CInt (range rng 21 - 10) in + let composed = Change.compose first second in + let applied = Change.apply value composed in + let sequential = Change.apply (Change.apply value first) second in + if not (Value.equal applied sequential) then fail "integer composition" (Printf.sprintf "seed %d" seed); + match composed with + | Change.CInt delta -> + let expected = + (match first with Change.CInt a -> a | _ -> 0) + (match second with Change.CInt b -> b | _ -> 0) + in + if delta <> expected then fail "integer sum" (Printf.sprintf "seed %d" seed) + | _ -> fail "integer sum" "expected an additive change") + seeds ); + ( "collection changes compose keywise", + fun () -> + List.iter + (fun seed -> + let rng = rng seed in + let element_ty = Types.TInt in + let value = collection_value rng element_ty in + let middle = collection_value rng element_ty in + let last = collection_value rng element_ty in + let step_one = change_of_values records_ctx (Types.TCollection element_ty) value middle in + let step_two = change_of_values records_ctx (Types.TCollection element_ty) middle last in + let composed = Change.compose step_one step_two in + let sequential = Change.apply (Change.apply value step_one) step_two in + let direct = Change.apply value composed in + if not (Value.equal sequential direct) then + fail "collection composition" + (Printf.sprintf "seed %d value=%s middle=%s last=%s one=%s two=%s composed=%s seq=%s direct=%s" + seed (Value.to_string value) (Value.to_string middle) (Value.to_string last) + (Change.to_string step_one) (Change.to_string step_two) (Change.to_string composed) + (Value.to_string sequential) (Value.to_string direct))) + seeds ); + ( "a change with equal old and new values is empty", + fun () -> + List.iter + (fun seed -> + let rng = rng seed in + List.iter + (fun ty -> + let value = value_of_type rng ty in + let change = change_of_values records_ctx ty value value in + if not (Change.is_empty change) then + fail "unchanged" (Printf.sprintf "seed %d type %s" seed (Types.pp ty))) + sample_types) + seeds ); + ( "applying a change to a mismatched value is rejected", + fun () -> + expect_diagnostic "mismatch" (fun () -> ignore (Change.apply (Value.VInt 1) (Change.CString "x"))); + expect_diagnostic "mismatch" (fun () -> ignore (Change.apply (Value.VString "x") (Change.CInt 1))) ); + ( "composing changes of different types is rejected", + fun () -> + expect_diagnostic "compose" (fun () -> ignore (Change.compose (Change.CInt 1) (Change.CString "x"))) ); + ] + diff --git a/test/test_harness.ml b/test/test_harness.ml index 1852774..b71541c 100644 --- a/test/test_harness.ml +++ b/test/test_harness.ml @@ -92,3 +92,17 @@ let check_message name expected thunk = match error_of thunk with | None -> fail name "expected a diagnostic" | Some diagnostic -> check_equal_string name expected diagnostic.Diagnostic.message + +type rng = { mutable state : int } + +let rng seed = { state = seed land 0x3FFFFFFF } + +let next rng = + rng.state <- (rng.state * 1103515245 + 12345) land 0x3FFFFFFF; + rng.state + +let range rng bound = if bound <= 0 then 0 else next rng mod bound + +let pick rng items = List.nth items (range rng (List.length items)) + +let string_of_int_list items = Util.join "," (List.map string_of_int items) diff --git a/test/test_harness.mli b/test/test_harness.mli index 3297602..06f7c59 100644 --- a/test/test_harness.mli +++ b/test/test_harness.mli @@ -21,3 +21,11 @@ val parse_error : string -> Diagnostic.t option val resolve_error : string -> Diagnostic.t option val infer_error : string -> Diagnostic.t option val check_message : string -> string -> (unit -> 'a) -> unit + +type rng = { mutable state : int } + +val rng : int -> rng +val next : rng -> int +val range : rng -> int -> int +val pick : rng -> 'a list -> 'a +val string_of_int_list : int list -> string diff --git a/test/test_main.ml b/test/test_main.ml index 21e40a7..8c27bbd 100644 --- a/test/test_main.ml +++ b/test/test_main.ml @@ -376,6 +376,7 @@ let () = Test_harness.run_suite "types" Test_type.cases; Test_harness.run_suite "specialize" Test_type.specialize_cases; Test_harness.run_suite "anf" Test_type.anf_cases; + Test_harness.run_suite "changes" Test_change.law_cases; Test_harness.run_suite "interpret" Test_incremental.cases; Printf.printf "%d cases, %d failures\n" (Test_harness.case_count ()) (Test_harness.failure_count ()); exit (if Test_harness.failure_count () = 0 then 0 else 1)