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"))) ); ]