Derive scalar changes and composition laws
This commit is contained in:
10 files changed
+527
-3
No files matched your search
@@ -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"))) );
|
||||
]
|
||||
|
||||
Reference in new issue
Block a user