open Test_harness let infer_program text = infer text let cases = [ ( "the example query infers a collection of tuples of string and int", fun () -> let program = infer_program (read_fixture "expensive_order.delta") in check_equal_string "query type" "collection (string, int)" (Types.pp program.Typed.tp_query_body.Typed.ty); check_equal_string "input element" "order" (Types.pp program.Typed.tp_input_element) ); ( "the example helper infers an integer arrow", fun () -> let program = infer_program (read_fixture "expensive_order.delta") in check_equal_string "helper type" "(int -> int)" (Types.pp (List.hd program.Typed.tp_helpers).Typed.th_scheme.Types.body) ); ( "revenue infers an integer query", fun () -> let program = infer_program (read_fixture "revenue.delta") in check_equal_string "query type" "int" (Types.pp program.Typed.tp_query_body.Typed.ty) ); ( "count_large infers an integer query", fun () -> let program = infer_program (read_fixture "count_large.delta") in check_equal_string "query type" "int" (Types.pp program.Typed.tp_query_body.Typed.ty) ); ( "a helper generalizes at its let binding", fun () -> let program = infer_program "type order = { customer : string; total : int }\ninput orders : collection order\nlet pair a b = (a, b)\nquery q = orders |> map (fun o -> pair o.total o.customer)\n" in let scheme = (List.hd program.Typed.tp_helpers).Typed.th_scheme in check_equal_int "two generalized variables" 2 (List.length scheme.Types.vars); check "the helper is a two argument function" (match Types.repr scheme.Types.body with | Types.TArrow (_, Types.TArrow _) -> true | _ -> false); check_equal_string "query type" "collection (int, string)" (Types.pp program.Typed.tp_query_body.Typed.ty) ); ( "a polymorphic helper is instantiated independently at each use", fun () -> let program = infer_program "type order = { customer : string; total : int }\ninput orders : collection order\nlet identity x = x\nlet tax n = identity n * 20 / 100\nquery q = orders |> map (fun o -> (identity o.customer, tax o.total))\n" in check_equal_string "query type" "collection (string, int)" (Types.pp program.Typed.tp_query_body.Typed.ty) ); ( "the occurs check rejects self application", fun () -> match infer_error "input rows : collection int\nlet f x = x x\nquery q = rows\n" with | None -> fail "occurs" "expected a diagnostic" | Some diagnostic -> check "message mentions an infinite type" (Util.starts_with "cannot construct the infinite type" diagnostic.Diagnostic.message) ); ( "an unannotated arithmetic helper that is applied to a string is rejected", fun () -> check_message "arithmetic" "type mismatch: expected int but got string" (fun () -> infer_program "input rows : collection int\nlet f n = n + 1\nquery q = rows |> map (fun r -> f \"a\")\n") ); ( "projection on a non record is rejected", fun () -> check_message "projection" "cannot project field `total` from a value of type int" (fun () -> infer_program "type order = { total : int }\ninput rows : collection int\nquery q = rows |> map (fun r -> r.total)\n") ); ( "unknown record fields are rejected", fun () -> check_message "unknown field" "no record type declares a field named `tota`" (fun () -> infer_program "type order = { total : int }\ninput rows : collection order\nquery q = rows |> map (fun r -> r.tota)\n") ); ( "record literals must provide every field", fun () -> check_message "missing field" "record literal of type `order` is missing field `customer`" (fun () -> infer_program "type order = { customer : string; total : int }\ninput rows : collection order\nquery q = rows |> map (fun r -> { total = r.total })\n") ); ( "record literals reject fields of another record", fun () -> check_message "mixed fields" "record `order` has no field named `other`" (fun () -> infer_program "type order = { total : int }\ninput rows : collection order\nquery q = rows |> map (fun r -> { total = r.total; other = 1 })\n") ); ( "a record field with a collection type is rejected", fun () -> check_message "collection field" "record field `items` has a collection type; collections may not be stored in records" (fun () -> infer_program "type box = { items : collection int }\ninput rows : collection box\nquery q = rows\n") ); ( "nested collection types are rejected", fun () -> check_message "collection type position" "collection types are only allowed as the input type and as query results" (fun () -> infer_program "input rows : collection (collection int)\nquery q = rows\n") ); ( "the input must be declared with a collection type", fun () -> check_message "input type" "the input collection must be declared with a collection type: input NAME : collection T" (fun () -> infer_program "input rows : int\nquery q = 1\n") ); ( "sum rejects a non integer collection", fun () -> check_message "sum" "sum expects a collection of integers but got collection string" (fun () -> infer_program "type order = { customer : string }\ninput rows : collection order\nquery q = rows |> map (fun r -> r.customer) |> sum\n") ); ( "sum rejects a scalar operand", fun () -> check_message "sum scalar" "sum expects a collection of integers but got int" (fun () -> infer_program "input rows : collection int\nquery q = sum 1\n") ); ( "filter must be applied to a collection", fun () -> check_message "filter arity" "`filter` and `map` must be applied to a collection" (fun () -> infer_program "input rows : collection int\nquery q = filter (fun x -> true)\n") ); ( "map cannot produce a collection", fun () -> check_message "nested collection" "nested collections are not supported: mapped element" (fun () -> infer_program "input rows : collection int\nquery q = rows |> map (fun r -> rows)\n") ); ( "count rejects a scalar operand", fun () -> check_message "count scalar" "count expects a collection but got int" (fun () -> infer_program "input rows : collection int\nquery q = count 1\n") ); ( "a query must produce a collection or an integer", fun () -> check_message "query result" "a query must produce a collection or an integer, but this query produces string" (fun () -> infer_program "input rows : collection int\nquery q = \"hello\"\n") ); ( "equality is rejected on functions", fun () -> check_message "function equality" "`=` is only supported on integers, booleans, strings, unit, tuples and records of these, but the operands have type (int -> int)" (fun () -> infer_program "input rows : collection int\nlet bad = (fun x -> x + 1) = (fun x -> x + 1)\nquery q = rows\n" ) ); ( "conditional branches must have the same type", fun () -> check_message "branch mismatch" "type mismatch: expected int but got string" (fun () -> infer_program "input rows : collection int\nquery q = if true then 1 else \"x\"\n") ); ( "unknown type names are rejected", fun () -> check_message "unknown type" "unknown type `order`" (fun () -> infer_program "input rows : collection order\nquery q = rows\n") ); ( "negation is integer only", fun () -> check_message "negation" "type mismatch: expected bool but got int" (fun () -> infer_program "input rows : collection int\nquery q = -true\n") ); ( "a constant integer query is accepted", fun () -> let program = infer_program "input rows : collection int\nquery q = 40 + 2\n" in check_equal_string "query type" "int" (Types.pp program.Typed.tp_query_body.Typed.ty) ); ( "the typed dump is deterministic", fun () -> Types.reset (); Ident.reset (); let first = Typed.program_to_string (infer_program (read_fixture "expensive_order.delta")) in Types.reset (); Ident.reset (); let second = Typed.program_to_string (infer_program (read_fixture "expensive_order.delta")) in check_equal_string "identical dumps" first second ); ( "nested record projections are typed", fun () -> let program = infer_program "type inner = { amount : int }\ntype outer = { inner : inner; label : string }\ninput rows : collection outer\nquery q = rows |> map (fun r -> (r.inner.amount, r.label))\n" in check_equal_string "query type" "collection (int, string)" (Types.pp program.Typed.tp_query_body.Typed.ty) ); ( "projecting a field of another record is rejected", fun () -> check_message "wrong record" "cannot project field `amount` from a value of type outer" (fun () -> infer_program "type inner = { amount : int }\ntype outer = { inner : inner }\ninput rows : collection outer\nquery q = rows |> map (fun r -> r.amount)\n") ); ( "projecting from a scalar is rejected", fun () -> check_message "scalar projection" "cannot project field `amount` from a value of type int" (fun () -> infer_program "type inner = { amount : int }\ninput rows : collection int\nquery q = rows |> map (fun r -> r.amount)\n") ); ( "a filter predicate must return bool", fun () -> check_message "predicate type" "type mismatch: expected int but got bool" (fun () -> infer_program "type order = { total : int }\ninput rows : collection order\nquery q = rows |> filter (fun r -> r.total)\n") ); ( "a map projection may not return a function", fun () -> check_message "function element" "collections of functions are not supported: mapped element" (fun () -> infer_program "input rows : collection int\nquery q = rows |> map (fun r -> fun x -> r + x)\n") ); ( "collections may not appear inside tuples", fun () -> check_message "collection in tuple" "collections may not appear inside tuples, but this component has type collection int" (fun () -> infer_program "input rows : collection int\nquery q = (rows, 1)\n") ); ( "a collection cannot be stored in a record field", fun () -> check_message "collection in record" "type mismatch: expected collection int but got int" (fun () -> infer_program "type box = { items : int }\ninput rows : collection int\nquery q = rows |> map (fun r -> { items = rows })\n") ); ( "filter and map over a helper name are typed", fun () -> let program = infer_program "type order = { total : int }\ninput rows : collection order\nlet big o = o.total > 1000\nlet value o = o.total\nquery q = rows |> filter big |> map value\n" in check_equal_string "query type" "collection int" (Types.pp program.Typed.tp_query_body.Typed.ty) ); ] let rec binder_stamps expr acc = let walk = binder_stamps in match expr.Typed.te with | Typed.TLet (ident, bound, body) -> walk body (walk bound (Ident.stamp ident :: acc)) | Typed.TLambda (ident, body) -> walk body (Ident.stamp ident :: acc) | Typed.TApp (fn, argument) -> walk argument (walk fn acc) | Typed.TIf (a, b, c) -> walk c (walk b (walk a acc)) | Typed.TBinop (_, a, b) -> walk b (walk a acc) | Typed.TTuple items -> List.fold_left (fun acc item -> walk item acc) acc items | Typed.TRecord (_, fields) -> List.fold_left (fun acc (_, value) -> walk value acc) acc fields | Typed.TField (record, _) -> walk record acc | Typed.TFilter (collection, predicate) -> walk predicate (walk collection acc) | Typed.TMap (collection, projection) -> walk projection (walk collection acc) | Typed.TSum collection | Typed.TCount collection -> walk collection acc | Typed.TInt _ | Typed.TBool _ | Typed.TString _ | Typed.TUnit | Typed.TVar _ | Typed.TSource _ -> acc let stamp_unique stamps = let seen = Hashtbl.create 32 in let rec check = function | [] -> true | stamp :: rest -> if Hashtbl.mem seen stamp then false else (Hashtbl.add seen stamp (); check rest) in check stamps let rec collect_map_functions expr acc = match expr.Typed.te with | Typed.TMap (collection, projection) -> collect_map_functions collection (("map", projection) :: acc) | Typed.TFilter (collection, predicate) -> collect_map_functions collection (("filter", predicate) :: acc) | Typed.TSum collection | Typed.TCount collection -> collect_map_functions collection acc | Typed.TLet (_, bound, body) -> collect_map_functions body (collect_map_functions bound acc) | _ -> acc let function_is_lambda expr = match expr.Typed.te with Typed.TLambda _ -> true | _ -> false let rec has_let expr = match expr.Typed.te with | Typed.TLet (_, _, _) -> true | Typed.TLambda (_, body) -> has_let body | Typed.TApp (fn, argument) -> has_let fn || has_let argument | Typed.TIf (a, b, c) -> has_let a || has_let b || has_let c | Typed.TBinop (_, a, b) -> has_let a || has_let b | Typed.TTuple items -> List.exists has_let items | Typed.TRecord (_, fields) -> List.exists (fun (_, value) -> has_let value) fields | Typed.TField (record, _) -> has_let record | Typed.TFilter (collection, predicate) -> has_let collection || has_let predicate | Typed.TMap (collection, projection) -> has_let collection || has_let projection | Typed.TSum collection | Typed.TCount collection -> has_let collection | Typed.TInt _ | Typed.TBool _ | Typed.TString _ | Typed.TUnit | Typed.TVar _ | Typed.TSource _ -> false let specialize text = Specialize.program (infer text) let specialize_cases = [ ( "inlining a helper twice does not duplicate binder stamps", fun () -> Ident.reset (); let program = specialize "input rows : collection int\nlet scale n = n * 2\nlet quad n = scale (scale n)\nquery q = rows |> map (fun r -> quad r + quad r)\n" in check "all binders are distinct" (stamp_unique (binder_stamps program.Typed.tp_query_body [])) ); ( "a helper used as a mapping function specializes to a lambda", fun () -> let program = specialize "type order = { total : int }\ninput rows : collection order\nlet value o = o.total\nquery q = rows |> map value\n" in let functions = collect_map_functions program.Typed.tp_query_body [] in check "map function is a lambda" (List.for_all (fun (_, fn) -> function_is_lambda fn) functions) ); ( "a helper used as a predicate specializes to a lambda", fun () -> let program = specialize "type order = { total : int }\ninput rows : collection order\nlet big o = o.total > 1000\nquery q = rows |> filter big |> count\n" in let functions = collect_map_functions program.Typed.tp_query_body [] in check_equal_int "one collection function" 1 (List.length functions); check "filter predicate is a lambda" (List.for_all (fun (_, fn) -> function_is_lambda fn) functions) ); ( "higher order helpers specialize at their call sites", fun () -> let program = specialize "input rows : collection int\nlet twice f x = f (f x)\nlet inc n = n + 1\nquery q = rows |> map (fun r -> twice inc r) |> sum\n" in check_equal_int "no helper references remain" 0 (List.length (collect_map_functions program.Typed.tp_query_body []) - 1) ); ( "an escaping function value is rejected", fun () -> check_message "escaping function" "the mapping function must be a function literal or a helper that specializes to one, but this expression is a function value" (fun () -> specialize "input rows : collection int\nlet choose b = if b then (fun n -> n) else (fun n -> n + 1)\nquery q = rows |> map (choose true)\n") ); ( "a predicate that uses the input collection is rejected", fun () -> check_message "captured collection" "the predicate cannot be incrementalized because it uses `rows` from the surrounding scope" (fun () -> specialize "input rows : collection int\nquery q = rows |> filter (fun r -> r > count rows) |> count\n") ); ( "plain let bindings are inlined into the query", fun () -> let program = specialize "input rows : collection int\nquery q = let base = 10 in rows |> map (fun r -> r + base) |> sum\n" in check "no let bindings survive" (not (has_let program.Typed.tp_query_body)) ); ]